val stateful_buffer (a: Type0) (l: UInt32.t{UInt32.v l > 0}) (zero: a) : stateful unit
val stateful_buffer (a: Type0) (l: UInt32.t{UInt32.v l > 0}) (zero: a) : stateful unit
let stateful_buffer (a:Type0) (l: UInt32.t { UInt32.v l > 0 }) (zero: a) :
  stateful unit =
  Stateful
    (fun _ -> b:B.buffer a { B.len b == l })
    (fun #_ 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 #_ l s h0 h1 -> ())
    (fun #_ l s h0 h1 -> ())
module Impl.Noise.Stateful
// TODO: move to HACL, F* or Karamel

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

open Lib.Sequence
module S = Lib.Sequence
module L = FStar.List
module Seq = FStar.Seq
open Lib.ByteSequence

open Lib.Buffer
open LowStar.BufferOps

module LB = Lib.Buffer
module B = LowStar.Buffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module G = FStar.Ghost
module U8 = FStar.UInt8

// For buffer_or_null_loc_addr, buffer_or_null_loc_freeable.
// TODO: move them to another files
open Impl.Noise.TypeOrUnit

#push-options "--z3rlimit 25 --fuel 0 --ifuel 0"

(*** Primitive typeclass *)
/// Stateful typeclass: the base typeclass, containing all the primitive operations
/// and predicates.
/// Note that the [footprint] is indenpendant of the memory snapshot.
/// It is the case when there are no memory indirections (if the type is actually
/// a record of buffers, for example). In other situations (a linked list for
/// example), this can be achieved by putting all the stateful data inside a region.
/// Note that making the footprint independant of the memory really makes reasoning
/// a lot easier.
/// Note that the [invariant] and the [freeable] predicate MAY NEED the memory
/// snapshot.
inline_for_extraction noeq
type stateful (index: Type0) =
| Stateful:
  // Low-level types
  s: (index -> Type0) ->

  // Abstract footprint.
  footprint: (#i:index -> 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 a s
  t: (index -> Type0) ->
  v: (i:index -> h:HS.mem -> s:s i -> GTot (t i)) ->

  // Adequate framing lemmas, relying on v.

  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 s) /\
      B.modifies l h0 h1))
    (ensures (
      invariant h1 s /\
      v i h0 s == v i h1 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 s) /\
      B.modifies l h0 h1))
    (ensures (
      freeable h1 s))
    [ SMTPat (freeable h1 s); SMTPat (B.modifies l h0 h1) ]) ->

  stateful index

/// An instantiation of [stateful] as buffers of fixed length.
// This is a copy-paste from Hacl.Streaming.Interface
/
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.TypeOrUnit.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.Stateful.fst
a: Type0 -> l: FStar.UInt32.t{FStar.UInt32.v l > 0} -> zero: a
  -> Impl.Noise.Stateful.stateful Prims.unit
FStar.UInt32.t Prims.b2t Prims.op_GreaterThan FStar.UInt32.v Impl.Noise.Stateful.Stateful Prims.unit LowStar.Buffer.buffer Prims.eq2 LowStar.Monotonic.Buffer.len LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.loc_addr_of_buffer LowStar.Monotonic.Buffer.loc FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.freeable LowStar.Monotonic.Buffer.live Lib.Sequence.seq Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n Lib.Sequence.length LowStar.Monotonic.Buffer.as_seq Impl.Noise.Stateful.stateful
let stateful_buffer (a: Type0) (l: UInt32.t{UInt32.v l > 0}) (zero: a) : stateful unit =
  
Stateful (fun _ -> b: B.buffer a {B.len b == l})
  (fun #_ 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 #_ l s h0 h1 -> ())
  (fun #_ l s h0 h1 -> ())