val f_no_elem (#dt: stateful unit) (#rtype: find_return_type dt)
    : r: f_rty rtype {rtype.f_g_get_elem r == None}
val f_no_elem (#dt: stateful unit) (#rtype: find_return_type dt)
    : r: f_rty rtype {rtype.f_g_get_elem r == None}
let f_no_elem (#dt : stateful unit) (#rtype : find_return_type dt) :
  r:f_rty rtype{rtype.f_g_get_elem r == None} =
  match rtype with
  | Mkfind_return_type rty get_elem from_elem no_elem -> no_elem
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))

/// Reflecting a stateful, imperative list as a functional one in a given heap.
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)

/// Whenever we use a function like [gfor_allP], it is better to introduce
/// an auxiliary predicate (otherwise, there are typing problems).
let dt_inv_free (#dt : stateful unit) (h : HS.mem) (x : dt_s dt) : GTot Type0 =
  dt_invariant #dt h x /\
  dt_freeable #dt h x

let elems_invariants: #dt:stateful unit -> h:HS.mem -> elems:list (dt_s dt) -> GTot Type0 =
  fun #dt h elems ->
  gfor_allP (dt_inv_free h) elems

noextract
val invariant: #dt:stateful unit -> h:HS.mem -> ll:t dt -> Type0

val region_of: #dt:stateful unit -> ll:t dt -> GTot B.loc

/// Various predicates
/// ------------------

let gsame_elementp (#dt: stateful unit) (h0 h1: HS.mem) :
  dt_s dt -> GTot Type0 =
  fun x -> dt_v h1 x == dt_v h0 x

let gsame_elementsp (#dt: stateful unit) (ll : list (dt_s dt)) (h0 h1: HS.mem) : GTot Type0 =
  gfor_allP (gsame_elementp h0 h1) ll

val gsame_elementsp_refl
  (#dt : stateful unit) (ll : list (dt_s dt)) (h0 : HS.mem) :
  Lemma
  (requires (elems_invariants h0 ll))
  (ensures (gsame_elementsp ll h0 h0))

val gsame_elementsp_trans (#dt: stateful unit) (ll : list (dt_s dt)) (h0 h1 h2: HS.mem) :
  Lemma
  (requires (gsame_elementsp ll h0 h1 /\ gsame_elementsp ll h1 h2))
  (ensures (gsame_elementsp ll h0 h2))

val gsame_elementsp_list_in_listP_trans
  (#dt: stateful unit) (ll0 ll1 : list (dt_s dt)) (h0 h1 h2: HS.mem) :
  Lemma
  (requires (
    gsame_elementsp ll0 h0 h1 /\
    gsame_elementsp ll1 h1 h2 /\
    list_in_listP ll0 ll1))
  (ensures (gsame_elementsp ll0 h0 h2))

val gsame_elementsp_elems_v_lem (#dt: stateful unit) (ll : list (dt_s dt)) (h0 h1: HS.mem) :
  Lemma
  (requires (gsame_elementsp ll h0 h1))
  (ensures (elems_v h1 ll == elems_v h0 ll))

/// The element [e] is an element in list [ll].
let list_owns_element (#dt: stateful unit) (h: HS.mem) (ll: t dt) (e: dt_s dt) : GTot Type0 =
  memP e (get_elems h ll)

/// Frame invariant
/// ---------------
val frame_invariant: #dt:stateful unit -> ll:t dt -> l:B.loc -> h0:HS.mem -> h1: HS.mem -> Lemma
  (requires
    invariant h0 ll /\
    B.loc_disjoint l (region_of ll) /\
    B.modifies l h0 h1)
  (ensures
    invariant h1 ll /\
    // The list of elements is the same
    get_elems h1 ll == get_elems h0 ll /\
    // The elmements themselves are left unchanged
    gsame_elementsp (get_elems h0 ll) h0 h1 /\
    // The following comes from the two preceding facts, but it is
    // more convenient if it is directly derived here
    v h1 ll == v h0 ll)
  [ SMTPatOr [
      [ SMTPat (invariant h0 ll); SMTPat (B.modifies l h0 h1) ];
    ]]

/// Elements lemmas and predicates
/// -----------------------------

val invariant_implies_elements_invariants :
     #dt:stateful unit
  -> h:HS.mem
  -> ll:t dt ->
  Lemma (requires invariant h ll)
  (ensures elems_invariants h (get_elems h ll))

/// Creating an imperative list
/// ---------------------------

inline_for_extraction noextract
val create_in: #dt:stateful unit -> r:HS.rid -> ST (t dt)
  (requires fun h0 ->
    ST.is_eternal_region r)
  (ensures fun h0 ll h1 ->
    invariant h1 ll /\
    B.(modifies loc_none h0 h1) /\
    v h1 ll == [] /\
    B.(loc_includes (loc_all_regions_from false r) (region_of ll)))

/// Find
/// ----

inline_for_extraction noextract
type fspec_ty (dt : stateful unit) = dt_t dt -> Tot bool

/// Type of a predicate function, used by [find] and [filter].
inline_for_extraction noextract
let pred_st (#dt: stateful unit) (ll: t dt)
            (l : Ghost.erased B.loc)
            (inv : HS.mem -> G.erased Type0)
            (inv_lem : (h0:HS.mem -> h1:HS.mem ->
                        Lemma
                        // Note that we allow the linked list to be modified between
                        // two calls: it is because we use [pred_st] both for [find]
                        // and [filter]
                        (requires (inv h0 /\ B.(modifies l h0 h1) /\ B.(equal_stack_domains h0 h1)))
                        (ensures (inv h1))))
            (spec: G.erased (fspec_ty dt)) =
  x:dt_s dt ->
  Stack bool
  (requires (fun h0 ->
    inv h0 /\
    dt_invariant h0 x /\
    B.loc_includes (region_of ll) (dt_footprint x)))
  (ensures (fun h0 b h1 ->
    B.(modifies loc_none h0 h1) /\ // This causes trouble because we use while loops
    inv h1 /\
    b = (G.reveal spec) (dt_v h0 x)))

/// The code of the find function can be customized a bit. By default, it is
/// convenient to return an option. However, the elements contained in the
/// list are often pointers, in which case we can simply return NULL if we
/// don't find a peer.

inline_for_extraction noextract
noeq type find_return_type (dt : stateful unit) = {
  // The return type
  f_rty : Type0;
  // Test if an element was found - for writing the specification only
  f_g_get_elem : (r:f_rty -> GTot (option (dt_s dt)));
  // Return an element
  f_from_elem : (e: dt_s dt -> r:f_rty{f_g_get_elem r == Some e});
  // No element found
  f_no_elem : r:f_rty{f_g_get_elem r == None};
}

inline_for_extraction noextract
let find_return_type_option dt =
{
  f_rty = option (dt_s dt);
  f_g_get_elem = (fun r -> r);
  f_from_elem = (fun x -> Some x);
  f_no_elem = None;  
}

/// Small helpers - without those, the code is not normalized correctly
inline_for_extraction noextract
let f_rty (#dt : stateful unit) (rtype : find_return_type dt) =
  match rtype with
  | Mkfind_return_type rty get_elem from_elem no_elem -> rty

inline_for_extraction noextract
let f_get_elem (#dt : stateful unit) (#rtype : find_return_type dt) :
  r:f_rty rtype -> GTot (option (dt_s dt)) =
  match rtype with
  | Mkfind_return_type rty get_elem from_elem no_elem -> get_elem

inline_for_extraction noextract
let f_from_elem (#dt : stateful unit) (#rtype : find_return_type dt) :
  e: dt_s dt -> r:f_rty rtype{rtype.f_g_get_elem r == Some e} =
  match rtype with
  | Mkfind_return_type rty get_elem from_elem no_elem -> from_elem
/
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
r:
Impl.Noise.LinkedList.f_rty rtype
  {Mkfind_return_type?.f_g_get_elem rtype r == FStar.Pervasives.Native.None}
Impl.Noise.LinkedList.stateful Prims.unit Impl.Noise.LinkedList.find_return_type FStar.Pervasives.Native.option Impl.Noise.LinkedList.dt_s Prims.eq2 FStar.Pervasives.Native.Some FStar.Pervasives.Native.None Impl.Noise.LinkedList.f_rty Impl.Noise.LinkedList.__proj__Mkfind_return_type__item__f_g_get_elem
let f_no_elem (#dt: stateful unit) (#rtype: find_return_type dt)
    : r: f_rty rtype {rtype.f_g_get_elem r == None} =
  
match rtype with | Mkfind_return_type rty get_elem from_elem no_elem -> no_elem