val elems_frame_invariant :
     #dt:stateful unit
  -> elems:list (dt_s dt)
  -> l:B.loc
  -> h0:HS.mem
  -> h1:HS.mem ->
  Lemma
  (requires (
    elems_invariants h0 elems /\
    B.loc_disjoint l (elems_footprint elems) /\
    B.modifies l h0 h1))
  (ensures (
    elems_invariants h1 elems /\
    elems_footprint elems == elems_footprint elems /\
    // Two versions of the same property - one is used for the high-level
    // specification revealed to the user, the other is used to preserve
    // internal invariants
    gsame_elementsp elems h0 h1 /\
    elems_v h1 elems == elems_v h0 elems))
  [ SMTPat (elems_invariants h0 elems);
    SMTPat (B.modifies l h0 h1)]
val elems_frame_invariant :
     #dt:stateful unit
  -> elems:list (dt_s dt)
  -> l:B.loc
  -> h0:HS.mem
  -> h1:HS.mem ->
  Lemma
  (requires (
    elems_invariants h0 elems /\
    B.loc_disjoint l (elems_footprint elems) /\
    B.modifies l h0 h1))
  (ensures (
    elems_invariants h1 elems /\
    elems_footprint elems == elems_footprint elems /\
    // Two versions of the same property - one is used for the high-level
    // specification revealed to the user, the other is used to preserve
    // internal invariants
    gsame_elementsp elems h0 h1 /\
    elems_v h1 elems == elems_v h0 elems))
  [ SMTPat (elems_invariants h0 elems);
    SMTPat (B.modifies l h0 h1)]
let rec elems_frame_invariant #dt elems l h0 h1 =
  match elems with
  | [] -> ()
  | e :: elems' ->
    assert(dt_invariant #dt h0 e);
    assert(dt_freeable #dt h0 e);
    dt_frame_invariant l e h0 h1;
    dt_frame_freeable l e h0 h1;
    elems_frame_invariant elems' l 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) ]

let dt_frame_invariant_forward #dt l s h0 h1 = dt_frame_invariant l s h0 h1

val dt_frame_freeable_forward :
  #dt:stateful unit -> l:B.loc -> s:dt_s dt -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    dt_invariant h0 s /\
    dt_freeable h0 s /\
    B.loc_disjoint l (dt_footprint s) /\
    B.modifies l h0 h1))
  (ensures (
    dt_freeable h1 s))
  [ SMTPat (dt_freeable h0 s); SMTPat (B.modifies l h0 h1) ]

let dt_frame_freeable_forward #dt l s h0 h1 = dt_frame_freeable l s h0 h1

#push-options "--ifuel 1"
val elems_footprint: #dt:stateful unit -> ls:list (dt_s dt) -> GTot B.loc
let rec elems_footprint #dt ls =
  match ls with
  | [] -> B.loc_none
  | x :: ls' -> B.loc_union (dt_footprint x) (elems_footprint ls')
#pop-options

val elems_disjoint: #dt:stateful unit -> x:dt_s dt -> y:dt_s dt -> GTot Type0
let elems_disjoint #dt x y =
  B.loc_disjoint (dt_footprint x) (dt_footprint y)

