val frame_invariant: #index:Type0 -> c:block index -> i:index -> l:B.loc -> s:state' c i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant c i h0 s /\
    B.loc_disjoint l (footprint c i h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant c i h1 s /\
    footprint c i h0 s == footprint c i h1 s /\
    preserves_freeable c i s h0 h1))
  [ SMTPat (invariant c i h1 s); SMTPat (B.modifies l h0 h1) ]
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
val frame_invariant: #index:Type0 -> c:block index -> i:index -> l:B.loc -> s:state' c i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant c i h0 s /\
    B.loc_disjoint l (footprint c i h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant c i h1 s /\
    footprint c i h0 s == footprint c i h1 s /\
    preserves_freeable c i s h0 h1))
  [ SMTPat (invariant c i h1 s); SMTPat (B.modifies l h0 h1) ]
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
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 LowStar.Monotonic.Buffer.loc Hacl.Streaming.Functor.state' FStar.Monotonic.HyperStack.mem Hacl.Streaming.Interface.__proj__Stateful__item__s Hacl.Streaming.Interface.__proj__Block__item__state LowStar.Buffer.buffer Lib.IntTypes.uint8 Prims.b2t Prims.op_Equality FStar.UInt32.t LowStar.Monotonic.Buffer.len LowStar.Buffer.trivial_preorder Hacl.Streaming.Interface.__proj__Block__item__blocks_state_len FStar.UInt64.t FStar.Ghost.erased FStar.Seq.Base.seq Hacl.Streaming.Spec.uint8 Hacl.Streaming.Interface.optional_key Hacl.Streaming.Interface.__proj__Block__item__km Hacl.Streaming.Interface.__proj__Block__item__key Hacl.Streaming.Interface.__proj__Stateful__item__frame_invariant Prims.unit Hacl.Streaming.Functor.stateful_frame_preserves_freeable FStar.Pervasives.allow_inversion Hacl.Streaming.Interface.key_management Hacl.Streaming.Functor.state_s LowStar.Monotonic.Buffer.deref
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)
val frame_invariant: #index:Type0 -> c:block index -> i:index -> l:B.loc -> s:state' c i -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant c i h0 s /\
    B.loc_disjoint l (footprint c i h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant c i h1 s /\
    footprint c i h0 s == footprint c i h1 s /\
    preserves_freeable c i s h0 h1))
  [ SMTPat (invariant c i h1 s); SMTPat (B.modifies l h0 h1) ]

    c: Hacl.Streaming.Interface.block index ->
    i: index ->
    l: LowStar.Monotonic.Buffer.loc ->
    s: Hacl.Streaming.Functor.state' c i ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        Hacl.Streaming.Functor.invariant c i h0 s /\
        LowStar.Monotonic.Buffer.loc_disjoint l (Hacl.Streaming.Functor.footprint c i h0 s) /\
        LowStar.Monotonic.Buffer.modifies l h0 h1)
      (ensures
        Hacl.Streaming.Functor.invariant c i h1 s /\
        Hacl.Streaming.Functor.footprint c i h0 s == Hacl.Streaming.Functor.footprint c i h1 s /\
        Hacl.Streaming.Functor.preserves_freeable c i s h0 h1)
      [
        SMTPat (Hacl.Streaming.Functor.invariant c i h1 s);
        SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1)
      ]