def CC.Denot : Type

Denotation of types.

Equations

• CC.Denot = (CC.Memory → CC.Exp ∅ → Prop)

def CC.PreDenot : Type

Pre-denotation. It takes a capability to form a denotation.

Equations

• CC.PreDenot = (CC.CapabilitySet → CC.Denot)

def CC.CapDenot : Type

Capture-denotation. Given any memory, it produces a set of capabilities.

Equations

• CC.CapDenot = (CC.Memory → CC.CapabilitySet)

inductive CC.CapabilityBound : Type

A bound on capability sets. It can either be a concrete set of the top element.

• top : CapabilityBound
• set : CapabilitySet → CapabilityBound

def CC.CapBoundDenot : Type

Capture bound denotation.

Equations

• CC.CapBoundDenot = (CC.Memory → CC.CapabilityBound)

def CC.Denot.as_mpost (d : Denot) : Mpost

Equations

• d.as_mpost e m = d m e

def CC.Denot.is_monotonic (d : Denot) : Prop

Equations

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

def CC.CapDenot.is_monotonic_for (cd : CapDenot) (cs : CaptureSet ∅) : Prop

Equations

• cd.is_monotonic_for cs = ∀ {m1 m2 : CC.Memory}, cs.WfInHeap m1.heap → m2.subsumes m1 → cd m1 = cd m2

def CC.Denot.is_transparent (d : Denot) : Prop

Equations

• d.is_transparent = ∀ {m : CC.Memory} {x : ℕ} {v : CC.HeapVal}, m.lookup x = some (CC.Cell.val v) → d m v.unwrap → d m (CC.Exp.var (CC.Var.free x))

def CC.Denot.is_bool_independent (d : Denot) : Prop

Equations

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

def CC.Denot.is_proper (d : Denot) : Prop

Equations

• d.is_proper = (d.is_monotonic ∧ d.is_transparent ∧ d.is_bool_independent)

theorem CC.compute_reachability_eq_resolve_reachability (h : Heap) (v : Exp ∅) (hv : v.IsSimpleVal) : compute_reachability h v hv = resolve_reachability h v

For simple values, compute_reachability equals resolve_reachability.

axiom CC.Memory.reachability_invariant (m : Memory) (x : ℕ) (v : HeapVal) : m.heap x = some (Cell.val v) → v.reachability = compute_reachability m.heap v.unwrap ⋯

Heap invariant: the reachability stored in a heap value equals the computed reachability for that value.

This invariant is maintained by the operational semantics, which always uses compute_reachability when creating heap values (see eval_letin in BigStep.lean).

This is a fundamental property connecting operational reachability (stored in the heap) with denotational reachability (computed from expression structure).

theorem CC.reachability_of_loc_eq_resolve_reachability (m : Memory) (x : ℕ) (v : HeapVal) (hx : m.heap x = some (Cell.val v)) : reachability_of_loc m.heap x = resolve_reachability m.heap v.unwrap

Reachability of a heap location equals resolve_reachability of the stored value.

def CC.PreDenot.is_reachability_safe (denot : PreDenot) : Prop

This pre-denotation actually enforces the reachability bound.

Equations

• denot.is_reachability_safe = ∀ (R : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅), denot R m e → CC.resolve_reachability m.heap e ⊆ R

def CC.PreDenot.is_reachability_monotonic (pd : PreDenot) : Prop

This pre-denotation is monotonic over reachability sets.

Equations

• pd.is_reachability_monotonic = ∀ (R1 R2 : CC.CapabilitySet), R1 ⊆ R2 → ∀ (m : CC.Memory) (e : CC.Exp ∅), pd R1 m e → pd R2 m e

def CC.PreDenot.implies_wf (pd : PreDenot) : Prop

This pre-denotation entails heap well-formedness.

Equations

• pd.implies_wf = ∀ (R : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅), pd R m e → e.WfInHeap m.heap

def CC.PreDenot.is_tight (pd : PreDenot) : Prop

This pre-denotation is "tight" on reachability sets.

Equations

• pd.is_tight = ∀ (R : CC.CapabilitySet) (m : CC.Memory) (fx : ℕ), pd R m (CC.Exp.var (CC.Var.free fx)) → pd (CC.reachability_of_loc m.heap fx) m (CC.Exp.var (CC.Var.free fx))

def CC.PreDenot.is_proper (pd : PreDenot) : Prop

This is a proper pre-denotation.

Equations