#push-options "--ifuel 1"
val elems_pairwise_disjoint: #dt:stateful unit -> ls:list (dt_s dt) -> GTot Type0
let elems_pairwise_disjoint #dt ls =
  pairwise_grelP (elems_disjoint #dt) ls
#pop-options

val gfor_allP_elems_disjoint_implies_disjoint_from_footprint :
     #dt:stateful unit
  -> x:dt_s dt
  -> ls:list (dt_s dt) ->
  Lemma
  (requires (gfor_allP (elems_disjoint x) ls))
  (ensures (
    B.loc_disjoint (dt_footprint x) (elems_footprint ls)))

#push-options "--fuel 1 --ifuel 1"
let rec gfor_allP_elems_disjoint_implies_disjoint_from_footprint #dt x ls =
  match ls with
  | [] -> ()
  | y :: ls' ->
    gfor_allP_elems_disjoint_implies_disjoint_from_footprint x ls'
#pop-options

val disjoint_from_footprint_implies_gfor_allP_elems_disjoint :
     #dt:stateful unit
  -> x:dt_s dt
  -> ls:list (dt_s dt) ->
  Lemma
  (requires (B.loc_disjoint (dt_footprint x) (elems_footprint ls)))
  (ensures (gfor_allP (elems_disjoint x) ls))

#push-options "--fuel 1 --ifuel 1"
let rec disjoint_from_footprint_implies_gfor_allP_elems_disjoint #dt x ls =
  match ls with
  | [] -> ()
  | y :: ls' ->
    disjoint_from_footprint_implies_gfor_allP_elems_disjoint x ls'
#pop-options

val elems_pairwise_disjoint_implies_disjoint_from_footprint :
     #dt:stateful unit
  -> x:dt_s dt
  -> ls:list (dt_s dt) ->
  Lemma
  (requires (elems_pairwise_disjoint (x :: ls)))
  (ensures (B.loc_disjoint (dt_footprint x) (elems_footprint ls)))

#push-options "--fuel 1 --ifuel 1"
let elems_pairwise_disjoint_implies_disjoint_from_footprint #dt x ls =
  gfor_allP_elems_disjoint_implies_disjoint_from_footprint x ls
#pop-options

val disjoint_from_footprint_implies_elems_pairwise_disjoint :
     #dt:stateful unit
  -> x:dt_s dt
  -> ls:list (dt_s dt) ->
  Lemma
  (requires (
    elems_pairwise_disjoint ls /\
    B.loc_disjoint (dt_footprint x) (elems_footprint ls)))
  (ensures (elems_pairwise_disjoint (x :: ls)))

#push-options "--fuel 1 --ifuel 1"
let disjoint_from_footprint_implies_elems_pairwise_disjoint #dt x ls =
  disjoint_from_footprint_implies_gfor_allP_elems_disjoint x ls
#pop-options

val elems_invariants_hd_lem:
  #dt:stateful unit -> h:HS.mem -> x:dt_s dt -> elems:list (dt_s dt) ->
  Lemma (requires (elems_invariants h (x :: elems)))
  (ensures (
    dt_invariant h x /\
    dt_freeable h x /\
    elems_invariants h elems))
#push-options "--fuel 1 --ifuel 1"
let elems_invariants_hd_lem #dt h x elems = ()
#pop-options

let invariant #dt h ll =
  let head = B.deref h ll.ptr in
  let elems = B.deref h ll.elems in
  let r_new = B.deref h ll.r_new in

  B.live h ll.ptr /\
  B.freeable ll.ptr /\
  B.live h ll.elems /\
  B.freeable ll.elems /\
  B.live h ll.r_new /\
  B.freeable ll.r_new /\
  LL1.well_formed h head elems /\
  LL1.invariant h head elems /\
  elems_invariants h elems /\

  // We use regions for separation only, not for any footprint reasoning:
  // - ptr_v_rid is a sub-region of r and contains ptr and v, disjoint from each other
  // - spine_rid is a sub-region of r, disjoint from ptr_v_rid, and contains the LL1.footprint
  ll.r =!= FStar.Monotonic.HyperHeap.root /\
  ST.is_eternal_region ll.r /\
  ST.is_eternal_region r_new /\
  ST.is_eternal_region ll.r_spine /\
  begin
  let r_loc = B.loc_all_regions_from false ll.r in
  let r_new_ptr_loc = B.loc_addr_of_buffer ll.r_new in
  let r_new_loc = B.loc_all_regions_from false r_new in
  let r_spine_loc = B.loc_region_only true ll.r_spine in
  let ptr_loc = B.loc_addr_of_buffer ll.ptr in
  let elems_ptr_loc = B.loc_addr_of_buffer ll.elems in
  let spine_loc = LL1.footprint h head elems in
  let elems_loc = elems_footprint elems in
  B.all_disjoint [r_new_ptr_loc; r_new_loc; r_spine_loc; ptr_loc; elems_ptr_loc; elems_loc] /\
  B.loc_includes r_loc r_new_ptr_loc /\
  B.loc_includes r_loc r_new_loc /\
  B.loc_includes r_loc r_spine_loc /\
  B.loc_includes r_loc ptr_loc /\
  B.loc_includes r_loc elems_ptr_loc /\
  B.loc_includes r_spine_loc spine_loc /\
  B.loc_includes r_loc elems_loc /\
  elems_pairwise_disjoint elems
  end

let region_of #dt ll = B.loc_all_regions_from false ll.r

/// Some utilities

val elems_frame_forall_disjoint :
     #dt:stateful unit
  -> e:dt_s dt
  -> elems:list (dt_s dt)
  -> l:B.loc
  -> h0:HS.mem
  -> h1:HS.mem ->
  Lemma
  (requires (
    gfor_allP (elems_disjoint e) elems /\
    B.loc_disjoint l (B.loc_union (dt_footprint e) (elems_footprint elems)) /\
    B.modifies l h0 h1))
  (ensures (
    gfor_allP (elems_disjoint e) elems))

#push-options "--fuel 2 --ifuel 2"
let rec elems_frame_forall_disjoint #dt e elems l h0 h1 =
  match elems with
  | [] -> ()
  | e' :: elems' ->
    elems_frame_forall_disjoint e elems' l h0 h1
#pop-options

val elems_frame_invariant :
     #dt:stateful unit
  -> elems:list (dt_s dt)
  -> l:B.loc
  -> h0:HS.mem
  -> h1:HS.mem ->
  Lemma
  (requires (
    elems_invariants h0 elems /\
    B.loc_disjoint l (elems_footprint elems) /\
    B.modifies l h0 h1))
  (ensures (
    elems_invariants h1 elems /\
    elems_footprint elems == elems_footprint elems /\
    // Two versions of the same property - one is used for the high-level
    // specification revealed to the user, the other is used to preserve
    // internal invariants
    gsame_elementsp elems h0 h1 /\
    elems_v h1 elems == elems_v h0 elems))
  [ SMTPat (elems_invariants h0 elems);
    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

    elems: Prims.list (Impl.Noise.LinkedList.dt_s dt) ->
    l: LowStar.Monotonic.Buffer.loc ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        Impl.Noise.LinkedList.elems_invariants h0 elems /\
        LowStar.Monotonic.Buffer.loc_disjoint l (Impl.Noise.LinkedList.elems_footprint elems) /\
        LowStar.Monotonic.Buffer.modifies l h0 h1)
      (ensures
        Impl.Noise.LinkedList.elems_invariants h1 elems /\
        Impl.Noise.LinkedList.elems_footprint elems == Impl.Noise.LinkedList.elems_footprint elems /\
        Impl.Noise.LinkedList.gsame_elementsp elems h0 h1 /\
        Impl.Noise.LinkedList.elems_v h1 elems == Impl.Noise.LinkedList.elems_v h0 elems)
      [
        SMTPat (Impl.Noise.LinkedList.elems_invariants h0 elems);
        SMTPat (LowStar.Monotonic.Buffer.modifies l h0 h1)
      ]
Impl.Noise.LinkedList.stateful Prims.unit Prims.list Impl.Noise.LinkedList.dt_s LowStar.Monotonic.Buffer.loc FStar.Monotonic.HyperStack.mem Impl.Noise.LinkedList.elems_frame_invariant Impl.Noise.LinkedList.dt_frame_freeable Impl.Noise.LinkedList.dt_frame_invariant Prims._assert Impl.Noise.LinkedList.dt_freeable Impl.Noise.LinkedList.dt_invariant
let rec elems_frame_invariant #dt elems l h0 h1 =
  
match elems with
| [] -> ()
| e :: elems' ->
  assert (dt_invariant #dt h0 e);
  assert (dt_freeable #dt h0 e);
  dt_frame_invariant l e h0 h1;
  dt_frame_freeable l e h0 h1;
  elems_frame_invariant elems' l h0 h1