inductive CC.Eval : CapabilitySet → Memory → Exp ∅ → Mpost → Prop

• eval_val {v : Exp ∅} {Q : Mpost} {C : CapabilitySet} {m : Memory} (hv : v.IsVal) (hQ : Q v m) : Eval C m v Q
• eval_var {Q : Mpost} {C : CapabilitySet} {m : Memory} {x : Var Kind.var ∅} (hQ : Q (Exp.var x) m) : Eval C m (Exp.var x) Q
• eval_apply {cs : CaptureSet ∅} {T : Ty TySort.capt ∅} {e : Exp (∅,x)} {hv : (Exp.abs cs T e).IsSimpleVal} {R C : CapabilitySet} {y : Var Kind.var ∅} {Q : Mpost} {m : Memory} {x : ℕ} : m.lookup x = some (Cell.val { unwrap := Exp.abs cs T e, isVal := hv, reachability := R }) → Eval C m (e.subst (Subst.openVar y)) Q → Eval C m (Exp.app (Var.free x) y) Q
• eval_invoke {C : CapabilitySet} {y : ℕ} {hv : Exp.unit.IsSimpleVal} {R : CapabilitySet} {Q : Mpost} {m : Memory} {x : ℕ} : x ∈ C → m.lookup x = some (Cell.capability CapabilityInfo.basic) → m.lookup y = some (Cell.val { unwrap := Exp.unit, isVal := hv, reachability := R }) → Q Exp.unit m → Eval C m (Exp.app (Var.free x) (Var.free y)) Q
• eval_tapply {cs : CaptureSet ∅} {T0 : Ty TySort.shape ∅} {e : Exp (∅,X)} {hv : (Exp.tabs cs T0 e).IsSimpleVal} {R C : CapabilitySet} {Q : Mpost} {S : Ty TySort.shape ∅} {m : Memory} {x : ℕ} : m.lookup x = some (Cell.val { unwrap := Exp.tabs cs T0 e, isVal := hv, reachability := R }) → Eval C m (e.subst (Subst.openTVar Ty.top)) Q → Eval C m (Exp.tapp (Var.free x) S) Q
• eval_capply {cs : CaptureSet ∅} {B0 : CaptureBound ∅} {e : Exp (∅,C)} {hv : (Exp.cabs cs B0 e).IsSimpleVal} {R C : CapabilitySet} {CS : CaptureSet ∅} {Q : Mpost} {m : Memory} {x : ℕ} : m.lookup x = some (Cell.val { unwrap := Exp.cabs cs B0 e, isVal := hv, reachability := R }) → Eval C m (e.subst (Subst.openCVar CS)) Q → Eval C m (Exp.capp (Var.free x) CS) Q
• eval_letin {C : CapabilitySet} {e1 : Exp ∅} {Q : Mpost} {e2 : Exp (∅,x)} {m : Memory} {Q1 : Mpost} (hpred : Q1.is_monotonic) (hbool : Q1.is_bool_independent) : Eval C m e1 Q1 → ∀ (h_nonstuck : ∀ {m1 : Memory} {v : Exp ∅}, Q1 v m1 → v.IsSimpleAns ∧ v.WfInHeap m1.heap) (h_val : ∀ {m1 : Memory} {v : Exp ∅}, m1.subsumes m → ∀ (hv : v.IsSimpleVal) (hwf_v : v.WfInHeap m1.heap), Q1 v m1 → ∀ (l' : ℕ) (hfresh : m1.lookup l' = none), Eval C (m1.extend_val l' { unwrap := v, isVal := hv, reachability := compute_reachability m1.heap v hv } hwf_v ⋯ hfresh) (e2.subst (Subst.openVar (Var.free l'))) Q) (h_var : ∀ {m1 : Memory} {x : Var Kind.var ∅}, m1.subsumes m → x.WfInHeap m1.heap → Q1 (Exp.var x) m1 → Eval C m1 (e2.subst (Subst.openVar x)) Q), Eval C m (e1.letin e2) Q
• eval_unpack {C : CapabilitySet} {e1 : Exp ∅} {Q : Mpost} {e2 : Exp (∅,C,x)} {m : Memory} {Q1 : Mpost} (hpred : Q1.is_monotonic) (hbool : Q1.is_bool_independent) : Eval C m e1 Q1 → ∀ (h_nonstuck : ∀ {m1 : Memory} {v : Exp ∅}, Q1 v m1 → v.IsPack ∧ v.WfInHeap m1.heap) (h_val : ∀ {m1 : Memory} {x : Var Kind.var ∅} {cs : CaptureSet ∅}, m1.subsumes m → x.WfInHeap m1.heap → cs.WfInHeap m1.heap → Q1 (Exp.pack cs x) m1 → Eval C m1 (e2.subst (Subst.unpack cs x)) Q), Eval C m (e1.unpack e2) Q
• eval_read {C : CapabilitySet} {Q : Mpost} {m : Memory} {x : ℕ} {b : Bool} : x ∈ C → m.lookup x = some (Cell.capability (CapabilityInfo.mcell b)) → Q (if b = true then Exp.btrue else Exp.bfalse) m → Eval C m (Exp.read (Var.free x)) Q
• eval_write_true {C : CapabilitySet} {b0 : Bool} {hv : Exp.btrue.IsSimpleVal} {R : CapabilitySet} {Q : Mpost} {m : Memory} {x y : ℕ} : x ∈ C → ∀ (hx : m.lookup x = some (Cell.capability (CapabilityInfo.mcell b0))), m.lookup y = some (Cell.val { unwrap := Exp.btrue, isVal := hv, reachability := R }) → Q Exp.unit (m.update_mcell x true ⋯) → Eval C m (Exp.write (Var.free x) (Var.free y)) Q
• eval_write_false {C : CapabilitySet} {b0 : Bool} {hv : Exp.bfalse.IsSimpleVal} {R : CapabilitySet} {Q : Mpost} {m : Memory} {x y : ℕ} : x ∈ C → ∀ (hx : m.lookup x = some (Cell.capability (CapabilityInfo.mcell b0))), m.lookup y = some (Cell.val { unwrap := Exp.bfalse, isVal := hv, reachability := R }) → Q Exp.unit (m.update_mcell x false ⋯) → Eval C m (Exp.write (Var.free x) (Var.free y)) Q
• eval_cond {C : CapabilitySet} {x : Var Kind.var ∅} {e2 : Exp ∅} {Q : Mpost} {e3 : Exp ∅} {m : Memory} {Q1 : Mpost} (hpred : Q1.is_monotonic) (hbool : Q1.is_bool_independent) : Eval C m (Exp.var x) Q1 → ∀ (h_nonstuck : ∀ {m1 : Memory} {v : Exp ∅}, Q1 v m1 → resolve m1.heap v = some Exp.btrue ∨ resolve m1.heap v = some Exp.bfalse) (h_true : ∀ {m1 : Memory} {v : Exp ∅}, m1.subsumes m → Q1 v m1 → resolve m1.heap v = some Exp.btrue → Eval C m1 e2 Q) (h_false : ∀ {m1 : Memory} {v : Exp ∅}, m1.subsumes m → Q1 v m1 → resolve m1.heap v = some Exp.bfalse → Eval C m1 e3 Q), Eval C m (Exp.cond x e2 e3) Q

