val dt_frame_invariant : l: LowStar.Monotonic.Buffer.loc ->
    x: Impl.Noise.LinkedList.dt_s dt ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        Stateful?.invariant (Stateful_malloc_from_input?.smfi_stateful dt) h0 x /\
        LowStar.Monotonic.Buffer.loc_disjoint l
          (Stateful?.footprint (Stateful_malloc_from_input?.smfi_stateful dt) x) /\
        LowStar.Monotonic.Buffer.modifies l h0 h1)
      (ensures
        Stateful?.invariant (Stateful_malloc_from_input?.smfi_stateful dt) h1 x /\
        Stateful?.v (Stateful_malloc_from_input?.smfi_stateful dt) () h0 x ==
        Stateful?.v (Stateful_malloc_from_input?.smfi_stateful dt) () h1 x)
      [
        SMTPat (Stateful?.invariant (Stateful_malloc_from_input?.smfi_stateful dt) h1 x);
        SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1)
      ]
let dt_frame_invariant (#dt : stateful unit) (l : B.loc) (x:dt_s dt) =
  dt.smfi_stateful.frame_invariant l x
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
/
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

    l: LowStar.Monotonic.Buffer.loc ->
    x: Impl.Noise.LinkedList.dt_s dt ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        Stateful?.invariant (Stateful_malloc_from_input?.smfi_stateful dt) h0 x /\
        LowStar.Monotonic.Buffer.loc_disjoint l
          (Stateful?.footprint (Stateful_malloc_from_input?.smfi_stateful dt) x) /\
        LowStar.Monotonic.Buffer.modifies l h0 h1)
      (ensures
        Stateful?.invariant (Stateful_malloc_from_input?.smfi_stateful dt) h1 x /\
        Stateful?.v (Stateful_malloc_from_input?.smfi_stateful dt) () h0 x ==
        Stateful?.v (Stateful_malloc_from_input?.smfi_stateful dt) () h1 x)
      [
        SMTPat (Stateful?.invariant (Stateful_malloc_from_input?.smfi_stateful dt) h1 x);
        SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1)
      ]
Impl.Noise.LinkedList.stateful Prims.unit LowStar.Monotonic.Buffer.loc Impl.Noise.LinkedList.dt_s Impl.Noise.Stateful.__proj__Stateful__item__frame_invariant Impl.Noise.Stateful.__proj__Stateful_malloc_from_input__item__smfi_stateful FStar.Monotonic.HyperStack.mem Prims.l_and Impl.Noise.Stateful.__proj__Stateful__item__invariant LowStar.Monotonic.Buffer.loc_disjoint Impl.Noise.Stateful.__proj__Stateful__item__footprint LowStar.Monotonic.Buffer.modifies Prims.squash Prims.eq2 Impl.Noise.Stateful.__proj__Stateful__item__t Impl.Noise.Stateful.__proj__Stateful__item__v Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let dt_frame_invariant (#dt: stateful unit) (l: B.loc) (x: dt_s dt) =
  
dt.smfi_stateful.frame_invariant l x