val stateful_unused (t: Type0) : stateful t
let stateful_unused (t: Type0): stateful t =
  Stateful
    (fun _ -> unit)
    (fun #_ h s -> B.loc_none)
    (fun #_ h s -> True)
    (fun #_ h s -> True)
    (fun _ -> unit)
    (fun _ h s -> ())
    (fun #_ h s -> ())
    (fun #_ l s h0 h1 -> ())
    (fun #_ l s h0 h1 -> ())
    (fun _ -> ())
    (fun _ r -> ())
    (fun _ s -> ())
    (fun _ _ _ -> ())
val stateful_unused (t: Type0) : stateful t
let stateful_unused (t: Type0) : stateful t =
Stateful (fun _ -> unit)
  (fun #_ h s -> B.loc_none)
  (fun #_ h s -> True)
  (fun #_ h s -> True)
  (fun _ -> unit)
  (fun _ h s -> ())
  (fun #_ h s -> ())
  (fun #_ l s h0 h1 -> ())
  (fun #_ l s h0 h1 -> ())
  (fun _ -> ())
  (fun _ r -> ())
  (fun _ s -> ())
  (fun _ _ _ -> ())
Hacl.Streaming.Interface.fsti.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.UpdateMulti.fst.checked Lib.IntTypes.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Streaming.Interface.fsti
Hacl.Streaming.Interface.Stateful Prims.unit FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.loc Prims.l_True FStar.Monotonic.HyperHeap.rid FStar.Ghost.erased Hacl.Streaming.Interface.stateful
module Hacl.Streaming.Interface

open FStar.HyperStack.ST
open FStar.Integers

/// This is the interface that the streaming functor expects from a block-based
/// API. We need to be abstract vis à vis the state representations of the
/// underlying block-based API. For that, we use classic framing lemma and
/// invariant preservation techniques used in EverCrypt and elsewhere.

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 100"

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

open LowStar.BufferOps
open FStar.Mul

inline_for_extraction noextract
let uint8 = Lib.IntTypes.uint8

inline_for_extraction noextract
let uint32 = Lib.IntTypes.uint32

/// The type class of stateful types: a low-level representation, a high-level
/// value, and a ``v`` function to switch between the two.
///
/// The low-level representation needs to abide by all the important framing
/// principles to allow clients to efficiently work with a ``stateful index``.
///
/// More interestingly, we require some extra operations that arise in the
/// process of manipulating instances of this type class:
/// - the ability to allocate on the stack (useful for temporaries)
/// - the ability to allocate on the heap (useful for retaining a copy of a stateful)
/// - the ability to copy
/// - a predicate that captures the fact that the invariant depends only on the
///   footprint of the stateful, i.e. does not rely on some gcmalloc'd global
///   state in the global scope.
///
/// This may seem like a lot but actually most low-level representations satisfy
/// these principles!
inline_for_extraction noextract noeq
type stateful (index: Type0) =
| Stateful:
  // Low-level types
  s: (index -> Type0) ->

  // Astract footprint.
  footprint: (#i:index -> h:HS.mem -> s:s i -> GTot B.loc) ->
  freeable: (#i:index -> h:HS.mem -> p:s i -> Type) ->
  invariant: (#i:index -> h:HS.mem -> s:s i -> Type) ->

  // A pure representation of an s
  t: (index -> Type0) ->
  v: (i:index -> h:HS.mem -> s:s i -> GTot (t i)) ->

  // Adequate framing lemmas, relying on v.
  invariant_loc_in_footprint: (#i:index -> h:HS.mem -> s:s i -> Lemma
    (requires (invariant h s))
    (ensures (B.loc_in (footprint #i h s) h))
    [ SMTPat (invariant h s) ]) ->

  frame_invariant: (#i:index -> l:B.loc -> s:s i -> h0:HS.mem -> h1:HS.mem -> Lemma
    (requires (
      invariant h0 s /\
      B.loc_disjoint l (footprint #i h0 s) /\
      B.modifies l h0 h1))
    (ensures (
      invariant h1 s /\
      v i h0 s == v i h1 s /\
      footprint #i h1 s == footprint #i h0 s))
    [ SMTPat (invariant h1 s); SMTPat (B.modifies l h0 h1) ]) ->

  frame_freeable: (#i:index -> l:B.loc -> s:s i -> h0:HS.mem -> h1:HS.mem -> Lemma
    (requires (
      invariant h0 s /\
      freeable h0 s /\
      B.loc_disjoint l (footprint #i h0 s) /\
      B.modifies l h0 h1))
    (ensures (
      freeable h1 s))
    [ SMTPat (freeable h1 s); SMTPat (B.modifies l h0 h1) ]) ->

  // Stateful operations
  alloca: (i:index -> StackInline (s i)
    (requires (fun _ -> True))
    (ensures (fun h0 s h1 ->
      invariant #i h1 s /\
      B.(modifies loc_none h0 h1) /\
      B.fresh_loc (footprint #i h1 s) h0 h1 /\
      B.(loc_includes (loc_region_only true (HS.get_tip h1)) (footprint #i h1 s))))) ->

  create_in: (i:index ->
    r:HS.rid ->
    ST (s i)
    (requires (fun h0 ->
      HyperStack.ST.is_eternal_region r))
    (ensures (fun h0 s h1 ->
      invariant #i h1 s /\
      B.(modifies loc_none h0 h1) /\
      B.fresh_loc (footprint #i h1 s) h0 h1 /\
      B.(loc_includes (loc_region_only true r) (footprint #i h1 s)) /\
      freeable #i h1 s))) ->

  free: (
    i: G.erased index -> (
    let i = G.reveal i in
    s:s i -> ST unit
    (requires fun h0 ->
      freeable #i h0 s /\
      invariant #i h0 s)
    (ensures fun h0 _ h1 ->
      B.(modifies (footprint #i h0 s) h0 h1)))) ->

  copy: (
    i:G.erased index -> (
    let i = G.reveal i in
    s_src:s i ->
    s_dst:s i ->
    Stack unit
      (requires (fun h0 ->
        invariant #i h0 s_src /\
        invariant #i h0 s_dst /\
        B.(loc_disjoint (footprint #i h0 s_src) (footprint #i h0 s_dst))))
      (ensures fun h0 _ h1 ->
        B.(modifies (footprint #i h0 s_dst) h0 h1) /\
        footprint #i h0 s_dst == footprint #i h1 s_dst /\
        (freeable #i h0 s_dst ==> freeable #i h1 s_dst) /\
        invariant #i h1 s_dst /\
        v i h1 s_dst == v i h0 s_src))) ->

  stateful index

inline_for_extraction noextract
let stateful_buffer (a: Type) (l: UInt32.t { UInt32.v l > 0 }) (zero: a) (t: Type0): stateful t =
  Stateful
    (fun _ -> b:B.buffer a { B.len b == l })
    (fun #_ h s -> B.loc_addr_of_buffer s)
    (fun #_ h s -> B.freeable s)
    (fun #_ h s -> B.live h s)
    (fun _ -> s:S.seq a { S.length s == UInt32.v l })
    (fun _ h s -> B.as_seq h s)
    (fun #_ h s -> ())
    (fun #_ l s h0 h1 -> ())
    (fun #_ l s h0 h1 -> ())
    (fun _ -> B.alloca zero l)
    (fun _ r -> B.malloc r zero l)
    (fun _ s -> B.free s)
    (fun _ s_src s_dst -> B.blit s_src 0ul s_dst 0ul l)

inline_for_extraction noextract
val stateful_unused (t: Type0) : stateful t
t: Type0 -> Hacl.Streaming.Interface.stateful t