Add reproducible compiler status for bn254 and Goldilocks - #5
Open
BornPsych wants to merge 10 commits into
Open
Conversation
The ledger headers record `rustc --version`, so a ledger regenerated here and one regenerated by CI have to come from one toolchain. The pin is the one the pinned Noir crates declare in their own `rust-toolchain.toml`.
`projection_hash` fingerprints the mono AST, the artifact Mavros consumes: it strips source locations, debug tables and identifier-use ids, renumbers functions, globals and locals by first encounter in a fixed traversal from `main`, keeps names, types, exact literals, operators and attributes, and hashes the resulting text with SHA-256. Two builds that reach the same program through differently numbered items, as `#[field]` gating makes the two fields do, therefore project identically. `PROJECTION_VERSION` names the text format and is bumped whenever it changes.
The referee kept no record of what one compiler did at the previous pin, tolerated either side failing to run, and compared failures by kind only. This makes a committed ledger the cross-revision comparison. Dump format 3: `RunRecord` records each step of a program's run (load, compile, interpret, the check against the `return` recorded in `Prover.toml`, the mono-AST projection) under its own panic guard; `ComparableError` carries a kind and a payload (normalized assertion message, overflowing operation and width, unsupported construct, compiler diagnostic text); `DiffValue::Field` carries its canonical value; the provenance records the compiler's own build stamp, the corpus content hash, the toolchain and the enabled features. `ledger/bn254.md`, `ledger/goldilocks.md` and `ledger/cross-field.md` hold one row per corpus program and fixture, generated at the pinned `c978bd2675` by `just ledger`; CI regenerates them per field and fails when a fresh run differs from the committed copy. Divergences are rows with a verdict, not assertions. Capability tags predict the one-sided gaps the recorded inputs cause; `KNOWN_FIELD_DEPENDENT` names programs whose semantics are field-dependent by design and must keep diverging. Guards: the eleven `worldfnd/noir` pins must agree with each other and with the compiler stamp; the sweep refuses a corpus checkout at another revision or with local changes; programs run in place, as Noir's own harness runs them, so path dependencies resolve. Two defects surfaced by the new tests are fixed: panic messages were lost (a `&Box<dyn Any>` was handed to a `&dyn Any` parameter and unsized to the box), so every goldilocks monomorphizer crash read `panic`; and overflow errors did not name the operand width.
`c978bd2675` was the tip of `ys/goldilocks-port`; `7db2450226` is its merge into `provekit-v2` (worldfnd/noir#10) and has the identical tree. The regenerated ledgers differ from the previous commit's in the `noir_rev` header line of each file and in nothing else.
A program with a git dependency that fails to elaborate under goldilocks names the dependency's file in its `DependencyCompileGap` payload, and `nargo_toml` clones such dependencies under `~/nargo`, a path that differs between machines. The first CI run of the ledger gate caught four such rows whose truncated cells carried different hash suffixes. The home-relative cache root now normalizes to `<nargo>` like the program, checkout and referee roots, with a unit test feeding a cached dependency path through the normalizer.
BornPsych
changed the title
`FieldDescriptor::current` and `bits`, the `mavros-oracle` arm of the feature list and the linear-scan fallback in the projection's function lookup had no callers outside their own tests. Everything the ledger and corpus modules only use internally is private now, and the crate no longer exports `is_coverage_gap` or `normalize_text`. `FailureKind` and `Verdict` implement `Display` instead of a `label` method. Tests that exercised one rule in several functions are one function each.
The source hash covered `Nargo.toml`, `Prover.toml` and `src/**`, which left the nested crates of `traits_in_crates_1` and `traits_in_crates_2` outside the fingerprint. It now covers every file under the program directory except `target/`, so the `source` column and the corpus hash change for the programs that carry extra files.
BornPsych
changed the title
Mavros keeps one glanceable `STATUS.md` with a glyph per check; the three ledgers were wide tables of text. `STATUS.md` now has one row per program with `compile`, `run` and `return` under each field, the cross-field verdict, whether both monomorphized ASTs project to the same hash, and an eight-digit fingerprint of the underlying records, so any change in a payload, value or hash still moves the row; the payloads themselves stay in the JSON dumps. The field jobs only upload their dumps; the `status` job renders the file and is the single CI gate. Targets are `make sweep`, `make render`, `make status`, `make status-check`; the module is `status.rs`.
The source hash covers a program's git-tracked files only, so an ignored file cannot move a row that the cleanliness check accepts; path normalization also matches a root's lexically normalized form and stops at name boundaries. A recorded return whose type the field cannot represent leaves the return check not run instead of failing it: the two goldilocks rows that showed a failed return had compared nothing, and a fixture covers the case. The allowlist keeps the four programs that are field-dependent by design, and the render fails when an allowlisted program stops being field-dependent, a tagged program's gap is not the predicted one, or an invariant fixture is missing. A failed projection step shows as an AST mismatch; a panic's detail keeps the whole message; the record fingerprint separates the source hash from the steps. Classification notes, the unused embedded-curve capability, the field descriptor, the divergence buckets and `failure_kind_of` are gone; `DiffValue` and `StepOutcome` implement `Display`; the crate calls itself the interpreter throughout. CI pins `dtolnay/rust-toolchain` by commit and refuses an empty pin; the toolchain file lists the clippy and rustfmt components.
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
1 participant
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.
This PR adds
STATUS.md, a saved scorecard of what the pinned Noir compiler and this interpreter do with every one of Noir'sexecution_successtest programs and our own small test programs, under both bn254 and Goldilocks. Each row shows whether a program compiled, ran, and returned the recorded answer under each field, whether the two fields agree, whether the compiled program has the same shape under both, and a short code that changes whenever anything underneath changes. Known gaps are labelled rather than hidden: values Goldilocks cannot represent, standard-library code that does not compile there yet, and a short list of programs that are allowed to differ by design; anything else that differs is marked as a divergence for someone to look at. CI regenerates the file on every push and fails when it differs from the committed one, so any later change to the compiler or the interpreter shows up as a row change a reviewer can see and approve. Along the way the PR locks the Rust version and the exact Noir commit, fixes two small bugs the new checks found (panic messages were being lost, and overflow errors did not say which integer width overflowed), and documentsmake status, which regenerates the file in about seven minutes per field.