State-separating cell references #
Heap Ident stores typed cells at stable identifiers. CellRef Ident packages
one identifier as a typed reference, so heap programs can say explicitly which
cell they read or write.
The main purpose of this file is frame reasoning. A program that writes only a
known footprint preserves every cell outside that footprint, and the same idea
lifts from deterministic state programs to support-based effectful programs and
to oracle handlers interpreted by simulateQ.
The file is organized around four small layers:
Cell references #
A capability naming one typed cell in a Heap Ident. The value type of
the reference is dependent: r.Value = CellSpec.type r.id.
- id : Ident
The underlying heap cell identifier.
Instances For
def
VCVio.StateSeparating.CellRef.set
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
(r : CellRef Ident)
(h : Heap Ident)
(x : r.Value)
:
Heap Ident
Write a referenced cell in a heap.
Instances For
Deterministic state operations #
def
VCVio.StateSeparating.CellRef.write
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
(r : CellRef Ident)
(x : r.Value)
:
StateT (Heap Ident) Id PUnit.{max (u + 1) (v + 1)}
Deterministically write a referenced cell.
Instances For
Effectful state operations #
def
VCVio.StateSeparating.CellRef.readM
{Ident : Type u}
[CellSpec Ident]
(r : CellRef Ident)
{m : Type (max u v) → Type u_1}
[Monad m]
:
Effectfully read a referenced cell. This is the monadic version of
CellRef.read: it works in any ambient monad, not just Id.
Instances For
def
VCVio.StateSeparating.CellRef.writeM
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
(r : CellRef Ident)
(x : r.Value)
{m : Type (max u v) → Type u_1}
[Monad m]
:
StateT (Heap Ident) m PUnit.{max (u + 1) (v + 1)}
Effectfully write a referenced cell. This is the monadic version of
CellRef.write: it updates only the selected heap cell and performs no other
ambient effects.
Instances For
Support-based frame predicates #
def
VCVio.StateSeparating.CellRef.SupportPreserves
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(c : StateT (Heap Ident) m α)
(r : CellRef Ident)
:
An effectful heap program preserves a cell reference when every
support-reachable final heap has the same value at that reference as the
initial heap. This is the right generalization of Preserves beyond Id:
for probabilistic/oracle computations there may be many possible final states.
Instances For
def
VCVio.StateSeparating.CellRef.SupportWritesOnly
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(c : StateT (Heap Ident) m α)
(writes : Set Ident)
:
An effectful heap program writes only a set of identifiers when every cell outside the set is support-preserved.
Instances For
theorem
VCVio.StateSeparating.CellRef.supportWritesOnly_mono
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{writes₁ writes₂ : Set Ident}
(hc : SupportWritesOnly c writes₁)
(hsubset : writes₁ ⊆ writes₂)
:
SupportWritesOnly c writes₂
theorem
VCVio.StateSeparating.CellRef.supportPreserves_pure
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(x : α)
(r : CellRef Ident)
:
SupportPreserves (pure x) r
theorem
VCVio.StateSeparating.CellRef.supportWritesOnly_pure_empty
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(x : α)
:
SupportWritesOnly (pure x) ∅
theorem
VCVio.StateSeparating.CellRef.supportPreserves_readM
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
(r s : CellRef Ident)
:
theorem
VCVio.StateSeparating.CellRef.readM_supportWritesOnly_empty
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
(r : CellRef Ident)
:
theorem
VCVio.StateSeparating.CellRef.supportPreserves_bind
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α β : Type (max u v)}
{c : StateT (Heap Ident) m α}
{k : α → StateT (Heap Ident) m β}
{r : CellRef Ident}
(hc : SupportPreserves c r)
(hk : ∀ (a : α), SupportPreserves (k a) r)
:
SupportPreserves (c >>= k) r
theorem
VCVio.StateSeparating.CellRef.writeM_supportWritesOnly_single
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
(r : CellRef Ident)
(x : r.Value)
:
SupportWritesOnly (r.writeM x) {r.id}
theorem
VCVio.StateSeparating.CellRef.supportWritesOnly_bind
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α β : Type (max u v)}
{c : StateT (Heap Ident) m α}
{k : α → StateT (Heap Ident) m β}
{writes₁ writes₂ : Set Ident}
(hc : SupportWritesOnly c writes₁)
(hk : ∀ (a : α), SupportWritesOnly (k a) writes₂)
:
SupportWritesOnly (c >>= k) (writes₁ ∪ writes₂)
theorem
VCVio.StateSeparating.CellRef.supportWritesOnly_bind_dep
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α β : Type (max u v)}
{c : StateT (Heap Ident) m α}
{k : α → StateT (Heap Ident) m β}
{writes₁ : Set Ident}
{writes₂ : α → Set Ident}
(hc : SupportWritesOnly c writes₁)
(hk : ∀ (a : α), SupportWritesOnly (k a) (writes₂ a))
:
Dependent effectful bind form: the continuation's write set may depend on the first result.
structure
VCVio.StateSeparating.CellRef.SupportWriteFootprint
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(c : StateT (Heap Ident) m α)
:
Type u
A support-based write footprint packages a program with the set of cells it may write and the proof that every other cell is preserved.
- writes : Set Ident
Cells that the effectful program may write.
- sound : SupportWritesOnly c self.writes
Soundness: every cell outside
writesis support-framed through.
Instances For
theorem
VCVio.StateSeparating.CellRef.SupportWriteFootprint.preserves
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
(footprint : SupportWriteFootprint c)
(r : CellRef Ident)
(hr : r.id ∉ footprint.writes)
:
SupportPreserves c r
def
VCVio.StateSeparating.CellRef.SupportWriteFootprint.pure
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(x : α)
:
Instances For
def
VCVio.StateSeparating.CellRef.SupportWriteFootprint.readM
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
(r : CellRef Ident)
:
Instances For
def
VCVio.StateSeparating.CellRef.SupportWriteFootprint.writeM
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
[DecidableEq Ident]
(r : CellRef Ident)
(x : r.Value)
:
SupportWriteFootprint (r.writeM x)
Instances For
def
VCVio.StateSeparating.CellRef.SupportWriteFootprint.bind
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α β : Type (max u v)}
{c : StateT (Heap Ident) m α}
{k : α → StateT (Heap Ident) m β}
(footprint : SupportWriteFootprint c)
(kont : (a : α) → SupportWriteFootprint (k a))
:
SupportWriteFootprint (c >>= k)
Instances For
Probability corollaries for cell frames #
theorem
VCVio.StateSeparating.CellRef.SupportPreserves.prob_changed_eq_zero
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreserves c r)
(h : Heap Ident)
:
A support-level frame implies that the cell-change event has probability zero. This is the probability-facing corollary most proofs want after a generic frame theorem has done the support-level work.
theorem
VCVio.StateSeparating.CellRef.SupportPreserves.prob_unchanged_eq_sub_probFailure
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreserves c r)
(h : Heap Ident)
:
If a cell is support-preserved, then the probability of reading the initial value at the end is exactly one minus the failure probability.
theorem
VCVio.StateSeparating.CellRef.SupportPreserves.prob_unchanged_eq_one_of_probFailure_eq_zero
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreserves c r)
(h : Heap Ident)
(hnf : Pr[⊥ | c.run h] = 0)
:
Failure-free specialization of prob_unchanged_eq_sub_probFailure.
theorem
VCVio.StateSeparating.CellRef.SupportPreserves.prob_unchanged_eq_one
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_2}
[Monad m]
[HasEvalPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreserves c r)
(h : Heap Ident)
:
If the ambient monad has total probability semantics, support preservation gives probability-one preservation directly.
theorem
VCVio.StateSeparating.CellRef.SupportPreserves.prob_final_eq_eq_zero_of_ne
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreserves c r)
(h : Heap Ident)
{x : r.Value}
(hne : x ≠ r.get h)
:
If the initial cell value is not x, then a support-preserved cell has
final value x with probability zero.
theorem
VCVio.StateSeparating.CellRef.SupportWritesOnly.prob_changed_eq_zero
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{writes : Set Ident}
(hc : SupportWritesOnly c writes)
(r : CellRef Ident)
(hr : r.id ∉ writes)
(h : Heap Ident)
:
theorem
VCVio.StateSeparating.CellRef.SupportWritesOnly.prob_unchanged_eq_sub_probFailure
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{writes : Set Ident}
(hc : SupportWritesOnly c writes)
(r : CellRef Ident)
(hr : r.id ∉ writes)
(h : Heap Ident)
:
theorem
VCVio.StateSeparating.CellRef.SupportWritesOnly.prob_final_eq_eq_zero_of_ne
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{writes : Set Ident}
(hc : SupportWritesOnly c writes)
(r : CellRef Ident)
(hr : r.id ∉ writes)
(h : Heap Ident)
{x : r.Value}
(hne : x ≠ r.get h)
:
Preservation except an event #
def
VCVio.StateSeparating.CellRef.SupportPreservesExcept
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(c : StateT (Heap Ident) m α)
(r : CellRef Ident)
(event : Heap Ident → α × Heap Ident → Prop)
:
A computation preserves a cell except on an event when every support-reachable outcome outside that event has the initial cell value. The event may depend on the initial heap.
Instances For
theorem
VCVio.StateSeparating.CellRef.SupportPreservesExcept.of_supportPreserves
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{event : Heap Ident → α × Heap Ident → Prop}
(hc : SupportPreserves c r)
:
SupportPreservesExcept c r event
theorem
VCVio.StateSeparating.CellRef.SupportPreservesExcept.mono_event
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{event : Heap Ident → α × Heap Ident → Prop}
(hc : SupportPreservesExcept c r event)
{event' : Heap Ident → α × Heap Ident → Prop}
(hsubset : ∀ (h : Heap Ident) (z : α × Heap Ident), event h z → event' h z)
:
SupportPreservesExcept c r event'
theorem
VCVio.StateSeparating.CellRef.SupportPreservesExcept.supportPreserves_of_false_event
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreservesExcept c r fun (x : Heap Ident) (x_1 : α × Heap Ident) => False)
:
SupportPreserves c r
theorem
VCVio.StateSeparating.CellRef.SupportPreservesExcept.prob_changed_le_prob_event
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{event : Heap Ident → α × Heap Ident → Prop}
(hc : SupportPreservesExcept c r event)
(h : Heap Ident)
:
If a cell can change only when event occurs, then the change probability
is bounded by the event probability.
theorem
VCVio.StateSeparating.CellRef.SupportPreservesExcept.prob_changed_eq_zero_of_prob_event_eq_zero
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{event : Heap Ident → α × Heap Ident → Prop}
(hc : SupportPreservesExcept c r event)
(h : Heap Ident)
(hevent : (probEvent (c.run h) fun (z : α × Heap Ident) => event h z) = 0)
:
theorem
VCVio.StateSeparating.CellRef.SupportPreservesExcept.prob_changed_le_of_prob_event_le
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{event : Heap Ident → α × Heap Ident → Prop}
(hc : SupportPreservesExcept c r event)
(h : Heap Ident)
{ε : ENNReal}
(hevent : (probEvent (c.run h) fun (z : α × Heap Ident) => event h z) ≤ ε)
:
Relational and measured cell effects #
def
VCVio.StateSeparating.CellRef.SupportCellRel
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(c : StateT (Heap Ident) m α)
(r : CellRef Ident)
(rel : r.Value → r.Value → Prop)
:
A support-level relation between the initial and final value of one cell.
This is the general qualitative layer underneath preservation (rel := Eq) and
monotonicity/growth assertions.
Instances For
theorem
VCVio.StateSeparating.CellRef.SupportCellRel.of_supportPreserves
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportPreserves c r)
:
SupportCellRel c r Eq
theorem
VCVio.StateSeparating.CellRef.SupportCellRel.supportPreserves_of_eq
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
(hc : SupportCellRel c r Eq)
:
SupportPreserves c r
theorem
VCVio.StateSeparating.CellRef.SupportCellRel.bind
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α β : Type (max u v)}
{c : StateT (Heap Ident) m α}
{k : α → StateT (Heap Ident) m β}
{r : CellRef Ident}
{rel : r.Value → r.Value → Prop}
(hc : SupportCellRel c r rel)
(hk : ∀ (a : α), SupportCellRel (k a) r rel)
(htrans : ∀ (x y z : r.Value), rel x y → rel y z → rel x z)
:
SupportCellRel (c >>= k) r rel
theorem
VCVio.StateSeparating.CellRef.SupportCellRel.prob_violate_eq_zero
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{rel : r.Value → r.Value → Prop}
(hc : SupportCellRel c r rel)
(h : Heap Ident)
:
A support-level cell relation makes violations of the relation a probability-zero event.
def
VCVio.StateSeparating.CellRef.SupportMeasureBound
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
(c : StateT (Heap Ident) m α)
(r : CellRef Ident)
(measure : r.Value → ℕ)
(δ : ℕ)
:
A measured cell bound says a numeric measure of a cell can increase by at
most δ on every support-reachable execution path. Binds compose by adding
their deltas.
Instances For
theorem
VCVio.StateSeparating.CellRef.SupportMeasureBound.of_supportPreserves
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{measure : r.Value → ℕ}
(hc : SupportPreserves c r)
:
SupportMeasureBound c r measure 0
theorem
VCVio.StateSeparating.CellRef.SupportMeasureBound.mono_delta
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{measure : r.Value → ℕ}
{δ₁ δ₂ : ℕ}
(hc : SupportMeasureBound c r measure δ₁)
(hle : δ₁ ≤ δ₂)
:
SupportMeasureBound c r measure δ₂
theorem
VCVio.StateSeparating.CellRef.SupportMeasureBound.bind
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSet m]
{α β : Type (max u v)}
{c : StateT (Heap Ident) m α}
{k : α → StateT (Heap Ident) m β}
{r : CellRef Ident}
{measure : r.Value → ℕ}
{δ₁ δ₂ : ℕ}
(hc : SupportMeasureBound c r measure δ₁)
(hk : ∀ (a : α), SupportMeasureBound (k a) r measure δ₂)
:
SupportMeasureBound (c >>= k) r measure (δ₁ + δ₂)
theorem
VCVio.StateSeparating.CellRef.SupportMeasureBound.prob_exceeds_eq_zero
{Ident : Type u}
[CellSpec Ident]
{m : Type (max u v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{α : Type (max u v)}
{c : StateT (Heap Ident) m α}
{r : CellRef Ident}
{measure : r.Value → ℕ}
{δ : ℕ}
(hc : SupportMeasureBound c r measure δ)
(h : Heap Ident)
:
A measured support bound gives probability zero to exceeding the bound.
Deterministic specialization #
def
VCVio.StateSeparating.CellRef.Preserves
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
(c : StateT (Heap Ident) Id α)
(r : CellRef Ident)
:
A deterministic heap program preserves a cell reference when the final heap has the same value at that reference as the initial heap.
This exact Id-specific predicate is equivalent to SupportPreserves, whose
support contains exactly the single deterministic output. The exact form keeps
deterministic examples pleasant to use, while the combinator proofs below are
derived from the generic support-based API.
Instances For
theorem
VCVio.StateSeparating.CellRef.supportWritesOnly_of_writesOnly
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
{c : StateT (Heap Ident) Id α}
{writes : Set Ident}
(hc : WritesOnly c writes)
:
SupportWritesOnly c writes
theorem
VCVio.StateSeparating.CellRef.writesOnly_of_supportWritesOnly
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
{c : StateT (Heap Ident) Id α}
{writes : Set Ident}
(hc : SupportWritesOnly c writes)
:
WritesOnly c writes
theorem
VCVio.StateSeparating.CellRef.writesOnly_mono
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
{c : StateT (Heap Ident) Id α}
{writes₁ writes₂ : Set Ident}
(hc : WritesOnly c writes₁)
(hsubset : writes₁ ⊆ writes₂)
:
WritesOnly c writes₂
theorem
VCVio.StateSeparating.CellRef.read_writesOnly_empty
{Ident : Type u}
[CellSpec Ident]
(r : CellRef Ident)
:
WritesOnly r.read ∅
theorem
VCVio.StateSeparating.CellRef.write_writesOnly_single
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
(r : CellRef Ident)
(x : r.Value)
:
WritesOnly (r.write x) {r.id}
theorem
VCVio.StateSeparating.CellRef.writesOnly_bind
{Ident : Type u}
[CellSpec Ident]
{α β : Type (max u v)}
{c : StateT (Heap Ident) Id α}
{k : α → StateT (Heap Ident) Id β}
{writes₁ writes₂ : Set Ident}
(hc : WritesOnly c writes₁)
(hk : ∀ (a : α), WritesOnly (k a) writes₂)
:
WritesOnly (c >>= k) (writes₁ ∪ writes₂)
theorem
VCVio.StateSeparating.CellRef.writesOnly_bind_dep
{Ident : Type u}
[CellSpec Ident]
{α β : Type (max u v)}
{c : StateT (Heap Ident) Id α}
{k : α → StateT (Heap Ident) Id β}
{writes₁ : Set Ident}
{writes₂ : α → Set Ident}
(hc : WritesOnly c writes₁)
(hk : ∀ (a : α), WritesOnly (k a) (writes₂ a))
:
Dependent bind form: the continuation's write set may depend on the first result. The resulting write set is the union of the first write set and all possible continuation write sets.
Read agreement and result-dependence footprints #
def
VCVio.StateSeparating.CellRef.ResultDependsOnly
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
(c : StateT (Heap Ident) Id α)
(reads : Set Ident)
:
A deterministic heap program's result depends only on a set of cells when heaps agreeing on those cells produce equal return values. This intentionally tracks only the returned value, not the final heap.
Instances For
theorem
VCVio.StateSeparating.CellRef.resultDependsOnly_pure
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
(x : α)
:
ResultDependsOnly (pure x) ∅
theorem
VCVio.StateSeparating.CellRef.resultDependsOnly_read
{Ident : Type u}
[CellSpec Ident]
(r : CellRef Ident)
:
theorem
VCVio.StateSeparating.CellRef.resultDependsOnly_write
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
(r : CellRef Ident)
(x : r.Value)
:
ResultDependsOnly (r.write x) ∅
Compositional write footprints #
structure
VCVio.StateSeparating.CellRef.WriteFootprint
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
(c : StateT (Heap Ident) Id α)
:
Type u
A compositional write footprint packages a deterministic heap program with the set of cells it may write and the proof that all other cells are preserved.
- writes : Set Ident
Cells that the program may write.
- sound : WritesOnly c self.writes
Soundness: every cell outside
writesis framed through.
Instances For
def
VCVio.StateSeparating.CellRef.WriteFootprint.pure
{Ident : Type u}
[CellSpec Ident]
{α : Type (max u v)}
(x : α)
:
Instances For
def
VCVio.StateSeparating.CellRef.WriteFootprint.read
{Ident : Type u}
[CellSpec Ident]
(r : CellRef Ident)
:
Instances For
def
VCVio.StateSeparating.CellRef.WriteFootprint.write
{Ident : Type u}
[CellSpec Ident]
[DecidableEq Ident]
(r : CellRef Ident)
(x : r.Value)
:
WriteFootprint (r.write x)
Instances For
def
VCVio.StateSeparating.CellRef.WriteFootprint.bind
{Ident : Type u}
[CellSpec Ident]
{α β : Type (max u v)}
{c : StateT (Heap Ident) Id α}
{k : α → StateT (Heap Ident) Id β}
(footprint : WriteFootprint c)
(kont : (a : α) → WriteFootprint (k a))
:
WriteFootprint (c >>= k)
Instances For
Query-implementation cell frames #
def
VCVio.StateSeparating.QueryImpl.PreservesCell
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSet m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(r : CellRef Ident₀)
:
A QueryImpl preserves a heap cell when each single query step leaves
that cell unchanged on every support-reachable post-state. This is the
support-level analogue of CellRef.Preserves for probabilistic handlers.
Instances For
def
VCVio.StateSeparating.QueryImpl.WritesOnlyCells
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSet m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(writes : spec.Domain → Set Ident₀)
:
A QueryImpl writes only the cells named by a per-query footprint when
each query step support-preserves every cell outside its footprint.
Instances For
theorem
VCVio.StateSeparating.QueryImpl.writesOnlyCells_mono
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSet m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
{writes₁ writes₂ : spec.Domain → Set Ident₀}
(himpl : WritesOnlyCells impl writes₁)
(hsubset : ∀ (t : spec.Domain), writes₁ t ⊆ writes₂ t)
:
WritesOnlyCells impl writes₂
theorem
VCVio.StateSeparating.QueryImpl.preservesCell_of_writesOnlyCells
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSet m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
{writes : spec.Domain → Set Ident₀}
{r : CellRef Ident₀}
(himpl : WritesOnlyCells impl writes)
(hr : ∀ (t : spec.Domain), r.id ∉ writes t)
:
PreservesCell impl r
structure
VCVio.StateSeparating.QueryImpl.CellWriteFootprint
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSet m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
:
Type (max uι u₀)
A compositional cell-write footprint for a whole query implementation: every domain element gets a set of cells it may write, plus a support-level proof that no other cells change.
Per-query cells that may be written by the handler branch.
- sound : WritesOnlyCells impl self.writes
Soundness of the footprint.
Instances For
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.preservesCell
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSet m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
:
PreservesCell impl r
theorem
VCVio.StateSeparating.OracleComp.simulateQ_run_cellPreserved
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[LawfulMonad m]
[HasEvalSet m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(r : CellRef Ident₀)
(himpl : QueryImpl.PreservesCell impl r)
(A : OracleComp spec α)
(h : Heap Ident₀)
(z : α × Heap Ident₀)
:
If every handler query preserves a cell, then interpreting any
OracleComp through that handler preserves the cell.
theorem
VCVio.StateSeparating.QueryImpl.PreservesCell.prob_changed_eq_zero
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
{r : CellRef Ident₀}
(himpl : PreservesCell impl r)
(t : spec.Domain)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.QueryImpl.PreservesCell.prob_unchanged_eq_sub_probFailure
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
{r : CellRef Ident₀}
(himpl : PreservesCell impl r)
(t : spec.Domain)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.prob_changed_eq_zero
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(t : spec.Domain)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.prob_unchanged_eq_sub_probFailure
{ι : Type uι}
{spec : OracleSpec ι}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(t : spec.Domain)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.OracleComp.simulateQ_run_cellChange_prob_eq_zero
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[LawfulMonad m]
[HasEvalSPMF m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(r : CellRef Ident₀)
(himpl : QueryImpl.PreservesCell impl r)
(A : OracleComp spec α)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.OracleComp.simulateQ_run_cellUnchanged_prob_eq_sub_probFailure
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[LawfulMonad m]
[HasEvalSPMF m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(r : CellRef Ident₀)
(himpl : QueryImpl.PreservesCell impl r)
(A : OracleComp spec α)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.OracleComp.simulateQ_run_cellUnchanged_prob_eq_one_of_probFailure_eq_zero
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[LawfulMonad m]
[HasEvalSPMF m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(r : CellRef Ident₀)
(himpl : QueryImpl.PreservesCell impl r)
(A : OracleComp spec α)
(h : Heap Ident₀)
(hnf : Pr[⊥ | (simulateQ impl A).run h] = 0)
:
theorem
VCVio.StateSeparating.OracleComp.simulateQ_run_cellUnchanged_prob_eq_one
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[LawfulMonad m]
[HasEvalPMF m]
(impl : QueryImpl spec (StateT (Heap Ident₀) m))
(r : CellRef Ident₀)
(himpl : QueryImpl.PreservesCell impl r)
(A : OracleComp spec α)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.simulateQ_run_cellPreserved
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_1}
[Monad m]
[LawfulMonad m]
[HasEvalSet m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(A : OracleComp spec α)
(h : Heap Ident₀)
(z : α × Heap Ident₀)
:
A query-implementation cell-write footprint lifts through interpretation: if a cell is outside every per-query footprint, the interpreted computation preserves that cell.
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.simulateQ_run_cellChange_prob_eq_zero
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_2}
[Monad m]
[LawfulMonad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(A : OracleComp spec α)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.simulateQ_run_cellUnchanged_prob_eq_sub_probFailure
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_2}
[Monad m]
[LawfulMonad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(A : OracleComp spec α)
(h : Heap Ident₀)
:
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.simulateQ_run_cellUnchanged_prob_eq_one_of_probFailure_eq_zero
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_2}
[Monad m]
[LawfulMonad m]
[HasEvalSPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(A : OracleComp spec α)
(h : Heap Ident₀)
(hnf : Pr[⊥ | (simulateQ impl A).run h] = 0)
:
theorem
VCVio.StateSeparating.QueryImpl.CellWriteFootprint.simulateQ_run_cellUnchanged_prob_eq_one
{ι : Type uι}
{spec : OracleSpec ι}
{α : Type (max u₀ v)}
{Ident₀ : Type u₀}
[CellSpec Ident₀]
{m : Type (max u₀ v) → Type u_2}
[Monad m]
[LawfulMonad m]
[HasEvalPMF m]
{impl : QueryImpl spec (StateT (Heap Ident₀) m)}
(footprint : CellWriteFootprint impl)
(r : CellRef Ident₀)
(hr : ∀ (t : spec.Domain), r.id ∉ footprint.writes t)
(A : OracleComp spec α)
(h : Heap Ident₀)
:
Examples #
@[implicit_reducible]
@[implicit_reducible]
Query-handler write footprints #
@[implicit_reducible]
Every demo query returns unit; the interesting part is the heap effect.
Instances For
The handler writes only the cells declared by demoWrites.
Pack the handler-level footprint once, so later proofs need not unfold every query branch.
Instances For
The flag is outside every branch footprint, so each handler step preserves it.
A tiny client computation that calls several branches of the demo handler.
Instances For
The previous theorem as a reusable support-preservation predicate.
A compositional footprint for cacheAndLogStep. Reads contribute no writes,
writes contribute singleton footprints, and binds union the footprints.
Instances For
The compositional footprint gives flag preservation without unfolding each state update in the final proof.
A compositional footprint for the two-write program. The write set is
computed by WriteFootprint.bind: first {cache}, then {log}.
Instances For
Once the footprint says the write set is {cache, log}, flag preservation
is a one-line frame application plus a membership proof.
As a corollary, flagRef is preserved by cacheAndLogStep.