val create_in: #t_k:eqtype -> #t_v:Type -> r:HS.rid -> ST (t t_k t_v)
  (requires fun h0 ->
    ST.is_eternal_region r)
  (ensures fun h0 ll h1 ->
    invariant h1 ll /\
    B.(modifies loc_none h0 h1) /\
    v h1 ll == M.const None /\
    region_of ll == B.(loc_all_regions_from false r))
let create_in #_ #_ r =
  LL2.create_in r
val create_in: #t_k:eqtype -> #t_v:Type -> r:HS.rid -> ST (t t_k t_v)
  (requires fun h0 ->
    ST.is_eternal_region r)
  (ensures fun h0 ll h1 ->
    invariant h1 ll /\
    B.(modifies loc_none h0 h1) /\
    v h1 ll == M.const None /\
    region_of ll == B.(loc_all_regions_from false r))
let create_in #_ #_ r =
LL2.create_in r
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 FStar.Monotonic.HyperHeap.rid LowStar.Lib.LinkedList2.create_in FStar.Pervasives.Native.tuple2 LowStar.Lib.LinkedList2.t LowStar.Lib.AssocList.t
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"
val create_in: #t_k:eqtype -> #t_v:Type -> r:HS.rid -> ST (t t_k t_v)
  (requires fun h0 ->
    ST.is_eternal_region r)
  (ensures fun h0 ll h1 ->
    invariant h1 ll /\
    B.(modifies loc_none h0 h1) /\
    v h1 ll == M.const None /\
    region_of ll == B.(loc_all_regions_from false r))
r: FStar.Monotonic.HyperHeap.rid -> FStar.HyperStack.ST.ST (LowStar.Lib.AssocList.t t_k t_v)