val seq_hide
  (#t: Secret.inttype { Secret.unsigned t })
  (x: seq (Secret.uint_t t Secret.PUB))
: Tot (seq (Secret.uint_t t Secret.SEC))
val seq_hide
  (#t: Secret.inttype { Secret.unsigned t })
  (x: seq (Secret.uint_t t Secret.PUB))
: Tot (seq (Secret.uint_t t Secret.SEC))
let seq_hide
  #t x
= seq_map (Secret.cast t Secret.SEC) 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)
/
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
x: FStar.Seq.Base.seq (Lib.IntTypes.uint_t t Lib.IntTypes.PUB)
  -> FStar.Seq.Base.seq (Lib.IntTypes.uint_t t Lib.IntTypes.SEC)
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned FStar.Seq.Base.seq Lib.IntTypes.uint_t Lib.IntTypes.PUB QUIC.Secret.Seq.seq_map Lib.IntTypes.SEC Lib.IntTypes.cast
let seq_hide #t x =
  
seq_map (Secret.cast t Secret.SEC) x