Add support for randomized computation

.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,29 +25,31 @@ 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: |
           curl -sSfL https://elan.lean-lang.org/elan-init.sh | sh -s -- -y --default-toolchain none
           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

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

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

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)

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

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]