• pd.is_proper = (pd.is_reachability_safe ∧ pd.is_reachability_monotonic ∧ pd.implies_wf ∧ pd.is_tight ∧ ∀ (C : CC.CapabilitySet), (pd C).is_proper)

theorem CC.Denot.as_mpost_is_monotonic {d : Denot} (hmon : d.is_monotonic) : d.as_mpost.is_monotonic

theorem CC.Denot.as_mpost_is_bool_independent {d : Denot} (hbool : d.is_bool_independent) : d.as_mpost.is_bool_independent

def CC.Denot.Imply (d1 d2 : Denot) : Prop

Equations

• d1.Imply d2 = ∀ (m : CC.Memory) (e : CC.Exp ∅), d1 m e → d2 m e

def CC.PreDenot.Imply (pd1 pd2 : PreDenot) : Prop

Equations

• pd1.Imply pd2 = ∀ (C : CC.CapabilitySet), (pd1 C).Imply (pd2 C)

def CC.Denot.ImplyAt (d1 : Denot) (m : Memory) (d2 : Denot) : Prop

Equations

• d1.ImplyAt m d2 = ∀ (e : CC.Exp ∅), d1 m e → d2 m e

def CC.PreDenot.ImplyAt (pd1 pd2 : PreDenot) (m : Memory) : Prop

Equations

• pd1.ImplyAt pd2 m = ∀ (C : CC.CapabilitySet), (pd1 C).ImplyAt m (pd2 C)

def CC.Denot.ImplyAfter (d1 : Denot) (m : Memory) (d2 : Denot) : Prop

Equations

