[jotabulacios]

Motivation

formal/ pins Clean at 1a6c2842. Since then Clean removed StaticLookupChannel in favour of
Air.Flat.Lookup (#446), tagged every interaction as a push or a pull with a nonnegative
multiplicity, where a pull must have multiplicity 0 or 1 (#493), made the interaction-count bound of
a balance check explicit (Balance.fits, an InteractionsFit premise of TableSoundness) and moved
to Lean v4.35.0. Moving to current Clean main breaks every table, so this PR updates Clean and adapts
the model, with no change in what is proven.

Description

• Bump Clean to f3abad7c (current main) and Lean to v4.35.0.
• Move StaticLookupChannel into formal/ (LambdaVM/StaticLookup.lean); BITWISE reads its
  tables through toChannel.
• EQ, LT, SHIFT: each pull's multiplicity requirement (0 or 1) follows from the existing bit
  constraints; guarantees are now stated for multiplicity 1 instead of -1.
• EqLookup: rewritten for the current SoundEnsemble API (balance parameter, channels added
  before tables, unique table names, a demand generation mode per component); eq_rows_correct
  takes the InteractionsFit premise.
• Channels/Counted.lean: ported to directions. not_consistent now needs only two interactions,
  since BalancedInteractions counts a pull of multiplicity N ≥ 2 as a push.
• Lean 4.35: rename the deprecated if_*/dif_* lemmas and replace a grind call that no longer
  closes its goal.
• Regenerate export/*.json (interactions now carry direction and a nonnegative multiplicity)
  and sign Lean multiplicities by direction in lean_diff.rs.

How to Test

1. cd formal && lake build
2. lake env lean --run LambdaVM/Export.lean && git diff --exit-code -- export
3. cargo test -p lambda-vm-prover --lib lean_diff

Note

The Lean toolchain moves from v4.33.1 to v4.35.0 (it comes with Clean), so local environments and anything that depends on formal/ need lake update. The first CI run downloads a new Mathlib cache and takes longer.

[jotabulacios]

/ai-review

[github-actions]

AI Review

PR #1030 · 18 changed files

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[claude]

Review: Clean bump to f3abad7c + Lean v4.35.0

I found no correctness or safety problems. This PR only touches proofs and a test harness, so it has no runtime or GPU impact.

Checked

• lean_diff.rs: the new sign is pull → −m, push → +m. That matches the old exported multiplicities (the -1·μ constant, 18446744069414584320, that was removed from export/*.json) and the Rust convention (sender −m, receiver +m), so the comparison means the same as before. panic! on an unknown direction is the right call in a test.
• Counted.lean: the port to directions looks right. A push with mult ≠ 0 owes the guarantee. A pull owes it only when its multiplicity is not a count. The new two-interaction witness in not_consistent is a stronger result and much simpler than the old p / N construction.
• EQ / LT / SHIFT: the old multiplicity requirements were discharged vacuously. They are now discharged directly from μ ∈ {0,1} (mul_one_sub_eq_zero_iff), which matches Clean's new rule that a pull's multiplicity must be 0 or 1.
• No sorry, admit, axiom or native_decide was added.

Low / cleanup

1. Possible dead code: every call to requirement_vacuous (Eq.lean, Lt.lean) and req_vacuous (Shift.lean) is removed. If either lemma is defined in formal/ and not in Clean, it is now unused and should be deleted. I couldn't check this from here, because the base branch formal/clean-model isn't available locally.
2. Shift.lean completeness (BYTE_ALU[AND, shift, 15] when left): have := h; linear_combination -this was left over from removing neg_inj.mp. It can be just linear_combination -h. Likewise, have hs1 : input_signed = 1 := h and have hd1 : input_direction = 1 := h only rename h. Using h directly, or intro hs1, is simpler.
3. EqLookup.lean adds about 15 @[circuit_norm] rfl lemmas (*_name, *_channelsWith*, eqComponent_circuit, etc.) just to close the side goals of addTable. That's fine for one ensemble. If more ensembles follow, a single simp [circuit_norm, pushStaticComponent, eqComponent, ...] unfold, or a small helper, would avoid repeating this per component.

Note for CI and users: the toolchain moves to v4.35.0, so local formal/ checkouts need lake update, as the PR description says.

🤖 Generated with Claude Code

[jotabulacios]

/ai-review

[claude]

Low (readability): You rewrote this doc comment, but it still opens with "a sender adds +m, a receiver −m". Two lines below, the code does the opposite: if i.is_sender { -m } else { m }. Only the closing clause hints that the convention is flipped. Consider stating the convention the comparison actually uses, for example:

Suggested change

	/// `(bus id, signed multiplicity, bus elements)` of a Rust interaction on a row. A sender
	/// adds `+m`, a receiver `−m`; Clean's pull is `−e` and push `+e`, so the signs agree once a
	/// receiver (the table that answers the lookup, Clean's push) keeps its multiplicity.
	/// adds `+m`, a receiver `−m`; Clean's pull of multiplicity `e` counts `−e` and its push `+e`,
	/// so the signs agree once a receiver (the table that answers the lookup, Clean's push) keeps
	/// its multiplicity.
	/// `(bus id, signed multiplicity, bus elements)` of a Rust interaction on a row, signed the way
	/// Clean signs it: a sender (Clean's pull) counts `−m`, a receiver (the table that answers the
	/// lookup, Clean's push) counts `+m`. `lean_interaction_at` signs Lean's pulls the same way.

[claude]

Review

No Critical/High/Medium issues found. This is a mechanical port to the new Clean API: it doesn't weaken any proof and doesn't change prover or executor code.

What I checked:

• Sign convention in lean_diff.rs: Lean exports now carry direction and a nonnegative multiplicity. lean_interaction_at negates pulls, which matches rust_interaction_at (it negates senders). The diff still compares the same signed values as before. If the direction field is missing or has an unknown value, the test panics, which is the right behaviour for a test.
• Pull multiplicities in EQ / LT / SHIFT: each pull must now have multiplicity 0 or 1. The PR proves this from the existing μ·(1−μ)=0 constraint. The removed helpers req_vacuous and requirement_vacuous have no remaining callers.
• Counted.lean: the counted channel's push requirement is mult ≠ 0 → guarantee (same as Channel.toRaw). not_consistent now uses a simpler two-pull counterexample that matches Clean's BalancedInteractions, which counts a pull of multiplicity N ≥ 2 as a push. The gap it documents is unchanged: dedup chips with μ up to 255 still can't go into a SoundEnsemble. That remains a known limitation, not something this PR introduces.
• eq_rows_correct: it now takes the InteractionsFit premise explicitly. Before, that bound was built into the balance check, so this is a restatement, not a weakening.

Minor (one inline comment): the rewritten doc comment on rust_interaction_at still describes the sender/receiver sign the opposite way from what the code does.