width-generic comptime integer - #7
Merged
Merged
Conversation
A `Value::Field` carries an `acvm::FieldValue` — a canonical representative together with the field it belongs to — instead of the compiled-in `FieldElement`. The interpreter takes its field from the label the monomorphized output records, so one build compiles and interprets the same program under bn254 and under Goldilocks. `compile_for_validation` asks for a field and asserts the monomorphizer answered with it, which is the check the compiler's design record asks every consumer of the output to make. `try_to_field` uses `FieldConfig::fits_unsigned`, the compiler's own predicate, so a cast it accepts is exactly one the type checker admitted. A `Field` literal whose magnitude the field cannot hold is refused rather than reduced, matching `FieldValue::try_from_bigint`; the old local `bigint_to_field` wrapped it silently. A `Field` input crosses from the ABI parser, which still reads the linked field, into the interpreted one and is refused when that field cannot hold it. Tolerating dependency diagnostics now depends on the field being compiled for, not on the feature the crate was built with: the standard library's un-gated code is written for bn254, so any other field reaches errors that say nothing about the program under test. Noir moves to the stage-4b tip, where comptime `Field` values carry their field and the driver refuses a non-linked field only where the backend engages.
`FIELD` selects the field a sweep records, and `Capability` asks the compiler's own `FieldConfig::fits_unsigned` rather than restating the rule against hard-coded moduli. `Sides` takes the two fields from the dumps themselves, so the renderer no longer parses moduli out of strings to recognise them. Whether a recorded return is compared exactly follows the field rather than the cargo feature, since it is the corpus recording bn254 values that makes bn254 the exact one. The sweep still needs a build linked against the field it records, and now says so: `Prover.toml` values reach the interpreter through the ABI parser, which reads them in the linked field, and the entry-point rule tells a native `-1` from a quoted `p - 1` by their source syntax — which an `InputValue::Field` has already erased into one element. Guessing which was meant either refuses an input the field can hold or runs a program on a value its file does not specify; the second would report agreement between two different computations. `dump_records` asserts the swept and linked fields agree. A single-build sweep waits for the ABI codec to take a field of its own. An integer input now meets the entry-point rule of the field being interpreted: its unsigned fixed-width bit pattern must be a value of that field. That rule was reaching the sweep only through the linked parser, and the corpus caught its absence — six programs lost the one-sided gap their capability tags predict. STATUS.md is regenerated at the new pin and is unchanged but for the revision: all 536 programs keep their verdicts under both fields.
The compiler's comptime integer is now one `Int { signed, bits, value }`
for every width instead of nine native variants. Nothing here reads it:
the crate takes the monomorphized program, its field label and the ABI,
none of which moved.
STATUS.md is regenerated at the new pin and changes only in `noir_rev`:
all 536 programs keep their verdicts and record fingerprints under both
fields, which is what a behaviour-neutral compiler change must leave.
BornPsych
changed the title
`inputs_from_prover_toml` and `expected_return_from_prover_toml` now refuse a field the build is not linked against instead of re-homing what the ABI parser returns. The parser reads a file in the linked field and resolves a native `-1` and a quoted `p - 1` to the same element, so the spelling that distinguishes them is gone by the time an `InputValue` arrives; interpreting one in another field would have to guess which was written. Refusing says that plainly, and the per-field checks the decoder was carrying go with it: an integer's fixed-width bit pattern is bounded against the modulus by the parser itself, and a `Field` it accepted is already a value of the field it read. The sweep asserts the two fields agree, so those checks were restating the parser. That leaves the caller who builds `Value` inputs by hand, for whom nothing checked anything. `interpret_with_inputs` now walks them first. Every `Field` must belong to the program's field, because `FieldValue`'s arithmetic asserts on mixed operands and would turn a caller's mistake into an interpreter ICE part-way through a run. Every integer must be a value of the width and signedness it declares: `IntValue`'s members are public, so an input can name one outside the range its own type describes, and the interpreter has no way to tell that from a value it produced itself. A width of zero is refused too — it holds no values, and asking for its range would underflow. The walk descends through arrays, tuple cells and references, visiting each shared cell once so an alias or a cycle cannot loop it.
The commentary had grown to restate what the code beside it already shows, and in places to argue a design decision at the point of use rather than record it. Where a comment repeated a call, a name or a type, it goes; where it carried a reason the code cannot, it stays and gets shorter. The claims that named goldilocks now name the field they mean, since tolerating a dependency diagnostic and comparing a recorded return follow the field being compiled for, not the feature the crate was built with. `field_to_bigint` was a local wrapper around a panic `FieldElement::to_u128` no longer has: `FieldValue` keeps a canonical representative and hands it over as a `BigInt` directly. The callers say `to_bigint` and the wrapper goes, along with the four comments explaining why it existed. Two asserts in the renderer had gone quiet. `Sides` reads the field names out of the dumps, which left `field_modulus` checked by nothing but a comparison the field-name assert above it already makes impossible. Each dump now has to record the modulus of the field it claims, so a dump that disagrees with itself is refused rather than classified against properties its own provenance disputes. `temp_noir_package` is the scaffolding the projection test had inlined; the input tests needed the same thing, so it moves next to the other corpus helpers.
BornPsych
added this pull request to stack #9
September 16, 2026 21:39
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
2 participants
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.
One build now compiles and runs the same program under bn254 and then under Goldilocks. Check:
cargo testin both builds, clippy with warnings denied in both,make status.What changed
Fieldvalue remembers which field it belongs to. The interpreter reads the field from the compiled program (Noir has labelled it since feat(frontend): pass field configuration through the compiler noir#12), not from how the crate was built. A test compiles and runs one program under both fields.Fieldliteral too big for the field is refused, not silently wrapped. Same rule as the compiler.(from groups discusssion)Fieldcast asks the compiler's own rule about which widths fit, so the interpreter and the type checker cannot disagree.make sweep FIELD=goldilocksnames the field it records and refuses to run on a bn254 build.Where it stops short
Prover.tomlinputs. Noir's input parser still reads them in the field the crate was linked against. Once a plain-1and a written-outp - 1become the same number, nothing can tell them apart. So the sweep behindSTATUS.mdstill needs a build linked against the field it records.The pin
The last commit pins Noir at the tip of
provekit-v2after worldfnd/noir#15, where a compile-time integer has one shape for every width instead of nine. This crate reads none of that. Fresh sweep under both fields: only the revision line ofSTATUS.mdchanged; all 536 programs keep the same result and the same fingerprint.