val extend
    (#a:eqtype)
    (#b:a -> Type)
    (#inv:DM.t a (opt b) -> Type)
    (#r:HST.erid)
    (t:t r a b inv)
    (x:a)
    (y:b x)
  : Stack unit
       (requires (fun h ->
         ~(defined t x h) /\
         inv (repr (upd (HS.sel h t) x y))))
       (ensures (fun h0 u h1 ->
         let cur = HS.sel h0 t in
         HS.contains h1 t /\
         HS.modifies (Set.singleton r) h0 h1 /\
         HS.modifies_ref r (Set.singleton (HS.as_addr t)) h0 h1 /\
         HS.sel h1 t == upd cur x y /\
         witnessed (contains t x y)))
let extend #a #b #inv #r t x y =
    recall t;
    let cur = !t in
    t := upd cur x y;
    mr_witness t (contains t x y)
val extend
    (#a:eqtype)
    (#b:a -> Type)
    (#inv:DM.t a (opt b) -> Type)
    (#r:HST.erid)
    (t:t r a b inv)
    (x:a)
    (y:b x)
  : Stack unit
       (requires (fun h ->
         ~(defined t x h) /\
         inv (repr (upd (HS.sel h t) x y))))
       (ensures (fun h0 u h1 ->
         let cur = HS.sel h0 t in
         HS.contains h1 t /\
         HS.modifies (Set.singleton r) h0 h1 /\
         HS.modifies_ref r (Set.singleton (HS.as_addr t)) h0 h1 /\
         HS.sel h1 t == upd cur x y /\
         witnessed (contains t x y)))
let extend #a #b #inv #r t x y =
recall t;
let cur = !t in
t := upd cur x y;
mr_witness t (contains t x y)
FStar.Monotonic.DependentMap.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.DependentMap.fsti.checked
FStar.Monotonic.DependentMap.fst
Prims.eqtype FStar.DependentMap.t FStar.Monotonic.DependentMap.opt FStar.HyperStack.ST.erid FStar.Monotonic.DependentMap.t FStar.HyperStack.ST.mr_witness FStar.Monotonic.DependentMap.imap FStar.Monotonic.DependentMap.grows FStar.Monotonic.DependentMap.contains Prims.unit FStar.HyperStack.ST.op_Colon_Equals FStar.Monotonic.DependentMap.upd FStar.HyperStack.ST.op_Bang FStar.HyperStack.ST.recall
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Monotonic.DependentMap
(** A library for mutable partial, dependent maps,
    that grow monotonically,
    while subject to an invariant on the entire map *)
open FStar.HyperStack.ST
module HS = FStar.HyperStack
module DM = FStar.DependentMap

/// `map a b`: Represent the partial map as a list of pairs of points
let map a b = list (x:a & b x)

/// `repr r`: Converts the list of pairs into a DM.t
let rec repr (#a:eqtype) (#b:a -> Type) (r:map a b)
    : GTot (partial_dependent_map a b)
    = match r with
      | [] -> empty_partial_dependent_map
      | (|x, y|)::tl -> DM.upd (repr tl) x (Some y)

/// Three basic operations on map: empty, sel upd
let empty #a #b = []

let rec sel #a #b r x =
    match r with
    | [] -> None
    | (|x', y|)::tl ->
      if x = x' then Some y else sel tl x

let upd #a #b r x v = (|x, v|)::r

////////////////////////////////////////////////////////////////////////////////

/// `grows'` and `grows`: a preorder of invariant-respecting maps
///    - Needs to be introduced in 2 steps because of an F* limitation
let grows' (#a:eqtype) (#b:a -> Type) (#inv:(partial_dependent_map a b -> Type))
           (m1:imap a b inv) (m2:imap a b inv) =
    forall x.{:pattern (Some? (sel m1 x))}
           Some? (sel m1 x) ==>
              Some? (sel m2 x) /\
              Some?.v (sel m1 x) == Some?.v (sel m2 x)
let grows #a #b #inv = grows' #a #b #inv

let contains_stable #a #b #inv #r t x y = ()
let defined_stable #a #b #inv #r t x = ()
////////////////////////////////////////////////////////////////////////////////

//The main stateful interface is minimal and straigtforward
let alloc #a #b #inv #r _ = ralloc r []
val extend
    (#a:eqtype)
    (#b:a -> Type)
    (#inv:DM.t a (opt b) -> Type)
    (#r:HST.erid)
    (t:t r a b inv)
    (x:a)
    (y:b x)
  : Stack unit
       (requires (fun h ->
         ~(defined t x h) /\
         inv (repr (upd (HS.sel h t) x y))))
       (ensures (fun h0 u h1 ->
         let cur = HS.sel h0 t in
         HS.contains h1 t /\
         HS.modifies (Set.singleton r) h0 h1 /\
         HS.modifies_ref r (Set.singleton (HS.as_addr t)) h0 h1 /\
         HS.sel h1 t == upd cur x y /\
         witnessed (contains t x y)))
t: FStar.Monotonic.DependentMap.t r a b inv -> x: a -> y: b x
  -> FStar.HyperStack.ST.Stack Prims.unit