val filtered_footprint_invariants_lem
  (#dt : stateful unit) (filter_all : bool) (fspec : dt_s dt -> GTot bool)
  (ll : list (dt_s dt)) (h0 : HS.mem) :
  Lemma
  (requires (elems_invariants h0 ll))
  (ensures (
    let filtered = gfilter_gen filter_all fspec ll in
    elems_invariants h0 filtered /\
    B.loc_includes (elems_footprint ll) (elems_footprint filtered)))
val filtered_footprint_invariants_lem
  (#dt : stateful unit) (filter_all : bool) (fspec : dt_s dt -> GTot bool)
  (ll : list (dt_s dt)) (h0 : HS.mem) :
  Lemma
  (requires (elems_invariants h0 ll))
  (ensures (
    let filtered = gfilter_gen filter_all fspec ll in
    elems_invariants h0 filtered /\
    B.loc_includes (elems_footprint ll) (elems_footprint filtered)))
let rec filtered_footprint_invariants_lem #dt filter_all fspec ll h0 =
  match ll with
  | [] -> ()
  | x :: ll' -> filtered_footprint_invariants_lem #dt filter_all fspec ll' h0
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)]

#push-options "--fuel 1 --ifuel 1"
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
#pop-options

val elems_frame :
     #dt:stateful unit
  -> elems:list (dt_s dt)
  -> l:B.loc
  -> h0:HS.mem
  -> h1:HS.mem ->
  Lemma
  (requires (
    elems_invariants h0 elems /\
    elems_pairwise_disjoint elems /\
    B.loc_disjoint l (elems_footprint elems) /\
    B.modifies l h0 h1))
  (ensures (
    elems_invariants h1 elems /\
    elems_pairwise_disjoint 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 h0 elems == elems_v h1 elems))
  [ SMTPat (elems_invariants h0 elems);
    SMTPat (B.modifies l h0 h1)]

let elems_frame #dt elems l h0 h1 =
  elems_frame_invariant elems l h0 h1

#push-options "--fuel 1 --ifuel 1"
let rec gsame_elementsp_refl ll h0 =
  match ll with
  | [] -> ()
  | x :: ll' -> gsame_elementsp_refl ll' h0
#pop-options

