val null (#a: Type u#a) (#pcm: pcm a) : ref a pcm
let null (#a:Type u#a) (#pcm:pcm a) : ref a pcm = core_ref_null
val null (#a: Type u#a) (#pcm: pcm a) : ref a pcm
let null (#a: Type u#a) (#pcm: pcm a) : ref a pcm =
core_ref_null
Steel.Heap.fsti.checked
Steel.Preorder.fst.checked prims.fst.checked FStar.Universe.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.Ghost.fsti.checked
Steel.Heap.fsti
FStar.PCM.pcm Steel.Heap.core_ref_null Steel.Heap.ref
(*
   Copyright 2019 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
open FStar.Ghost
open FStar.PCM

/// This module defines the behavior of a structured heap where each memory cell is governed by
/// a partial commutative monoid. This PCM structure is reused for the entire heap as it is possible
/// to talk about disjoint heaps and join them together.
///
/// In a sense, a heap here can be seen as a partial heap, containing a partial view of the state of
/// the memory. Combining disjoint heaps is then equivalent to conciling two partial views of the
/// memory together. This is our base for separation logic.
///
/// The heap is instrumented with affine heap predicates, heap predicates that don't change if you
/// augment the heap on which they're valid by joining another partial heap. These affine heap
/// predicates are the terms of our separation logic.
///
/// Finally, the module defines actions for heap, which are frame-preserving heap updates.

(**** The base : partial heaps *)

(**
  Abstract type of heaps. Can conceptually be thought of as a map from addresses to
  contents of memory cells.
*)
val heap  : Type u#(a + 1)

(** A [core_ref] is a key into the [heap] or [null] *)
val core_ref : Type u#0

(** We index a [core_ref] by the type of its heap contents
    and a [pcm] governing it, for ease of type inference *)
let ref (a:Type u#a) (pcm:pcm a) : Type u#0 = core_ref

val core_ref_null : core_ref

(** [null] is a specific reference, that is not associated to any value
val null (#a: Type u#a) (#pcm: pcm a) : ref a pcm
Steel.Heap.ref a pcm