val invariant_s_funct :
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  s:state c i t t' ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Pure Type0 (requires
    update_pre c i s data len h0 /\
    U32.v (c.init_input_len i) + S.length (seen c i h0 s) + U32.v len <= U64.v (c.max_input_len i) /\
    state_is_updated c i t t' s data len h0 h1)
  (ensures (fun _ -> True)))
let invariant_s_funct #index c i t t' p data len h0 h1 =
  let blocks, rest = split_at_last_all_seen c i h1 p in
  let s = B.get h1 p 0 in
  let State block_state buf_ total_len seen key = s in
  let key_v = optional_reveal #index #i #c.km #c.key h0 key in
  let init_s = c.init_s i key_v in
  (**) Math.Lemmas.modulo_lemma 0 (U32.v (c.block_len i));
  c.state.v i h1 block_state == c.update_multi_s i init_s 0 blocks /\
  S.equal (S.slice (B.as_seq h1 buf_) 0 (Seq.length rest)) rest
val invariant_s_funct :
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  s:state c i t t' ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Pure Type0 (requires
    update_pre c i s data len h0 /\
    U32.v (c.init_input_len i) + S.length (seen c i h0 s) + U32.v len <= U64.v (c.max_input_len i) /\
    state_is_updated c i t t' s data len h0 h1)
  (ensures (fun _ -> True)))
let invariant_s_funct #index c i t t' p data len h0 h1 =
let blocks, rest = split_at_last_all_seen c i h1 p in
let s = B.get h1 p 0 in
let State block_state buf_ total_len seen key = s in
let key_v = optional_reveal #index #i #c.km #c.key h0 key in
let init_s = c.init_s i key_v in
Math.Lemmas.modulo_lemma 0 (U32.v (c.block_len i));
c.state.v i h1 block_state == c.update_multi_s i init_s 0 blocks /\
S.equal (S.slice (B.as_seq h1 buf_) 0 (Seq.length rest)) rest
Hacl.Streaming.Functor.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.UpdateMulti.fst.checked Lib.IntTypes.fsti.checked Hacl.Streaming.Types.fst.checked Hacl.Streaming.Spec.fst.checked Hacl.Streaming.Interface.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked
Hacl.Streaming.Functor.fst
Hacl.Streaming.Interface.block FStar.Ghost.erased Prims.eq2 Hacl.Streaming.Interface.__proj__Stateful__item__s Hacl.Streaming.Interface.__proj__Block__item__state FStar.Ghost.reveal Hacl.Streaming.Interface.optional_key Hacl.Streaming.Interface.__proj__Block__item__km Hacl.Streaming.Interface.__proj__Block__item__key Hacl.Streaming.Functor.state LowStar.Buffer.buffer Hacl.Streaming.Spec.uint8 FStar.UInt32.t FStar.Monotonic.HyperStack.mem Hacl.Streaming.Spec.bytes Lib.IntTypes.uint8 Prims.b2t Prims.op_Equality LowStar.Monotonic.Buffer.len LowStar.Buffer.trivial_preorder Hacl.Streaming.Interface.__proj__Block__item__blocks_state_len FStar.UInt64.t FStar.Seq.Base.seq Prims.l_and Hacl.Streaming.Interface.__proj__Stateful__item__t Hacl.Streaming.Interface.__proj__Stateful__item__v Hacl.Streaming.Interface.__proj__Block__item__update_multi_s FStar.Seq.Base.equal FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq FStar.Seq.Base.length Prims.unit FStar.Math.Lemmas.modulo_lemma FStar.UInt32.v Hacl.Streaming.Interface.__proj__Block__item__block_len Hacl.Streaming.Interface.__proj__Block__item__init_s Hacl.Streaming.Functor.optional_reveal Hacl.Streaming.Functor.state_s LowStar.Monotonic.Buffer.get FStar.Pervasives.Native.tuple2 Hacl.Streaming.Functor.split_at_last_all_seen
module Hacl.Streaming.Functor

/// Provided an instance of the type class, this creates a streaming API on top.
/// This means that every function in this module takes two extra arguments
/// compared to the previous streaming module specialized for hashes: the type
/// of the index, and a type class for that index. Then, as usual, a given value
/// for the index as a parameter.

#set-options "--max_fuel 0 --max_ifuel 0 \
  --using_facts_from '*,-LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2' --z3rlimit 50"

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module G = FStar.Ghost
module S = FStar.Seq
module U32 = FStar.UInt32
module U64 = FStar.UInt64

open Hacl.Streaming.Interface
open FStar.HyperStack.ST
open LowStar.BufferOps
open FStar.Mul
open Hacl.Streaming.Spec

/// State machinery
/// ===============

/// Little bit of trickery here to make sure state_s is parameterized over
/// something at Type0, not Type0 -> Type0 -- otherwise it wouldn't monomorphize
/// in KaRaMeL.
noeq
type state_s #index (c: block index) (i: index)
  (t: Type0 { t == c.state.s i })
  (t': Type0 { t' == optional_key i c.km c.key })
=
| State:
    block_state: t ->
    buf: B.buffer Lib.IntTypes.uint8 { B.len buf = c.blocks_state_len i } ->
    total_len: UInt64.t ->
    seen: G.erased (S.seq uint8) ->
    // Stupid name conflict on overloaded projectors leads to inscrutable
    // interleaving errors. Need a field name that does not conflict with the
    // one in Hacl.Streaming.Interface. Sigh!!
    p_key: t' ->
    state_s #index c i t t'

/// Defining a series of helpers to deal with the indexed type of the key. This
/// makes proofs easier.

