diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8934d1c..e596272 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -5,12 +5,17 @@ on: branches: [main] pull_request: +permissions: + contents: read + jobs: build: name: Build Caliper runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4 + with: + persist-credentials: false - name: Install elan run: | @@ -20,15 +25,17 @@ jobs: - name: Fetch mathlib build cache run: lake exe cache get - - name: Build the Caliper library - run: lake build Caliper + - name: Build Caliper and examples + run: lake build --wfail Caliper Examples unicorn-tests: name: Differential RV64 tests (Unicorn) runs-on: ubuntu-latest needs: build steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4 + with: + persist-credentials: false - name: Install elan run: | @@ -36,13 +43,13 @@ jobs: echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - name: Install uv - uses: astral-sh/setup-uv@v5 + uses: astral-sh/setup-uv@e58605a9b6da7c637471fab8847a5e5a6b8df081 # v5 - name: Fetch mathlib build cache run: lake exe cache get - name: Build Caliper and the test lowering - run: lake build Caliper CaliperTest + run: lake build --wfail Caliper CaliperTest Examples - name: Export differential vectors run: lake env lean --run CaliperTest/Export.lean diff --git a/Caliper.lean b/Caliper.lean index 88ebb31..46af18d 100644 --- a/Caliper.lean +++ b/Caliper.lean @@ -1,4 +1,8 @@ import Caliper.Core +import Caliper.Tape +import Caliper.Probability +import Caliper.ProbTriple +import Caliper.Retry import Caliper.Triple import Caliper.Builder import Caliper.Render diff --git a/Caliper/Builder.lean b/Caliper/Builder.lean index c769c0c..c73944e 100644 --- a/Caliper/Builder.lean +++ b/Caliper/Builder.lean @@ -68,6 +68,12 @@ def freshBuf : Build w BufId := def emit (c : Stmt w) : Build w Unit := fun s => ((), { s with code := c :: s.code }) +/-- Consume one tape word at runtime, placing it in a fresh register. -/ +def rand : Build w Reg := do + let d ← freshReg + emit (.rand d) + return d + /-- Right-nested sequencing of a code list (no trailing `skip`). -/ def seqAll : List (Stmt w) → Stmt w | [] => .skip diff --git a/Caliper/Core.lean b/Caliper/Core.lean index f0ca314..44d4c19 100644 --- a/Caliper/Core.lean +++ b/Caliper/Core.lean @@ -30,7 +30,7 @@ time is a syntactic constant. Two consequences for the instruction set: obligation), hence is worst-case unit time: no doubling, no amortisation anywhere in the machine. A growable vector is a library on top. -`Exec C c s s' t d p`: from `s`, `c` terminates in `s'` spending `t` time units, +`Exec C tape c s s' t d p`: from `s`, `c` terminates in `s'` spending `t` time units, with net live-memory change `d` (signed words) and peak growth `p` above the starting level. Live memory is the sum of reserved buffer capacities, so push and pop are memory-neutral. Registers are outside the dynamic profile: their lifetimes @@ -59,7 +59,13 @@ abbrev BufId := ℕ /-- Machine words. Fixed at `w = 64` by the `Caliper64` surface. -/ abbrev Word (w : ℕ) := BitVec w -variable {w : ℕ} +/-- An immutable, infinite input tape of words. -/ +abbrev RandomTape (w : ℕ) := ℕ → Word w + +/-- A fixed tape for deterministic examples. -/ +def RandomTape.zero {w : ℕ} : RandomTape w := fun _ => 0 + +variable {w : ℕ} {tape : RandomTape w} /-! ## Operations -/ @@ -115,6 +121,8 @@ inductive Stmt (w : ℕ) where | seq (c₁ c₂ : Stmt w) /-- `d ← v` -/ | imm (d : Reg) (v : Word w) + /-- Read the next word of the supplied tape into `d`, advancing the tape cursor. -/ + | rand (d : Reg) /-- `d ← a` -/ | mov (d a : Reg) /-- `d ← op a` -/ @@ -176,6 +184,8 @@ Skylake-ish latency table, and any bound proved generically over `C` instantiate both. -/ structure CostModel where imm : ℕ := 1 + /-- Abstract cost of consuming one input-tape word. -/ + rand : ℕ := 1 mov : ℕ := 1 un : UnOp → ℕ := fun _ => 1 bin : BinOp → ℕ := fun _ => 1 @@ -242,6 +252,7 @@ the acquisition that created the buffer, and the alloc *base* `memAlloc`, since zero-time allocation is the zero-capacity one, which acquires nothing. -/ structure CostModel.Admissible (C : CostModel) : Prop where imm : 1 ≤ C.imm + rand : 1 ≤ C.rand mov : 1 ≤ C.mov un : ∀ op, 1 ≤ C.un op bin : ∀ op, 1 ≤ C.bin op @@ -272,6 +283,8 @@ reserved capacity. All indexed by `ℕ` and represented as functions, which make separation lemmas below one-liners. Buffers are real `Array`s so that the interpreter does not walk a closure chain per element. -/ structure State (w : ℕ) where + /-- Input-tape cursor; bookkeeping outside the program memory metric. -/ + tapePos : ℕ := 0 regs : Reg → Word w bufs : BufId → Array (Word w) /-- Reserved capacity in words; live memory is the sum of capacities. -/ @@ -286,6 +299,22 @@ def State.init (w : ℕ) : State w where def State.setReg (s : State w) (d : Reg) (v : Word w) : State w := { s with regs := fun r => if r = d then v else s.regs r } +/-- Consume exactly one word without changing buffers or capacities. -/ +def State.readRandom (s : State w) (tape : RandomTape w) (d : Reg) : State w := + { s.setReg d (tape s.tapePos) with tapePos := s.tapePos + 1 } + +@[simp] theorem tapePos_readRandom (s : State w) (tape : RandomTape w) (d : Reg) : + (s.readRandom tape d).tapePos = s.tapePos + 1 := rfl + +@[simp] theorem regs_readRandom (s : State w) (tape : RandomTape w) (d : Reg) : + (s.readRandom tape d).regs = (s.setReg d (tape s.tapePos)).regs := rfl + +@[simp] theorem bufs_readRandom (s : State w) (tape : RandomTape w) (d : Reg) : + (s.readRandom tape d).bufs = s.bufs := rfl + +@[simp] theorem caps_readRandom (s : State w) (tape : RandomTape w) (d : Reg) : + (s.readRandom tape d).caps = s.caps := rfl + /-- Update the filled contents of `b` (capacity unchanged). -/ def State.setBuf (s : State w) (b : BufId) (a : Array (Word w)) : State w := { s with bufs := fun b' => if b' = b then a else s.bufs b' } @@ -339,78 +368,79 @@ a side condition decidable over two `ℕ`s. -/ /-! ## Semantics -`Exec C c s s' t d p`: statement `c` takes state `s` to `s'`, spending `t` time units, +`Exec C tape c s s' t d p`: statement `c` takes state `s` to `s'`, spending `t` time units, changing live memory by `d` words (net, signed) with peak growth `p`. Out-of-range `memLoad`/`memStore` have no rule, so a derivation witnesses memory safety. -/ -inductive Exec (C : CostModel) : Stmt w → State w → State w → ℕ → ℤ → ℤ → Prop where - | skip {s} : Exec C .skip s s 0 0 0 +inductive Exec (C : CostModel) (tape : RandomTape w) : Stmt w → State w → State w → ℕ → ℤ → ℤ → Prop where + | skip {s} : Exec C tape .skip s s 0 0 0 | seq {c₁ c₂ s s₁ s₂ t₁ d₁ p₁ t₂ d₂ p₂} : - Exec C c₁ s s₁ t₁ d₁ p₁ → Exec C c₂ s₁ s₂ t₂ d₂ p₂ → - Exec C (c₁ ;; c₂) s s₂ (t₁ + t₂) (d₁ + d₂) (max p₁ (d₁ + p₂)) - | imm {d v s} : Exec C (.imm d v) s (s.setReg d v) C.imm 0 0 - | mov {d a s} : Exec C (.mov d a) s (s.setReg d (s.regs a)) C.mov 0 0 + Exec C tape c₁ s s₁ t₁ d₁ p₁ → Exec C tape c₂ s₁ s₂ t₂ d₂ p₂ → + Exec C tape (c₁ ;; c₂) s s₂ (t₁ + t₂) (d₁ + d₂) (max p₁ (d₁ + p₂)) + | imm {d v s} : Exec C tape (.imm d v) s (s.setReg d v) C.imm 0 0 + | rand {d s} : Exec C tape (.rand d) s (s.readRandom tape d) C.rand 0 0 + | mov {d a s} : Exec C tape (.mov d a) s (s.setReg d (s.regs a)) C.mov 0 0 | un {op d a s} : - Exec C (.un op d a) s (s.setReg d (op.eval (s.regs a))) (C.un op) 0 0 + Exec C tape (.un op d a) s (s.setReg d (op.eval (s.regs a))) (C.un op) 0 0 | bin {op d a b s} : - Exec C (.bin op d a b) s (s.setReg d (op.eval (s.regs a) (s.regs b))) + Exec C tape (.bin op d a b) s (s.setReg d (op.eval (s.regs a) (s.regs b))) (C.bin op) 0 0 /-- Reserve capacity (dynamic, from a register): charges the new capacity, credits the old. Time is `C.memAlloc + cap * C.allocPerWord`, state-dependent, since the capacity is read from a register at runtime. -/ | memAlloc {b n s} : - Exec C (.memAlloc b n) s (s.allocBuf b (s.regs n).toNat) + Exec C tape (.memAlloc b n) s (s.allocBuf b (s.regs n).toNat) (C.memAlloc + (s.regs n).toNat * C.allocPerWord) (((s.regs n).toNat : ℤ) - (s.caps b : ℤ)) (max (((s.regs n).toNat : ℤ) - (s.caps b : ℤ)) 0) /-- Reserve capacity (immediate): identical semantics at capacity `n`, with the per-word time charge a pure function of the instruction. -/ | memAllocI {b n s} : - Exec C (.memAllocI b n) s (s.allocBuf b n) + Exec C tape (.memAllocI b n) s (s.allocBuf b n) (C.memAlloc + n * C.allocPerWord) ((n : ℤ) - (s.caps b : ℤ)) (max ((n : ℤ) - (s.caps b : ℤ)) 0) /-- Free: credits the whole capacity, at time `C.memFree`, 0 in both shipped tables (release was priced at acquisition). -/ | memFree {b s} : - Exec C (.memFree b) s (s.allocBuf b 0) C.memFree (-(s.caps b : ℤ)) 0 + Exec C tape (.memFree b) s (s.allocBuf b 0) C.memFree (-(s.caps b : ℤ)) 0 | memLen {d b s} : - Exec C (.memLen d b) s (s.setReg d (BitVec.ofNat w (s.bufs b).size)) C.memLen 0 0 + Exec C tape (.memLen d b) s (s.setReg d (BitVec.ofNat w (s.bufs b).size)) C.memLen 0 0 | memLoad {d b i s} (h : (s.regs i).toNat < (s.bufs b).size) : - Exec C (.memLoad d b i) s (s.setReg d (s.bufs b)[(s.regs i).toNat]) C.memLoad 0 0 + Exec C tape (.memLoad d b i) s (s.setReg d (s.bufs b)[(s.regs i).toNat]) C.memLoad 0 0 | memStore {b i src s} (h : (s.regs i).toNat < (s.bufs b).size) : - Exec C (.memStore b i src) s + Exec C tape (.memStore b i src) s (s.setBuf b ((s.bufs b).set (s.regs i).toNat (s.regs src) h)) C.memStore 0 0 /-- Push requires free capacity: no rule otherwise, so a derivation proves the program stays within what it reserved. Memory-neutral. -/ | memPush {b src s} (h : (s.bufs b).size < s.caps b) : - Exec C (.memPush b src) s (s.setBuf b ((s.bufs b).push (s.regs src))) + Exec C tape (.memPush b src) s (s.setBuf b ((s.bufs b).push (s.regs src))) C.memPush 0 0 /-- Pop keeps the capacity: memory-neutral. -/ | memPop {b s} : - Exec C (.memPop b) s (s.setBuf b (s.bufs b).pop) C.memPop 0 0 + Exec C tape (.memPop b) s (s.setBuf b (s.bufs b).pop) C.memPop 0 0 | ifNZ_true {c thn els s s' t d p} (h : s.regs c ≠ 0) : - Exec C thn s s' t d p → Exec C (.ifNZ c thn els) s s' (C.branch + t) d p + Exec C tape thn s s' t d p → Exec C tape (.ifNZ c thn els) s s' (C.branch + t) d p | ifNZ_false {c thn els s s' t d p} (h : s.regs c = 0) : - Exec C els s s' t d p → Exec C (.ifNZ c thn els) s s' (C.branch + t) d p + Exec C tape els s s' t d p → Exec C tape (.ifNZ c thn els) s s' (C.branch + t) d p | while_done {g c b s s₁ tg dg pg} : - Exec C g s s₁ tg dg pg → s₁.regs c = 0 → - Exec C (.whileNZ g c b) s s₁ (tg + C.branch) dg pg + Exec C tape g s s₁ tg dg pg → s₁.regs c = 0 → + Exec C tape (.whileNZ g c b) s s₁ (tg + C.branch) dg pg | while_step {g c b s s₁ s₂ s₃ tg dg pg tb db pb tl dl pl} : - Exec C g s s₁ tg dg pg → s₁.regs c ≠ 0 → Exec C b s₁ s₂ tb db pb → - Exec C (.whileNZ g c b) s₂ s₃ tl dl pl → - Exec C (.whileNZ g c b) s s₃ (tg + C.branch + tb + tl) (dg + db + dl) + Exec C tape g s s₁ tg dg pg → s₁.regs c ≠ 0 → Exec C tape b s₁ s₂ tb db pb → + Exec C tape (.whileNZ g c b) s₂ s₃ tl dl pl → + Exec C tape (.whileNZ g c b) s s₃ (tg + C.branch + tb + tl) (dg + db + dl) (max pg (dg + max pb (db + pl))) /-! ## Basic metatheory -/ -/-- The machine is deterministic: a statement has at most one outcome, hence at most +/-- For a fixed tape the machine is deterministic: a statement has at most one outcome, hence at most one cost, so "the" running time is well defined and a bound proved for one execution bounds all of them. -/ theorem Exec.deterministic {C : CostModel} {c : Stmt w} {s s₁ s₂ : State w} {t₁ t₂ : ℕ} {d₁ p₁ d₂ p₂ : ℤ} - (h₁ : Exec C c s s₁ t₁ d₁ p₁) (h₂ : Exec C c s s₂ t₂ d₂ p₂) : + (h₁ : Exec C tape c s s₁ t₁ d₁ p₁) (h₂ : Exec C tape c s s₂ t₂ d₂ p₂) : s₁ = s₂ ∧ t₁ = t₂ ∧ d₁ = d₂ ∧ p₁ = p₂ := by induction h₁ generalizing s₂ t₂ d₂ p₂ with | seq _ _ ih₁ ih₂ => @@ -446,19 +476,19 @@ theorem Exec.deterministic {C : CostModel} {c : Stmt w} {s s₁ s₂ : State w} /-- The peak never dips below the start level. -/ theorem Exec.peak_nonneg {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) : 0 ≤ p := by + {d p : ℤ} (h : Exec C tape c s s' t d p) : 0 ≤ p := by induction h <;> omega /-- The net change is bounded by the peak. -/ theorem Exec.net_le_peak {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) : d ≤ p := by + {d p : ℤ} (h : Exec C tape c s s' t d p) : d ≤ p := by induction h <;> omega /-- The induction core of `Exec.peak_le_time`: both memory indices bounded by the running time in one induction, since the `seq`/`whileNZ` peak algebra needs the net bound of the prefix to bound the peak of the whole. -/ theorem Exec.net_and_peak_le_time {C : CostModel} {c : Stmt w} {s s' : State w} - {t : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) (hC : 1 ≤ C.allocPerWord) : + {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hC : 1 ≤ C.allocPerWord) : d ≤ (t : ℤ) ∧ p ≤ (t : ℤ) := by induction h with | @memAlloc b n s => @@ -484,25 +514,25 @@ execution's live-memory peak exceeds its running time, so one certificate covers both resources. The register-side counterpart is `Stmt.Straight.regPeak₀_le` (`Liveness.lean`). -/ theorem Exec.peak_le_time {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) (hC : 1 ≤ C.allocPerWord) : p ≤ (t : ℤ) := + {d p : ℤ} (h : Exec C tape c s s' t d p) (hC : 1 ≤ C.allocPerWord) : p ≤ (t : ℤ) := (h.net_and_peak_le_time hC).2 /-- Corollary of `Exec.peak_le_time`: the net live-memory change is bounded by the running time as well. -/ theorem Exec.net_le_time {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) (hC : 1 ≤ C.allocPerWord) : d ≤ (t : ℤ) := + {d p : ℤ} (h : Exec C tape c s s' t d p) (hC : 1 ≤ C.allocPerWord) : d ≤ (t : ℤ) := (h.net_and_peak_le_time hC).1 /-- `Exec.peak_le_time` under the packaged `CostModel.Admissible` hypothesis (satisfied by both shipped tables: `CostModel.unit.admissible`, `CostModel.cycles.admissible`). -/ theorem Exec.peak_le_time_admissible {C : CostModel} {c : Stmt w} {s s' : State w} - {t : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) (hC : C.Admissible) : p ≤ (t : ℤ) := + {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hC : C.Admissible) : p ≤ (t : ℤ) := h.peak_le_time hC.allocPerWord /-- `Exec.net_le_time` under the packaged `CostModel.Admissible` hypothesis. -/ theorem Exec.net_le_time_admissible {C : CostModel} {c : Stmt w} {s s' : State w} - {t : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) (hC : C.Admissible) : d ≤ (t : ℤ) := + {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hC : C.Admissible) : d ≤ (t : ℤ) := h.net_le_time hC.allocPerWord /-! ### Framing: which registers and buffers a statement can touch @@ -514,6 +544,7 @@ decidable, hence dischargeable by `simp`/`decide` on concrete code. -/ def Stmt.Writes : Stmt w → Reg → Prop | .skip, _ => False | .seq c₁ c₂, r => c₁.Writes r ∨ c₂.Writes r + | .rand d, r => r = d | .imm d _, r => r = d | .mov d _, r => r = d | .un _ d _, r => r = d @@ -549,6 +580,7 @@ instance instDecidableWrites : ∀ (c : Stmt w) (r : Reg), Decidable (c.Writes r have := instDecidableWrites c₁ r have := instDecidableWrites c₂ r inferInstanceAs (Decidable (_ ∨ _)) + | .rand d, r => inferInstanceAs (Decidable (r = d)) | .imm d _, r => inferInstanceAs (Decidable (r = d)) | .mov d _, r => inferInstanceAs (Decidable (r = d)) | .un _ d _, r => inferInstanceAs (Decidable (r = d)) @@ -576,6 +608,7 @@ instance instDecidableTouches : ∀ (c : Stmt w) (b : BufId), Decidable (c.Touch have := instDecidableTouches c₁ b have := instDecidableTouches c₂ b inferInstanceAs (Decidable (_ ∨ _)) + | .rand .., _ => inferInstanceAs (Decidable False) | .imm .., _ => inferInstanceAs (Decidable False) | .mov .., _ => inferInstanceAs (Decidable False) | .un .., _ => inferInstanceAs (Decidable False) @@ -615,13 +648,13 @@ private theorem Writes_Touches_eq_lemmas_realized : True := by /-- Register frame rule. -/ theorem Exec.frame_reg {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} {r : Reg} - (h : Exec C c s s' t d p) (hr : ¬ c.Writes r) : s'.regs r = s.regs r := by + (h : Exec C tape c s s' t d p) (hr : ¬ c.Writes r) : s'.regs r = s.regs r := by induction h with | skip => rfl | seq _ _ ih₁ ih₂ => simp only [Writes_seq, not_or] at hr rw [ih₂ hr.2, ih₁ hr.1] - | imm | mov | un | bin | memLen | memLoad => + | rand | imm | mov | un | bin | memLen | memLoad => exact regs_setReg_ne _ _ hr | memAlloc | memAllocI | memFree | memStore | memPush | memPop => rfl | ifNZ_true _ _ ih => exact ih fun hh => hr (Or.inl hh) @@ -634,13 +667,13 @@ theorem Exec.frame_reg {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} instead of an entailment. -/ theorem Exec.frame_buf {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} {b : BufId} - (h : Exec C c s s' t d p) (hb : ¬ c.Touches b) : s'.bufs b = s.bufs b := by + (h : Exec C tape c s s' t d p) (hb : ¬ c.Touches b) : s'.bufs b = s.bufs b := by induction h with | skip => rfl | seq _ _ ih₁ ih₂ => simp only [Touches_seq, not_or] at hb rw [ih₂ hb.2, ih₁ hb.1] - | imm | mov | un | bin | memLen | memLoad => rfl + | rand | imm | mov | un | bin | memLen | memLoad => rfl | memStore | memPush | memPop => exact bufs_setBuf_ne _ _ hb | memAlloc | memAllocI | memFree => exact bufs_allocBuf_ne _ _ hb | ifNZ_true _ _ ih => exact ih fun hh => hb (Or.inl hh) @@ -652,13 +685,13 @@ theorem Exec.frame_buf {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} /-- Capacity frame rule: an untouched buffer keeps its reserved capacity too. -/ theorem Exec.frame_cap {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} {b : BufId} - (h : Exec C c s s' t d p) (hb : ¬ c.Touches b) : s'.caps b = s.caps b := by + (h : Exec C tape c s s' t d p) (hb : ¬ c.Touches b) : s'.caps b = s.caps b := by induction h with | skip => rfl | seq _ _ ih₁ ih₂ => simp only [Touches_seq, not_or] at hb rw [ih₂ hb.2, ih₁ hb.1] - | imm | mov | un | bin | memLen | memLoad => rfl + | rand | imm | mov | un | bin | memLen | memLoad => rfl | memStore | memPush | memPop => rfl | memAlloc | memAllocI | memFree => exact caps_allocBuf_ne _ _ hb | ifNZ_true _ _ ih => exact ih fun hh => hb (Or.inl hh) @@ -715,6 +748,7 @@ or dynamically-allocating code come from the `Triple` logic. -/ def Stmt.staticTime (C : CostModel) : Stmt w → ℕ | .skip => 0 | .seq c₁ c₂ => c₁.staticTime C + c₂.staticTime C + | .rand .. => C.rand | .imm .. => C.imm | .mov .. => C.mov | .un op .. => C.un op @@ -744,7 +778,7 @@ def Stmt.AllocFree : Stmt w → Prop /-- Branch-free code runs in constant time: the running time is a function of the syntax alone, never of the state. -/ theorem Exec.straight_time_eq {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) (hs : c.Straight) : t = c.staticTime C := by + {d p : ℤ} (h : Exec C tape c s s' t d p) (hs : c.Straight) : t = c.staticTime C := by induction h with | seq _ _ ih₁ ih₂ => exact congrArg₂ (· + ·) (ih₁ hs.1) (ih₂ hs.2) | memAlloc | ifNZ_true | ifNZ_false | while_done | while_step => exact hs.elim @@ -754,7 +788,7 @@ theorem Exec.straight_time_eq {C : CostModel} {c : Stmt w} {s s' : State w} {t : longer exact, since the branches may cost different amounts, but `staticTime`'s `branch + max` shape bounds every execution. -/ theorem Exec.time_le_staticTime_of_loopFree {C : CostModel} {c : Stmt w} - {s s' : State w} {t : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) + {s s' : State w} {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hl : c.LoopFree) : t ≤ c.staticTime C := by induction h with | seq _ _ ih₁ ih₂ => exact Nat.add_le_add (ih₁ hl.1) (ih₂ hl.2) @@ -769,7 +803,7 @@ theorem Exec.time_le_staticTime_of_loopFree {C : CostModel} {c : Stmt w} straight-line or not, has non-positive net and zero peak growth. `memFree` may make the net strictly negative. -/ theorem Exec.allocFree_space {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) (ha : c.AllocFree) : + {d p : ℤ} (h : Exec C tape c s s' t d p) (ha : c.AllocFree) : d ≤ 0 ∧ p ≤ 0 := by induction h with | seq _ _ ih₁ ih₂ => @@ -792,7 +826,7 @@ their inputs. This is data-independence of the abstract time counter, an ingredi of a constant-time argument, not by itself a side-channel guarantee. -/ theorem Exec.straight_data_independent {C : CostModel} {c : Stmt w} {s₁ s₁' s₂ s₂' : State w} {t₁ t₂ : ℕ} {d₁ p₁ d₂ p₂ : ℤ} - (h₁ : Exec C c s₁ s₁' t₁ d₁ p₁) (h₂ : Exec C c s₂ s₂' t₂ d₂ p₂) + (h₁ : Exec C tape c s₁ s₁' t₁ d₁ p₁) (h₂ : Exec C tape c s₂ s₂' t₂ d₂ p₂) (hs : c.Straight) : t₁ = t₂ := (h₁.straight_time_eq hs).trans (h₂.straight_time_eq hs).symm @@ -852,7 +886,7 @@ theorem Stmt.Straight.staticTime?_eq {c : Stmt w} (hs : c.Straight) (C : CostMod every execution, on every input. The `Option`-valued API needs no side condition: `some` already certifies straightness. -/ theorem Exec.staticTime?_time_eq {C : CostModel} {c : Stmt w} {s s' : State w} - {t n : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) (hn : c.staticTime? C = some n) : + {t n : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hn : c.staticTime? C = some n) : t = n := by obtain ⟨hs, rfl⟩ := Stmt.staticTime?_eq_some.mp hn exact h.straight_time_eq hs @@ -910,7 +944,7 @@ theorem State.init_wellFormed : (State.init w).WellFormed where syntax, so this is a static quantity; in particular `c` cannot touch a buffer at or above `c.memBound` (`Stmt.touches_lt_memBound`). -/ def Stmt.memBound : Stmt w → ℕ - | .skip | .imm .. | .mov .. | .un .. | .bin .. => 0 + | .skip | .rand .. | .imm .. | .mov .. | .un .. | .bin .. => 0 | .seq c₁ c₂ => max c₁.memBound c₂.memBound | .memAlloc b _ => b + 1 | .memAllocI b _ => b + 1 @@ -954,12 +988,12 @@ theorem Stmt.touches_lt_of_memBound_le {c : Stmt w} {B : ℕ} (hB : c.memBound hypothesis is exactly what keeps the invariant alive), `memAlloc`/`memFree` install an empty array along with the new capacity, and no other instruction grows a buffer. -/ theorem Exec.sizes_le_caps {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec C c s s' t d p) (hs : ∀ b, (s.bufs b).size ≤ s.caps b) : + {d p : ℤ} (h : Exec C tape c s s' t d p) (hs : ∀ b, (s.bufs b).size ≤ s.caps b) : ∀ b, (s'.bufs b).size ≤ s'.caps b := by induction h with | skip => exact hs | seq _ _ ih₁ ih₂ => exact ih₂ (ih₁ hs) - | imm | mov | un | bin | memLen | memLoad => exact hs + | rand | imm | mov | un | bin | memLen | memLoad => exact hs | @memAlloc b n s => intro b' by_cases hb : b' = b @@ -1001,7 +1035,7 @@ theorem Exec.sizes_le_caps {C : CostModel} {c : Stmt w} {s s' : State w} {t : /-- A support bound survives execution: capacities only change at buffers named in `c`, all of which lie below the bound. -/ theorem Exec.supportBound_preserved {C : CostModel} {c : Stmt w} {s s' : State w} - {t : ℕ} {d p : ℤ} {B : ℕ} (h : Exec C c s s' t d p) + {t : ℕ} {d p : ℤ} {B : ℕ} (h : Exec C tape c s s' t d p) (hc : ∀ b, c.Touches b → b < B) (hs : s.SupportBound B) : s'.SupportBound B := by intro b hb @@ -1013,7 +1047,7 @@ reachable from the initial state is well-formed, so the memory profile of an execution from an honest start reads as physical memory (`Exec.liveMem_eq`, `Exec.reaches_liveMem_le_peak`). -/ theorem Exec.wellFormed_preserved {C : CostModel} {c : Stmt w} {s s' : State w} - {t : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) (hwf : s.WellFormed) : + {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hwf : s.WellFormed) : s'.WellFormed where size_le_cap := h.sizes_le_caps hwf.size_le_cap finite := by @@ -1031,6 +1065,12 @@ def State.liveMem (s : State w) : ℕ → ℕ | 0 => 0 | B + 1 => s.liveMem B + s.caps B +@[simp] theorem liveMem_readRandom (s : State w) (tape : RandomTape w) (r : Reg) + (B : ℕ) : (s.readRandom tape r).liveMem B = s.liveMem B := by + induction B with + | zero => rfl + | succ B ih => simp only [State.liveMem, caps_readRandom, ih] + @[simp] theorem liveMem_setReg (s : State w) (r : Reg) (v : Word w) (B : ℕ) : (s.setReg r v).liveMem B = s.liveMem B := by induction B with @@ -1096,7 +1136,7 @@ theorem liveMem_eq_of_supportBound {s : State w} {B B' : ℕ} (hs : s.SupportBou absolute footprint moves by exactly `d`, not merely by at most `d`. A `Triple` still only certifies `d ≤ D`; the exactness is between `d` and the state. -/ theorem Exec.liveMem_eq {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} {B : ℕ} (h : Exec C c s s' t d p) + {d p : ℤ} {B : ℕ} (h : Exec C tape c s s' t d p) (hc : ∀ b, c.Touches b → b < B) : (s'.liveMem B : ℤ) = s.liveMem B + d := by induction h with @@ -1104,7 +1144,7 @@ theorem Exec.liveMem_eq {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} | seq _ _ ih₁ ih₂ => rw [ih₂ (fun b hb => hc b (Or.inr hb)), ih₁ (fun b hb => hc b (Or.inl hb))] ring - | imm | mov | un | bin | memLen | memLoad => simp + | rand | imm | mov | un | bin | memLen | memLoad => simp | memAlloc => rw [liveMem_allocBuf _ _ (hc _ rfl)]; omega | memAllocI => rw [liveMem_allocBuf _ _ (hc _ rfl)]; omega | memFree => rw [liveMem_allocBuf _ _ (hc _ rfl)]; omega @@ -1119,43 +1159,43 @@ theorem Exec.liveMem_eq {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} /-- The final footprint stays within the peak: `liveMem s' ≤ liveMem s + p`. -/ theorem Exec.liveMem_le_peak {C : CostModel} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} {B : ℕ} (h : Exec C c s s' t d p) + {d p : ℤ} {B : ℕ} (h : Exec C tape c s s' t d p) (hc : ∀ b, c.Touches b → b < B) : (s'.liveMem B : ℤ) ≤ s.liveMem B + p := by have h₁ := h.liveMem_eq hc have h₂ := h.net_le_peak omega -/-- `Reaches C c s m`: an execution of `c` from `s` passes through state `m`, either +/-- `Reaches C tape c s m`: an execution of `c` from `s` passes through state `m`, either the start state or a state at an instruction boundary strictly inside the execution; the branch conditions keep every constructor on the path actually taken. The final state is covered separately by `Exec.liveMem_le_peak`, so together the two enumerate every state an execution visits. -/ -inductive Reaches (C : CostModel) : Stmt w → State w → State w → Prop where - | start {c : Stmt w} {s : State w} : Reaches C c s s +inductive Reaches (C : CostModel) (tape : RandomTape w) : Stmt w → State w → State w → Prop where + | start {c : Stmt w} {s : State w} : Reaches C tape c s s | seq_left {c₁ c₂ : Stmt w} {s m : State w} : - Reaches C c₁ s m → Reaches C (c₁ ;; c₂) s m + Reaches C tape c₁ s m → Reaches C tape (c₁ ;; c₂) s m | seq_right {c₁ c₂ : Stmt w} {s s₁ m : State w} {t₁ : ℕ} {d₁ p₁ : ℤ} : - Exec C c₁ s s₁ t₁ d₁ p₁ → Reaches C c₂ s₁ m → Reaches C (c₁ ;; c₂) s m + Exec C tape c₁ s s₁ t₁ d₁ p₁ → Reaches C tape c₂ s₁ m → Reaches C tape (c₁ ;; c₂) s m | ifNZ_true {r : Reg} {thn els : Stmt w} {s m : State w} : - s.regs r ≠ 0 → Reaches C thn s m → Reaches C (.ifNZ r thn els) s m + s.regs r ≠ 0 → Reaches C tape thn s m → Reaches C tape (.ifNZ r thn els) s m | ifNZ_false {r : Reg} {thn els : Stmt w} {s m : State w} : - s.regs r = 0 → Reaches C els s m → Reaches C (.ifNZ r thn els) s m + s.regs r = 0 → Reaches C tape els s m → Reaches C tape (.ifNZ r thn els) s m | while_guard {g body : Stmt w} {r : Reg} {s m : State w} : - Reaches C g s m → Reaches C (.whileNZ g r body) s m + Reaches C tape g s m → Reaches C tape (.whileNZ g r body) s m | while_body {g body : Stmt w} {r : Reg} {s s₁ m : State w} {tg : ℕ} {dg pg : ℤ} : - Exec C g s s₁ tg dg pg → s₁.regs r ≠ 0 → Reaches C body s₁ m → - Reaches C (.whileNZ g r body) s m + Exec C tape g s s₁ tg dg pg → s₁.regs r ≠ 0 → Reaches C tape body s₁ m → + Reaches C tape (.whileNZ g r body) s m | while_loop {g body : Stmt w} {r : Reg} {s s₁ s₂ m : State w} {tg tb : ℕ} {dg pg db pb : ℤ} : - Exec C g s s₁ tg dg pg → s₁.regs r ≠ 0 → Exec C body s₁ s₂ tb db pb → - Reaches C (.whileNZ g r body) s₂ m → Reaches C (.whileNZ g r body) s m + Exec C tape g s s₁ tg dg pg → s₁.regs r ≠ 0 → Exec C tape body s₁ s₂ tb db pb → + Reaches C tape (.whileNZ g r body) s₂ m → Reaches C tape (.whileNZ g r body) s m /-- The peak bounds every intermediate state: any state an execution passes through (`Reaches`) has absolute footprint at most `p` above the start, so `p` is the high-water mark of the whole execution, not a statement about its endpoints. -/ theorem Exec.reaches_liveMem_le_peak {C : CostModel} {c : Stmt w} {s s' m : State w} - {t : ℕ} {d p : ℤ} {B : ℕ} (h : Exec C c s s' t d p) (hm : Reaches C c s m) + {t : ℕ} {d p : ℤ} {B : ℕ} (h : Exec C tape c s s' t d p) (hm : Reaches C tape c s m) (hc : ∀ b, c.Touches b → b < B) : (m.liveMem B : ℤ) ≤ s.liveMem B + p := by induction hm generalizing s' t d p with @@ -1215,7 +1255,7 @@ exceeds `liveMem`. A free can neither drive the footprint negative nor fund an allocation the profile did not pay for; by `Exec.liveMem_eq` the footprint after `memFree b ;; memAlloc b' n` is `liveMem s - s.caps b + n`, all charged. -/ theorem Exec.memFree_credit_le {C : CostModel} {b : BufId} {s s' : State w} {t : ℕ} - {d p : ℤ} {B : ℕ} (h : Exec C (.memFree b) s s' t d p) (hb : b < B) : + {d p : ℤ} {B : ℕ} (h : Exec C tape (.memFree b) s s' t d p) (hb : b < B) : -d ≤ (s.liveMem B : ℤ) := by cases h have := caps_le_liveMem s hb @@ -1228,15 +1268,16 @@ recursive call consumes one unit, so any `fuel ≥` statement depth × loop trip suffices); `none` means "ran out of fuel, or hit an out-of-range buffer access". Fuel is an interpreter artifact; no cost is derived from it. -/ -def run (C : CostModel) : ℕ → Stmt w → State w → Option (State w × ℕ × ℤ × ℤ) +def run (C : CostModel) (tape : RandomTape w) : ℕ → Stmt w → State w → Option (State w × ℕ × ℤ × ℤ) | 0, _, _ => none | f + 1, c, s => match c with | .skip => some (s, 0, 0, 0) | .seq c₁ c₂ => do - let (s₁, t₁, d₁, p₁) ← run C f c₁ s - let (s₂, t₂, d₂, p₂) ← run C f c₂ s₁ + let (s₁, t₁, d₁, p₁) ← run C tape f c₁ s + let (s₂, t₂, d₂, p₂) ← run C tape f c₂ s₁ some (s₂, t₁ + t₂, d₁ + d₂, max p₁ (d₁ + p₂)) + | .rand d => some (s.readRandom tape d, C.rand, 0, 0) | .imm d v => some (s.setReg d v, C.imm, 0, 0) | .mov d a => some (s.setReg d (s.regs a), C.mov, 0, 0) | .un op d a => some (s.setReg d (op.eval (s.regs a)), C.un op, 0, 0) @@ -1270,18 +1311,18 @@ def run (C : CostModel) : ℕ → Stmt w → State w → Option (State w × ℕ | .memPop b => some (s.setBuf b (s.bufs b).pop, C.memPop, 0, 0) | .ifNZ c thn els => if s.regs c = 0 then do - let (s', t, d, p) ← run C f els s + let (s', t, d, p) ← run C tape f els s some (s', C.branch + t, d, p) else do - let (s', t, d, p) ← run C f thn s + let (s', t, d, p) ← run C tape f thn s some (s', C.branch + t, d, p) | .whileNZ g cc b => do - let (s₁, tg, dg, pg) ← run C f g s + let (s₁, tg, dg, pg) ← run C tape f g s if s₁.regs cc = 0 then some (s₁, tg + C.branch, dg, pg) else do - let (s₂, tb, db, pb) ← run C f b s₁ - let (s₃, tl, dl, pl) ← run C f (.whileNZ g cc b) s₂ + let (s₂, tb, db, pb) ← run C tape f b s₁ + let (s₃, tl, dl, pl) ← run C tape f (.whileNZ g cc b) s₂ some (s₃, tg + C.branch + tb + tl, dg + db + dl, max pg (dg + max pb (db + pl))) @@ -1289,7 +1330,7 @@ def run (C : CostModel) : ℕ → Stmt w → State w → Option (State w × ℕ the costs it reports. So `#eval`-ing a program gives numbers that the `Exec`-level theorems are about. -/ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} {t : ℕ} {d p : ℤ}, - run C f c s = some (s', t, d, p) → Exec C c s s' t d p := by + run C tape f c s = some (s', t, d, p) → Exec C tape c s s' t d p := by intro f induction f with | zero => intro c s s' t d p h; cases h @@ -1301,14 +1342,14 @@ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} obtain ⟨rfl, rfl, rfl, rfl⟩ := h; exact .skip | .seq c₁ c₂ => simp only [run] at h - cases h₁ : run C f c₁ s with + cases h₁ : run C tape f c₁ s with | none => simp only [h₁, Option.bind_eq_bind, Option.bind_none] at h cases h | some r₁ => obtain ⟨s₁, t₁, d₁, p₁⟩ := r₁ simp only [h₁, Option.bind_eq_bind, Option.bind_some] at h - cases h₂ : run C f c₂ s₁ with + cases h₂ : run C tape f c₂ s₁ with | none => simp only [h₂, Option.bind_none] at h cases h @@ -1317,6 +1358,9 @@ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} simp only [h₂, Option.bind_some, Option.some.injEq, Prod.mk.injEq] at h obtain ⟨rfl, rfl, rfl, rfl⟩ := h exact .seq (ih _ h₁) (ih _ h₂) + | .rand d => + simp only [run, Option.some.injEq] at h + obtain ⟨rfl, rfl, rfl, rfl⟩ := h; exact .rand | .imm d v => simp only [run, Option.some.injEq] at h obtain ⟨rfl, rfl, rfl, rfl⟩ := h; exact .imm @@ -1369,7 +1413,7 @@ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} simp only [run] at h by_cases hc : s.regs c = 0 · rw [if_pos hc] at h - cases h₁ : run C f els s with + cases h₁ : run C tape f els s with | none => simp only [h₁, Option.bind_eq_bind, Option.bind_none] at h cases h @@ -1379,7 +1423,7 @@ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} obtain ⟨rfl, rfl, rfl, rfl⟩ := h exact .ifNZ_false hc (ih _ h₁) · rw [if_neg hc] at h - cases h₁ : run C f thn s with + cases h₁ : run C tape f thn s with | none => simp only [h₁, Option.bind_eq_bind, Option.bind_none] at h cases h @@ -1390,7 +1434,7 @@ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} exact .ifNZ_true hc (ih _ h₁) | .whileNZ g cc b => simp only [run] at h - cases hg : run C f g s with + cases hg : run C tape f g s with | none => simp only [hg, Option.bind_eq_bind, Option.bind_none] at h cases h @@ -1403,14 +1447,14 @@ theorem run_sound {C : CostModel} : ∀ (f : ℕ) (c : Stmt w) {s s' : State w} obtain ⟨rfl, rfl, rfl, rfl⟩ := h exact .while_done (ih _ hg) hz · rw [if_neg hz] at h - cases hb : run C f b s₁ with + cases hb : run C tape f b s₁ with | none => simp only [hb, Option.bind_none] at h cases h | some rb => obtain ⟨s₂, tb, db, pb⟩ := rb simp only [hb, Option.bind_some] at h - cases hl : run C f (.whileNZ g cc b) s₂ with + cases hl : run C tape f (.whileNZ g cc b) s₂ with | none => simp only [hl, Option.bind_none] at h cases h diff --git a/Caliper/Corpus/Arith.lean b/Caliper/Corpus/Arith.lean index c97ba0f..7b3ae61 100644 --- a/Caliper/Corpus/Arith.lean +++ b/Caliper/Corpus/Arith.lean @@ -80,10 +80,10 @@ def timeBound (C : CostModel) (n : ℕ) : ℕ := (0, 0), for any cost model. -/ theorem spec {C : CostModel} (xs ys : BufId) (aX aY : Array (Word w)) (hsz : aX.size < 2 ^ w) (hlen : aY.size = aX.size) : - Triple C (fun s => s.bufs xs = aX ∧ s.bufs ys = aY) (code xs ys) + Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = aX ∧ s.bufs ys = aY) (code xs ys) (fun s => s.regs 0 = dotTo aX aY aX.size) (timeBound C aX.size) 0 0 := by - have hguard : ∀ k, Triple C (Inv xs ys aX aY k) (.bin .ult 3 1 2) + have hguard : ∀ k, Triple C Caliper.RandomTape.zero (Inv xs ys aX aY k) (.bin .ult 3 1 2) (InvG xs ys aX aY k) (C.bin .ult) 0 0 := by intro k apply Triple.bin @@ -99,7 +99,7 @@ theorem spec {C : CostModel} (xs ys : BufId) (aX aY : Array (Word w)) rintro k s ⟨⟨hbx, hby, hn, hik, hacc⟩, hflag⟩ hnz have hlt := cond_of_flag_ne hflag hnz exact ⟨k - 1, by omega⟩ - have hbody : ∀ k, Triple C (fun s => InvG xs ys aX aY (k + 1) s ∧ s.regs 3 ≠ 0) + have hbody : ∀ k, Triple C Caliper.RandomTape.zero (fun s => InvG xs ys aX aY (k + 1) s ∧ s.regs 3 ≠ 0) (.memLoad 4 xs 1 ;; .memLoad 5 ys 1 ;; .bin .mul 6 4 5 ;; .bin .add 0 0 6 ;; .imm 7 1 ;; .bin .add 1 1 7) (Inv xs ys aX aY k) @@ -125,15 +125,15 @@ theorem spec {C : CostModel} (xs ys : BufId) (aX aY : Array (Word w)) · simp [-BitVec.toNat_add, hbx, hby] rw [toNat_add_ofNat_one hlt hsz] simp [dotTo, hlt, hlt.trans_le hlen.ge, hacc] - have h1 : Triple C (fun s => s.bufs xs = aX ∧ s.bufs ys = aY) (.imm 0 0) + have h1 : Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = aX ∧ s.bufs ys = aY) (.imm 0 0) (fun s => s.bufs xs = aX ∧ s.bufs ys = aY ∧ s.regs 0 = 0) C.imm 0 0 := Triple.imm fun s hs => by simp [hs.1, hs.2] - have h2 : Triple C (fun s => s.bufs xs = aX ∧ s.bufs ys = aY ∧ s.regs 0 = 0) + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = aX ∧ s.bufs ys = aY ∧ s.regs 0 = 0) (.imm 1 0) (fun s => s.bufs xs = aX ∧ s.bufs ys = aY ∧ s.regs 0 = 0 ∧ s.regs 1 = 0) C.imm 0 0 := Triple.imm fun s hs => by simp [hs.1, hs.2.1, hs.2.2] - have h3 : Triple C + have h3 : Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = aX ∧ s.bufs ys = aY ∧ s.regs 0 = 0 ∧ s.regs 1 = 0) (.memLen 2 xs) (Inv xs ys aX aY aX.size) C.memLen 0 0 := by apply Triple.memLen @@ -158,7 +158,7 @@ theorem spec {C : CostModel} (xs ys : BufId) (aX aY : Array (Word w)) /-- `⟨1,2,3⟩ · ⟨4,5,6⟩ = 32`: `(value, time, net, peak)`, with time `29 = timeBound .unit 3`, an instance of `spec`. -/ def demo : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 1000 (code 0 1) + (run .unit Caliper.RandomTape.zero 1000 (code 0 1) { State.init 64 with bufs := fun b => if b = 0 then #[1, 2, 3] else if b = 1 then #[4, 5, 6] else #[] caps := fun b => if b = 0 ∨ b = 1 then 3 else 0 }).map @@ -230,10 +230,10 @@ is instantiated with the *value* of `r1`: each iteration replaces it by `a % b < `0 < w` keeps the flag readable, 1 being 0 in a 0-bit word. Time-only judgment; the memory side is below. -/ theorem time_spec {C : CostModel} (hw : 0 < w) (a b : Word w) : - TimeTriple C (fun s => s.regs 0 = a ∧ s.regs 1 = b) (code (w := w)) + TimeTriple C Caliper.RandomTape.zero (fun s => s.regs 0 = a ∧ s.regs 1 = b) (code (w := w)) (fun s => (s.regs 0).toNat = Nat.gcd a.toNat b.toNat) (timeBound C b.toNat) := by - have hguard : ∀ k, TimeTriple C (Inv a b k) (.un .isNonZero 2 1) + have hguard : ∀ k, TimeTriple C Caliper.RandomTape.zero (Inv a b k) (.un .isNonZero 2 1) (InvG a b k) (C.un .isNonZero) := by intro k apply TimeTriple.un @@ -249,7 +249,7 @@ theorem time_spec {C : CostModel} (hw : 0 < w) (a b : Word w) : exact hnz hflag have := toNat_ne_zero hb exact ⟨k - 1, by omega⟩ - have hbody : ∀ k, TimeTriple C (fun (s : State w) => InvG a b (k + 1) s ∧ s.regs 2 ≠ 0) + have hbody : ∀ k, TimeTriple C Caliper.RandomTape.zero (fun (s : State w) => InvG a b (k + 1) s ∧ s.regs 2 ≠ 0) (.bin .umod 3 0 1 ;; .mov 0 1 ;; .mov 1 3) (Inv a b k) (C.bin .umod + (C.mov + C.mov)) := by rintro k s ⟨⟨⟨hg, hk⟩, hflag⟩, hnz⟩ @@ -291,7 +291,7 @@ theorem time_spec {C : CostModel} (hw : 0 < w) (a b : Word w) : /-- The full triple: the time proof above recombined, by determinism, with the free space triple, the code containing no allocation. -/ theorem spec {C : CostModel} (hw : 0 < w) (a b : Word w) : - Triple C (fun s => s.regs 0 = a ∧ s.regs 1 = b) (code (w := w)) + Triple C Caliper.RandomTape.zero (fun s => s.regs 0 = a ∧ s.regs 1 = b) (code (w := w)) (fun s => (s.regs 0).toNat = Nat.gcd a.toNat b.toNat) (timeBound C b.toNat) 0 0 := (time_spec hw a b).and_space' @@ -300,7 +300,7 @@ theorem spec {C : CostModel} (hw : 0 < w) (a b : Word w) : /-- `gcd 252 105 = 21` in 17 unit steps: 4 guard evaluations, the last seeing `b = 0`, and 3 bodies. An instance of `spec`. -/ def demo : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 1000 (code (w := 64)) + (run .unit Caliper.RandomTape.zero 1000 (code (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 252 else if r = 1 then 105 else 0 }).map fun (s, t, d, p) => (s.regs 0, t, d, p) @@ -355,7 +355,7 @@ def code : Stmt w := exponent 13 = 0b1101 drives 4 iterations, 3 of them through the multiply branch, so the time is data-dependent. -/ def demo : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 1000 (code (w := 64)) + (run .unit Caliper.RandomTape.zero 1000 (code (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 3 else if r = 1 then 13 else 0 }).map fun (s, t, d, p) => (s.regs 2, t, d, p) @@ -393,7 +393,7 @@ def code : Stmt w := /-- `popcount 0xDEADBEEF = 24`: `(count, time, net, peak)`, 32 iterations, the position of the highest set bit. -/ def demo : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 1000 (code (w := 64)) + (run .unit Caliper.RandomTape.zero 1000 (code (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 0xDEADBEEF else 0 }).map fun (s, t, d, p) => (s.regs 1, t, d, p) @@ -438,7 +438,7 @@ def code : Stmt w := /-- `a = 2^64 - 1`, `b = 10`: `(q, r, ok, mulhi)`, with the identity flag 1 and the widening product's high word 9. -/ def demo : Option (Word 64 × Word 64 × Word 64 × Word 64) := - (run .unit 100 (code (w := 64)) + (run .unit Caliper.RandomTape.zero 100 (code (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 0xFFFFFFFFFFFFFFFF else if r = 1 then 10 else 0 }).map fun (s, _, _, _) => (s.regs 2, s.regs 3, s.regs 5, s.regs 6) @@ -451,7 +451,7 @@ def demo : Option (Word 64 × Word 64 × Word 64 × Word 64) := recomposition identity still holds. RISC-V's `DIVU` returns all-ones here, so the lowering bridges that; `REMU` already matches. -/ def demoZero : Option (Word 64 × Word 64 × Word 64) := - (run .unit 100 (code (w := 64)) + (run .unit Caliper.RandomTape.zero 100 (code (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 5 else 0 }).map fun (s, _, _, _) => (s.regs 2, s.regs 3, s.regs 5) @@ -488,9 +488,9 @@ def minCode : Stmt w := /-- `min(1000, 37) = 37` and `min(37, 1000) = 37`: the two orders cost the same 5 instructions, straight-line code being constant-time by construction. -/ def minDemo : Option (Word 64 × Word 64) := do - let (s₁, _, _, _) ← run .unit 100 (minCode (w := 64)) + let (s₁, _, _, _) ← run .unit Caliper.RandomTape.zero 100 (minCode (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 1000 else if r = 1 then 37 else 0 } - let (s₂, _, _, _) ← run .unit 100 (minCode (w := 64)) + let (s₂, _, _, _) ← run .unit Caliper.RandomTape.zero 100 (minCode (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 37 else if r = 1 then 1000 else 0 } return (s₁.regs 5, s₂.regs 5) @@ -514,7 +514,7 @@ def isPow2Code : Stmt w := /-- `(isPow2 64, isPow2 96, isPow2 0)` = `(1, 0, 0)`. -/ def isPow2Demo : Option (Word 64 × Word 64 × Word 64) := do let go (x : Word 64) : Option (Word 64) := - (run .unit 100 (isPow2Code (w := 64)) + (run .unit Caliper.RandomTape.zero 100 (isPow2Code (w := 64)) { State.init 64 with regs := fun r => if r = 0 then x else 0 }).map fun (s, _, _, _) => s.regs 5 return (← go 64, ← go 96, ← go 0) @@ -540,7 +540,7 @@ def packCode : Stmt w := /-- `(packed, ok')` for `hi = 0xDEAD`, `lo = 0xBEEF`. -/ def packDemo : Option (Word 64 × Word 64) := - (run .unit 100 (packCode (w := 64)) + (run .unit Caliper.RandomTape.zero 100 (packCode (w := 64)) { State.init 64 with regs := fun r => if r = 0 then 0xDEAD else if r = 1 then 0xBEEF else 0 }).map fun (s, _, _, _) => (s.regs 4, s.regs 7) diff --git a/Caliper/Corpus/Memory.lean b/Caliper/Corpus/Memory.lean index 72cc8fb..6c1df11 100644 --- a/Caliper/Corpus/Memory.lean +++ b/Caliper/Corpus/Memory.lean @@ -108,12 +108,12 @@ untouched, in time `timeBound C arr.size`, with net and peak live-memory growth `dst ≠ src` is the one separation fact, a statement about buffer *names*. -/ theorem spec {C : CostModel} (src dst : BufId) (hne : dst ≠ src) (arr : Array (Word w)) (hsz : arr.size < 2 ^ w) : - Triple C (fun s => s.bufs src = arr) (code src dst) + Triple C Caliper.RandomTape.zero (fun s => s.bufs src = arr) (code src dst) (fun s => s.bufs dst = arr ∧ s.bufs src = arr) (timeBound C arr.size) arr.size arr.size := by have hne' : src ≠ dst := fun h => hne h.symm -- the guard: one `ult`, verdict in r2 - have hguard : ∀ k, Triple C (Inv src dst arr k) (.bin .ult 2 0 1) + have hguard : ∀ k, Triple C Caliper.RandomTape.zero (Inv src dst arr k) (.bin .ult 2 0 1) (InvG src dst arr k) (C.bin .ult) 0 0 := by intro k apply Triple.bin @@ -131,7 +131,7 @@ theorem spec {C : CostModel} (src dst : BufId) (hne : dst ≠ src) have hlt := cond_of_flag_ne hflag hnz exact ⟨k - 1, by omega⟩ -- the body: load, push, increment - have hbody : ∀ k, Triple C (fun s => InvG src dst arr (k + 1) s ∧ s.regs 2 ≠ 0) + have hbody : ∀ k, Triple C Caliper.RandomTape.zero (fun s => InvG src dst arr (k + 1) s ∧ s.regs 2 ≠ 0) (.memLoad 3 src 0 ;; .memPush dst 3 ;; .imm 4 1 ;; .bin .add 0 0 4) (Inv src dst arr k) (C.memLoad + (C.memPush + (C.imm + C.bin .add))) 0 0 := by @@ -154,11 +154,11 @@ theorem spec {C : CostModel} (src dst : BufId) (hne : dst ≠ src) simp [prefixOf, hlt, hsrc] · simp [hcap] -- prologue: read the length, allocate, zero the index - have h1 : Triple C (fun s => s.bufs src = arr) (.memLen 1 src) + have h1 : Triple C Caliper.RandomTape.zero (fun s => s.bufs src = arr) (.memLen 1 src) (fun s => s.bufs src = arr ∧ s.regs 1 = BitVec.ofNat w arr.size) C.memLen 0 0 := Triple.memLen fun s hs => by simp [hs] - have h2 : Triple C + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.bufs src = arr ∧ s.regs 1 = BitVec.ofNat w arr.size) (.memAlloc dst 1) (fun s => s.bufs src = arr ∧ s.regs 1 = BitVec.ofNat w arr.size @@ -174,7 +174,7 @@ theorem spec {C : CostModel} (src dst : BufId) (hne : dst ≠ src) · simp [hlen] · simp [hval] · simp - have h3 : Triple C + have h3 : Triple C Caliper.RandomTape.zero (fun s => s.bufs src = arr ∧ s.regs 1 = BitVec.ofNat w arr.size ∧ s.caps dst = arr.size ∧ s.bufs dst = #[]) (.imm 0 0) (Inv src dst arr arr.size) C.imm 0 0 := by @@ -204,7 +204,7 @@ theorem spec {C : CostModel} (src dst : BufId) (hne : dst ≠ src) `(dst contents, time, net, peak)`, with time `25 = timeBound .unit 3` and memory `(3, 3)`, instances of `spec`. -/ def demo : Option (Array (Word 64) × ℕ × ℤ × ℤ) := - (run .unit 1000 (code 0 1) + (run .unit Caliper.RandomTape.zero 1000 (code 0 1) { State.init 64 with bufs := fun b => if b = 0 then #[7, 11, 13] else #[] caps := fun b => if b = 0 then 3 else 0 }).map @@ -244,7 +244,7 @@ def code (b : BufId) : Stmt w := /-- Overwrite `#[1, 2, 3, 4]` with the value 9 from `r5`: `(contents, time, net, peak)`: zero memory, in place. -/ def demo : Option (Array (Word 64) × ℕ × ℤ × ℤ) := - (run .unit 1000 (code 0) + (run .unit Caliper.RandomTape.zero 1000 (code 0) { State.init 64 with regs := fun r => if r = 5 then 9 else 0 bufs := fun b => if b = 0 then #[1, 2, 3, 4] else #[] @@ -289,7 +289,7 @@ def code (b : BufId) : Stmt w := /-- Reverse `#[1, 2, 3, 4, 5]` in place: `(contents, time, net, peak)`. -/ def demo : Option (Array (Word 64) × ℕ × ℤ × ℤ) := - (run .unit 1000 (code 0) + (run .unit Caliper.RandomTape.zero 1000 (code 0) { State.init 64 with bufs := fun b => if b = 0 then #[1, 2, 3, 4, 5] else #[] caps := fun b => if b = 0 then 5 else 0 }).map @@ -334,7 +334,7 @@ def code (b : BufId) : Stmt w := sum is 17 and the buffer ends empty with its 3-word capacity credited back (net −3). -/ def demo : Option (Word 64 × ℕ × ℕ × ℕ × ℤ × ℤ) := - (run .unit 1000 (code 0) + (run .unit Caliper.RandomTape.zero 1000 (code 0) { State.init 64 with bufs := fun b => if b = 0 then #[3, 5, 9] else #[] caps := fun b => if b = 0 then 3 else 0 }).map diff --git a/Caliper/Corpus/Sort.lean b/Caliper/Corpus/Sort.lean index 55bbd4b..05b1b80 100644 --- a/Caliper/Corpus/Sort.lean +++ b/Caliper/Corpus/Sort.lean @@ -68,7 +68,7 @@ def code (b : BufId) : Stmt w := /-- Sort a length-6 buffer, returning `(contents, time, net, peak)`. -/ def runOn (arr : Array (Word 64)) : Option (Array (Word 64) × ℕ × ℤ × ℤ) := - (run .unit 100000 (code 0) + (run .unit Caliper.RandomTape.zero 100000 (code 0) { State.init 64 with bufs := fun b => if b = 0 then arr else #[] caps := fun b => if b = 0 then arr.size else 0 }).map @@ -135,7 +135,7 @@ def prog : Stmt 64 := `(result, time, net, peak)`, memory (9, 9): the result buffer, charged once at its immediate allocation. -/ def demo : Option (Array (Word 64) × ℕ × ℤ × ℤ) := - (run .unit 100000 prog + (run .unit Caliper.RandomTape.zero 100000 prog { State.init 64 with bufs := fun b => if b = 0 then #[1, 2, 3, 4, 5, 6, 7, 8, 9] diff --git a/Caliper/Examples.lean b/Caliper/Examples.lean index bd6a828..7acc454 100644 --- a/Caliper/Examples.lean +++ b/Caliper/Examples.lean @@ -80,15 +80,15 @@ def swapCode : Stmt w := .mov 2 0 ;; .mov 0 1 ;; .mov 1 2 /-- Functional spec with time and memory bounds. Note the time bound `3 * C.mov` holds for every input. -/ theorem swapCode_spec {C : CostModel} (a b : Word w) : - Triple C (fun s => s.regs 0 = a ∧ s.regs 1 = b) (swapCode (w := w)) + Triple C Caliper.RandomTape.zero (fun s => s.regs 0 = a ∧ s.regs 1 = b) (swapCode (w := w)) (fun s => s.regs 0 = b ∧ s.regs 1 = a) (3 * C.mov) 0 0 := by - have h1 : Triple C (fun s => s.regs 0 = a ∧ s.regs 1 = b) (.mov 2 0) + have h1 : Triple C Caliper.RandomTape.zero (fun s => s.regs 0 = a ∧ s.regs 1 = b) (.mov 2 0) (fun s => s.regs 1 = b ∧ s.regs 2 = a) C.mov 0 0 := Triple.mov fun s hs => by simp [hs.1, hs.2] - have h2 : Triple C (fun s => s.regs 1 = b ∧ s.regs 2 = a) (.mov 0 1) + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.regs 1 = b ∧ s.regs 2 = a) (.mov 0 1) (fun s => s.regs 0 = b ∧ s.regs 2 = a) C.mov 0 0 := Triple.mov fun s hs => by simp [hs.1, hs.2] - have h3 : Triple C (fun s => s.regs 0 = b ∧ s.regs 2 = a) (.mov 1 2) + have h3 : Triple C Caliper.RandomTape.zero (fun s => s.regs 0 = b ∧ s.regs 2 = a) (.mov 1 2) (fun s => s.regs 0 = b ∧ s.regs 1 = a) C.mov 0 0 := Triple.mov fun s hs => by simp [hs.1, hs.2] exact (h1.seq (h2.seq h3)).conseq (fun _ h => h) (fun _ h => h) @@ -97,7 +97,7 @@ theorem swapCode_spec {C : CostModel} (a b : Word w) : /-- The time is not merely bounded; it is *equal* to the syntactic constant, on every input. This is what gives "unit time per instruction" its meaning. -/ theorem swapCode_time {C : CostModel} {s s' : State w} {t : ℕ} {d p : ℤ} - (h : Exec C swapCode s s' t d p) : t = 3 * C.mov := by + (h : Exec C Caliper.RandomTape.zero swapCode s s' t d p) : t = 3 * C.mov := by have := h.straight_time_eq ⟨trivial, trivial, trivial⟩ simp only [swapCode, Stmt.staticTime] at this omega @@ -105,8 +105,8 @@ theorem swapCode_time {C : CostModel} {s s' : State w} {t : ℕ} {d p : ℤ} /-- Constant-time in the side-channel sense: two runs on unrelated inputs cost the same. -/ theorem swapCode_data_independent {C : CostModel} {s₁ s₁' s₂ s₂' : State w} - {t₁ t₂ : ℕ} {d₁ p₁ d₂ p₂ : ℤ} (h₁ : Exec C swapCode s₁ s₁' t₁ d₁ p₁) - (h₂ : Exec C swapCode s₂ s₂' t₂ d₂ p₂) : t₁ = t₂ := + {t₁ t₂ : ℕ} {d₁ p₁ d₂ p₂ : ℤ} (h₁ : Exec C Caliper.RandomTape.zero swapCode s₁ s₁' t₁ d₁ p₁) + (h₂ : Exec C Caliper.RandomTape.zero swapCode s₂ s₂' t₂ d₂ p₂) : t₁ = t₂ := h₁.straight_data_independent h₂ ⟨trivial, trivial, trivial⟩ /-- `mulhi` sanity check: the high word of `2^63 * 4` is `2`. -/ @@ -165,11 +165,11 @@ for any cost model. The `arr.size < 2 ^ w` assumption is what makes the index increment wrap-free. -/ theorem spec {C : CostModel} (xs : BufId) (arr : Array (Word w)) (hsz : arr.size < 2 ^ w) : - Triple C (fun s => s.bufs xs = arr) (code xs) + Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = arr) (code xs) (fun s => s.regs 0 = sumTo arr arr.size) (timeBound C arr.size) 0 0 := by -- the guard: one `ult`, leaving the verdict in r3 - have hguard : ∀ k, Triple C (Inv xs arr k) (.bin .ult 3 1 2) (InvG xs arr k) + have hguard : ∀ k, Triple C Caliper.RandomTape.zero (Inv xs arr k) (.bin .ult 3 1 2) (InvG xs arr k) (C.bin .ult) 0 0 := by intro k apply Triple.bin @@ -186,7 +186,7 @@ theorem spec {C : CostModel} (xs : BufId) (arr : Array (Word w)) have hlt := cond_of_flag_ne hflag hnz exact ⟨k - 1, by omega⟩ -- the body: read, accumulate, increment - have hbody : ∀ k, Triple C (fun s => InvG xs arr (k + 1) s ∧ s.regs 3 ≠ 0) + have hbody : ∀ k, Triple C Caliper.RandomTape.zero (fun s => InvG xs arr (k + 1) s ∧ s.regs 3 ≠ 0) (.memLoad 4 xs 1 ;; .bin .add 0 0 4 ;; .imm 5 1 ;; .bin .add 1 1 5) (Inv xs arr k) (C.memLoad + (C.bin .add + (C.imm + C.bin .add))) 0 0 := by @@ -204,13 +204,13 @@ theorem spec {C : CostModel} (xs : BufId) (arr : Array (Word w)) rw [toNat_add_ofNat_one hlt hsz] simp [sumTo, hlt, hacc] -- prologue - have h1 : Triple C (fun s => s.bufs xs = arr) (.imm 0 0) + have h1 : Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = arr) (.imm 0 0) (fun s => s.bufs xs = arr ∧ s.regs 0 = 0) C.imm 0 0 := Triple.imm fun s hs => by simp [hs] - have h2 : Triple C (fun s => s.bufs xs = arr ∧ s.regs 0 = 0) (.imm 1 0) + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = arr ∧ s.regs 0 = 0) (.imm 1 0) (fun s => s.bufs xs = arr ∧ s.regs 0 = 0 ∧ s.regs 1 = 0) C.imm 0 0 := Triple.imm fun s hs => by simp [hs.1, hs.2] - have h3 : Triple C (fun s => s.bufs xs = arr ∧ s.regs 0 = 0 ∧ s.regs 1 = 0) + have h3 : Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = arr ∧ s.regs 0 = 0 ∧ s.regs 1 = 0) (.memLen 2 xs) (Inv xs arr arr.size) C.memLen 0 0 := by apply Triple.memLen rintro s ⟨hb, h0, h1'⟩ @@ -234,7 +234,7 @@ theorem spec {C : CostModel} (xs : BufId) (arr : Array (Word w)) /-- The bound specialized to the uniform cost model: `6n + 5` steps. -/ theorem spec_unit (xs : BufId) (arr : Array (Word w)) (hsz : arr.size < 2 ^ w) : - Triple .unit (fun s => s.bufs xs = arr) (code xs) + Triple .unit Caliper.RandomTape.zero (fun s => s.bufs xs = arr) (code xs) (fun s => s.regs 0 = sumTo arr arr.size) (6 * arr.size + 5) 0 0 := (spec xs arr hsz).weaken (by unfold timeBound CostModel.unit; simp; omega) (le_refl _) (le_refl _) @@ -294,10 +294,10 @@ allocation: net and peak are both `n`. The capacity is *dynamic* (read from `r2` so the allocation's per-word time charge is data-dependent and enters the bound as `n * C.allocPerWord` through the capacity bound of `Triple.memAlloc`. -/ theorem spec {C : CostModel} (b : BufId) (n : ℕ) (hn : n < 2 ^ w) : - Triple C (fun s => s.regs 2 = BitVec.ofNat w n) (code b) + Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (code b) (fun s => s.bufs b = iotaTo w n) (timeBound C n) n n := by - have hguard : ∀ k, Triple C (Inv (w := w) b n k) (.bin .ult 1 0 2) + have hguard : ∀ k, Triple C Caliper.RandomTape.zero (Inv (w := w) b n k) (.bin .ult 1 0 2) (InvG (w := w) b n k) (C.bin .ult) 0 0 := by intro k apply Triple.bin @@ -312,7 +312,7 @@ theorem spec {C : CostModel} (b : BufId) (n : ℕ) (hn : n < 2 ^ w) : rintro k s ⟨⟨hlim, hik, hbuf, hcap⟩, hflag⟩ hnz have hlt := cond_of_flag_ne hflag hnz exact ⟨k - 1, by omega⟩ - have hbody : ∀ k, Triple C (fun (s : State w) => InvG b n (k + 1) s ∧ s.regs 1 ≠ 0) + have hbody : ∀ k, Triple C Caliper.RandomTape.zero (fun (s : State w) => InvG b n (k + 1) s ∧ s.regs 1 ≠ 0) (.memPush b 0 ;; .imm 3 1 ;; .bin .add 0 0 3) (Inv b n k) (C.memPush + (C.imm + C.bin .add)) 0 0 := by @@ -331,7 +331,7 @@ theorem spec {C : CostModel} (b : BufId) (n : ℕ) (hn : n < 2 ^ w) : rw [toNat_add_ofNat_one hlt hn] simp [iotaTo] · simp [hcap] - have h1 : Triple C (fun s => s.regs 2 = BitVec.ofNat w n) (.memAlloc b 2) + have h1 : Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (.memAlloc b 2) (fun s => s.regs 2 = BitVec.ofNat w n ∧ s.caps b = n ∧ s.bufs b = #[]) (C.memAlloc + n * C.allocPerWord) n n := by apply Triple.memAlloc @@ -343,7 +343,7 @@ theorem spec {C : CostModel} (b : BufId) (n : ℕ) (hn : n < 2 ^ w) : · simp [hs] · simp [hval] · simp - have h2 : Triple C + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n ∧ s.caps b = n ∧ s.bufs b = #[]) (.imm 0 0) (Inv b n n) C.imm 0 0 := by apply Triple.imm @@ -413,10 +413,10 @@ def timeBound (C : CostModel) (n : ℕ) : ℕ := /-- Linear time, net memory 0 and peak memory 1, for any `n`. -/ theorem spec {C : CostModel} (sb : BufId) (n : ℕ) (hn : n < 2 ^ w) : - Triple C (fun s => s.regs 2 = BitVec.ofNat w n) (code sb) + Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (code sb) (fun s => s.bufs sb = #[] ∧ s.caps sb = 0) (timeBound C n) 0 1 := by - have hguard : ∀ k, Triple C (Inv (w := w) sb n k) (.bin .ult 1 0 2) + have hguard : ∀ k, Triple C Caliper.RandomTape.zero (Inv (w := w) sb n k) (.bin .ult 1 0 2) (InvG (w := w) sb n k) (C.bin .ult) 0 0 := by intro k apply Triple.bin @@ -431,7 +431,7 @@ theorem spec {C : CostModel} (sb : BufId) (n : ℕ) (hn : n < 2 ^ w) : rintro k s ⟨⟨hlim, hik, hbuf, hcap⟩, hflag⟩ hnz have hlt := cond_of_flag_ne hflag hnz exact ⟨k - 1, by omega⟩ - have hbody : ∀ k, Triple C (fun (s : State w) => InvG sb n (k + 1) s ∧ s.regs 1 ≠ 0) + have hbody : ∀ k, Triple C Caliper.RandomTape.zero (fun (s : State w) => InvG sb n (k + 1) s ∧ s.regs 1 ≠ 0) (.memPush sb 0 ;; .memPop sb ;; .imm 3 1 ;; .bin .add 0 0 3) (Inv sb n k) (C.memPush + (C.memPop + (C.imm + C.bin .add))) 0 0 := by @@ -448,7 +448,7 @@ theorem spec {C : CostModel} (sb : BufId) (n : ℕ) (hn : n < 2 ^ w) : omega · simp [hbuf] · simp [hcap] - have h1 : Triple C + have h1 : Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (.memAllocI sb 1) (fun s => s.regs 2 = BitVec.ofNat w n ∧ s.caps sb = 1 ∧ s.bufs sb = #[]) @@ -459,7 +459,7 @@ theorem spec {C : CostModel} (sb : BufId) (n : ℕ) (hn : n < 2 ^ w) : · simp [hlim] · simp · simp - have h2 : Triple C + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n ∧ s.caps sb = 1 ∧ s.bufs sb = #[]) (.imm 0 0) (Inv sb n n) C.imm 0 0 := by apply Triple.imm @@ -470,7 +470,7 @@ theorem spec {C : CostModel} (sb : BufId) (n : ℕ) (hn : n < 2 ^ w) : · simp [hbuf] · simp [hcap] have hW := Triple.whileNZ_measure hguard hpos hbody n - have hF : Triple C (fun s => ∃ k', InvG (w := w) sb n k' s ∧ s.regs 1 = 0) + have hF : Triple C Caliper.RandomTape.zero (fun s => ∃ k', InvG (w := w) sb n k' s ∧ s.regs 1 = 0) (.memFree sb) (fun s => s.bufs sb = #[] ∧ s.caps sb = 0) C.memFree (-(1 : ℤ)) 0 := by apply Triple.memFree' (K := 1) @@ -500,7 +500,7 @@ def code (xs ys : BufId) : Stmt w := theorem spec {C : CostModel} (xs ys : BufId) (arrX arrY : Array (Word w)) (hx : arrX.size < 2 ^ w) (hy : arrY.size < 2 ^ w) : - Triple C (fun s => s.bufs xs = arrX ∧ s.bufs ys = arrY) (code xs ys) + Triple C Caliper.RandomTape.zero (fun s => s.bufs xs = arrX ∧ s.bufs ys = arrY) (code xs ys) (fun s => s.regs 0 = SumBuf.sumTo arrY arrY.size + SumBuf.sumTo arrX arrX.size) (SumBuf.timeBound C arrX.size + SumBuf.timeBound C arrY.size + C.mov + C.bin .add) 0 0 := by @@ -508,7 +508,7 @@ theorem spec {C : CostModel} (xs ys : BufId) have h1 := (SumBuf.spec (C := C) xs arrX hx).frame_buf (b := ys) (arr := arrY) (by simp [SumBuf.code, Stmt.Touches]) -- save the result - have h2 : Triple C + have h2 : Triple C Caliper.RandomTape.zero (fun s => s.regs 0 = SumBuf.sumTo arrX arrX.size ∧ s.bufs ys = arrY) (.mov 6 0) (fun s => s.bufs ys = arrY ∧ s.regs 6 = SumBuf.sumTo arrX arrX.size) @@ -518,7 +518,7 @@ theorem spec {C : CostModel} (xs ys : BufId) have h3 := (SumBuf.spec (C := C) ys arrY hy).frame_reg (r := 6) (v := SumBuf.sumTo arrX arrX.size) (by simp [SumBuf.code, Stmt.Writes]) -- combine - have h4 : Triple C + have h4 : Triple C Caliper.RandomTape.zero (fun s => s.regs 0 = SumBuf.sumTo arrY arrY.size ∧ s.regs 6 = SumBuf.sumTo arrX arrX.size) (.bin .add 0 0 6) @@ -570,9 +570,9 @@ def timeBound (C : CostModel) (n : ℕ) : ℕ := /-- A pure running-time bound: the same measure-indexed loop argument as `SumBuf.spec`, through `TimeTriple`, with no memory quantity mentioned anywhere. -/ theorem time_spec {C : CostModel} (n : ℕ) (hn : n < 2 ^ w) : - TimeTriple C (fun s => s.regs 2 = BitVec.ofNat w n) (code (w := w)) + TimeTriple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (code (w := w)) (fun s => (s.regs 0).toNat = n) (timeBound C n) := by - have hguard : ∀ k, TimeTriple C (Inv (w := w) n k) (.bin .ult 1 0 2) + have hguard : ∀ k, TimeTriple C Caliper.RandomTape.zero (Inv (w := w) n k) (.bin .ult 1 0 2) (InvG (w := w) n k) (C.bin .ult) := by intro k apply TimeTriple.bin @@ -585,7 +585,7 @@ theorem time_spec {C : CostModel} (n : ℕ) (hn : n < 2 ^ w) : rintro k s ⟨⟨hlim, hik⟩, hflag⟩ hnz have hlt := cond_of_flag_ne hflag hnz exact ⟨k - 1, by omega⟩ - have hbody : ∀ k, TimeTriple C (fun (s : State w) => InvG n (k + 1) s ∧ s.regs 1 ≠ 0) + have hbody : ∀ k, TimeTriple C Caliper.RandomTape.zero (fun (s : State w) => InvG n (k + 1) s ∧ s.regs 1 ≠ 0) (.imm 3 1 ;; .bin .add 0 0 3) (Inv n k) (C.imm + C.bin .add) := by rintro k s ⟨⟨⟨hlim, hik⟩, hflag⟩, hnz⟩ have hlt : (s.regs 0).toNat < n := cond_of_flag_ne hflag hnz @@ -594,7 +594,7 @@ theorem time_spec {C : CostModel} (n : ℕ) (hn : n < 2 ^ w) : · simp [-BitVec.toNat_add] rw [toNat_add_ofNat_one hlt hn] omega - have h1 : TimeTriple C (fun s => s.regs 2 = BitVec.ofNat w n) (.imm 0 0) + have h1 : TimeTriple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (.imm 0 0) (Inv n n) C.imm := TimeTriple.imm fun s hs => ⟨by simp [hs], by simp⟩ have hW := TimeTriple.whileNZ_measure hguard hpos hbody n @@ -609,7 +609,7 @@ theorem time_spec {C : CostModel} (n : ℕ) (hn : n < 2 ^ w) : /-- Recombined: the time-only proof above, and a space triple obtained for free (`code` contains no `memAlloc`), glued into a full `Triple` by determinism. -/ theorem spec {C : CostModel} (n : ℕ) (hn : n < 2 ^ w) : - Triple C (fun s => s.regs 2 = BitVec.ofNat w n) (code (w := w)) + Triple C Caliper.RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat w n) (code (w := w)) (fun s => (s.regs 0).toNat = n) (timeBound C n) 0 0 := (time_spec n hn).and_space' ((time_spec n hn).space_of_allocFree ⟨trivial, trivial, trivial, trivial⟩) @@ -636,8 +636,8 @@ def InvG (b : BufId) (k : ℕ) (s : State w) : Prop := loop runs longer than any given time bound (`no_time_bound`). The measure, the buffer length, still drives the induction; it never appears in the bounds. -/ theorem space_spec {C : CostModel} (b : BufId) : - SpaceTriple C (fun _ => True) (code (w := w) b) (fun _ => True) 0 0 := by - have hguard : ∀ k, SpaceTriple C (Inv (w := w) b k) (.memLen 1 b) + SpaceTriple C Caliper.RandomTape.zero (fun _ => True) (code (w := w) b) (fun _ => True) 0 0 := by + have hguard : ∀ k, SpaceTriple C Caliper.RandomTape.zero (Inv (w := w) b k) (.memLen 1 b) (InvG (w := w) b k) 0 0 := by intro k apply SpaceTriple.memLen @@ -647,7 +647,7 @@ theorem space_spec {C : CostModel} (b : BufId) : rintro (_ | k) s ⟨_, hflag⟩ hnz · exact absurd (hflag.trans (by simp)) hnz · exact ⟨k, rfl⟩ - have hbody : ∀ k, SpaceTriple C (fun (s : State w) => InvG b (k + 1) s ∧ s.regs 1 ≠ 0) + have hbody : ∀ k, SpaceTriple C Caliper.RandomTape.zero (fun (s : State w) => InvG b (k + 1) s ∧ s.regs 1 ≠ 0) (.memPop b) (Inv b k) 0 0 := by intro k apply SpaceTriple.memPop @@ -675,7 +675,7 @@ private theorem ofNat_eq_zero_iff {n : ℕ} (hn : n < 2 ^ w) : steps under the unit cost model. (The hypothesis keeps the length register from wrapping; it is preserved as the buffer shrinks.) -/ private theorem time_lower {b : BufId} {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (h : Exec .unit c s s' t d p) + {d p : ℤ} (h : Exec .unit Caliper.RandomTape.zero c s s' t d p) (hc : c = .whileNZ (.memLen 1 b) 1 (.memPop b)) (hsz : (s.bufs b).size < 2 ^ w) : (s.bufs b).size ≤ t := by induction h with @@ -702,7 +702,7 @@ private theorem time_lower {b : BufId} {c : Stmt w} {s s' : State w} {t : ℕ} in a word is beaten by starting with a buffer of length `T + 1`. Contrast `space_spec`, which holds with bounds `0`/`0` for the same trivial precondition. -/ theorem no_time_bound (b : BufId) (T : ℕ) (hT : T + 1 < 2 ^ w) : - ¬ TimeTriple .unit (fun _ => True) (code (w := w) b) (fun _ => True) T := by + ¬ TimeTriple .unit Caliper.RandomTape.zero (fun _ => True) (code (w := w) b) (fun _ => True) T := by intro h obtain ⟨s', t, d, p, hexec, -, ht⟩ := h { State.init w with @@ -792,7 +792,7 @@ def code : Stmt 64 := the program allocating nothing. The register side is the inferred `regPeak₀ = 2`; the combined statement is `ScopedSumSq.total_space` in `Liveness.lean`. -/ theorem space_spec {C : CostModel} : - SpaceTriple C (fun _ => True) code (fun _ => True) 0 0 := by + SpaceTriple C Caliper.RandomTape.zero (fun _ => True) code (fun _ => True) 0 0 := by intro s _ refine ⟨_, _, _, _, .seq .imm (.seq .bin (.seq .imm (.seq .bin .bin))), trivial, ?_, ?_⟩ <;> simp @@ -811,7 +811,7 @@ add r4, r1, r3 /-- Value `3² + 4² = 25`, realized: unit time 5 (five ALU/imm instructions), buffers-only memory (0, 0). -/ def demo : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 100 code (State.init 64)).map fun (s, t, d, p) => (s.regs 4, t, d, p) + (run .unit Caliper.RandomTape.zero 100 code (State.init 64)).map fun (s, t, d, p) => (s.regs 4, t, d, p) /-- info: some (25#64, 5, 0, 0) -/ #guard_msgs in @@ -844,7 +844,7 @@ add r2, r1, r1 /-- Value `3² + 3² = 18`; unit time 3; buffers-only memory (0, 0). -/ def nestedDemo : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 100 (Build.build nestedB).2 (State.init 64)).map + (run .unit Caliper.RandomTape.zero 100 (Build.build nestedB).2 (State.init 64)).map fun (s, t, d, p) => (s.regs 2, t, d, p) /-- info: some (18#64, 3, 0, 0) -/ @@ -867,16 +867,16 @@ def demoState : State 64 := /-- Sum: expect value 17, time 23, memory (0, 0). -/ def demoSum : Option (Word 64 × ℕ × ℤ × ℤ) := - (run .unit 1000 (SumBuf.code 0) demoState).map fun (s, t, d, p) => (s.regs 0, t, d, p) + (run .unit Caliper.RandomTape.zero 1000 (SumBuf.code 0) demoState).map fun (s, t, d, p) => (s.regs 0, t, d, p) /-- Iota 5: expect buffer `#[0,1,2,3,4]`, memory (5, 5). -/ def demoIota : Option (Array (Word 64) × ℕ × ℤ × ℤ) := - (run .unit 1000 (Iota.code 0) + (run .unit Caliper.RandomTape.zero 1000 (Iota.code 0) ((State.init 64).setReg 2 5)).map fun (s, t, d, p) => (s.bufs 0, t, d, p) /-- Scratch loop, 100 iterations: expect net 0, peak 1. -/ def demoScratch : Option (ℕ × ℤ × ℤ) := - (run .unit 2000 (ScratchLoop.code 0) + (run .unit Caliper.RandomTape.zero 2000 (ScratchLoop.code 0) ((State.init 64).setReg 2 100)).map fun (_, t, d, p) => (t, d, p) /-- info: some (17#64, 23, 0, 0) -/ @@ -913,7 +913,7 @@ def pairProg : ℕ × Stmt 64 := Build.var ((x : Exp 64) + y) def pairDemo : Option (Word 64 × ℤ × ℤ) := - (run .unit 1000 pairProg.2 (State.init 64)).map + (run .unit Caliper.RandomTape.zero 1000 pairProg.2 (State.init 64)).map fun (s, _, d, p) => (s.regs pairProg.1, d, p) /-- info: some (50#64, 4, 4) -/ diff --git a/Caliper/Geometric.lean b/Caliper/Geometric.lean new file mode 100644 index 0000000..049dd0d --- /dev/null +++ b/Caliper/Geometric.lean @@ -0,0 +1,55 @@ +import Caliper.PMF +import Mathlib.Analysis.SpecificLimits.Basic +import Mathlib.Topology.Algebra.InfiniteSum.Ring + +/-! Geometric series used to account for unbounded retry costs. -/ +open scoped ENNReal + +namespace Caliper + +/-- The expected attempt count is a double geometric sum. This identity is valid +also at the extended endpoints, with the usual `0 * ∞ = 0` convention. -/ +theorem tsum_succ_mul_geometric (r : ℝ≥0∞) : + (∑' n : ℕ, (n + 1 : ℝ≥0∞) * r ^ n) = (1 - r)⁻¹ * (1 - r)⁻¹ := by + rw [← ENNReal.tsum_geometric, ← ENNReal.tsum_mul_left] + simp_rw [← ENNReal.tsum_mul_right] + rw [← ENNReal.tsum_prod, + ← Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.tsum_eq + (fun p : ℕ × ℕ => r ^ p.2 * r ^ p.1)] + change _ = ∑' c : (n : ℕ) × ↥(Finset.antidiagonal n), r ^ c.2.val.2 * r ^ c.2.val.1 + rw [ENNReal.tsum_sigma (fun (n : ℕ) (p : ↥(Finset.antidiagonal n)) => r ^ p.val.2 * r ^ p.val.1)] + apply tsum_congr + intro n + simp only [tsum_fintype, ← pow_add] + have hpow (p : ↥(Finset.antidiagonal n)) : r ^ (p.val.2 + p.val.1) = r ^ n := by + rw [Nat.add_comm, Finset.mem_antidiagonal.mp p.property] + simp_rw [hpow] + simp [nsmul_eq_mul] + +/-- Total mass of a geometric first-hit law with success chance `1/N`. -/ +theorem geometric_mass (N : ℕ) (hN : 0 < N) : + (∑' n : ℕ, (1 - (N : ℝ≥0∞)⁻¹) ^ n * (N : ℝ≥0∞)⁻¹) = 1 := by + have hq : (N : ℝ≥0∞)⁻¹ ≤ 1 := ENNReal.inv_le_one.mpr (by exact_mod_cast hN) + rw [ENNReal.tsum_mul_right, ENNReal.tsum_geometric, + ENNReal.sub_sub_cancel (by simp) hq, inv_inv] + exact ENNReal.mul_inv_cancel (by exact_mod_cast (Nat.ne_of_gt hN)) (by simp) + +/-- Constant cost per attempt gives expected total cost `N*K`. -/ +theorem geometric_cost (N K : ℕ) (hN : 0 < N) : + (∑' n : ℕ, (1 - (N : ℝ≥0∞)⁻¹) ^ n * (N : ℝ≥0∞)⁻¹ * + (((n + 1) * K : ℕ) : ℝ≥0∞)) = (N : ℝ≥0∞) * K := by + have hq : (N : ℝ≥0∞)⁻¹ ≤ 1 := ENNReal.inv_le_one.mpr (by exact_mod_cast hN) + have hzero : (N : ℝ≥0∞) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hN) + calc + _ = (∑' n : ℕ, (n + 1 : ℝ≥0∞) * (1 - (N : ℝ≥0∞)⁻¹) ^ n) * + (N : ℝ≥0∞)⁻¹ * K := by + rw [← ENNReal.tsum_mul_right, ← ENNReal.tsum_mul_right] + apply tsum_congr + intro n + push_cast + ac_rfl + _ = _ := by + rw [tsum_succ_mul_geometric, ENNReal.sub_sub_cancel (by simp) hq, inv_inv] + rw [mul_assoc (N : ℝ≥0∞) (N : ℝ≥0∞) _, ENNReal.mul_inv_cancel hzero (by simp), mul_one] + +end Caliper diff --git a/Caliper/Liveness.lean b/Caliper/Liveness.lean index e06d538..b59f3e0 100644 --- a/Caliper/Liveness.lean +++ b/Caliper/Liveness.lean @@ -39,7 +39,7 @@ register slots (register-writing leaves) are disjoint. namespace Caliper -variable {w : ℕ} +variable {w : ℕ} {tape : RandomTape w} /-! ## Per-instruction register footprints -/ @@ -49,6 +49,7 @@ backward dataflow only consults it at leaves. -/ def Stmt.readsSet : Stmt w → Finset ℕ | .skip => ∅ | .seq c₁ c₂ => c₁.readsSet ∪ c₂.readsSet + | .rand _ => ∅ | .imm _ _ => ∅ | .mov _ a => {a} | .un _ _ a => {a} @@ -70,6 +71,7 @@ dataflow only consults leaves. -/ def Stmt.writesSet : Stmt w → Finset ℕ | .skip => ∅ | .seq c₁ c₂ => c₁.writesSet ∪ c₂.writesSet + | .rand d => {d} | .imm d _ => {d} | .mov d _ => {d} | .un _ d _ => {d} @@ -262,6 +264,7 @@ no register and are not counted, which is what lets the straight-line corollary survive 0-cost instructions like `memAllocI _ 0`. -/ def Stmt.writesTotal : Stmt w → ℕ | .seq c₁ c₂ => c₁.writesTotal + c₂.writesTotal + | .rand .. => 1 | .imm .. => 1 | .mov .. => 1 | .un .. => 1 @@ -397,19 +400,19 @@ register liveness is static information, not because they are free. `SpaceBound` packages the sum as the number a space claim should quote, so a buffers-only figure cannot masquerade as "the memory". -/ -/-- `SpaceBound C P c Q M`: from any state satisfying `P`, `c` terminates in a state +/-- `SpaceBound C tape P c Q M`: from any state satisfying `P`, `c` terminates in a state satisfying `Q` with total peak footprint at most `M`, dynamic buffer peak plus the inferred register peak `c.regPeak₀`. The buffer side is an ordinary `SpaceTriple`, the register side a compile-time constant of the code. -/ -def SpaceBound (C : CostModel) (P : State w → Prop) (c : Stmt w) +def SpaceBound (C : CostModel) (tape : RandomTape w) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) (M : ℤ) : Prop := - ∃ D Mbuf : ℤ, SpaceTriple C P c Q D Mbuf ∧ Mbuf + (c.regPeak₀ : ℤ) ≤ M + ∃ D Mbuf : ℤ, SpaceTriple C tape P c Q D Mbuf ∧ Mbuf + (c.regPeak₀ : ℤ) ≤ M /-- Intro rule for `SpaceBound`: a buffer-side `SpaceTriple` plus the register peak, summed. -/ theorem SpaceTriple.spaceBound {C : CostModel} {P Q : State w → Prop} - {c : Stmt w} {D Mbuf M : ℤ} (h : SpaceTriple C P c Q D Mbuf) - (hM : Mbuf + (c.regPeak₀ : ℤ) ≤ M) : SpaceBound C P c Q M := + {c : Stmt w} {D Mbuf M : ℤ} (h : SpaceTriple C tape P c Q D Mbuf) + (hM : Mbuf + (c.regPeak₀ : ℤ) ≤ M) : SpaceBound C tape P c Q M := ⟨D, Mbuf, h, hM⟩ /-! ### Time ≥ total memory, on the straight fragment @@ -433,7 +436,7 @@ def Stmt.allocTotal : Stmt w → ℕ /-- On straight-line code the buffer peak never exceeds the total immediate allocation capacity: a syntactic bound, in any cost model. -/ theorem Exec.straight_peak_le_allocTotal {C : CostModel} {c : Stmt w} - {s s' : State w} {t : ℕ} {d p : ℤ} (h : Exec C c s s' t d p) + {s s' : State w} {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hs : c.Straight) : p ≤ (c.allocTotal : ℤ) := by induction h with | seq h₁ h₂ ih₁ ih₂ => @@ -471,7 +474,7 @@ live-ins by their first-write instructions are disjoint (`Stmt.Straight.allocTotal_add_writesTotal_le_staticTime_unit`), so the sum fits in `t`, not `2t`. -/ theorem Exec.straight_total_footprint_le {c : Stmt w} {s s' : State w} {t : ℕ} - {d p : ℤ} (hexec : Exec CostModel.unit c s s' t d p) (h : c.Straight) : + {d p : ℤ} (hexec : Exec CostModel.unit tape c s s' t d p) (h : c.Straight) : p + (c.regPeak₀ : ℤ) ≤ ((c.liveBefore ∅).card + t : ℤ) := by have h1 := hexec.straight_peak_le_allocTotal h have h2 := c.regPeak_le_card_liveBefore_add_writesTotal ∅ @@ -530,14 +533,14 @@ register peak: the total a space claim should quote. -/ /-- `ScopedSumSq`: buffer peak 0 + register peak 2 = total 2. -/ theorem ScopedSumSq.total_space {C : CostModel} : - SpaceBound C (fun _ => True) Examples.ScopedSumSq.code (fun _ => True) 2 := + SpaceBound C RandomTape.zero (fun _ => True) Examples.ScopedSumSq.code (fun _ => True) 2 := Examples.ScopedSumSq.space_spec.spaceBound (by decide) /-- `SumBuf` (on buffer 0): buffer peak 0 + register peak 6 = total 6, alongside its linear time bound. -/ theorem SumBuf.total_space {C : CostModel} (arr : Array (Word 64)) (hsz : arr.size < 2 ^ 64) : - SpaceBound C (fun s => s.bufs 0 = arr) (Examples.SumBuf.code 0) + SpaceBound C RandomTape.zero (fun s => s.bufs 0 = arr) (Examples.SumBuf.code 0) (fun s => s.regs 0 = Examples.SumBuf.sumTo arr arr.size) 6 := (Examples.SumBuf.spec 0 arr hsz).space.spaceBound (by decide) @@ -545,7 +548,7 @@ theorem SumBuf.total_space {C : CostModel} (arr : Array (Word 64)) independent of the trip count: memory reuse in the buffer summand, static inference in the register summand. -/ theorem ScratchLoop.total_space {C : CostModel} (n : ℕ) (hn : n < 2 ^ 64) : - SpaceBound C (fun s => s.regs 2 = BitVec.ofNat 64 n) + SpaceBound C RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat 64 n) (Examples.ScratchLoop.code 0) (fun s => s.bufs 0 = #[] ∧ s.caps 0 = 0) 5 := (Examples.ScratchLoop.spec 0 n hn).space.spaceBound (by decide) @@ -553,7 +556,7 @@ theorem ScratchLoop.total_space {C : CostModel} (n : ℕ) (hn : n < 2 ^ 64) : /-- `Iota` (on buffer 0): buffer peak `n` + register peak 4 = total `n + 4`, the one genuinely linear-space example. -/ theorem Iota.total_space {C : CostModel} (n : ℕ) (hn : n < 2 ^ 64) : - SpaceBound C (fun s => s.regs 2 = BitVec.ofNat 64 n) + SpaceBound C RandomTape.zero (fun s => s.regs 2 = BitVec.ofNat 64 n) (Examples.Iota.code 0) (fun s => s.bufs 0 = Examples.Iota.iotaTo 64 n) ((n : ℤ) + 4) := (Examples.Iota.spec 0 n hn).space.spaceBound diff --git a/Caliper/Outcome.lean b/Caliper/Outcome.lean new file mode 100644 index 0000000..379f6b2 --- /dev/null +++ b/Caliper/Outcome.lean @@ -0,0 +1,150 @@ +import Caliper.TapeMeasure + +/-! +# Countable outcomes of a fixed program + +Although arbitrary machine states form an uncountable type, a fixed program and +initial state have only countably many terminating outcomes: each is witnessed by +a finite sequence of input words. This fact supports probabilistic composition. +-/ + +namespace Caliper + +open MeasureTheory + +variable {w : ℕ} + +abbrev Outcome (w : ℕ) := State w × ℕ × ℤ × ℤ + +def HasOutcome (C : CostModel) (tape : RandomTape w) (c : Stmt w) (s : State w) + (r : Outcome w) : Prop := Exec C tape c s r.1 r.2.1 r.2.2.1 r.2.2.2 + +noncomputable def outcome (C : CostModel) (c : Stmt w) (s : State w) + (tape : RandomTape w) : Option (Outcome w) := by + classical + exact if h : ∃ r, HasOutcome C tape c s r then some (Classical.choose h) else none + +theorem outcome_of_exec {C : CostModel} {tape : RandomTape w} {c : Stmt w} {s : State w} + {r : Outcome w} (he : HasOutcome C tape c s r) : outcome C c s tape = some r := by + have h : ∃ r, HasOutcome C tape c s r := ⟨r, he⟩ + have hx := Classical.choose_spec h + obtain ⟨hs, ht, hd, hp⟩ := hx.deterministic he + have hr : Classical.choose h = r := by + apply Prod.ext hs + exact Prod.ext ht (Prod.ext hd hp) + simp only [outcome, dif_pos h, hr] + +/-- Possible terminating outcomes over arbitrary tapes. -/ +def possibleOutcomes (C : CostModel) (c : Stmt w) (s : State w) : Set (Outcome w) := + {r | ∃ tape, HasOutcome C tape c s r} + +theorem possibleOutcomes_countable (C : CostModel) (c : Stmt w) (s : State w) : + (possibleOutcomes C c s).Countable := by + classical + let extend (tr : (n : ℕ) × (Fin n → Word w)) : RandomTape w := + fun i => if h : i < tr.1 then tr.2 ⟨i, h⟩ else 0 + let f (tr : (n : ℕ) × (Fin n → Word w)) := outcome C c s (extend tr) + have hsub : possibleOutcomes C c s ⊆ Option.some ⁻¹' Set.range f := by + rintro r ⟨tape, he⟩ + let tr : (n : ℕ) × (Fin n → Word w) := ⟨r.1.tapePos, fun i => tape i⟩ + refine ⟨tr, ?_⟩ + apply outcome_of_exec + apply he.withTape + intro i _ hi + simp only [extend, tr, dif_pos hi] + exact ((Set.countable_range f).preimage (by intro x y h; exact Option.some.inj h)).mono hsub + +/-- A particular outcome is a prefix event ending at its final cursor. -/ +theorem HasOutcome.measurableSet (C : CostModel) (c : Stmt w) (s : State w) + (r : Outcome w) : + MeasurableSet[RandomTape.prefixSigma r.1.tapePos] {tape | HasOutcome C tape c s r} := by + apply RandomTape.prefix_measurableSet + intro tape other ha + constructor + · intro he + exact he.withTape tape (fun i _ hi => (ha i hi).symm) + · intro he + exact he.withTape other (fun i _ hi => ha i hi) + +/-- Distinct outcomes belong to disjoint tape events. -/ +theorem HasOutcome.disjoint {C : CostModel} {c : Stmt w} {s : State w} + {r r' : Outcome w} (hne : r ≠ r') : + Disjoint {tape | HasOutcome C tape c s r} {tape | HasOutcome C tape c s r'} := by + apply Set.disjoint_left.mpr + intro tape h h' + obtain ⟨hs, ht, hd, hp⟩ := h.deterministic h' + exact hne (Prod.ext hs (Prod.ext ht (Prod.ext hd hp))) + +/-- After any safely terminating subroutine, the unread tape is uniform and +independent of every predicate on its outcome. The probability is unconditional: +if the subroutine terminates only with mass `p`, the joint event has mass `p * μ F`. +Neither elapsed time nor the consumed-word count must be fixed. -/ +theorem uniformTape_after_exec (C : CostModel) (c : Stmt w) (s : State w) + (Q : Outcome w → Prop) {F : Set (RandomTape w)} (hF : MeasurableSet F) : + uniformTape w {tape | ∃ r, HasOutcome C tape c s r ∧ Q r ∧ + RandomTape.drop r.1.tapePos tape ∈ F} = + uniformTape w {tape | ∃ r, HasOutcome C tape c s r ∧ Q r} * uniformTape w F := by + classical + let A : Set (Outcome w) := {r | r ∈ possibleOutcomes C c s ∧ Q r} + letI : Countable A := ((possibleOutcomes_countable C c s).mono (fun _ h => h.1)).to_subtype + let E (a : A) : Set (RandomTape w) := {tape | HasOutcome C tape c s a.val} + have he : {tape | ∃ r, HasOutcome C tape c s r ∧ Q r} = ⋃ a : A, E a := by + ext tape + simp only [Set.mem_setOf_eq, Set.mem_iUnion] + constructor + · rintro ⟨r, hr, hq⟩ + exact ⟨⟨r, ⟨⟨tape, hr⟩, hq⟩⟩, hr⟩ + · rintro ⟨a, ha⟩ + exact ⟨a.val, ha, a.property.2⟩ + have hef : {tape | ∃ r, HasOutcome C tape c s r ∧ Q r ∧ + RandomTape.drop r.1.tapePos tape ∈ F} = + ⋃ a : A, E a ∩ RandomTape.drop a.val.1.tapePos ⁻¹' F := by + ext tape + simp only [Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_preimage] + constructor + · rintro ⟨r, hr, hq, hf⟩ + exact ⟨⟨r, ⟨⟨tape, hr⟩, hq⟩⟩, hr, hf⟩ + · rintro ⟨a, ha, hf⟩ + exact ⟨a.val, ha, a.property.2, hf⟩ + rw [he, hef] + apply uniformTape_partition_drop (fun a : A => a.val.1.tapePos) E + (fun a => HasOutcome.measurableSet C c s a.val) _ hF + intro a b hab + exact HasOutcome.disjoint (fun h => hab (Subtype.ext h)) + +/-- Sampling after any subroutine gives a uniform word on each safely returning +run. Success mass is retained, rather than implicitly conditioned to one. -/ +theorem resultProb_seq_rand (C : CostModel) (c : Stmt w) (s : State w) (r : Reg) (v : Word w) : + resultProb C (c ;; .rand r) s (fun s' _ _ _ => s'.regs r = v) = + resultProb C c s (fun _ _ _ _ => True) * ((2 ^ w : ℕ) : ENNReal)⁻¹ := by + let F : Set (RandomTape w) := {tape | tape 0 = v} + have hF : MeasurableSet F := by + simpa only [F, Set.preimage, Set.mem_singleton_iff] using + ((measurable_pi_apply 0 : Measurable (fun tape : RandomTape w => tape 0)) (measurableSet_singleton v)) + have he : {tape | ∃ s' t d p, Exec C tape (c ;; .rand r) s s' t d p ∧ s'.regs r = v} = + {tape | ∃ out, HasOutcome C tape c s out ∧ True ∧ + RandomTape.drop out.1.tapePos tape ∈ F} := by + ext tape + constructor + · rintro ⟨s', t, d, p, hexec, hv⟩ + cases hexec with + | @seq _ _ _ s₁ _ t₁ d₁ p₁ _ _ _ h₁ h₂ => + cases h₂ + exact ⟨(s₁, t₁, d₁, p₁), h₁, trivial, + by simpa [F, RandomTape.drop, State.readRandom, State.setReg] using hv⟩ + · rintro ⟨out, h₁, _, hv⟩ + exact ⟨_, _, _, _, Exec.seq h₁ Exec.rand, + by simpa [F, RandomTape.drop, State.readRandom, State.setReg] using hv⟩ + unfold resultProb + rw [he, uniformTape_after_exec C c s (fun _ => True) hF] + rw [show uniformTape w F = ((2 ^ w : ℕ) : ENNReal)⁻¹ from uniformTape_eval 0 v] + congr 1 + congr 1 + ext tape + constructor + · rintro ⟨out, he, _⟩ + exact ⟨out.1, out.2.1, out.2.2.1, out.2.2.2, he, trivial⟩ + · rintro ⟨s', t, d, p, he, _⟩ + exact ⟨(s', t, d, p), he, trivial⟩ + +end Caliper diff --git a/Caliper/PMF.lean b/Caliper/PMF.lean new file mode 100644 index 0000000..da20fb3 --- /dev/null +++ b/Caliper/PMF.lean @@ -0,0 +1,57 @@ +import Mathlib.Probability.ProbabilityMassFunction.Constructions +import Mathlib.MeasureTheory.Integral.Lebesgue.Countable +import Mathlib.Data.Real.ENatENNReal + +/-! +# Expectations of discrete distributions + +This API is generic in the PMF and its observable. In particular, Caliper's +runtime distribution needs no separate program-specific expectation. +-/ + +open MeasureTheory +open scoped ENNReal + +namespace PMF + +variable {α β : Type*} + +/-- Extended nonnegative expectation; zero mass contributes zero even at `∞`. -/ +noncomputable def expect (p : PMF α) (f : α → ℝ≥0∞) : ℝ≥0∞ := + ∑' x, p x * f x + +@[simp] theorem expect_pure (x : α) (f : α → ℝ≥0∞) : + (PMF.pure x).expect f = f x := by + classical + simp [expect, PMF.pure_apply] + +theorem expect_mono (p : PMF α) {f g : α → ℝ≥0∞} (h : ∀ x, f x ≤ g x) : + p.expect f ≤ p.expect g := + ENNReal.tsum_le_tsum fun x => mul_le_mul_right (h x) (p x) + +@[simp] theorem expect_const (p : PMF α) (v : ℝ≥0∞) : + p.expect (fun _ => v) = v := by + simp only [expect, ENNReal.tsum_mul_right, p.tsum_coe, one_mul] + +theorem expect_add (p : PMF α) (f g : α → ℝ≥0∞) : + p.expect (fun x => f x + g x) = p.expect f + p.expect g := by + simp only [expect, mul_add, ENNReal.tsum_add] + +theorem expect_bind (p : PMF α) (q : α → PMF β) (f : β → ℝ≥0∞) : + (p.bind q).expect f = p.expect (fun x => (q x).expect f) := by + simp only [expect, PMF.bind_apply, ← ENNReal.tsum_mul_right] + rw [ENNReal.tsum_comm] + simp only [← ENNReal.tsum_mul_left, mul_assoc] + +theorem expect_map (p : PMF α) (g : α → β) (f : β → ℝ≥0∞) : + (p.map g).expect f = p.expect (fun x => f (g x)) := by + change (p.bind (fun x => PMF.pure (g x))).expect f = _ + simp only [expect_bind, expect_pure] + +/-- The discrete sum agrees with the measure-theoretic expectation. -/ +theorem expect_eq_lintegral [Countable α] [MeasurableSpace α] + [MeasurableSingletonClass α] (p : PMF α) (f : α → ℝ≥0∞) : + p.expect f = ∫⁻ x, f x ∂p.toMeasure := by + simp only [expect, lintegral_countable', PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), mul_comm] + +end PMF diff --git a/Caliper/ProbTriple.lean b/Caliper/ProbTriple.lean new file mode 100644 index 0000000..14ac1ee --- /dev/null +++ b/Caliper/ProbTriple.lean @@ -0,0 +1,250 @@ +import Caliper.Outcome +import Caliper.Triple + +/-! +# Probabilistic resource triples + +The postcondition and buffer bounds hold on almost every uniform tape. Time is +bounded in expectation using the runtime PMF. Fixed-tape triples remain +available for proofs that cover every supplied tape. +-/ + +open MeasureTheory +open scoped ENNReal + +namespace Caliper + +variable {w : ℕ} {C : CostModel} + +/-- Almost-sure safe correctness and memory bounds, with an expected-time bound. -/ +def ProbTriple (C : CostModel) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) + (T : ℝ≥0∞) (D M : ℤ) : Prop := + ∀ s, P s → + (∀ᵐ tape ∂uniformTape w, ∃ s' t d p, + Exec C tape c s s' t d p ∧ Q s' ∧ d ≤ D ∧ p ≤ M) ∧ + (runTimePMF C c s).expect ENat.toENNReal ≤ T + +/-- Bound a PMF expectation by an almost-everywhere bound on witnessed executions. -/ +theorem runTimePMF_expect_le {c : Stmt w} {s : State w} + (f : RandomTape w → ℝ≥0∞) + (h : ∀ᵐ tape ∂uniformTape w, ∃ s' t d p, + Exec C tape c s s' t d p ∧ (t : ℝ≥0∞) ≤ f tape) : + (runTimePMF C c s).expect ENat.toENNReal ≤ ∫⁻ tape, f tape ∂uniformTape w := by + rw [runTimePMF_expect_eq] + apply lintegral_mono_ae + filter_upwards [h] with tape ht + obtain ⟨s', t, d, p, he, ht⟩ := ht + simpa only [runTime_of_exec he, ENat.toENNReal_coe] using ht + +namespace ProbTriple + +theorem conseq {P P' Q Q' : State w → Prop} {c : Stmt w} {T T' : ℝ≥0∞} + {D D' M M' : ℤ} (h : ProbTriple C P c Q T D M) + (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) + (hT : T ≤ T') (hD : D ≤ D') (hM : M ≤ M') : + ProbTriple C P' c Q' T' D' M' := by + intro s hs + obtain ⟨ha, ht⟩ := h s (hP s hs) + refine ⟨?_, ht.trans hT⟩ + filter_upwards [ha] with tape ha + obtain ⟨s', t, d, p, he, hq, hd, hp⟩ := ha + exact ⟨s', t, d, p, he, hQ s' hq, hd.trans hD, hp.trans hM⟩ + +/-- Every all-tape worst-case proof also gives a probabilistic specification. -/ +theorem of_forall_triple {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} + (h : ∀ tape, Triple C tape P c Q T D M) : ProbTriple C P c Q T D M := by + intro s hs + constructor + · apply Filter.Eventually.of_forall + intro tape + obtain ⟨s', t, d, p, he, hq, _, hd, hp⟩ := h tape s hs + exact ⟨s', t, d, p, he, hq, hd, hp⟩ + · calc + _ ≤ ∫⁻ _ : RandomTape w, (T : ℝ≥0∞) ∂uniformTape w := + runTimePMF_expect_le _ (Filter.Eventually.of_forall fun tape => by + obtain ⟨s', t, d, p, he, _, ht, _, _⟩ := h tape s hs + exact ⟨s', t, d, p, he, by exact_mod_cast ht⟩) + _ = T := by simp + +/-- Deterministic library routines can be called from randomized programs using +an existing fixed-tape specification and a syntactic no-randomness certificate. -/ +theorem of_randomFree {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} + {tape : RandomTape w} (h : Triple C tape P c Q T D M) (hc : c.RandomFree) : + ProbTriple C P c Q T D M := + of_forall_triple fun other => h.withTape_of_randomFree hc other + +protected theorem skip {P Q : State w → Prop} (h : ∀ s, P s → Q s) : + ProbTriple C P (.skip (w := w)) Q 0 0 0 := by + exact_mod_cast of_forall_triple (fun _ => Triple.skip h) + +/-- Every possible word must establish the postcondition. -/ +protected theorem rand {P Q : State w → Prop} {r : Reg} + (h : ∀ s, P s → ∀ v : Word w, Q { s.setReg r v with tapePos := s.tapePos + 1 }) : + ProbTriple C P (.rand r) Q C.rand 0 0 := + of_forall_triple fun tape => Triple.rand (fun s hs => h s hs (tape s.tapePos)) + +/-- Sequential composition uses the unread uniform tail, including when the first +subroutine consumes a variable number of words. Costs add; buffer peaks compose +with the net allocation of the first subroutine. -/ +protected theorem seq {P R Q : State w → Prop} {c₁ c₂ : Stmt w} {T₁ T₂ : ℝ≥0∞} + {D₁ M₁ D₂ M₂ : ℤ} + (h₁ : ProbTriple C P c₁ R T₁ D₁ M₁) (h₂ : ProbTriple C R c₂ Q T₂ D₂ M₂) : + ProbTriple C P (c₁ ;; c₂) Q (T₁ + T₂) (D₁ + D₂) (max M₁ (D₁ + M₂)) := by + classical + intro s hs + let good : Set (Outcome w) := {r | r ∈ possibleOutcomes C c₁ s ∧ + R r.1 ∧ r.2.2.1 ≤ D₁ ∧ r.2.2.2 ≤ M₁} + have hc : good.Countable := (possibleOutcomes_countable C c₁ s).mono (fun _ h => h.1) + letI : Countable good := hc.to_subtype + let E (a : good) : Set (RandomTape w) := {tape | HasOutcome C tape c₁ s a.val} + let f (a : good) (tape : RandomTape w) := + ENat.toENNReal (runTime C c₂ a.val.1 tape) + have hE a : MeasurableSet[RandomTape.prefixSigma a.val.1.tapePos] (E a) := + HasOutcome.measurableSet C c₁ s a.val + have hm a : MeasurableSet (E a) := RandomTape.prefixSigma_le _ _ (hE a) + have hf a : Measurable[RandomTape.tailSigma a.val.1.tapePos] (f a) := + (measurable_of_countable ENat.toENNReal).comp (runTime_tail_measurable C c₂ a.val.1) + have hfm a : Measurable (f a) := (hf a).mono (RandomTape.tailSigma_le _) le_rfl + have hd : Pairwise (fun a b => Disjoint (E a) (E b)) := by + intro a b hab + exact HasOutcome.disjoint (fun h => hab (Subtype.ext h)) + have hmass : (∑' a, uniformTape w (E a)) ≤ 1 := by + rw [← measure_iUnion hd hm] + simpa using (measure_mono (Set.subset_univ (⋃ a, E a)) : uniformTape w (⋃ a, E a) ≤ uniformTape w Set.univ) + obtain ⟨ha₁, ht₁⟩ := h₁ s hs + have ha₂ : ∀ᵐ tape ∂uniformTape w, ∀ a : good, ∃ s' t d p, + Exec C tape c₂ a.val.1 s' t d p ∧ Q s' ∧ d ≤ D₂ ∧ p ≤ M₂ := + ae_all_iff.mpr (fun a => (h₂ a.val.1 a.property.2.1).1) + have ha : ∀ᵐ tape ∂uniformTape w, ∃ a : good, ∃ s' t d p, + HasOutcome C tape c₁ s a.val ∧ Exec C tape c₂ a.val.1 s' t d p ∧ + Q s' ∧ d ≤ D₂ ∧ p ≤ M₂ := by + filter_upwards [ha₁, ha₂] with tape h₁t h₂t + obtain ⟨s₁, t₁, d₁, p₁, he₁, hr, hd₁, hp₁⟩ := h₁t + let a : good := ⟨(s₁, t₁, d₁, p₁), ⟨⟨tape, he₁⟩, hr, hd₁, hp₁⟩⟩ + obtain ⟨s', t, d, p, he₂, hq, hd₂, hp₂⟩ := h₂t a + exact ⟨a, s', t, d, p, he₁, he₂, hq, hd₂, hp₂⟩ + constructor + · filter_upwards [ha] with tape ht + obtain ⟨a, s', t, d, p, he₁, he₂, hq, hd₂, hp₂⟩ := ht + have hd₁ := a.property.2.2.1 + have hp₁ := a.property.2.2.2 + exact ⟨s', a.val.2.1 + t, a.val.2.2.1 + d, max a.val.2.2.2 (a.val.2.2.1 + p), + .seq he₁ he₂, hq, by omega, by omega⟩ + · let future (tape : RandomTape w) := ∑' a : good, (E a).indicator (f a) tape + have hfuture : (∫⁻ tape, future tape ∂uniformTape w) ≤ T₂ := by + rw [show (∫⁻ tape, future tape ∂uniformTape w) = + ∑' a : good, ∫⁻ tape, (E a).indicator (f a) tape ∂uniformTape w from + lintegral_tsum (fun a => ((hfm a).indicator (hm a)).aemeasurable)] + simp_rw [lintegral_prefix_indicator_future _ (hE _) _ (hf _)] + calc + _ ≤ ∑' a : good, uniformTape w (E a) * T₂ := ENNReal.tsum_le_tsum fun a => by + apply mul_le_mul_right + rw [← runTimePMF_expect_eq] + exact (h₂ a.val.1 a.property.2.1).2 + _ = (∑' a : good, uniformTape w (E a)) * T₂ := ENNReal.tsum_mul_right + _ ≤ 1 * T₂ := mul_le_mul_left hmass T₂ + _ = T₂ := one_mul _ + calc + _ ≤ ∫⁻ tape, ENat.toENNReal (runTime C c₁ s tape) + future tape + ∂uniformTape w := runTimePMF_expect_le _ (by + filter_upwards [ha] with tape ht + obtain ⟨a, s', t, d, p, he₁, he₂, _, _, _⟩ := ht + refine ⟨s', a.val.2.1 + t, _, _, .seq he₁ he₂, ?_⟩ + rw [runTime_of_exec he₁, ENat.toENNReal_coe, Nat.cast_add] + apply add_le_add_right + have hterm := ENNReal.le_tsum (f := fun a : good => (E a).indicator (f a) tape) a + simpa only [Set.indicator_of_mem (show tape ∈ E a from he₁), f, + runTime_of_exec he₂, ENat.toENNReal_coe] using hterm) + _ = (runTimePMF C c₁ s).expect ENat.toENNReal + + ∫⁻ tape, future tape ∂uniformTape w := by + have hm₁ : Measurable (fun tape => ENat.toENNReal (runTime C c₁ s tape)) := + (measurable_of_countable ENat.toENNReal).comp (measurable_runTime C c₁ s) + rw [lintegral_add_left hm₁, runTimePMF_expect_eq] + _ ≤ T₁ + T₂ := add_le_add ht₁ hfuture + +/-- Branch on a register value; branch selection cannot inspect semantic costs. -/ +protected theorem ifNZ {P Q : State w → Prop} {r : Reg} {a b : Stmt w} + {T : ℝ≥0∞} {D M : ℤ} + (ha : ProbTriple C (fun s => P s ∧ s.regs r ≠ 0) a Q T D M) + (hb : ProbTriple C (fun s => P s ∧ s.regs r = 0) b Q T D M) : + ProbTriple C P (.ifNZ r a b) Q (C.branch + T) D M := by + intro s hs + by_cases hz : s.regs r = 0 + · obtain ⟨hc, ht⟩ := hb s ⟨hs, hz⟩ + constructor + · filter_upwards [hc] with tape he + obtain ⟨s', t, d, p, he, hq, hd, hp⟩ := he + exact ⟨s', C.branch + t, d, p, .ifNZ_false hz he, hq, hd, hp⟩ + · calc + _ ≤ ∫⁻ tape, (C.branch : ℝ≥0∞) + ENat.toENNReal (runTime C b s tape) + ∂uniformTape w := runTimePMF_expect_le _ (by + filter_upwards [hc] with tape he + obtain ⟨s', t, d, p, he, _, _, _⟩ := he + refine ⟨s', C.branch + t, d, p, .ifNZ_false hz he, ?_⟩ + simp only [runTime_of_exec he, ENat.toENNReal_coe, Nat.cast_add, le_refl]) + _ = C.branch + (runTimePMF C b s).expect ENat.toENNReal := by + rw [lintegral_add_left measurable_const, runTimePMF_expect_eq] + simp + _ ≤ C.branch + T := add_le_add_right ht _ + · obtain ⟨hc, ht⟩ := ha s ⟨hs, hz⟩ + constructor + · filter_upwards [hc] with tape he + obtain ⟨s', t, d, p, he, hq, hd, hp⟩ := he + exact ⟨s', C.branch + t, d, p, .ifNZ_true hz he, hq, hd, hp⟩ + · calc + _ ≤ ∫⁻ tape, (C.branch : ℝ≥0∞) + ENat.toENNReal (runTime C a s tape) + ∂uniformTape w := runTimePMF_expect_le _ (by + filter_upwards [hc] with tape he + obtain ⟨s', t, d, p, he, _, _, _⟩ := he + refine ⟨s', C.branch + t, d, p, .ifNZ_true hz he, ?_⟩ + simp only [runTime_of_exec he, ENat.toENNReal_coe, Nat.cast_add, le_refl]) + _ = C.branch + (runTimePMF C a s).expect ENat.toENNReal := by + rw [lintegral_add_left measurable_const, runTimePMF_expect_eq] + simp + _ ≤ C.branch + T := add_le_add_right ht _ + +/-- A countable collection of terminating cases suffices for unbounded randomized +computations. The masses must sum to one; failed runs are never conditioned away. +The cases can, for example, enumerate the number of iterations of a retry loop. -/ +theorem of_countable_cases {α : Type*} [Countable α] {P Q : State w → Prop} + {c : Stmt w} {T : ℝ≥0∞} {D M : ℤ} + (E : State w → α → Set (RandomTape w)) (cost : α → ℕ) + (hm : ∀ s a, MeasurableSet (E s a)) + (hd : ∀ s, Pairwise (fun a b => Disjoint (E s a) (E s b))) + (hmass : ∀ s, P s → (∑' a, uniformTape w (E s a)) = 1) + (hexec : ∀ s, P s → ∀ a tape, tape ∈ E s a → ∃ s' t d p, + Exec C tape c s s' t d p ∧ Q s' ∧ t ≤ cost a ∧ d ≤ D ∧ p ≤ M) + (htime : ∀ s, P s → (∑' a, uniformTape w (E s a) * (cost a : ℝ≥0∞)) ≤ T) : + ProbTriple C P c Q T D M := by + classical + intro s hs + have hcover : ∀ᵐ tape ∂uniformTape w, tape ∈ ⋃ a, E s a := by + apply (mem_ae_iff_prob_eq_one (MeasurableSet.iUnion (hm s))).mpr + rw [measure_iUnion (hd s) (hm s), hmass s hs] + constructor + · filter_upwards [hcover] with tape ht + obtain ⟨a, ha⟩ := Set.mem_iUnion.mp ht + obtain ⟨s', t, d, p, he, hq, _, hD, hM⟩ := hexec s hs a tape ha + exact ⟨s', t, d, p, he, hq, hD, hM⟩ + · calc + _ ≤ ∫⁻ tape, ∑' a, (E s a).indicator (fun _ => (cost a : ℝ≥0∞)) tape + ∂uniformTape w := runTimePMF_expect_le _ (by + filter_upwards [hcover] with tape ht + obtain ⟨a, ha⟩ := Set.mem_iUnion.mp ht + obtain ⟨s', t, d, p, he, _, hc, _, _⟩ := hexec s hs a tape ha + refine ⟨s', t, d, p, he, ?_⟩ + calc + (t : ℝ≥0∞) ≤ cost a := by exact_mod_cast hc + _ = (E s a).indicator (fun _ => (cost a : ℝ≥0∞)) tape := + (Set.indicator_of_mem ha (fun _ => (cost a : ℝ≥0∞))).symm + _ ≤ _ := ENNReal.le_tsum a) + _ = ∑' a, uniformTape w (E s a) * (cost a : ℝ≥0∞) := by + rw [lintegral_tsum (fun a => (measurable_const.indicator (hm s a)).aemeasurable)] + congr 1 + funext a + rw [lintegral_indicator (hm s a)] + simp [mul_comm] + _ ≤ T := htime s hs + +end ProbTriple +end Caliper diff --git a/Caliper/Probability.lean b/Caliper/Probability.lean new file mode 100644 index 0000000..8a567d2 --- /dev/null +++ b/Caliper/Probability.lean @@ -0,0 +1,256 @@ +import Caliper.Tape +import Caliper.PMF +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Probability.Independence.InfinitePi +import Mathlib.MeasureTheory.MeasurableSpace.Instances +import Mathlib.Data.ENat.Lattice + +/-! +# Uniform tapes and runtime distributions + +Execution remains deterministic. Probability is the product measure on input words. +The induced runtime PMF retains unsuccessful executions as mass at `∞`. +-/ + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace Caliper + +variable {w : ℕ} + +/-- Words have exactly `2^w` possible values. -/ +def Word.equivFin : Word w ≃ Fin (2 ^ w) where + toFun := BitVec.toFin + invFun := BitVec.ofFin + left_inv x := by cases x; rfl + right_inv _ := rfl + +instance : Fintype (Word w) := Fintype.ofEquiv (Fin (2 ^ w)) Word.equivFin.symm + +@[simp] theorem Word.card : Fintype.card (Word w) = 2 ^ w := + (Fintype.card_congr Word.equivFin).trans (Fintype.card_fin _) + +instance : MeasurableSpace (Word w) := ⊤ +instance : DiscreteMeasurableSpace (Word w) := ⟨fun _ => trivial⟩ + +/-- Independent uniform words at every tape position. -/ +noncomputable def uniformTape (w : ℕ) : Measure (RandomTape w) := + Measure.infinitePi fun _ : ℕ => (PMF.uniformOfFintype (Word w)).toMeasure + +instance : IsProbabilityMeasure (uniformTape w) := by + unfold uniformTape + infer_instance + +/-- Tapes with a prescribed finite prefix. -/ +def RandomTape.cylinder {n : ℕ} (xs : Fin n → Word w) : Set (RandomTape w) := + {tape | ∀ i : Fin n, tape (i : ℕ) = xs i} + +theorem RandomTape.measurableSet_cylinder {n : ℕ} (xs : Fin n → Word w) : + MeasurableSet (RandomTape.cylinder xs) := by + unfold cylinder + simp only [Set.setOf_forall] + exact MeasurableSet.iInter fun i => (measurable_pi_apply (i : ℕ)) (measurableSet_singleton _) + +/-- Any event witnessed by a finite prefix is measurable. -/ +theorem RandomTape.measurableSet_of_prefix (E : Set (RandomTape w)) + (hE : ∀ tape ∈ E, ∃ n, ∀ other, (∀ i < n, other i = tape i) → other ∈ E) : + MeasurableSet E := by + classical + have hEq : E = ⋃ n : ℕ, ⋃ xs : Fin n → Word w, + if RandomTape.cylinder xs ⊆ E then RandomTape.cylinder xs else ∅ := by + ext tape + simp only [Set.mem_iUnion] + constructor + · intro ht + obtain ⟨n, hn⟩ := hE tape ht + refine ⟨n, fun i => tape i, ?_⟩ + have hc : RandomTape.cylinder (fun i : Fin n => tape i) ⊆ E := by + intro other ho + apply hn other + intro i hi + exact ho ⟨i, hi⟩ + simp only [if_pos hc] + exact fun _ => rfl + · rintro ⟨n, xs, hx⟩ + split at hx + · exact ‹RandomTape.cylinder xs ⊆ E› hx + · exact hx.elim + rw [hEq] + apply MeasurableSet.iUnion + intro n + apply MeasurableSet.iUnion + intro xs + split + · exact RandomTape.measurableSet_cylinder xs + · exact MeasurableSet.empty + +/-- A tape coordinate has exactly the uniform word law. -/ +theorem uniformTape_eval (i : ℕ) (v : Word w) : + uniformTape w {tape | tape i = v} = ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹ := by + have h := congrArg (fun μ : Measure (Word w) => μ {v}) + (Measure.infinitePi_map_eval (fun _ : ℕ => (PMF.uniformOfFintype (Word w)).toMeasure) i) + rw [Measure.map_apply (measurable_pi_apply i) (measurableSet_singleton v)] at h + simpa only [uniformTape, PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), PMF.uniformOfFintype_apply, + Word.card, Set.preimage, Set.mem_singleton_iff] using h + +/-- Distinct tape positions are independent, including after any fixed offset. -/ +theorem uniformTape_independent : + iIndepFun (fun i : ℕ => fun tape : RandomTape w => tape i) (uniformTape w) := + iIndepFun_infinitePi (X := fun _ x => x) (fun _ => measurable_id) + +/-- A specified prefix of `n` words has mass `(2^w)^(-n)`. -/ +theorem uniformTape_cylinder {n : ℕ} (xs : Fin n → Word w) : + uniformTape w (RandomTape.cylinder xs) = (((2 ^ w : ℕ) : ℝ≥0∞)⁻¹) ^ n := by + classical + let ext : RandomTape w := fun i => if h : i < n then xs ⟨i, h⟩ else 0 + have hset : RandomTape.cylinder xs = + (↑(Finset.range n) : Set ℕ).pi (fun i => {ext i}) := by + ext tape + simp only [RandomTape.cylinder, Set.mem_setOf_eq, Set.mem_pi, Finset.mem_coe, + Finset.mem_range, Set.mem_singleton_iff] + constructor + · intro h i hi + simpa only [ext, dif_pos hi] using h ⟨i, hi⟩ + · intro h i + simpa only [ext, dif_pos i.isLt] using h i i.isLt + rw [hset] + unfold uniformTape + rw [Measure.infinitePi_pi _ (fun _ _ => measurableSet_singleton _)] + simp only [PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), PMF.uniformOfFintype_apply, Word.card, + Finset.prod_const, Finset.card_range] + +variable (C : CostModel) (c : Stmt w) (s : State w) + +/-- An arbitrary predicate on terminating results defines a measurable tape event. -/ +theorem measurableSet_exec (Q : State w → ℕ → ℤ → ℤ → Prop) : + MeasurableSet {tape | ∃ s' t d p, Exec C tape c s s' t d p ∧ Q s' t d p} := by + apply RandomTape.measurableSet_of_prefix + rintro tape ⟨s', t, d, p, he, hq⟩ + refine ⟨s'.tapePos, ?_⟩ + intro other ha + exact ⟨s', t, d, p, he.withTape other (fun i _ hi => ha i hi), hq⟩ + +/-- Cost of safe termination; unsuccessful execution has value `∞`. -/ +noncomputable def runTime (tape : RandomTape w) : ℕ∞ := + by + classical + exact if h : ∃ t, ∃ s' d p, Exec C tape c s s' t d p then + ((Classical.choose h : ℕ) : ℕ∞) else ⊤ + +variable {C c s} + +theorem runTime_of_exec {tape : RandomTape w} {s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) : runTime C c s tape = (t : ℕ∞) := by + have ht : ∃ t, ∃ s' d p, Exec C tape c s s' t d p := ⟨t, s', d, p, h⟩ + obtain ⟨s₀, d₀, p₀, h₀⟩ := Classical.choose_spec ht + have heq := (h₀.deterministic h).2.1 + simp only [runTime, dif_pos ht, heq] + +theorem runTime_eq_coe_iff (tape : RandomTape w) (t : ℕ) : + runTime C c s tape = (t : ℕ∞) ↔ ∃ s' d p, Exec C tape c s s' t d p := by + constructor + · intro heq + unfold runTime at heq + split at heq + · have ht := Classical.choose_spec ‹∃ t, ∃ s' d p, Exec C tape c s s' t d p› + have heq' : Classical.choose ‹∃ t, ∃ s' d p, Exec C tape c s s' t d p› = t := by + exact_mod_cast heq + simpa only [heq'] using ht + · simp at heq + · rintro ⟨s', d, p, he⟩ + exact runTime_of_exec he + +theorem runTime_eq_top_iff (tape : RandomTape w) : + runTime C c s tape = ⊤ ↔ ¬ ∃ s' t d p, Exec C tape c s s' t d p := by + constructor + · intro ht ⟨s', t, d, p, he⟩ + rw [runTime_of_exec he] at ht + exact ENat.coe_ne_top _ ht + · intro hn + apply dif_neg + rintro ⟨t, s', d, p, he⟩ + exact hn ⟨s', t, d, p, he⟩ + +variable (C c s) + +theorem measurable_runTime : Measurable (runTime C c s) := by + apply ENat.measurable_iff.mpr + intro t + have hm := measurableSet_exec C c s (fun _ t' _ _ => t' = t) + simpa only [Set.preimage, Set.mem_singleton_iff, runTime_eq_coe_iff, + exists_and_right, exists_eq_right] using hm + +/-- The unconditional PMF of safe termination costs, including an atom at `∞`. -/ +noncomputable def runTimePMF : PMF ℕ∞ := + letI : IsProbabilityMeasure ((uniformTape w).map (runTime C c s)) := + Measure.isProbabilityMeasure_map (measurable_runTime C c s).aemeasurable + ((uniformTape w).map (runTime C c s)).toPMF + +/-- PMF atoms are exactly the corresponding tape-event probabilities. -/ +theorem runTimePMF_apply (t : ℕ∞) : + runTimePMF C c s t = uniformTape w {tape | runTime C c s tape = t} := by + unfold runTimePMF + rw [Measure.toPMF_apply, Measure.map_apply (measurable_runTime C c s) + (measurableSet_singleton t)] + rfl + +/-- Expectations of the PMF agree with integration over tapes for every observable. -/ +theorem runTimePMF_expect_eq (f : ℕ∞ → ℝ≥0∞) : + (runTimePMF C c s).expect f = + ∫⁻ tape, f (runTime C c s tape) ∂uniformTape w := by + rw [PMF.expect_eq_lintegral] + unfold runTimePMF + rw [Measure.toPMF_toMeasure, lintegral_map (measurable_of_countable f) + (measurable_runTime C c s)] + +/-- Zero mass at infinity is exactly almost-sure safe termination. -/ +theorem runTimePMF_top_eq_zero_iff : + runTimePMF C c s ⊤ = 0 ↔ + ∀ᵐ tape ∂uniformTape w, ∃ s' t d p, Exec C tape c s s' t d p := by + rw [runTimePMF_apply, ae_iff] + simp only [runTime_eq_top_iff] + +/-- A constant runtime gives a point-mass distribution. -/ +theorem runTimePMF_eq_pure (t : ℕ∞) + (h : ∀ tape, runTime C c s tape = t) : + runTimePMF C c s = PMF.pure t := by + classical + apply PMF.ext + intro t' + rw [runTimePMF_apply, PMF.pure_apply] + simp only [h] + by_cases ht : t' = t + · subst t'; simp + · have ht' : t ≠ t' := Ne.symm ht + simp [ht, ht'] + +/-- A random-free terminating computation has the same cost on every tape. -/ +theorem runTimePMF_of_randomFree {tape : RandomTape w} {s' : State w} + {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) (hc : c.RandomFree) : + runTimePMF C c s = PMF.pure (t : ℕ∞) := + runTimePMF_eq_pure C c s t fun other => + runTime_of_exec (h.withTape_of_randomFree hc other) + +/-- Probability of a property of a safely terminating outcome. -/ +noncomputable def resultProb (Q : State w → ℕ → ℤ → ℤ → Prop) : ℝ≥0∞ := + uniformTape w {tape | ∃ s' t d p, Exec C tape c s s' t d p ∧ Q s' t d p} + +/-- For an explicitly known total execution, outcome probabilities simplify directly. -/ +theorem resultProb_of_exec (Q : State w → ℕ → ℤ → ℤ → Prop) + (out : RandomTape w → State w) (time : RandomTape w → ℕ) + (net peak : RandomTape w → ℤ) + (h : ∀ tape, Exec C tape c s (out tape) (time tape) (net tape) (peak tape)) : + resultProb C c s Q = + uniformTape w {tape | Q (out tape) (time tape) (net tape) (peak tape)} := by + unfold resultProb + congr 1 + ext tape + constructor + · rintro ⟨s', t, d, p, he, hq⟩ + obtain ⟨rfl, rfl, rfl, rfl⟩ := he.deterministic (h tape) + exact hq + · intro hq + exact ⟨_, _, _, _, h tape, hq⟩ + +end Caliper diff --git a/Caliper/Render.lean b/Caliper/Render.lean index e7e2889..33841c9 100644 --- a/Caliper/Render.lean +++ b/Caliper/Render.lean @@ -44,6 +44,7 @@ for the dialect). Blocks indent their bodies by two spaces per nesting level. -/ def Stmt.render : Stmt w → List String | .skip => ["skip"] | .seq c₁ c₂ => c₁.render ++ c₂.render + | .rand d => [s!"{pad "rand" 6}r{d}"] | .imm d v => [s!"{pad "imm" 6}r{d}, {v.toNat}"] | .mov d a => [s!"{pad "mov" 6}r{d}, r{a}"] | .un op d a => [s!"{pad op.mnemonic 5}r{d}, r{a}"] diff --git a/Caliper/Retry.lean b/Caliper/Retry.lean new file mode 100644 index 0000000..cdacc15 --- /dev/null +++ b/Caliper/Retry.lean @@ -0,0 +1,241 @@ +import Caliper.ProbTriple +import Caliper.Geometric + +/-! +# Unbounded retry on a uniform word tape + +`retryZero` samples until it sees zero. It can diverge on a fixed tape, but has +almost-sure safe termination under `uniformTape`. Its specification composes with +other randomized subroutines using `ProbTriple.seq`. +-/ + +open MeasureTheory +open scoped ENNReal + +namespace Caliper + +variable {w : ℕ} + +/-- Exactly `n` failures followed by the first zero word. -/ +def RandomTape.firstZero (n : ℕ) : Set (RandomTape w) := + {tape | (∀ i < n, tape i ≠ 0) ∧ tape n = 0} + +theorem RandomTape.measurableSet_firstZero (n : ℕ) : + MeasurableSet (RandomTape.firstZero (w := w) n) := by + apply RandomTape.measurableSet_of_prefix + intro tape ht + refine ⟨n + 1, ?_⟩ + intro other ha + exact ⟨fun i hi => by rw [ha i (by omega)]; exact ht.1 i hi, + by rw [ha n (by omega)]; exact ht.2⟩ + +theorem RandomTape.firstZero_disjoint : + Pairwise (fun n m => Disjoint (RandomTape.firstZero (w := w) n) (RandomTape.firstZero m)) := by + intro n m hnm + apply Set.disjoint_left.mpr + intro tape hn hm + rcases lt_or_gt_of_ne hnm with h | h + · exact hm.1 n h hn.2 + · exact hn.1 m h hm.2 + +/-- First-hit probabilities are geometric, with success probability `1 / 2^w`. -/ +theorem uniformTape_firstZero (n : ℕ) : + uniformTape w (RandomTape.firstZero n) = + (1 - ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹) ^ n * ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹ := by + classical + let S (i : ℕ) : Set (Word w) := if i < n then {0}ᶜ else {0} + have hS i : MeasurableSet (S i) := by + dsimp [S] + split + · exact (measurableSet_singleton _).compl + · exact measurableSet_singleton _ + have he : RandomTape.firstZero n = (↑(Finset.range (n + 1)) : Set ℕ).pi S := by + ext tape + simp only [RandomTape.firstZero, Set.mem_setOf_eq, Set.mem_pi, Finset.mem_coe, + Finset.mem_range] + constructor + · rintro ⟨hn, hz⟩ i hi + by_cases h : i < n + · simpa [S, h] using hn i h + · have : i = n := by omega + subst i + simpa [S] using hz + · intro h + constructor + · intro i hi + simpa [S, hi] using h i (by omega) + · simpa [S] using h n (by omega) + rw [he] + unfold uniformTape + rw [Measure.infinitePi_pi _ (fun i _ => hS i), Finset.prod_range_succ] + have hp : ∀ i ∈ Finset.range n, + (PMF.uniformOfFintype (Word w)).toMeasure (S i) = + 1 - ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹ := by + intro i hi + simp only [Finset.mem_range] at hi + rw [show S i = {0}ᶜ from if_pos hi, measure_compl (measurableSet_singleton _) (measure_ne_top _ _)] + simp only [measure_univ, PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), + PMF.uniformOfFintype_apply, Word.card] + rw [Finset.prod_congr rfl hp] + simp [S, PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), + PMF.uniformOfFintype_apply, Word.card] + +/-- Retry until a sampled word equals zero. No instruction reads the attempt count. -/ +def retryZero (r : Reg) : Stmt w := .whileNZ (.rand r) r .skip + +theorem retryZero_exec (C : CostModel) (r : Reg) (s : State w) (tape : RandomTape w) + (n : ℕ) (hn : RandomTape.drop s.tapePos tape ∈ RandomTape.firstZero n) : + Exec C tape (retryZero r) s + { s.setReg r 0 with tapePos := s.tapePos + n + 1 } + ((n + 1) * (C.rand + C.branch)) 0 0 := by + induction n generalizing s with + | zero => + have hz : (s.readRandom tape r).regs r = 0 := by + simpa [RandomTape.firstZero, RandomTape.drop] using hn.2 + have he := Exec.while_done (C := C) (tape := tape) (b := Stmt.skip) Exec.rand hz + convert he using 1 <;> simp_all [retryZero, State.readRandom, State.setReg] + | succ n ih => + have hne : (s.readRandom tape r).regs r ≠ 0 := by + simpa [RandomTape.drop] using hn.1 0 (by omega) + have hnext : RandomTape.drop (s.readRandom tape r).tapePos tape ∈ + RandomTape.firstZero n := by + constructor + · intro i hi + simpa [RandomTape.drop, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using + hn.1 (i + 1) (by omega) + · simpa [RandomTape.drop, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hn.2 + have he := Exec.while_step (C := C) (tape := tape) Exec.rand hne Exec.skip + (ih (s.readRandom tape r) hnext) + convert he using 1 <;> + simp [retryZero, State.readRandom, State.setReg, + Nat.add_assoc, Nat.add_mul, Nat.mul_add] + · constructor + · omega + · funext r' + by_cases hr : r' = r <;> simp [hr] + · omega + +/-- Every safe execution of retry is witnessed by a finite first-zero event. -/ +theorem retryZero_exec_firstZero {C : CostModel} {r : Reg} {s s' : State w} + {tape : RandomTape w} {t : ℕ} {d p : ℤ} + (he : Exec C tape (retryZero r) s s' t d p) : + ∃ n, RandomTape.drop s.tapePos tape ∈ RandomTape.firstZero n ∧ + t = (n + 1) * (C.rand + C.branch) := by + have aux {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (he : Exec C tape c s s' t d p) : c = retryZero r → + ∃ n, RandomTape.drop s.tapePos tape ∈ RandomTape.firstZero n ∧ + t = (n + 1) * (C.rand + C.branch) := by + induction he with + | while_done hg hz _ => + intro hc + cases hc + cases hg + refine ⟨0, ⟨?_, ?_⟩, by omega⟩ + · intro i hi; omega + · simpa [RandomTape.drop, State.readRandom, State.setReg] using hz + | @while_step g c b s s₁ s₂ s₃ tg dg pg tb db pb tl dl pl hg hn hb hl _ _ ihl => + intro hc + cases hc + cases hg + cases hb + obtain ⟨n, hn', ht⟩ := ihl rfl + refine ⟨n + 1, ⟨?_, ?_⟩, ?_⟩ + · intro i hi + cases i with + | zero => simpa [RandomTape.drop, State.readRandom, State.setReg] using hn + | succ i => + simpa [RandomTape.drop, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using + hn'.1 i (by omega) + · simpa [RandomTape.drop, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hn'.2 + · rw [ht]; ring + | _ => intro hc; cases hc + exact aux he rfl + +/-- Each finite runtime atom is geometric. Positive per-attempt cost makes attempt +counts distinguishable in the time PMF. -/ +theorem retryZero_timePMF (C : CostModel) (r : Reg) (s : State w) + (hC : 0 < C.rand + C.branch) (n : ℕ) : + runTimePMF C (retryZero r) s (((n + 1) * (C.rand + C.branch) : ℕ) : ℕ∞) = + (1 - ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹) ^ n * ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹ := by + rw [runTimePMF_apply] + have he : {tape | runTime C (retryZero r) s tape = + (((n + 1) * (C.rand + C.branch) : ℕ) : ℕ∞)} = + RandomTape.drop s.tapePos ⁻¹' RandomTape.firstZero n := by + ext tape + rw [Set.mem_setOf_eq, runTime_eq_coe_iff] + constructor + · rintro ⟨s', d, p, hexec⟩ + obtain ⟨m, hm, ht⟩ := retryZero_exec_firstZero hexec + have : n = m := by nlinarith + subst m + exact hm + · intro hn + exact ⟨_, 0, 0, retryZero_exec C r s tape n hn⟩ + rw [he, ← Measure.map_apply (RandomTape.measurable_drop _) (RandomTape.measurableSet_firstZero _), + uniformTape_drop, uniformTape_firstZero] + +/-- Almost-sure correctness of unbounded retry, for any word width and starting +cursor. Expected time is at most `2^w` times the sampling-and-branch cost. -/ +theorem retryZero_spec (C : CostModel) (r : Reg) : + ProbTriple C (fun _ : State w => True) (retryZero r) (fun s => s.regs r = 0) + ((2 ^ w : ℕ) * (C.rand + C.branch) : ℝ≥0∞) 0 0 := by + let E (s : State w) (n : ℕ) : Set (RandomTape w) := RandomTape.drop s.tapePos ⁻¹' RandomTape.firstZero n + have hm (s : State w) n : MeasurableSet (E s n) := + (RandomTape.measurable_drop s.tapePos) (RandomTape.measurableSet_firstZero n) + have hmass (s : State w) n : uniformTape w (E s n) = + (1 - ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹) ^ n * ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹ := by + rw [show uniformTape w (E s n) = + ((uniformTape w).map (RandomTape.drop s.tapePos)) (RandomTape.firstZero n) from + (Measure.map_apply (RandomTape.measurable_drop _) (RandomTape.measurableSet_firstZero _)).symm, + uniformTape_drop, uniformTape_firstZero] + apply ProbTriple.of_countable_cases E (fun n => (n + 1) * (C.rand + C.branch)) hm + · intro s n m hne + exact (RandomTape.firstZero_disjoint hne).preimage _ + · intro s _ + simp_rw [hmass] + exact geometric_mass _ (by positivity) + · intro s _ n tape hn + exact ⟨_, _, 0, 0, retryZero_exec C r s tape n hn, by simp [State.setReg], + le_rfl, le_rfl, le_rfl⟩ + · intro s _ + simp_rw [hmass] + simpa only [Nat.cast_add] using le_of_eq (geometric_cost (2 ^ w) (C.rand + C.branch) (by positivity)) + +/-- In particular, the infinity atom is zero; this is not an assumption of the model. -/ +theorem retryZero_almostSure (C : CostModel) (r : Reg) (s : State w) : + runTimePMF C (retryZero r) s ⊤ = 0 := by + apply (runTimePMF_top_eq_zero_iff C (retryZero r) s).mpr + filter_upwards [(retryZero_spec C r s trivial).1] with tape ht + obtain ⟨s', t, d, p, he, _, _, _⟩ := ht + exact ⟨s', t, d, p, he⟩ + +/-- Exact expected runtime, derived from the runtime PMF. -/ +theorem retryZero_expect (C : CostModel) (r : Reg) (s : State w) + (hC : 0 < C.rand + C.branch) : + (runTimePMF C (retryZero r) s).expect ENat.toENNReal = + ((2 ^ w : ℕ) : ℝ≥0∞) * (C.rand + C.branch) := by + apply le_antisymm + · exact (retryZero_spec C r s trivial).2 + · let time (n : ℕ) : ℕ∞ := ((n + 1) * (C.rand + C.branch) : ℕ) + have hinj : Function.Injective time := by + intro n m h + dsimp only [time] at h + have h' : (n + 1) * (C.rand + C.branch) = (m + 1) * (C.rand + C.branch) := by + exact_mod_cast h + nlinarith + have h := ENNReal.tsum_comp_le_tsum_of_injective hinj + (fun t => runTimePMF C (retryZero r) s t * ENat.toENNReal t) + simp only [time, retryZero_timePMF C r s hC, ENat.toENNReal_coe] at h + rw [geometric_cost (2 ^ w) (C.rand + C.branch) (by positivity)] at h + simpa only [Nat.cast_add, PMF.expect] using h + +/-- A tape with no zero never safely terminates, despite almost-sure termination +under the uniform tape measure. -/ +theorem retryZero_no_zero {C : CostModel} {r : Reg} {s : State w} {tape : RandomTape w} + (h : ∀ i, tape i ≠ 0) : runTime C (retryZero r) s tape = ⊤ := by + apply (runTime_eq_top_iff tape).mpr + rintro ⟨s', t, d, p, he⟩ + obtain ⟨n, hn, _⟩ := retryZero_exec_firstZero he + exact h (s.tapePos + n) hn.2 + +end Caliper diff --git a/Caliper/Tape.lean b/Caliper/Tape.lean new file mode 100644 index 0000000..ad0970f --- /dev/null +++ b/Caliper/Tape.lean @@ -0,0 +1,207 @@ +import Caliper.Core + +/-! +# Deterministic execution against a word tape + +The input tape is immutable. Only `rand` advances its cursor, so an execution +observes a finite prefix and can be replayed with any tape agreeing on that prefix. +-/ + +namespace Caliper + +variable {w : ℕ} {C : CostModel} {tape : RandomTape w} + +/-- Statements that never consume an input-tape word. -/ +def Stmt.RandomFree : Stmt w → Prop + | .rand _ => False + | .seq a b => a.RandomFree ∧ b.RandomFree + | .ifNZ _ a b => a.RandomFree ∧ b.RandomFree + | .whileNZ g _ b => g.RandomFree ∧ b.RandomFree + | _ => True + +instance instDecidableRandomFree : ∀ (c : Stmt w), Decidable c.RandomFree + | .rand _ => inferInstanceAs (Decidable False) + | .seq a b | .ifNZ _ a b => + have := instDecidableRandomFree a + have := instDecidableRandomFree b + inferInstanceAs (Decidable (_ ∧ _)) + | .whileNZ g _ b => + have := instDecidableRandomFree g + have := instDecidableRandomFree b + inferInstanceAs (Decidable (_ ∧ _)) + | .skip | .imm .. | .mov .. | .un .. | .bin .. | .memAlloc .. | .memAllocI .. + | .memFree .. | .memLen .. | .memLoad .. | .memStore .. | .memPush .. | .memPop .. => + inferInstanceAs (Decidable True) + +/-- Programs cannot observe elapsed time: changing every instruction price +preserves termination, the returned state, and both memory costs. -/ +theorem Exec.withCostModel {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) (C' : CostModel) : + ∃ t', Exec C' tape c s s' t' d p := by + induction h with + | seq _ _ ih₁ ih₂ => + obtain ⟨t₁, h₁⟩ := ih₁ + obtain ⟨t₂, h₂⟩ := ih₂ + exact ⟨_, .seq h₁ h₂⟩ + | ifNZ_true hn _ ih => + obtain ⟨t, h⟩ := ih + exact ⟨_, .ifNZ_true hn h⟩ + | ifNZ_false hz _ ih => + obtain ⟨t, h⟩ := ih + exact ⟨_, .ifNZ_false hz h⟩ + | while_done _ hz ih => + obtain ⟨t, h⟩ := ih + exact ⟨_, .while_done h hz⟩ + | while_step _ hn _ _ ihg ihb ihl => + obtain ⟨tg, hg⟩ := ihg + obtain ⟨tb, hb⟩ := ihb + obtain ⟨tl, hl⟩ := ihl + exact ⟨_, .while_step hg hn hb hl⟩ + | skip => exact ⟨_, .skip⟩ + | imm => exact ⟨_, .imm⟩ + | rand => exact ⟨_, .rand⟩ + | mov => exact ⟨_, .mov⟩ + | un => exact ⟨_, .un⟩ + | bin => exact ⟨_, .bin⟩ + | memAlloc => exact ⟨_, .memAlloc⟩ + | memAllocI => exact ⟨_, .memAllocI⟩ + | memFree => exact ⟨_, .memFree⟩ + | memLen => exact ⟨_, .memLen⟩ + | memLoad h => exact ⟨_, .memLoad h⟩ + | memStore h => exact ⟨_, .memStore h⟩ + | memPush h => exact ⟨_, .memPush h⟩ + | memPop => exact ⟨_, .memPop⟩ + +/-- The input cursor never moves backwards. -/ +theorem Exec.tapePos_mono {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) : s.tapePos ≤ s'.tapePos := by + induction h <;> simp_all -failIfUnchanged [State.setReg, State.setBuf, State.allocBuf, State.readRandom] <;> + omega + +/-- Random-free programs leave the input cursor unchanged. -/ +theorem Exec.tapePos_eq_of_randomFree {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) (hc : c.RandomFree) : s'.tapePos = s.tapePos := by + induction h <;> simp_all [Stmt.RandomFree, State.setReg, State.setBuf, State.allocBuf] + +/-- Every terminating derivation is returned by all sufficiently large fuels. -/ +theorem Exec.run_eventually {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) : + ∃ n, ∀ f, n ≤ f → run C tape f c s = some (s', t, d, p) := by + induction h with + | seq _ _ ih₁ ih₂ => + obtain ⟨n₁, ih₁⟩ := ih₁ + obtain ⟨n₂, ih₂⟩ := ih₂ + refine ⟨max n₁ n₂ + 1, ?_⟩ + intro f hf + cases f with + | zero => omega + | succ f => simp [run, ih₁ f (by omega), ih₂ f (by omega)] + | ifNZ_true hn _ ih => + obtain ⟨n, ih⟩ := ih + refine ⟨n + 1, ?_⟩ + intro f hf + cases f with + | zero => omega + | succ f => simp only [run, if_neg hn, ih f (by omega), Option.bind_eq_bind, Option.bind_some] + | ifNZ_false hz _ ih => + obtain ⟨n, ih⟩ := ih + refine ⟨n + 1, ?_⟩ + intro f hf + cases f with + | zero => omega + | succ f => simp [run, hz, ih f (by omega)] + | while_done _ hz ih => + obtain ⟨n, ih⟩ := ih + refine ⟨n + 1, ?_⟩ + intro f hf + cases f with + | zero => omega + | succ f => simp [run, hz, ih f (by omega)] + | while_step _ hn _ _ ihg ihb ihl => + obtain ⟨ng, ihg⟩ := ihg + obtain ⟨nb, ihb⟩ := ihb + obtain ⟨nl, ihl⟩ := ihl + refine ⟨max ng (max nb nl) + 1, ?_⟩ + intro f hf + cases f with + | zero => omega + | succ f => simp only [run, ihg f (by omega), Option.bind_eq_bind, Option.bind_some, if_neg hn, + ihb f (by omega), ihl f (by omega)] + | _ => + refine ⟨1, ?_⟩ + intro f hf + cases f <;> simp_all [run] + +/-- Interpreter completeness for terminating executions. -/ +theorem run_complete {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) : ∃ f, run C tape f c s = some (s', t, d, p) := by + obtain ⟨n, hn⟩ := h.run_eventually + exact ⟨n, hn n le_rfl⟩ + +/-- Increasing fuel cannot change or lose a successful interpreter result. -/ +theorem run_mono {f g : ℕ} (hfg : f ≤ g) (c : Stmt w) (s : State w) + {result : State w × ℕ × ℤ × ℤ} (h : run C tape f c s = some result) : + run C tape g c s = some result := by + induction f generalizing g c s result with + | zero => simp [run] at h + | succ f ih => + cases g with + | zero => omega + | succ g => + have hfg' : f ≤ g := by omega + cases c with + | seq c₁ c₂ => + simp only [run, Option.bind_eq_bind, Option.bind_eq_some_iff] at h ⊢ + obtain ⟨r₁, h₁, r₂, h₂, hr⟩ := h + exact ⟨r₁, ih hfg' _ _ h₁, r₂, ih hfg' _ _ h₂, hr⟩ + | ifNZ r thn els => + simp only [run] at h ⊢ + split at h <;> rename_i hc + all_goals simp only [hc, ↓reduceIte, Option.bind_eq_bind, Option.bind_eq_some_iff] at h ⊢ + all_goals obtain ⟨r', hr', heq⟩ := h; exact ⟨r', ih hfg' _ _ hr', heq⟩ + | whileNZ guard r body => + simp only [run, Option.bind_eq_bind, Option.bind_eq_some_iff] at h ⊢ + obtain ⟨rg, hg, h⟩ := h + refine ⟨rg, ih hfg' _ _ hg, ?_⟩ + split at h <;> rename_i hc + · simp only [hc, ↓reduceIte]; exact h + · simp only [hc, ↓reduceIte] + simp only [Option.bind_eq_some_iff] at h ⊢ + obtain ⟨rb, hb, rl, hl, heq⟩ := h + exact ⟨rb, ih hfg' _ _ hb, rl, ih hfg' _ _ hl, heq⟩ + | _ => exact h + +/-- Only tape words consumed by the derivation can affect its outcome. -/ +theorem Exec.withTape {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) (other : RandomTape w) + (agree : ∀ i, s.tapePos ≤ i → i < s'.tapePos → other i = tape i) : + Exec C other c s s' t d p := by + induction h with + | @rand d s => + have hv := agree _ le_rfl (Nat.lt_succ_self _) + simpa only [State.readRandom, hv] using (Exec.rand (C := C) (tape := other) (d := d) (s := s)) + | seq h₁ h₂ ih₁ ih₂ => + exact .seq (ih₁ fun i hlo hhi => agree i hlo (lt_of_lt_of_le hhi h₂.tapePos_mono)) + (ih₂ fun i hlo hhi => agree i (h₁.tapePos_mono.trans hlo) hhi) + | ifNZ_true hn _ ih => exact .ifNZ_true hn (ih agree) + | ifNZ_false hz _ ih => exact .ifNZ_false hz (ih agree) + | while_done _ hz ih => exact .while_done (ih agree) hz + | while_step hg hn hb hl ihg ihb ihl => + exact .while_step + (ihg fun i hlo hhi => agree i hlo + (lt_of_lt_of_le hhi (hb.tapePos_mono.trans hl.tapePos_mono))) hn + (ihb fun i hlo hhi => agree i (hg.tapePos_mono.trans hlo) + (lt_of_lt_of_le hhi hl.tapePos_mono)) + (ihl fun i hlo hhi => agree i ((hg.tapePos_mono.trans hb.tapePos_mono).trans hlo) hhi) + | _ => constructor <;> assumption + +/-- Changing the tape cannot change a random-free execution. -/ +theorem Exec.withTape_of_randomFree {c : Stmt w} {s s' : State w} {t : ℕ} {d p : ℤ} + (h : Exec C tape c s s' t d p) (hc : c.RandomFree) (other : RandomTape w) : + Exec C other c s s' t d p := by + apply h.withTape other + intro i hlo hhi + have := h.tapePos_eq_of_randomFree hc + omega + +end Caliper diff --git a/Caliper/TapeMeasure.lean b/Caliper/TapeMeasure.lean new file mode 100644 index 0000000..84d9a37 --- /dev/null +++ b/Caliper/TapeMeasure.lean @@ -0,0 +1,210 @@ +import Caliper.Probability +import Mathlib.Probability.Independence.Integration + +/-! +# Fresh tails of uniform word tapes + +Prefix events are independent of the unread suffix. The stopped-tail theorem +extends this to an execution-dependent cursor using a countable partition by the +number of consumed words. +-/ + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace Caliper + +variable {w : ℕ} + +def RandomTape.prefix (n : ℕ) (tape : RandomTape w) : Fin n → Word w := + fun i => tape i + +def RandomTape.drop (n : ℕ) (tape : RandomTape w) : RandomTape w := + fun i => tape (n + i) + +@[fun_prop] theorem RandomTape.measurable_prefix (n : ℕ) : + Measurable (RandomTape.prefix (w := w) n) := + measurable_pi_iff.mpr fun i => measurable_pi_apply (i : ℕ) + +@[fun_prop] theorem RandomTape.measurable_drop (n : ℕ) : + Measurable (RandomTape.drop (w := w) n) := + measurable_pi_iff.mpr fun i => measurable_pi_apply (n + i) + +/-- Dropping a fixed prefix preserves the uniform tape law. -/ +theorem uniformTape_drop (n : ℕ) : + (uniformTape w).map (RandomTape.drop n) = uniformTape w := + Measure.map_infinitePi_infinitePi_of_inj (P := fun _ : ℕ => + (PMF.uniformOfFintype (Word w)).toMeasure) (f := fun i => n + i) + (fun _ _ h => Nat.add_left_cancel h) + +/-- The sigma algebra generated by the first `n` tape words. -/ +@[reducible] def RandomTape.prefixSigma (n : ℕ) : MeasurableSpace (RandomTape w) := + ⨆ i : ℕ, ⨆ (_ : i < n), (inferInstance : MeasurableSpace (Word w)).comap (fun tape => tape i) + +@[reducible] def RandomTape.tailSigma (n : ℕ) : MeasurableSpace (RandomTape w) := + ⨆ i : ℕ, ⨆ (_ : n ≤ i), (inferInstance : MeasurableSpace (Word w)).comap (fun tape => tape i) + +theorem RandomTape.prefixSigma_le (n : ℕ) : + RandomTape.prefixSigma (w := w) n ≤ (inferInstance : MeasurableSpace (RandomTape w)) := by + apply iSup_le + intro i + apply iSup_le + intro _ + exact (measurable_pi_apply i).comap_le + +private theorem prefix_measurable (n : ℕ) : + @Measurable (RandomTape w) (Fin n → Word w) (RandomTape.prefixSigma n) _ + (RandomTape.prefix n) := by + letI : MeasurableSpace (RandomTape w) := RandomTape.prefixSigma n + apply measurable_pi_iff.mpr + intro i + apply Measurable.of_comap_le + exact le_iSup_of_le (i : ℕ) (le_iSup_of_le i.isLt le_rfl) + +theorem RandomTape.drop_measurable_tail (n : ℕ) : + @Measurable (RandomTape w) (RandomTape w) (RandomTape.tailSigma n) _ + (RandomTape.drop n) := by + letI : MeasurableSpace (RandomTape w) := RandomTape.tailSigma n + apply measurable_pi_iff.mpr + intro i + apply Measurable.of_comap_le + exact le_iSup_of_le (n + i) (le_iSup_of_le (Nat.le_add_right n i) le_rfl) + +theorem uniformTape_prefix_tail_independent (n : ℕ) : + Indep (RandomTape.prefixSigma (w := w) n) (RandomTape.tailSigma n) (uniformTape w) := by + apply indep_iSup_of_disjoint (fun i => (measurable_pi_apply i).comap_le) + uniformTape_independent.iIndep + exact Set.disjoint_left.mpr fun i hi hni => Nat.not_lt_of_ge hni hi + +theorem RandomTape.tailSigma_le (n : ℕ) : + RandomTape.tailSigma (w := w) n ≤ (inferInstance : MeasurableSpace (RandomTape w)) := by + apply iSup_le + intro i + apply iSup_le + intro _ + exact (measurable_pi_apply i).comap_le + +/-- Complete a tail by putting zeros before its starting position. -/ +def RandomTape.restore (n : ℕ) (tail : RandomTape w) : RandomTape w := + fun i => if n ≤ i then tail (i - n) else 0 + +@[fun_prop] theorem RandomTape.measurable_restore (n : ℕ) : + Measurable (RandomTape.restore (w := w) n) := by + apply measurable_pi_iff.mpr + intro i + by_cases hi : n ≤ i + · simpa only [RandomTape.restore, if_pos hi] using (measurable_pi_apply (i - n)) + · simpa only [RandomTape.restore, if_neg hi] using (measurable_const (a := (0 : Word w))) + +/-- Replacing the unread suffix by an equal suffix preserves all terminating results. -/ +theorem exec_restore_drop_iff (C : CostModel) (c : Stmt w) (s s' : State w) + (t : ℕ) (d p : ℤ) (tape : RandomTape w) : + Exec C (RandomTape.restore s.tapePos (RandomTape.drop s.tapePos tape)) c s s' t d p ↔ + Exec C tape c s s' t d p := by + have ha i (hi : s.tapePos ≤ i) : + RandomTape.restore s.tapePos (RandomTape.drop s.tapePos tape) i = tape i := by + simp only [RandomTape.restore, RandomTape.drop, if_pos hi, Nat.add_sub_of_le hi] + constructor + · intro he + exact he.withTape tape (fun i hi _ => (ha i hi).symm) + · intro he + exact he.withTape _ (fun i hi _ => ha i hi) + +/-- Termination time depends measurably only on the unread suffix. -/ +theorem runTime_tail_measurable (C : CostModel) (c : Stmt w) (s : State w) : + Measurable[RandomTape.tailSigma s.tapePos] (runTime C c s) := by + have heq : runTime C c s = + (runTime C c s ∘ RandomTape.restore s.tapePos) ∘ RandomTape.drop s.tapePos := by + funext tape + dsimp only [Function.comp_apply] + by_cases h : ∃ s' t d p, Exec C tape c s s' t d p + · obtain ⟨s', t, d, p, he⟩ := h + rw [runTime_of_exec he, + runTime_of_exec ((exec_restore_drop_iff C c s s' t d p tape).mpr he)] + · have h' : ¬ ∃ s' t d p, + Exec C (RandomTape.restore s.tapePos (RandomTape.drop s.tapePos tape)) c s s' t d p := by + simpa only [exec_restore_drop_iff] using h + rw [(runTime_eq_top_iff tape).mpr h, + (runTime_eq_top_iff _).mpr h'] + rw [heq] + exact ((measurable_runTime C c s).comp + (RandomTape.measurable_restore s.tapePos)).comp (RandomTape.drop_measurable_tail s.tapePos) + +/-- Integrating a future observable over a prefix event factors into mass and expectation. -/ +theorem lintegral_prefix_indicator_future (n : ℕ) {E : Set (RandomTape w)} + (hE : MeasurableSet[RandomTape.prefixSigma n] E) (f : RandomTape w → ℝ≥0∞) + (hf : Measurable[RandomTape.tailSigma n] f) : + (∫⁻ tape, E.indicator f tape ∂uniformTape w) = + uniformTape w E * ∫⁻ tape, f tape ∂uniformTape w := by + classical + have hi : Measurable[RandomTape.prefixSigma n] + (E.indicator (fun _ : RandomTape w => (1 : ℝ≥0∞))) := measurable_const.indicator hE + have h := lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace + (RandomTape.prefixSigma_le n) (RandomTape.tailSigma_le n) + (uniformTape_prefix_tail_independent n) hi hf + convert h using 1 + · apply lintegral_congr + intro tape + by_cases ht : tape ∈ E <;> simp [Set.indicator, ht] + · rw [lintegral_indicator (RandomTape.prefixSigma_le n _ hE)] + simp + +/-- The prefix tuple and the remaining infinite tape are independent. -/ +theorem uniformTape_prefix_drop_independent (n : ℕ) : + IndepFun (RandomTape.prefix (w := w) n) (RandomTape.drop n) (uniformTape w) := by + rw [IndepFun_iff_Indep] + exact indep_of_indep_of_le (uniformTape_prefix_tail_independent n) + (prefix_measurable n).comap_le (RandomTape.drop_measurable_tail n).comap_le + +/-- A prefix-measurable event cannot bias any measurable event on the unread tail. -/ +theorem uniformTape_prefix_inter_drop (n : ℕ) {E F : Set (RandomTape w)} + (hE : MeasurableSet[RandomTape.prefixSigma n] E) (hF : MeasurableSet F) : + uniformTape w (E ∩ RandomTape.drop n ⁻¹' F) = uniformTape w E * uniformTape w F := by + have h := (Indep_iff _ _ _).mp (uniformTape_prefix_tail_independent (w := w) n) + E (RandomTape.drop n ⁻¹' F) hE ((RandomTape.drop_measurable_tail n) hF) + have hdrop : uniformTape w (RandomTape.drop n ⁻¹' F) = uniformTape w F := by + rw [← Measure.map_apply (RandomTape.measurable_drop n) hF, uniformTape_drop] + exact h.trans (congrArg (uniformTape w E * ·) hdrop) + +/-- Fixed-prefix invariance is enough for prefix measurability. -/ +theorem RandomTape.prefix_measurableSet (n : ℕ) (E : Set (RandomTape w)) + (hE : ∀ tape other, (∀ i < n, other i = tape i) → (other ∈ E ↔ tape ∈ E)) : + MeasurableSet[RandomTape.prefixSigma n] E := by + classical + let extend : (Fin n → Word w) → RandomTape w := + fun xs i => if h : i < n then xs ⟨i, h⟩ else 0 + have hEq : E = RandomTape.prefix n ⁻¹' {xs | extend xs ∈ E} := by + ext tape + exact (hE tape (extend (RandomTape.prefix n tape)) (by + intro i hi + simp only [extend, dif_pos hi, RandomTape.prefix])).symm + rw [hEq] + exact prefix_measurable n ((Set.to_countable _).measurableSet) + +/-- Termination at cursor `n` is determined by the first `n` words. -/ +theorem measurableSet_exec_cursor (C : CostModel) (c : Stmt w) (s : State w) (n : ℕ) + (Q : State w → ℕ → ℤ → ℤ → Prop) : + MeasurableSet[RandomTape.prefixSigma n] + {tape | ∃ s' t d p, Exec C tape c s s' t d p ∧ s'.tapePos = n ∧ Q s' t d p} := by + apply RandomTape.prefix_measurableSet + intro tape other ha + constructor + · rintro ⟨s', t, d, p, he, hn, hq⟩ + exact ⟨s', t, d, p, he.withTape tape (fun i _ hi => (ha i (by omega)).symm), hn, hq⟩ + · rintro ⟨s', t, d, p, he, hn, hq⟩ + exact ⟨s', t, d, p, he.withTape other (fun i _ hi => ha i (by omega)), hn, hq⟩ + +/-- Fresh-tail factorization over a countable partition of consumed prefixes. -/ +theorem uniformTape_partition_drop {α : Type*} [Countable α] + (n : α → ℕ) (E : α → Set (RandomTape w)) + (hE : ∀ a, MeasurableSet[RandomTape.prefixSigma (n a)] (E a)) + (hd : Pairwise (fun a b => Disjoint (E a) (E b))) {F : Set (RandomTape w)} (hF : MeasurableSet F) : + uniformTape w (⋃ a, E a ∩ RandomTape.drop (n a) ⁻¹' F) = + uniformTape w (⋃ a, E a) * uniformTape w F := by + have hm a : MeasurableSet (E a) := (RandomTape.prefixSigma_le (n a)) _ (hE a) + rw [measure_iUnion (fun a b hab => (hd hab).mono Set.inter_subset_left Set.inter_subset_left) + (fun a => (hm a).inter ((RandomTape.measurable_drop (n a)) hF))] + simp_rw [uniformTape_prefix_inter_drop _ (hE _) hF] + rw [ENNReal.tsum_mul_right, measure_iUnion hd hm] + +end Caliper diff --git a/Caliper/Triple.lean b/Caliper/Triple.lean index d788878..a32252a 100644 --- a/Caliper/Triple.lean +++ b/Caliper/Triple.lean @@ -1,9 +1,9 @@ -import Caliper.Core +import Caliper.Tape /-! # Upper-bound Hoare triples -`Triple C P c Q T D M` is total correctness with resource *upper bounds*: from any +`Triple C tape P c Q T D M` is total correctness with resource *upper bounds*: from any state satisfying `P`, the statement terminates and is memory-safe, an `Exec` derivation existing, the result satisfies `Q`, and @@ -36,39 +36,47 @@ deterministic the two judgments recombine into a full `Triple` namespace Caliper -variable {w : ℕ} {C : CostModel} +variable {w : ℕ} {tape : RandomTape w} {C : CostModel} /-- Total-correctness triple with time bound `T`, net-memory bound `D` and peak-memory bound `M`. -/ -def Triple (C : CostModel) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) +def Triple (C : CostModel) (tape : RandomTape w) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) (T : ℕ) (D M : ℤ) : Prop := - ∀ s, P s → ∃ s' t d p, Exec C c s s' t d p ∧ Q s' ∧ t ≤ T ∧ d ≤ D ∧ p ≤ M + ∀ s, P s → ∃ s' t d p, Exec C tape c s s' t d p ∧ Q s' ∧ t ≤ T ∧ d ≤ D ∧ p ≤ M namespace Triple +/-- Reuse a random-free subroutine's fixed-tape specification on any caller tape. -/ +theorem withTape_of_randomFree {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} + (h : Triple C tape P c Q T D M) (hc : c.RandomFree) (other : RandomTape w) : + Triple C other P c Q T D M := by + intro s hs + obtain ⟨s', t, d, p, he, hq, ht, hd, hp⟩ := h s hs + exact ⟨s', t, d, p, he.withTape_of_randomFree hc other, hq, ht, hd, hp⟩ + /-- Consequence: strengthen the precondition, weaken the postcondition, raise the bounds. This is why proving `≤` bounds beats proving exact costs: bounds compose without case splits. -/ theorem conseq {P P' Q Q' : State w → Prop} {c : Stmt w} {T T' : ℕ} {D D' M M' : ℤ} - (h : Triple C P c Q T D M) (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) - (hT : T ≤ T') (hD : D ≤ D') (hM : M ≤ M') : Triple C P' c Q' T' D' M' := by + (h : Triple C tape P c Q T D M) (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) + (hT : T ≤ T') (hD : D ≤ D') (hM : M ≤ M') : Triple C tape P' c Q' T' D' M' := by intro s hs obtain ⟨s', t, d, p, hexec, hq, ht, hd, hp⟩ := h s (hP s hs) exact ⟨s', t, d, p, hexec, hQ s' hq, ht.trans hT, hd.trans hD, hp.trans hM⟩ theorem weaken {P Q : State w → Prop} {c : Stmt w} {T T' : ℕ} {D D' M M' : ℤ} - (h : Triple C P c Q T D M) (hT : T ≤ T') (hD : D ≤ D') (hM : M ≤ M') : - Triple C P c Q T' D' M' := + (h : Triple C tape P c Q T D M) (hT : T ≤ T') (hD : D ≤ D') (hM : M ≤ M') : + Triple C tape P c Q T' D' M' := h.conseq (fun _ => id) (fun _ => id) hT hD hM protected theorem skip {P Q : State w → Prop} (h : ∀ s, P s → Q s) : - Triple C P (.skip (w := w)) Q 0 0 0 := + Triple C tape P (.skip (w := w)) Q 0 0 0 := fun s hs => ⟨s, 0, 0, 0, .skip, h s hs, le_refl _, le_refl _, le_refl _⟩ protected theorem seq {P R Q : State w → Prop} {c₁ c₂ : Stmt w} {T₁ T₂ : ℕ} {D₁ M₁ D₂ M₂ : ℤ} - (h₁ : Triple C P c₁ R T₁ D₁ M₁) (h₂ : Triple C R c₂ Q T₂ D₂ M₂) : - Triple C P (c₁ ;; c₂) Q (T₁ + T₂) (D₁ + D₂) (max M₁ (D₁ + M₂)) := by + (h₁ : Triple C tape P c₁ R T₁ D₁ M₁) (h₂ : Triple C tape R c₂ Q T₂ D₂ M₂) : + Triple C tape P (c₁ ;; c₂) Q (T₁ + T₂) (D₁ + D₂) (max M₁ (D₁ + M₂)) := by intro s hs obtain ⟨s₁, t₁, d₁, p₁, he₁, hr, ht₁, hd₁, hp₁⟩ := h₁ s hs obtain ⟨s₂, t₂, d₂, p₂, he₂, hq, ht₂, hd₂, hp₂⟩ := h₂ s₁ hr @@ -81,21 +89,27 @@ Each takes the "forward" form: the precondition must imply the postcondition of updated state. Chained with `seq` these give a weakest-precondition-style calculation. -/ protected theorem imm {P Q : State w → Prop} {d : Reg} {v : Word w} - (h : ∀ s, P s → Q (s.setReg d v)) : Triple C P (.imm d v) Q C.imm 0 0 := + (h : ∀ s, P s → Q (s.setReg d v)) : Triple C tape P (.imm d v) Q C.imm 0 0 := fun s hs => ⟨_, _, _, _, .imm, h s hs, le_refl _, le_refl _, le_refl _⟩ +/-- The postcondition is checked against the word at the current tape cursor. -/ +protected theorem rand {P Q : State w → Prop} {d : Reg} + (h : ∀ s, P s → Q (s.readRandom tape d)) : + Triple C tape P (.rand d) Q C.rand 0 0 := + fun s hs => ⟨_, _, _, _, .rand, h s hs, le_refl _, le_refl _, le_refl _⟩ + protected theorem mov {P Q : State w → Prop} {d a : Reg} - (h : ∀ s, P s → Q (s.setReg d (s.regs a))) : Triple C P (.mov d a) Q C.mov 0 0 := + (h : ∀ s, P s → Q (s.setReg d (s.regs a))) : Triple C tape P (.mov d a) Q C.mov 0 0 := fun s hs => ⟨_, _, _, _, .mov, h s hs, le_refl _, le_refl _, le_refl _⟩ protected theorem un {P Q : State w → Prop} {op : UnOp} {d a : Reg} (h : ∀ s, P s → Q (s.setReg d (op.eval (s.regs a)))) : - Triple C P (.un op d a) Q (C.un op) 0 0 := + Triple C tape P (.un op d a) Q (C.un op) 0 0 := fun s hs => ⟨_, _, _, _, .un, h s hs, le_refl _, le_refl _, le_refl _⟩ protected theorem bin {P Q : State w → Prop} {op : BinOp} {d a b : Reg} (h : ∀ s, P s → Q (s.setReg d (op.eval (s.regs a) (s.regs b)))) : - Triple C P (.bin op d a b) Q (C.bin op) 0 0 := + Triple C tape P (.bin op d a b) Q (C.bin op) 0 0 := fun s hs => ⟨_, _, _, _, .bin, h s hs, le_refl _, le_refl _, le_refl _⟩ /-- Reserve capacity (dynamic). The caller supplies an upper bound `N` on the @@ -105,7 +119,7 @@ data-dependent time charge `C.memAlloc + newCap * C.allocPerWord ≤ C.memAlloc + N * C.allocPerWord`. -/ protected theorem memAlloc {P Q : State w → Prop} {b : BufId} {n : Reg} {N : ℕ} (h : ∀ s, P s → (s.regs n).toNat ≤ N ∧ Q (s.allocBuf b (s.regs n).toNat)) : - Triple C P (.memAlloc b n) Q (C.memAlloc + N * C.allocPerWord) N N := by + Triple C tape P (.memAlloc b n) Q (C.memAlloc + N * C.allocPerWord) N N := by intro s hs obtain ⟨hN, hq⟩ := h s hs refine ⟨_, _, _, _, .memAlloc, hq, ?_, by omega, by omega⟩ @@ -117,26 +131,26 @@ protected theorem memAlloc {P Q : State w → Prop} {b : BufId} {n : Reg} {N : nonnegative). -/ protected theorem memAllocI {P Q : State w → Prop} {b : BufId} {n : ℕ} (h : ∀ s, P s → Q (s.allocBuf b n)) : - Triple C P (.memAllocI b n) Q (C.memAlloc + n * C.allocPerWord) n n := + Triple C tape P (.memAllocI b n) Q (C.memAlloc + n * C.allocPerWord) n n := fun s hs => ⟨_, _, _, _, .memAllocI, h s hs, le_refl _, by omega, by omega⟩ /-- Free a buffer: never charges memory. -/ protected theorem memFree {P Q : State w → Prop} {b : BufId} - (h : ∀ s, P s → Q (s.allocBuf b 0)) : Triple C P (.memFree b) Q C.memFree 0 0 := + (h : ∀ s, P s → Q (s.allocBuf b 0)) : Triple C tape P (.memFree b) Q C.memFree 0 0 := fun s hs => ⟨_, _, _, _, .memFree, h s hs, le_refl _, by omega, le_refl _⟩ /-- Free with a known lower bound `K` on the capacity being released: credits `-K`. This is the rule that makes an alloc…free block's net vanish. -/ protected theorem memFree' {P Q : State w → Prop} {b : BufId} {K : ℕ} (h : ∀ s, P s → K ≤ s.caps b ∧ Q (s.allocBuf b 0)) : - Triple C P (.memFree b) Q C.memFree (-(K : ℤ)) 0 := by + Triple C tape P (.memFree b) Q C.memFree (-(K : ℤ)) 0 := by intro s hs obtain ⟨hK, hq⟩ := h s hs exact ⟨_, _, _, _, .memFree, hq, le_refl _, by omega, le_refl _⟩ protected theorem memLen {P Q : State w → Prop} {d : Reg} {b : BufId} (h : ∀ s, P s → Q (s.setReg d (BitVec.ofNat w (s.bufs b).size))) : - Triple C P (.memLen d b) Q C.memLen 0 0 := + Triple C tape P (.memLen d b) Q C.memLen 0 0 := fun s hs => ⟨_, _, _, _, .memLen, h s hs, le_refl _, le_refl _, le_refl _⟩ /-- The in-range obligation `hlt` is the memory-safety proof; there is no rule for the @@ -144,7 +158,7 @@ out-of-range case, so a completed triple entails safety. -/ protected theorem memLoad {P Q : State w → Prop} {d : Reg} {b : BufId} {i : Reg} (h : ∀ s, P s → ∃ hlt : (s.regs i).toNat < (s.bufs b).size, Q (s.setReg d (s.bufs b)[(s.regs i).toNat])) : - Triple C P (.memLoad d b i) Q C.memLoad 0 0 := by + Triple C tape P (.memLoad d b i) Q C.memLoad 0 0 := by intro s hs obtain ⟨hlt, hq⟩ := h s hs exact ⟨_, _, _, _, .memLoad hlt, hq, le_refl _, le_refl _, le_refl _⟩ @@ -152,7 +166,7 @@ protected theorem memLoad {P Q : State w → Prop} {d : Reg} {b : BufId} {i : Re protected theorem memStore {P Q : State w → Prop} {b : BufId} {i src : Reg} (h : ∀ s, P s → ∃ hlt : (s.regs i).toNat < (s.bufs b).size, Q (s.setBuf b ((s.bufs b).set (s.regs i).toNat (s.regs src) hlt))) : - Triple C P (.memStore b i src) Q C.memStore 0 0 := by + Triple C tape P (.memStore b i src) Q C.memStore 0 0 := by intro s hs obtain ⟨hlt, hq⟩ := h s hs exact ⟨_, _, _, _, .memStore hlt, hq, le_refl _, le_refl _, le_refl _⟩ @@ -163,7 +177,7 @@ and what makes push worst-case unit time. Memory-neutral: the word was charged a protected theorem memPush {P Q : State w → Prop} {b : BufId} {src : Reg} (h : ∀ s, P s → (s.bufs b).size < s.caps b ∧ Q (s.setBuf b ((s.bufs b).push (s.regs src)))) : - Triple C P (.memPush b src) Q C.memPush 0 0 := by + Triple C tape P (.memPush b src) Q C.memPush 0 0 := by intro s hs obtain ⟨hcap, hq⟩ := h s hs exact ⟨_, _, _, _, .memPush hcap, hq, le_refl _, le_refl _, le_refl _⟩ @@ -171,14 +185,14 @@ protected theorem memPush {P Q : State w → Prop} {b : BufId} {src : Reg} /-- Pop keeps the capacity: memory-neutral. -/ protected theorem memPop {P Q : State w → Prop} {b : BufId} (h : ∀ s, P s → Q (s.setBuf b (s.bufs b).pop)) : - Triple C P (.memPop b) Q C.memPop 0 0 := + Triple C tape P (.memPop b) Q C.memPop 0 0 := fun s hs => ⟨_, _, _, _, .memPop, h s hs, le_refl _, le_refl _, le_refl _⟩ protected theorem ifNZ {P Q : State w → Prop} {r : Reg} {thn els : Stmt w} {T : ℕ} {D M : ℤ} - (ht : Triple C (fun s => P s ∧ s.regs r ≠ 0) thn Q T D M) - (he : Triple C (fun s => P s ∧ s.regs r = 0) els Q T D M) : - Triple C P (.ifNZ r thn els) Q (C.branch + T) D M := by + (ht : Triple C tape (fun s => P s ∧ s.regs r ≠ 0) thn Q T D M) + (he : Triple C tape (fun s => P s ∧ s.regs r = 0) els Q T D M) : + Triple C tape P (.ifNZ r thn els) Q (C.branch + T) D M := by intro s hs by_cases hr : s.regs r = 0 · obtain ⟨s', t, d, p, hexec, hq, hT, hD, hM⟩ := he s ⟨hs, hr⟩ @@ -201,10 +215,10 @@ when each iteration's net `Dg + Db` is `≤ 0`, memory being reused, neither net peak grows with `k`. -/ theorem whileNZ_measure {I J : ℕ → State w → Prop} {g body : Stmt w} {r : Reg} {Tg Tb : ℕ} {Dg Mg Db Mb : ℤ} - (hg : ∀ k, Triple C (I k) g (J k) Tg Dg Mg) + (hg : ∀ k, Triple C tape (I k) g (J k) Tg Dg Mg) (hpos : ∀ k s, J k s → s.regs r ≠ 0 → ∃ k', k = k' + 1) - (hb : ∀ k, Triple C (fun s => J (k + 1) s ∧ s.regs r ≠ 0) body (I k) Tb Db Mb) : - ∀ k, Triple C (I k) (.whileNZ g r body) + (hb : ∀ k, Triple C tape (fun s => J (k + 1) s ∧ s.regs r ≠ 0) body (I k) Tb Db Mb) : + ∀ k, Triple C tape (I k) (.whileNZ g r body) (fun s => ∃ k', J k' s ∧ s.regs r = 0) ((k + 1) * (Tg + C.branch) + k * Tb) (Dg + k * max (Dg + Db) 0) @@ -258,23 +272,23 @@ carried across its triple for free. -/ triple. Instantiate `R` with e.g. `fun s => s.regs 3 = x ∧ s.bufs 0 = arr`; the `hR` hypothesis is discharged by `Exec.frame_reg`/`Exec.frame_buf` + `decide`. -/ theorem frame_post {P Q R : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} - (h : Triple C P c Q T D M) - (hR : ∀ s s' t d p, Exec C c s s' t d p → R s → R s') : - Triple C (fun s => P s ∧ R s) c (fun s => Q s ∧ R s) T D M := by + (h : Triple C tape P c Q T D M) + (hR : ∀ s s' t d p, Exec C tape c s s' t d p → R s → R s') : + Triple C tape (fun s => P s ∧ R s) c (fun s => Q s ∧ R s) T D M := by intro s ⟨hp, hr⟩ obtain ⟨s', t, d, p, hexec, hq, hT, hD, hM⟩ := h s hp exact ⟨s', t, d, p, hexec, ⟨hq, hR s s' t d p hexec hr⟩, hT, hD, hM⟩ /-- Specialization: a register the statement never writes keeps its value. -/ theorem frame_reg {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} {r : Reg} - {v : Word w} (h : Triple C P c Q T D M) (hw : ¬ c.Writes r) : - Triple C (fun s => P s ∧ s.regs r = v) c (fun s => Q s ∧ s.regs r = v) T D M := + {v : Word w} (h : Triple C tape P c Q T D M) (hw : ¬ c.Writes r) : + Triple C tape (fun s => P s ∧ s.regs r = v) c (fun s => Q s ∧ s.regs r = v) T D M := h.frame_post fun _ _ _ _ _ hexec hr => (hexec.frame_reg hw).trans hr /-- Specialization: a buffer the statement never touches keeps its contents. -/ theorem frame_buf {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} {b : BufId} - {arr : Array (Word w)} (h : Triple C P c Q T D M) (ht : ¬ c.Touches b) : - Triple C (fun s => P s ∧ s.bufs b = arr) c (fun s => Q s ∧ s.bufs b = arr) T D M := + {arr : Array (Word w)} (h : Triple C tape P c Q T D M) (ht : ¬ c.Touches b) : + Triple C tape (fun s => P s ∧ s.bufs b = arr) c (fun s => Q s ∧ s.bufs b = arr) T D M := h.frame_post fun _ _ _ _ _ hexec hb => (hexec.frame_buf ht).trans hb end Triple @@ -300,27 +314,27 @@ trip-count-independent space bound but no uniform time bound. -/ /-- Time-only total-correctness triple: from any state satisfying `P`, the statement terminates (memory-safely) in a state satisfying `Q` within `t ≤ T` time units. The execution's memory profile is existentially forgotten. -/ -def TimeTriple (C : CostModel) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) +def TimeTriple (C : CostModel) (tape : RandomTape w) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) (T : ℕ) : Prop := - ∀ s, P s → ∃ s' t d p, Exec C c s s' t d p ∧ Q s' ∧ t ≤ T + ∀ s, P s → ∃ s' t d p, Exec C tape c s s' t d p ∧ Q s' ∧ t ≤ T /-- Space-only total-correctness triple: net live-memory change `d ≤ D` and peak growth `p ≤ M`. The running time is existentially forgotten; the statement still terminates, an `Exec` derivation being exhibited, but `t` is unbounded. -/ -def SpaceTriple (C : CostModel) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) +def SpaceTriple (C : CostModel) (tape : RandomTape w) (P : State w → Prop) (c : Stmt w) (Q : State w → Prop) (D M : ℤ) : Prop := - ∀ s, P s → ∃ s' t d p, Exec C c s s' t d p ∧ Q s' ∧ d ≤ D ∧ p ≤ M + ∀ s, P s → ∃ s' t d p, Exec C tape c s s' t d p ∧ Q s' ∧ d ≤ D ∧ p ≤ M /-- Forget the memory bounds of a full triple. -/ theorem Triple.time {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} - (h : Triple C P c Q T D M) : TimeTriple C P c Q T := by + (h : Triple C tape P c Q T D M) : TimeTriple C tape P c Q T := by intro s hs obtain ⟨s', t, d, p, hexec, hq, hT, _, _⟩ := h s hs exact ⟨s', t, d, p, hexec, hq, hT⟩ /-- Forget the time bound of a full triple. -/ theorem Triple.space {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} - (h : Triple C P c Q T D M) : SpaceTriple C P c Q D M := by + (h : Triple C tape P c Q T D M) : SpaceTriple C tape P c Q D M := by intro s hs obtain ⟨s', t, d, p, hexec, hq, _, hD, hM⟩ := h s hs exact ⟨s', t, d, p, hexec, hq, hD, hM⟩ @@ -331,8 +345,8 @@ namespace TimeTriple time-only and a space-only triple from the same state coincide, and separately proved bounds hold of the one real execution. -/ theorem and_space {P Q₁ Q₂ : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} - (h₁ : TimeTriple C P c Q₁ T) (h₂ : SpaceTriple C P c Q₂ D M) : - Triple C P c (fun s => Q₁ s ∧ Q₂ s) T D M := by + (h₁ : TimeTriple C tape P c Q₁ T) (h₂ : SpaceTriple C tape P c Q₂ D M) : + Triple C tape P c (fun s => Q₁ s ∧ Q₂ s) T D M := by intro s hs obtain ⟨s', t, d, p, hexec, hq₁, hT⟩ := h₁ s hs obtain ⟨s'', t', d', p', hexec', hq₂, hD, hM⟩ := h₂ s hs @@ -341,8 +355,8 @@ theorem and_space {P Q₁ Q₂ : State w → Prop} {c : Stmt w} {T : ℕ} {D M : /-- Recombination when the two judgments share a postcondition. -/ theorem and_space' {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} - (h₁ : TimeTriple C P c Q T) (h₂ : SpaceTriple C P c Q D M) : - Triple C P c Q T D M := + (h₁ : TimeTriple C tape P c Q T) (h₂ : SpaceTriple C tape P c Q D M) : + Triple C tape P c Q T D M := (h₁.and_space h₂).conseq (fun _ => id) (fun _ h => h.1) (le_refl _) (le_refl _) (le_refl _) @@ -350,32 +364,32 @@ theorem and_space' {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {D M : ℤ} the execution the time triple already exhibits satisfies `d ≤ 0 ∧ p ≤ 0` outright (`Exec.allocFree_space`). -/ theorem space_of_allocFree {P Q : State w → Prop} {c : Stmt w} {T : ℕ} - (h : TimeTriple C P c Q T) (ha : c.AllocFree) : SpaceTriple C P c Q 0 0 := by + (h : TimeTriple C tape P c Q T) (ha : c.AllocFree) : SpaceTriple C tape P c Q 0 0 := by intro s hs obtain ⟨s', t, d, p, hexec, hq, _⟩ := h s hs obtain ⟨hd, hp⟩ := hexec.allocFree_space ha exact ⟨s', t, d, p, hexec, hq, hd, hp⟩ theorem conseq {P P' Q Q' : State w → Prop} {c : Stmt w} {T T' : ℕ} - (h : TimeTriple C P c Q T) (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) - (hT : T ≤ T') : TimeTriple C P' c Q' T' := by + (h : TimeTriple C tape P c Q T) (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) + (hT : T ≤ T') : TimeTriple C tape P' c Q' T' := by intro s hs obtain ⟨s', t, d, p, hexec, hq, ht⟩ := h s (hP s hs) exact ⟨s', t, d, p, hexec, hQ s' hq, ht.trans hT⟩ theorem weaken {P Q : State w → Prop} {c : Stmt w} {T T' : ℕ} - (h : TimeTriple C P c Q T) (hT : T ≤ T') : TimeTriple C P c Q T' := + (h : TimeTriple C tape P c Q T) (hT : T ≤ T') : TimeTriple C tape P c Q T' := h.conseq (fun _ => id) (fun _ => id) hT protected theorem skip {P Q : State w → Prop} (h : ∀ s, P s → Q s) : - TimeTriple C P (.skip (w := w)) Q 0 := + TimeTriple C tape P (.skip (w := w)) Q 0 := (Triple.skip h).time /-- Sequencing time bounds is plain addition; none of `Triple.seq`'s (net, peak) profile algebra appears, which is the point of the decoupled judgment. -/ protected theorem seq {P R Q : State w → Prop} {c₁ c₂ : Stmt w} {T₁ T₂ : ℕ} - (h₁ : TimeTriple C P c₁ R T₁) (h₂ : TimeTriple C R c₂ Q T₂) : - TimeTriple C P (c₁ ;; c₂) Q (T₁ + T₂) := by + (h₁ : TimeTriple C tape P c₁ R T₁) (h₂ : TimeTriple C tape R c₂ Q T₂) : + TimeTriple C tape P (c₁ ;; c₂) Q (T₁ + T₂) := by intro s hs obtain ⟨s₁, t₁, d₁, p₁, he₁, hr, ht₁⟩ := h₁ s hs obtain ⟨s₂, t₂, d₂, p₂, he₂, hq, ht₂⟩ := h₂ s₁ hr @@ -388,21 +402,26 @@ Projections of the corresponding `Triple` rules, except `memAlloc`, whose full r carries a memory obligation a time bound does not need. -/ protected theorem imm {P Q : State w → Prop} {d : Reg} {v : Word w} - (h : ∀ s, P s → Q (s.setReg d v)) : TimeTriple C P (.imm d v) Q C.imm := + (h : ∀ s, P s → Q (s.setReg d v)) : TimeTriple C tape P (.imm d v) Q C.imm := (Triple.imm h).time +protected theorem rand {P Q : State w → Prop} {d : Reg} + (h : ∀ s, P s → Q (s.readRandom tape d)) : + TimeTriple C tape P (.rand d) Q C.rand := + (Triple.rand h).time + protected theorem mov {P Q : State w → Prop} {d a : Reg} - (h : ∀ s, P s → Q (s.setReg d (s.regs a))) : TimeTriple C P (.mov d a) Q C.mov := + (h : ∀ s, P s → Q (s.setReg d (s.regs a))) : TimeTriple C tape P (.mov d a) Q C.mov := (Triple.mov h).time protected theorem un {P Q : State w → Prop} {op : UnOp} {d a : Reg} (h : ∀ s, P s → Q (s.setReg d (op.eval (s.regs a)))) : - TimeTriple C P (.un op d a) Q (C.un op) := + TimeTriple C tape P (.un op d a) Q (C.un op) := (Triple.un h).time protected theorem bin {P Q : State w → Prop} {op : BinOp} {d a b : Reg} (h : ∀ s, P s → Q (s.setReg d (op.eval (s.regs a) (s.regs b)))) : - TimeTriple C P (.bin op d a b) Q (C.bin op) := + TimeTriple C tape P (.bin op d a b) Q (C.bin op) := (Triple.bin h).time /-- Reserve capacity (dynamic). Unlike the other time rules the capacity bound `N` @@ -410,51 +429,51 @@ does not disappear: the charge `C.memAlloc + newCap * C.allocPerWord` is data-dependent, so bounding the requested capacity is what a time bound needs. -/ protected theorem memAlloc {P Q : State w → Prop} {b : BufId} {n : Reg} {N : ℕ} (h : ∀ s, P s → (s.regs n).toNat ≤ N ∧ Q (s.allocBuf b (s.regs n).toNat)) : - TimeTriple C P (.memAlloc b n) Q (C.memAlloc + N * C.allocPerWord) := + TimeTriple C tape P (.memAlloc b n) Q (C.memAlloc + N * C.allocPerWord) := (Triple.memAlloc h).time /-- Reserve capacity (immediate): statically priced, no side obligation. -/ protected theorem memAllocI {P Q : State w → Prop} {b : BufId} {n : ℕ} (h : ∀ s, P s → Q (s.allocBuf b n)) : - TimeTriple C P (.memAllocI b n) Q (C.memAlloc + n * C.allocPerWord) := + TimeTriple C tape P (.memAllocI b n) Q (C.memAlloc + n * C.allocPerWord) := (Triple.memAllocI h).time protected theorem memFree {P Q : State w → Prop} {b : BufId} - (h : ∀ s, P s → Q (s.allocBuf b 0)) : TimeTriple C P (.memFree b) Q C.memFree := + (h : ∀ s, P s → Q (s.allocBuf b 0)) : TimeTriple C tape P (.memFree b) Q C.memFree := (Triple.memFree h).time protected theorem memLen {P Q : State w → Prop} {d : Reg} {b : BufId} (h : ∀ s, P s → Q (s.setReg d (BitVec.ofNat w (s.bufs b).size))) : - TimeTriple C P (.memLen d b) Q C.memLen := + TimeTriple C tape P (.memLen d b) Q C.memLen := (Triple.memLen h).time protected theorem memLoad {P Q : State w → Prop} {d : Reg} {b : BufId} {i : Reg} (h : ∀ s, P s → ∃ hlt : (s.regs i).toNat < (s.bufs b).size, Q (s.setReg d (s.bufs b)[(s.regs i).toNat])) : - TimeTriple C P (.memLoad d b i) Q C.memLoad := + TimeTriple C tape P (.memLoad d b i) Q C.memLoad := (Triple.memLoad h).time protected theorem memStore {P Q : State w → Prop} {b : BufId} {i src : Reg} (h : ∀ s, P s → ∃ hlt : (s.regs i).toNat < (s.bufs b).size, Q (s.setBuf b ((s.bufs b).set (s.regs i).toNat (s.regs src) hlt))) : - TimeTriple C P (.memStore b i src) Q C.memStore := + TimeTriple C tape P (.memStore b i src) Q C.memStore := (Triple.memStore h).time protected theorem memPush {P Q : State w → Prop} {b : BufId} {src : Reg} (h : ∀ s, P s → (s.bufs b).size < s.caps b ∧ Q (s.setBuf b ((s.bufs b).push (s.regs src)))) : - TimeTriple C P (.memPush b src) Q C.memPush := + TimeTriple C tape P (.memPush b src) Q C.memPush := (Triple.memPush h).time protected theorem memPop {P Q : State w → Prop} {b : BufId} (h : ∀ s, P s → Q (s.setBuf b (s.bufs b).pop)) : - TimeTriple C P (.memPop b) Q C.memPop := + TimeTriple C tape P (.memPop b) Q C.memPop := (Triple.memPop h).time protected theorem ifNZ {P Q : State w → Prop} {r : Reg} {thn els : Stmt w} {T : ℕ} - (ht : TimeTriple C (fun s => P s ∧ s.regs r ≠ 0) thn Q T) - (he : TimeTriple C (fun s => P s ∧ s.regs r = 0) els Q T) : - TimeTriple C P (.ifNZ r thn els) Q (C.branch + T) := by + (ht : TimeTriple C tape (fun s => P s ∧ s.regs r ≠ 0) thn Q T) + (he : TimeTriple C tape (fun s => P s ∧ s.regs r = 0) els Q T) : + TimeTriple C tape P (.ifNZ r thn els) Q (C.branch + T) := by intro s hs by_cases hr : s.regs r = 0 · obtain ⟨s', t, d, p, hexec, hq, hT⟩ := he s ⟨hs, hr⟩ @@ -467,10 +486,10 @@ protected theorem ifNZ {P Q : State w → Prop} {r : Reg} {thn els : Stmt w} {T hypotheses and no memory conclusion. Time is linear in `k`. -/ theorem whileNZ_measure {I J : ℕ → State w → Prop} {g body : Stmt w} {r : Reg} {Tg Tb : ℕ} - (hg : ∀ k, TimeTriple C (I k) g (J k) Tg) + (hg : ∀ k, TimeTriple C tape (I k) g (J k) Tg) (hpos : ∀ k s, J k s → s.regs r ≠ 0 → ∃ k', k = k' + 1) - (hb : ∀ k, TimeTriple C (fun s => J (k + 1) s ∧ s.regs r ≠ 0) body (I k) Tb) : - ∀ k, TimeTriple C (I k) (.whileNZ g r body) + (hb : ∀ k, TimeTriple C tape (fun s => J (k + 1) s ∧ s.regs r ≠ 0) body (I k) Tb) : + ∀ k, TimeTriple C tape (I k) (.whileNZ g r body) (fun s => ∃ k', J k' s ∧ s.regs r = 0) ((k + 1) * (Tg + C.branch) + k * Tb) := by intro k @@ -500,23 +519,23 @@ theorem whileNZ_measure {I J : ℕ → State w → Prop} {g body : Stmt w} {r : /-! ### Framing -/ theorem frame_post {P Q R : State w → Prop} {c : Stmt w} {T : ℕ} - (h : TimeTriple C P c Q T) - (hR : ∀ s s' t d p, Exec C c s s' t d p → R s → R s') : - TimeTriple C (fun s => P s ∧ R s) c (fun s => Q s ∧ R s) T := by + (h : TimeTriple C tape P c Q T) + (hR : ∀ s s' t d p, Exec C tape c s s' t d p → R s → R s') : + TimeTriple C tape (fun s => P s ∧ R s) c (fun s => Q s ∧ R s) T := by intro s ⟨hp, hr⟩ obtain ⟨s', t, d, p, hexec, hq, hT⟩ := h s hp exact ⟨s', t, d, p, hexec, ⟨hq, hR s s' t d p hexec hr⟩, hT⟩ /-- A register the statement never writes keeps its value. -/ theorem frame_reg {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {r : Reg} - {v : Word w} (h : TimeTriple C P c Q T) (hw : ¬ c.Writes r) : - TimeTriple C (fun s => P s ∧ s.regs r = v) c (fun s => Q s ∧ s.regs r = v) T := + {v : Word w} (h : TimeTriple C tape P c Q T) (hw : ¬ c.Writes r) : + TimeTriple C tape (fun s => P s ∧ s.regs r = v) c (fun s => Q s ∧ s.regs r = v) T := h.frame_post fun _ _ _ _ _ hexec hr => (hexec.frame_reg hw).trans hr /-- A buffer the statement never touches keeps its contents. -/ theorem frame_buf {P Q : State w → Prop} {c : Stmt w} {T : ℕ} {b : BufId} - {arr : Array (Word w)} (h : TimeTriple C P c Q T) (ht : ¬ c.Touches b) : - TimeTriple C (fun s => P s ∧ s.bufs b = arr) c (fun s => Q s ∧ s.bufs b = arr) T := + {arr : Array (Word w)} (h : TimeTriple C tape P c Q T) (ht : ¬ c.Touches b) : + TimeTriple C tape (fun s => P s ∧ s.bufs b = arr) c (fun s => Q s ∧ s.bufs b = arr) T := h.frame_post fun _ _ _ _ _ hexec hb => (hexec.frame_buf ht).trans hb end TimeTriple @@ -524,26 +543,26 @@ end TimeTriple namespace SpaceTriple theorem conseq {P P' Q Q' : State w → Prop} {c : Stmt w} {D D' M M' : ℤ} - (h : SpaceTriple C P c Q D M) (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) - (hD : D ≤ D') (hM : M ≤ M') : SpaceTriple C P' c Q' D' M' := by + (h : SpaceTriple C tape P c Q D M) (hP : ∀ s, P' s → P s) (hQ : ∀ s, Q s → Q' s) + (hD : D ≤ D') (hM : M ≤ M') : SpaceTriple C tape P' c Q' D' M' := by intro s hs obtain ⟨s', t, d, p, hexec, hq, hd, hp⟩ := h s (hP s hs) exact ⟨s', t, d, p, hexec, hQ s' hq, hd.trans hD, hp.trans hM⟩ theorem weaken {P Q : State w → Prop} {c : Stmt w} {D D' M M' : ℤ} - (h : SpaceTriple C P c Q D M) (hD : D ≤ D') (hM : M ≤ M') : - SpaceTriple C P c Q D' M' := + (h : SpaceTriple C tape P c Q D M) (hD : D ≤ D') (hM : M ≤ M') : + SpaceTriple C tape P c Q D' M' := h.conseq (fun _ => id) (fun _ => id) hD hM protected theorem skip {P Q : State w → Prop} (h : ∀ s, P s → Q s) : - SpaceTriple C P (.skip (w := w)) Q 0 0 := + SpaceTriple C tape P (.skip (w := w)) Q 0 0 := (Triple.skip h).space /-- Sequencing composes the memory profile exactly as in `Triple.seq`, with no time arithmetic anywhere. -/ protected theorem seq {P R Q : State w → Prop} {c₁ c₂ : Stmt w} {D₁ M₁ D₂ M₂ : ℤ} - (h₁ : SpaceTriple C P c₁ R D₁ M₁) (h₂ : SpaceTriple C R c₂ Q D₂ M₂) : - SpaceTriple C P (c₁ ;; c₂) Q (D₁ + D₂) (max M₁ (D₁ + M₂)) := by + (h₁ : SpaceTriple C tape P c₁ R D₁ M₁) (h₂ : SpaceTriple C tape R c₂ Q D₂ M₂) : + SpaceTriple C tape P (c₁ ;; c₂) Q (D₁ + D₂) (max M₁ (D₁ + M₂)) := by intro s hs obtain ⟨s₁, t₁, d₁, p₁, he₁, hr, hd₁, hp₁⟩ := h₁ s hs obtain ⟨s₂, t₂, d₂, p₂, he₂, hq, hd₂, hp₂⟩ := h₂ s₁ hr @@ -556,21 +575,26 @@ All projections of the corresponding `Triple` rules; the dropped time bound neve constrains anything. -/ protected theorem imm {P Q : State w → Prop} {d : Reg} {v : Word w} - (h : ∀ s, P s → Q (s.setReg d v)) : SpaceTriple C P (.imm d v) Q 0 0 := + (h : ∀ s, P s → Q (s.setReg d v)) : SpaceTriple C tape P (.imm d v) Q 0 0 := (Triple.imm h).space +protected theorem rand {P Q : State w → Prop} {d : Reg} + (h : ∀ s, P s → Q (s.readRandom tape d)) : + SpaceTriple C tape P (.rand d) Q 0 0 := + (Triple.rand h).space + protected theorem mov {P Q : State w → Prop} {d a : Reg} - (h : ∀ s, P s → Q (s.setReg d (s.regs a))) : SpaceTriple C P (.mov d a) Q 0 0 := + (h : ∀ s, P s → Q (s.setReg d (s.regs a))) : SpaceTriple C tape P (.mov d a) Q 0 0 := (Triple.mov h).space protected theorem un {P Q : State w → Prop} {op : UnOp} {d a : Reg} (h : ∀ s, P s → Q (s.setReg d (op.eval (s.regs a)))) : - SpaceTriple C P (.un op d a) Q 0 0 := + SpaceTriple C tape P (.un op d a) Q 0 0 := (Triple.un h).space protected theorem bin {P Q : State w → Prop} {op : BinOp} {d a b : Reg} (h : ∀ s, P s → Q (s.setReg d (op.eval (s.regs a) (s.regs b)))) : - SpaceTriple C P (.bin op d a b) Q 0 0 := + SpaceTriple C tape P (.bin op d a b) Q 0 0 := (Triple.bin h).space /-- Reserve capacity (dynamic), charging at most `N`. With no time bound to draw, @@ -580,7 +604,7 @@ negative, instead of `Triple.memAlloc`'s bound on the requested capacity. -/ protected theorem memAlloc {P Q : State w → Prop} {b : BufId} {n : Reg} {N : ℤ} (h : ∀ s, P s → (((s.regs n).toNat : ℤ) - (s.caps b : ℤ) ≤ N) ∧ Q (s.allocBuf b (s.regs n).toNat)) : - SpaceTriple C P (.memAlloc b n) Q N (max N 0) := by + SpaceTriple C tape P (.memAlloc b n) Q N (max N 0) := by intro s hs obtain ⟨hN, hq⟩ := h s hs exact ⟨_, _, _, _, .memAlloc, hq, hN, by omega⟩ @@ -588,51 +612,51 @@ protected theorem memAlloc {P Q : State w → Prop} {b : BufId} {n : Reg} {N : /-- Reserve capacity (immediate), charging at most the syntactic capacity `n`. -/ protected theorem memAllocI {P Q : State w → Prop} {b : BufId} {n : ℕ} (h : ∀ s, P s → Q (s.allocBuf b n)) : - SpaceTriple C P (.memAllocI b n) Q n n := + SpaceTriple C tape P (.memAllocI b n) Q n n := (Triple.memAllocI h).space protected theorem memFree {P Q : State w → Prop} {b : BufId} - (h : ∀ s, P s → Q (s.allocBuf b 0)) : SpaceTriple C P (.memFree b) Q 0 0 := + (h : ∀ s, P s → Q (s.allocBuf b 0)) : SpaceTriple C tape P (.memFree b) Q 0 0 := (Triple.memFree h).space /-- Free with a known lower bound `K` on the released capacity: credits `-K`. -/ protected theorem memFree' {P Q : State w → Prop} {b : BufId} {K : ℕ} (h : ∀ s, P s → K ≤ s.caps b ∧ Q (s.allocBuf b 0)) : - SpaceTriple C P (.memFree b) Q (-(K : ℤ)) 0 := + SpaceTriple C tape P (.memFree b) Q (-(K : ℤ)) 0 := (Triple.memFree' h).space protected theorem memLen {P Q : State w → Prop} {d : Reg} {b : BufId} (h : ∀ s, P s → Q (s.setReg d (BitVec.ofNat w (s.bufs b).size))) : - SpaceTriple C P (.memLen d b) Q 0 0 := + SpaceTriple C tape P (.memLen d b) Q 0 0 := (Triple.memLen h).space protected theorem memLoad {P Q : State w → Prop} {d : Reg} {b : BufId} {i : Reg} (h : ∀ s, P s → ∃ hlt : (s.regs i).toNat < (s.bufs b).size, Q (s.setReg d (s.bufs b)[(s.regs i).toNat])) : - SpaceTriple C P (.memLoad d b i) Q 0 0 := + SpaceTriple C tape P (.memLoad d b i) Q 0 0 := (Triple.memLoad h).space protected theorem memStore {P Q : State w → Prop} {b : BufId} {i src : Reg} (h : ∀ s, P s → ∃ hlt : (s.regs i).toNat < (s.bufs b).size, Q (s.setBuf b ((s.bufs b).set (s.regs i).toNat (s.regs src) hlt))) : - SpaceTriple C P (.memStore b i src) Q 0 0 := + SpaceTriple C tape P (.memStore b i src) Q 0 0 := (Triple.memStore h).space protected theorem memPush {P Q : State w → Prop} {b : BufId} {src : Reg} (h : ∀ s, P s → (s.bufs b).size < s.caps b ∧ Q (s.setBuf b ((s.bufs b).push (s.regs src)))) : - SpaceTriple C P (.memPush b src) Q 0 0 := + SpaceTriple C tape P (.memPush b src) Q 0 0 := (Triple.memPush h).space protected theorem memPop {P Q : State w → Prop} {b : BufId} (h : ∀ s, P s → Q (s.setBuf b (s.bufs b).pop)) : - SpaceTriple C P (.memPop b) Q 0 0 := + SpaceTriple C tape P (.memPop b) Q 0 0 := (Triple.memPop h).space protected theorem ifNZ {P Q : State w → Prop} {r : Reg} {thn els : Stmt w} {D M : ℤ} - (ht : SpaceTriple C (fun s => P s ∧ s.regs r ≠ 0) thn Q D M) - (he : SpaceTriple C (fun s => P s ∧ s.regs r = 0) els Q D M) : - SpaceTriple C P (.ifNZ r thn els) Q D M := by + (ht : SpaceTriple C tape (fun s => P s ∧ s.regs r ≠ 0) thn Q D M) + (he : SpaceTriple C tape (fun s => P s ∧ s.regs r = 0) els Q D M) : + SpaceTriple C tape P (.ifNZ r thn els) Q D M := by intro s hs by_cases hr : s.regs r = 0 · obtain ⟨s', t, d, p, hexec, hq, hD, hM⟩ := he s ⟨hs, hr⟩ @@ -646,10 +670,10 @@ memory-reusing iteration (`Dg + Db ≤ 0`) gives trip-count-independent bounds. time bound in the conclusion, hence no `Tg`/`Tb` hypotheses. -/ theorem whileNZ_measure {I J : ℕ → State w → Prop} {g body : Stmt w} {r : Reg} {Dg Mg Db Mb : ℤ} - (hg : ∀ k, SpaceTriple C (I k) g (J k) Dg Mg) + (hg : ∀ k, SpaceTriple C tape (I k) g (J k) Dg Mg) (hpos : ∀ k s, J k s → s.regs r ≠ 0 → ∃ k', k = k' + 1) - (hb : ∀ k, SpaceTriple C (fun s => J (k + 1) s ∧ s.regs r ≠ 0) body (I k) Db Mb) : - ∀ k, SpaceTriple C (I k) (.whileNZ g r body) + (hb : ∀ k, SpaceTriple C tape (fun s => J (k + 1) s ∧ s.regs r ≠ 0) body (I k) Db Mb) : + ∀ k, SpaceTriple C tape (I k) (.whileNZ g r body) (fun s => ∃ k', J k' s ∧ s.regs r = 0) (Dg + k * max (Dg + Db) 0) (max Mg (Dg + Mb) + k * max (Dg + Db) 0) := by @@ -687,23 +711,23 @@ theorem whileNZ_measure {I J : ℕ → State w → Prop} {g body : Stmt w} {r : /-! ### Framing -/ theorem frame_post {P Q R : State w → Prop} {c : Stmt w} {D M : ℤ} - (h : SpaceTriple C P c Q D M) - (hR : ∀ s s' t d p, Exec C c s s' t d p → R s → R s') : - SpaceTriple C (fun s => P s ∧ R s) c (fun s => Q s ∧ R s) D M := by + (h : SpaceTriple C tape P c Q D M) + (hR : ∀ s s' t d p, Exec C tape c s s' t d p → R s → R s') : + SpaceTriple C tape (fun s => P s ∧ R s) c (fun s => Q s ∧ R s) D M := by intro s ⟨hp, hr⟩ obtain ⟨s', t, d, p, hexec, hq, hD, hM⟩ := h s hp exact ⟨s', t, d, p, hexec, ⟨hq, hR s s' t d p hexec hr⟩, hD, hM⟩ /-- A register the statement never writes keeps its value. -/ theorem frame_reg {P Q : State w → Prop} {c : Stmt w} {D M : ℤ} {r : Reg} - {v : Word w} (h : SpaceTriple C P c Q D M) (hw : ¬ c.Writes r) : - SpaceTriple C (fun s => P s ∧ s.regs r = v) c (fun s => Q s ∧ s.regs r = v) D M := + {v : Word w} (h : SpaceTriple C tape P c Q D M) (hw : ¬ c.Writes r) : + SpaceTriple C tape (fun s => P s ∧ s.regs r = v) c (fun s => Q s ∧ s.regs r = v) D M := h.frame_post fun _ _ _ _ _ hexec hr => (hexec.frame_reg hw).trans hr /-- A buffer the statement never touches keeps its contents. -/ theorem frame_buf {P Q : State w → Prop} {c : Stmt w} {D M : ℤ} {b : BufId} - {arr : Array (Word w)} (h : SpaceTriple C P c Q D M) (ht : ¬ c.Touches b) : - SpaceTriple C (fun s => P s ∧ s.bufs b = arr) c (fun s => Q s ∧ s.bufs b = arr) + {arr : Array (Word w)} (h : SpaceTriple C tape P c Q D M) (ht : ¬ c.Touches b) : + SpaceTriple C tape (fun s => P s ∧ s.bufs b = arr) c (fun s => Q s ∧ s.bufs b = arr) D M := h.frame_post fun _ _ _ _ _ hexec hb => (hexec.frame_buf ht).trans hb diff --git a/Caliper/W64.lean b/Caliper/W64.lean index 66d7940..dad33d2 100644 --- a/Caliper/W64.lean +++ b/Caliper/W64.lean @@ -1,4 +1,4 @@ -import Caliper.Triple +import Caliper.ProbTriple import Caliper.Builder /-! @@ -29,6 +29,9 @@ namespace Caliper64 /-- 64-bit machine words. -/ abbrev Word := Caliper.Word 64 +/-- Infinite tapes of 64-bit words. -/ +abbrev RandomTape := Caliper.RandomTape 64 + /-- Statements over 64-bit words. -/ abbrev Stmt := Caliper.Stmt 64 @@ -40,7 +43,7 @@ abbrev State.init : State := Caliper.State.init 64 /-! ## Semantics -/ -/-- Cost semantics at word size 64: `Exec C c s s' t d p`. -/ +/-- Cost semantics at word size 64: `Exec C tape c s s' t d p`. -/ abbrev Exec := Caliper.Exec (w := 64) /-- The reference interpreter at word size 64. -/ @@ -57,6 +60,15 @@ abbrev TimeTriple := Caliper.TimeTriple (w := 64) /-- Space-only total-correctness triple. -/ abbrev SpaceTriple := Caliper.SpaceTriple (w := 64) +/-- Uniform measure on infinite tapes of 64-bit words. -/ +noncomputable abbrev uniformTape := Caliper.uniformTape 64 + +/-- Unconditional runtime distribution, including mass at infinity. -/ +noncomputable abbrev runTimePMF := Caliper.runTimePMF (w := 64) + +/-- Almost-sure correctness with expected time and memory bounds. -/ +abbrev ProbTriple := Caliper.ProbTriple (w := 64) + /-! ## Surface syntax -/ /-- The program-builder monad at word size 64. -/ @@ -95,7 +107,7 @@ example : sum34.2 = (.imm 0 3 ;; .imm 1 4 ;; .bin .add 2 0 1) := rfl /-- The sum lands in the result register within 3 unit-cost instructions, touching no buffer memory (the dynamic profile is buffers-only). -/ example : - Triple .unit (fun _ => True) sum34.2 (fun s => s.regs sum34.1 = 7) 3 0 0 := by + Triple .unit Caliper.RandomTape.zero (fun _ => True) sum34.2 (fun s => s.regs sum34.1 = 7) 3 0 0 := by intro s _ refine ⟨_, _, _, _, .seq .imm (.seq .imm .bin), ?_, ?_, ?_, ?_⟩ · simp [show sum34.1 = 2 from rfl, Caliper.State.setReg] @@ -104,7 +116,7 @@ example : · simp /-- The reference interpreter agrees. -/ -example : (run .unit 20 sum34.2 State.init).map (fun r => r.1.regs sum34.1) +example : (run .unit Caliper.RandomTape.zero 20 sum34.2 State.init).map (fun r => r.1.regs sum34.1) = some 7 := rfl end Demo diff --git a/CaliperTest/Export.lean b/CaliperTest/Export.lean index 1477ff8..3db9112 100644 --- a/CaliperTest/Export.lean +++ b/CaliperTest/Export.lean @@ -85,7 +85,7 @@ def codeBase : Nat := 0x1000 def exportCase (tc : TestCase) : IO Unit := do let s₀ := tc.state - let some (s', t, _, _) := run .unit tc.fuel tc.stmt s₀ + let some (s', t, _, _) := run .unit Caliper.RandomTape.zero tc.fuel tc.stmt s₀ | throw <| IO.userError s!"{tc.name}: interpreter failed (out of fuel or unsafe access)" let ctx := tc.ctx let words ← match lowerProgram ctx tc.stmt with diff --git a/CaliperTest/RV64.lean b/CaliperTest/RV64.lean index af76477..8e14f0a 100644 --- a/CaliperTest/RV64.lean +++ b/CaliperTest/RV64.lean @@ -233,6 +233,7 @@ partial def lowerStmt (ctx : Ctx) : Stmt 64 → Except String (Array UInt32) let a ← lowerStmt ctx c₁ let b ← lowerStmt ctx c₂ .ok (a ++ b) + | .rand _ => .error "rand requires a tape-input backend" | .imm d v => do let rd ← regMap d .ok (li rd v.toNat) @@ -338,4 +339,7 @@ def lowerProgram (ctx : Ctx) (c : Stmt 64) : Except String (Array UInt32) := do let w ← lowerStmt ctx c .ok (w.push ebreak) +-- Random instructions require an explicit tape backend. +#guard lowerProgram (layout []) (.rand 0) == .error "rand requires a tape-input backend" + end CaliperTest.RV64 diff --git a/Examples.lean b/Examples.lean new file mode 100644 index 0000000..1c2715b --- /dev/null +++ b/Examples.lean @@ -0,0 +1,4 @@ +import Examples.Replay +import Examples.Distributions +import Examples.Retry +import Examples.Composition diff --git a/Examples/Composition.lean b/Examples/Composition.lean new file mode 100644 index 0000000..a5bd804 --- /dev/null +++ b/Examples/Composition.lean @@ -0,0 +1,63 @@ +import Caliper.Retry + +/-! +# Composing randomized subroutines + +A retrying caller consumes an unbounded number of words. A callee then samples +from the returned cursor. Its sample remains uniform, and expected costs add. +-/ + +open Caliper MeasureTheory +open scoped ENNReal + +namespace CaliperExamples.Composition + +/-- The callee is specified at every initial cursor and every caller output. -/ +theorem retry_then_sample : + ProbTriple .unit (fun _ : State 1 => True) (retryZero 0 ;; .rand 1) + (fun s => s.regs 0 = 0) 5 0 0 := by + have hsample : ProbTriple .unit (fun s : State 1 => s.regs 0 = 0) (.rand 1) + (fun s => s.regs 0 = 0) CostModel.unit.rand 0 0 := by + apply ProbTriple.rand + intro s hs v + simpa [State.setReg] using hs + have h := (retryZero_spec (w := 1) .unit 0).seq hsample + norm_num [CostModel.unit] at h + exact h + +/-- The next sample is uniform after a random-length retry, without conditioning +on termination. The caller's almost-sure termination is proved separately. -/ +example (s : State 1) (v : Word 1) : + resultProb .unit (retryZero 0 ;; .rand 1) s (fun s' _ _ _ => s'.regs 1 = v) = + (2 : ℝ≥0∞)⁻¹ := by + rw [resultProb_seq_rand] + have hsuccess : resultProb .unit (retryZero 0) s (fun _ _ _ _ => True) = 1 := by + apply (mem_ae_iff_prob_eq_one (measurableSet_exec _ _ _ _)).mp + filter_upwards [(retryZero_spec .unit 0 s trivial).1] with tape ht + obtain ⟨s', t, d, p, he, _, _, _⟩ := ht + exact ⟨s', t, d, p, he, trivial⟩ + rw [hsuccess] + norm_num + +/-- Existing fixed-tape specifications remain usable for deterministic callees. -/ +example {c : Stmt 1} {Q : State 1 → Prop} {T : ℕ} {D M : ℤ} + (h : Triple .unit RandomTape.zero (fun s => s.regs 0 = 0) c Q T D M) + (hc : c.RandomFree) : + ProbTriple .unit (fun _ : State 1 => True) (retryZero 0 ;; c) Q + (4 + T) D (max 0 M) := by + have hseq := (retryZero_spec (w := 1) .unit 0).seq (ProbTriple.of_randomFree h hc) + norm_num [CostModel.unit] at hseq + exact hseq + +/-- Elapsed time is external accounting: even radically different prices preserve +all state changes and memory usage for the same tape. -/ +example {C C' : CostModel} {tape : RandomTape 64} {c : Stmt 64} + {s s' : State 64} {t : ℕ} {d p : ℤ} (h : Exec C tape c s s' t d p) : + ∃ t', Exec C' tape c s s' t' d p := h.withCostModel C' + +/-- This tape fails twice, succeeds, and supplies a fresh word to the callee. -/ +example : (run .unit (fun i => if i = 2 then (0 : Word 1) else 1) + 20 (retryZero 0 ;; .rand 1) (State.init 1)).map + (fun (s, t, _, _) => (s.regs 0, s.regs 1, s.tapePos, t)) = some (0, 1, 4, 7) := rfl + +end CaliperExamples.Composition diff --git a/Examples/Distributions.lean b/Examples/Distributions.lean new file mode 100644 index 0000000..774324d --- /dev/null +++ b/Examples/Distributions.lean @@ -0,0 +1,90 @@ +import Caliper.ProbTriple + +/-! Probability laws for actual Caliper programs, checked during the CI build. -/ +open Caliper MeasureTheory +open scoped ENNReal + +namespace CaliperExamples.Distributions + +variable {w : ℕ} + +/-- A sample is uniform at every starting cursor. -/ +example (s : State w) (r : Reg) (v : Word w) : + resultProb .unit (.rand r) s (fun s' _ _ _ => s'.regs r = v) = + ((2 ^ w : ℕ) : ℝ≥0∞)⁻¹ := by + rw [resultProb_of_exec _ _ _ _ (fun tape => s.readRandom tape r) + (fun _ => 1) (fun _ => 0) (fun _ => 0) (fun _ => Exec.rand)] + simpa only [regs_readRandom, regs_setReg_self] using uniformTape_eval s.tapePos v + +/-- Two independent output words: every ordered pair has mass `2^(-2w)`. -/ +example (x y : Word w) : + resultProb .unit (.rand 0 ;; .rand 1) (State.init w) + (fun s' _ _ _ => s'.regs 0 = x ∧ s'.regs 1 = y) = + (((2 ^ w : ℕ) : ℝ≥0∞)⁻¹) ^ 2 := by + rw [resultProb_of_exec _ _ _ _ + (fun tape => ((State.init w).readRandom tape 0).readRandom tape 1) + (fun _ => 2) (fun _ => 0) (fun _ => 0) (fun _ => Exec.seq Exec.rand Exec.rand)] + have he : {tape : RandomTape w | + (((State.init w).readRandom tape 0).readRandom tape 1).regs 0 = x ∧ + (((State.init w).readRandom tape 0).readRandom tape 1).regs 1 = y} = + RandomTape.cylinder ![x, y] := by + ext tape + simp [RandomTape.cylinder, Fin.forall_fin_two, State.readRandom, State.setReg, State.init] + rw [he, uniformTape_cylinder] + +/-- Random output need not imply random runtime. -/ +example (s : State w) : runTimePMF .unit (.rand 0) s = PMF.pure 1 := + runTimePMF_eq_pure _ _ _ _ (fun _ => runTime_of_exec Exec.rand) + +example (s : State w) : + (runTimePMF .unit (.rand 0) s).expect ENat.toENNReal = 1 := by + rw [runTimePMF_eq_pure _ _ _ _ (fun _ => runTime_of_exec Exec.rand)] + simp only [PMF.expect_pure, ENat.toENNReal_coe] + norm_num [CostModel.unit] + +/-- An invalid load is charged to infinity, even though it fails immediately. -/ +example : runTimePMF .unit (.memLoad 0 0 0) (State.init 64) = PMF.pure ⊤ := by + apply runTimePMF_eq_pure + intro tape + apply (runTime_eq_top_iff tape).mpr + rintro ⟨s', t, d, p, he⟩ + cases he with + | memLoad h => simp [State.init] at h + +/-- A deterministic program has a point-mass runtime under the uniform tape law. -/ +example : runTimePMF .unit (.imm 0 (7 : Word 64)) (State.init 64) = PMF.pure 1 := + runTimePMF_of_randomFree _ _ _ (tape := RandomTape.zero) Exec.imm trivial + +/-- A sampled one triggers an invalid load; a sampled zero returns safely. -/ +def maybeFault : Stmt 1 := .rand 0 ;; .ifNZ 0 (.memLoad 1 0 0) .skip + +example : runTimePMF .unit maybeFault (State.init 1) ⊤ = (2 : ℝ≥0∞)⁻¹ := by + rw [runTimePMF_apply] + have he : {tape | runTime .unit maybeFault (State.init 1) tape = ⊤} = + {tape : RandomTape 1 | tape 0 = 0}ᶜ := by + ext tape + rw [Set.mem_setOf_eq, runTime_eq_top_iff] + change (¬ ∃ s' t d p, Exec .unit tape maybeFault (State.init 1) s' t d p) ↔ tape 0 ≠ 0 + constructor + · intro hn hz + apply hn + refine ⟨_, 2, 0, 0, Exec.seq Exec.rand (Exec.ifNZ_false ?_ Exec.skip)⟩ + simpa [State.readRandom, State.setReg, State.init] using hz + · intro hn + rintro ⟨s', t, d, p, hexec⟩ + cases hexec with + | seq hr hb => + cases hr + cases hb with + | ifNZ_false hz _ => + exact hn (by simpa [State.readRandom, State.setReg, State.init] using hz) + | ifNZ_true _ hf => + cases hf with + | memLoad hi => simp [State.readRandom, State.setReg, State.init] at hi + rw [he, measure_compl (by + simpa only [Set.preimage, Set.mem_singleton_iff] using + ((measurable_pi_apply 0 : Measurable (fun tape : RandomTape 1 => tape 0)) + (measurableSet_singleton (0 : Word 1)))) (measure_ne_top _ _), uniformTape_eval] + norm_num + +end CaliperExamples.Distributions diff --git a/Examples/Replay.lean b/Examples/Replay.lean new file mode 100644 index 0000000..c4b0e3c --- /dev/null +++ b/Examples/Replay.lean @@ -0,0 +1,58 @@ +import Caliper.Tape +import Caliper.Builder +import Caliper.Render +import Caliper.Liveness + +/-! +# Replaying computations against fixed word tapes + +These examples are compiled by `lake build Examples`, including in CI. The tape +is supplied by the caller; the same tape and initial state always give the same run. +-/ + +namespace CaliperExamples.Replay + +open Caliper + +def tape : RandomTape 64 := fun i => BitVec.ofNat 64 (i + 7) + +def pair : Stmt 64 := .rand 0 ;; .rand 1 + +example : (run .unit tape 10 pair (State.init 64)).map + (fun (s, t, d, p) => (s.regs 0, s.regs 1, s.tapePos, t, d, p)) = + some (7, 8, 2, 2, 0, 0) := rfl + +/-- A resumed execution continues from the returned cursor. -/ +example : (do + let (s, _, _, _) ← run .unit tape 10 pair (State.init 64) + let (s', t, d, p) ← run .unit tape 10 (.rand 2) s + pure (s'.regs 2, s'.tapePos, t, d, p)) = some (9, 3, 1, 0, 0) := rfl + +example : (run .unit tape 10 (.rand 0) { State.init 64 with tapePos := 5 }).map + (fun (s, _, _, _) => (s.regs 0, s.tapePos)) = some (12, 6) := rfl + +example : (run .unit RandomTape.zero 10 pair (State.init 64)).map + (fun (s, t, _, _) => (s.regs 0, s.regs 1, s.tapePos, t)) = some (0, 0, 2, 2) := rfl + +/-- Only the branch actually taken consumes words. -/ +def branch : Stmt 4 := + .rand 0 ;; .ifNZ 0 (.rand 1 ;; .rand 2) .skip ;; .rand 3 + +example : (run .unit (fun i => BitVec.ofNat 4 i) 20 branch (State.init 4)).map + (fun (s, t, _, _) => (s.regs 3, s.tapePos, t)) = some (1, 2, 3) := rfl + +example : (run .unit (fun i => BitVec.ofNat 4 (i + 1)) 20 branch (State.init 4)).map + (fun (s, t, _, _) => (s.regs 3, s.tapePos, t)) = some (4, 4, 5) := rfl + +/-- Even the zero-bit word consumes one tape position. -/ +example : (run .unit RandomTape.zero 2 (.rand 0) (State.init 0)).map + (fun (s, t, _, _) => (s.regs 0, s.tapePos, t)) = some (0, 1, 1) := rfl + +example : Build.build (Build.rand (w := 64)) = (0, .rand 0) := rfl +example : (Stmt.rand (w := 64) 0).renderString = "rand r0" := rfl +example : pair.staticTime? .unit = some 2 := rfl +example : pair.readsSet = ∅ := by decide +example : pair.writesSet = {0, 1} := by decide +example : (Stmt.rand (w := 64) 0).RandomFree = False := rfl + +end CaliperExamples.Replay diff --git a/Examples/Retry.lean b/Examples/Retry.lean new file mode 100644 index 0000000..c26f871 --- /dev/null +++ b/Examples/Retry.lean @@ -0,0 +1,44 @@ +import Caliper.Retry + +/-! +# A randomized loop with no fixed runtime bound + +With one-bit words, retrying until zero takes two attempts on average. Each +attempt costs one sample and one branch, giving expected unit cost four. +-/ +open Caliper +open scoped ENNReal + +namespace CaliperExamples.Retry + +example (n : ℕ) : + runTimePMF .unit (retryZero 0) (State.init 1) ((2 * (n + 1) : ℕ) : ℕ∞) = + (2⁻¹ : ℝ≥0∞) ^ (n + 1) := by + have h := retryZero_timePMF .unit 0 (State.init 1) (by decide) n + norm_num [CostModel.unit, pow_succ, Nat.mul_comm] at h ⊢ + exact h + +example : runTimePMF .unit (retryZero 0) (State.init 1) ⊤ = 0 := + retryZero_almostSure _ _ _ + +example : (runTimePMF .unit (retryZero 0) (State.init 1)).expect ENat.toENNReal = 4 := by + rw [retryZero_expect _ _ _ (by decide)] + norm_num [CostModel.unit] + +/-- The degenerate zero-bit word always succeeds on the first attempt. -/ +example : (runTimePMF .unit (retryZero 0) (State.init 0)).expect ENat.toENNReal = 2 := by + rw [retryZero_expect _ _ _ (by decide)] + norm_num [CostModel.unit] + +example : runTime .unit (retryZero 0) (State.init 1) (fun _ => 1) = ⊤ := + retryZero_no_zero (fun _ => by decide) + +/-- Replay three failures and a success: four attempts, eight cost units. -/ +example : (run .unit (fun i => if i < 3 then (1 : Word 1) else 0) + 20 (retryZero 0) (State.init 1)).map + (fun (s, t, d, p) => (s.regs 0, s.tapePos, t, d, p)) = some (0, 4, 8, 0, 0) := rfl + +example : (run .unit RandomTape.zero 3 (retryZero 0) (State.init 64)).map + (fun (s, t, _, _) => (s.regs 0, s.tapePos, t)) = some (0, 1, 2) := rfl + +end CaliperExamples.Retry diff --git a/README.md b/README.md index 6ab272e..dc40474 100644 --- a/README.md +++ b/README.md @@ -19,12 +19,35 @@ The only datatype in Caliper is words of a fixed size, usually 64 bits. We hope for Caliper to become the "yardstick" by which we can compare "real world" complexity in Lean. +## Randomized computation + +`Stmt.rand r` reads the next word from an explicit `RandomTape w := ℕ → Word w`. +`run C tape fuel program state` is deterministic for every supplied tape. Use +`RandomTape.zero` for an all-zero tape, or supply a tape to replay a run. The returned +state carries the next unread position, so sequential programs share the tape. + +`uniformTape w` is the probability measure of independent uniform words. +`runTimePMF C program state : PMF ℕ∞` assigns finite costs to safe termination +and infinity to divergence or faults. Expected time is the generic expression +`(runTimePMF C program state).expect ENat.toENNReal`; probabilities are +unconditional. `ProbTriple.seq` adds expected costs and composes memory bounds, +including for subroutines that consume a variable number of words. + +Programs cannot read elapsed time or the tape cursor. Costs are semantic outputs; +changing the cost model cannot affect program behavior (`Exec.withCostModel`). +Randomness is an immutable input tape with explicit state threading, rather than a +probabilistic execution monad. The existing `Build` monad constructs programs. + +See [`Examples/`](Examples/) for replay, distribution, retry, and composition +examples. Their executable checks and Lean proofs are built in CI. + ## Correspondence to RISC-V A Caliper program can easily be translated into RISC-V assembly. The only requirements are: - Register allocation and liveness analysis: Caliper has an infinite number of registers (each of which "cost" 1 memory), while the real CPU has a finite number of registers. +- Supplying random words: the abstract `rand` price models a tape read. The current RV64 test backend rejects `rand`; it needs a tape-input implementation before lowering randomized programs. - Implementing a heap: Caliper can allocate/free arrays of words of fixed/variable size, hence a heap must be implemented. Overall the goal of Caliper is that if a Caliper program can be proven to have computational cost $n$, diff --git a/doc/caliper.md b/doc/caliper.md index 6536d13..1f956f8 100644 --- a/doc/caliper.md +++ b/doc/caliper.md @@ -11,6 +11,11 @@ upper bounds on running time and on allocated memory. |---|---| | `Core.lean` | Syntax (`Stmt`), cost models (`CostModel`, `CostModel.Admissible`), big-step cost semantics (`Exec`), determinism, framing (`Writes`/`Touches`), the unit-time theorems, the partial static clock (`staticTime?`), peak memory ≤ running time (`Exec.peak_le_time`), well-formed states and absolute live memory (`State.WellFormed`, `State.liveMem`), reference interpreter (`run`) and its soundness | | `Render.lean` | Pretty-printer: `Stmt.render`/`Stmt.renderString` emit the `mem.`-qualified assembly dialect used for the listings in this document | +| `Tape.lean` | Fixed-tape locality, replay completeness, random-free programs, and independence of program behavior from the cost model | +| `PMF.lean`, `Probability.lean` | Generic PMF expectation, uniform word tapes, unconditional result probabilities, and runtime distributions | +| `TapeMeasure.lean`, `Outcome.lean` | Independent unread tails after variable-length subroutines and countable terminating outcomes | +| `ProbTriple.lean` | Almost-sure resource specifications, expected-time sequencing, deterministic callee reuse, branching, and countable terminating cases | +| `Geometric.lean`, `Retry.lean` | Unbounded retry, geometric runtime atoms, almost-sure termination, and exact expected time | | `Triple.lean` | Upper-bound Hoare triples (`Triple`), one rule per instruction, `seq`/`conseq`/`ifNZ`, the measure-indexed loop rule `whileNZ_measure`, frame rules; time-only and space-only judgments (`TimeTriple`/`SpaceTriple`) with the same rule set, recombinable via determinism (`TimeTriple.and_space`) | | `Builder.lean` | Surface syntax: builder monad with fresh register/buffer naming, expression compiler (`Exp`), structured `if_`/`while_`, typed buffer handles (`Buf`), product types (`PairR`, `PairBuf`) | | `Examples.lean` | Worked examples with full proofs, builder ↔ core checks, interpreter demos | @@ -44,7 +49,7 @@ the builder allocates names automatically. ### What "unit time" means Costs come from a `CostModel`: a table indexed by the *instruction*, never by the -state. `Exec C c s s' t d p` charges each instruction its table entry, so: +state. `Exec C tape c s s' t d p` charges each instruction its table entry, so: - `Exec.straight_time_eq`: a branch-free program's running time is a syntactic constant. The proved statement is data-independence of the *abstract time @@ -102,7 +107,7 @@ Consequences for the instruction set: ### Upper bounds, not exact times; memory as a (net, peak) profile -`Triple C P c Q T D M` is total correctness plus `t ≤ T` (time), `d ≤ D` (net +`Triple C tape P c Q T D M` is total correctness plus `t ≤ T` (time), `d ≤ D` (net live-memory change, signed) and `p ≤ M` (peak live-memory growth). Exhibiting the underlying `Exec` derivation also proves memory safety: out-of-range accesses have no derivation, since the `memLoad`/`memStore` rules demand an in-range proof. @@ -211,7 +216,7 @@ Time and memory bounds are also independently provable: `TimeTriple` bounds only the running time and `SpaceTriple` only the (net, peak) pair, each with the full rule set, so a time proof carries no memory algebra and vice versa. The `Drain` example has a trip-count-independent space bound even though no uniform time bound -exists for it. Since the machine is deterministic, separately proved judgments +exists for it. For a fixed tape the machine is deterministic, so separately proved judgments recombine into a full `Triple` (`TimeTriple.and_space`). #### The static register metric, in brief @@ -230,7 +235,7 @@ programs. ### Executable -`run C fuel c s` is a fuel-based reference interpreter; `run_sound` proves anything +`run C tape fuel c s` is a fuel-based reference interpreter; `run_sound` proves anything it returns is a genuine `Exec` derivation with the same costs, so `#eval` numbers are instances of the proved bounds (the examples check this with `#guard_msgs`). @@ -419,3 +424,57 @@ their own concrete numerals. `#print axioms ` is the audit tool. - Registers in the examples use fixed conventions (callee-clobbered scratch); a register-window or parameterized-register discipline is mechanical to add (distinctness side conditions close by `decide`). + + +## Random word tapes and composition + +`RandomTape w` is `ℕ → Word w`. `Stmt.rand d` copies the word at `State.tapePos` +into register `d`, advances that cursor once, and charges `C.rand`. No other +instruction consumes input. The tape and cursor are external input bookkeeping; +they do not contribute to register liveness or allocated-buffer memory. Neither +has a program instruction for inspection, seeking, or rewinding. Elapsed cost is +also unavailable to programs: `Exec.withCostModel` proves that changing prices +preserves safe termination, the final state, and both memory costs. + +All fixed-tape semantics and triples take `tape` explicitly. `RandomTape.zero` +selects deterministic all-zero inputs without disabling the `rand` instruction. +`Stmt.RandomFree` certifies that a program consumes no words; its executions and +runtime law are independent of the supplied tape. Replay uses the returned +state, including its cursor. Fuel is an interpreter limit, not an observable clock; +`run_mono` and `run_complete` relate it to unbounded executions. + +`uniformTape w` is the infinite product of uniform word distributions. It is a +measure, since infinite tapes are not a countable discrete sample space. The +runtime *image* is countable and is exposed as `runTimePMF : PMF ℕ∞`. +Faults and divergence both contribute to infinity, even if a fault happens after a +finite instruction count. `resultProb` counts safe terminating outcomes without +conditioning on success. Generic `PMF.expect`, `PMF.expect_map`, and `PMF.expect_bind` +provide expectation and its composition laws. + +`Exec.withTape` proves finite-prefix locality. `uniformTape_after_exec` then proves +that the unread tail after a safely terminating subroutine is uniform and independent +of any predicate on its outcome, including its runtime and consumed-word count. +For a subroutine terminating with probability `p`, an unread-tail event of mass `q` +has joint mass `p*q`; no termination assumption is hidden in a conditional probability. +This is essential when a callee follows a caller that consumes a variable-length +prefix. Replaying each component from cursor zero would reuse randomness and does +not implement sequential composition. + +`ProbTriple C P c Q T D M` gives almost-sure safe correctness and memory bounds, +plus expected time at most `T`. Its sequence rule gives `T₁ + T₂`, `D₁ + D₂`, and +`max M₁ (D₁ + M₂)`. Specifications quantify over initial states, allowing a callee to +start at any cursor. Its input registers may carry random values returned by the +caller: the callee's specification must hold for each state satisfying the intermediate +postcondition. `ProbTriple.of_randomFree` lifts an existing fixed-tape deterministic +subroutine specification into this logic. `of_countable_cases` handles unbounded computations by proving +countably many terminating cases whose unconditional masses sum to one. + +`retryZero r` repeatedly samples until it sees zero. Its runtime distribution is +geometric with success probability `2^(-w)`, zero mass at infinity, and exact +expected cost `2^w * (C.rand + C.branch)` when per-attempt cost is positive. The +proof also covers `w = 0`; a fixed tape without any zero can still diverge. + +The top-level `Examples` Lake library is a default build target and an explicit CI +target. It checks fixed-tape replay and proves probability and resource statements. +The RV64 differential suite continues to cover the supported deterministic lowering; +randomized instructions report an explicit unsupported-backend error. diff --git a/lakefile.lean b/lakefile.lean index d824a4a..fe09d5b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -10,6 +10,10 @@ package caliper where @[default_target] lean_lib Caliper where +/-- Executable examples and their proofs; built in CI. -/ +@[default_target] +lean_lib Examples where + /-- Test-only: RV64 lowering + differential-vector exporter. Not imported by `Caliper`; users running `lake build Caliper` never build it. -/ lean_lib CaliperTest where