val affine_star (p q:slprop) (m:mem)
  : Lemma ((interp (p `star` q) m ==> interp p m /\ interp q m))
let affine_star (p q:slprop) (m:mem) =
  H.affine_star p q (heap_of_mem m)
val affine_star (p q:slprop) (m:mem)
  : Lemma ((interp (p `star` q) m ==> interp p m /\ interp q m))
let affine_star (p q: slprop) (m: mem) =
H.affine_star p q (heap_of_mem m)
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.slprop Steel.Memory.mem Steel.Heap.affine_star Steel.Memory.heap_of_mem Prims.unit
(*
   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
val affine_star (p q:slprop) (m:mem)
  : Lemma ((interp (p `star` q) m ==> interp p m /\ interp q m))
p: Steel.Memory.slprop -> q: Steel.Memory.slprop -> m: Steel.Memory.mem
  -> FStar.Pervasives.Lemma
    (ensures
      Steel.Memory.interp (Steel.Memory.star p q) m ==>
      Steel.Memory.interp p m /\ Steel.Memory.interp q m)