let optional_freeable #index
  (#i: index)
  (#km: key_management)
  (#key: stateful index)
  (h: HS.mem)
  (k: optional_key i km key)
=
  allow_inversion key_management;
  match km with
  | Erased -> True
  | Runtime -> key.freeable #i h k

let optional_invariant #index
  (#i: index)
  (#km: key_management)
  (#key: stateful index)
  (h: HS.mem)
  (k: optional_key i km key)
=
  allow_inversion key_management;
  match km with
  | Erased -> True
  | Runtime -> key.invariant #i h k

let optional_footprint #index
  (#i: index)
  (#km: key_management)
  (#key: stateful index)
  (h: HS.mem)
  (k: optional_key i km key)
=
  allow_inversion key_management;
  match km with
  | Erased -> B.loc_none
  | Runtime -> key.footprint #i h k

let optional_reveal #index
  (#i: index)
  (#km: key_management)
  (#key: stateful index)
  (h: HS.mem)
  (k: optional_key i km key)
=
  allow_inversion key_management;
  match km with
  | Erased -> G.reveal k
  | Runtime -> key.v i h k

let optional_hide #index
  (#i: index)
  (#km: key_management)
  (#key: stateful index)
  (h: HS.mem)
  (k: key.s i):
  optional_key i km key
=
  allow_inversion key_management;
  match km with
  | Erased -> G.hide (key.v i h k)
  | Runtime -> k


/// This lemma is used to convert the Hacl.Streaming.Interface.stateful.frame_freeable
/// lemma, written with freeable in its precondition, into a lemma of the form:
/// [> freeable h0 s => freeable h1 s
val stateful_frame_preserves_freeable:
  #index:Type0 -> #sc:stateful index -> #i:index -> l:B.loc -> s:sc.s i -> h0:HS.mem -> h1:HS.mem ->
  Lemma
  (requires (
    sc.invariant h0 s /\
    B.loc_disjoint l (sc.footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    sc.freeable h0 s ==> sc.freeable h1 s))

let stateful_frame_preserves_freeable #index #sc #i l s h0 h1 =
  let lem h0 h1 :
    Lemma
    (requires (
      sc.invariant h0 s /\
      B.loc_disjoint l (sc.footprint h0 s) /\
      B.modifies l h0 h1 /\
      sc.freeable h0 s))
    (ensures (
       sc.freeable h1 s))
    [SMTPat (sc.freeable h0 s);
     SMTPat (sc.freeable h1 s)] =
     sc.frame_freeable l s h0 h1
  in
  ()

let optional_frame #index
  (#i: index)
  (#km: key_management)
  (#key: stateful index)
  (l: B.loc)
  (s: optional_key i km key)
  (h0 h1: HS.mem):
  Lemma
    (requires (
      optional_invariant h0 s /\
      B.loc_disjoint l (optional_footprint h0 s) /\
      B.modifies l h0 h1))
    (ensures (
      optional_invariant h1 s /\
      optional_reveal h0 s == optional_reveal h1 s /\
      optional_footprint h1 s == optional_footprint h0 s /\
      (optional_freeable h0 s ==> optional_freeable h1 s)))
=
  allow_inversion key_management;
  match km with
  | Erased -> ()
  | Runtime ->
      key.frame_invariant #i l s h0 h1;
      stateful_frame_preserves_freeable #index #key #i l s h0 h1

let footprint_s #index (c: block index) (i: index) (h: HS.mem) s =
  let State block_state buf_ _ _ p_key = s in
  B.(loc_addr_of_buffer buf_ `loc_union` c.state.footprint h block_state `loc_union` optional_footprint h p_key)

/// Invariants
/// ==========

#push-options "--z3cliopt smt.arith.nl=false"
inline_for_extraction noextract
let invariant_s #index (c: block index) (i: index) h s =
  let State block_state buf_ total_len seen key = s in
  let seen = G.reveal seen in
  let key_v = optional_reveal h key in
  let all_seen = S.append (c.init_input_s i key_v) seen in
  let blocks, rest = split_at_last c i all_seen in
  (**) Math.Lemmas.modulo_lemma 0 (U32.v (Block?.block_len c i));
  (**) assert(0 % U32.v (Block?.block_len c i) = 0);
  (**) Math.Lemmas.modulo_lemma 0 (U32.v (Block?.blocks_state_len c i));
  (**) assert(0 % U32.v (Block?.blocks_state_len c i) = 0);

  // Liveness and disjointness (administrative)
  B.live h buf_ /\ c.state.invariant #i h block_state /\ optional_invariant h key /\
  B.(loc_disjoint (loc_buffer buf_) (c.state.footprint h block_state)) /\
  B.(loc_disjoint (loc_buffer buf_) (optional_footprint h key)) /\
  B.(loc_disjoint (optional_footprint h key) (c.state.footprint h block_state)) /\

  // Formerly, the "hashes" predicate
  S.length blocks + S.length rest = U64.v total_len /\
  U32.v (c.init_input_len i) + S.length seen = U64.v total_len /\
  U64.v total_len <= U64.v (c.max_input_len i) /\

  // Note the double equals here, we now no longer know that this is a sequence.
  c.state.v i h block_state == c.update_multi_s i (c.init_s i key_v) 0 blocks /\
  S.equal (S.slice (B.as_seq h buf_) 0 (Seq.length rest)) rest
#pop-options

inline_for_extraction noextract
let freeable_s (#index: Type0) (c: block index) (i: index) (h: HS.mem) (s: state_s' c i): Type0 =
  let State block_state buf_ total_len seen key = s in
  B.freeable buf_ /\ c.state.freeable h block_state /\ optional_freeable h key

let freeable (#index : Type0) (c: block index) (i: index) (h: HS.mem) (s: state' c i) =
  freeable_s c i h (B.get h s 0) /\
  B.freeable s

#push-options "--max_ifuel 1"
let invariant_loc_in_footprint #index c i s m =
  [@inline_let]
  let _ = c.state.invariant_loc_in_footprint #i in
  [@inline_let]
  let _ = c.key.invariant_loc_in_footprint #i in
  ()
#pop-options

let seen #index c i h s =
  G.reveal (State?.seen (B.deref h s))

let seen_bounded #index c i h s =
  ()

let key #index c i h s =
  optional_reveal h (State?.p_key (B.deref h s))

let init_input (#index:Type0) (c:block index) (i:index) (h:HS.mem) (s:state' c i) : GTot bytes =
  c.init_input_s i (key c i h s)

let all_seen (#index:Type0) (c:block index) (i:index) (h:HS.mem) (s:state' c i) : GTot bytes =
  S.append (init_input c i h s) (seen c i h s)

let frame_invariant #index c i l s h0 h1 =
  let state_t = B.deref h0 s in
  let State block_state _ _ _ p_key = state_t in
  c.state.frame_invariant #i l block_state h0 h1;
  stateful_frame_preserves_freeable #index #c.state #i l block_state h0 h1;
  allow_inversion key_management;
  match c.km with
  | Erased -> ()
  | Runtime ->
      stateful_frame_preserves_freeable #index #c.key #i l p_key h0 h1;
      c.key.frame_invariant #i l p_key h0 h1

let frame_seen #_ _ _ _ _ _ _ =
  ()

/// Stateful API
/// ============

let index_of_state #index c i t t' s =
  let open LowStar.BufferOps in
  let State block_state _ _ _ _ = !*s in
  c.index_of_state i block_state

let seen_length #index c i t t' s =
  let open LowStar.BufferOps in
  let State _ _ total_len _ _ = !*s in
  total_len

(* TODO: create_in and alloca have big portions of proofs in common, so it may
 * be possible to factorize them, but it is not clear how *)
#restart-solver
#push-options "--z3rlimit 100"
let create_in #index c i t t' k r =
  [@inline_let] let _ = c.state.invariant_loc_in_footprint #i in
  [@inline_let] let _ = c.key.invariant_loc_in_footprint #i in
  allow_inversion key_management;

  (**) let h0 = ST.get () in

  (**) B.loc_unused_in_not_unused_in_disjoint h0;
  let buf = B.malloc r (Lib.IntTypes.u8 0) (c.blocks_state_len i) in
  (**) let h1 = ST.get () in
  (**) assert (B.fresh_loc (B.loc_buffer buf) h0 h1);
  (**) B.loc_unused_in_not_unused_in_disjoint h1;
  (**) B.(modifies_only_not_unused_in loc_none h0 h1);
  (**) c.key.frame_invariant B.loc_none k h0 h1;

  let block_state = c.state.create_in i r in
  (**) let h2 = ST.get () in
  (**) assert (B.fresh_loc (c.state.footprint #i h2 block_state) h0 h2);
  (**) B.loc_unused_in_not_unused_in_disjoint h2;
  (**) B.(modifies_only_not_unused_in loc_none h1 h2);
  (**) c.key.frame_invariant B.loc_none k h1 h2;

  let k': optional_key i c.km c.key =
    match c.km with
    | Runtime ->
        let k' = c.key.create_in i r in
        (**) let h3 = ST.get () in
        (**) B.loc_unused_in_not_unused_in_disjoint h3;
        (**) B.(modifies_only_not_unused_in loc_none h2 h3);
        (**) c.key.frame_invariant B.loc_none k h2 h3;
        (**) c.state.frame_invariant B.loc_none block_state h2 h3;
        (**) c.state.frame_freeable B.loc_none block_state h2 h3;
        (**) assert (B.fresh_loc (c.key.footprint #i h3 k') h0 h3);
        (**) assert (c.key.invariant #i h3 k');
        (**) assert (c.key.invariant #i h3 k);
        (**) assert B.(loc_disjoint (c.key.footprint #i h3 k) (c.key.footprint #i h3 k'));
        c.key.copy i k k';
        (**) let h4 = ST.get () in
        (**) assert (B.fresh_loc (c.key.footprint #i h4 k') h0 h4);
        (**) B.loc_unused_in_not_unused_in_disjoint h4;
        (**) B.(modifies_only_not_unused_in loc_none h2 h4);
        (**) assert (c.key.invariant #i h4 k');
        (**) c.key.frame_invariant (c.key.footprint #i h3 k') k h3 h4;
        (**) c.state.frame_invariant (c.key.footprint #i h3 k') block_state h3 h4;
        (**) c.state.frame_freeable (c.key.footprint #i h3 k') block_state h3 h4;
        k'
    | Erased ->
        G.hide (c.key.v i h0 k)
  in
  (**) let h5 = ST.get () in
  (**) assert (B.fresh_loc (optional_footprint h5 k') h0 h5);
  (**) assert (B.fresh_loc (c.state.footprint #i h5 block_state) h0 h5);

  [@inline_let] let total_len = Int.Cast.uint32_to_uint64 (c.init_input_len i) in
  let s = State block_state buf total_len (G.hide S.empty) k' in
  (**) assert (B.fresh_loc (footprint_s c i h5 s) h0 h5);

  (**) B.loc_unused_in_not_unused_in_disjoint h5;
  let p = B.malloc r s 1ul in
  (**) let h6 = ST.get () in
  (**) B.(modifies_only_not_unused_in loc_none h5 h6);
  (**) B.(modifies_only_not_unused_in loc_none h0 h6);
  (**) c.key.frame_invariant B.loc_none k h5 h6;
  (**) c.state.frame_invariant B.loc_none block_state h5 h6;
  (**) optional_frame B.loc_none k' h5 h6;
  (**) assert (B.fresh_loc (B.loc_addr_of_buffer p) h0 h6);
  (**) assert (B.fresh_loc (footprint_s c i h6 s) h0 h6);
  (**) c.state.frame_freeable B.loc_none block_state h5 h6;
  (**) assert (optional_reveal h5 k' == optional_reveal h6 k');

  c.init (G.hide i) k buf block_state;
  (**) let h7 = ST.get () in
  (**) assert (B.fresh_loc (c.state.footprint #i h7 block_state) h0 h7);
  (**) assert (B.fresh_loc (B.loc_buffer buf) h0 h7);
  (**) optional_frame (B.loc_union (c.state.footprint #i h7 block_state) (B.loc_buffer buf)) k' h6 h7;
  (**) c.update_multi_zero i (c.state.v i h7 block_state) 0;
  (**) B.modifies_only_not_unused_in B.loc_none h0 h7;
  (**) assert (c.state.v i h7 block_state == c.init_s i (optional_reveal h6 k'));

  (**) let h8 = ST.get () in
  (**) assert (U64.v total_len <= U64.v (c.max_input_len i));

  (**) begin
  (**) let s = B.get h8 p 0 in
  (**) let key_v = key c i h8 p in
  (**) let init_input = c.init_input_s i key_v in
  (**) split_at_last_init c i init_input;
  (**) assert(invariant_s c i h8 s)
  (**) end;
  (**) assert (invariant c i h8 p);

  (**) assert (seen c i h8 p == S.empty);
  (**) assert B.(modifies loc_none h0 h8);
  (**) assert (B.fresh_loc (footprint c i h8 p) h0 h8);
  (**) assert B.(loc_includes (loc_region_only true r) (footprint c i h8 p));

  (**) assert (ST.equal_stack_domains h1 h8);
  (**) assert (ST.equal_stack_domains h0 h1);

  p
#pop-options

#push-options "--z3rlimit 100"
let copy #index c i t t' s0 r =
  [@inline_let] let _ = c.state.invariant_loc_in_footprint #i in
  [@inline_let] let _ = c.key.invariant_loc_in_footprint #i in
  allow_inversion key_management;

  // All source state is suffixed by 0.
  let State block_state0 buf0 total_len0 seen0 k0 = !*s0 in
  let i = c.index_of_state i block_state0 in

  (**) let h0 = ST.get () in

  (**) B.loc_unused_in_not_unused_in_disjoint h0;
  let buf = B.malloc r (Lib.IntTypes.u8 0) (c.blocks_state_len i) in
  B.blit buf0 0ul buf 0ul (c.blocks_state_len i);
  (**) let h1 = ST.get () in
  (**) assert (B.fresh_loc (B.loc_buffer buf) h0 h1);
  (**) B.loc_unused_in_not_unused_in_disjoint h1;
  (**) B.(modifies_only_not_unused_in loc_none h0 h1);
  (**) if c.km = Runtime then
  (**)   c.key.frame_invariant #i B.loc_none k0 h0 h1;
  (**) c.state.frame_invariant #i B.loc_none block_state0 h0 h1;
  (**) assert (invariant c i h1 s0);

  let block_state = c.state.create_in i r in
  (**) let h2 = ST.get () in
  (**) assert (B.fresh_loc (c.state.footprint #i h2 block_state) h0 h2);
  (**) B.loc_unused_in_not_unused_in_disjoint h2;
  (**) B.(modifies_only_not_unused_in loc_none h1 h2);
  (**) if c.km = Runtime then
  (**)   c.key.frame_invariant #i B.loc_none k0 h1 h2;
  (**) c.state.frame_invariant #i B.loc_none block_state0 h0 h1;
  (**) assert (invariant c i h2 s0);

  c.state.copy (G.hide i) block_state0 block_state;
  (**) let h2 = ST.get () in
  (**) B.loc_unused_in_not_unused_in_disjoint h2;
  (**) B.(modifies_only_not_unused_in loc_none h1 h2);
  (**) if c.km = Runtime then
  (**)   c.key.frame_invariant #i (c.state.footprint #i h2 block_state) k0 h1 h2;

  let k': optional_key i c.km c.key =
    match c.km with
    | Runtime ->
        let k' = c.key.create_in i r in
        (**) let h3 = ST.get () in
        (**) B.loc_unused_in_not_unused_in_disjoint h3;
        (**) B.(modifies_only_not_unused_in loc_none h2 h3);
        (**) c.key.frame_invariant #i B.loc_none k0 h2 h3;
        (**) c.state.frame_invariant #i B.loc_none block_state h2 h3;
        (**) c.state.frame_freeable #i B.loc_none block_state h2 h3;
        (**) assert (B.fresh_loc (c.key.footprint #i h3 k') h0 h3);
        (**) assert (c.key.invariant #i h3 k');
        (**) assert (c.key.invariant #i h3 k0);
        (**) assert B.(loc_disjoint (c.key.footprint #i h3 k0) (c.key.footprint #i h3 k'));
        c.key.copy i k0 k';
        (**) let h4 = ST.get () in
        (**) assert (B.fresh_loc (c.key.footprint #i h4 k') h0 h4);
        (**) B.loc_unused_in_not_unused_in_disjoint h4;
        (**) B.(modifies_only_not_unused_in loc_none h2 h4);
        (**) assert (c.key.invariant #i h4 k');
        (**) c.key.frame_invariant #i (c.key.footprint #i h3 k') k0 h3 h4;
        (**) c.state.frame_invariant #i (c.key.footprint #i h3 k') block_state h3 h4;
        (**) c.state.frame_freeable #i (c.key.footprint #i h3 k') block_state h3 h4;
        k'
    | Erased -> k0
  in
  (**) let h5 = ST.get () in
  (**) assert (B.fresh_loc (optional_footprint h5 k') h0 h5);
  (**) assert (B.fresh_loc (c.state.footprint #i h5 block_state) h0 h5);

  let s = State block_state buf total_len0 seen0 k' in
  (**) assert (B.fresh_loc (footprint_s c i h5 s) h0 h5);

  (**) B.loc_unused_in_not_unused_in_disjoint h5;
  let p = B.malloc r s 1ul in
  (**) let h6 = ST.get () in
  (**) B.(modifies_only_not_unused_in loc_none h5 h6);
  (**) B.(modifies_only_not_unused_in loc_none h0 h6);
  (**) if c.km = Runtime then
  (**)   c.key.frame_invariant #i B.loc_none k0 h5 h6;
  (**) c.state.frame_invariant #i B.loc_none block_state h5 h6;
  (**) optional_frame B.loc_none k' h5 h6;
  (**) assert (B.fresh_loc (B.loc_addr_of_buffer p) h0 h6);
  (**) assert (B.fresh_loc (footprint_s c i h6 s) h0 h6);
  (**) c.state.frame_freeable B.loc_none block_state h5 h6;
  (**) assert (optional_reveal h5 k' == optional_reveal h6 k');

  p
#pop-options

#push-options "--z3rlimit 200"
let alloca #index c i t t' k =
  [@inline_let] let _ = c.state.invariant_loc_in_footprint #i in
  [@inline_let] let _ = c.key.invariant_loc_in_footprint #i in
  allow_inversion key_management;

  (**) let h0 = ST.get () in

  (**) B.loc_unused_in_not_unused_in_disjoint h0;
  let buf = B.alloca (Lib.IntTypes.u8 0) (c.blocks_state_len i) in
  (**) let h1 = ST.get () in
  (**) assert (B.fresh_loc (B.loc_buffer buf) h0 h1);
  (**) B.loc_unused_in_not_unused_in_disjoint h1;
  (**) B.(modifies_only_not_unused_in loc_none h0 h1);
  (**) c.key.frame_invariant B.loc_none k h0 h1;

  let block_state = c.state.alloca i in
  (**) let h2 = ST.get () in
  (**) assert (B.fresh_loc (c.state.footprint #i h2 block_state) h0 h2);
  (**) B.loc_unused_in_not_unused_in_disjoint h2;
  (**) B.(modifies_only_not_unused_in loc_none h1 h2);
  (**) c.key.frame_invariant B.loc_none k h1 h2;

  let k': optional_key i c.km c.key =
    match c.km with
    | Runtime ->
        let k' = c.key.alloca i in
        (**) let h3 = ST.get () in
        (**) B.loc_unused_in_not_unused_in_disjoint h3;
        (**) B.(modifies_only_not_unused_in loc_none h2 h3);
        (**) c.key.frame_invariant B.loc_none k h2 h3;
        (**) c.state.frame_invariant B.loc_none block_state h2 h3;
        (**) assert (B.fresh_loc (c.key.footprint #i h3 k') h0 h3);
        (**) assert (c.key.invariant #i h3 k');
        (**) assert (c.key.invariant #i h3 k);
        (**) assert B.(loc_disjoint (c.key.footprint #i h3 k) (c.key.footprint #i h3 k'));
        c.key.copy i k k';
        (**) let h4 = ST.get () in
        (**) assert (B.fresh_loc (c.key.footprint #i h4 k') h0 h4);
        (**) B.loc_unused_in_not_unused_in_disjoint h4;
        (**) B.(modifies_only_not_unused_in loc_none h2 h4);
        (**) assert (c.key.invariant #i h4 k');
        (**) c.key.frame_invariant (c.key.footprint #i h3 k') k h3 h4;
        (**) c.state.frame_invariant (c.key.footprint #i h3 k') block_state h3 h4;
        k'
    | Erased ->
        G.hide (c.key.v i h0 k)
  in
  (**) let h5 = ST.get () in
  (**) assert (B.fresh_loc (optional_footprint h5 k') h0 h5);
  (**) assert (B.fresh_loc (c.state.footprint #i h5 block_state) h0 h5);

  [@inline_let] let total_len = Int.Cast.uint32_to_uint64 (c.init_input_len i) in
  let s = State block_state buf total_len (G.hide S.empty) k' in
  (**) assert (B.fresh_loc (footprint_s c i h5 s) h0 h5);

  (**) B.loc_unused_in_not_unused_in_disjoint h5;
  let p = B.alloca s 1ul in
  (**) let h6 = ST.get () in
  (**) B.(modifies_only_not_unused_in loc_none h5 h6);
  (**) B.(modifies_only_not_unused_in loc_none h0 h6);
  (**) c.key.frame_invariant B.loc_none k h5 h6;
  (**) c.state.frame_invariant B.loc_none block_state h5 h6;
  (**) optional_frame B.loc_none k' h5 h6;
  (**) assert (B.fresh_loc (B.loc_addr_of_buffer p) h0 h6);
  (**) assert (B.fresh_loc (footprint_s c i h6 s) h0 h6);
  (**) assert (optional_reveal h5 k' == optional_reveal h6 k');

  c.init (G.hide i) k buf block_state;
  (**) let h7 = ST.get () in
  (**) assert (B.fresh_loc (c.state.footprint #i h7 block_state) h0 h7);
  (**) assert (B.fresh_loc (B.loc_buffer buf) h0 h7);
  (**) optional_frame (B.loc_union (c.state.footprint #i h7 block_state) (B.loc_buffer buf)) k' h6 h7;
  (**) c.update_multi_zero i (c.state.v i h7 block_state) 0;
  (**) B.modifies_only_not_unused_in B.loc_none h0 h7;
  (**) assert (c.state.v i h7 block_state == c.init_s i (optional_reveal h6 k'));

  (**) let h8 = ST.get () in
  (**) assert (U64.v total_len <= U64.v (c.max_input_len i));
  (**) begin
  (**) let key_v = key c i h8 p in
  (**) let init_input = c.init_input_s i key_v in
  (**) split_at_last_init c i init_input;
  (**) assert(invariant_s c i h8 s)
  (**) end;
  (**) assert (invariant c i h8 p);
  (**) assert (seen c i h8 p == S.empty);
  (**) assert B.(modifies loc_none h0 h8);
  (**) assert (B.fresh_loc (footprint c i h8 p) h0 h8);
  (**) assert B.(loc_includes (loc_region_only true (HS.get_tip h8)) (footprint c i h8 p));
  (**) assert(ST.same_refs_in_non_tip_regions h0 h8);

  p
#pop-options

#push-options "--z3cliopt smt.arith.nl=false"
let init #index c i t t' k s =
  [@inline_let] let _ = c.state.invariant_loc_in_footprint #i in
  [@inline_let] let _ = c.key.invariant_loc_in_footprint #i in
  allow_inversion key_management;

  let open LowStar.BufferOps in
  (**) let h1 = ST.get () in
  let State block_state buf _ _ k' = !*s in
  let i = c.index_of_state i block_state in
  LowStar.Ignore.ignore i; // This is only used in types and proofs
  [@inline_let]
  let block_state: c.state.s i = block_state in

  c.init (G.hide i) k buf block_state;

  (**) let h2 = ST.get () in
  (**) optional_frame #_ #i #c.km #c.key (B.loc_union (c.state.footprint #i h1 block_state) (B.loc_buffer buf)) k' h1 h2;
  (**) c.key.frame_invariant (B.loc_union (c.state.footprint #i h1 block_state) (B.loc_buffer buf)) k h1 h2;
  (**) Math.Lemmas.modulo_lemma 0 (U32.v (Block?.block_len c i));
  (**) assert(0 % UInt32.v (Block?.block_len c i) = 0);
  (**) assert (key c i h1 s == key c i h2 s);
  (**) c.update_multi_zero i (c.state.v i h2 block_state) 0;

  let k': optional_key i c.km c.key =
    match c.km with
    | Runtime ->
        c.key.copy i k k';
        (**) let h4 = ST.get () in
        (**) assert (c.key.invariant #i h4 k');
        (**) c.key.frame_invariant (c.key.footprint #i h2 k') k h2 h4;
        (**) c.state.frame_invariant (c.key.footprint #i h2 k') block_state h2 h4;
        (**) stateful_frame_preserves_freeable (c.key.footprint #i h2 k') block_state h2 h4;
        k'
    | Erased ->
        G.hide (c.key.v i h1 k)
  in
  (**) let h2 = ST.get () in
  (**) assert(preserves_freeable c i s h1 h2);

  [@inline_let] let total_len = Int.Cast.uint32_to_uint64 (c.init_input_len i) in
  let tmp: state_s c i t t' = State block_state buf total_len (G.hide S.empty) k' in
  B.upd s 0ul tmp;
  (**) let h3 = ST.get () in
  (**) c.state.frame_invariant B.(loc_buffer s) block_state h2 h3;
  (**) c.key.frame_invariant B.(loc_buffer s) k h2 h3;
  (**) optional_frame #_ #i #c.km #c.key B.(loc_buffer s) k' h2 h3;
  (**) stateful_frame_preserves_freeable B.(loc_buffer s) block_state h2 h3;
  (**) assert(preserves_freeable c i s h2 h3);

  // This seems to cause insurmountable difficulties. Puzzled.
  ST.lemma_equal_domains_trans h1 h2 h3;

  // AR: 07/22: same old `Seq.equal` and `==` story
  (**) assert (Seq.equal (seen c i h3 s) Seq.empty);

  (**) assert (footprint c i h1 s == footprint c i h3 s);
  (**) assert (B.(modifies (footprint c i h1 s) h1 h3));
  (**) assert (U64.v total_len <= U64.v (c.max_input_len i));
  (**) begin
  (**) let key_v = key c i h3 s in
  (**) let all_seen_ = all_seen c i h3 s in
  // SH (11/22): the proof fails if we don't introduce the call to [split_at_last]
  (**) let blocks, rest = split_at_last c i all_seen_ in
  (**) let init_input = c.init_input_s i key_v in
  (**) split_at_last_init c i init_input;
  (**) assert (invariant_s c i h3 (B.get h3 s 0))
  (**) end;

  (**) assert(preserves_freeable c i s h1 h3)
#pop-options

/// Some helpers to minimize modulo-reasoning
/// =========================================

val split_at_last_num_blocks_lem (#index : Type0) (c: block index) (i: index) (b: nat):
  Lemma (
    let n_blocks = split_at_last_num_blocks c i b in
    let blocks = n_blocks * U32.v (c.blocks_state_len i) in
    0 <= blocks /\ blocks <= b)

let split_at_last_num_blocks_lem #index c i b = ()

/// The ``rest`` function below allows computing, based ``total_len`` stored in
/// the state, the length of useful data currently stored in ``buf``.
/// Unsurprisingly, there's a fair amount of modulo reasoning here because of
/// 64-bit-to-32-bit conversions, so we do them once and for all in a helper.
#push-options "--z3cliopt smt.arith.nl=false"
inline_for_extraction noextract
let rest #index (c: block index) (i: index)
  (total_len: UInt64.t): (x:UInt32.t {
    let n = split_at_last_num_blocks c i (U64.v total_len) in
    let l = U32.v (c.blocks_state_len i) in
    0 <= n * l /\ n * l <= U64.v total_len /\
    U32.v x = U64.v total_len - (n * l)})
=
  let open FStar.Int.Cast in
  [@inline_let] let l = uint32_to_uint64 (c.blocks_state_len i) in
  [@inline_let] let r = total_len `U64.rem` l in
  (**) let total_len_v : Ghost.erased nat = U64.v total_len in
  (**) let l_v : Ghost.erased nat = U64.v l in
  (**) let r_v : Ghost.erased nat = U64.v r in
  (**) assert(Ghost.reveal r_v = total_len_v - ((total_len_v / l_v) * l_v));
  (**) Math.Lemmas.euclidean_division_definition total_len_v l_v;
  (**) assert(Ghost.reveal r_v = total_len_v % l_v);
  (**) assert(r_v < l_v);

  if U64.(r =^ uint_to_t 0) && U64.(total_len >^ uint_to_t 0) then
    begin
    (**) split_at_last_num_blocks_lem c i (U64.v total_len);
    c.blocks_state_len i
    end
  else
    begin
    [@inline_let] let r' = FStar.Int.Cast.uint64_to_uint32 r in
    (**) FStar.Math.Lemmas.small_modulo_lemma_1 (U64.v r) (pow2 32);
    (**) calc (==) {
    (**)   U32.v r';
    (**) (==) { }
    (**)   U64.v r % pow2 32;
    (**) (==) { FStar.Math.Lemmas.small_modulo_lemma_1 (U64.v r) (pow2 32) }
    (**)   U64.v r;
    (**) (==) { FStar.Math.Lemmas.euclidean_division_definition (U64.v total_len) (U64.v (uint32_to_uint64 (c.blocks_state_len i))) }
    (**)   U64.v total_len % U64.v (uint32_to_uint64 (c.blocks_state_len i) );
    (**) (==) { }
    (**)   U64.v total_len % U32.v (c.blocks_state_len i);
    (**) };
    (**) assert(
    (**)   let n = split_at_last_num_blocks c i (U64.v total_len) in
    (**)   let l = U32.v (c.blocks_state_len i) in
    (**)    U32.v r' = U64.v total_len - (n * l));
    r'
    end
#pop-options


/// The ``nblocks`` function below allows computing, given ``total_len`` stored in
/// the state, the number of blocks of data which have been processed (the remaining
/// unprocessed data being left in ``buf``).
#push-options "--z3cliopt smt.arith.nl=false"
inline_for_extraction noextract
let nblocks #index (c: block index) (i: index)
  (len: UInt32.t): (x:UInt32.t {
    let l = U32.v (c.blocks_state_len i) in
    U32.v x * l <= U32.v len /\
    U32.v x = split_at_last_num_blocks c i (U32.v len) })
=
  let open FStar.Int.Cast in
  [@inline_let] let l = c.blocks_state_len i in
  [@inline_let] let r = rest c i (uint32_to_uint64 len) in
  (**) let len_v : Ghost.erased nat = U32.v len in
  (**) let l_v : Ghost.erased nat = U32.v l in
  (**) let r_v : Ghost.erased nat = U32.v r in
  (**) let n_s : Ghost.erased nat = split_at_last_num_blocks c i len_v in
  (**) assert(Ghost.reveal len_v = n_s * l_v + r_v);
  (**) Math.Lemmas.nat_times_nat_is_nat n_s l_v;
  (**) assert(U32.v r <= U32.v len);
  [@inline_let] let blocks = len `U32.sub` r in
  (**) let blocks_v : Ghost.erased nat = U32.v blocks in
  (**) assert(blocks_v % l_v = 0);
  [@inline_let] let n = blocks `U32.div` l in
  (**) let n_v : Ghost.erased nat = U32.v n in
  (**) assert(n_v * l_v = Ghost.reveal blocks_v);
  (**) split_at_last_num_blocks_spec c i len_v n_v r_v;
  n
#pop-options

/// The ``rest`` function to call on the unprocessed data length in the ``finish``
/// function.
#push-options "--z3cliopt smt.arith.nl=false"
inline_for_extraction noextract
let rest_finish #index (c: block index) (i: index)
  (len: UInt32.t): (x:UInt32.t {
    let l = U32.v (c.block_len i) in
    let n = fst (Lib.UpdateMulti.split_at_last_lazy_nb_rem l (U32.v len)) in
    0 <= n * l /\ n * l <= U32.v len /\
    U32.v x = U32.v len - (n * l)})
=
  [@inline_let] let l = c.block_len i in
  [@inline_let] let r = len `U32.rem` l in
  (**) split_at_last_num_blocks_lem c i (U32.v len);
  if U32.(r =^ uint_to_t 0) && U32.(len >^ uint_to_t 0) then
    begin
    (**) begin
    (**) let l = U32.v (c.block_len i) in
    (**) let n = fst (Lib.UpdateMulti.split_at_last_lazy_nb_rem l (U32.v len)) in
    (**) Math.Lemmas.nat_times_nat_is_nat n l
    (**) end;
    c.block_len i
    end
  else
    r
#pop-options

/// We always add 32-bit lengths to 64-bit lengths. Having a helper for that allows
/// doing modulo reasoning once and for all.
inline_for_extraction noextract
let add_len #index (c: block index) (i: index) (total_len: UInt64.t) (len: UInt32.t):
  Pure UInt64.t
    (requires U64.v total_len + U32.v len <= U64.v (c.max_input_len i))
    (ensures fun x -> U64.v x = U64.v total_len + U32.v len /\ U64.v x <= U64.v (c.max_input_len i))
=
  total_len `U64.add` Int.Cast.uint32_to_uint64 len

#push-options "--z3cliopt smt.arith.nl=false"
inline_for_extraction noextract
let add_len_small #index (c: block index) (i: index) (total_len: UInt64.t) (len: UInt32.t): Lemma
  (requires
    U32.v len <= U32.v (c.blocks_state_len i) - U32.v (rest c i total_len) /\
    U64.v total_len + U32.v len <= U64.v (c.max_input_len i))
  (ensures (rest c i (add_len c i total_len len) = rest c i total_len `U32.add` len))
=
  let total_len_v = U64.v total_len in
  let l = U32.v (c.blocks_state_len i) in
  let b = total_len_v + U32.v len in
  let n = split_at_last_num_blocks c i total_len_v in
  let r = U32.v (rest c i total_len) in
  assert(total_len_v = n * l + r);
  let r' = U32.v (rest c i total_len) + U32.v len in
  assert(r' <= l);
  assert(r' = 0 ==> b = 0);
  Math.Lemmas.euclidean_division_definition b l;
  assert(b = n * l + r');
  split_at_last_num_blocks_spec c i b n r'
#pop-options


/// Beginning of the three sub-cases (see Hacl.Streaming.Spec)
/// ==========================================================

noextract
let total_len_h #index (c: block index) (i: index) h (p: state' c i) =
  State?.total_len (B.deref h p)

noextract
let split_at_last_all_seen #index (c: block index) (i: index) h (p: state' c i) =
  let all_seen = all_seen c i h p in
  let blocks, rest = split_at_last c i all_seen in
  blocks, rest

inline_for_extraction noextract
val update_small:
  #index:Type0 ->
  (c: block index) ->
  i:index -> (
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  s:state c i t t' ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  Stack unit
    (requires fun h0 ->
      update_pre c i s data len h0 /\
      U32.v (c.init_input_len i) + S.length (seen c i h0 s) + U32.v len <= U64.v (c.max_input_len i) /\
      U32.v len <= U32.v (c.blocks_state_len i) - U32.v (rest c i (total_len_h c i h0 s)))
    (ensures fun h0 s' h1 ->
      update_post c i s data len h0 h1))

/// SH: The proof obligations for update_small have problem succeeding in command
/// line mode: hence the restart-solver instruction, the crazy rlimit and the
/// intermediate lemma. Interestingly (and frustratingly), the proof succeeds
/// quite quickly locally on command-line with this rlimit, but fails with a lower
/// one. Besides, the lemma is needed only for the CI regression.
let split_at_last_rest_eq (#index : Type0) (c: block index)
                          (i: index)
                          (t:Type0 { t == c.state.s i })
                          (t':Type0 { t' == optional_key i c.km c.key })
                          (s: state c i t t') (h0: HS.mem) :
  Lemma
  (requires (
    invariant c i h0 s))
  (ensures (
    let s = B.get h0 s 0 in
    let State block_state buf total_len seen_ k' = s in
    let key_v = optional_reveal #index #i #c.km #c.key h0 k' in
    let all_seen = S.append (c.init_input_s i key_v) seen_ in
    let _, r = split_at_last c i all_seen in
    let sz = rest c i total_len in
    Seq.length r == U32.v sz)) =
  let s = B.get h0 s 0 in
  let State block_state buf total_len seen_ k' = s in
  let key_v = optional_reveal #index #i #c.km #c.key h0 k' in
  let all_seen = S.append (c.init_input_s i key_v) seen_ in
  let _, r = split_at_last c i all_seen in
  let sz = rest c i total_len in
  ()

/// Particularly difficult proof. Z3 profiling indicates that a pattern goes off
/// the rails. So I disabled all of the known "bad" patterns, then did the proof
/// by hand. Fortunately, there were only two stateful operations. The idea was
/// to do all ofthe modifies-reasoning in the two lemmas above, then disable the
/// bad pattern for the main function.
///
/// This style is a little tedious, because it requires a little bit of digging
/// to understand what needs to hold in order to be able to prove that e.g. the
/// sequence remains unmodified from h0 to h2, but this seems more robust?
val modifies_footprint:
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  s:state' c i ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Lemma
    (requires (
      let State _ buf_ _ _ _ = B.deref h0 s in (
      update_pre c i s data len h0 /\
      B.(modifies (loc_buffer buf_) h0 h1))))
    (ensures (
      let State bs0 buf0 _ _ k0 = B.deref h0 s in
      let State bs1 buf1 _ _ k1 = B.deref h1 s in (
      footprint c i h0 s == footprint c i h1 s /\
      preserves_freeable c i s h0 h1 /\
      bs0 == bs1 /\ buf0 == buf1 /\ k0 == k1 /\
      c.state.invariant h1 bs1 /\
      c.state.v i h1 bs1 == c.state.v i h0 bs0 /\
      c.state.footprint h1 bs1 == c.state.footprint h0 bs0 /\
      B.(loc_disjoint (loc_addr_of_buffer s) (loc_buffer buf1)) /\
      B.(loc_disjoint (loc_addr_of_buffer s) (loc_buffer data)) /\
      B.(loc_disjoint (loc_addr_of_buffer s) (loc_addr_of_buffer buf1)) /\
      B.(loc_disjoint (loc_addr_of_buffer s) (c.state.footprint h1 bs1)) /\
      B.(loc_disjoint (loc_buffer s) (loc_buffer buf1)) /\
      B.(loc_disjoint (loc_buffer s) (loc_buffer data)) /\
      B.(loc_disjoint (loc_buffer s) (c.state.footprint h1 bs1)) /\
      (if c.km = Runtime then
        c.key.invariant #i h1 k1 /\
        c.key.v i h1 k1 == c.key.v i h0 k0 /\
        c.key.footprint #i h1 k1 == c.key.footprint #i h0 k0 /\
        B.(loc_disjoint (loc_addr_of_buffer s) (c.key.footprint #i h1 k1)) /\
        B.(loc_disjoint (loc_buffer s) (c.key.footprint #i h1 k1))
      else
        B.(loc_disjoint (loc_addr_of_buffer s) loc_none) /\
        True)))))

let modifies_footprint c i p data len h0 h1 =
  let _ = c.state.frame_freeable #i in
  let _ = c.key.frame_freeable #i in
  let s0 = B.deref h0 p in
  let s1 = B.deref h0 p in
  let State bs0 buf0 _ _ k0 = s0 in
  let State bs1 buf0 _ _ k1 = s1 in
  c.state.frame_invariant (B.loc_buffer buf0) bs0 h0 h1;
  if c.km = Runtime then
    c.key.frame_invariant #i (B.loc_buffer buf0) k0 h0 h1

val modifies_footprint':
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  p:state' c i ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Lemma
    (requires (
      let State bs0 buf0 _ _ k0 = B.deref h0 p in
      let State bs1 buf1 _ _ k1 = B.deref h1 p in (
      B.live h0 p /\
      B.(loc_disjoint (loc_addr_of_buffer p) (c.state.footprint #i h0 bs0)) /\
      B.(loc_disjoint (loc_addr_of_buffer p) (loc_addr_of_buffer buf0)) /\
      c.state.invariant h0 bs0 /\
      (if c.km = Runtime then
        B.(loc_disjoint (loc_addr_of_buffer p) (c.key.footprint #i h0 k0)) /\
        c.key.invariant #i h0 k0
      else
        B.(loc_disjoint (loc_addr_of_buffer p) loc_none)) /\
      B.(modifies (loc_buffer p) h0 h1)) /\
      bs0 == bs1 /\ buf0 == buf1 /\ k0 == k1))
    (ensures (
      let State bs0 buf0 _ _ k0 = B.deref h0 p in
      let State bs1 buf1 _ _ k1 = B.deref h1 p in (
      B.live h1 p /\
      footprint c i h0 p == footprint c i h1 p /\
      preserves_freeable c i p h0 h1 /\
      B.(loc_disjoint (loc_addr_of_buffer p) (footprint_s c i h1 (B.deref h1 p))) /\
      B.(loc_disjoint (loc_addr_of_buffer p) (c.state.footprint #i h1 bs1)) /\
      B.(loc_disjoint (loc_buffer p) (c.state.footprint #i h1 bs1)) /\
      c.state.invariant h1 bs1 /\
      c.state.v i h1 bs1 == c.state.v i h0 bs0 /\
      c.state.footprint h1 bs1 == c.state.footprint h0 bs0 /\
      (if c.km = Runtime then
        c.key.invariant #i h1 k1 /\
        c.key.v i h1 k1 == c.key.v i h0 k0 /\
        c.key.footprint #i h1 k1 == c.key.footprint #i h0 k0 /\
        B.(loc_disjoint (loc_addr_of_buffer p) (c.key.footprint #i h1 k1)) /\
        B.(loc_disjoint (loc_buffer p) (c.key.footprint #i h1 k1))
      else
        B.(loc_disjoint (loc_addr_of_buffer p) loc_none))))))

let modifies_footprint' c i p data len h0 h1 =
  let _ = c.state.frame_freeable #i in
  let _ = c.key.frame_freeable #i in
  let _ = c.state.frame_invariant #i in
  let _ = c.key.frame_invariant #i in
  let _ = allow_inversion key_management in
  let s0 = B.deref h0 p in
  let s1 = B.deref h0 p in
  let State bs0 buf0 _ _ k0 = s0 in
  let State bs1 buf1 _ _ k1 = s1 in
  c.state.frame_invariant (B.loc_addr_of_buffer p) bs0 h0 h1;
  if c.km = Runtime then
    c.key.frame_invariant #i (B.loc_addr_of_buffer p) k0 h0 h1

/// Small helper which we use to factor out functional correctness proof obligations.
/// It states that a state was correctly updated to process some data between two
/// memory snapshots (the key is the same, the seen data was updated, etc.).
///
/// Note that we don't specify anything about the buffer and the block_state: they
/// might have been updated differently depending on the case.
unfold val state_is_updated :
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  s:state c i t t' ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Type0)

#push-options "--z3cliopt smt.arith.nl=false"
let state_is_updated #index c i t t' p data len h0 h1 =
  // Functional conditions about the memory updates
  let s0 = B.get h0 p 0 in
  let s1 = B.get h1 p 0 in
  let State block_state0 buf0 total_len0 seen0 key0 = s0 in
  let State block_state1 buf1 total_len1 seen1 key1 = s1 in

  block_state1 == block_state0 /\
  buf1 == buf0 /\
  U64.v total_len1 == U64.v total_len0 + U32.v len /\
  key1 == key0 /\

  seen1 `S.equal` (seen0 `S.append` (B.as_seq h0 data)) /\

  optional_reveal #index #i #c.km #c.key h1 key1 == optional_reveal #index #i #c.km #c.key h0 key0
#pop-options

/// The functional part of the invariant
unfold val invariant_s_funct :
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  s:state c i t t' ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Pure Type0 (requires
    update_pre c i s data len h0 /\
    U32.v (c.init_input_len i) + S.length (seen c i h0 s) + U32.v len <= U64.v (c.max_input_len i) /\
    state_is_updated c i t t' s data len h0 h1)
  (ensures (fun _ -> True)))
val invariant_s_funct :
  #index:Type0 ->
  (c: block index) ->
  i:G.erased index -> (
  let i = G.reveal i in
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  s:state c i t t' ->
  data: B.buffer uint8 ->
  len: UInt32.t ->
  h0: HS.mem ->
  h1: HS.mem ->
  Pure Type0 (requires
    update_pre c i s data len h0 /\
    U32.v (c.init_input_len i) + S.length (seen c i h0 s) + U32.v len <= U64.v (c.max_input_len i) /\
    state_is_updated c i t t' s data len h0 h1)
  (ensures (fun _ -> True)))
c: Hacl.Streaming.Interface.block index -> i: FStar.Ghost.erased index
  -> (let i = FStar.Ghost.reveal i in

          t: Type0{t == Stateful?.s (Block?.state c) i} ->
          t': Type0{t' == Hacl.Streaming.Interface.optional_key i (Block?.km c) (Block?.key c)} ->
          s: Hacl.Streaming.Functor.state c i t t' ->
          data: LowStar.Buffer.buffer Hacl.Streaming.Spec.uint8 ->
          len: FStar.UInt32.t ->
          h0: FStar.Monotonic.HyperStack.mem ->
          h1: FStar.Monotonic.HyperStack.mem
        -> Prims.Pure Type0)