val v (#dt: stateful unit) (h: HS.mem) (ll: t dt) : GTot (list (dt_t dt))
val v (#dt: stateful unit) (h: HS.mem) (ll: t dt) : GTot (list (dt_t dt))
let v: #dt:stateful unit -> h:HS.mem -> ll:t dt -> GTot (list (dt_t dt)) =
  fun #dt h ll ->
  elems_v h (get_elems h ll)
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

inline_for_extraction noextract
let dt_malloc #dt = dt.smfi_malloc ()

inline_for_extraction noextract
let dt_free #dt = dt.smfi_free ()

inline_for_extraction noextract
val t: stateful unit -> Type0

let elems_v: #dt:stateful unit -> h:HS.mem -> ll:list (dt_s dt) -> GTot (list (dt_t dt)) =
  fun #dt h ll ->
  gmap (fun x -> dt_v h x) ll

/// Getting the list of stateful elements stored in the list
val get_elems: #dt:stateful unit -> h:HS.mem -> ll:t dt -> GTot (list (dt_s dt))
/
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
h: FStar.Monotonic.HyperStack.mem -> ll: Impl.Noise.LinkedList.t dt
  -> Prims.GTot (Prims.list (Impl.Noise.LinkedList.dt_t dt))
Impl.Noise.LinkedList.stateful Prims.unit FStar.Monotonic.HyperStack.mem Impl.Noise.LinkedList.t Impl.Noise.LinkedList.elems_v Impl.Noise.LinkedList.get_elems Prims.list Impl.Noise.LinkedList.dt_t
let v: #dt: stateful unit -> h: HS.mem -> ll: t dt -> GTot (list (dt_t dt)) =
  
fun #dt h ll -> elems_v h (get_elems h ll)