Counted pulls in formal/: LT with byte μ and soundness by finishing order, on the Clean fork

.github/workflows/formal.yml

@@ -48,6 +48,40 @@ jobs:
       - name: Build
         run: lake build
 
+      # `LambdaVM/Axioms.lean` is a list of `#print axioms` lines, one per modelled circuit and
+      # per ensemble theorem. It is not part of the library, so `lake build` does not see it.
+      - name: No sorry, no axioms beyond the standard three
+        run: |
+          set -euo pipefail
+          report="${RUNNER_TEMP:-/tmp}/axioms.txt"
+          lake env lean LambdaVM/Axioms.lean | tee "$report"
+
+          # One report per `#print axioms` line: a renamed or deleted declaration fails here
+          # instead of quietly dropping out of the check.
+          expected=$(grep -c '^#print axioms ' LambdaVM/Axioms.lean || true)
+          got=$(grep -c 'depends on axioms\|does not depend on any axioms' "$report" || true)
+          if [ "$expected" -ne "$got" ]; then
+            echo "::error::expected $expected axiom reports, got $got"
+            exit 1
+          fi
+
+          if grep -q 'sorryAx' "$report"; then
+            echo "::error::a modelled circuit or ensemble theorem depends on sorry"
+            exit 1
+          fi
+
+          unexpected=$(
+            sed -n 's/.*depends on axioms: \[\(.*\)\]/\1/p' "$report" \
+              | tr ',' '\n' | sed 's/[[:space:]]//g; /^$/d' | sort -u \
+              | grep -vxF -e propext -e Classical.choice -e Quot.sound || true
+          )
+          if [ -n "$unexpected" ]; then
+            echo "::error::axioms outside propext, Classical.choice, Quot.sound: $(echo $unexpected)"
+            exit 1
+          fi
+
+          echo "$expected declarations checked, no sorry, no extra axioms"
+
       - name: Export is up to date
         run: |
           lake env lean --run LambdaVM/Export.lean

formal/LambdaVM.lean

@@ -13,3 +13,6 @@ public import LambdaVM.Tables.Eq
 public import LambdaVM.Tables.Shift
 public import LambdaVM.Ensembles.EqLookup
 public import LambdaVM.Channels.Counted
+public import LambdaVM.Tables.MinToy
+public import LambdaVM.Ensembles.LtStaged
+public import LambdaVM.Ensembles.CountedSameBus

formal/LambdaVM/Axioms.lean

@@ -0,0 +1,30 @@
+module
+
+public import LambdaVM
+
+/-!
+# Axiom check
+
+Every modelled circuit and every ensemble theorem must rest on nothing beyond Lean's three
+standard axioms: `propext`, `Classical.choice`, `Quot.sound`. In particular none of them may
+depend on `sorryAx`.
+
+`.github/workflows/formal.yml` runs this file with `lake env lean` and fails if any report
+names `sorryAx` or an axiom outside those three. It also counts the `#print axioms` lines
+here and requires one report for each, so a declaration that stops existing fails the build
+rather than silently dropping out of the check. Add a line for every new circuit, ensemble
+soundness theorem or global row theorem.
+-/
+
+-- The modelled chips. Each `circuit` bundles its own soundness and completeness proofs.
+#print axioms LambdaVM.LT.circuit
+#print axioms LambdaVM.EQ.circuit
+#print axioms LambdaVM.SHIFT.circuit
+#print axioms LambdaVM.MinToy.circuit
+#print axioms LambdaVM.CountedMin.circuit
+
+-- The ensembles.
+#print axioms LambdaVM.Ensembles.eq_rows_correct
+#print axioms LambdaVM.Ensembles.LtStaged.tableSoundness
+#print axioms LambdaVM.Ensembles.LtStaged.tableSoundness_withMin
+#print axioms LambdaVM.CountedMin.tableSoundness

formal/LambdaVM/Buses/Alu.lean

