val dt_frame_invariant_forward :
  #dt:stateful unit -> l:B.loc -> s:dt_s dt -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    dt_invariant h0 s /\
    B.loc_disjoint l (dt_footprint s) /\
    B.modifies l h0 h1))
  (ensures (
    dt_invariant h1 s /\
    dt_v h0 s == dt_v h1 s))
  [ SMTPat (dt_invariant h0 s); SMTPat (B.modifies l h0 h1) ]
val dt_frame_invariant_forward :
  #dt:stateful unit -> l:B.loc -> s:dt_s dt -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    dt_invariant h0 s /\
    B.loc_disjoint l (dt_footprint s) /\
    B.modifies l h0 h1))
  (ensures (
    dt_invariant h1 s /\
    dt_v h0 s == dt_v h1 s))
  [ SMTPat (dt_invariant h0 s); SMTPat (B.modifies l h0 h1) ]
let dt_frame_invariant_forward #dt l s h0 h1 = dt_frame_invariant l s h0 h1
module Impl.Noise.LinkedList

/// A Low*, stateful linked list containing stateful data.
///
/// Two functions were a bit hard to implement: [filter] and [filter_one].
/// For those, we implement different flavours:
/// - a recursive, non tail-call version
/// - a recursive, tail-call version (only for [filter_one])
/// - a non recursive version using a loop (only for [filter_one])
///
/// The recursive versions don't extract, because they have non-extractable
/// meta parameters in their signature, unless you ask Karamel to turn tail-call
/// recursion to loops at extraction time.
///
/// It shouldn't be difficult to implement the tail-call version of
/// [filter], put aside the fact that we need to make sure that the
/// head of the list is valid (i.e.: the head element satisfies the
/// filtering predicate) before working on the rest of the list. This
/// didn't cause much trouble for [filter_one], because if it is not
/// the case we just have to pop the head. Also, it should be possible
/// to factorize several signatures between [filter] and [filter_one],
/// a bit like what we did for the non tail-call version.
/// 
/// If implemented for [filter], the loop versions of [filter] and [filter_one]
/// are, in a sense, strictly better than the recursive ones, because they
/// are the ones we want to extract. However, it is probably a good idea
/// to preserve the tail-call versions, because they were very useful to
/// figure out the structure of the proofs, as well as a big part of the
/// collection of lemmas we need throughout this file. For instance, trying
/// to implement the loop version of [filter] without having implemented
/// its tail-call equivalent before would be a very bad idea. Finally,
/// when working on [filter], it should be possible to generalize and reuse
/// some of the definitions used in [filter_one], leading to easier proofs
/// and better maintainability.

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
module M = Spec.Noise.Map

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

let _align_beg = ()

[@CAbstractStruct]
noeq
type t_ (t1: Type0): Type0 = {
  ptr: B.pointer (LL1.t t1);
  // Relies on a new pointer-to-unit elimination phase in KaRaMeL
  // LL1 requires the client to keep track of a high-level ghost list
  // of the low-level elements in the low-level linked lidt. We can
  // then convert them to a list of high-level elements
  elems: B.pointer (G.erased (list t1));
  // For separation; all erased.
  r: HS.rid; // The region containing the whole list
  r_new : B.pointer HS.rid; // A sub-region in which to perform allocations
  r_spine : HS.rid;
}

inline_for_extraction noextract
let t (dt: stateful unit) = t_ (dt_s dt)

let get_elems #dt h ll =
  B.deref h ll.elems

// We rewrite the signature for the two following lemmas in order to make sure
// they are framed correctly. Also, as they are only valid locally, we adopt a
// more aggressive forward style in the patterns
val dt_frame_invariant_forward :
  #dt:stateful unit -> l:B.loc -> s:dt_s dt -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    dt_invariant h0 s /\
    B.loc_disjoint l (dt_footprint s) /\
    B.modifies l h0 h1))
  (ensures (
    dt_invariant h1 s /\
    dt_v h0 s == dt_v h1 s))
  [ SMTPat (dt_invariant h0 s); SMTPat (B.modifies l h0 h1) ]
/
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.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.HyperStack.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.List.Tot.fst.checked FStar.IndefiniteDescription.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked C.Loops.fst.checked
Impl.Noise.LinkedList.fst

    l: LowStar.Monotonic.Buffer.loc ->
    s: Impl.Noise.LinkedList.dt_s dt ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        Impl.Noise.LinkedList.dt_invariant h0 s /\
        LowStar.Monotonic.Buffer.loc_disjoint l (Impl.Noise.LinkedList.dt_footprint s) /\
        LowStar.Monotonic.Buffer.modifies l h0 h1)
      (ensures
        Impl.Noise.LinkedList.dt_invariant h1 s /\
        Impl.Noise.LinkedList.dt_v h0 s == Impl.Noise.LinkedList.dt_v h1 s)
      [
        SMTPat (Impl.Noise.LinkedList.dt_invariant h0 s);
        SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1)
      ]
Impl.Noise.LinkedList.stateful Prims.unit LowStar.Monotonic.Buffer.loc Impl.Noise.LinkedList.dt_s FStar.Monotonic.HyperStack.mem Impl.Noise.LinkedList.dt_frame_invariant
let dt_frame_invariant_forward #dt l s h0 h1 =
  
dt_frame_invariant l s h0 h1