ragu_core: add Gadget::from_wires_gadget on GadgetKind#8
Open
mitschabaude wants to merge 12 commits into
Open
Conversation
New kind-level method that constructs a gadget by pulling wires from an iterator in the same canonical order that map_gadget visits them. Witness payloads are synthesized via MaybeKind::empty, so the method only compiles against drivers whose MaybeKind represents non-existing values (e.g. extraction drivers). Real drivers hit a const panic at monomorphization time, preventing silent stub-witness bugs. Gadget gets a defaulted from_wires proxy that forwards to Kind::from_wires_gadget, mirroring how map/map_gadget and enforce_equal/enforce_equal_gadget are split today. Derive generates from_wires_gadget for every #[derive(Gadget)] user: - #[ragu(wire)]: pull one item from the iterator. - #[ragu(value)]: synthesize via MaybeKind::empty(). - #[ragu(gadget)]: recurse via the Gadget::from_wires proxy. - #[ragu(phantom)]: PhantomData. Hand-impls updated for (), [G; N], (G1, G2), Box<G>, Demoted, FixedVec, and the TwoWires/OneWire test fixtures. On the extraction side, ExtractionDriver::alloc_input<T> now takes any T: Gadget and constructs it from a generator iterator, replacing the WireDeserializer template trick. WireDeserializer is deleted; every instance file collapses from ~25 lines of setup to a single `dr.alloc_input()?` call plus the gadget method. Extracted Lean output is byte-for-byte unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
New tiny proc-macro crate `lean_extraction_macros` exporting a single `extract_gadget!(Name, Field, closure)` macro. The closure's typed parameters become input gadgets (allocated via `dr.alloc_input()`); the last (untyped) parameter is the driver; the body returns `Result<T>` where `T` is anything collectable by `WireCollector`, including tuples of gadgets (which go through the foreign `(G1, G2)` Gadget impl). Collapses each instance file to a single invocation: - point_double.rs: 26 → 10 lines - point_negate.rs: 26 → 10 lines - point_add_incomplete.rs: 36 → 13 lines - point_alloc.rs: 44 → 20 lines (two invocations, Fp + Fq) Extracted Lean output is byte-for-byte unchanged. The macro has to live in its own crate (rustc requires `proc-macro = true` to be an exclusive property of a crate). We don't fold it into `ragu_macros` because that crate is about ragu_core derive macros, and this macro references `lean_extraction` internals. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…sec/fv-ci-ux # Conflicts: # fv/crates/lean_extraction/src/instances/point_add_incomplete.rs # fv/crates/lean_extraction/src/instances/point_alloc.rs # fv/crates/lean_extraction/src/instances/point_double.rs # fv/crates/lean_extraction/src/instances/point_negate.rs
|
constructing a gadget from a raw flat wire stream feels like it has footguns, though that’s just a vague and unfounded intuition. cc @ebfull |
With each instance now a single `extract_gadget!` invocation, the four
per-instance files (point_double, point_negate, point_alloc,
point_add_incomplete) plus their `mod.rs` are excessive. Merge them into
a single `instances.rs` module with shared `use` statements at the top.
main.rs imports simplify from per-submodule paths to a single flat
`use crate::instances::{...};`.
Extracted Lean output is byte-for-byte unchanged.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mitschabaude
commented
Apr 20, 2026
Member
Author
There was a problem hiding this comment.
all extracted instances now live here
- Apply nightly rustfmt to the consolidated `instances.rs`. - Drop the redundant explicit path on `[`ExtractionDriver`]` — the type is already in scope via `use`, and nightly rustdoc rejects the repeated target under `-D warnings`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.
Builds on top of the clean-integration PR. Three additions.
Gadget::from_wiresin ragu_coreNew kind-level method
GadgetKind::from_wires_gadgetthat constructs any gadget by pulling wires from an iterator in the canonicalmap_gadgetorder. Witness payloads are synthesized viaMaybeKind::empty, so it only compiles against drivers whoseMaybeKindrepresents non-existing values — real drivers hit aconst panicat monomorphization.Gadget::from_wiresis a defaulted proxy on top, mirroring the existingmap/map_gadgetsplit.The
#[derive(Gadget)]macro generates it automatically. Hand-impls updated for(),[G; N],(G1, G2),Box<G>,Demoted,FixedVec,InternalCircuitValues,RxValues.On the extraction side, this replaces the
Point::constant(dr, generator())+WireDeserializertemplate trick with a cleandr.alloc_input::<T>().Gadget::to_wires+ roundtrip testsDual of
from_wires: a defaulted method that serializes a gadget into a flatVec<D::Wire>viamap. Retires the extraction-localWireCollector::collect_fromhelper.The round-trip invariant (
from_wiresandto_wiresare mutual inverses forMaybeKind = Emptydrivers) is documented on both methods and covered by three test modules:crates/ragu_core/src/gadgets/roundtrip.rs— foreign impls ((), arrays, tuples,Box) plus hand-writtenSingle/Pairfixtures.crates/ragu_primitives/tests/roundtrip.rs—Element(derive),FixedVec,Demoted.crates/ragu_pcd/src/internal/native/stages/query.rs—InternalCircuitValues,RxValues.extract_gadget!macroNew tiny proc-macro crate
lean_extraction_macrosexportingextract_gadget!(Name, Field, closure). The closure's typed params become input gadgets (viaalloc_input); the last untyped param is the driver; the body's return value is flattened viaGadget::to_wires(tuple outputs compose through the foreign(G1, G2)impl).Every instance collapses to a single line, and the five instance files are consolidated into a single
instances.rs:Extracted Lean output is byte-for-byte unchanged throughout.
Test plan
cargo build --locked --workspacecargo test --locked --workspacecargo run --locked -p lean_extraction -- check— every generated Lean file byte-identicalcargo run --locked -p lean_extraction -- export— succeedslake build --wfailunderqa/lean/— Lean project builds clean🤖 Generated with Claude Code