@@ -65,6 +65,10 @@ def shiftResult (word signed direction x s : ℕ) : ℕ :=
   else if signed = 0 then x >>> k
   else sra64 x k
 
+/-- `opsel` of MIN: a toy operation for the counted-pulls PoC, not an RV64IM op. It has the shape of
+DIVREM: its chip pulls LT on this bus and pushes its own result on the same bus. -/
+def opselMIN : ℕ := 7
+
 /-- What a puller learns. The caller must have range-checked both words of both operands
 (the chips' `IS_WORD` assumptions). One clause per `opsel`, selected by the flag byte read
 as a natural. -/
@@ -83,7 +87,11 @@ def Guarantees (m : Msg (F p)) : Prop :=
     (∀ w s d : ℕ, w < 2 → s < 2 → d < 2 →
       m.flags.val = opselSHIFT + w + 32 * s + 64 * d →
       m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
-      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256))
+      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256)) ∧
+    -- MIN (toy, see `opselMIN`): flags = opsel(MIN), out = the unsigned minimum
+    (m.flags.val = opselMIN →
+      m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
+      dword m.outLo m.outHi = min (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi))
 
 def channel : Channel (F p) Msg where
   name := "ALU"

formal/LambdaVM/Channels/Counted.lean

@@ -19,7 +19,9 @@ The price is in the balance premise. `exists_push_of_pull` needs `N · length <
 `BalancedInteractions` only matches pulls of multiplicity `1`, and counts a pull of any other
 nonzero multiplicity as a push; `not_consistent` shows the gap is real: for `N ≥ 2` the counted
 channel is not `Consistent`, so it cannot be finished in a `SoundEnsemble` until that premise
-carries the bound. With `N = 1` everything coincides (`counted 1 channel` is `Normal`).
+carries the bound. With `N = 1` everything coincides (`counted 1 channel` is `Normal`). With the
+bounded balance `BalancedUpTo N` of the modified Clean (`counted-pulls`), `consistentUpTo` closes
+the gap.
 -/
 
 namespace LambdaVM.Counted
@@ -275,6 +277,33 @@ theorem not_consistent (N : ℕ) (hN : 2 ≤ N) (hN' : N ≤ 255)
   convert h
   simp [ProvableType.fromElements_toElements]
 
+/-- With the bounded balance of the modified Clean (`BalancedUpTo N`, the premise `not_consistent`
+asks for), the counted channel is consistent: a pull of `1, …, N` is matched by an interaction
+that is not such a pull, and that interaction's requirement is the guarantee. -/
+instance consistentUpTo (N : ℕ) (channel : Channel (F p) Message) :
+    (counted N channel).ConsistentUpTo N where
+  consistent interactions data balanced reqs a a_mem := by
+    obtain ⟨ a_channel, - ⟩ := reqs a a_mem
+    by_cases a_pull : a.PullUpTo N
+    case neg =>
+      rcases a with ⟨ _, a_direction, a_mult, a_msg, a_size ⟩
+      subst a_channel
+      simp only [Interaction.Guarantees, counted]
+      exact fun h_direction h_count => absurd ⟨ h_direction, h_count ⟩ a_pull
+    obtain ⟨ b, b_mem, b_msg, b_ne_zero, b_not_pull ⟩ := balanced.matchedUpTo a a_mem a_pull
+    obtain ⟨ b_channel, b_reqs ⟩ := reqs b b_mem
+    rcases a with ⟨ _, a_direction, a_mult, a_msg, a_size ⟩
+    rcases b with ⟨ _, b_direction, b_mult, b_msg', b_size ⟩
+    subst a_channel b_channel
+    simp only at b_msg
+    subst b_msg
+    simp only [Interaction.Guarantees, Interaction.Requirements, Interaction.msgVector,
+      counted] at b_reqs ⊢
+    intro _ _
+    cases b_direction with
+    | push => exact b_reqs b_ne_zero
+    | pull => exact b_reqs b_ne_zero (b_not_pull rfl)
+
 end LambdaVM.Counted
 
 /-! ## A deduplicated row