Repository navigation
feat(formal): Clean/Lean model of BITWISE, LT, EQ and SHIFT with proo… - #1027
Draft
ColoCarletti wants to merge 17 commits into
Draft
ColoCarletti wants to merge 17 commits into
ColoCarletti wants to merge 17 commits into
Conversation
…fs and a differential check against the prover
Contributor
|
/review-ai |
Contributor
|
/ai-review |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
| let (prog, _) = cb.finish(num_base_from_meta(&meta)); | ||
|
|
||
| // Fingerprints over random rows. | ||
| let rows = random_rows(num_cols, 0xC1EA_0000 ^ label.len() as u64); |
Contributor
There was a problem hiding this comment.
Low (readability): label.len() gives the same seed for "LT" and "EQ" (both are length 2), so salting by label length does nothing here. It's harmless because the tables differ, but a fixed seed (or one passed in per table) would be clearer.
| path: | | ||
| formal/.lake | ||
| !formal/.lake/packages/mathlib | ||
| key: lake-${{ hashFiles('formal/lean-toolchain', 'formal/lake-manifest.json') }}-${{ github.sha }} |
Contributor
There was a problem hiding this comment.
Low (CI): Because the key ends in github.sha, every push saves a new .lake cache entry. That cache includes the Clean and CompPoly builds, so entries will pile up and push older caches (including the Rust ones) out of the repo's 10 GB cache quota. Consider keying only on toolchain + manifest, plus a hash of formal/**/*.lean if incremental builds matter.
Contributor
|
Review summary No critical, high or medium issues. The Rust changes are test-only, apart from making
Minor notes (two are posted inline):
🤖 Generated with Claude Code |
…el to its channel API. Clean removed StaticLookupChannel in favour of Air.Flat.Lookup, so the structure moves to LambdaVM/StaticLookup.lean and BITWISE reads its tables through toChannel. Interactions now carry a direction and a nonnegative multiplicity, and a pull must have multiplicity 0 or 1: EQ, LT and SHIFT discharge that from their existing bit constraints, and their guarantees are stated for multiplicity 1 instead of -1. EqLookup is rewritten for the current SoundEnsemble API (a balance parameter, channels added before tables, unique table names, a demand generation mode per component), and eq_rows_correct takes the InteractionsFit premise that TableSoundness now has. Channels/Counted.lean is ported to directions; not_consistent needs only two interactions, since a pull of multiplicity N >= 2 counts as a push. A grind call in IsByte that no longer closes its goal is replaced by a direct proof. The export now records each interaction's direction, so the JSON files are regenerated and lean_diff.rs signs Lean multiplicities by direction. Nothing that is proven changes.
…p fallback the linter flags. if_true, if_false, if_pos, if_neg, dif_pos and dif_neg become ite_true, ite_false, ite_eq_left, ite_eq_right, dite_eq_left and dite_eq_right, as in Clean. In SHIFT, first | ... | skip becomes try first | ..., which behaves the same. The build has no warnings left.
… the bump, and the renames left in SHIFT's completeness proof. Both lemmas discharged a pull requirement stated with the old multiplicity -1 (`¬ -e = -1 → ¬ e = 0 → P`), which the directed interactions no longer produce. In SHIFT, the hypotheses that needed neg_inj.mp to go from `-x = -1` to `x = 1` now arrive as `x = 1`, so they are introduced under their final names instead of being copied.
…tates the sign the comparison uses: a sender (Clean's pull) counts −m and a receiver (Clean's push) +m. The old first sentence described the prover's LogUp sum, where a sender adds +m, and read as if it contradicted the code below it. Comment only, no code change.
Clean's Demand.direction is the net sign of a message, pushes minus pulls, so a demand of direction .pull is one that was pulled more often than pushed and needs a component that pushes to answer it. EQ pushes its result on the ALU bus, so its generation mode has to trigger on .pull, the same way pushStaticComponent does and the same way Clean's own add8Component and lookup provider do. The field is inert today, since generation is not part of TableSoundness and nothing here runs Clean's witness generator, but .push described a component that answers pushes by pulling, which EQ never does.
The Clean bump changed the things this file documents: pulls carry a nonnegative multiplicity with an explicit direction instead of a negative one, a pull owes a multiplicity of 0 or 1, BalancedInteractions no longer carries the interaction count bound (it moved to the Balance's fits, reaching soundness as the InteractionsFit premise), and not_consistent is now a two-interaction witness instead of the p/N construction. Also lists LambdaVM/StaticLookup.lean, which the bump added, and records that the export format carries the direction.
Bump Clean to current main (f3abad7c) and Lean to v4.35.0 in formal/
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.
…fs and a differential check against the prover