val b32_hide (s: Seq.seq FStar.UInt8.t {Seq.length s < pow2 32})
    : Tot (res: bytes{res == hide s}) (decreases (Seq.length s))
let rec b32_hide (s: Seq.seq FStar.UInt8.t { Seq.length s < pow2 32 }) : Tot (res: bytes { res == hide s })
  (decreases (Seq.length s))
=
  let res : bytes =
    if Seq.length s = 0
    then empty_bytes
    else append (create 1ul (Seq.index s 0)) (b32_hide (Seq.slice s 1 (Seq.length s)))
  in
  b32_equal res (hide s);
  res
val b32_hide (s: Seq.seq FStar.UInt8.t {Seq.length s < pow2 32})
    : Tot (res: bytes{res == hide s}) (decreases (Seq.length s))
let rec b32_hide (s: Seq.seq FStar.UInt8.t {Seq.length s < pow2 32})
    : Tot (res: bytes{res == hide s}) (decreases (Seq.length s)) =
let res:bytes =
  if Seq.length s = 0
  then empty_bytes
  else append (create 1ul (Seq.index s 0)) (b32_hide (Seq.slice s 1 (Seq.length s)))
in
b32_equal res (hide s);
res
LowParse.Bytes32.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
LowParse.Bytes32.fst
FStar.Seq.Base.seq FStar.UInt8.t Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.pow2 Prims.unit LowParse.Bytes32.b32_equal FStar.Bytes.hide FStar.Bytes.bytes Prims.op_Equality Prims.int FStar.Bytes.empty_bytes Prims.bool FStar.Bytes.append FStar.Bytes.create FStar.UInt32.__uint_to_t FStar.Seq.Base.index LowParse.Bytes32.b32_hide FStar.Seq.Base.slice Prims.eq2
module LowParse.Bytes32
include FStar.Bytes

module U32 = FStar.UInt32

(* TODO: move to FStar.Bytes *)

inline_for_extraction
let b32slice
  (b: bytes)
  (s: U32.t)
  (e: U32.t)
: Pure bytes
  (requires (U32.v s <= U32.v e /\ U32.v e <= length b))
  (ensures (fun res -> reveal res == Seq.slice (reveal b) (U32.v s) (U32.v e)))
= slice b s e

inline_for_extraction
let b32append
  (b1: bytes)
  (b2: bytes)
: Pure bytes
  (requires (length b1 + length b2 < 4294967296))
  (ensures (fun y -> reveal y == Seq.append (reveal b1) (reveal b2)))
= append b1 b2

let b32_index_reveal
  (b: bytes)
  (i: nat { i < length b })
: Lemma
  (Seq.index (reveal b) i == index b i)
= ()

let b32_reveal_create
  (len: U32.t)
  (v: byte)
: Lemma
  (reveal (create len v) == Seq.create (U32.v len) v)
  [SMTPat (reveal (create len v))]
= let b = create len v in
  let lhs = reveal b in
  let rhs = Seq.create (U32.v len) v in
  let pty = (i: nat { i < Seq.length lhs }) in
  let post
    (i: pty)
  : GTot Type0
  = Seq.index lhs (i <: nat) == Seq.index rhs (i <: nat)
  in
  let f
    (i: pty)
  : Lemma
    (post i)
  = assert (get b (U32.uint_to_t i) == v)
  in
  Classical.forall_intro #pty #post f;
  Seq.lemma_eq_intro lhs rhs;
  Seq.lemma_eq_elim lhs rhs

let reveal_empty' : squash (reveal empty_bytes == Seq.empty) =
  assert (Seq.equal (reveal empty_bytes) Seq.empty)

let reveal_empty () : Lemma
  (reveal empty_bytes == Seq.empty)
= ()

let b32_equal
  (b1 b2: bytes)
: Lemma
  (requires (reveal b1 `Seq.equal` reveal b2))
  (ensures (b1 == b2))
= ()

let rec b32_hide (s: Seq.seq FStar.UInt8.t { Seq.length s < pow2 32 }) : Tot (res: bytes { res == hide s })
val b32_hide (s: Seq.seq FStar.UInt8.t {Seq.length s < pow2 32})
    : Tot (res: bytes{res == hide s}) (decreases (Seq.length s))
s: FStar.Seq.Base.seq FStar.UInt8.t {FStar.Seq.Base.length s < Prims.pow2 32}
  -> Prims.Tot (res: FStar.Bytes.bytes{res == FStar.Bytes.hide s})