val dt_t (dt: stateful unit) : Type0
val dt_t (dt: stateful unit) : Type0
let dt_t (dt : stateful unit) : Type0 = dt.smfi_stateful.t ()
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 ()
/
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
dt: Impl.Noise.LinkedList.stateful Prims.unit -> Type0
Impl.Noise.LinkedList.stateful Prims.unit Impl.Noise.Stateful.__proj__Stateful__item__t Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_stateful
let dt_t (dt: stateful unit) : Type0 =
  
dt.smfi_stateful.t ()