• d1.ImplyAfter m d2 = ∀ (m' : CC.Memory), m'.subsumes m → d1.ImplyAt m' d2

def CC.PreDenot.ImplyAfter (pd1 : PreDenot) (m : Memory) (pd2 : PreDenot) : Prop

Equations

• pd1.ImplyAfter m pd2 = ∀ (C : CC.CapabilitySet), (pd1 C).ImplyAfter m (pd2 C)

theorem CC.Denot.imply_implyat {m : Memory} {d1 d2 : Denot} (himp : d1.Imply d2) : d1.ImplyAt m d2

theorem CC.Denot.implyat_trans {m : Memory} {d3 d1 d2 : Denot} (himp1 : d1.ImplyAt m d2) (himp2 : d2.ImplyAt m d3) : d1.ImplyAt m d3

theorem CC.Denot.imply_after_to_m_entails_after {d1 d2 : Denot} {m : Memory} (himp : d1.ImplyAfter m d2) : d1.as_mpost.entails_after m d2.as_mpost

theorem CC.Denot.imply_after_subsumes {m1 m2 : Memory} {d1 d2 : Denot} (himp : d1.ImplyAfter m1 d2) (hmem : m2.subsumes m1) : d1.ImplyAfter m2 d2

theorem CC.Denot.imply_after_to_imply_at {m : Memory} {d1 d2 : Denot} (himp : d1.ImplyAfter m d2) : d1.ImplyAt m d2

theorem CC.Denot.imply_after_trans {m : Memory} {d1 d2 d3 : Denot} (himp1 : d1.ImplyAfter m d2) (himp2 : d2.ImplyAfter m d3) : d1.ImplyAfter m d3

theorem CC.Denot.apply_imply_at {m : Memory} {e : Exp ∅} {d1 d2 : Denot} (ht : d1 m e) (himp : d1.ImplyAt m d2) : d2 m e

inductive CC.TypeInfo : Kind → Type

• var : ℕ → TypeInfo Kind.var
• tvar : PreDenot → TypeInfo Kind.tvar
• cvar : CaptureSet ∅ → TypeInfo Kind.cvar

inductive CC.TypeEnv : Sig → Type

• empty : TypeEnv ∅
• extend {s : Sig} {k : Kind} : TypeEnv s → TypeInfo k → TypeEnv (s,,k)

def CC.TypeEnv.extend_var {s : Sig} (Γ : TypeEnv s) (x : ℕ) : TypeEnv (s,x)

Equations

• Γ.extend_var x = Γ.extend (CC.TypeInfo.var x)

def CC.TypeEnv.extend_tvar {s : Sig} (Γ : TypeEnv s) (T : PreDenot) : TypeEnv (s,X)

Equations

• Γ.extend_tvar T = Γ.extend (CC.TypeInfo.tvar T)

def CC.TypeEnv.extend_cvar {s : Sig} (Γ : TypeEnv s) (ground : CaptureSet ∅) : TypeEnv (s,C)

Equations

• Γ.extend_cvar ground = Γ.extend (CC.TypeInfo.cvar ground)

def CC.TypeEnv.lookup {s : Sig} {k : Kind} (Γ : TypeEnv s) (x : BVar s k) : TypeInfo k

Equations

• (a.extend info).lookup CC.BVar.here = info
• (Γ.extend a).lookup x_2.there = Γ.lookup x_2

def CC.TypeEnv.lookup_var {s : Sig} (Γ : TypeEnv s) (x : BVar s Kind.var) : ℕ

Equations

• Γ.lookup_var x = match Γ.lookup x with | CC.TypeInfo.var y => y

def CC.TypeEnv.lookup_tvar {s : Sig} (Γ : TypeEnv s) (x : BVar s Kind.tvar) : PreDenot

Equations

• Γ.lookup_tvar x = match Γ.lookup x with | CC.TypeInfo.tvar T => T

def CC.TypeEnv.lookup_cvar {s : Sig} (Γ : TypeEnv s) (x : BVar s Kind.cvar) : CaptureSet ∅

Equations

• Γ.lookup_cvar x = match Γ.lookup x with | CC.TypeInfo.cvar cs => cs

def CC.Subst.from_TypeEnv {s : Sig} (env : TypeEnv s) : Subst s ∅

Equations

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

theorem CC.Subst.from_TypeEnv_empty : from_TypeEnv TypeEnv.empty = id

def CC.CaptureSet.ground_denot : CaptureSet ∅ → CapDenot

Compute denotation for a ground capture set.

Equations

• CC.CaptureSet.empty.ground_denot = fun (x : CC.Memory) => ∅
• (cs1.union cs2).ground_denot = fun (m : CC.Memory) => cs1.ground_denot m ∪ cs2.ground_denot m
• (CC.CaptureSet.var (CC.Var.free x_1)).ground_denot = fun (m : CC.Memory) => CC.reachability_of_loc m.heap x_1

def CC.CaptureSet.denot {s : Sig} (ρ : TypeEnv s) (cs : CaptureSet s) : CapDenot

Equations

• CC.CaptureSet.denot ρ cs = (cs.subst (CC.Subst.from_TypeEnv ρ)).ground_denot

def CC.CaptureBound.denot {s : Sig} : TypeEnv s → CaptureBound s → CapBoundDenot

Equations

• CC.CaptureBound.denot x✝ CC.CaptureBound.unbound = fun (x : CC.Memory) => CC.CapabilityBound.top
• CC.CaptureBound.denot x✝ (CC.CaptureBound.bound cs) = fun (m : CC.Memory) => CC.CapabilityBound.set (CC.CaptureSet.denot x✝ cs m)

inductive CC.CapabilitySet.BoundedBy : CapabilitySet → CapabilityBound → Prop

• top {C : CapabilitySet} : C.BoundedBy CapabilityBound.top
• set {C1 C2 : CapabilitySet} : C1 ⊆ C2 → C1.BoundedBy (CapabilityBound.set C2)

inductive CC.CapabilityBound.SubsetEq : CapabilityBound → CapabilityBound → Prop

• refl {B : CapabilityBound} : B.SubsetEq B
• set {C1 C2 : CapabilitySet} : C1 ⊆ C2 → (CapabilityBound.set C1).SubsetEq (CapabilityBound.set C2)
• top {B : CapabilityBound} : B.SubsetEq CapabilityBound.top

instance CC.instHasSubsetCapabilityBound : HasSubset CapabilityBound

Equations

• CC.instHasSubsetCapabilityBound = { Subset := CC.CapabilityBound.SubsetEq }

theorem CC.CapabilitySet.BoundedBy.trans {C : CapabilitySet} {B1 B2 : CapabilityBound} (hbound : C.BoundedBy B1) (hsub : B1 ⊆ B2) : C.BoundedBy B2

@[irreducible]

def CC.Ty.shape_val_denot {s : Sig} : TypeEnv s → Ty TySort.shape s → PreDenot

Equations

• One or more equations did not get rendered due to their size.
• CC.Ty.shape_val_denot x✝ CC.Ty.top = fun (R : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅) => e.WfInHeap m.heap ∧ CC.resolve_reachability m.heap e ⊆ R
• CC.Ty.shape_val_denot x✝ (CC.Ty.tvar X) = x✝.lookup_tvar X
• CC.Ty.shape_val_denot x✝ CC.Ty.unit = fun (x : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅) => CC.resolve m.heap e = some CC.Exp.unit
• CC.Ty.shape_val_denot x✝ CC.Ty.bool = fun (x : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅) => CC.resolve m.heap e = some CC.Exp.btrue ∨ CC.resolve m.heap e = some CC.Exp.bfalse

@[irreducible]

def CC.Ty.capt_val_denot {s : Sig} : TypeEnv s → Ty TySort.capt s → Denot

Equations

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

@[irreducible]

def CC.Ty.exi_val_denot {s : Sig} : TypeEnv s → Ty TySort.exi s → Denot

Equations

• One or more equations did not get rendered due to their size.
• CC.Ty.exi_val_denot x✝ T.typ = CC.Ty.capt_val_denot x✝ T

def CC.Ty.capt_exp_denot {s : Sig} : TypeEnv s → Ty TySort.capt s → PreDenot

Equations

• CC.Ty.capt_exp_denot x✝¹ x✝ = fun (A : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅) => CC.Eval A m e (CC.Ty.capt_val_denot x✝¹ x✝).as_mpost

@[irreducible]

def CC.Ty.exi_exp_denot {s : Sig} : TypeEnv s → Ty TySort.exi s → PreDenot

Equations

• CC.Ty.exi_exp_denot x✝¹ x✝ = fun (A : CC.CapabilitySet) (m : CC.Memory) (e : CC.Exp ∅) => CC.Eval A m e (CC.Ty.exi_val_denot x✝¹ x✝).as_mpost

instance CC.instCaptHasDenotation {s : Sig} : HasDenotation (Ty TySort.capt s) (TypeEnv s) Denot

Equations

• CC.instCaptHasDenotation = { interp := CC.Ty.capt_val_denot }

instance CC.instCaptHasExpDenotation {s : Sig} : HasExpDenotation (Ty TySort.capt s) (TypeEnv s) PreDenot

Equations

• CC.instCaptHasExpDenotation = { interp := CC.Ty.capt_exp_denot }

instance CC.instExiHasDenotation {s : Sig} : HasDenotation (Ty TySort.exi s) (TypeEnv s) Denot

Equations

• CC.instExiHasDenotation = { interp := CC.Ty.exi_val_denot }

instance CC.instExiHasExpDenotation {s : Sig} : HasExpDenotation (Ty TySort.exi s) (TypeEnv s) PreDenot

Equations

• CC.instExiHasExpDenotation = { interp := CC.Ty.exi_exp_denot }

instance CC.instShapeHasDenotation {s : Sig} : HasDenotation (Ty TySort.shape s) (TypeEnv s) PreDenot

Equations

• CC.instShapeHasDenotation = { interp := CC.Ty.shape_val_denot }

instance CC.instCaptureSetHasDenotation {s : Sig} : HasDenotation (CaptureSet s) (TypeEnv s) CapDenot

Equations

• CC.instCaptureSetHasDenotation = { interp := CC.CaptureSet.denot }

instance CC.instCaptureBoundHasDenotation {s : Sig} : HasDenotation (CaptureBound s) (TypeEnv s) CapBoundDenot

Equations

• CC.instCaptureBoundHasDenotation = { interp := CC.CaptureBound.denot }

def CC.EnvTyping {s : Sig} : Ctx s → TypeEnv s → Memory → Prop

Equations

• One or more equations did not get rendered due to their size.
• CC.EnvTyping CC.Ctx.empty CC.TypeEnv.empty x✝ = True
• CC.EnvTyping (Γ.push (CC.Binding.var T)) (env.extend (CC.TypeInfo.var n)) x✝ = (⟦T⟧_[env] x✝ (CC.Exp.var (CC.Var.free n)) ∧ CC.EnvTyping Γ env x✝)
• CC.EnvTyping (Γ.push (CC.Binding.tvar S)) (env.extend (CC.TypeInfo.tvar denot)) x✝ = (denot.is_proper ∧ denot.ImplyAfter x✝ ⟦S⟧_[env] ∧ CC.EnvTyping Γ env x✝)

def CC.SemanticTyping {s : Sig} (C : CaptureSet s) (Γ : Ctx s) (e : Exp s) (E : Ty TySort.exi s) : Prop

Equations

• (C # Γ ⊨ e : E) = ∀ (ρ : CC.TypeEnv s) (m : CC.Memory), CC.EnvTyping Γ ρ m → ⟦E⟧e_[ρ] (CC.CaptureSet.denot ρ C m) m (e.subst (CC.Subst.from_TypeEnv ρ))

def CC.«term_#_⊨_:_» : Lean.TrailingParserDescr

Equations

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

theorem CC.Subst.from_TypeEnv_weaken_open {s : Sig} {env : TypeEnv s} {x : ℕ} : (from_TypeEnv env).lift.comp (openVar (Var.free x)) = from_TypeEnv (env.extend_var x)

theorem CC.Exp.from_TypeEnv_weaken_open {s : Sig} {env : TypeEnv s} {x : ℕ} {e : Exp (s,x)} : (e.subst (Subst.from_TypeEnv env).lift).subst (Subst.openVar (Var.free x)) = e.subst (Subst.from_TypeEnv (env.extend_var x))

theorem CC.Subst.from_TypeEnv_weaken_open_tvar {s : Sig} {env : TypeEnv s} {d : PreDenot} : (from_TypeEnv env).lift.comp (openTVar Ty.top) = from_TypeEnv (env.extend_tvar d)

theorem CC.Exp.from_TypeEnv_weaken_open_tvar {s : Sig} {env : TypeEnv s} {d : PreDenot} {e : Exp (s,X)} : (e.subst (Subst.from_TypeEnv env).lift).subst (Subst.openTVar Ty.top) = e.subst (Subst.from_TypeEnv (env.extend_tvar d))

theorem CC.Subst.from_TypeEnv_weaken_open_cvar {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} : (from_TypeEnv env).lift.comp (openCVar cs) = from_TypeEnv (env.extend_cvar cs)

theorem CC.Exp.from_TypeEnv_weaken_open_cvar {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} {e : Exp (s,C)} : (e.subst (Subst.from_TypeEnv env).lift).subst (Subst.openCVar cs) = e.subst (Subst.from_TypeEnv (env.extend_cvar cs))

theorem CC.Subst.from_TypeEnv_weaken_unpack {a✝ : Sig} {ρ : TypeEnv a✝} {cs : CaptureSet ∅} {x : ℕ} : (from_TypeEnv ρ).lift.lift.comp (unpack cs (Var.free x)) = from_TypeEnv ((ρ.extend_cvar cs).extend_var x)

theorem CC.from_TypeEnv_wf_in_heap {s : Sig} {Γ : Ctx s} {ρ : TypeEnv s} {m : Memory} (htyping : EnvTyping Γ ρ m) : (Subst.from_TypeEnv ρ).WfInHeap m.heap

If a TypeEnv is typed with EnvTyping, then the substitution obtained from it via Subst.from_TypeEnv is well-formed in the heap.

This is a key lemma connecting the semantic typing judgment to syntactic well-formedness. Since EnvTyping ensures each variable location in the environment exists in memory, the substitution that maps variables to these locations must be well-formed.

def CC.Denot.Equiv (d1 d2 : Denot) : Prop

Equations

• d1.Equiv d2 = ∀ (m : CC.Memory) (e : CC.Exp ∅), d1 m e ↔ d2 m e

instance CC.Denot.instHasEquiv : HasEquiv Denot

Equations

• CC.Denot.instHasEquiv = { Equiv := CC.Denot.Equiv }

def CC.Denot.equiv_refl (d : Denot) : d ≈ d

Equations

• ⋯ = ⋯

def CC.Denot.equiv_symm (d1 d2 : Denot) : d1 ≈ d2 → d2 ≈ d1

Equations

• ⋯ = ⋯

def CC.Denot.equiv_trans (d1 d2 d3 : Denot) : d1 ≈ d2 → d2 ≈ d3 → d1 ≈ d3

Equations

• ⋯ = ⋯

theorem CC.Denot.eq_to_equiv (d1 d2 : Denot) : d1 = d2 → d1 ≈ d2

theorem CC.Denot.equiv_ltr {m : Memory} {e : Exp ∅} {d1 d2 : Denot} (heqv : d1 ≈ d2) (h1 : d1 m e) : d2 m e

theorem CC.Denot.equiv_rtl {m : Memory} {e : Exp ∅} {d1 d2 : Denot} (heqv : d1 ≈ d2) (h2 : d2 m e) : d1 m e

theorem CC.Denot.equiv_to_imply {d1 d2 : Denot} (heqv : d1 ≈ d2) : d1.Imply d2 ∧ d2.Imply d1

theorem CC.Denot.equiv_to_imply_l {d1 d2 : Denot} (heqv : d1 ≈ d2) : d1.Imply d2

theorem CC.Denot.equiv_to_imply_r {d1 d2 : Denot} (heqv : d1 ≈ d2) : d2.Imply d1

theorem CC.Denot.imply_to_entails (d1 d2 : Denot) (himp : d1.Imply d2) : d1.as_mpost.entails d2.as_mpost

def CC.PreDenot.Equiv (pd1 pd2 : PreDenot) : Prop

Equations

• pd1.Equiv pd2 = ∀ (A : CC.CapabilitySet), pd1 A ≈ pd2 A

instance CC.PreDenot.instHasEquiv : HasEquiv PreDenot

Equations

• CC.PreDenot.instHasEquiv = { Equiv := CC.PreDenot.Equiv }

theorem CC.PreDenot.equiv_def {pd1 pd2 : PreDenot} : pd1 ≈ pd2 ↔ ∀ (A : CapabilitySet) (m : Memory) (e : Exp ∅), pd1 A m e ↔ pd2 A m e

theorem CC.PreDenot.eq_to_equiv {pd1 pd2 : PreDenot} (h : pd1 = pd2) : pd1 ≈ pd2

theorem CC.PreDenot.equiv_refl (pd : PreDenot) : pd ≈ pd

theorem CC.PreDenot.equiv_symm (pd1 pd2 : PreDenot) : pd1 ≈ pd2 → pd2 ≈ pd1

theorem CC.PreDenot.equiv_trans (pd1 pd2 pd3 : PreDenot) : pd1 ≈ pd2 → pd2 ≈ pd3 → pd1 ≈ pd3

theorem CC.Denot.imply_refl (d : Denot) : d.Imply d

theorem CC.Denot.imply_trans {d1 d2 d3 : Denot} (h1 : d1.Imply d2) (h2 : d2.Imply d3) : d1.Imply d3

theorem CC.resolve_var_heap_some {heap : Heap} {x : ℕ} {v : HeapVal} (hheap : heap x = some (Cell.val v)) : resolve heap (Exp.var (Var.free x)) = some v.unwrap

theorem CC.resolve_val {heap : Heap} {v : Exp ∅} (hval : v.IsVal) : resolve heap v = some v

theorem CC.resolve_var_heap_trans {heap : Heap} {x : ℕ} {v : HeapVal} (hheap : heap x = some (Cell.val v)) : resolve heap (Exp.var (Var.free x)) = resolve heap v.unwrap

theorem CC.resolve_var_or_val {store : Heap} {e v : Exp ∅} (hv : resolve store e = some v) : (∃ (x : Var Kind.var ∅), e = Exp.var x) ∨ e = v

theorem CC.resolve_ans_to_val {store : Heap} {e v : Exp ∅} (hv : resolve store e = some v) (hans : v.IsAns) : e.IsAns

def CC.PreDenot.is_monotonic (pd : PreDenot) : Prop

Equations

• pd.is_monotonic = ∀ (C : CC.CapabilitySet), (pd C).is_monotonic

def CC.PreDenot.is_transparent (pd : PreDenot) : Prop

Equations

• pd.is_transparent = ∀ (C : CC.CapabilitySet), (pd C).is_transparent

def CC.PreDenot.is_bool_independent (pd : PreDenot) : Prop

Equations

• pd.is_bool_independent = ∀ (C : CC.CapabilitySet), (pd C).is_bool_independent

structure CC.TypeEnv.IsMonotonic {s : Sig} (env : TypeEnv s) : Prop

• tvar (X : BVar s Kind.tvar) : (env.lookup_tvar X).is_monotonic

def CC.TypeEnv.is_transparent {s : Sig} (env : TypeEnv s) : Prop

Equations

• env.is_transparent = ∀ (X : CC.BVar s CC.Kind.tvar), (env.lookup_tvar X).is_transparent

def CC.TypeEnv.is_bool_independent {s : Sig} (env : TypeEnv s) : Prop

Equations

• env.is_bool_independent = ∀ (X : CC.BVar s CC.Kind.tvar), (env.lookup_tvar X).is_bool_independent

def CC.TypeEnv.is_reachability_safe {s : Sig} (env : TypeEnv s) : Prop

Equations

• env.is_reachability_safe = ∀ (X : CC.BVar s CC.Kind.tvar), (env.lookup_tvar X).is_reachability_safe

def CC.TypeEnv.is_reachability_monotonic {s : Sig} (env : TypeEnv s) : Prop

Equations

• env.is_reachability_monotonic = ∀ (X : CC.BVar s CC.Kind.tvar), (env.lookup_tvar X).is_reachability_monotonic

def CC.TypeEnv.is_implying_wf {s : Sig} (env : TypeEnv s) : Prop

Equations

• env.is_implying_wf = ∀ (X : CC.BVar s CC.Kind.tvar), (env.lookup_tvar X).implies_wf

def CC.TypeEnv.is_tight {s : Sig} (env : TypeEnv s) : Prop

Equations

• env.is_tight = ∀ (X : CC.BVar s CC.Kind.tvar), (env.lookup_tvar X).is_tight

theorem CC.typed_env_is_monotonic {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.IsMonotonic

theorem CC.typed_env_is_transparent {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.is_transparent

theorem CC.typed_env_is_bool_independent {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.is_bool_independent

theorem CC.typed_env_is_reachability_safe {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.is_reachability_safe

theorem CC.typed_env_is_reachability_monotonic {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.is_reachability_monotonic

theorem CC.typed_env_is_implying_wf {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.is_implying_wf

theorem CC.typed_env_is_tight {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem : Memory} (ht : EnvTyping Γ env mem) : env.is_tight

theorem CC.shape_val_denot_is_transparent {s : Sig} {env : TypeEnv s} (henv : env.is_transparent) (T : Ty TySort.shape s) : (Ty.shape_val_denot env T).is_transparent

theorem CC.shape_val_denot_is_bool_independent {s : Sig} {env : TypeEnv s} (henv : env.is_bool_independent) (T : Ty TySort.shape s) (C : CapabilitySet) : (Ty.shape_val_denot env T C).is_bool_independent

theorem CC.capt_val_denot_is_transparent {s : Sig} {env : TypeEnv s} (henv : env.is_transparent) (T : Ty TySort.capt s) : (Ty.capt_val_denot env T).is_transparent

theorem CC.exi_val_denot_is_transparent {s : Sig} {env : TypeEnv s} (henv : env.is_transparent) (T : Ty TySort.exi s) : (Ty.exi_val_denot env T).is_transparent

theorem CC.ground_denot_is_monotonic {C : CaptureSet ∅} : C.ground_denot.is_monotonic_for C

theorem CC.capture_set_denot_is_monotonic {s : Sig} {ρ : TypeEnv s} {C : CaptureSet s} : (CaptureSet.denot ρ C).is_monotonic_for (C.subst (Subst.from_TypeEnv ρ))

theorem CC.capture_bound_denot_is_monotonic {s : Sig} {ρ : TypeEnv s} {m1 m2 : Memory} {B : CaptureBound s} (hwf : (B.subst (Subst.from_TypeEnv ρ)).WfInHeap m1.heap) (hsub : m2.subsumes m1) : CaptureBound.denot ρ B m1 = CaptureBound.denot ρ B m2

def CC.shape_val_denot_is_monotonic {s : Sig} {env : TypeEnv s} (henv : env.IsMonotonic) (T : Ty TySort.shape s) : (Ty.shape_val_denot env T).is_monotonic

Equations

• ⋯ = ⋯

def CC.capt_val_denot_is_monotonic {s : Sig} {env : TypeEnv s} (henv : env.IsMonotonic) (T : Ty TySort.capt s) : (Ty.capt_val_denot env T).is_monotonic

Equations

• ⋯ = ⋯

def CC.exi_val_denot_is_monotonic {s : Sig} {env : TypeEnv s} (henv : env.IsMonotonic) (T : Ty TySort.exi s) : (Ty.exi_val_denot env T).is_monotonic

Equations

• ⋯ = ⋯

def CC.capt_val_denot_is_bool_independent {s : Sig} {env : TypeEnv s} (henv : env.is_bool_independent) (T : Ty TySort.capt s) : (Ty.capt_val_denot env T).is_bool_independent

Equations

• ⋯ = ⋯

def CC.exi_val_denot_is_bool_independent {s : Sig} {env : TypeEnv s} (henv : env.is_bool_independent) (T : Ty TySort.exi s) : (Ty.exi_val_denot env T).is_bool_independent

Equations

• ⋯ = ⋯

def CC.capt_exp_denot_is_monotonic {s : Sig} {env : TypeEnv s} (henv_mono : env.IsMonotonic) (henv_bool : env.is_bool_independent) (T : Ty TySort.capt s) {C : CapabilitySet} {m1 m2 : Memory} {e : Exp ∅} : e.WfInHeap m1.heap → m2.subsumes m1 → Ty.capt_exp_denot env T C m1 e → Ty.capt_exp_denot env T C m2 e

Equations

• ⋯ = ⋯

def CC.exi_exp_denot_is_monotonic {s : Sig} {env : TypeEnv s} (henv_mono : env.IsMonotonic) (henv_bool : env.is_bool_independent) (T : Ty TySort.exi s) {C : CapabilitySet} {m1 m2 : Memory} {e : Exp ∅} : e.WfInHeap m1.heap → m2.subsumes m1 → Ty.exi_exp_denot env T C m1 e → Ty.exi_exp_denot env T C m2 e

Equations

• ⋯ = ⋯

theorem CC.env_typing_monotonic {a✝ : Sig} {Γ : Ctx a✝} {env : TypeEnv a✝} {mem1 mem2 : Memory} (ht : EnvTyping Γ env mem1) (hmem : mem2.subsumes mem1) : EnvTyping Γ env mem2

def CC.SemSubcapt {s : Sig} (Γ : Ctx s) (C1 C2 : CaptureSet s) : Prop

Semantic subcapturing.

Equations

• CC.SemSubcapt Γ C1 C2 = ∀ (env : CC.TypeEnv s) (m : CC.Memory), CC.EnvTyping Γ env m → CC.CaptureSet.denot env C1 m ⊆ CC.CaptureSet.denot env C2 m

def CC.SemSubtyp {s : Sig} {k : TySort} (Γ : Ctx s) (T1 T2 : Ty k s) : Prop

Equations

• CC.SemSubtyp Γ T1_2 T2_2 = ∀ (env : CC.TypeEnv s) (H : CC.Memory), CC.EnvTyping Γ env H → (CC.Ty.shape_val_denot env T1_2).ImplyAfter H (CC.Ty.shape_val_denot env T2_2)
• CC.SemSubtyp Γ T1_2 T2_2 = ∀ (env : CC.TypeEnv s) (H : CC.Memory), CC.EnvTyping Γ env H → (CC.Ty.capt_val_denot env T1_2).ImplyAfter H (CC.Ty.capt_val_denot env T2_2)
• CC.SemSubtyp Γ T1_2 T2_2 = ∀ (env : CC.TypeEnv s) (H : CC.Memory), CC.EnvTyping Γ env H → (CC.Ty.exi_val_denot env T1_2).ImplyAfter H (CC.Ty.exi_val_denot env T2_2)

theorem CC.shape_val_denot_is_reachability_safe {s : Sig} {env : TypeEnv s} (hts : env.is_reachability_safe) (T : Ty TySort.shape s) : (Ty.shape_val_denot env T).is_reachability_safe

theorem CC.shape_val_denot_is_reachability_monotonic {s : Sig} {env : TypeEnv s} (hts : env.is_reachability_monotonic) (T : Ty TySort.shape s) : (Ty.shape_val_denot env T).is_reachability_monotonic

theorem CC.wf_from_resolve_unit {m : Memory} {e : Exp ∅} (hresolve : resolve m.heap e = some Exp.unit) : e.WfInHeap m.heap

If the type environment is well-typed, then the denotation of any shape type is proper. A PreDenot is proper if it is reachability-safe, monotonic, and transparent. This theorem combines the reachability safety, monotonicity, and transparency results for shape type denotations.

theorem CC.shape_val_denot_implies_wf {s : Sig} {env : TypeEnv s} (hts : env.is_implying_wf) (T : Ty TySort.shape s) : (Ty.shape_val_denot env T).implies_wf

theorem CC.shape_val_denot_is_tight {s : Sig} {T : Ty TySort.shape s} {env : TypeEnv s} (hts : env.is_tight) : (Ty.shape_val_denot env T).is_tight

theorem CC.shape_val_denot_is_proper {s : Sig} {Γ : Ctx s} {m : Memory} {env : TypeEnv s} {S : Ty TySort.shape s} (hts : EnvTyping Γ env m) : (Ty.shape_val_denot env S).is_proper

theorem CC.capt_denot_implyafter_lift {a✝ : Sig} {env : TypeEnv a✝} {T1 : Ty TySort.capt a✝} {H : Memory} {T2 : Ty TySort.capt a✝} (himp : (Ty.capt_val_denot env T1).ImplyAfter H (Ty.capt_val_denot env T2)) : (Ty.capt_exp_denot env T1).ImplyAfter H (Ty.capt_exp_denot env T2)

theorem CC.exi_denot_implyafter_lift {a✝ : Sig} {env : TypeEnv a✝} {T1 : Ty TySort.exi a✝} {H : Memory} {T2 : Ty TySort.exi a✝} (himp : (Ty.exi_val_denot env T1).ImplyAfter H (Ty.exi_val_denot env T2)) : (Ty.exi_exp_denot env T1).ImplyAfter H (Ty.exi_exp_denot env T2)