val disjoint_cells_sym (c0 c1: cell u#h)
    : Lemma (requires disjoint_cells c0 c1) (ensures disjoint_cells c1 c0)
let disjoint_cells_sym (c0 c1:cell u#h)
  : Lemma (requires disjoint_cells c0 c1)
          (ensures disjoint_cells c1 c0)
  = let Ref t0 p0 f0 v0 = c0 in
    let Ref t1 p1 f0 v1 = c1 in
    p0.comm v0 v1;
    ()
val disjoint_cells_sym (c0 c1: cell u#h)
    : Lemma (requires disjoint_cells c0 c1) (ensures disjoint_cells c1 c0)
let disjoint_cells_sym (c0 c1: cell u#h)
    : Lemma (requires disjoint_cells c0 c1) (ensures disjoint_cells c1 c0) =
let Ref t0 p0 f0 v0 = c0 in
let Ref t1 p1 f0 v1 = c1 in
p0.comm v0 v1;
()
Steel.Heap.fst.checked
Steel.Preorder.fst.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.WellFounded.fst.checked FStar.PropositionalExtensionality.fst.checked FStar.Preorder.fst.checked FStar.PredicateExtensionality.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.IndefiniteDescription.fsti.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Steel.Heap.fst
Steel.Heap.cell FStar.PCM.pcm Steel.FractionalPermission.perm Prims.b2t Steel.FractionalPermission.lesser_equal_perm Steel.FractionalPermission.full_perm Prims.l_imp Prims.eq2 FStar.PCM.__proj__Mkpcm__item__refine Prims.unit FStar.PCM.__proj__Mkpcm__item__comm Steel.Heap.disjoint_cells Prims.squash Prims.Nil FStar.Pervasives.pattern
(*
   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.Heap
module F = FStar.FunctionalExtensionality
open FStar.FunctionalExtensionality
open FStar.PCM
module Frac = Steel.FractionalPermission

#set-options "--fuel 1 --ifuel 1"

// In the future, we may have other cases of cells
// for arrays and structs
noeq
type cell : Type u#(a + 1) =
  | Ref : a:Type u#a ->
          p:pcm a ->
          frac:Frac.perm{ frac `Frac.lesser_equal_perm` Frac.full_perm } ->
          v:a { frac == Frac.full_perm ==> p.refine v } ->
          cell

let addr = nat

/// This is just the core of a memory, about which one can write
/// assertions. At one level above, we'll encapsulate this memory
/// with a freshness counter, a lock store etc.
let heap : Type u#(a + 1) = addr ^-> option (cell u#a)

let empty_heap : heap = F.on _ (fun _ -> None)

let contains_addr (m:heap) (a:addr)
  : bool
  = Some? (m a)

let select_addr (m:heap) (a:addr{contains_addr m a})
  : cell
  = Some?.v (m a)

let update_addr' (m:heap) (a:addr) (c:option cell)
  : heap
  = F.on _ (fun a' -> if a = a' then c else m a')

let update_addr (m:heap) (a:addr) (c:cell)
  : heap
  = update_addr' m a (Some c)

let disjoint_cells (c0 c1:cell u#h) : prop =
    let Ref t0 p0 f0 v0 = c0 in
    let Ref t1 p1 f1 v1 = c1 in
    t0 == t1 /\
    p0 == p1 /\
    composable p0 v0 v1 /\
    (Frac.sum_perm f0 f1 `Frac.lesser_equal_perm` Frac.full_perm) /\
    (Frac.sum_perm f0 f1 == Frac.full_perm ==> p0.refine (op p0 v0 v1))

let disjoint_cells_sym (c0 c1:cell u#h)
  : Lemma (requires disjoint_cells c0 c1)
val disjoint_cells_sym (c0 c1: cell u#h)
    : Lemma (requires disjoint_cells c0 c1) (ensures disjoint_cells c1 c0)
c0: Steel.Heap.cell -> c1: Steel.Heap.cell
  -> FStar.Pervasives.Lemma (requires Steel.Heap.disjoint_cells c0 c1)
      (ensures Steel.Heap.disjoint_cells c1 c0)