val lift_tot_action_nf (#a #e #fp #fp': _) ($f: tot_action_nf_except e fp a fp')
    : MstTotNF a e fp fp'
let lift_tot_action_nf #a #e #fp #fp' ($f:tot_action_nf_except e fp a fp')
  : MstTotNF a e fp fp'
  = let m0 = NMSTTotal.get () in
    let m0' : hmem_with_inv_except e fp = m0 in
    let r = f m0' in
    let (| x, m1 |) = r in
    let m1' : hmem_with_inv_except e (fp' x) = m1 in
    assert (is_frame_preserving f);
    assert (m1 == dsnd (f m0));
    frame_preserving_respects_preorder f m0;
    NMSTTotal.put #_ #(mem_evolves) m1;
    x
val lift_tot_action_nf (#a #e #fp #fp': _) ($f: tot_action_nf_except e fp a fp')
    : MstTotNF a e fp fp'
let lift_tot_action_nf #a #e #fp #fp' ($f: tot_action_nf_except e fp a fp') : MstTotNF a e fp fp' =
let m0 = NMSTTotal.get () in
let m0':hmem_with_inv_except e fp = m0 in
let r = f m0' in
let (| x , m1 |) = r in
let m1':hmem_with_inv_except e (fp' x) = m1 in
assert (is_frame_preserving f);
assert (m1 == dsnd (f m0));
frame_preserving_respects_preorder f m0;
NMSTTotal.put #_ #(mem_evolves) m1;
x
Steel.Memory.fst.checked
Steel.Preorder.fst.checked Steel.Heap.fsti.checked prims.fst.checked FStar.Witnessed.Core.fsti.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.NMSTTotal.fst.checked FStar.List.Tot.fst.checked FStar.IndefiniteDescription.fsti.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Steel.Memory.fst
Steel.Memory.inames Steel.Memory.slprop Steel.Memory.tot_action_nf_except Steel.Memory.hmem_with_inv_except Prims.unit FStar.NMSTTotal.put Steel.Memory.full_mem Steel.Memory.mem_evolves Steel.Memory.frame_preserving_respects_preorder Prims._assert Prims.eq2 Prims.l_or Prims.l_and Steel.Memory.inames_ok Steel.Memory.interp Steel.Memory.star Steel.Memory.locks_invariant Prims.__proj__Mkdtuple2__item___1 FStar.Pervasives.dsnd Steel.Memory.is_frame_preserving Prims.dtuple2 FStar.NMSTTotal.get
(*
   Copyright 2020 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 Steel.Memory
module F = FStar.FunctionalExtensionality
open FStar.FunctionalExtensionality
open FStar.PCM
module H = Steel.Heap

noeq
type lock_state : Type u#(a + 1) =
  | Invariant : inv:H.slprop u#a -> lock_state

let lock_store : Type u#(a+1) = list (lock_state u#a)

noeq
type mem : Type u#(a + 1) =
  {
    ctr: nat;
    heap: H.heap u#a;
    locks: lock_store u#a;
  }

let heap_of_mem (x:mem) : H.heap = x.heap

let mem_of_heap (h:H.heap) : mem = {
  ctr = 0;
  heap = h;
  locks = []
}

let mem_set_heap (m:mem) (h:H.heap) : mem = {
  ctr = m.ctr;
  heap = h;
  locks = m.locks;
}

let core_mem (m:mem) : mem = mem_of_heap (heap_of_mem m)

let core_mem_invol m = ()

let disjoint (m0 m1:mem u#h)
  : prop
  = m0.ctr == m1.ctr /\
    H.disjoint m0.heap m1.heap /\
    m0.locks == m1.locks

let disjoint_sym m0 m1 = ()

let join m0 m1 = {
  ctr = m0.ctr;
  heap = H.join m0.heap m1.heap;
  locks = m0.locks
}

let join_commutative m0 m1 =
  H.join_commutative m0.heap m1.heap

let disjoint_join m0 m1 m2 =
  H.disjoint_join m0.heap m1.heap m2.heap

let join_associative m0 m1 m2 =
  H.join_associative m0.heap m1.heap m2.heap

let slprop = H.slprop

let interp p m = H.interp p m.heap

let equiv p1 p2 = forall m. interp p1 m <==> interp p2 m

let slprop_extensionality p q =
  assert (forall m. interp p m <==> interp q m);
  let aux (h:H.heap)
    : Lemma (H.interp p h <==> H.interp q h)
            [SMTPat (H.interp p h)]
    = let m : mem = { ctr = 0; heap = h; locks = [] } in
      assert (interp p m <==> interp q m)
  in
  assert (forall h. H.interp p h <==> H.interp q h);
  Steel.Heap.slprop_extensionality p q

let reveal_equiv p1 p2 = ()

let core_ref = H.core_ref
let core_ref_null = H.core_ref_null
let core_ref_is_null r = H.core_ref_is_null r

let emp : slprop u#a = H.emp
let pure = H.pure
let pts_to = H.pts_to
let h_and = H.h_and
let h_or = H.h_or
let star = H.star
let wand = H.wand
let h_exists = H.h_exists
let h_forall = H.h_forall

////////////////////////////////////////////////////////////////////////////////
//properties of equiv
////////////////////////////////////////////////////////////////////////////////

let equiv_symmetric (p1 p2:slprop u#a) = H.equiv_symmetric p1 p2

#push-options "--warn_error -271"
let equiv_heap_iff_equiv (p1 p2:slprop u#a)
  : Lemma (ensures (H.equiv p1 p2 <==> equiv p1 p2))
          [SMTPat (equiv p1 p2)]
  = let aux_lr ()
      : Lemma
        (requires H.equiv p1 p2)
        (ensures equiv p1 p2)
        [SMTPat ()]
      = ()
    in
    let aux_rl_helper1 (h:H.heap)
      : Lemma
        (requires equiv p1 p2 /\ H.interp p1 h)
        (ensures H.interp p2 h)
        [SMTPat ()]
      = assert (interp p2 (mem_of_heap h))
    in
    let aux_rl_helper2 (h:H.heap)
      : Lemma
        (requires equiv p1 p2 /\ H.interp p2 h)
        (ensures H.interp p1 h)
        [SMTPat ()]
      = assert (interp p2 (mem_of_heap h))
    in
    let aux_rl ()
      : Lemma
        (requires equiv p1 p2)
        (ensures H.equiv p1 p2)
        [SMTPat ()]
      = () in
    ()

let equiv_heap_iff_equiv_forall ()
  : Lemma (ensures (forall p1 p2. H.equiv p1 p2 <==> equiv p1 p2))
  = let aux p1 p2
      : Lemma (ensures (H.equiv p1 p2 <==> equiv p1 p2))
              [SMTPat ()]
      = equiv_heap_iff_equiv p1 p2
    in
    ()
#pop-options

let equiv_extensional_on_star (p1 p2 p3:slprop u#a) =
  equiv_heap_iff_equiv_forall ();
  H.equiv_extensional_on_star p1 p2 p3

let emp_unit p = H.emp_unit p

let intro_emp m = H.intro_emp (heap_of_mem m)

let pure_equiv p q = H.pure_equiv p q
let pure_interp q m = H.pure_interp q (heap_of_mem m)
let pure_star_interp p q m = H.pure_star_interp p q (heap_of_mem m)

////////////////////////////////////////////////////////////////////////////////
//pts_to
////////////////////////////////////////////////////////////////////////////////

let pts_to_compatible #a #pcm x v0 v1 m
  = H.pts_to_compatible #a #pcm x v0 v1 (heap_of_mem m)
let pts_to_compatible_equiv #a #pcm x v0 v1
  = H.pts_to_compatible_equiv #a #pcm x v0 v1
let pts_to_not_null #a #pcm x v m
  = H.pts_to_not_null #a #pcm x v (heap_of_mem m)

////////////////////////////////////////////////////////////////////////////////
// star
////////////////////////////////////////////////////////////////////////////////

let intro_star p q mp mq =
  H.intro_star p q (heap_of_mem mp) (heap_of_mem mq)

let elim_star p q m =
  let h = heap_of_mem m in
  H.elim_star p q h;
  assert (exists hl hr. H.disjoint hl hr /\ H.join hl hr == h /\ H.interp p hl /\ H.interp q hr);
  let hl = FStar.IndefiniteDescription.indefinite_description_tot H.heap (fun hl ->
     exists hr. H.disjoint hl hr /\ H.join hl hr == h /\ H.interp p hl /\ H.interp q hr) in
  let hr = FStar.IndefiniteDescription.indefinite_description_tot H.heap (fun hr ->
     H.disjoint hl hr /\ H.join hl hr == h /\ H.interp p hl /\ H.interp q hr) in
  let ml = mem_set_heap m hl in
  let mr = mem_set_heap m hr in
  assert (disjoint ml mr);
  assert (m == join ml mr);
  assert (interp p ml);
  assert (interp q mr);
  ()

let interp_star
  (p q: slprop)
  (m: mem)
: Lemma
  (interp (p `star` q) m <==> (exists (mp: mem) (mq: mem) . disjoint mp mq /\ interp p mp /\ interp q mq /\ join mp mq == m))
= let left = interp (p `star` q) m in
  let right = exists (mp: mem) (mq: mem) . disjoint mp mq /\ interp p mp /\ interp q mq /\ join mp mq == m in
  let f ()
  : Lemma
    (requires left)
    (ensures right)
  =
    elim_star p q m
  in
  let g ()
  : Lemma
    (requires right)
    (ensures left)
  =
    Classical.exists_elim left #_ #(fun mp -> exists (mq: mem) . disjoint mp mq /\ interp p mp /\ interp q mq /\ join mp mq == m) () (fun mp ->
      Classical.exists_elim left #_ #(fun mq -> disjoint mp mq /\ interp p mp /\ interp q mq /\ join mp mq == m) () (fun mq ->
        intro_star p q mp mq
      )
    )
  in
  Classical.move_requires f ();
  Classical.move_requires g ()

let star_commutative (p1 p2:slprop) =
  H.star_commutative p1 p2

let star_associative (p1 p2 p3:slprop) =
  H.star_associative p1 p2 p3

let star_congruence (p1 p2 p3 p4:slprop) =
  equiv_heap_iff_equiv_forall ();
  H.star_congruence p1 p2 p3 p4

let affine_star (p q:slprop) (m:mem) =
  H.affine_star p q (heap_of_mem m)

////////////////////////////////////////////////////////////////////////////////
// Invariants on the lock store
////////////////////////////////////////////////////////////////////////////////

let iname = nat
module S = FStar.Set
module L = FStar.List.Tot
module W = FStar.Witnessed.Core

let rec lock_store_invariant (e:inames) (l:lock_store u#a) : slprop u#a =
  let current_addr = L.length l - 1 in
  match l with
  | [] -> emp
  | Invariant p :: tl ->
    if current_addr `S.mem` e then
      lock_store_invariant e tl
    else
      p `star` lock_store_invariant e tl

let lock_i (i:iname) (l:lock_store { i < L.length l }) =
  let ix = L.length l - i - 1 in
  L.index l ix

let iname_for_p (i:iname) (p:slprop) : W.s_predicate lock_store =
  fun l ->
    i < L.length l /\
    (lock_i i l).inv == p

let lock_store_evolves : FStar.Preorder.preorder lock_store =
  fun (l1 l2 : lock_store) ->
    L.length l2 >= L.length l1 /\
    (forall (i:nat{i < L.length l1}).
       (lock_i i l1).inv == (lock_i i l2).inv)

let inames_in (e:inames) (l:lock_store) : prop = forall i. Set.mem i e ==> i < L.length l

let inames_ok e m = inames_in e m.locks

let inames_ok_empty m = ()

let extend_lock_store (e:inames) (l:lock_store{e `inames_in` l}) (p:slprop)
  : i:iname &
    l':lock_store {
      lock_store_invariant e l' == p `star` lock_store_invariant e l /\
      iname_for_p i p l'
    }
  = (| L.length l, Invariant p :: l |)

let set_add (i:iname) (s:inames) = Set.union (Set.singleton i) s

let rec move_invariant (e:inames) (l:lock_store) (p:slprop)
                       (i:iname{iname_for_p i p l /\ ~(i `Set.mem` e)})
   : Lemma (H.equiv (lock_store_invariant e l)
                    (p `star` lock_store_invariant (set_add i e) l))
   = let rec aux (i:iname) (m:lock_store)
       : Lemma (requires i >= L.length m)
               (ensures (lock_store_invariant e m `H.equiv`  lock_store_invariant (set_add i e) m))
       = match m with
         | [] -> ()
         | Invariant p::tl ->
           aux i tl;
           H.star_congruence p (lock_store_invariant e tl) p (lock_store_invariant (set_add i e) tl)
     in
     let current_addr = L.length l - 1 in
     match l with
     | [] -> ()
     | Invariant q::tl ->
       if i = current_addr
       then begin
         assert (lock_store_invariant e l == p `star` lock_store_invariant e tl);
         aux i tl;
         H.star_congruence p (lock_store_invariant e tl) p (lock_store_invariant (set_add i e) tl);
         ()
       end
       else begin
         move_invariant e tl p i;
         assert (lock_store_invariant e tl `equiv`
                 (p `star` lock_store_invariant (set_add i e) tl));
         H.star_congruence q (lock_store_invariant e tl) q (p `star` lock_store_invariant (set_add i e) tl);
         if Set.mem current_addr e
         then ()
         else begin
           let r = lock_store_invariant (set_add i e) tl in
           assert (lock_store_invariant e l `equiv`
                   (q `star` (p `star` r)));
           H.star_associative q p r;
           H.star_commutative q p;
           H.star_congruence (q `star` p) r (p `star` q) r;
           H.star_associative p q r
         end
       end

let heap_ctr_valid (ctr:nat) (h:H.heap u#a) : prop =
    h `H.free_above_addr` ctr

let ctr_validity (ctr:nat) (h:H.heap) : slprop =
    H.pure (heap_ctr_valid ctr h)

let locks_invariant (e:inames) (m:mem u#a) : slprop u#a =
   lock_store_invariant e m.locks
   `star`
   ctr_validity m.ctr (heap_of_mem m)

let full_mem_pred (m:mem) = H.full_heap_pred (heap_of_mem m)

(***** Following lemmas are needed in Steel.Effect *****)

let core_mem_interp (hp:slprop u#a) (m:mem u#a) = ()

let interp_depends_only_on (hp:slprop u#a) = H.interp_depends_only_on hp

let a_mem_prop_as_a_heap_prop
  (sl: slprop u#a)
  (f: a_mem_prop sl)
: Tot (H.a_heap_prop u#a)
=
  let g (h: H.heap u#a) : Tot prop = interp sl (mem_of_heap h) /\ f (mem_of_heap h) in
  let phi0 (h0 h1: H.heap u#a) : Lemma
    (requires (g h0 /\ H.disjoint h0 h1))
    (ensures (g h0 /\ H.disjoint h0 h1 /\ g (H.join h0 h1)))
  = assert (mem_of_heap (H.join h0 h1) == mem_of_heap h0 `join` mem_of_heap h1);
    interp_depends_only_on sl
  in
  let phi1 (h0 h1: H.heap u#a) : Lemma
    (ensures ((g h0 /\ H.disjoint h0 h1) ==> g (H.join h0 h1)))
  =
    Classical.move_requires (phi0 h0) h1
  in
  Classical.forall_intro_2 phi1;
  g

let refine_slprop sl f = H.as_slprop (a_mem_prop_as_a_heap_prop sl f)

let interp_refine_slprop sl f m =
  assert ((interp sl m /\ f m) <==> interp sl (core_mem m) /\ f (core_mem m))

let dep_hprop
  (s: slprop)
  (f: (hmem s -> Tot slprop))
  (h: H.heap)
: Tot prop
= exists (h1: H.heap) . exists (h2: H.heap) . interp s (mem_of_heap h1) /\ H.disjoint h1 h2 /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ h == h1 `H.join` h2

let dep_hprop_is_affine0
  (s: slprop)
  (f: (hmem s -> Tot slprop))
  (h h': H.heap)
  (sq' : squash (dep_hprop s f h /\ H.disjoint h h'))
: Lemma
  (H.disjoint h h' /\ dep_hprop s f (H.join h h'))
=
  let p2 (h h1 h2: H.heap) : Tot prop =
    interp s (mem_of_heap h1) /\
    H.disjoint h1 h2 /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ h == h1 `H.join` h2
  in
  let p1 (h h1: H.heap) : Tot prop =
    (exists h2 . p2 h h1 h2)
  in
  let h1 =
    FStar.IndefiniteDescription.indefinite_description_ghost H.heap (p1 h)
  in
  let h2 =
    FStar.IndefiniteDescription.indefinite_description_ghost H.heap (p2 h h1)
  in
  H.disjoint_join h' h1 h2;
  assert (H.disjoint h2 h');
  let h2' = H.join h2 h' in
  H.join_commutative h2 h' ;
  assert (h2' == H.join h' h2);
  assert (H.disjoint h1 h2');
  assert (mem_of_heap h2' == mem_of_heap h2 `join` mem_of_heap h');
  interp_depends_only_on (f (mem_of_heap h1));
  assert (interp (f (mem_of_heap h1)) (mem_of_heap h2'));
  H.join_commutative h1 h2;
  H.join_associative h' h2 h1;
  H.join_commutative h' h;
  H.join_commutative h2' h1;
  assert (H.join h h' == h1 `H.join` h2')

let impl_intro_gen (#p: Type0) (#q: Type0) ($prf: (squash p -> Lemma (q )))
    : Lemma (p ==> q)
= Classical.impl_intro_gen #p #(fun _ -> q) prf

let dep_hprop_is_affine1
  (s: slprop)
  (f: (hmem s -> Tot slprop))
  (h0 h1: H.heap)
: Lemma
  ((dep_hprop s f h0 /\ H.disjoint h0 h1) ==> (H.disjoint h0 h1 /\ dep_hprop s f (H.join h0 h1)))
= impl_intro_gen (dep_hprop_is_affine0 s f h0 h1)

let dep_hprop_is_affine
  (s: slprop)
  (f: (hmem s -> Tot slprop))
: Lemma
  (H.heap_prop_is_affine (dep_hprop s f))
= Classical.forall_intro_2 (dep_hprop_is_affine1 s f)

let sdep
  (s: slprop)
  (f: (hmem s -> Tot slprop))
: Tot slprop
=
  dep_hprop_is_affine s f;
  H.as_slprop (dep_hprop s f)

let interp_sdep
  (s: slprop)
  (f: (hmem s -> Tot slprop))
  (m: mem)
: Lemma
  (requires (dep_slprop_is_affine s f))
  (ensures (
    interp (sdep s f) m <==> (exists m1 m2 . interp s m1 /\ interp (f m1) m2 /\ disjoint m1 m2 /\ join m1 m2 == m)
  ))
=
  dep_hprop_is_affine s f;
  assert (forall m1 m2 . (interp s m1 /\ interp (f m1) m2 /\ disjoint m1 m2 /\ join m1 m2 == m) ==> (
    interp s (mem_of_heap m1.heap) /\ interp (f (mem_of_heap m1.heap)) (mem_of_heap m2.heap) /\
    H.disjoint m1.heap m2.heap /\
    H.join m1.heap m2.heap == m.heap
  ));
  interp_depends_only_on s;
  Classical.forall_intro (fun m -> interp_depends_only_on (f m));
  assert (forall h1 h2 . (interp s (mem_of_heap h1) /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ H.disjoint h1 h2 /\ H.join h1 h2 == m.heap) ==> (
    core_mem (mem_of_heap h1) == core_mem (mem_set_heap m h1) /\
    interp s (core_mem (mem_of_heap h1)) /\
    interp s (mem_set_heap m h1) /\
    core_mem (mem_of_heap h1) == core_mem (mem_set_heap m h1) /\
    f (mem_set_heap m h1) `equiv` f (mem_of_heap h1) /\
    interp (f (mem_set_heap m h1)) (mem_of_heap h2) /\
    interp (f (mem_set_heap m h1)) (mem_set_heap m h2) /\
    disjoint (mem_set_heap m h1) (mem_set_heap m h2) /\
    join (mem_set_heap m h1) (mem_set_heap m h2) == m
  ));
  ()

let h_exists_cong (#a:Type) (p q : a -> slprop)
    : Lemma
      (requires (forall x. p x `equiv` q x))
      (ensures (h_exists p `equiv` h_exists q))
    = equiv_heap_iff_equiv_forall ();
      H.h_exists_cong p q

let intro_h_exists #a x p m = H.intro_h_exists x p (heap_of_mem m)

let elim_h_exists (#a:_) (p:a -> slprop) (m:mem) = H.elim_h_exists p (heap_of_mem m)

////////////////////////////////////////////////////////////////////////////////
// Preorders and effects
////////////////////////////////////////////////////////////////////////////////
module PP = Steel.Preorder

let mem_evolves =
  fun (m0 m1:full_mem) ->
    H.heap_evolves (heap_of_mem m0) (heap_of_mem m1) /\
    m0.ctr <= m1.ctr /\
    lock_store_evolves m0.locks m1.locks

(** See [Steel.Heap.is_frame_preserving]. We add in [lock_invariants] now *)
let preserves_frame (e:inames) (pre post:slprop) (m0 m1:mem) =
  forall (frame:slprop).
    interp ((pre `star` frame) `star` locks_invariant e m0) m0 ==>
    (interp ((post `star` frame) `star` locks_invariant e m1) m1 /\
     (forall (f_frame:mprop frame). f_frame (core_mem m0) == f_frame (core_mem m1)))

(**
  This is a version of MstTot with frame quantified, as part of preserves_frame
*)
effect MstTotNF (a:Type u#a) (except:inames) (expects:slprop u#1) (provides: a -> slprop u#1) =
  NMSTTotal.NMSTATETOT a (full_mem u#1) mem_evolves
    (requires fun m0 ->
        inames_ok except m0 /\
        interp (expects `star` locks_invariant except m0) m0)
    (ensures fun m0 x m1 ->
        inames_ok except m1 /\
        interp (provides x `star` locks_invariant except m1) m1 /\
        preserves_frame except expects (provides x) m0 m1)

////////////////////////////////////////////////////////////////////////////////
// Lifting heap actions
////////////////////////////////////////////////////////////////////////////////

(**
  Heap actions come in two equivalent flavors:
  - one that take an explicit frame as argument (action_with_frame)
  - and one that quantify over all the frame

  We therefore define two lift routes:
  - a direct route for those with explicit frame
  - via MstTotNF for the rest
*)

let tot_pre_action_nf_except (e:inames) (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) =
  hmem_with_inv_except e fp ->
  (x:a & hmem_with_inv_except e (fp' x))

let tot_pre_action_nf = tot_pre_action_nf_except S.empty

let ac_reasoning_for_m_frame_preserving
    (p q r:slprop u#a) (m:mem u#a)
  : Lemma
    (requires interp ((p `star` q) `star` r) m)
    (ensures interp (p `star` r) m)
  = calc (equiv) {
    (p `star` q) `star` r;
       (equiv) { star_commutative p q;
                 equiv_extensional_on_star (p `star` q) (q `star` p) r }
    (q `star` p) `star` r;
       (equiv) { star_associative q p r }
    q `star` (p `star` r);
    };
    assert (interp (q `star` (p `star` r)) m);
    affine_star q (p `star` r) m

let is_frame_preserving
  (#e:inames)
  (#a:Type u#b)
  (#fp:slprop u#a)
  (#fp':a -> slprop u#a)
  (f:tot_pre_action_nf_except e fp a fp') =
  forall (frame:slprop u#a) (m0:hmem_with_inv_except e (fp `star` frame)).
    (ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0;
     let (| x, m1 |) = f m0 in
     interp ((fp' x `star` frame) `star` locks_invariant e m1) m1 /\
     mem_evolves m0 m1 /\
     (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1)))

let tot_action_nf_except (e:inames) (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) =
  f:tot_pre_action_nf_except e fp a fp'{ is_frame_preserving f }

let tot_action_nf = tot_action_nf_except S.empty

let linv e (m:mem) = locks_invariant e m

let hheap_of_hmem #fp #e (m:hmem_with_inv_except e fp)
  : h:H.hheap (fp `star` linv e m) { h `H.free_above_addr` m.ctr}
  = let h = heap_of_mem m in
    H.pure_interp (heap_ctr_valid m.ctr (heap_of_mem m)) h;
    h

let hmem_of_hheap #e (#fp0 #fp1:slprop) (m:hmem_with_inv_except e fp0)
                  (h:H.full_hheap (fp1 `star` linv e m) {
                       h `Heap.free_above_addr` m.ctr
                  })
    : m1:hmem_with_inv_except e fp1{linv e m `equiv` linv e m1}
    = let m1 : mem = { m with heap = h } in
      assert (interp (fp1 `star` linv e m) m1);
      star_commutative fp1 (linv e m);
      assert (interp (linv e m `star` fp1) m1);
      assert (linv e m1 ==  (lock_store_invariant e m1.locks)
                            `star` ctr_validity m1.ctr (heap_of_mem m1));
      assert (linv e m ==  (lock_store_invariant e m1.locks)
                             `star` ctr_validity m1.ctr (heap_of_mem m));
      H.pure_interp (heap_ctr_valid m1.ctr (heap_of_mem m))
                    (heap_of_mem m);
      assert (heap_ctr_valid m1.ctr (heap_of_mem m) <==>
              heap_ctr_valid m1.ctr (heap_of_mem m1));
      H.pure_equiv (heap_ctr_valid m1.ctr (heap_of_mem m))
                   (heap_ctr_valid m1.ctr (heap_of_mem m1));
      H.star_congruence (lock_store_invariant e m1.locks)
                        (ctr_validity m1.ctr (heap_of_mem m1))
                        (lock_store_invariant e m1.locks)
                        (ctr_validity m1.ctr (heap_of_mem m));
      assert (linv e m `equiv` linv e m1);
      let _ = equiv_extensional_on_star (linv e m) (linv e m1) fp1 in
      assert ((linv e m `star` fp1) `equiv` (linv e m1 `star` fp1));
      assert (interp (linv e m1 `star` fp1) m1);
      star_commutative (linv e m1) fp1;
      assert (interp (fp1 `star` linv e m1) m1);
      m1

let with_inv_except (m:mem) e (fp:slprop) = interp (fp `star` locks_invariant e m) m

#push-options "--warn_error -271"
let as_hprop (frame:slprop) (mp:mprop frame)
    : hp:H.hprop frame{forall m. mp (core_mem m) == hp (heap_of_mem m)}
    = let f = fun h -> mp (mem_of_heap h) in
      assert (forall m. mp (core_mem m) == f (heap_of_mem m));
      let aux (m0:H.hheap frame) (m1:H.heap{H.disjoint m0 m1})
        : Lemma
          (ensures (mem_of_heap (H.join m0 m1) == join (mem_of_heap m0) (mem_of_heap m1)))
          [SMTPat ()]
        = ()
      in
      f

let mprop_preservation_of_hprop_preservation
       (p:slprop) (m0 m1:mem)
    : Lemma
      (requires (forall (hp:H.hprop p). hp (heap_of_mem m0) == hp (heap_of_mem m1)))
      (ensures (forall (mp:mprop p). mp (core_mem m0) == mp (core_mem m1)))
    = let aux (mp:mprop p)
        : Lemma (mp (core_mem m0) == mp (core_mem m1))
          [SMTPat()]
        = assert (as_hprop p mp (heap_of_mem m0) == as_hprop p mp (heap_of_mem m1))
      in
      ()

let lift_heap_action (#fp:slprop) (#a:Type) (#fp':a -> slprop)
                     (e:inames)
                     ($f:H.action fp a fp')
  : tot_action_nf_except e fp a fp'
  = let g : tot_pre_action_nf_except e fp a fp' = fun m ->
        let h0 = hheap_of_hmem m in
        let (| x, h' |) = f h0 in
        (| x, hmem_of_hheap m h' |)
    in
    let aux (frame:slprop) (m0:hmem_with_inv_except e (fp `star` frame))
      : Lemma
        (ensures
          (ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0;
           let (| x, m1 |) = g m0 in
           interp ((fp' x `star` frame) `star` locks_invariant e m1) m1 /\
           mem_evolves m0 m1 /\
           (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1))))
        [SMTPat ()]
      = ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0;
        let (| x, m1 |) = g m0 in
        let h0 = hheap_of_hmem m0 in
        let (| x', h1 |) = f h0 in
        H.action_framing f (linv e m0) h0;
        assert (x == x');
        star_associative fp frame (linv e m0);
        H.action_framing f (frame `star` linv e m0) h0;
        assert (H.interp ((fp' x) `star` (frame `star` linv e m0)) h1);
        star_associative (fp' x) frame (linv e m0);
        assert (H.interp ((fp' x `star` frame) `star` linv e m0) h1);
        let h1' : H.hheap ((fp' x `star` frame) `star` linv e m0) = h1 in
        assert (m1 == hmem_of_hheap m0 h1');
        assert (with_inv_except m1 e (fp' x `star` frame));
        assert (forall (hp:H.hprop frame). hp h0 == hp h1);
        mprop_preservation_of_hprop_preservation frame m0 m1;
        ()
    in
    assert (is_frame_preserving g);
    g

let frame_preserving_respects_preorder #a #e #fp #fp' ($f:tot_action_nf_except e fp a fp') (m0:hmem_with_inv_except e fp)
  : Lemma (let (| x, m1 |) = f m0 in
           mem_evolves m0 m1)
  = let aux (frame:slprop) (m0:hmem_with_inv_except e (fp `star` frame))
        : Lemma
          (ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0;
            let (| x, m1 |) = f m0 in
            interp ((fp' x `star` frame) `star` locks_invariant e m1) m1 /\
            mem_evolves m0 m1)
        = ()
    in
    H.emp_unit fp;
    assert (interp (fp `star` linv e m0) m0);
    H.star_congruence (fp `star` emp) (linv e m0) fp (linv e m0);
    assert (interp ((fp `star` emp) `star` linv e m0) m0);
    aux emp m0

let lift_tot_action_nf #a #e #fp #fp' ($f:tot_action_nf_except e fp a fp')
val lift_tot_action_nf (#a #e #fp #fp': _) ($f: tot_action_nf_except e fp a fp')
    : MstTotNF a e fp fp'
$f: Steel.Memory.tot_action_nf_except e fp a fp' -> Steel.Memory.MstTotNF a