binius_spartan_frontend/
lib.rs

1// Copyright 2025 Irreducible Inc.
2
3#![warn(rustdoc::missing_crate_level_docs)]
4
5//! Frontend for building constraint systems for the Binius proof system.
6//!
7//! This crate provides tools for constructing and optimizing constraint systems that can be proven
8//! using the Binius SNARK protocol. It enables writing circuit logic once that works for both
9//! constraint generation and witness computation.
10//!
11//! # Overview
12//!
13//! A constraint system consists of multiplication constraints over binary field elements:
14//! - Each constraint has the form `A * B = C`
15//! - A, B, C are operands (XOR combinations of witness values)
16//! - Constraints reference positions in a witness array by index
17//!
18//! The witness is an array of field elements that satisfies all constraints. Part of the witness
19//! (public inputs/outputs) is known to the verifier, while the rest (private values) is known
20//! only to the prover.
21//!
22//! # Workflow
23//!
24//! 1. **Circuit Construction**: Use [`CircuitBuilder`] to build constraints symbolically
25//! 2. **Compilation**: Convert to optimized [`ConstraintSystem`] via [`compile()`]
26//! 3. **Witness Generation**: Use [`WitnessGenerator`] to compute witness values
27//! 4. **Validation**: Verify witness satisfies constraints (for testing)
28//!
29//! # Example
30//!
31//! ```rust
32//! use binius_field::{Ghash128b as B128, Field};
33//! use binius_spartan_frontend::{
34//!     circuit_builder::{CircuitBuilder, ConstraintBuilder, WitnessGenerator},
35//!     compiler::compile,
36//! };
37//!
38//! // Define a simple circuit: assert that a * b = c
39//! fn multiply<Builder: CircuitBuilder>(
40//!     builder: &mut Builder,
41//!     a: Builder::Wire,
42//!     b: Builder::Wire,
43//! ) -> Builder::Wire {
44//!     builder.mul(a, b)
45//! }
46//!
47//! // Build constraint system
48//! let mut constraint_builder = ConstraintBuilder::new();
49//! let a_wire = constraint_builder.alloc_inout();
50//! let b_wire = constraint_builder.alloc_inout();
51//! let c_wire = constraint_builder.alloc_inout();
52//! let product = multiply(&mut constraint_builder, a_wire, b_wire);
53//! constraint_builder.assert_eq(product, c_wire);
54//!
55//! // Compile to optimized constraint system
56//! let (cs, layout) = compile(constraint_builder);
57//!
58//! // Generate witness with concrete values
59//! let mut witness_gen = WitnessGenerator::new(&layout);
60//! let a = witness_gen.write_inout(a_wire, B128::new(3));
61//! let b = witness_gen.write_inout(b_wire, B128::new(5));
62//! let c = witness_gen.write_inout(c_wire, B128::new(15));
63//! let product = multiply(&mut witness_gen, a, b);
64//! witness_gen.assert_eq(product, c);
65//! let witness = witness_gen.build().unwrap();
66//!
67//! // Validate witness satisfies constraints
68//! cs.validate(&witness);
69//! ```
70//!
71//! # Architecture
72//!
73//! The crate uses a multi-phase compilation pipeline:
74//!
75//! 1. **IR Construction** ([`ConstraintSystemIR`]): Symbolic constraints with zero constraints
76//!    (additions) and multiplication constraints, using symbolic wires
77//!
78//! 2. **Optimization** ([`wire_elimination`]): Eliminates unnecessary private wires by substituting
79//!    zero constraints into multiplication constraints
80//!
81//! 3. **Finalization**: Converts symbolic wires to witness indices, producing the final
82//!    [`ConstraintSystem`] and [`WitnessLayout`]
83//!
84//! This separation allows optimization passes to work on a flexible IR while producing an
85//! efficient final constraint system that directly references witness array positions.
86//!
87//! [`CircuitBuilder`]: circuit_builder::CircuitBuilder
88//! [`ConstraintBuilder`]: circuit_builder::ConstraintBuilder
89//! [`WitnessGenerator`]: circuit_builder::WitnessGenerator
90//! [`ConstraintSystemIR`]: circuit_builder::ConstraintSystemIR
91//! [`ConstraintSystem`]: constraint_system::ConstraintSystem
92//! [`WitnessLayout`]: constraint_system::WitnessLayout
93//! [`compile()`]: compiler::compile
94
95pub mod circuit_builder;
96pub mod circuits;
97pub mod compiler;
98pub mod constraint_system;
99pub mod wire_elimination;
binius_spartan_frontend/lib.rs

binius_spartan_frontend/
lib.rs
