val join_commutative (m0 m1:mem)
  : Lemma
    (requires
      disjoint m0 m1)
    (ensures
      (disjoint m0 m1 /\
       disjoint m1 m0 /\
       join m0 m1 == join m1 m0))
let join_commutative m0 m1 =
  H.join_commutative m0.heap m1.heap
val join_commutative (m0 m1:mem)
  : Lemma
    (requires
      disjoint m0 m1)
    (ensures
      (disjoint m0 m1 /\
       disjoint m1 m0 /\
       join m0 m1 == join m1 m0))
let join_commutative m0 m1 =
H.join_commutative m0.heap m1.heap
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.mem Steel.Heap.join_commutative Steel.Memory.__proj__Mkmem__item__heap 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
}
val join_commutative (m0 m1:mem)
  : Lemma
    (requires
      disjoint m0 m1)
    (ensures
      (disjoint m0 m1 /\
       disjoint m1 m0 /\
       join m0 m1 == join m1 m0))
m0: Steel.Memory.mem -> m1: Steel.Memory.mem
  -> FStar.Pervasives.Lemma (requires Steel.Memory.disjoint m0 m1)
      (ensures
        Steel.Memory.disjoint m0 m1 /\ Steel.Memory.disjoint m1 m0 /\
        Steel.Memory.join m0 m1 == Steel.Memory.join m1 m0)