val find (#t_k: eqtype) (#t_v: Type0) (ll: t t_k t_v) (k: t_k):
  Stack (option t_v)
    (requires fun h0 ->
      invariant h0 ll)
    (ensures fun h0 x h1 ->
      let m: map t_k t_v = v h0 ll in
      h0 == h1 /\
      x == M.sel m k)
let find #_ #_ ll k =
  find_ !*ll.LL2.ptr !*ll.LL2.v k
val find (#t_k: eqtype) (#t_v: Type0) (ll: t t_k t_v) (k: t_k):
  Stack (option t_v)
    (requires fun h0 ->
      invariant h0 ll)
    (ensures fun h0 x h1 ->
      let m: map t_k t_v = v h0 ll in
      h0 == h1 /\
      x == M.sel m k)
let find #_ #_ ll k =
find_ !*ll.LL2.ptr !*ll.LL2.v k
LowStar.Lib.AssocList.fst.checked
prims.fst.checked LowStar.Lib.LinkedList2.fst.checked LowStar.Lib.LinkedList.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
LowStar.Lib.AssocList.fst
Prims.eqtype LowStar.Lib.AssocList.t LowStar.Lib.AssocList.find_ FStar.Pervasives.Native.option FStar.Ghost.erased Prims.list FStar.Pervasives.Native.tuple2 LowStar.BufferOps.op_Bang_Star LowStar.Buffer.trivial_preorder LowStar.Lib.LinkedList2.__proj__Mkt__item__v LowStar.Lib.LinkedList.t LowStar.Lib.LinkedList2.__proj__Mkt__item__ptr
module LowStar.Lib.AssocList

/// A Low*, stateful associative list that exposes a map-like interface.

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

module M = FStar.Map
module LL2 = LowStar.Lib.LinkedList2
module LL1 = LowStar.Lib.LinkedList

open FStar.HyperStack.ST
open LowStar.BufferOps

#set-options "--fuel 0 --ifuel 0"

/// Types, invariants, footprint
/// ----------------------------

/// We prefer the packed representation that is in general easier to use and will
/// look at the underlying predicate-based representation from LL1 only when
/// strictly needed.
let t k v =
  LL2.t (k & v)

/// Functions suffixed with an underscore operate on either LL1 or raw lists
/// while those without operate on LL2.
val v_: #t_k:eqtype -> #t_v:Type0 -> l:list (t_k & t_v) -> Tot (map t_k t_v)
let v_ #_ #t_v l =
  List.Tot.fold_right (fun (k, v) m -> M.upd m k (Some v)) l (M.const (None #t_v))

/// Reflecting a stateful, imperative map as a functional one in a given heap.
let v #_ #_ h ll =
  let l = LL2.v h ll in
  v_ l

let invariant #_ #_ h ll =
  LL2.invariant h ll

// No longer needed in the fsti.
val footprint: #t_k:eqtype -> #t_v:Type0 -> h:HS.mem -> ll:t t_k t_v -> Ghost B.loc
  (requires invariant h ll)
  (ensures fun _ -> True)

let footprint #_ #_ h ll =
  LL2.footprint h ll

let region_of #_ #_ ll =
  LL2.region_of ll

let frame #_ #_ ll _ h0 _ =
  LL2.footprint_in_r h0 ll

val footprint_in_r: #t_k:eqtype -> #t_v:Type0 -> h0:HS.mem -> ll:t t_k t_v -> Lemma
  (requires
    invariant h0 ll)
  (ensures
    B.(loc_includes (region_of ll) (footprint h0 ll)))
  [ SMTPat (footprint h0 ll) ]

let footprint_in_r #_ #_ h0 ll =
  LL2.footprint_in_r h0 ll

#push-options "--fuel 1"
let create_in #_ #_ r =
  LL2.create_in r
#pop-options

/// Find
/// ----

/// Proper recursion can only be done over the LL1.t type (unpacked representation).
val find_ (#t_k: eqtype) (#t_v: Type0) (hd: LL1.t (t_k & t_v)) (l: G.erased (list (t_k & t_v))) (k: t_k):
  Stack (option t_v)
    (requires fun h0 ->
      LL1.well_formed h0 hd l /\
      LL1.invariant h0 hd l)
    (ensures fun h0 x h1 ->
      let m: map t_k t_v = v_ l in
      h0 == h1 /\
      x == M.sel m k)

#push-options "--fuel 1 --ifuel 1"
let rec find_ #_ #_ hd l k =
  if B.is_null hd then
    None
  else
    let cell = !* hd in
    if fst cell.LL1.data = k then
      Some (snd cell.LL1.data)
    else
      find_ cell.LL1.next (List.Tot.tl l) k
#pop-options
val find (#t_k: eqtype) (#t_v: Type0) (ll: t t_k t_v) (k: t_k):
  Stack (option t_v)
    (requires fun h0 ->
      invariant h0 ll)
    (ensures fun h0 x h1 ->
      let m: map t_k t_v = v h0 ll in
      h0 == h1 /\
      x == M.sel m k)
ll: LowStar.Lib.AssocList.t t_k t_v -> k: t_k
  -> FStar.HyperStack.ST.Stack (FStar.Pervasives.Native.option t_v)