inductive CC.Step : CapabilitySet → Memory → Exp ∅ → Memory → Exp ∅ → Prop

Small-step evaluation relation indexed by a precise capability set. Step C m e m' e' means that expression e in memory m steps to e' in memory m' using exactly the capabilities in C.

• step_apply {m : Memory} {x y : ℕ} {cs : CaptureSet ∅} {T : Ty TySort.capt ∅} {e : Exp (∅,x)} {hv : (Exp.abs cs T e).IsSimpleVal} {R : CapabilitySet} : m.lookup x = some (Cell.val { unwrap := Exp.abs cs T e, isVal := hv, reachability := R }) → Step ∅ m (Exp.app (Var.free x) (Var.free y)) m (e.subst (Subst.openVar (Var.free y)))
• step_invoke {x : ℕ} {m : Memory} {y : ℕ} {hv : Exp.unit.IsSimpleVal} {R : CapabilitySet} : m.lookup x = some (Cell.capability CapabilityInfo.basic) → m.lookup y = some (Cell.val { unwrap := Exp.unit, isVal := hv, reachability := R }) → Step (CapabilitySet.cap x) m (Exp.app (Var.free x) (Var.free y)) m Exp.unit
• step_tapply {m : Memory} {x : ℕ} {S : Ty TySort.shape ∅} {cs : CaptureSet ∅} {S' : Ty TySort.shape ∅} {e : Exp (∅,X)} {hv : (Exp.tabs cs S' e).IsSimpleVal} {R : CapabilitySet} : m.lookup x = some (Cell.val { unwrap := Exp.tabs cs S' e, isVal := hv, reachability := R }) → Step ∅ m (Exp.tapp (Var.free x) S) m (e.subst (Subst.openTVar Ty.top))
• step_capply {m : Memory} {x : ℕ} {CS cs : CaptureSet ∅} {B : CaptureBound ∅} {e : Exp (∅,C)} {hv : (Exp.cabs cs B e).IsSimpleVal} {R : CapabilitySet} : m.lookup x = some (Cell.val { unwrap := Exp.cabs cs B e, isVal := hv, reachability := R }) → Step ∅ m (Exp.capp (Var.free x) CS) m (e.subst (Subst.openCVar CS))
• step_cond_var_true {m : Memory} {x : ℕ} {e1 e2 : Exp ∅} {hv : Exp.btrue.IsSimpleVal} {R : CapabilitySet} : m.lookup x = some (Cell.val { unwrap := Exp.btrue, isVal := hv, reachability := R }) → Step ∅ m (Exp.cond (Var.free x) e1 e2) m e1
• step_cond_var_false {m : Memory} {x : ℕ} {e1 e2 : Exp ∅} {hv : Exp.bfalse.IsSimpleVal} {R : CapabilitySet} : m.lookup x = some (Cell.val { unwrap := Exp.bfalse, isVal := hv, reachability := R }) → Step ∅ m (Exp.cond (Var.free x) e1 e2) m e2
• step_read {x : ℕ} {m : Memory} {b : Bool} : m.lookup x = some (Cell.capability (CapabilityInfo.mcell b)) → Step (CapabilitySet.cap x) m (Exp.read (Var.free x)) m (if b = true then Exp.btrue else Exp.bfalse)
• step_write_true {x : ℕ} {m : Memory} {y : ℕ} {b0 : Bool} {hv : Exp.btrue.IsSimpleVal} {R : CapabilitySet} (hx : m.lookup x = some (Cell.capability (CapabilityInfo.mcell b0))) : m.lookup y = some (Cell.val { unwrap := Exp.btrue, isVal := hv, reachability := R }) → Step (CapabilitySet.cap x) m (Exp.write (Var.free x) (Var.free y)) (m.update_mcell x true ⋯) Exp.unit
• step_write_false {x : ℕ} {m : Memory} {y : ℕ} {b0 : Bool} {hv : Exp.bfalse.IsSimpleVal} {R : CapabilitySet} (hx : m.lookup x = some (Cell.capability (CapabilityInfo.mcell b0))) : m.lookup y = some (Cell.val { unwrap := Exp.bfalse, isVal := hv, reachability := R }) → Step (CapabilitySet.cap x) m (Exp.write (Var.free x) (Var.free y)) (m.update_mcell x false ⋯) Exp.unit
• step_ctx_letin {C : CapabilitySet} {m : Memory} {e1 : Exp ∅} {m' : Memory} {e1' : Exp ∅} {e2 : Exp (∅,x)} : Step C m e1 m' e1' → Step C m (e1.letin e2) m' (e1'.letin e2)
• step_ctx_unpack {C : CapabilitySet} {m : Memory} {e1 : Exp ∅} {m' : Memory} {e1' : Exp ∅} {e2 : Exp (∅,C,x)} : Step C m e1 m' e1' → Step C m (e1.unpack e2) m' (e1'.unpack e2)
• step_rename {m : Memory} {y : ℕ} {e : Exp (∅,x)} : Step ∅ m ((Exp.var (Var.free y)).letin e) m (e.subst (Subst.openVar (Var.free y)))
• step_lift {v : Exp ∅} {m : Memory} {e : Exp (∅,x)} {l : ℕ} (hv : v.IsSimpleVal) (hwf : v.WfInHeap m.heap) (hfresh : m.heap l = none) : Step ∅ m (v.letin e) (m.extend l { unwrap := v, isVal := hv, reachability := compute_reachability m.heap v hv } hwf ⋯ hfresh) (e.subst (Subst.openVar (Var.free l)))
• step_unpack {m : Memory} {cs : CaptureSet ∅} {x : ℕ} {e : Exp (∅,C,x)} : Step ∅ m ((Exp.pack cs (Var.free x)).unpack e) m (e.subst (Subst.unpack cs (Var.free x)))

inductive CC.Reduce : CapabilitySet → Memory → Exp ∅ → Memory → Exp ∅ → Prop

Multi-step reduction relation: reflexive-transitive closure of Step. Reduce C m e m' e' means that e in memory m takes multiple steps to e' in memory m' using exactly the capabilities in C (union of all step capabilities).

Note: The capability set is precise - it's exactly what was used. Due to union not being definitionally associative, we define an equivalence-respecting version of transitivity.

• refl {m : Memory} {e : Exp ∅} : Reduce ∅ m e m e
• step {C1 : CapabilitySet} {m1 : Memory} {e1 : Exp ∅} {m2 : Memory} {e2 : Exp ∅} {C2 : CapabilitySet} {m3 : Memory} {e3 : Exp ∅} : Step C1 m1 e1 m2 e2 → Reduce C2 m2 e2 m3 e3 → Reduce (C1 ∪ C2) m1 e1 m3 e3

theorem CC.reduce_trans {C1 : CapabilitySet} {m1 : Memory} {e1 : Exp ∅} {m2 : Memory} {e2 : Exp ∅} {C2 : CapabilitySet} {m3 : Memory} {e3 : Exp ∅} (hred1 : Reduce C1 m1 e1 m2 e2) (hred2 : Reduce C2 m2 e2 m3 e3) : ∃ (C : CapabilitySet), C ≈ C1 ∪ C2 ∧ Reduce C m1 e1 m3 e3