Repository navigation
Counted pulls in formal/: LT with byte μ and soundness by finishing order, on the Clean fork - #1031
Draft
jotabulacios wants to merge 10 commits into
Draft
jotabulacios wants to merge 10 commits into
jotabulacios wants to merge 10 commits into
Conversation
…ove the counted channel consistent there. The lakefile points at the fork branch, which adds pulls of multiplicity up to N, a counted channel and soundness by finishing order on top of Clean f3abad7c. For now it is a path dependency on the build server (../../clean-fork-main); it becomes a git dependency on yetanotherco/clean once the branch is pushed. Channels/Counted.lean gains consistentUpTo: under BalancedUpTo N, which the fork's balance checks provide, the counted channel is consistent. It is the positive counterpart of not_consistent, which still shows the gap under BalancedInteractions alone.
…oes. mu is now a byte instead of a bit: the row pulls IS_HALF and MSB16 with multiplicity mu through counted channels, and bounds mu by pulling ARE_BYTES[mu, 0]. The row spec holds for rows with mu != 0, and the honest prover keeps mu below 2^8. With this the Lean LT chip matches the Rust one exactly, so lean_diff.rs no longer expects the mu bit constraint on the Lean side and ARE_BYTES on the Rust side; it asserts that no constraint or interaction appears on one side only.
…d pulls on one bus. MIN is not an RV64IM operation. Its chip pulls an LT result from the ALU bus and pushes its own result on the same bus, as the division chip pulls LT and MUL results and pushes DIVREM. The ALU guarantee gets a MIN clause (opsel 7), so EQ, LT and SHIFT also prove that their pushes are not MIN results.
… the ALU bus. LtStaged builds the LT ensemble with counted IS_HALF and MSB16 and proves its table soundness with tableSoundness_of_staged: ARE_BYTES is finished first, so LT's bound mu <= 255 on its counted pulls follows from that guarantee. It then adds MIN, finishing the ALU bus in two stages, every message that is not MIN before MIN. CountedSameBus does the same with CMIN, which pulls LT and pushes MIN with a counted multiplicity on the ALU bus, the shape of a deduplicated division chip, and proves it sound with tableSoundness_of_stagedOn.
…rk on GitHub instead of a local path, so the branch builds anywhere and not only on the build server. The pinned revision, 1cf67e24, is the same Clean the model was built against (counted pulls and soundness by finishing order on top of Clean main f3abad7c); Mathlib and CompPoly are unchanged.
…6 with multiplicity μ through Channel.counted 255 and matches lt.rs exactly, so the LT deltas and the "LT keeps μ a bit" notes are gone. The counted-pulls section says what the model takes from the yetanotherco/clean fork (Balance.logUpUpTo, Channel.counted, soundness by finishing order) and describes the LtStaged and CountedSameBus ensembles; the layout lists MinToy and flags MIN as a toy stand-in for DVRM on the ALU bus.
…It announced an end-to-end LT theorem and then described LtStaged as proving the LT ensemble sound, which overstates it: LtStaged proves Ensemble.TableSoundness, which is one premise of a sound ensemble and not the conclusion, and it leaves witness.Assumptions to the caller. That premise is not free here, because the ARE_BYTES, IS_HALF and MSB16 providers are not tables: provider and countedProvider push whatever value they are handed under Assumptions input data := channel.Guarantees input.1 data, so each one assumes its own answers are correct, and CountedSameBus reuses both of those components. The section now says that, says there is no lt_rows_correct, and keeps the contrast with EqLookup explicit, where pushStatic proves the guarantee from membership in a real static table and eq_rows_correct discharges witness.Assumptions outright. The technical content about what the fork supplies is unchanged.
…is branch removed. LT no longer has the isBit mu constraint: it pulls ARE_BYTES[mu, 0] as lt.rs does, so no table has a Lean-only constraint and all three lean_diff tests assert that the four unmatched lists are empty. The comment in lean_diff.rs still named that delta as the reason Lean-only constraints are skipped on honest rows, and the differential-check section of formal/README still said the deltas are skipped there while the Known differences section lists none. Both now describe what the test does, and the skip in lean_diff.rs is marked as a guard for a future table rather than something that fires today.
… rests on a sorry or on an axiom outside propext, Classical.choice and Quot.sound. The job built formal/ and checked that the export was up to date, but nothing ruled out a proof that holds only because a hole was left in it, which is the one failure mode a reader of the README cannot see. LambdaVM/Axioms.lean lists the five circuits (LT, EQ, SHIFT, MinToy, CountedMin) and the four ensemble theorems (eq_rows_correct, LtStaged.tableSoundness, LtStaged.tableSoundness_withMin, CountedMin.tableSoundness) as #print axioms lines; it is not imported by LambdaVM.lean, so lake build ignores it and the workflow runs it with lake env lean. The step also counts the reports against the #print axioms lines in the file, so a renamed or deleted declaration fails instead of dropping out of the check, and an unknown constant fails lean itself.
…with the four fixes that came out of the audit of that branch. The pin is a raw sha rather than a branch name, so the fork and this file move in lockstep and a reader of either knows exactly which Clean the proofs were checked against. The four are not a rewrite of the mechanism, only of how it is stated and what it is known to require. SoundChannels takes the pull bound after the subject, matching the argument order of every other predicate in that file; matchedUpTo_of_balanced gets a default so a plain balance check compiles again without naming the bound; each balance check exposes its pullBound to simp, which is what lets a proof discharge the bound instead of unfolding the check; and not_consistent proves the bound cannot be weakened, by exhibiting for 2 <= N <= 255 over Goldilocks a pair of pulls that satisfies plain BalancedInteractions while the counted channel reads both as pulls and the second guarantee is false. The model does not use the three APIs whose signatures moved, so nothing in formal/LambdaVM changes with the pin. That was checked by building all of lambda_vm against the new Clean before this commit, not inferred from the diff.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
Lambda VM chips deduplicate: one LT row answers
μ ≤ 255identical queries, so it pulls its rangechecks (
IS_HALF,MSB16) with multiplicityμ. Clean main requires every pull to havemultiplicity 0 or 1, which is why the model kept LT's
μa bit and documented two deltas againstlt.rs. Two things are missing upstream:1..Nwith a push. Field-sum balance alonedoesn't:
(p − 1)/2pulls of 2 and one pull of 1 sum top ≡ 0with no push. It does whenlength · N < p.bound
μ ≤ 255comes from its own pull ofARE_BYTES[μ, 0], and DVRM pulls LT/MUL results andpushes DIVREM results on the same ALU bus, which a whole-channel order reads as a cycle.
Both live in the
counted-pullsbranch of theyetanotherco/clean fork: Clean main
f3abad7c(the one #1030 moved to) plus three commits.Description
lakefile.toml/lake-manifest.json: Clean from the fork at1cf67e24. Mathlib and CompPolyare unchanged.
Tables/Lt.lean:μis a byte, as inlt.rs.IS_HALFandMSB16are pulled withmultiplicity
μthroughChannel.counted 255, bounded byARE_BYTES[μ, 0]. The export andlean_diff.rsnow match LT exactly (6 constraints, 10 interactions), so the LT deltas are gone.Ensembles/LtStaged.lean: the LT ensemble is sound underBalance.logUpUpTo 255, finishingARE_BYTESbefore the countedIS_HALFandMSB16, and those before ALU.Tables/MinToy.leanandopselMIN := 7inBuses/Alu.leangive an operation with DVRM's shape: it pulls an LT result on the ALU bus andpushes its own result on the same bus.
LtStaged.leanfinishes ALU in two stages (non-MINmessages, then MIN messages) and proves the ensemble sound;
Ensembles/CountedSameBus.lean(CMIN) does it with the ALU bus itself counted. EQ, LT and SHIFT discharge the extra
Alu.Guaranteesclause byomega. MIN is meant to be replaced by DVRM once it is modelled.Channels/Counted.lean: gainsconsistentUpTo, the positive counterpart ofnot_consistentunder the fork's
BalancedUpTo N. It is no longer used by any table; whether to keep onlynot_consistentor drop it is left for a follow-up.README.md: the counted-pulls section describes what comes from the fork and the new ensembles.Draft: opened to run
formal.ymland to discuss the approach. The fork stays onf3abad7cuntilsomething from newer Clean is needed.
How to Test
cd formal && lake exe cache get && lake buildlake env lean --run LambdaVM/Export.lean && git diff --exit-code -- exportcargo test -p lambda-vm-prover --lib lean_diff