val seq_gmap (#t1 #t2: Type) (f: (t1 -> GTot t2)) (x: seq t1)
    : GTot (lseq t2 (length x)) (decreases (length x))
val seq_gmap (#t1 #t2: Type) (f: (t1 -> GTot t2)) (x: seq t1)
    : GTot (lseq t2 (length x)) (decreases (length x))
let rec seq_gmap
  (#t1 #t2: Type)
  (f: (t1 -> GTot t2))
  (x: seq t1)
: GTot (lseq t2 (length x))
  (decreases (length x))
= if length x = 0
  then empty
  else cons (f (head x)) (seq_gmap f (tail x))
module QUIC.Secret.Seq
open FStar.Seq

module Secret = QUIC.Secret.Int
module U8 = FStar.UInt8
module Ghost = FStar.Ghost

(* NOTE: abstraction is NOT broken here *)

noextract
let rec seq_map
  (#t1 #t2: Type)
  (f: (t1 -> Tot t2))
  (x: seq t1)
: Tot (lseq t2 (length x))
  (decreases (length x))
= if length x = 0
  then empty
  else cons (f (head x)) (seq_map f (tail x))

let rec seq_map_index
  (#t1 #t2: Type)
  (f: (t1 -> Tot t2))
  (x: seq t1)
  (i: nat { i < length x })
: Lemma
  (ensures (index (seq_map f x) i == f (index x i)))
  (decreases (length x))
  [SMTPat (index (seq_map f x) i)]
= if i = 0
  then ()
  else seq_map_index f (tail x) (i - 1)

let seq_hide
  #t x
= seq_map (Secret.cast t Secret.SEC) x

let seq_hide_length
  #t x
= ()

#push-options "--z3rlimit 32"

let seq_hide_index
  #t x i
= ()

#pop-options
/
QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
QUIC.Secret.Seq.fst
f: (_: t1 -> Prims.GTot t2) -> x: FStar.Seq.Base.seq t1
  -> Prims.GTot (FStar.Seq.Properties.lseq t2 (FStar.Seq.Base.length x))
FStar.Seq.Base.seq Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.empty Prims.bool FStar.Seq.Base.cons FStar.Seq.Properties.head QUIC.Secret.Seq.seq_gmap FStar.Seq.Properties.tail FStar.Seq.Properties.lseq
let rec seq_gmap (#t1 #t2: Type) (f: (t1 -> GTot t2)) (x: seq t1)
    : GTot (lseq t2 (length x)) (decreases (length x)) =
  
if length x = 0 then empty else cons (f (head x)) (seq_gmap f (tail x))