val 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)
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)
val 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)
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)
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
FStar.Monotonic.HyperStack.mem LowStar.Lib.LinkedList.t Prims.list LowStar.Monotonic.Buffer.g_is_null LowStar.Lib.LinkedList.cell LowStar.Buffer.trivial_preorder Prims.Nil LowStar.Buffer.pointer Prims.bool Prims.Cons LowStar.Lib.LinkedList.cells LowStar.Lib.LinkedList.__proj__Mkcell__item__next LowStar.Monotonic.Buffer.deref FStar.List.Tot.Base.tl LowStar.Lib.LinkedList.well_formed 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)
val 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)
h: FStar.Monotonic.HyperStack.mem -> c: LowStar.Lib.LinkedList.t a -> l: Prims.list a
  -> Prims.Ghost (Prims.list (LowStar.Buffer.pointer (LowStar.Lib.LinkedList.cell a)))