val stateful_get_prim : st: Impl.Noise.LinkedList.stateful Prims.unit
  -> smfi_stateful:
    Impl.Noise.Stateful.stateful Prims.unit
      { forall (i: Prims.unit).
          Stateful?.t smfi_stateful i == Stateful?.t (Stateful_malloc_from_input?.smfi_input st) i }
let stateful_get_prim (st : stateful unit) =
  st.smfi_stateful
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
/
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
st: Impl.Noise.LinkedList.stateful Prims.unit
  -> smfi_stateful:
    Impl.Noise.Stateful.stateful Prims.unit
      { forall (i: Prims.unit).
          Stateful?.t smfi_stateful i == Stateful?.t (Stateful_malloc_from_input?.smfi_input st) i }
Impl.Noise.LinkedList.stateful Prims.unit Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_stateful Impl.Noise.Stateful.stateful Prims.l_Forall Prims.eq2 Impl.Noise.Stateful.__proj__Stateful__item__t Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_input
let stateful_get_prim (st: stateful unit) =
  
st.smfi_stateful