val disjoint (m0 m1:mem u#h) : prop
let disjoint (m0 m1:mem u#h)
  : prop
  = m0.ctr == m1.ctr /\
    H.disjoint m0.heap m1.heap /\
    m0.locks == m1.locks
val disjoint (m0 m1:mem u#h) : prop
let disjoint (m0 m1: mem u#h) : prop =
m0.ctr == m1.ctr /\ H.disjoint m0.heap m1.heap /\ m0.locks == m1.locks
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 Prims.l_and Prims.eq2 Prims.nat Steel.Memory.__proj__Mkmem__item__ctr Steel.Heap.disjoint Steel.Memory.__proj__Mkmem__item__heap Steel.Memory.lock_store Steel.Memory.__proj__Mkmem__item__locks Prims.prop
(*
   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)
val disjoint (m0 m1:mem u#h) : prop
m0: Steel.Memory.mem -> m1: Steel.Memory.mem -> Prims.prop