val test_incremental_api: Prims.unit -> St unit
let test_incremental_api (): St unit =
  // Note: this function cannot be in the Stack effect because it performs some
  // allocations (even though it frees them afterwards).
  push_frame ();
  let b1 = B.alloca_of_list [ u8 0x00; u8 0x01; u8 0x02; u8 0x04 ] in
  let b2 = B.alloca_of_list [ u8 0x05; u8 0x06; u8 0x07; u8 0x08 ] in

  let st = HI.create_in SHA2_256 HyperStack.root in
  HI.init (G.hide SHA2_256) st;
  let h0 = ST.get () in
  assert B.(loc_disjoint (S.footprint HI.evercrypt_hash SHA2_256 h0 st) (loc_buffer b1));
  assert (S.seen HI.evercrypt_hash SHA2_256 h0 st `Seq.equal` Seq.empty);

  assert_norm (4 < pow2 61);
  let EverCrypt.Error.Success = HI.update (G.hide SHA2_256) st b1 4ul in
  let h1 = ST.get () in
  assert (HI.hashed h1 st `Seq.equal` (Seq.append Seq.empty (B.as_seq h0 b1)));
  Seq.append_empty_l (B.as_seq h0 b1);
  assert (HI.hashed h1 st `Seq.equal` (B.as_seq h0 b1));

  assert (Seq.length (Ghost.reveal (Ghost.hide (B.as_seq h0 b1))) = 4);
  assert_norm (8 < pow2 61);
  let EverCrypt.Error.Success = HI.update (G.hide SHA2_256) st b2 4ul in
  let h2 = ST.get () in
  assert (HI.hashed h2 st `Seq.equal` (Seq.append (B.as_seq h0 b1) (B.as_seq h0 b2)));

  // An example of how to call the hash preservation lemma...
  let dst = B.alloca (u8 0) 32ul in
  let h3 = ST.get () in
  // Auto-framing!
  HI.finish (G.hide SHA2_256) st dst ();

  let h4 = ST.get () in
  assert (Seq.equal (B.as_seq h4 dst)
    (Spec.Agile.Hash.hash SHA2_256 (Seq.append (B.as_seq h0 b1) (B.as_seq h0 b2))));

  HI.free (G.hide SHA2_256) st;
  pop_frame ()
val test_incremental_api: Prims.unit -> St unit
let test_incremental_api () : St unit =
push_frame ();
let b1 = B.alloca_of_list [u8 0x00; u8 0x01; u8 0x02; u8 0x04] in
let b2 = B.alloca_of_list [u8 0x05; u8 0x06; u8 0x07; u8 0x08] in
let st = HI.create_in SHA2_256 HyperStack.root in
HI.init (G.hide SHA2_256) st;
let h0 = ST.get () in
assert B.(loc_disjoint (S.footprint HI.evercrypt_hash SHA2_256 h0 st) (loc_buffer b1));
assert ((S.seen HI.evercrypt_hash SHA2_256 h0 st) `Seq.equal` Seq.empty);
assert_norm (4 < pow2 61);
let EverCrypt.Error.Success = HI.update (G.hide SHA2_256) st b1 4ul in
let h1 = ST.get () in
assert ((HI.hashed h1 st) `Seq.equal` (Seq.append Seq.empty (B.as_seq h0 b1)));
Seq.append_empty_l (B.as_seq h0 b1);
assert ((HI.hashed h1 st) `Seq.equal` (B.as_seq h0 b1));
assert (Seq.length (Ghost.reveal (Ghost.hide (B.as_seq h0 b1))) = 4);
assert_norm (8 < pow2 61);
let EverCrypt.Error.Success = HI.update (G.hide SHA2_256) st b2 4ul in
let h2 = ST.get () in
assert ((HI.hashed h2 st) `Seq.equal` (Seq.append (B.as_seq h0 b1) (B.as_seq h0 b2)));
let dst = B.alloca (u8 0) 32ul in
let h3 = ST.get () in
HI.finish (G.hide SHA2_256) st dst ();
let h4 = ST.get () in
assert (Seq.equal (B.as_seq h4 dst)
      (Spec.Agile.Hash.hash SHA2_256 (Seq.append (B.as_seq h0 b1) (B.as_seq h0 b2))));
HI.free (G.hide SHA2_256) st;
pop_frame ()
Test.Hash.fst.checked
Spec.Hash.Lemmas.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Hacl.Streaming.Functor.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Hash.Incremental.fst.checked
Test.Hash.fst
Prims.unit FStar.HyperStack.ST.pop_frame EverCrypt.Hash.Incremental.free FStar.Ghost.hide EverCrypt.Hash.alg Spec.Hash.Definitions.SHA2_256 Prims._assert FStar.Seq.Base.equal Hacl.Streaming.Functor.uint8 LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder Spec.Agile.Hash.hash FStar.Seq.Base.append Hacl.Streaming.Interface.uint8 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get EverCrypt.Hash.Incremental.finish LowStar.Monotonic.Buffer.mbuffer Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.alloca Lib.IntTypes.u8 FStar.UInt32.__uint_to_t EverCrypt.Hash.Incremental.hashed EverCrypt.Error.error_code EverCrypt.Hash.Incremental.update FStar.Pervasives.assert_norm Prims.op_LessThan Prims.pow2 Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Ghost.reveal FStar.Seq.Base.seq FStar.Seq.Base.append_empty_l FStar.Seq.Base.empty Hacl.Streaming.Functor.seen Spec.Hash.Definitions.fixed_len_alg EverCrypt.Hash.Incremental.evercrypt_hash LowStar.Monotonic.Buffer.loc_disjoint Hacl.Streaming.Functor.footprint LowStar.Monotonic.Buffer.loc_buffer EverCrypt.Hash.Incremental.init Hacl.Streaming.Functor.state EverCrypt.Hash.state FStar.Ghost.erased EverCrypt.Hash.Incremental.create_in FStar.Monotonic.HyperHeap.root FStar.Pervasives.normalize_term FStar.List.Tot.Base.length Prims.Cons Lib.IntTypes.mk_int Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.Nil LowStar.Buffer.alloca_of_list FStar.HyperStack.ST.push_frame
module Test.Hash

module HI = EverCrypt.Hash.Incremental
module S = Hacl.Streaming.Functor

module ST = FStar.HyperStack.ST
module M = LowStar.Modifies

module MP = LowStar.ModifiesPat

module B = LowStar.Buffer
module G = FStar.Ghost

open LowStar.BufferOps
open Spec.Hash.Definitions
open Spec.Hash.Lemmas
open Lib.IntTypes

open FStar.HyperStack.ST


#set-options "--max_fuel 0 --max_ifuel 0"
let main (): St unit =
  // Nothing here: EverCrypt.Hash is no longer a public API, all clients
  // expected to go through HI
  ()

#push-options "--z3rlimit 100 --fuel 1 --ifuel 1"
let test_incremental_api (): St unit =
  // Note: this function cannot be in the Stack effect because it performs some
val test_incremental_api: Prims.unit -> St unit
_: Prims.unit -> FStar.HyperStack.ST.St Prims.unit