inductive CC.CapabilitySet : Type

A set of capability labels, representing an "authority": they are the set of capabilities a program at most uses.

• empty : CapabilitySet
• cap : ℕ → CapabilitySet
• union : CapabilitySet → CapabilitySet → CapabilitySet

inductive CC.CapabilitySet.mem : ℕ → CapabilitySet → Prop

• here {l : ℕ} : mem l (cap l)
• left {l : ℕ} {C1 C2 : CapabilitySet} : mem l C1 → mem l (C1.union C2)
• right {l : ℕ} {C1 C2 : CapabilitySet} : mem l C2 → mem l (C1.union C2)

instance CC.CapabilitySet.instMembership : Membership ℕ CapabilitySet

Equations

• CC.CapabilitySet.instMembership = { mem := fun (C : CC.CapabilitySet) (l : ℕ) => CC.CapabilitySet.mem l C }

instance CC.CapabilitySet.instEmptyCollection : EmptyCollection CapabilitySet

Equations

• CC.CapabilitySet.instEmptyCollection = { emptyCollection := CC.CapabilitySet.empty }

instance CC.CapabilitySet.instUnion : Union CapabilitySet

Equations

• CC.CapabilitySet.instUnion = { union := CC.CapabilitySet.union }

def CC.CapabilitySet.singleton (l : ℕ) : CapabilitySet

Equations

• CC.CapabilitySet.singleton l = CC.CapabilitySet.cap l

instance CC.CapabilitySet.instSingleton : Singleton ℕ CapabilitySet

Equations

• CC.CapabilitySet.instSingleton = { singleton := CC.CapabilitySet.singleton }

inductive CC.CapabilitySet.Subset : CapabilitySet → CapabilitySet → Prop

• refl {C : CapabilitySet} : C.Subset C
• empty {C : CapabilitySet} : CapabilitySet.empty.Subset C
• trans {C1 C2 C3 : CapabilitySet} : C1.Subset C2 → C2.Subset C3 → C1.Subset C3
• union_left {C1 C3 C2 : CapabilitySet} : C1.Subset C3 → C2.Subset C3 → (C1 ∪ C2).Subset C3
• union_right_left {C1 C2 : CapabilitySet} : C1.Subset (C1 ∪ C2)
• union_right_right {C1 C2 : CapabilitySet} : C1.Subset (C2 ∪ C1)

instance CC.CapabilitySet.instHasSubset : HasSubset CapabilitySet

Equations

• CC.CapabilitySet.instHasSubset = { Subset := CC.CapabilitySet.Subset }

theorem CC.CapabilitySet.subset_preserves_mem {C1 C2 : CapabilitySet} {x : ℕ} (hsub : C1 ⊆ C2) (hmem : x ∈ C1) : x ∈ C2

theorem CC.CapabilitySet.mem_imp_singleton_subset {C : CapabilitySet} {x : ℕ} (hmem : x ∈ C) : {x} ⊆ C

If an element is in a set, then the singleton of that element is a subset of the set.

theorem CC.CapabilitySet.subset_refl {C : CapabilitySet} : C ⊆ C

theorem CC.CapabilitySet.subset_trans {C1 C2 C3 : CapabilitySet} (h1 : C1 ⊆ C2) (h2 : C2 ⊆ C3) : C1 ⊆ C3

theorem CC.CapabilitySet.empty_subset {C : CapabilitySet} : empty ⊆ C

theorem CC.CapabilitySet.union_subset_of_subset_of_subset {C1 C2 C : CapabilitySet} (h1 : C1 ⊆ C) (h2 : C2 ⊆ C) : C1 ∪ C2 ⊆ C

theorem CC.CapabilitySet.subset_union_left {C1 C2 : CapabilitySet} : C1 ⊆ C1 ∪ C2

theorem CC.CapabilitySet.subset_union_right {C1 C2 : CapabilitySet} : C2 ⊆ C1 ∪ C2

def CC.CapabilitySet.equiv (C1 C2 : CapabilitySet) : Prop

Equations

• (C1 ≈ C2) = ∀ (x : ℕ), x ∈ C1 ↔ x ∈ C2

def CC.CapabilitySet.«term_≈_» : Lean.TrailingParserDescr

Equations

