feat: update to Noir 1.0.0-beta.25

[TomAFrench]

Overview

Updates Lampe's targeted Noir version from 1.0.0-beta.19 (with the stdlib still extracted at beta.14) to 1.0.0-beta.25: the extractor is ported to the new noirc APIs, the vendored stdlib is re-vendored and re-extracted at beta.25, and the handwritten stdlib theorem layer plus the testing projects are repaired so everything builds green. A new doc describes the version-update process end to end.

Extractor (src/)

Ports to the beta.25 noirc APIs: DependencyId::DataType, comptime-integer Type::Constant, flipped Type::Array(E, N) argument order, BigInt/byte literals, the reworked deprecation attributes, and the new QuotedType::Location / HirStatement::TraitAssociatedConstant (the latter's placeholder globals are skipped). Two behavioural changes were needed:

• Builtin/foreign trait impl methods no longer have elaborated bodies upstream, so the extractor now synthesizes a body forwarding to the intrinsic.
• Trait default methods materialize per impl with Self bound to itself; Self is now resolved to the impl's concrete type while generating an impl, and identity type-variable bindings no longer recurse forever.

Lampe library (Lampe/)

• Bool bit decompositions: Noir's bit decompositions now return bool arrays instead of u1 arrays. toLeBits/toBeBits/modulusLeBits/modulusBeBits move to .bool with Bool.toDigit/Digit.toBool conversions and roundtrip simp lemmas in Lampe.Data.Digits; the Hoare intro rules are restated accordingly.
• The new poseidon2_config_state_size foreign builtin is modeled as the constant 4, matching the width-4 (BN254) Poseidon2 configuration Lampe formalizes.
• Builtin.mkFormatString is now implemented (it was an unprovable stub; beta.25's poseidon2_permutation builds a format string for its static assert).
• The eDSL gains a dedicated token for the unitEq builtin (beta.25's stdlib exercises Eq for unit, and maximal munch tokenizes #_unitEq as the #_unit literal followed by Eq).
• Struct gains cross-member indexTpl/replaceTuple' simp lemmas, needed now that BoundedVec methods read and write through references.

Stdlib spec (stdlib/)

stdlib/src is re-vendored from the pinned rev (collections/map.nr and collections/vec.nr are gone, integer.nr, internal/ and meta/location.nr are new, slices have become vectors), the extracted std-1.0.0-beta.14 package is replaced by std-1.0.0-beta.25, and the theorem layer is repaired:

• &self migration: BoundedVec::get/get_unchecked/len, the BoundedVec and array higher-order methods (map/mapi/for_each/for_eachi/fold/reduce/all/any/concat/sort_via/sort), Option::is_some/is_none, and check_shuffle (now over &[T; N] operands) are all restated in the by-reference style and re-proved.
• u1 removal / bool bits: the u1 Eq/arith/bit specs are deleted; to_le_bits/to_be_bits, pow_32 and sgn0 proofs are converted to the bool-array decomposition (with Mathlib's lex List.LE' locally erased, since Bool is a LinearOrder and it would shadow the core list order the proofs use). bytes32_to_field was removed upstream, so its spec goes too.
• BoundedVec semantics: pop no longer zeroes the popped slot, from_parts lost its zeroing loop, from_parts_unchecked is deprecated (excluded from the extracted env, spec deleted), and extend_from_bounded_vec bounds its loop with cmp::min (covered by a new min_u32_spec). Eq is re-proved against the new element-wise active-prefix comparison.
• Poseidon2: the sponge struct is gone upstream; the new chunked finish_ref absorption is modeled directly (addToState/chunkState/finishDigest) and finish/finish_ref/write/RATE/CAPACITY/POSEIDON2_CONFIG_STATE_SIZE are re-proved.
• Embedded curves: EmbeddedCurvePoint lost is_infinite; infinity is canonically (0, 0). The Lampe curve model is reshaped and the point/scalar/MSM specs re-proved — the round-trip lemmas now require [Bn254.Prime p] so that (0, 0) is off-curve.
• Pedersen: the removed hash::from_field_unsafe is bridged via EmbeddedCurveScalar::from_field's safe decomposition.
• Misc: tuple Ord impls now end in a value-if, so the tuple3/4/5 proofs are restructured; Collections/Map specs are gone with the upstream module; some files explicitly raise heartbeat/recursion limits, as the larger extracted env pushes them over the defaults.

Testing projects (testing/)

Re-extracted at beta.25 with proofs repaired. The Merkle projects' vendored deps/hasher-0.0.0 snapshots are replaced by direct path requires on ../../hasher/lampe (the extractor no longer vendors dependencies that ship their own lampe directory, so the snapshots could never be regenerated), and Merkle gains a clean.sh matching Base64's. The Rust extraction tests now run on a 16MiB thread, as the beta.25 elaborator overflows the default 2MiB test-thread stack in debug builds.

Docs

docs/ gains a guide to the Noir version update process: every place the targeted version is referenced, the update procedure, and the testing steps that validate an update.