val dt_malloc : r: FStar.Monotonic.HyperHeap.rid ->
    input: Stateful?.s (Stateful_malloc_from_input?.smfi_input dt) ()
  -> FStar.HyperStack.ST.ST (Stateful?.s (Stateful_malloc_from_input?.smfi_stateful dt) ())
let dt_malloc #dt = dt.smfi_malloc ()
module Impl.Noise.LinkedList

/// A Low*, stateful linked list containing stateful data

module B = LowStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module ST = FStar.HyperStack.ST

module LL2 = LowStar.Lib.LinkedList2
module LL1 = LowStar.Lib.LinkedList

open FStar.HyperStack.ST
open LowStar.BufferOps
open Impl.Noise.Stateful
open Spec.Noise.Map

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

/// Types, invariants
/// -----------------

val _align_beg : unit

inline_for_extraction noextract
let stateful = stateful_malloc_from_input

inline_for_extraction noextract
let stateful_get_prim (st : stateful unit) =
  st.smfi_stateful

inline_for_extraction noextract
let dt_s (dt : stateful unit) : Type0 = dt.smfi_stateful.s ()

inline_for_extraction noextract
let dt_t (dt : stateful unit) : Type0 = dt.smfi_stateful.t ()

inline_for_extraction noextract
let dt_v (#dt : stateful unit) : HS.mem -> x:dt_s dt -> GTot (dt_t dt) =
  dt.smfi_stateful.v ()

inline_for_extraction noextract
let dt_footprint (#dt : stateful unit) : x:dt_s dt -> GTot B.loc =
  dt.smfi_stateful.footprint

inline_for_extraction noextract
let dt_invariant (#dt : stateful unit) : HS.mem -> x:dt_s dt -> GTot Type0 =
  dt.smfi_stateful.invariant

inline_for_extraction noextract
let dt_freeable (#dt : stateful unit) : HS.mem -> x:dt_s dt -> GTot Type0 =
  dt.smfi_stateful.freeable

let dt_frame_invariant (#dt : stateful unit) (l : B.loc) (x:dt_s dt) =
  dt.smfi_stateful.frame_invariant l x

let dt_frame_freeable (#dt : stateful unit) (l : B.loc) (x:dt_s dt) =
  dt.smfi_stateful.frame_freeable l x
/
Spec.Noise.Map.fst.checked prims.fst.checked LowStar.Lib.LinkedList2.fst.checked LowStar.Lib.LinkedList.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Impl.Noise.Stateful.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.LinkedList.fsti

    r: FStar.Monotonic.HyperHeap.rid ->
    input: Stateful?.s (Stateful_malloc_from_input?.smfi_input dt) ()
  -> FStar.HyperStack.ST.ST (Stateful?.s (Stateful_malloc_from_input?.smfi_stateful dt) ())
Impl.Noise.Stateful.stateful_malloc_from_input Prims.unit Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_malloc FStar.Monotonic.HyperHeap.rid Impl.Noise.Stateful.__proj__Stateful__item__s Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_input Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_stateful FStar.Monotonic.HyperStack.mem Prims.l_and FStar.HyperStack.ST.is_eternal_region Impl.Noise.Stateful.__proj__Stateful__item__invariant Prims.eq2 Impl.Noise.Stateful.__proj__Stateful__item__t Impl.Noise.Stateful.__proj__Stateful__item__v LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_regions FStar.Monotonic.HyperHeap.mod_set FStar.Set.singleton Impl.Noise.Stateful.__proj__Stateful__item__footprint Impl.Noise.Stateful.__proj__Stateful__item__freeable
let dt_malloc #dt =
  
dt.smfi_malloc ()