theorem
CC.step_val_absurd
{v : Exp ∅}
{C : CapabilitySet}
{m m' : Memory}
{e' : Exp ∅}
(hv : v.IsSimpleVal)
(hstep : Step C m v m' e')
:
theorem
CC.reduce_letin_inv
{C : CapabilitySet}
{m : Memory}
{e1 : Exp ∅}
{e2 : Exp (∅,x)}
{m' : Memory}
{a : Exp ∅}
(hred : Reduce C m (e1.letin e2) m' a)
(hans : a.IsAns)
:
(∃ (C1 : CapabilitySet) (C2 : CapabilitySet) (m0 : Memory) (y0 : ℕ),
C1 ∪ C2 ≈ C ∧ Reduce C1 m e1 m0 (Exp.var (Var.free y0)) ∧ Reduce C2 m0 (e2.subst (Subst.openVar (Var.free y0))) m' a) ∨ ∃ (C1 : CapabilitySet) (C2 : CapabilitySet) (m0 : Memory) (v0 : Exp ∅) (hv : v0.IsSimpleVal) (hwf :
v0.WfInHeap m0.heap) (l0 : ℕ) (hfresh : m0.heap l0 = none),
C1 ∪ C2 ≈ C ∧ Reduce C1 m e1 m0 v0 ∧ Reduce C2
(m0.extend l0 { unwrap := v0, isVal := hv, reachability := compute_reachability m0.heap v0 hv } hwf ⋯ hfresh)
(e2.subst (Subst.openVar (Var.free l0))) m' a
Inversion lemma for letin reduction with precise capability tracking. The capability set C is precisely the union of capabilities used in each sub-reduction.
theorem
CC.reduce_unpack_inv
{C : CapabilitySet}
{m : Memory}
{e1 : Exp ∅}
{e2 : Exp (∅,C,x)}
{m' : Memory}
{a : Exp ∅}
(hred : Reduce C m (e1.unpack e2) m' a)
(hans : a.IsAns)
:
∃ (C1 : CapabilitySet) (C2 : CapabilitySet) (m0 : Memory) (cs : CaptureSet ∅) (x : ℕ),
C1 ∪ C2 ≈ C ∧ Reduce C1 m e1 m0 (Exp.pack cs (Var.free x)) ∧ Reduce C2 m0 (e2.subst (Subst.unpack cs (Var.free x))) m' a
Inversion lemma for reduction of unpack expressions with precise capability tracking.
- done {R : CapabilitySet} {m : Memory} {e : Exp ∅} : e.IsAns → IsProgressive R m e
- step {C' : CapabilitySet} {m : Memory} {e : Exp ∅} {m' : Memory} {e' : Exp ∅} {C : CapabilitySet} : Step C' m e m' e' → C' ⊆ C → IsProgressive C m e
Instances For
theorem
CC.eval_ans_holds_post
{C : CapabilitySet}
{m : Memory}
{e : Exp ∅}
{Q : Mpost}
(heval : Eval C m e Q)
(hans : e.IsAns)
:
Q e m
If an answer has an evaluation, then the postcondition holds for it.
theorem
CC.eval_implies_progressive
{C : CapabilitySet}
{m : Memory}
{e : Exp ∅}
{Q : Mpost}
(heval : Eval C m e Q)
:
IsProgressive C m e
theorem
CC.step_preserves_eval
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{Q : Mpost}
{C' : CapabilitySet}
{m2 : Memory}
{e2 : Exp ∅}
(he : Eval C m1 e1 Q)
(hstep : Step C' m1 e1 m2 e2)
(hsub : C' ⊆ C)
:
Eval C m2 e2 Q
theorem
CC.reduce_preserves_eval
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{Q : Mpost}
{C' : CapabilitySet}
{m2 : Memory}
{e2 : Exp ∅}
(he : Eval C m1 e1 Q)
(hred : Reduce C' m1 e1 m2 e2)
(hsub : C' ⊆ C)
:
Eval C m2 e2 Q
Reduction preserves evaluation when the reduction uses a subset of available capabilities.
theorem
CC.eval_to_reduce
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{Q : Mpost}
{C' : CapabilitySet}
(heval : Eval C m1 e1 Q)
(hsub : C' ⊆ C)
(m2 : Memory)
(e2 : Exp ∅)
:
theorem
CC.CaptureSet.wf_masked
{a✝ : Sig}
{cs : CaptureSet a✝}
{H : Heap}
{D : Finset ℕ}
(hwf : cs.WfInHeap H)
:
theorem
CC.CaptureBound.wf_masked
{a✝ : Sig}
{cb : CaptureBound a✝}
{H : Heap}
{D : Finset ℕ}
(hwf : cb.WfInHeap H)
:
theorem
CC.masked_lookup_cap
{m : Memory}
{M : Finset ℕ}
{l : ℕ}
{info : CapabilityInfo}
:
m.lookup l = some (Cell.capability info) → l ∈ M → (m.masked_caps M).lookup l = some (Cell.capability info)
theorem
CC.Heap.masked_update_mcell_comm
{H : Heap}
{l : ℕ}
{b : Bool}
{M : Finset ℕ}
(hmem : l ∈ M)
:
(H.update_cell l (Cell.capability (CapabilityInfo.mcell b))).mask_caps M = (H.mask_caps M).update_cell l (Cell.capability (CapabilityInfo.mcell b))
Helper lemma: Heap masking and update_cell commute when the location is in the mask.
theorem
CC.Memory.masked_update_mcell_comm
{m : Memory}
{l : ℕ}
{b : Bool}
{M : Finset ℕ}
(hexists : ∃ (b0 : Bool), m.heap l = some (Cell.capability (CapabilityInfo.mcell b0)))
(hmem : l ∈ M)
:
Helper lemma: Memory masking and update_mcell commute when the location is in the mask.
theorem
CC.step_masked
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{m2 : Memory}
{e2 : Exp ∅}
(hstep : Step C m1 e1 m2 e2)
:
have M := C.to_finset;
Step C (m1.masked_caps M) e1 (m2.masked_caps M) e2
theorem
CC.step_masked_superset
{C1 : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{m2 : Memory}
{e2 : Exp ∅}
{C : CapabilitySet}
(hstep : Step C1 m1 e1 m2 e2)
(hsub : C1 ⊆ C)
:
Step C1 (m1.masked_caps C.to_finset) e1 (m2.masked_caps C.to_finset) e2
theorem
CC.reduce_masked_superset
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{m2 : Memory}
{e2 : Exp ∅}
{C' : CapabilitySet}
(hred : Reduce C m1 e1 m2 e2)
(hsub : C ⊆ C')
:
Reduce C (m1.masked_caps C'.to_finset) e1 (m2.masked_caps C'.to_finset) e2
theorem
CC.reduce_masked
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{m2 : Memory}
{e2 : Exp ∅}
(hred : Reduce C m1 e1 m2 e2)
:
have M := C.to_finset;
Reduce C (m1.masked_caps M) e1 (m2.masked_caps M) e2
theorem
CC.eval_exists_answer
{C : CapabilitySet}
{m : Memory}
{e : Exp ∅}
{Q : Mpost}
(heval : Eval C m e Q)
:
If Eval C m e Q holds, then there exist m' and e' such that e' is an answer, the memory m' subsumes m, and Q e' m' holds.
theorem
CC.eval_reduce_exists_answer
{C : CapabilitySet}
{m1 : Memory}
{e1 : Exp ∅}
{Q : Mpost}
(heval : Eval C m1 e1 Q)
:
If Eval C m1 e1 Q holds, then there exist C' ⊆ C, m2 and e2 such that e1 reduces to e2 (an answer) using capabilities C', and Q e2 m2 holds.
theorem
CC.eval_bounds_step_capability
{C : CapabilitySet}
{m : Memory}
{e : Exp ∅}
{Q : Mpost}
{C' : CapabilitySet}
{m' : Memory}
{e' : Exp ∅}
(heval : Eval C m e Q)
(hred : Step C' m e m' e')
:
theorem
CC.eval_bounds_reduce_capability
{C : CapabilitySet}
{m : Memory}
{e : Exp ∅}
{Q : Mpost}
{C' : CapabilitySet}
{m' : Memory}
{e' : Exp ∅}
(heval : Eval C m e Q)
(hred : Reduce C' m e m' e')
: