val 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 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
val 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 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
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.UInt32.t FStar.Bytes.byte FStar.Seq.Base.lemma_eq_elim Prims.unit FStar.Seq.Base.lemma_eq_intro FStar.Classical.forall_intro Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert Prims.eq2 FStar.Bytes.get FStar.UInt32.uint_to_t FStar.Seq.Base.index Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length FStar.Seq.Base.seq FStar.UInt8.t FStar.Seq.Base.create FStar.UInt32.v FStar.Bytes.reveal FStar.Bytes.lbytes Prims.l_Forall FStar.UInt32.lt FStar.Bytes.create Prims.Cons FStar.Pervasives.smt_pat
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)
val b32_reveal_create (len: U32.t) (v: byte)
    : Lemma (reveal (create len v) == Seq.create (U32.v len) v) [SMTPat (reveal (create len v))]
len: FStar.UInt32.t -> v: FStar.Bytes.byte
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Bytes.reveal (FStar.Bytes.create len v) ==
        FStar.Seq.Base.create (FStar.UInt32.v len) v)
      [SMTPat (FStar.Bytes.reveal (FStar.Bytes.create len v))]