val gfold_right (#a #b: _) (f: (b -> a -> GTot b)) (xs: list a) (acc: b)
    : Ghost b (requires True) (ensures fun _ -> True) (decreases xs)
let rec gfold_right #a #b (f: b -> a -> GTot b) (xs: list a) (acc: b): Ghost b
  (requires True)
  (ensures fun _ -> True)
  (decreases xs)
=
  match xs with
  | [] -> acc
  | x :: xs -> f (gfold_right f xs acc) x
val gfold_right (#a #b: _) (f: (b -> a -> GTot b)) (xs: list a) (acc: b)
    : Ghost b (requires True) (ensures fun _ -> True) (decreases xs)
let rec gfold_right #a #b (f: (b -> a -> GTot b)) (xs: list a) (acc: b)
    : Ghost b (requires True) (ensures fun _ -> True) (decreases xs) =
match xs with
| [] -> acc
| x :: xs -> f (gfold_right f xs acc) x
LowStar.Lib.LinkedList.fst.checked
TestLib.fsti.checked prims.fst.checked LowStar.Failure.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
LowStar.Lib.LinkedList.fst
Prims.list LowStar.Lib.LinkedList.gfold_right Prims.l_True
module LowStar.Lib.LinkedList

/// This module, oftentimes referred to as LL1 in other parts of the
/// documentation, provides a low-level view over a linked list. Unless you
/// intend on modifying the structure of the linked list (e.g. removing cells)
/// or iterating over each cell, your are probably better off using LL2.
///
/// This module is intentionally not relying on a tight abstraction, to i) permit
/// direct-style iteration by clients and ii) allow stating some SMTPat lemmas
/// only on LL1 rather than replicating them in LL2 (going from LL2 to LL1 can
/// happen automatically at the SMT level since LL2 does not have an fsti either).
///
/// Some open questions relative to the design of this module:
/// - should ``v`` be defined directly in terms of ``cells`` rather than have a
///   recursive definition along with an equivalence lemma?
/// - should ``footprint`` be defined directly in terms of ``cells`` rather than
///   have a recursive definition along with an equivalence lemma?
/// - is it worth the trouble defining a footprint? my intuition is that it's
///   fine and allows some clients to do very precise reasoning -- other modules
///   (e.g. AssocList), when establishing abstraction boundaries, can simplify
///   things and get rid of the precise footprint reasoning in favor of a static
///   region-based footprint
///
/// Some remaining work items:
/// - switch to C.Loops.while

open LowStar.BufferOps

module B = LowStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST

open FStar.HyperStack.ST

/// Breaking from my own recommendation here... using fuel 1 / ifuel 1 since
/// everything does recursive list reasoning.
#set-options "--__no_positivity --fuel 1 --ifuel 1"

/// Definition of the Low* type
/// ---------------------------
noeq
type t (a: Type0) =
  B.pointer_or_null (cell a)

and cell (a: Type0) = {
  next: t a;
  data: a;
}

/// Unlike the canonical style that associates a ``v`` function to any stateful
/// representation, we use a relation here. Writing a function is just
/// impossible, since we can't prove termination of ``v`` owing to the fact that
/// there may be an infinite number of cells in the heap.
///
/// LL2 is the module that switches to the function style.
///
/// Note: no need to use erased here for ``l`` since the function is already in ``GTot``.
let rec well_formed #a (h: HS.mem) (c: t a) (l: list a): GTot Type0 (decreases l) =
  B.live h c /\ (
  match l with
  | [] ->
    B.g_is_null c
  | a :: q ->
    B.length c == 1 /\ (
    let { data=data; next=next } = B.get h c 0 in
    a == data /\
    well_formed h next (G.hide q)
  ))

/// Precise reasoning via the cells predicate
/// -----------------------------------------
///
/// The modifies clauses are given either on the footprint of the list, or on a
/// region that includes the footprint of the list (higher up the stack, e.g.
/// LL2). This is good, but does not rule out "stupid" implementations that
/// might re-allocate every single list cell when, say, doing a pop.
///
/// For advanced usages which take pointers directly to individual list cells,
/// it's important to rule out these cases. We thus define the ``cells``
/// predicate for that purpose.

let rec cells #a (h: HS.mem) (c: t a) (l: list a): Ghost (list (B.pointer (cell a)))
  (requires well_formed h c l)
  (ensures fun _ -> True)
  (decreases l)
=
  if B.g_is_null c then
    []
  else
    c :: cells h (B.deref h c).next (List.Tot.tl l)

/// A missing bit of automated reasoning
/// ------------------------------------

/// This should be absolutely trivial, yet, because there's no pattern on
/// null_unique, we have to do the case analysis and the decomposition
/// ourselves. This is quite tedious, as it usually takes a while (at least it
/// did for me!) to realize that this property does not hold automatically.
///
/// I'm setting an SMTPat on this lemma because it's absolutely impossible to
/// get any work done without it.
let same_cells_same_pointer #a (h0 h1: HS.mem) (ll0 ll1: t a) (l0 l1: list a): Lemma
  (requires (
    well_formed h0 ll0 l0 /\
    well_formed h1 ll1 l1 /\
    cells h0 ll0 l0 == cells h1 ll1 l1))
  (ensures (
    ll0 == ll1))
  [ SMTPat (cells h0 ll0 l0); SMTPat (cells h1 ll1 l1) ]
=
  if B.g_is_null ll0 && B.g_is_null ll1 then begin
    B.null_unique ll0;
    B.null_unique ll1
  end else if not (B.g_is_null ll0) && not (B.g_is_null ll1) then begin
    ()
  end else
    false_elim ()

/// Classic stateful reasoning lemmas
/// ---------------------------------
///
/// This essentially follows ``stateful``, the type class of a mutable piece of
/// state defined using the modifies-theory of Low*v2 and equipped with the
/// right lemmas to enable usage by clients. See
/// hacl-star/code/streaming/Hacl.Streaming.Interface.fst for more context.

val footprint: (#a: Type) -> (h: HS.mem) -> (l: t a) -> (n: list a) -> Ghost B.loc
  (requires (well_formed h l n))
  (ensures (fun refs -> True))
  (decreases n)

let rec footprint #a h l n =
  if B.g_is_null l
  then B.loc_none
  else
    let {next = next} = B.get h l 0 in
    let refs = footprint h next (G.hide (L.tl n)) in
    B.loc_union (B.loc_addr_of_buffer l) refs

/// Departing from LinkedList4 here. I prefer to bolt these into the invariant
/// rather than requiring on some wizard lemmas from LowStar.Monotonic.Buffer to
/// deduce these.
val cells_pairwise_disjoint: #a:Type -> h:HS.mem -> l:t a -> n:list a -> Ghost Type0
  (requires well_formed h l n)
  (ensures fun _ -> True)
  (decreases n)

let rec cells_pairwise_disjoint #_ h l n =
  if B.g_is_null l then
    True
  else
    let next = (B.deref h l).next in
    B.loc_disjoint (B.loc_addr_of_buffer l) (footprint h next (L.tl n)) /\
    cells_pairwise_disjoint h next (L.tl n)

val cells_live_freeable: #a:Type -> h:HS.mem -> l:t a -> n:list a -> Ghost Type0
  (requires well_formed h l n)
  (ensures fun _ -> True)
  (decreases n)

let rec cells_live_freeable #_ h l n =
  if B.g_is_null l then
    True
  else
    let next = (B.deref h l).next in
    B.live h l /\ B.freeable l /\
    cells_live_freeable h next (L.tl n)

val invariant: #a:Type -> h:HS.mem -> l: t a -> n:list a -> Ghost Type0
  (requires well_formed h l n)
  (ensures fun _ -> True)
  (decreases n)
let invariant #a h l n =
  cells_live_freeable h l n /\ cells_pairwise_disjoint h l n

/// Normally this would be automatic and writing a custom lemma for that stuff
/// would be needed only when writing an fsti, however, as stated earlier,
/// recursion makes everything more difficult and this absolutely needs to be in
/// scope otherwise the modifies-clause theory cannot deduce disjointness of
/// fresh allocations w.r.t. the footprint.
let rec invariant_loc_in_footprint (#a: Type) (h: HS.mem) (l: t a) (n: list a): Lemma
  (requires well_formed h l n)
  (ensures B.loc_in (footprint h l n) h)
  (decreases n)
  [ SMTPat (invariant h l n) ]
=
  if B.g_is_null l then
    ()
  else
    let next = (B.deref h l).next in
    invariant_loc_in_footprint h next (L.tl n)

/// Another absolutely essential lemma, for which interestingly the pattern
/// "invariant h1 l n" does not work, but well_formed does... I guess that's
/// alright.
let rec frame (#a: Type) (l: t a) (n: list a) (r: B.loc) (h0 h1: HS.mem): Lemma
  (requires (
    well_formed h0 l n /\
    invariant h0 l n /\
    B.loc_disjoint r (footprint h0 l n) /\
    B.modifies r h0 h1
  ))
  (ensures (
    well_formed h1 l n /\
    footprint h1 l n == footprint h0 l n /\
    cells h1 l n == cells h0 l n /\
    invariant h1 l n
  ))
  (decreases n)
  [ SMTPat (well_formed h1 l n); SMTPat (B.modifies r h0 h1) ]
=
  if B.g_is_null l then
    ()
  else
    frame (B.deref h0 l).next (L.tl n) r h0 h1

/// Lemmas for working with linked lists
/// ------------------------------------
///
/// Since it's a recursive data structure, a lot of the automated reasoning from
/// LowStar.Buffer doesn't work since it requires inductions. Some helpful
/// properties are therefore proved here.

let rec length_functional #a (h: HS.mem) (c: t a) (l1 l2: list a):
  Lemma
    (requires (well_formed h c l1 /\ well_formed h c l2))
    (ensures (l1 == l2))
    (decreases (G.reveal l1))
    [ SMTPat (well_formed h c l1); SMTPat (well_formed h c l2) ] =
  if B.g_is_null c
  then ()
  else
    let { next=next } = B.get h c 0 in
    length_functional h next (G.hide (L.tl l1)) (G.hide (L.tl l2))

/// The footprint is based on loc_addr_of_buffer so that we can write a free
/// operation that operates on the footprint. However, this invalidates most of
/// the helper lemmas for disjointness that were present in the previous
/// iteration of this module, named LinkedList4.fst. It's ok, we bake
/// disjointness directly onto the invariant and it works just as well.

/// Connection between ``cells`` and ``v``
/// --------------------------------------

/// Redefining some helpers.
#push-options "--ifuel 1"
let rec gmap #a #b (f: a -> GTot b) (xs: list a): GTot (list b) =
  match xs with
  | [] -> []
  | x :: xs -> f x :: gmap f xs

/// "As we all know", right folds are the easiest to work with because they
/// follow the natural structure of recursion (left-folds are evil).
let rec gfold_right #a #b (f: b -> a -> GTot b) (xs: list a) (acc: b): Ghost b
  (requires True)
  (ensures fun _ -> True)
  (decreases xs)
val gfold_right (#a #b: _) (f: (b -> a -> GTot b)) (xs: list a) (acc: b)
    : Ghost b (requires True) (ensures fun _ -> True) (decreases xs)
f: (_: b -> _: a -> Prims.GTot b) -> xs: Prims.list a -> acc: b -> Prims.Ghost b