val create_in:
  #index: Type0 ->
  c:block index ->
  i:index ->
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  create_in_st c i t t'
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
val create_in:
  #index: Type0 ->
  c:block index ->
  i:index ->
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  create_in_st c i t t'
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;
(let open B in 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;
(let open B in 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;
    (let open B in 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;
    (let open B in 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
(let open B in modifies_only_not_unused_in loc_none h5 h6);
(let open B in 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));
(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));
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
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 Prims.eq2 Hacl.Streaming.Interface.__proj__Stateful__item__s Hacl.Streaming.Interface.__proj__Block__item__state Hacl.Streaming.Interface.optional_key Hacl.Streaming.Interface.__proj__Block__item__km Hacl.Streaming.Interface.__proj__Block__item__key FStar.Monotonic.HyperHeap.rid Prims.unit Prims._assert FStar.HyperStack.ST.equal_stack_domains LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_region_only Hacl.Streaming.Functor.footprint LowStar.Monotonic.Buffer.fresh_loc LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none FStar.Seq.Base.seq Hacl.Streaming.Spec.uint8 Hacl.Streaming.Functor.seen FStar.Seq.Base.empty Hacl.Streaming.Functor.invariant Hacl.Streaming.Functor.invariant_s Hacl.Streaming.Spec.split_at_last_init Hacl.Streaming.Interface.uint8 Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.Seq.Base.length FStar.UInt32.v Hacl.Streaming.Interface.__proj__Block__item__init_input_len Hacl.Streaming.Interface.__proj__Block__item__init_input_s Hacl.Streaming.Interface.__proj__Stateful__item__t Hacl.Streaming.Functor.key Hacl.Streaming.Functor.state_s LowStar.Monotonic.Buffer.get LowStar.Buffer.trivial_preorder Prims.op_LessThanOrEqual FStar.UInt64.v Hacl.Streaming.Interface.__proj__Block__item__max_input_len Hacl.Streaming.Functor.state FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Streaming.Interface.__proj__Stateful__item__v Hacl.Streaming.Interface.__proj__Block__item__init_s Hacl.Streaming.Functor.optional_reveal LowStar.Monotonic.Buffer.modifies_only_not_unused_in Hacl.Streaming.Interface.__proj__Block__item__update_multi_zero Hacl.Streaming.Functor.optional_frame LowStar.Monotonic.Buffer.loc_union Hacl.Streaming.Interface.__proj__Stateful__item__footprint LowStar.Monotonic.Buffer.loc_buffer Lib.IntTypes.uint8 Hacl.Streaming.Interface.__proj__Block__item__init FStar.Ghost.hide Hacl.Streaming.Interface.__proj__Stateful__item__frame_freeable Hacl.Streaming.Functor.footprint_s LowStar.Monotonic.Buffer.loc_addr_of_buffer Hacl.Streaming.Interface.__proj__Stateful__item__frame_invariant LowStar.Monotonic.Buffer.mbuffer Prims.l_and Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.uint_to_t FStar.UInt32.t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.freeable LowStar.Buffer.malloc FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.loc_unused_in_not_unused_in_disjoint Hacl.Streaming.Functor.State FStar.UInt64.t FStar.Int.Cast.uint32_to_uint64 Hacl.Streaming.Functor.optional_footprint Hacl.Streaming.Interface.__proj__Stateful__item__invariant Hacl.Streaming.Interface.__proj__Stateful__item__copy LowStar.Monotonic.Buffer.loc_disjoint Hacl.Streaming.Interface.__proj__Stateful__item__create_in Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Hacl.Streaming.Interface.__proj__Block__item__blocks_state_len Lib.IntTypes.u8 FStar.Pervasives.allow_inversion Hacl.Streaming.Interface.key_management Prims.squash LowStar.Monotonic.Buffer.loc_in Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil Hacl.Streaming.Interface.__proj__Stateful__item__invariant_loc_in_footprint
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"
val create_in:
  #index: Type0 ->
  c:block index ->
  i:index ->
  t:Type0 { t == c.state.s i } ->
  t':Type0 { t' == optional_key i c.km c.key } ->
  create_in_st c i t t'

    c: Hacl.Streaming.Interface.block index ->
    i: index ->
    t: Type0{t == Stateful?.s (Block?.state c) i} ->
    t': Type0{t' == Hacl.Streaming.Interface.optional_key i (Block?.km c) (Block?.key c)}
  -> Hacl.Streaming.Functor.create_in_st c i t t'