theorem CC.eval_monotonic {e : Exp ∅} {C : CapabilitySet} {Q : Mpost} {m1 m2 : Memory} (hpred : Q.is_monotonic) (hbool : Q.is_bool_independent) (hsub : m2.subsumes m1) (hwf : e.WfInHeap m1.heap) (heval : Eval C m1 e Q) : Eval C m2 e Q

def CC.Mpost.entails_at (Q1 : Mpost) (m : Memory) (Q2 : Mpost) : Prop

Equations

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

def CC.Mpost.entails_after (Q1 : Mpost) (m : Memory) (Q2 : Mpost) : Prop

Equations

• Q1.entails_after m Q2 = ∀ (m' : CC.Memory), m'.subsumes m → Q1.entails_at m' Q2

theorem CC.Mpost.entails_to_entails_after {m : Memory} {Q1 Q2 : Mpost} (himp : Q1.entails Q2) : Q1.entails_after m Q2

theorem CC.Mpost.entails_after_refl (Q : Mpost) (m : Memory) : Q.entails_after m Q

theorem CC.Mpost.entails_after_subsumes {Q1 : Mpost} {m : Memory} {Q2 : Mpost} {m' : Memory} (himp : Q1.entails_after m Q2) (hsub : m'.subsumes m) : Q1.entails_after m' Q2

theorem CC.eval_post_monotonic_general {m : Memory} {C : CapabilitySet} {e : Exp ∅} {Q1 Q2 : Mpost} (himp : Q1.entails_after m Q2) (heval : Eval C m e Q1) : Eval C m e Q2

theorem CC.eval_post_monotonic {C : CapabilitySet} {m : Memory} {e : Exp ∅} {Q1 Q2 : Mpost} (himp : Q1.entails Q2) (heval : Eval C m e Q1) : Eval C m e Q2

theorem CC.eval_capability_set_monotonic {m : Memory} {e : Exp ∅} {Q : Mpost} {A1 A2 : CapabilitySet} (heval : Eval A1 m e Q) (hsub : A1 ⊆ A2) : Eval A2 m e Q