Repository navigation
Counted pulls in formal/: LT with byte μ and soundness by finishing order, on the Clean fork - #1031
Draft
jotabulacios wants to merge 6 commits into
Draft
jotabulacios wants to merge 6 commits into
jotabulacios wants to merge 6 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.
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