val seq_reveal_index'
      (#t: Secret.inttype{Secret.unsigned t})
      (#sec: Secret.secrecy_level)
      (x: seq (Secret.uint_t t sec))
      (i: nat)
    : Lemma (requires (i < length x))
      (ensures (index (seq_reveal x) i == Secret.reveal (index x i)))
      [SMTPat (index (seq_reveal x) i)]
let seq_reveal_index'
  (#t: Secret.inttype { Secret.unsigned t })
  (#sec: Secret.secrecy_level)
  (x: seq (Secret.uint_t t sec))
  (i: nat)
: Lemma
  (requires (i < length x))
  (ensures (
    index (seq_reveal x) i == Secret.reveal (index x i)
  ))
  [SMTPat (index (seq_reveal x) i)]
= seq_reveal_index x i
val seq_reveal_index'
      (#t: Secret.inttype{Secret.unsigned t})
      (#sec: Secret.secrecy_level)
      (x: seq (Secret.uint_t t sec))
      (i: nat)
    : Lemma (requires (i < length x))
      (ensures (index (seq_reveal x) i == Secret.reveal (index x i)))
      [SMTPat (index (seq_reveal x) i)]
let seq_reveal_index'
      (#t: Secret.inttype{Secret.unsigned t})
      (#sec: Secret.secrecy_level)
      (x: seq (Secret.uint_t t sec))
      (i: nat)
    : Lemma (requires (i < length x))
      (ensures (index (seq_reveal x) i == Secret.reveal (index x i)))
      [SMTPat (index (seq_reveal x) i)] =
seq_reveal_index x i
QUIC.Secret.Seq.fsti.checked
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.fsti
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned Lib.IntTypes.secrecy_level FStar.Seq.Base.seq Lib.IntTypes.uint_t Prims.nat QUIC.Secret.Seq.seq_reveal_index Prims.unit Prims.op_LessThan FStar.Seq.Base.length Prims.squash Prims.eq2 Lib.IntTypes.PUB FStar.Seq.Base.index QUIC.Secret.Seq.seq_reveal QUIC.Secret.Int.reveal Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module QUIC.Secret.Seq
include FStar.Seq

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

noextract
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_length
  (#t: Secret.inttype { Secret.unsigned t })
  (x: seq (Secret.uint_t t Secret.PUB))
: Lemma
  (length (seq_hide x) == length x)
  [SMTPat (length (seq_hide x))]

val seq_hide_index
  (#t: Secret.inttype { Secret.unsigned t })
  (x: seq (Secret.uint_t t Secret.PUB))
  (i: nat)
: Lemma
  (requires (i < length x))
  (ensures (
    Secret.v (index (seq_hide x) i) == Secret.v (index x i)
  ))

let seq_hide_index'
  (#t: Secret.inttype { Secret.unsigned t })
  (x: seq (Secret.uint_t t Secret.PUB))
  (i: nat)
: Lemma
  (requires (i < length x))
  (ensures (
    index (seq_hide x) i == Secret.hide #t (index x i)
  ))
  [SMTPat (index (seq_hide x) i)]
= seq_hide_index x i

val seq_reveal
  (#t: Secret.inttype { Secret.unsigned t })
  (#sec: Secret.secrecy_level)
  (x: seq (Secret.uint_t t sec))
: GTot (seq (Secret.uint_t t Secret.PUB))

val seq_reveal_length
  (#t: Secret.inttype { Secret.unsigned t })
  (#sec: Secret.secrecy_level)
  (x: seq (Secret.uint_t t sec))
: Lemma
  (length (seq_reveal x) == length x)
  [SMTPat (length (seq_reveal x))]

val seq_reveal_index
  (#t: Secret.inttype { Secret.unsigned t })
  (#sec: Secret.secrecy_level)
  (x: seq (Secret.uint_t t sec))
  (i: nat)
: Lemma
  (requires (i < length x))
  (ensures (
    Secret.v (index (seq_reveal x) i) == Secret.v (index x i)
  ))

let seq_reveal_index'
  (#t: Secret.inttype { Secret.unsigned t })
  (#sec: Secret.secrecy_level)
  (x: seq (Secret.uint_t t sec))
  (i: nat)
: Lemma
  (requires (i < length x))
  (ensures (
    index (seq_reveal x) i == Secret.reveal (index x i)
  ))
val seq_reveal_index'
      (#t: Secret.inttype{Secret.unsigned t})
      (#sec: Secret.secrecy_level)
      (x: seq (Secret.uint_t t sec))
      (i: nat)
    : Lemma (requires (i < length x))
      (ensures (index (seq_reveal x) i == Secret.reveal (index x i)))
      [SMTPat (index (seq_reveal x) i)]
x: FStar.Seq.Base.seq (Lib.IntTypes.uint_t t sec) -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires i < FStar.Seq.Base.length x)
      (ensures
        FStar.Seq.Base.index (QUIC.Secret.Seq.seq_reveal x) i ==
        QUIC.Secret.Int.reveal (FStar.Seq.Base.index x i))
      [SMTPat (FStar.Seq.Base.index (QUIC.Secret.Seq.seq_reveal x) i)]