val reveal_eq (b: Seq.seq Lib.IntTypes.uint8)
    : Lemma (ensures reveal #(Seq.length b) b == QUIC.Secret.Seq.seq_reveal b)
      [SMTPat (QUIC.Secret.Seq.seq_reveal b)]
val reveal_eq (b: Seq.seq Lib.IntTypes.uint8)
    : Lemma (ensures reveal #(Seq.length b) b == QUIC.Secret.Seq.seq_reveal b)
      [SMTPat (QUIC.Secret.Seq.seq_reveal b)]
let reveal_eq (b:Seq.seq Lib.IntTypes.uint8): Lemma
  (ensures reveal #(Seq.length b) b == QUIC.Secret.Seq.seq_reveal b)
  [ SMTPat (QUIC.Secret.Seq.seq_reveal b) ]
= 
  assert (reveal #(Seq.length b) b `Seq.equal` QUIC.Secret.Seq.seq_reveal b)
module Model.Helpers

let lbytes (l:nat) = b:Seq.seq Lib.IntTypes.uint8 { Seq.length b = l }

let hide (b:Seq.seq UInt8.t) : lbytes (Seq.length b) =
  Seq.init (Seq.length b) (fun i -> Lib.RawIntTypes.u8_from_UInt8 (Seq.index b i))

let hide_eq (b:Seq.seq UInt8.t) : Lemma
  (ensures hide b == QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)
  [ SMTPat (QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b) ]
= 
  assert (hide b `Seq.equal` QUIC.Secret.Seq.seq_hide b)

let reveal #l (b:lbytes l) : (QUIC.Spec.lbytes l) =
  Seq.init l (fun i -> Lib.RawIntTypes.u8_to_UInt8 (Seq.index b i))
/
QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.RandomSequence.fsti.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
Model.Helpers.fsti
b: FStar.Seq.Base.seq Lib.IntTypes.uint8
  -> FStar.Pervasives.Lemma (ensures Model.Helpers.reveal b == QUIC.Secret.Seq.seq_reveal b)
      [SMTPat (QUIC.Secret.Seq.seq_reveal b)]
FStar.Seq.Base.seq Lib.IntTypes.uint8 Prims._assert FStar.Seq.Base.equal QUIC.Spec.Base.byte Model.Helpers.reveal FStar.Seq.Base.length QUIC.Secret.Seq.seq_reveal Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Lib.IntTypes.uint_t Lib.IntTypes.PUB Prims.Nil
let reveal_eq (b: Seq.seq Lib.IntTypes.uint8)
    : Lemma (ensures reveal #(Seq.length b) b == QUIC.Secret.Seq.seq_reveal b)
      [SMTPat (QUIC.Secret.Seq.seq_reveal b)] =
  
assert ((reveal #(Seq.length b) b) `Seq.equal` (QUIC.Secret.Seq.seq_reveal b))