/// Same as the above lemma, but with an SMT pattern to trigger locally
val gsame_elementsp_refl_smt
  (#dt : stateful unit) (ll : list (dt_s dt)) (h0 : HS.mem) :
  Lemma
  (requires (elems_invariants h0 ll))
  (ensures (gsame_elementsp ll h0 h0))
  [SMTPat (gsame_elementsp ll h0 h0)]

let gsame_elementsp_refl_smt #dt ll h0 =
  gsame_elementsp_refl #dt ll h0

let gsame_elementsp_trans #dt ll h0 h1 h2 =
  assert(gsame_elementsp ll h0 h1);
  assert(gsame_elementsp ll h1 h2);
  list_in_listP_refl ll;
  gfor_allP_list_in_listP_and
    (fun x -> dt_v h1 x == dt_v h0 x)
    (fun x -> dt_v h2 x == dt_v h1 x)
    (fun x -> dt_v h2 x == dt_v h0 x) (fun x -> ())
    ll ll

let gsame_elementsp_list_in_listP_trans #dt ll0 ll1 h0 h1 h2 =
  assert(gsame_elementsp ll0 h0 h1);
  assert(gsame_elementsp ll1 h1 h2);
  gfor_allP_list_in_listP (fun x -> dt_v h2 x == dt_v h1 x) ll0 ll1;
  assert(gsame_elementsp ll0 h1 h2);
  gsame_elementsp_trans #dt ll0 h0 h1 h2

#push-options "--fuel 1 --ifuel 1"
let rec gsame_elementsp_elems_v_lem #dt ll h0 h1 =
  match ll with
  | [] -> ()
  | x :: ll' -> gsame_elementsp_elems_v_lem ll' h0 h1
#pop-options

let frame_invariant #dt ll l h0 h1 =
  let ls = B.deref h0 ll.ptr in
  let elems = B.deref h0 ll.elems in
  elems_frame_invariant elems l h0 h1;
  LL1.frame ls elems l h0 h1

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

let glist_owns_element (#dt: stateful unit) (ll: list (dt_s dt)) (e: dt_s dt) : GTot Type0 =
  memP e ll

let invariant_implies_elements_invariants #dt h ll = ()

#push-options "--z3rlimit 50 --fuel 1"
let create_in #dt r =
  (**) let h0 = get () in
  let r' = ST.new_region r in
  (**) assert(B.(loc_includes (loc_all_regions_from false r) (loc_all_regions_from false r')));
  let r_new = ST.new_region r' in
  let r_misc = ST.new_region r' in
  let r_spine = ST.new_region r' in
  let ptr = B.malloc r_misc (B.null <: LL1.t (dt_s dt)) 1ul in
  let elems = B.malloc r_misc (G.hide ([] <: list (dt_s dt))) 1ul in
  let r_new_ptr = B.malloc r_misc r_new 1ul in
  { ptr = ptr; elems = elems; r = r'; r_spine = r_spine; r_new = r_new_ptr }
#pop-options

val elements_list_footprint :
  #dt:stateful unit ->
  h:HS.mem ->
  ll:LL1.t (dt_s dt) ->
  llv:Ghost.erased (list (dt_s dt)) ->
  Ghost B.loc (requires (LL1.well_formed h ll llv)) (ensures (fun _ -> True))

let elements_list_footprint #dt h ll llv =
  B.loc_union (LL1.footprint h ll llv) (elems_footprint llv)

val elements_list_invariant:
  #dt:stateful unit ->
  h:HS.mem ->
  ll:LL1.t (dt_s dt) ->
  llv:Ghost.erased (list (dt_s dt)) ->
  GTot Type0

let elements_list_invariant #dt h ll llv =
  LL1.well_formed h ll llv /\
  LL1.invariant h ll llv /\
  elems_invariants #dt h llv /\
  elems_pairwise_disjoint #dt llv /\
  B.loc_disjoint (LL1.footprint h ll llv) (elems_footprint llv)

val elements_list_frame_invariant :
  #dt:stateful unit ->
  ll:LL1.t (dt_s dt) ->
  llv:Ghost.erased (list (dt_s dt)) ->
  l:B.loc ->
  h0:HS.mem ->
  h1:HS.mem ->
  Lemma
  (requires (
    elements_list_invariant h0 ll llv /\
    B.modifies l h0 h1 /\
    B.loc_disjoint l (elements_list_footprint h0 ll llv)))
  (ensures (
    elements_list_invariant h1 ll llv /\
    gsame_elementsp llv h0 h1 /\
    elems_v h1 llv == elems_v h0 llv))
  [SMTPat (B.modifies l h0 h1); SMTPat (elements_list_invariant h0 ll llv)]

let elements_list_frame_invariant #dt ll llv l h0 h1 =
  elems_frame llv l h0 h1

let ll1_pred_inv_lem
  (#dt: stateful unit)
  (l_ref : B.loc)
  (inv : HS.mem -> G.erased Type0) =
  h0:HS.mem -> l:B.loc -> h1:HS.mem ->
  Lemma
  (requires (
    inv h0 /\
    B.modifies l h0 h1 /\
    ST.equal_stack_domains h0 h1 /\
    B.loc_includes l_ref l))
  (ensures (inv h1))
  [SMTPat (inv h0); SMTPat (B.modifies l h0 h1)]

/// This signature (and a lot others later) take [l_all] and [l_mod] locs as
/// parameters. In some situations, it would be possible to not take those
/// as parameters, but we still use them because otherwise adding terms
/// of the form [B.loc_union (elements_list_footprint ...) ...] everywhere
/// really clutters the code.
inline_for_extraction noextract
let ll1_pred_st
  (#dt: stateful unit)
  (l_all l_mod : B.loc)
  (inv : HS.mem -> G.erased Type0)
  (inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (spec: G.erased (fspec_ty dt)) =
  x:dt_s dt ->
  Stack bool
  (requires (fun h0 ->
    inv h0 /\
    dt_invariant h0 x /\
    B.loc_includes l_all (dt_footprint x)))
  (ensures (fun h0 b h1 ->
    B.(modifies loc_none h0 h1) /\
    b = (G.reveal spec) (dt_v h0 x)))

// Below, we don't need to take [l_mod] as parameter,
// but it is more convenient and readable.
let find_loop_pre
  (#dt: stateful unit)
  (l_all l_mod : G.erased B.loc)
  (lltp : B.pointer (LL1.t (dt_s dt)))
  (llvp : B.pointer (Ghost.erased (list (dt_s dt))))
  (#inv : HS.mem -> G.erased Type0)
  (#inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (#fspec : G.erased (fspec_ty dt))
  (f : ll1_pred_st l_all l_mod inv inv_lem fspec) =
  (fun h0 ->
    let llt = B.deref h0 lltp in
    let llv = B.deref h0 llvp in
    B.live h0 lltp /\ B.live h0 llt /\ B.live h0 llvp /\
    elements_list_invariant h0 llt llv /\
    inv h0 /\
    begin
    let tp_loc = B.loc_addr_of_buffer lltp in
    let vp_loc = B.loc_addr_of_buffer llvp in
    let ll_loc = elements_list_footprint h0 llt llv in
    B.all_disjoint [tp_loc; vp_loc; ll_loc] /\
    G.reveal l_mod == B.(loc_buffer lltp `loc_union` loc_buffer llvp) /\
    B.loc_includes l_all ll_loc /\
    True
    end)

/// The main part of the [find] function, which contains the while loop
inline_for_extraction noextract
val find_loop
  (#dt: stateful unit)
  (l_all l_mod : G.erased B.loc)
  (lltp : B.pointer (LL1.t (dt_s dt)))
  (llvp : B.pointer (Ghost.erased (list (dt_s dt))))
  (#inv : HS.mem -> G.erased Type0)
  (#inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (#fspec : G.erased (fspec_ty dt))
  (f : ll1_pred_st l_all l_mod inv inv_lem fspec) :
  Stack unit
  (requires find_loop_pre #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f)

  (ensures (fun h0 unit h1 ->
    let llv0 = B.deref h0 llvp in
    let llv1 = B.deref h1 llvp in
    let llt1 = B.deref h1 lltp in
    B.(modifies l_mod h0 h1) /\
    B.live h1 lltp /\ B.live h1 llt1 /\ B.live h1 llvp /\
    elements_list_invariant h1 llt1 llv1 /\
    inv h1 /\
    begin
    let r_v = L.tryFind fspec (elems_v h0 llv0) in
    match not (B.g_is_null llt1) with
    | false -> r_v == None
    | true ->
      begin
      let x = (B.deref h1 llt1).LL1.data in
      r_v == Some (dt_v h1 x) /\
      dt_invariant #dt h1 x /\
      dt_freeable #dt h1 x /\
      B.loc_includes l_all (dt_footprint #dt x) /\
      glist_owns_element llv0 x /\
      True
      end
    end))

inline_for_extraction noextract
let find_loop_inv
  (#dt: stateful unit)
  (l_all l_mod : G.erased B.loc)
  (lltp : B.pointer (LL1.t (dt_s dt)))
  (llvp : B.pointer (Ghost.erased (list (dt_s dt))))
  (#inv : HS.mem -> G.erased Type0)
  (#inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (#fspec : G.erased (fspec_ty dt))
  (f : ll1_pred_st l_all l_mod inv inv_lem fspec)
  (h00: HS.mem { find_loop_pre #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 })
=
  fun h0 ->
  let llt0 = B.deref h00 lltp in
  let llv0 = B.deref h00 llvp in
  let llt = B.deref h0 lltp in
  let llv = B.deref h0 llvp in
  B.live h0 lltp /\ B.live h0 llt /\ B.live h0 llvp /\
  elements_list_invariant h0 llt llv /\
  inv h0 /\
  begin
  let ll0_loc = elements_list_footprint h00 llt0 llv0 in
  let ll_loc = elements_list_footprint h0 llt llv in
  B.loc_includes ll0_loc ll_loc /\
  B.(modifies l_mod h00 h0) /\
  L.tryFind fspec (elems_v h00 llv0) == L.tryFind fspec (elems_v h0 llv) /\
  list_in_listP llv llv0 /\
  True
  end

inline_for_extraction noextract
let find_loop_guard
  (#dt: stateful unit)
  (l_all l_mod : G.erased B.loc)
  (lltp : B.pointer (LL1.t (dt_s dt)))
  (llvp : B.pointer (Ghost.erased (list (dt_s dt))))
  (#inv : HS.mem -> G.erased Type0)
  (#inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (#fspec : G.erased (fspec_ty dt))
  (f : ll1_pred_st l_all l_mod inv inv_lem fspec)
  (h00: HS.mem { find_loop_pre #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 })
  (h0:HS.mem{find_loop_inv #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 h0}): GTot bool =
  let llt = B.deref h0 lltp in
  if B.g_is_null llt then false
  else
    let x = (B.deref h0 llt).LL1.data in
    not (Ghost.reveal fspec (dt_v h0 x))

#push-options "--fuel 1 --ifuel 1"
inline_for_extraction noextract
let find_loop_test
  (#dt: stateful unit)
  (l_all l_mod : G.erased B.loc)
  (lltp : B.pointer (LL1.t (dt_s dt)))
  (llvp : B.pointer (Ghost.erased (list (dt_s dt))))
  (#inv : HS.mem -> G.erased Type0)
  (#inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (#fspec : G.erased (fspec_ty dt))
  (f : ll1_pred_st l_all l_mod inv inv_lem fspec)
  (h00: HS.mem { find_loop_pre #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 })
  ():
  Stack bool (requires find_loop_inv #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00)
  (ensures  fun h0 b h1 -> b == find_loop_guard #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 h0 /\
            B.(modifies loc_none h0 h1)) =
  (**) let h0 = get () in
  let llt = B.index lltp 0ul in
  let llv = B.index llvp 0ul in
  if B.is_null llt then
    false
  else
    begin
    let c = B.index llt 0ul in
    (**) let h1 = get () in
    [@inline_let] let x = c.LL1.data in
    begin
    (**) inv_lem h0 B.loc_none h1;
    (**) dt_frame_invariant #dt B.loc_none x h0 h1;
    (**) dt_frame_freeable #dt B.loc_none x h0 h1;
    (**) LL1.frame llt llv B.loc_none h0 h1;
    (**) elems_frame_invariant #dt llv B.loc_none h0 h1
    end;
    let b = f x in
    (**) let h2 = get () in
    (**) inv_lem h1 B.loc_none h2;
    (**) dt_frame_invariant #dt B.loc_none x h1 h2;
    (**) dt_frame_freeable #dt B.loc_none x h1 h2;
    (**) LL1.frame llt llv B.loc_none h1 h2;
    (**) elems_frame_invariant #dt llv B.loc_none h1 h2;
    not b
    end

inline_for_extraction noextract
let find_loop_test_
  (#dt: stateful unit)
  (l_all l_mod : G.erased B.loc)
  (lltp : B.pointer (LL1.t (dt_s dt)))
  (llvp : B.pointer (Ghost.erased (list (dt_s dt))))
  (#inv : HS.mem -> G.erased Type0)
  (#inv_lem : ll1_pred_inv_lem #dt l_mod inv)
  (#fspec : G.erased (fspec_ty dt))
  (f : ll1_pred_st l_all l_mod inv inv_lem fspec)
  (h00: HS.mem { find_loop_pre #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 })
  ():
  Stack bool (requires find_loop_inv #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00)
  (ensures  fun _ b h -> find_loop_inv #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 h /\
    b == find_loop_guard #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 h)
=
  (**) let h0 = get () in
  (**) assert(inv h0);
  let b = find_loop_test #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 () in
  (**) let h1 = get () in
  begin
  (**) let llt = B.deref h0 lltp in
  (**) let llv = B.deref h0 llvp in
  (**) elements_list_frame_invariant #dt llt llv B.loc_none h0 h1;
  (**) inv_lem h0 B.loc_none h1;
  (**) assert(inv h1)
  end;
  b

let find_loop #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f =
  (**) let h00 = get () in
  [@inline_let]
  let inv' : HS.mem -> Type0 = find_loop_inv #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 in

  [@inline_let]
  let guard = find_loop_guard #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00 in

  [@inline_let]
  let test: unit -> Stack bool
    (requires (fun h -> inv' h))
    (ensures  fun _ b h -> inv' h /\ b == guard h)
  =
    find_loop_test_ #dt l_all l_mod lltp llvp #inv #inv_lem #fspec f h00
  in

  [@inline_let]
  let body : (unit -> Stack unit
                    (requires fun h -> inv' h /\ guard h)
                    (ensures  fun _ _ h -> inv' h)) =
    fun () ->
    (**) let h0 = get () in
    let llt = B.index lltp 0ul in
    let llv = B.index llvp 0ul in
    let c = B.index llt 0ul in
    B.upd lltp 0ul c.LL1.next;
    B.upd llvp 0ul (L.tl llv);
    (**) let h1 = get () in
    begin
    (**) assert(B.modifies l_mod h0 h1);
    (**) inv_lem h0 l_mod h1;
    (**) LL1.frame llt llv l_mod h0 h1;
    (**) elems_frame_invariant llv l_mod h0 h1
    end
  in
  
  // The original list is included in itself
  (**) list_in_listP_refl (B.deref h00 llvp);
  (**) assert(inv' h00);

  C.Loops.while #(fun h -> inv' h) #(fun b h -> inv' h /\ b == guard h) test body
#pop-options

#push-options "--z3rlimit 100 --fuel 1 --ifuel 1"
let find #dt ll #inv #inv_lem #fspec rtype f =
  (**) let h0 = get () in
  let llt: LL1.t (dt_s dt) = !* ll.ptr in
  let llv = !* ll.elems in
  (**) let h1 = get () in
  (**) assert(invariant #dt h1 ll);
  push_frame ();
  let lltp: B.buffer (LL1.t (dt_s dt)) = B.alloca llt 1ul in
  let llvp = B.alloca llv 1ul in
  (**) let h2 = get () in
  ST.recall_region ll.r;
  (**) let tp_loc = Ghost.hide B.(loc_buffer lltp) in
  (**) let vp_loc = Ghost.hide B.(loc_buffer llvp) in
  (**) let l_mod = Ghost.hide B.(loc_union tp_loc vp_loc) in
  (**) let ll_loc = Ghost.hide (elements_list_footprint #dt h0 llt llv) in
  (**) let l_mod = Ghost.hide B.(loc_union tp_loc vp_loc) in
  (**) let l_all = Ghost.hide (region_of #dt ll) in
  (**) assert(B.(loc_disjoint (loc_all_regions_from false ll.r) tp_loc));
  (**) assert(B.(loc_disjoint (loc_all_regions_from false ll.r) vp_loc));
  [@inline_let]
  let inv' : HS.mem -> Ghost.erased Type0=
    fun h ->
    B.(modifies loc_none h1 h) /\
    B.live h lltp /\
    B.live h llvp /\
    B.(fresh_loc (loc_addr_of_buffer lltp)) h1 h /\
    B.(fresh_loc (loc_addr_of_buffer llvp)) h1 h /\
    B.(loc_includes (loc_region_only true (HS.get_tip h)) l_mod) /\
    inv h
  in
  [@inline_let]
  let inv_lem' : ll1_pred_inv_lem #dt l_mod inv' =
    fun h0' l h1' ->
    (**) B.(modifies_only_not_unused_in loc_none h1 h1');
    (**) assert(B.(modifies loc_none h1 h1'));
    (**) inv_lem h1 h1';
    (**) assert(B.(fresh_loc (loc_addr_of_buffer lltp)) h1 h1');
    (**) assert(B.(fresh_loc (loc_addr_of_buffer llvp)) h1 h1');
    (**) assert(B.(loc_includes (loc_region_only true (HS.get_tip h1')) l_mod))
  in
  [@inline_let]
  let f' : ll1_pred_st l_all l_mod inv' inv_lem' fspec =
    fun x -> f x
  in
  (**) B.(modifies_only_not_unused_in loc_none h1 h2);
  (**) elements_list_frame_invariant #dt llt llv B.loc_none h1 h2;
  (**) assert(elements_list_invariant #dt h2 llt llv);
  (**) inv_lem h1 h2;
  find_loop #dt l_all l_mod lltp llvp #inv' #inv_lem' #fspec f';
  (**) let h3 = get () in
  (**) assert(B.modifies l_mod h2 h3);
  let llt = !* lltp in 
  let res: f_rty rtype =
    if B.is_null llt then f_no_elem
    else
      begin
      let c: LL1.cell (dt_s dt) = !* llt in
      [@inline_let] let x = c.LL1.data in
      f_from_elem x
      end
  in
  pop_frame ();
  (**) let h4 = get () in
  begin
  (**) let r_stack = FStar.Monotonic.HyperStack.get_tip h2 in
  (**) assert(B.modifies (B.loc_region_only false r_stack) h3 h4);
  (**) begin match f_get_elem res with
  (**) | None -> ()
  (**) | Some res -> dt_frame_invariant #dt (B.loc_region_only false r_stack) res h3 h4
  (**) end;
  (**) B.(modifies_only_not_unused_in loc_none h0 h4);
  (**) inv_lem h0 h4
  end;
  res
#pop-options

let _ = ()

/// Adding elements
/// ---------------

#restart-solver
#push-options "--z3rlimit 50 --fuel 1 --ifuel 1"
let push #dt ll input =
  (**) let h0 = get () in
  let r_new = !* ll.r_new in
  let r_elem = ST.new_region r_new in
  let r_new' = ST.new_region r_new in
  (**) let h1 = get () in
  (**) dt.smfi_input.frame_invariant B.loc_none input h0 h1;
  (**) frame_invariant ll B.loc_none h0 h1;
  let x = dt_malloc #dt r_elem input in
  (**) let h2 = get () in
  (**) frame_invariant ll B.loc_none h1 h2;
  LL1.push ll.r_spine (!* ll.elems) ll.ptr x;
  (**) let h3 = get () in
  (**) assert(B.(modifies (loc_buffer ll.ptr) h2 h3));
  let elems = !* ll.elems in
  begin
  (**) let r_new_loc = B.loc_all_regions_from false r_new in
  (**) let r_elem_loc = B.loc_all_regions_from false r_elem in
  (**) let r_new'_loc = B.loc_all_regions_from false r_new' in
  (**) assert(B.loc_includes r_new_loc r_elem_loc);
  (**) assert(B.loc_includes r_new_loc r_new'_loc);
  (**) assert(B.loc_includes r_elem_loc (dt_footprint x));
  (**) assert(B.loc_includes r_new_loc (dt_footprint x)); // This one is necessary: otherwise, patterns won't trigger
  (**) assert(B.loc_disjoint (dt_footprint x) (elems_footprint elems));
  (**) disjoint_from_footprint_implies_elems_pairwise_disjoint x elems
  end;
  ll.elems *= G.hide (x :: elems);
  ll.r_new *= r_new';
  (**) let h5 = get () in
  begin
  (**) let ptr_loc = B.loc_buffer ll.ptr in
  (**) let elems_ptr_loc = B.loc_buffer ll.elems in
  (**) let r_new_loc = B.loc_buffer ll.r_new in
  (**) let l = B.(ptr_loc `loc_union` elems_ptr_loc `loc_union` r_new_loc) in
  (**) assert(B.modifies l h0 h5);
  (**) dt_frame_invariant l x h2 h5;
  (**) dt_frame_freeable l x h2 h5;
  (**) elems_frame (B.deref h0 ll.elems) l h0 h5;
  (**) assert(dt_invariant h5 x);
  (**) assert(elems_invariants h5 (B.deref h5 ll.elems));
  (**) assert(invariant h5 ll)
  end;
  begin
  (**) let elems0 = B.deref h0 ll.elems in
  (**) let elems1 = B.deref h5 ll.elems in
  (**) assert(Cons? elems1);
  (**) assert(Cons?.tl elems1 == G.reveal elems0);
  (**) assert(gsame_elementsp elems0 h0 h5)
  end;
  x
#pop-options

/// Removing elements
/// -----------------

#push-options "--fuel 1 --ifuel 1"
let pop #dt ll =
  (**) let h0 = get () in
  let elem1 = LL1.pop ll.r_spine (!* ll.elems) ll.ptr in
  (**) let h1 = get () in
  begin
  (**) let elems = B.deref h0 ll.elems in
  (**) let l = B.(loc_buffer ll.ptr `loc_union` LL1.footprint h0 (B.deref h0 ll.ptr) elems) in
  (**) assert(B.(modifies l h0 h1));
  (**) assert(B.loc_disjoint l (dt_footprint elem1));
  (**) dt_frame_invariant l elem1 h0 h1;
  (**) dt_frame_freeable l elem1 h0 h1;
  (**) assert(dt_invariant h1 elem1);
  (**) assert(dt_freeable h1 elem1)
  end;
  dt_free #dt elem1;
  let elems = !* ll.elems in
  (**) let h2 = get () in
  ll.elems *= G.hide (L.tl elems);
  (**) let h3 = get () in
  begin
  (**) let elems_ptr_loc = B.loc_addr_of_buffer ll.elems in
  (**) let elem1_loc = dt_footprint elem1 in
  (**) let ll_loc = LL1.footprint h0 (B.deref h0 ll.ptr) elems in
  (**) let ll_ptr_loc = B.loc_buffer ll.ptr in
  (**) let l = B.(elems_ptr_loc `loc_union` elem1_loc `loc_union` ll_loc `loc_union` ll_ptr_loc) in
  (**) assert(B.(modifies l h0 h3));
  (**) let elems' = L.tl elems in
  (**) let elems'_loc = elems_footprint elems' in
  (**) assert(B.loc_disjoint elems_ptr_loc elems'_loc);
  (**) elems_pairwise_disjoint_implies_disjoint_from_footprint #dt elem1 elems';
  (**) assert(B.loc_disjoint elem1_loc elems'_loc);
  (**) assert(B.loc_disjoint ll_loc elems'_loc);
  (**) assert(B.loc_disjoint ll_ptr_loc elems'_loc);
  (**) assert(B.loc_disjoint l elems'_loc);
  (**) elems_frame elems' l h0 h3
  end
#pop-options


/// Filter/filter_one implementation non tail-call implementations:
/// We write one function which takes a meta parameter, used to switch
/// between filter and filter_one. This allows us to factorize the proofs.

let gfilter_gen (filter : bool) :
  #a: Type -> f:(a -> GTot bool) -> l: list a -> GTot (list a) =
  if filter then gfilter else gfilter_one

val gfilter_elements_same_lem
  (#dt: stateful unit)
  (ll: list (dt_s dt))
  (fspec : G.erased (fspec_ty dt))
  (h0 h1: HS.mem) :
  Lemma
  (requires (gsame_elementsp ll h0 h1))
  (ensures (
    gfilter_elements fspec h1 ll == gfilter_elements fspec h0 ll))
  [SMTPat (gsame_elementsp ll h0 h1);
   SMTPat (gfilter_elements fspec h0 ll)]

#push-options "--fuel 1 --ifuel 1"
let rec gfilter_elements_same_lem #dt ll fspec h0 h1 =
  match ll with
  | [] -> ()
  | x :: ll' -> gfilter_elements_same_lem ll' fspec h0 h1
#pop-options

val gfilter_one_element_same_lem
  (#dt: stateful unit)
  (ll: list (dt_s dt))
  (fspec : G.erased (fspec_ty dt))
  (h0 h1: HS.mem) :
  Lemma
  (requires (gsame_elementsp ll h0 h1))
  (ensures (
    gfilter_one_element fspec h1 ll == gfilter_one_element fspec h0 ll))
  [SMTPat (gsame_elementsp ll h0 h1);
   SMTPat (gfilter_one_element fspec h0 ll)]

#push-options "--fuel 1 --ifuel 1"
let rec gfilter_one_element_same_lem #dt ll fspec h0 h1 =
  match ll with
  | [] -> ()
  | x :: ll' -> gfilter_one_element_same_lem ll' fspec h0 h1
#pop-options

val frame_gsame_elementsp1
  (#dt : stateful unit) (ll : list (dt_s dt)) (l : B.loc)
  (h0 h1 h2 : HS.mem) :
  Lemma
  (requires (
    B.loc_disjoint l (elems_footprint ll) /\
    B.modifies l h1 h2 /\
    elems_invariants h1 ll /\
    gsame_elementsp ll h0 h1))
  (ensures (gsame_elementsp ll h0 h2))
  [SMTPat (B.modifies l h1 h2);
   SMTPat (gsame_elementsp ll h0 h1)]

// We could do the proofs in a smarter manner, but doing them by recursion is
// actually so simple...
#push-options "--fuel 1 --ifuel 1"
let rec frame_gsame_elementsp1 #dt ll l h0 h1 h2 =
  match ll with
  | [] -> ()
  | x :: ll' ->
    dt_frame_invariant l x h1 h2;
    frame_gsame_elementsp1 ll' l h0 h1 h2

val gfilter_elements_invariants_lem
  (#dt : stateful unit) (ll : list (dt_s dt))
  (fspec : G.erased (fspec_ty dt))
  (h : HS.mem) :
  Lemma (requires (elems_invariants h ll))
  (ensures (
    elems_invariants h (gfilter_elements fspec h ll)))

val frame_gsame_elementsp2
  (#dt : stateful unit) (ll : list (dt_s dt)) (l : B.loc)
  (h0 h1 h2 : HS.mem) :
  Lemma
  (requires (
    B.loc_disjoint l (elems_footprint ll) /\
    B.modifies l h0 h1 /\
    elems_invariants h0 ll /\
    gsame_elementsp ll h1 h2))
  (ensures (gsame_elementsp ll h0 h2))
  [SMTPat (B.modifies l h0 h1);
   SMTPat (gsame_elementsp ll h1 h2)]

let rec frame_gsame_elementsp2 #dt ll l h0 h1 h2 =
  match ll with
  | [] -> ()
  | x :: ll' ->
    dt_frame_invariant l x h0 h1;
    frame_gsame_elementsp2 ll' l h0 h1 h2

#push-options "--fuel 1 --ifuel 1"
let rec gfilter_elements_invariants_lem #dt ll fspec h =
  match ll with
  | [] -> ()
  | x :: ll' -> gfilter_elements_invariants_lem ll' fspec h
#pop-options

val gfilter_one_element_invariants_lem
  (#dt : stateful unit) (ll : list (dt_s dt))
  (fspec : G.erased (fspec_ty dt))
  (h : HS.mem) :
  Lemma (requires (elems_invariants h ll))
  (ensures (
    elems_invariants h (gfilter_one_element fspec h ll)))
  [SMTPat (elems_invariants h (gfilter_one_element fspec h ll))]

#push-options "--fuel 1 --ifuel 1"
let rec gfilter_one_element_invariants_lem #dt ll fspec h =
  match ll with
  | [] -> ()
  | x :: ll' -> gfilter_one_element_invariants_lem ll' fspec h
#pop-options

val gfilter_one_element_cons_elems_pairwise_disjoint
  (#dt : stateful unit) (x : dt_s dt) (ll : list (dt_s dt))
  (fspec : G.erased (fspec_ty dt))
  (h : HS.mem) :
  Lemma (requires (
//    elems_invariants h (x :: ll) /\
    elems_pairwise_disjoint (x :: ll)))
  (ensures (
    elems_pairwise_disjoint (x :: gfilter_one_element fspec h ll)))
  (decreases ll)
  [SMTPat (elems_pairwise_disjoint (x :: gfilter_one_element fspec h ll))]

#push-options "--fuel 2 --ifuel 2"
let rec gfilter_one_element_cons_elems_pairwise_disjoint #dt x ll fspec h =
  match ll with
  | [] -> ()
  | x' :: ll' ->
    if filter_pred fspec h x' then
      begin
      gfilter_one_element_cons_elems_pairwise_disjoint #dt x ll' fspec h;
      gfilter_one_element_cons_elems_pairwise_disjoint #dt x' ll' fspec h
      end
    else
      begin
      assert(gfilter_one_element fspec h ll == ll')
      end
#pop-options

val gsame_elementsp_modifies (#dt: stateful unit) (ll : list (dt_s dt)) (l : B.loc) (h0 h1: HS.mem) :
  Lemma
  (requires (
    B.(modifies l h0 h1) /\
    elems_invariants h0 ll /\
    B.loc_disjoint l (elems_footprint #dt ll)))
  (ensures (gsame_elementsp ll h0 h1))
  [SMTPat (B.(modifies l h0 h1));
   SMTPat (elems_invariants h0 ll)]

#push-options "--ifuel 1 --fuel 1"
let rec gsame_elementsp_modifies #dt ll l h0 h1 =
  match ll with
  | [] -> ()
  | x :: ll' -> gsame_elementsp_modifies ll' l h0 h1
#pop-options
#pop-options

val gsame_elementsp_modifies_lem
  (#dt : stateful unit) (ll : list (dt_s dt)) (l : B.loc) (h0 h1 : HS.mem) :
  Lemma
  (requires (
    elems_invariants h0 ll /\
    B.(modifies l h0 h1) /\
    B.(loc_disjoint (elems_footprint ll) l)))
  (ensures (
    gsame_elementsp ll h0 h1))
  [SMTPat (gsame_elementsp ll h0 h1);
   SMTPat (elems_invariants h0 ll);
   SMTPat (B.(modifies l h0 h1))]

let gsame_elementsp_modifies_lem #dt ll l h0 h1 =
  gsame_elementsp_refl ll h0

val gfilter_one_element_eq_lem
  (#dt: stateful unit) (fspec : G.erased (fspec_ty dt))
  (ll : list (dt_s dt)) (l : B.loc) (h0 h1 : HS.mem) :
  Lemma
  (requires (
    B.(modifies l h0 h1) /\
    elems_invariants h0 ll /\
    B.loc_disjoint l (elems_footprint #dt ll)))
  (ensures (
    gfilter_one_element fspec h0 ll == gfilter_one_element fspec h1 ll))
  [SMTPat (B.(modifies l h0 h1));
   SMTPat (B.loc_disjoint l (elems_footprint #dt ll));
   SMTPat (gfilter_one_element fspec h1 ll)]

#push-options "--ifuel 1 --fuel 1"
let rec gfilter_one_element_eq_lem #dt fspec ll l h0 h1 =
  match ll with
  | [] -> ()
  | x :: ll' -> gfilter_one_element_eq_lem #dt fspec ll' l h0 h1
#pop-options

val gsame_elementsp_gfilter_one_element_eq_lem
  (#dt: stateful unit) (fspec : G.erased (fspec_ty dt))
  (ll : list (dt_s dt)) (h0 h1 : HS.mem) :
  Lemma
  (requires (
    gsame_elementsp ll h0 h1))
  (ensures (
    gfilter_one_element fspec h0 ll == gfilter_one_element fspec h1 ll))
  [SMTPat (gsame_elementsp ll h0 h1);
   SMTPat (gfilter_one_element fspec h1 ll)]

#push-options "--ifuel 1 --fuel 1"
let rec gsame_elementsp_gfilter_one_element_eq_lem #dt fspec ll h0 h1 =
  match ll with
  | [] -> ()
  | x :: ll' -> gsame_elementsp_gfilter_one_element_eq_lem #dt fspec ll' h0 h1
#pop-options

val filtered_footprint_invariants_lem
  (#dt : stateful unit) (filter_all : bool) (fspec : dt_s dt -> GTot bool)
  (ll : list (dt_s dt)) (h0 : HS.mem) :
  Lemma
  (requires (elems_invariants h0 ll))
  (ensures (
    let filtered = gfilter_gen filter_all fspec ll in
    elems_invariants h0 filtered /\
    B.loc_includes (elems_footprint ll) (elems_footprint filtered)))
/
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

    filter_all: Prims.bool ->
    fspec: (_: Impl.Noise.LinkedList.dt_s dt -> Prims.GTot Prims.bool) ->
    ll: Prims.list (Impl.Noise.LinkedList.dt_s dt) ->
    h0: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma (requires Impl.Noise.LinkedList.elems_invariants h0 ll)
      (ensures
        (let filtered = Impl.Noise.LinkedList.gfilter_gen filter_all fspec ll in
          Impl.Noise.LinkedList.elems_invariants h0 filtered /\
          LowStar.Monotonic.Buffer.loc_includes (Impl.Noise.LinkedList.elems_footprint ll)
            (Impl.Noise.LinkedList.elems_footprint filtered)))
Impl.Noise.LinkedList.stateful Prims.unit Prims.bool Impl.Noise.LinkedList.dt_s Prims.list FStar.Monotonic.HyperStack.mem Impl.Noise.LinkedList.filtered_footprint_invariants_lem
let rec filtered_footprint_invariants_lem #dt filter_all fspec ll h0 =
  
match ll with
| [] -> ()
| x :: ll' -> filtered_footprint_invariants_lem #dt filter_all fspec ll' h0