• CC.CapabilitySet.«term_≈_» = Lean.ParserDescr.trailingNode `CC.CapabilitySet.«term_≈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))

theorem CC.CapabilitySet.equiv_refl {C : CapabilitySet} : C ≈ C

theorem CC.CapabilitySet.equiv_symm {C1 C2 : CapabilitySet} (h : C1 ≈ C2) : C2 ≈ C1

theorem CC.CapabilitySet.equiv_trans {C1 C2 C3 : CapabilitySet} (h1 : C1 ≈ C2) (h2 : C2 ≈ C3) : C1 ≈ C3

theorem CC.CapabilitySet.empty_union_equiv {C : CapabilitySet} : ∅ ∪ C ≈ C

theorem CC.CapabilitySet.union_empty_equiv {C : CapabilitySet} : C ∪ ∅ ≈ C

theorem CC.CapabilitySet.union_assoc_equiv {C1 C2 C3 : CapabilitySet} : C1 ∪ C2 ∪ C3 ≈ C1 ∪ (C2 ∪ C3)

theorem CC.CapabilitySet.subset_of_equiv_subset {C1 C2 C : CapabilitySet} (heq : C1 ≈ C2) (hsub : C2 ⊆ C) : C1 ⊆ C

If C1 ≈ C2 and C2 ⊆ C, then C1 ⊆ C. This allows transferring subset through equivalence.

structure CC.HeapVal : Type

A heap value. It must be a simple value, with a reachability set computed.

• unwrap : Exp ∅
• isVal : self.unwrap.IsSimpleVal
• reachability : CapabilitySet

theorem CC.Exp.IsSimpleVal.to_IsVal {s : Sig} {e : Exp s} (h : e.IsSimpleVal) : e.IsVal

Convert IsSimpleVal to IsVal

inductive CC.CapabilityInfo : Type

Underlying info of a capability.

• basic : CapabilityInfo
• mcell : Bool → CapabilityInfo

inductive CC.Cell : Type

A heap cell.

• val : HeapVal → Cell
• capability : CapabilityInfo → Cell
• masked : Cell

def CC.Heap : Type

Equations

• CC.Heap = (ℕ → Option CC.Cell)

def CC.Heap.empty : Heap

Equations

• CC.Heap.empty x✝ = none

instance CC.Heap.instEmptyCollection : EmptyCollection Heap

Equations

• CC.Heap.instEmptyCollection = { emptyCollection := CC.Heap.empty }

def CC.Heap.extend (h : Heap) (l : ℕ) (v : HeapVal) : Heap

Equations

• h.extend l v l' = if l' = l then some (CC.Cell.val v) else h l'

def CC.Heap.extend_cap (h : Heap) (l : ℕ) : Heap

Equations

• h.extend_cap l l' = if l' = l then some (CC.Cell.capability CC.CapabilityInfo.basic) else h l'

def CC.Heap.update_cell (h : Heap) (l : ℕ) (c : Cell) : Heap

Update a cell in the heap with a new cell value.

Equations

• h.update_cell l c l' = if l' = l then some c else h l'

def CC.Cell.subsumes : Cell → Cell → Prop

Auxiliary relation: one cell subsumes another. For mutable cells, the boolean value is irrelevant.

Equations

• (CC.Cell.capability (CC.CapabilityInfo.mcell a)).subsumes (CC.Cell.capability (CC.CapabilityInfo.mcell a_1)) = True
• x✝¹.subsumes x✝ = (x✝¹ = x✝)

theorem CC.Cell.subsumes_refl (c : Cell) : c.subsumes c

theorem CC.Cell.subsumes_trans {c1 c2 c3 : Cell} (h12 : c1.subsumes c2) (h23 : c2.subsumes c3) : c1.subsumes c3

def CC.Heap.subsumes (big small : Heap) : Prop

Equations

• big.subsumes small = ∀ (l : ℕ) (v : CC.Cell), small l = some v → ∃ (v' : CC.Cell), big l = some v' ∧ v'.subsumes v

theorem CC.Heap.subsumes_refl (h : Heap) : h.subsumes h

def CC.Hprop : Type

Heap predicate.

Equations

• CC.Hprop = (CC.Heap → Prop)

def CC.Hpost : Type

Postcondition.

Equations

• CC.Hpost = (CC.Exp ∅ → CC.Hprop)

def CC.Hpost.is_monotonic (Q : Hpost) : Prop

Monotonicity of postconditions.

Equations

• Q.is_monotonic = ∀ {h1 h2 : CC.Heap} {e : CC.Exp ∅}, h2.subsumes h1 → Q e h1 → Q e h2

def CC.Hpost.entails (Q1 Q2 : Hpost) : Prop

Equations

• Q1.entails Q2 = ∀ (h : CC.Heap) (e : CC.Exp ∅), Q1 e h → Q2 e h

def CC.Hpost.entails_refl (Q : Hpost) : Q.entails Q

Equations

• ⋯ = hQ

def CC.Heap.subsumes_trans {h1 h2 h3 : Heap} (h12 : h1.subsumes h2) (h23 : h2.subsumes h3) : h1.subsumes h3

Equations

• ⋯ = ⋯

theorem CC.Heap.update_mcell_subsumes (h : Heap) (l : ℕ) (hexists : ∃ (b0 : Bool), h l = some (Cell.capability (CapabilityInfo.mcell b0))) (b : Bool) : (h.update_cell l (Cell.capability (CapabilityInfo.mcell b))).subsumes h

Updating an mcell with another mcell creates a heap that subsumes the original.

theorem CC.Heap.extend_lookup_eq (h : Heap) (l : ℕ) (v : HeapVal) : h.extend l v l = some (Cell.val v)

theorem CC.Heap.extend_subsumes {v : HeapVal} {H : Heap} {l : ℕ} (hfresh : H l = none) : (H.extend l v).subsumes H

inductive CC.CaptureSet.WfInHeap {s : Sig} : CaptureSet s → Heap → Prop

• wf_empty {s : Sig} {H : Heap} : ∅.WfInHeap H
• wf_union {s : Sig} {C1 : CaptureSet s} {H : Heap} {C2 : CaptureSet s} : C1.WfInHeap H → C2.WfInHeap H → (C1 ∪ C2).WfInHeap H
• wf_var_free {s : Sig} {H : Heap} {val : Cell} {x : ℕ} : H x = some val → (var (Var.free x)).WfInHeap H
• wf_var_bound {s : Sig} {x : BVar s Kind.var} {H : Heap} : (var (Var.bound x)).WfInHeap H
• wf_cvar {s : Sig} {x : BVar s Kind.cvar} {H : Heap} : (cvar x).WfInHeap H

inductive CC.Var.WfInHeap {k : Kind} {s : Sig} : Var k s → Heap → Prop

• wf_bound {k : Kind} {s : Sig} {x : BVar s k} {H : Heap} : (bound x).WfInHeap H
• wf_free {k : Kind} {s : Sig} {H : Heap} {val : Cell} {n : ℕ} : H n = some val → (free n).WfInHeap H

inductive CC.CaptureBound.WfInHeap {s : Sig} : CaptureBound s → Heap → Prop

• wf_unbound {s : Sig} {H : Heap} : unbound.WfInHeap H
• wf_bound {s : Sig} {cs : CaptureSet s} {H : Heap} : cs.WfInHeap H → (bound cs).WfInHeap H

inductive CC.Ty.WfInHeap {sort : TySort} {s : Sig} : Ty sort s → Heap → Prop

• wf_top {x✝ : Sig} {H : Heap} : top.WfInHeap H
• wf_tvar {x✝ : Sig} {x : BVar x✝ Kind.tvar} {H : Heap} : (tvar x).WfInHeap H
• wf_arrow {x✝ : Sig} {T1 : Ty TySort.capt x✝} {H : Heap} {T2 : Ty TySort.exi (x✝,x)} : T1.WfInHeap H → T2.WfInHeap H → (T1.arrow T2).WfInHeap H
• wf_poly {x✝ : Sig} {T1 : Ty TySort.shape x✝} {H : Heap} {T2 : Ty TySort.exi (x✝,X)} : T1.WfInHeap H → T2.WfInHeap H → (T1.poly T2).WfInHeap H
• wf_cpoly {x✝ : Sig} {cb : CaptureBound x✝} {H : Heap} {T : Ty TySort.exi (x✝,C)} : cb.WfInHeap H → T.WfInHeap H → (cpoly cb T).WfInHeap H
• wf_unit {x✝ : Sig} {H : Heap} : unit.WfInHeap H
• wf_cap {x✝ : Sig} {H : Heap} : cap.WfInHeap H
• wf_bool {x✝ : Sig} {H : Heap} : bool.WfInHeap H
• wf_cell {x✝ : Sig} {H : Heap} : cell.WfInHeap H
• wf_capt {x✝ : Sig} {cs : CaptureSet x✝} {H : Heap} {T : Ty TySort.shape x✝} : cs.WfInHeap H → T.WfInHeap H → (capt cs T).WfInHeap H
• wf_exi {x✝ : Sig} {T : Ty TySort.capt (x✝,C)} {H : Heap} : T.WfInHeap H → T.exi.WfInHeap H
• wf_typ {x✝ : Sig} {T : Ty TySort.capt x✝} {H : Heap} : T.WfInHeap H → T.typ.WfInHeap H

inductive CC.Exp.WfInHeap {s : Sig} : Exp s → Heap → Prop

• wf_var {s : Sig} {x : Var Kind.var s} {H : Heap} : x.WfInHeap H → (var x).WfInHeap H
• wf_abs {s : Sig} {cs : CaptureSet s} {H : Heap} {T : Ty TySort.capt s} {e : Exp (s,x)} : cs.WfInHeap H → T.WfInHeap H → e.WfInHeap H → (abs cs T e).WfInHeap H
• wf_tabs {s : Sig} {cs : CaptureSet s} {H : Heap} {T : Ty TySort.shape s} {e : Exp (s,X)} : cs.WfInHeap H → T.WfInHeap H → e.WfInHeap H → (tabs cs T e).WfInHeap H
• wf_cabs {s : Sig} {cs : CaptureSet s} {H : Heap} {cb : CaptureBound s} {e : Exp (s,C)} : cs.WfInHeap H → cb.WfInHeap H → e.WfInHeap H → (cabs cs cb e).WfInHeap H
• wf_pack {s : Sig} {cs : CaptureSet s} {H : Heap} {x : Var Kind.var s} : cs.WfInHeap H → x.WfInHeap H → (pack cs x).WfInHeap H
• wf_app {s : Sig} {x : Var Kind.var s} {H : Heap} {y : Var Kind.var s} : x.WfInHeap H → y.WfInHeap H → (app x y).WfInHeap H
• wf_tapp {s : Sig} {x : Var Kind.var s} {H : Heap} {T : Ty TySort.shape s} : x.WfInHeap H → T.WfInHeap H → (tapp x T).WfInHeap H
• wf_capp {s : Sig} {x : Var Kind.var s} {H : Heap} {cs : CaptureSet s} : x.WfInHeap H → cs.WfInHeap H → (capp x cs).WfInHeap H
• wf_letin {s : Sig} {e1 : Exp s} {H : Heap} {e2 : Exp (s,x)} : e1.WfInHeap H → e2.WfInHeap H → (e1.letin e2).WfInHeap H
• wf_unpack {s : Sig} {e1 : Exp s} {H : Heap} {e2 : Exp (s,C,x)} : e1.WfInHeap H → e2.WfInHeap H → (e1.unpack e2).WfInHeap H
• wf_unit {s : Sig} {H : Heap} : unit.WfInHeap H
• wf_btrue {s : Sig} {H : Heap} : btrue.WfInHeap H
• wf_bfalse {s : Sig} {H : Heap} : bfalse.WfInHeap H
• wf_read {s : Sig} {x : Var Kind.var s} {H : Heap} : x.WfInHeap H → (read x).WfInHeap H
• wf_write {s : Sig} {x : Var Kind.var s} {H : Heap} {y : Var Kind.var s} : x.WfInHeap H → y.WfInHeap H → (write x y).WfInHeap H
• wf_cond {s : Sig} {x : Var Kind.var s} {H : Heap} {e2 e3 : Exp s} : x.WfInHeap H → e2.WfInHeap H → e3.WfInHeap H → (cond x e2 e3).WfInHeap H

theorem CC.Var.wf_of_closed {k : Kind} {s : Sig} {x : Var k s} {H : Heap} (hclosed : x.IsClosed) : x.WfInHeap H

Closedness implies well-formedness for variables.

theorem CC.CaptureSet.wf_of_closed {s : Sig} {cs : CaptureSet s} {H : Heap} (hclosed : cs.IsClosed) : cs.WfInHeap H

Closedness implies well-formedness for capture sets.

theorem CC.CaptureBound.wf_of_closed {s : Sig} {cb : CaptureBound s} {H : Heap} (hclosed : cb.IsClosed) : cb.WfInHeap H

Closedness implies well-formedness for capture bounds.

theorem CC.Ty.wf_of_closed {sort : TySort} {s : Sig} {T : Ty sort s} {H : Heap} (hclosed : T.IsClosed) : T.WfInHeap H

Closedness implies well-formedness for types.

theorem CC.Exp.wf_of_closed {s : Sig} {e : Exp s} {H : Heap} (hclosed : e.IsClosed) : e.WfInHeap H

Closedness implies well-formedness for expressions.

theorem CC.Var.wf_monotonic {a✝ : Kind} {a✝¹ : Sig} {x : Var a✝ a✝¹} {h1 h2 : Heap} (hsub : h2.subsumes h1) (hwf : x.WfInHeap h1) : x.WfInHeap h2

theorem CC.CaptureSet.wf_monotonic {a✝ : Sig} {cs : CaptureSet a✝} {h1 h2 : Heap} (hsub : h2.subsumes h1) (hwf : cs.WfInHeap h1) : cs.WfInHeap h2

theorem CC.CaptureBound.wf_monotonic {a✝ : Sig} {cb : CaptureBound a✝} {h1 h2 : Heap} (hsub : h2.subsumes h1) (hwf : cb.WfInHeap h1) : cb.WfInHeap h2

theorem CC.Ty.wf_monotonic {a✝ : TySort} {a✝¹ : Sig} {T : Ty a✝ a✝¹} {h1 h2 : Heap} (hsub : h2.subsumes h1) (hwf : T.WfInHeap h1) : T.WfInHeap h2

theorem CC.Exp.wf_monotonic {a✝ : Sig} {e : Exp a✝} {h1 h2 : Heap} (hsub : h2.subsumes h1) (hwf : e.WfInHeap h1) : e.WfInHeap h2

theorem CC.Exp.wf_inv_letin {s : Sig} {e1 : Exp s} {e2 : Exp (s,x)} {H : Heap} (hwf : (e1.letin e2).WfInHeap H) : e1.WfInHeap H ∧ e2.WfInHeap H

Inversion for let-in: if let x = e1 in e2 is well-formed, then both e1 and e2 are well-formed.

theorem CC.Exp.wf_inv_unpack {s : Sig} {e1 : Exp s} {e2 : Exp (s,C,x)} {H : Heap} (hwf : (e1.unpack e2).WfInHeap H) : e1.WfInHeap H ∧ e2.WfInHeap H

Inversion for unpack: if unpack e1 in e2 is well-formed, then both e1 and e2 are well-formed.

theorem CC.Exp.wf_inv_cond {s : Sig} {x : Var Kind.var s} {e2 e3 : Exp s} {H : Heap} (hwf : (cond x e2 e3).WfInHeap H) : x.WfInHeap H ∧ e2.WfInHeap H ∧ e3.WfInHeap H

Inversion for conditionals.

theorem CC.Exp.wf_inv_abs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.capt s} {e : Exp (s,x)} {H : Heap} (hwf : (abs cs T e).WfInHeap H) : cs.WfInHeap H ∧ T.WfInHeap H ∧ e.WfInHeap H

Inversion for lambda abstraction: if λ(cs) (x : T). e is well-formed, then its capture set, type, and body are all well-formed.

theorem CC.Exp.wf_inv_tabs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.shape s} {e : Exp (s,X)} {H : Heap} (hwf : (tabs cs T e).WfInHeap H) : cs.WfInHeap H ∧ T.WfInHeap H ∧ e.WfInHeap H

Inversion for type abstraction: if Λ(cs) (X <: T). e is well-formed, then its capture set, type bound, and body are all well-formed.

theorem CC.Exp.wf_inv_cabs {s : Sig} {cs : CaptureSet s} {cb : CaptureBound s} {e : Exp (s,C)} {H : Heap} (hwf : (cabs cs cb e).WfInHeap H) : cs.WfInHeap H ∧ cb.WfInHeap H ∧ e.WfInHeap H

Inversion for capture abstraction: if λ[cs] (C <: cb). e is well-formed, then its capture set, capture bound, and body are all well-formed.

structure CC.Subst.WfInHeap {s1 s2 : Sig} (s : Subst s1 s2) (H : Heap) : Prop

• wf_var (x : BVar s1 Kind.var) : (s.var x).WfInHeap H
• wf_tvar (X : BVar s1 Kind.tvar) : (s.tvar X).WfInHeap H
• wf_cvar (C : BVar s1 Kind.cvar) : (s.cvar C).WfInHeap H

def CC.reachability_of_loc (h : Heap) (l : ℕ) : CapabilitySet

Lookup the reachability set of a location.

Equations

• One or more equations did not get rendered due to their size.

def CC.expand_captures (h : Heap) (cs : CaptureSet ∅) : CapabilitySet

Resolve reachability of each element of the capture set.

Equations

• CC.expand_captures h CC.CaptureSet.empty = ∅
• CC.expand_captures h (CC.CaptureSet.var (CC.Var.free loc)) = CC.reachability_of_loc h loc
• CC.expand_captures h (cs1.union cs2) = CC.expand_captures h cs1 ∪ CC.expand_captures h cs2

def CC.compute_reachability (h : Heap) (v : Exp ∅) (hv : v.IsSimpleVal) : CapabilitySet

Compute reachability for a heap value.

Equations

• CC.compute_reachability h (CC.Exp.abs cs a a_1) hv_2 = CC.expand_captures h cs
• CC.compute_reachability h (CC.Exp.tabs cs a a_1) hv_2 = CC.expand_captures h cs
• CC.compute_reachability h (CC.Exp.cabs cs a a_1) hv_2 = CC.expand_captures h cs
• CC.compute_reachability h CC.Exp.unit hv_2 = ∅
• CC.compute_reachability h CC.Exp.btrue hv_2 = ∅
• CC.compute_reachability h CC.Exp.bfalse hv_2 = ∅

def CC.resolve : Heap → Exp ∅ → Option (Exp ∅)

Equations

• One or more equations did not get rendered due to their size.
• CC.resolve x✝ (CC.Exp.var (CC.Var.free x_2)) = match x✝ x_2 with | some (CC.Cell.val v) => some v.unwrap | x => none
• CC.resolve x✝¹ x✝ = some x✝

def CC.resolve_reachability (H : Heap) (e : Exp ∅) : CapabilitySet

Equations

• CC.resolve_reachability H (CC.Exp.var (CC.Var.free x)) = CC.reachability_of_loc H x
• CC.resolve_reachability H (CC.Exp.abs cs a a_1) = CC.expand_captures H cs
• CC.resolve_reachability H (CC.Exp.tabs cs a a_1) = CC.expand_captures H cs
• CC.resolve_reachability H (CC.Exp.cabs cs a a_1) = CC.expand_captures H cs
• CC.resolve_reachability H e = ∅

theorem CC.resolve_monotonic {e v : Exp ∅} {H1 H2 : Heap} (hsub : H2.subsumes H1) (hres : resolve H1 e = some v) : resolve H2 e = some v

theorem CC.reachability_of_loc_monotonic {v : Cell} {h1 h2 : Heap} (hsub : h2.subsumes h1) (l : ℕ) (hex : h1 l = some v) : reachability_of_loc h2 l = reachability_of_loc h1 l

theorem CC.expand_captures_monotonic {h1 h2 : Heap} (hsub : h2.subsumes h1) (cs : CaptureSet ∅) (hwf : cs.WfInHeap h1) : expand_captures h2 cs = expand_captures h1 cs

Expanding a capture set in a bigger heap yields the same result. Proof by induction on cs. Requires all free locations in cs to exist in h1.

theorem CC.resolve_reachability_monotonic {H1 H2 : Heap} (hsub : H2.subsumes H1) (e : Exp ∅) (hwf : e.WfInHeap H1) : resolve_reachability H2 e = resolve_reachability H1 e

theorem CC.compute_reachability_monotonic {h1 h2 : Heap} (hsub : h2.subsumes h1) (v : Exp ∅) (hv : v.IsSimpleVal) (hwf : v.WfInHeap h1) : compute_reachability h2 v hv = compute_reachability h1 v hv

Computing reachability of a value in a bigger heap yields the same result. Proof by cases on hv, using expand_captures_monotonic.

theorem CC.reachability_of_loc_update_mcell (h : Heap) (l : ℕ) (hexists : ∃ (b0 : Bool), h l = some (Cell.capability (CapabilityInfo.mcell b0))) (b : Bool) (l' : ℕ) : reachability_of_loc (h.update_cell l (Cell.capability (CapabilityInfo.mcell b))) l' = reachability_of_loc h l'

Updating an mcell preserves reachability_of_loc for all locations.

theorem CC.expand_captures_update_mcell (h : Heap) (l : ℕ) (hexists : ∃ (b0 : Bool), h l = some (Cell.capability (CapabilityInfo.mcell b0))) (b : Bool) (cs : CaptureSet ∅) : expand_captures (h.update_cell l (Cell.capability (CapabilityInfo.mcell b))) cs = expand_captures h cs

Updating an mcell preserves expand_captures.

theorem CC.compute_reachability_update_mcell (h : Heap) (l : ℕ) (hexists : ∃ (b0 : Bool), h l = some (Cell.capability (CapabilityInfo.mcell b0))) (b : Bool) (v : Exp ∅) (hv : v.IsSimpleVal) : compute_reachability (h.update_cell l (Cell.capability (CapabilityInfo.mcell b))) v hv = compute_reachability h v hv

Updating an mcell preserves compute_reachability.

structure CC.Heap.WfHeap (H : Heap) : Prop

A heap is well-formed if all values stored in it contain well-formed expressions.

• wf_val (l : ℕ) (hv : HeapVal) : H l = some (Cell.val hv) → hv.unwrap.WfInHeap H
• wf_reach (l : ℕ) (v : Exp ∅) (hv : v.IsSimpleVal) (R : CapabilitySet) : H l = some (Cell.val { unwrap := v, isVal := hv, reachability := R }) → R = compute_reachability H v hv

theorem CC.Heap.wf_empty : ∅.WfHeap

The empty heap is well-formed.

theorem CC.Heap.wf_extend {H : Heap} {l : ℕ} {v : HeapVal} (hwf_H : H.WfHeap) (hwf_v : v.unwrap.WfInHeap H) (hreach : v.reachability = compute_reachability H v.unwrap ⋯) (hfresh : H l = none) : (H.extend l v).WfHeap

Extending a well-formed heap with a well-formed value preserves well-formedness.

theorem CC.Heap.wf_lookup {H : Heap} {l : ℕ} {hv : HeapVal} (hwf_H : H.WfHeap) (hlookup : H l = some (Cell.val hv)) : hv.unwrap.WfInHeap H

If a heap is well-formed and we look up a value, the expression is well-formed.

theorem CC.Var.wf_rename {k : Kind} {s1 s2 : Sig} {x : Var k s1} {f : Rename s1 s2} {H : Heap} (hwf : x.WfInHeap H) : (x.rename f).WfInHeap H

Renaming preserves well-formedness of variables.

theorem CC.CaptureSet.wf_rename {s1 s2 : Sig} {cs : CaptureSet s1} {f : Rename s1 s2} {H : Heap} (hwf : cs.WfInHeap H) : (cs.rename f).WfInHeap H

Renaming preserves well-formedness of capture sets.

theorem CC.CaptureBound.wf_rename {s1 s2 : Sig} {cb : CaptureBound s1} {f : Rename s1 s2} {H : Heap} (hwf : cb.WfInHeap H) : (cb.rename f).WfInHeap H

Renaming preserves well-formedness of capture bounds.

theorem CC.Ty.wf_rename {sort : TySort} {s1 s2 : Sig} {T : Ty sort s1} {f : Rename s1 s2} {H : Heap} (hwf : T.WfInHeap H) : (T.rename f).WfInHeap H

Renaming preserves well-formedness of types.

theorem CC.Exp.wf_rename {s1 s2 : Sig} {e : Exp s1} {f : Rename s1 s2} {H : Heap} (hwf : e.WfInHeap H) : (e.rename f).WfInHeap H

Renaming preserves well-formedness of expressions.

theorem CC.CaptureSet.wf_of_var {s : Sig} {x : Var Kind.var s} {H : Heap} (hwf : x.WfInHeap H) : (var x).WfInHeap H

A well-formed variable yields a well-formed capture set.

theorem CC.Subst.wf_lift {s1 s2 : Sig} {k : Kind} {σ : Subst s1 s2} {H : Heap} (hwf_σ : σ.WfInHeap H) : σ.lift.WfInHeap H

Lifting a well-formed substitution preserves well-formedness.

theorem CC.Var.wf_subst {s1 s2 : Sig} {x : Var Kind.var s1} {σ : Subst s1 s2} {H : Heap} (hwf_x : x.WfInHeap H) (hwf_σ : σ.WfInHeap H) : (x.subst σ).WfInHeap H

Well-formed substitutions preserve well-formedness of variables.

theorem CC.CaptureSet.wf_subst {s1 s2 : Sig} {cs : CaptureSet s1} {σ : Subst s1 s2} {H : Heap} (hwf_cs : cs.WfInHeap H) (hwf_σ : σ.WfInHeap H) : (cs.subst σ).WfInHeap H

Well-formed substitutions preserve well-formedness of capture sets.

theorem CC.CaptureBound.wf_subst {s1 s2 : Sig} {cb : CaptureBound s1} {σ : Subst s1 s2} {H : Heap} (hwf_cb : cb.WfInHeap H) (hwf_σ : σ.WfInHeap H) : (cb.subst σ).WfInHeap H

Well-formed substitutions preserve well-formedness of capture bounds.

theorem CC.Ty.wf_subst {sort : TySort} {s1 s2 : Sig} {T : Ty sort s1} {σ : Subst s1 s2} {H : Heap} (hwf_T : T.WfInHeap H) (hwf_σ : σ.WfInHeap H) : (T.subst σ).WfInHeap H

Well-formed substitutions preserve well-formedness of types.

theorem CC.Exp.wf_subst {s1 s2 : Sig} {e : Exp s1} {σ : Subst s1 s2} {H : Heap} (hwf_e : e.WfInHeap H) (hwf_σ : σ.WfInHeap H) : (e.subst σ).WfInHeap H

Well-formed substitutions preserve well-formedness of expressions.

theorem CC.Subst.wf_openVar {s : Sig} {x : Var Kind.var s} {H : Heap} (hwf_x : x.WfInHeap H) : (openVar x).WfInHeap H

Opening substitution for variables is well-formed if the variable is well-formed.

theorem CC.Subst.wf_openTVar {s : Sig} {U : Ty TySort.shape s} {H : Heap} (hwf_U : U.WfInHeap H) : (openTVar U).WfInHeap H

Opening substitution for type variables is well-formed if the type is well-formed.

theorem CC.Subst.wf_openCVar {s : Sig} {C : CaptureSet s} {H : Heap} (hwf_C : C.WfInHeap H) : (openCVar C).WfInHeap H

Opening substitution for capture variables is well-formed if the capture set is well-formed.

theorem CC.Subst.wf_unpack {s : Sig} {C : CaptureSet s} {x : Var Kind.var s} {H : Heap} (hwf_C : C.WfInHeap H) (hwf_x : x.WfInHeap H) : (unpack C x).WfInHeap H

Unpack substitution is well-formed if both the capture set and variable are well-formed.

def CC.Heap.HasFinDom (H : Heap) (L : Finset ℕ) : Prop

Equations

• H.HasFinDom L = ∀ (l : ℕ), H l ≠ none ↔ l ∈ L

def CC.Heap.empty_has_fin_dom : ∅.HasFinDom ∅

Equations

• ⋯ = ⋯

theorem CC.Heap.extend_has_fin_dom {H : Heap} {dom : Finset ℕ} {l : ℕ} {v : HeapVal} (hdom : H.HasFinDom dom) (hfresh : H l = none) : (H.extend l v).HasFinDom (dom ∪ {l})

theorem CC.Heap.extend_cap_has_fin_dom {H : Heap} {dom : Finset ℕ} {l : ℕ} (hdom : H.HasFinDom dom) (hfresh : H l = none) : (H.extend_cap l).HasFinDom (dom ∪ {l})

structure CC.Memory : Type

Memory is a well-formed heap.

• heap : Heap
• wf : self.heap.WfHeap
• findom : ∃ (dom : Finset ℕ), self.heap.HasFinDom dom

def CC.Memory.empty : Memory

Create an empty memory.

Equations

• CC.Memory.empty = { heap := ∅, wf := CC.Heap.wf_empty, findom := CC.Memory.empty._proof_1 }

def CC.Memory.lookup (m : Memory) (l : ℕ) : Option Cell

Lookup a value in memory.

Equations

• m.lookup l = m.heap l

def CC.Memory.extend (m : Memory) (l : ℕ) (v : HeapVal) (hwf_v : v.unwrap.WfInHeap m.heap) (hreach : v.reachability = compute_reachability m.heap v.unwrap ⋯) (hfresh : m.heap l = none) : Memory

Extend memory with a new value. Requires proof that the value is well-formed and the location is fresh.

Equations

• m.extend l v hwf_v hreach hfresh = { heap := m.heap.extend l v, wf := ⋯, findom := ⋯ }

theorem CC.Memory.Heap.extend_cap_subsumes {H : Heap} {l : ℕ} (hfresh : H l = none) : (H.extend_cap l).subsumes H

Heap extension with capability subsumes original heap.

def CC.Memory.extend_cap (m : Memory) (l : ℕ) (hfresh : m.heap l = none) : Memory

Extend memory with a capability cell.

Equations

• m.extend_cap l hfresh = { heap := m.heap.extend_cap l, wf := ⋯, findom := ⋯ }

def CC.Memory.extend_val (m : Memory) (l : ℕ) (v : HeapVal) (hwf_v : v.unwrap.WfInHeap m.heap) (hreach : v.reachability = compute_reachability m.heap v.unwrap ⋯) (hfresh : m.heap l = none) : Memory

Extend memory with a value that's well-formed in the current heap. This is often more convenient than extend in practice.

Equations

• m.extend_val l v hwf_v hreach hfresh = { heap := m.heap.extend l v, wf := ⋯, findom := ⋯ }

def CC.Memory.update_mcell (m : Memory) (l : ℕ) (b : Bool) (hexists : ∃ (b0 : Bool), m.heap l = some (Cell.capability (CapabilityInfo.mcell b0))) : Memory

Update a mutable cell in memory with a new boolean value. Requires proof that the location contains a mutable cell.

Equations

• m.update_mcell l b hexists = { heap := m.heap.update_cell l (CC.Cell.capability (CC.CapabilityInfo.mcell b)), wf := ⋯, findom := ⋯ }

def CC.Memory.subsumes (m1 m2 : Memory) : Prop

Memory subsumption: m1 subsumes m2 if m1's heap subsumes m2's heap.

Equations

• m1.subsumes m2 = m1.heap.subsumes m2.heap

theorem CC.Memory.subsumes_refl (m : Memory) : m.subsumes m

Reflexivity of memory subsumption.

theorem CC.Memory.subsumes_trans {m1 m2 m3 : Memory} (h12 : m1.subsumes m2) (h23 : m2.subsumes m3) : m1.subsumes m3

Transitivity of memory subsumption.

theorem CC.Memory.update_mcell_subsumes (m : Memory) (l : ℕ) (b : Bool) (hexists : ∃ (b0 : Bool), m.heap l = some (Cell.capability (CapabilityInfo.mcell b0))) : (m.update_mcell l b hexists).subsumes m

Updating a mutable cell creates a memory that subsumes the original.

theorem CC.Memory.update_mcell_subsumes_compat {m1 m2 : Memory} (l : ℕ) (b : Bool) (hexists1 : ∃ (b0 : Bool), m1.heap l = some (Cell.capability (CapabilityInfo.mcell b0))) (hexists2 : ∃ (b0 : Bool), m2.heap l = some (Cell.capability (CapabilityInfo.mcell b0))) (hsub : m2.subsumes m1) : (m2.update_mcell l b hexists2).subsumes (m1.update_mcell l b hexists1)

Updating mcells in subsuming memories preserves subsumption.

theorem CC.Memory.extend_lookup_eq (m : Memory) (l : ℕ) (v : HeapVal) (hwf_v : v.unwrap.WfInHeap m.heap) (hreach : v.reachability = compute_reachability m.heap v.unwrap ⋯) (hfresh : m.heap l = none) : (m.extend l v hwf_v hreach hfresh).lookup l = some (Cell.val v)

Looking up from a memory after extension at the same location returns the value.

theorem CC.Memory.extend_subsumes (m : Memory) (l : ℕ) (v : HeapVal) (hwf_v : v.unwrap.WfInHeap m.heap) (hreach : v.reachability = compute_reachability m.heap v.unwrap ⋯) (hfresh : m.heap l = none) : (m.extend l v hwf_v hreach hfresh).subsumes m

Extension subsumes the original memory.

theorem CC.Memory.extend_val_subsumes (m : Memory) (l : ℕ) (v : HeapVal) (hwf_v : v.unwrap.WfInHeap m.heap) (hreach : v.reachability = compute_reachability m.heap v.unwrap ⋯) (hfresh : m.heap l = none) : (m.extend_val l v hwf_v hreach hfresh).subsumes m

Extension with extend_val subsumes the original memory.

theorem CC.Memory.extend_cap_subsumes (m : Memory) (l : ℕ) (hfresh : m.heap l = none) : (m.extend_cap l hfresh).subsumes m

Capability extension subsumes the original memory.

theorem CC.Memory.wf_monotonic {e : Exp ∅} {m1 m2 : Memory} (hsub : m2.subsumes m1) (hwf : e.WfInHeap m1.heap) : e.WfInHeap m2.heap

Well-formedness is preserved under memory subsumption.

theorem CC.Memory.wf_lookup {m : Memory} {l : ℕ} {hv : HeapVal} (hlookup : m.lookup l = some (Cell.val hv)) : hv.unwrap.WfInHeap m.heap

Looking up a value from a memory yields a well-formed expression.

def CC.Mprop : Type

Memory predicate.

Equations

• CC.Mprop = (CC.Memory → Prop)

def CC.Mpost : Type

Memory postcondition.

Equations

• CC.Mpost = (CC.Exp ∅ → CC.Mprop)

def CC.Mpost.is_monotonic (Q : Mpost) : Prop

Monotonicity of memory postconditions.

Equations

• Q.is_monotonic = ∀ {m1 m2 : CC.Memory} {e : CC.Exp ∅}, e.WfInHeap m1.heap → m2.subsumes m1 → Q e m1 → Q e m2

def CC.Mpost.is_bool_independent (Q : Mpost) : Prop

Equations

• Q.is_bool_independent = ∀ {m : CC.Memory}, Q CC.Exp.btrue m ↔ Q CC.Exp.bfalse m

def CC.Mpost.entails (Q1 Q2 : Mpost) : Prop

Entailment between memory postconditions.

Equations

• Q1.entails Q2 = ∀ (m : CC.Memory) (e : CC.Exp ∅), Q1 e m → Q2 e m

def CC.Mpost.entails_refl (Q : Mpost) : Q.entails Q

Equations

• ⋯ = hQ

theorem CC.Memory.exists_fresh (m : Memory) : ∃ (l : ℕ), m.lookup l = none

def CC.Heap.HasCapDom (H : Heap) (d : Finset ℕ) : Prop

A heap has a capability domain if all capabilities on this heap lives in the given domain.

Equations

• H.HasCapDom d = ∀ (l : ℕ), (∃ (info : CC.CapabilityInfo), H l = some (CC.Cell.capability info)) ↔ l ∈ d

def CC.Heap.mask_caps (H : Heap) (d : Finset ℕ) : Heap

Masks capabilities in the heap outside of the given domain.

Equations

• H.mask_caps d l = match H l with | some (CC.Cell.capability info) => if l ∈ d then some (CC.Cell.capability info) else some CC.Cell.masked | some v => some v | none => none

def CC.CapabilitySet.to_finset : CapabilitySet → Finset ℕ

Turns a capability set into a finite set of natural numbers.

Equations

• CC.CapabilitySet.empty.to_finset = ∅
• (cs1.union cs2).to_finset = cs1.to_finset ∪ cs2.to_finset
• (CC.CapabilitySet.cap x_1).to_finset = {x_1}