### High-level setup and prove_verify functions

Source: https://context7.com/binius-zk/binius64/llms.txt

The `binius_examples` library provides `setup` and `prove_verify` for bundling verifier and prover setup. `prove_verify` proves and immediately verifies, returning an error if the proof is invalid.

```rust
use binius_examples::{setup, prove_verify, StdVerifier, StdProver};
use binius_hash::sha256::Sha256HashSuite;
use binius_core::constraint_system::{ConstraintSystem, ValueVec};

let cs:      ConstraintSystem = /* compiled circuit */ todo!();
let witness: ValueVec         = /* populated witness */ todo!();

// Setup both verifier and prover in one call (log_inv_rate=1)
let (verifier, prover): (StdVerifier, StdProver) =
    setup::<Sha256HashSuite>(cs, 1, None).expect("setup failed");

// Prove and immediately verify (returns Err if proof is invalid)
prove_verify(&verifier, &prover, witness).expect("prove/verify cycle failed");
println!("Prove-verify succeeded!");
```

--------------------------------

### Run Complete Example

Source: https://github.com/binius-zk/binius64/blob/main/crates/frontend/ceck/README.md

Shows how to run the complete example file and the expected output indicating test results.

```bash
$ ceck example.ceck
Test 1: EQUIVALENT
Test 2: NOT EQUIVALENT (as expected)
```

--------------------------------

### Install and Run ceck CLI Tool

Source: https://context7.com/binius-zk/binius64/llms.txt

Instructions for installing the `ceck` CLI tool, with and without Z3 support, and examples of running test files, specifying random trials, skipping SMT, and piping test input.

```bash
# Install (from repo root)
cargo build -p ceck
cargo build -p ceck --features z3   # with full SMT support

# Run a test file
ceck testsuite/basic_and.ceck

# Test with more random trials
ceck --random-tests 100000 my_circuit.ceck

# Skip SMT (fast mode)
ceck --skip-smt my_circuit.ceck

# Pipe a test inline
echo '(assert_eqv (constraint_set (and $a $b $c)) (constraint_set (and $b $a $c)))' | ceck -
```

--------------------------------

### Add Example to Cargo.toml

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Shows the TOML format for adding a new example binary to the `prover/examples/Cargo.toml` file, specifying the example's name and its source file path.

```toml
[[example]]
name = "my_circuit"
path = "examples/my_circuit.rs"
```

--------------------------------

### Run SHA-512 Preimage Example (Bash)

Source: https://github.com/binius-zk/binius64/blob/main/README.md

Execute a Binius64 example to prove a SHA-512 preimage using the CLI framework. Ensure RUSTFLAGS is set for native optimizations.

```bash
$ RUSTFLAGS="-Ctarget-cpu=native" cargo run --release --example sha512 prove --max-len-bytes 65536 --exact-len
   Finished `release` profile [optimized + debuginfo] target(s) in 0.09s
     Running `target/release/examples/sha512 prove --max-len-bytes 65536 --exact-len`
Building circuit [ 2.99s | 100.00% ]

Setup [ 619.81ms | 100.00% ] { log_inv_rate = 1 }

Generating witness [ 14.12ms | 100.00% ]
├── Input population [ 173.34µs | 1.23% ]
└── Circuit evaluation [ 12.60ms | 89.22% ]

prove [ 128.58ms | 100.00% ] { operation = prove, perfetto_category = operation, n_witness_words = 1048576, n_bitand = 1048576, n_intmul = 1 }
...
```

--------------------------------

### Build and Run Example Circuit

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Provides commands for building and running a Binius64 example circuit using Cargo. Demonstrates running with default, custom parameters, showing help, increasing verbosity, and enabling features.

```bash
# Build
cargo build --release --example my_circuit

# Run with default parameters
cargo run --release --example my_circuit

# Run with custom parameters
cargo run --release --example my_circuit -- --max-size 2048 --input "test data"

# Show help
cargo run --release --example my_circuit -- --help

# Run with increased verbosity
RUST_LOG=info cargo run --release --example my_circuit

# With perfetto feature for performance profiling
cargo run --release --example my_circuit --features perfetto
```

--------------------------------

### Complete ceck Example File

Source: https://github.com/binius-zk/binius64/blob/main/crates/frontend/ceck/README.md

A complete example file demonstrating both equivalent and non-equivalent constraint systems, along with expected test outcomes.

```lisp
; This should pass - both implement v2 = v0 & v1
(assert_eqv
  (constraint_set
    (and $v0 $v1 $v2)
  )
  (constraint_set
    (and $v1 $v0 $v2)  ; AND is commutative
  )
)

; This should fail - different constraints
(assert_not_eqv
  (constraint_set
    (and $v0 $v1 $v2)
  )
  (constraint_set
    (and $v0 $v0 $v2)  ; Different operand
  )
)
```

--------------------------------

### Create a New Circuit Example with Binius

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Implement the `ExampleCircuit` trait, define `Params` and `Instance` structs for CLI parsing, and call `Cli::new().run()` to handle the rest. This template shows how to structure a new circuit example.

```rust
use anyhow::{ensure, Result};
use binius_examples::{Cli, ExampleCircuit};
use binius_frontend::compiler::{circuit::WitnessFiller, CircuitBuilder, Wire};
use clap::Args;

// The main example struct that holds circuit components
struct MyCircuitExample {
    params: Params,
    // Store any gadgets or wire references needed for witness population
    // e.g., gadget: MyGadget,
}

// Circuit parameters that affect structure (compile-time configuration)
#[derive(Args, Debug)]
struct Params {
    /// Maximum size for the circuit
    #[arg(long, default_value_t = 1024)]
    max_size: usize,

    /// Whether to use optimized mode
    #[arg(long, default_value_t = false)]
    optimized: bool,
}

// Instance data for witness population (runtime values)
#[derive(Args, Debug)]
struct Instance {
    /// Input value (if not provided, random data is generated)
    #[arg(long)]
    input: Option<String>,

    /// Size of the input
    #[arg(long)]
    size: Option<usize>,
}

impl ExampleCircuit for MyCircuitExample {
    type Params = Params;
    type Instance = Instance;

    fn build(params: Params, builder: &mut CircuitBuilder) -> Result<Self> {
        // Build your circuit here
        // 1. Add witnesses
        // 2. Add constants
        // 3. Create gadgets
        // 4. Add constraints
        
        // Example:
        // let input_wire = builder.add_witness();
        // let output_wire = builder.add_inout();
        // let gadget = MyGadget::new(builder, params.max_size, input_wire, output_wire);
        
        Ok(Self {
            params,
            // gadget,
        })
    }

    fn populate_witness(&self, instance: Instance, w: &mut WitnessFiller) -> Result<()> {
        // Process instance data and populate witness values
        
        // Example with random or user-provided input:
        let input_data = if let Some(input) = instance.input {
            // Process user-provided input
            input.as_bytes().to_vec()
        } else {
            // Generate random data
            let size = instance.size.unwrap_or(self.params.max_size);
            let mut rng = rand::rngs::StdRng::seed_from_u64(0);
            let mut data = vec![0u8; size];
            rand::RngCore::fill_bytes(&mut rng, &mut data);
            data
        };
        
        // Validate instance data against circuit parameters
        ensure!(
            input_data.len() <= self.params.max_size,
            "Input size ({}) exceeds maximum ({})",
            input_data.len(),
            self.params.max_size
        );
        
        // Populate witness values
        // self.gadget.populate_input(w, &input_data);
        // self.gadget.populate_output(w, &output);
        
        Ok(())
    }
}

fn main() -> Result<()> {
    // Create and run the CLI - this is all you need!
    Cli::<MyCircuitExample>::new("my_circuit")
        .about("Description of what your circuit does")
        .run()
}

```

--------------------------------

### Implementing ExampleCircuit for CLI-driven examples

Source: https://context7.com/binius-zk/binius64/llms.txt

Implement the `ExampleCircuit` trait to create a CLI with subcommands like `prove`, `stat`, and `save`. This example shows a simple circuit that proves `secret XOR secret == 0`.

```rust
use anyhow::Result;
use binius_frontend::{CircuitBuilder, WitnessFiller};
use binius_examples::{Cli, ExampleCircuit};
use clap::Args;

pub struct MyCircuit { secret_wire: binius_frontend::Wire }

#[derive(Args, Clone)]
pub struct MyParams { #[arg(long)] n: usize }

#[derive(Args, Clone)]
pub struct MyInstance { #[arg(long)] value: u64 }

impl ExampleCircuit for MyCircuit {
    type Params   = MyParams;
    type Instance = MyInstance;

    fn build(params: MyParams, b: &mut CircuitBuilder) -> Result<Self> {
        let secret = b.add_witness();
        let public = b.add_inout();
        // Prove secret XOR secret == 0
        let xored = b.bxor(secret, secret);
        b.assert_zero("self_xor_zero", xored);
        Ok(Self { secret_wire: secret })
    }

    fn populate_witness(&self, inst: MyInstance, w: &mut WitnessFiller) -> Result<()> {
        w.set_wire(self.secret_wire, binius_core::word::Word(inst.value));
        Ok(())
    }
}

fn main() -> Result<()> {
    // Run with: cargo run --example my_circuit prove --n 10 --value 42
    // Or:       cargo run --example my_circuit stat --n 10
    Cli::<MyCircuit>::new("my_circuit")
        .about("A simple example circuit")
        .run()
}
```

--------------------------------

### Binius64 AND Constraint Example

Source: https://github.com/binius-zk/binius64/blob/main/ARCHITECTURE.md

Illustrates the structure of an AND constraint in the Binius64 proof system, asserting bitwise AND relations between shifted witness values.

```plaintext
(w[i] << s₁ ⊕ w[j] >> s₂ ⊕ ...) & (w[k] ⊕ ...) = (w[m] ~>> s₃ ⊕ ...)
```

--------------------------------

### Generate Artifacts for Sha256 Circuit

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Use this command to generate the constraint system and witness files for the sha256 example circuit. Ensure you have the example circuit available.

```bash
cargo run --release --example sha256 -- save \
    --cs-path out/sha256/cs.bin \
    --pub-witness-path out/sha256/public.bin \
    --non-pub-data-path out/sha256/non_public.bin
```

--------------------------------

### ceck Lisp-like Test File Examples

Source: https://context7.com/binius-zk/binius64/llms.txt

Examples of `.ceck` test files demonstrating equivalence checks for AND and MUL constraints, including commutativity, inequality detection, and handling of shifted operands.

```lisp
; my_circuit.ceck — verifies commutativity and detects inequality
(assert_eqv
  (constraint_set
    (and $v0 $v1 $v2)               ; (v0 & v1) ^ v2 = 0
  )
  (constraint_set
    (and $v1 $v0 $v2)               ; AND is commutative
  )
)

(assert_not_eqv
  (constraint_set
    (mul $a $b $hi $lo)             ; a * b = (hi << 64) | lo
  )
  (constraint_set
    (mul $a $a $hi $lo)             ; a * a ≠ a * b in general
  )
)

; Shifted operands
(assert_eqv
  (constraint_set
    (and (xor (sll $v0 5) $v1) $v2 $v3)
  )
  (constraint_set
    (and (xor (sll $v0 5) $v1) $v2 $v3)
  )
)
```

--------------------------------

### Install Z3 and pkg-config on macOS

Source: https://github.com/binius-zk/binius64/blob/main/crates/frontend/ceck/README.md

Installs Z3 and pkg-config on macOS using Homebrew, prerequisites for building ceck with Z3 support.

```bash
brew install z3 pkg-config
```

--------------------------------

### Documentation Comment Structure

Source: https://github.com/binius-zk/binius64/blob/main/CONTRIBUTING.md

Follow this recommended structure for documenting code components: a short sentence summary, a more detailed explanation, a copy-pasteable code example, and advanced explanations if needed.

```rust
[short sentence explaining what it is]

[more detailed explanation]

[at least one code example that users can copy/paste to try it]

[even more advanced explanations if necessary]
```

--------------------------------

### Construct, Serialize, and Deserialize ConstraintSystem in Rust

Source: https://context7.com/binius-zk/binius64/llms.txt

Demonstrates manual construction of a `ConstraintSystem` with AND constraints, followed by serialization and deserialization for cross-process transfer. Use this for understanding the core data structure or for manual setup outside of `CircuitBuilder`.

```rust
use binius_core::constraint_system::{
    ConstraintSystem,
    AndConstraint,
    MulConstraint,
    ShiftedValueIndex,
    ValueIndex,
    ValueVecLayout,
    ValueVec
};
use binius_utils::serialization::{SerializeBytes, DeserializeBytes};

// Manual construction (normally done by CircuitBuilder)
let layout = ValueVecLayout {
    n_const: 2, n_inout: 2, n_witness: 4, n_internal: 4,
    offset_inout: 2, offset_witness: 4, committed_total_len: 16, n_scratch: 0,
};
let constants = vec![binius_core::word::Word(1), binius_core::word::Word(0)];
let and_constraints = vec![
    AndConstraint::plain_abc(
        vec![ValueIndex(0)],                            // a: constant[0]
        vec![ValueIndex(4)],                            // b: witness[0]
        vec![ValueIndex(8)],                            // c: internal[0]
    ),
    AndConstraint::abc(
        vec![ShiftedValueIndex::sll(ValueIndex(4), 5)], // a: witness[0] << 5
        vec![ShiftedValueIndex::srl(ValueIndex(5), 3)], // b: witness[1] >> 3
        vec![ShiftedValueIndex::plain(ValueIndex(9))],
    ),
];
let mut cs = ConstraintSystem::new(constants, layout, and_constraints, vec![]);
cs.validate_and_prepare().expect("CS is well-formed");

// Serialize / deserialize for storage or network transfer
let mut buf = Vec::new();
cs.serialize(&mut buf).unwrap();
let cs2 = ConstraintSystem::deserialize(&mut buf.as_slice()).unwrap();
assert_eq!(cs.n_and_constraints(), cs2.n_and_constraints());

// Inspect sizes
println!("AND constraints: {}", cs.n_and_constraints());
println!("MUL constraints: {}", cs.n_mul_constraints());
println!("Witness words:   {}", cs.value_vec_len());
```

--------------------------------

### Binius64 MUL Constraint Example

Source: https://github.com/binius-zk/binius64/blob/main/ARCHITECTURE.md

Defines the format for MUL constraints in the Binius64 proof system, representing 64-bit unsigned integer multiplication.

```plaintext
p * q = 2^64 * hi + lo
```

--------------------------------

### Build ceck with Z3 support

Source: https://github.com/binius-zk/binius64/blob/main/crates/frontend/ceck/README.md

Builds the ceck binary with Z3 support for complete verification. Requires Z3 and pkg-config to be installed.

```bash
cargo build -p ceck --features z3
```

--------------------------------

### Perform Bitwise Operations with CircuitBuilder

Source: https://context7.com/binius-zk/binius64/llms.txt

Illustrates the use of core bitwise gates on 64-bit words provided by CircuitBuilder, including AND, OR, XOR, NOT, and a fused AND-XOR (fax) operation. Also shows an example of computing the SHA-256 sigma0 function.

```rust
use binius_frontend::CircuitBuilder;

let b = CircuitBuilder::new();
let x = b.add_witness();
let y = b.add_witness();
let w = b.add_witness();

let and_result  = b.band(x, y);          // z = x & y          (1 AND)
let or_result   = b.bor(x, y);           // z = x | y          (1 AND)
let xor_result  = b.bxor(x, y);          // z = x ^ y          (linear)
let not_result  = b.bnot(x);             // z = ~x             (linear)
let fax_result  = b.fax(x, y, w);        // z = (x & y) ^ w   (1 AND)
let xn          = b.bxor_multi(&[x, y, w]); // z = x ^ y ^ w  (linear)

// SHA-256 sigma0: ROTR32(x,2) ^ ROTR32(x,13) ^ SHR32(x,3)
let r2  = b.rotr32(x, 2);
let r13 = b.rotr32(x, 13);
let s3  = b.srl32(x, 3);
let sigma0 = b.bxor_multi(&[r2, r13, s3]);
```

--------------------------------

### ceck Test File Format

Source: https://github.com/binius-zk/binius64/blob/main/crates/frontend/ceck/README.md

Examples of assertions for checking constraint system equivalence and non-equivalence using the ceck test file format.

```lisp
; Assert two constraint systems are equivalent
(assert_eqv
  (constraint_set
    (and $v0 $v1 $v2)
  )
  (constraint_set
    (and $v0 $v1 $v2)
  )
)

; Assert two constraint systems are NOT equivalent
(assert_not_eqv
  (constraint_set
    (and $v0 $v1 $v2)
  )
  (constraint_set
    (and $v0 $v1 0x0)
  )
)
```

--------------------------------

### Disable Multithreading (Bash)

Source: https://github.com/binius-zk/binius64/blob/main/README.md

Run a Binius64 example with multithreading disabled by using the `--no-default-features` flag, which controls the `rayon` Cargo feature.

```bash
cargo run --no-default-features
```

--------------------------------

### Prover::setup and Prover::prove for Generating Proofs

Source: https://context7.com/binius-zk/binius64/llms.txt

Use `Prover::setup` to derive proving keys from the verifier and `Prover::prove` to generate a proof transcript from a witness. Ensure all necessary imports are included. The generated proof can then be used with the verifier.

```rust
use binius_prover::Prover;
use binius_verifier::{Verifier, config::StdChallenger};
use binius_verifier::transcript::ProverTranscript;
use binius_hash::sha256::Sha256HashSuite;
use binius_field::arch::OptimalPackedB128;
use binius_core::constraint_system::ValueVec;

let cs = /* circuit.constraint_system().clone() */ todo!();
let witness: ValueVec = /* filler.into_value_vec() */ todo!();

let verifier = Verifier::<Sha256HashSuite>::setup(cs, 1).expect("verifier setup failed");
let prover   = Prover::<OptimalPackedB128, Sha256HashSuite>::setup(verifier.clone())
    .expect("prover setup failed");

let challenger = StdChallenger::default();
let mut prover_transcript = ProverTranscript::new(challenger.clone());
prover.prove(witness.clone(), &mut prover_transcript).expect("proving failed");

let proof = prover_transcript.finalize();
println!("Proof size: {} KiB", proof.len() / 1024);

// Hand proof_bytes + public inputs to verifier
let mut verifier_transcript =
    binius_verifier::transcript::VerifierTranscript::new(challenger, proof);
verifier.verify(witness.public(), &mut verifier_transcript).unwrap();
verifier_transcript.finalize().unwrap();
```

--------------------------------

### Initialize and Configure CLI Builder

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Use the `Cli` builder to set up a new circuit with basic information like name, description, version, and author. The `run()` method initiates the circuit building process.

```rust
Cli::<MyExample>::new("my_circuit")
    .about("Short description")           // Shown in help
    .long_about("Detailed description")   // Shown with --help
    .version("1.0.0")                     // Version info
    .author("Your Name")                  // Author info
    .run()
```

--------------------------------

### Verify Proofs with Verifier::setup and Verifier::verify

Source: https://context7.com/binius-zk/binius64/llms.txt

Preprocess a constraint system with `Verifier::setup` for repeated verification. Use `verify` to check a proof transcript against public inputs.

```rust
use binius_verifier::{Verifier, config::StdChallenger};
use binius_verifier::transcript::VerifierTranscript;
use binius_hash::sha256::Sha256HashSuite;
use binius_core::constraint_system::ConstraintSystem;

// Assume cs: ConstraintSystem was previously compiled
let cs: ConstraintSystem = /* circuit.constraint_system().clone() */ todo!();

// Setup: validates and prepares the CS, chooses FRI params
// log_inv_rate = 1 means code rate 1/2 (standard security/size tradeoff)
let verifier: Verifier<Sha256HashSuite> =
    Verifier::setup(cs, /*log_inv_rate=*/ 1).expect("setup failed");

// Verify a proof given the public inputs (produced by a prover)
let proof_bytes: Vec<u8> = /* received from prover */ vec![];
let public: &[binius_core::word::Word] = /* public portion of witness */ &[];

let challenger = StdChallenger::default();
let mut transcript = VerifierTranscript::new(challenger, proof_bytes);
verifier.verify(public, &mut transcript).expect("proof is invalid");
transcript.finalize().expect("transcript not fully consumed");
println!("Proof verified successfully!");
```

--------------------------------

### Verifier::setup / Verifier::verify

Source: https://context7.com/binius-zk/binius64/llms.txt

Provides functionality for verifying proofs. `Verifier::setup` preprocesses a constraint system for repeated verification, and `Verifier::verify` checks a proof transcript against the public inputs.

```APIDOC
## Verifier::setup / Verifier::verify

### Description
Provides functionality for verifying proofs. `Verifier::setup` preprocesses a constraint system for repeated verification, and `Verifier::verify` checks a proof transcript against the public inputs.

### Usage
```rust
let verifier: Verifier<Sha256HashSuite> =
    Verifier::setup(cs, /*log_inv_rate=*/ 1).expect("setup failed");

let challenger = StdChallenger::default();
let mut transcript = VerifierTranscript::new(challenger, proof_bytes);
verifier.verify(public, &mut transcript).expect("proof is invalid");
transcript.finalize().expect("transcript not fully consumed");
```
```

--------------------------------

### Build a Simple Circuit with CircuitBuilder

Source: https://context7.com/binius-zk/binius64/llms.txt

Demonstrates how to use CircuitBuilder to construct a basic arithmetic circuit for proving knowledge of 'x' such that '(x & mask) == expected_output'. This involves adding public inputs/outputs and private witnesses, then applying gate operations and compiling the circuit.

```rust
use binius_frontend::{CircuitBuilder, Wire, WitnessFiller};
use binius_core::word::Word;

// Build a simple circuit: prove knowledge of x s.t. (x & mask) == expected_output
let mut builder = CircuitBuilder::new();

// Public I/O visible to both prover and verifier
let mask:     Wire = builder.add_inout();
let expected: Wire = builder.add_inout();

// Private witness known only to the prover
let x: Wire = builder.add_witness();

// Gate operations
let masked = builder.band(x, mask);                 // 1 AND constraint
let diff   = builder.bxor(masked, expected);         // 1 linear constraint (free-ish)
builder.assert_zero("masked_equals_expected", diff); // 1 AND constraint

// Compile to constraint system
let circuit = builder.build();
println!("AND constraints: {}", circuit.constraint_system().n_and_constraints());
// Expected output: AND constraints: 2
```

--------------------------------

### Load and Prove Circuit from Files from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command demonstrates loading a previously saved circuit state (constraint system and witness) from files and then performing the proof. This is the second step in a two-step proving process.

```bash
cargo run --release --example sha256 load-prove \
    --cs-path /tmp/cs.bin \
    --pub-witness-path /tmp/pub.bin \
    --non-pub-data-path /tmp/priv.bin \
    --key-collection-path /tmp/keys.bin
```

--------------------------------

### Run SHA-256 Preimage Proof from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command demonstrates how to prove a SHA-256 preimage with a 1024-byte message using the binius-circuits CLI. Ensure RUSTFLAGS are set for SIMD optimizations.

```bash
export RUSTFLAGS="-C target-cpu=native"   # enable SIMD optimizations

# Prove a SHA-256 preimage (1024-byte message, exact length)
cargo run --release --example sha256 prove --max-len-bytes 1024 --exact-len
```

--------------------------------

### Run Bitcoin Header Chain Proof from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command shows how to prove a Bitcoin header chain of 10 blocks using the binius-circuits CLI. Ensure RUSTFLAGS are set for SIMD optimizations.

```bash
# Prove a Bitcoin header chain (10 blocks)
cargo run --release --example bitcoin_header_chain prove --n-blocks 10
```

--------------------------------

### Run ceck with different options

Source: https://github.com/binius-zk/binius64/blob/main/crates/frontend/ceck/README.md

Demonstrates how to run ceck on a test file, read from stdin, skip SMT checking, or skip random testing.

```bash
# Run on a test file
ceck test.ceck

# Read from stdin
echo "(assert_eqv (constraint_set) (constraint_set))" | ceck -

# Skip SMT checking (only randblast)
ceck test.ceck --skip-smt

# Skip random testing (only SMT)
ceck test.ceck --skip-random
```

--------------------------------

### Extract Byte from 64-bit Word

Source: https://context7.com/binius-zk/binius64/llms.txt

Extract a specific byte from a 64-bit word, zero-extending it into the lower 8 bits. Bytes are indexed from 0 (least significant) to 7 (most significant). This can be used to repack bytes into a new word, for example, in big-endian order.

```rust
use binius_frontend::CircuitBuilder;

let b = CircuitBuilder::new();
let word = b.add_witness();

let byte0 = b.extract_byte(word, 0); // bits [7:0]
let byte3 = b.extract_byte(word, 3); // bits [31:24]
let byte7 = b.extract_byte(word, 7); // bits [63:56]  (most significant)

// Example: repack bytes into a word (big-endian layout)
let bytes: Vec<_> = (0..8).map(|j| b.extract_byte(word, 7 - j)).collect();
```

--------------------------------

### Run Ethereum ECDSA Signature Proof from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command demonstrates proving an Ethereum ECDSA signature (ecrecover) using the binius-circuits CLI. RUSTFLAGS should be configured for SIMD optimizations.

```bash
# Prove an Ethereum ECDSA signature (ecrecover)
cargo run --release --example ethsign prove
```

--------------------------------

### Build and Test Commands for Binius64

Source: https://github.com/binius-zk/binius64/blob/main/AGENTS.md

Standard Cargo commands for building, testing, formatting, linting, and documenting Rust projects. Use `--release` for optimized builds and specific flags for detailed linting or documentation generation.

```bash
cargo build                    # Debug build
```

```bash
cargo build --release          # Release build
```

```bash
cargo test                     # Run tests
```

```bash
cargo test -p <crate>          # Test specific crate
```

```bash
cargo fmt                      # Format code
```

```bash
cargo clippy --all --all-features --tests --benches --examples -- -D warnings
```

```bash
cargo doc --no-deps --document-private-items   # Build rustdoc
```

```bash
typos                          # Check for typos
```

```bash
pre-commit run --all-files     # Run all checks
```

--------------------------------

### Produce Proof with Binius Prover

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

This command utilizes the Binius prover binary to generate a proof from the previously created artifacts. Specify the paths to the constraint system, public witness, non-public data, and the desired output proof path. The log of the inverse rate can also be set.

```bash
cargo run --release --bin prover -- \
    --cs-path out/sha256/cs.bin \
    --pub-witness-path out/sha256/public.bin \
    --non-pub-data-path out/sha256/non_public.bin \
    --proof-path out/sha256/proof.bin \
    --log-inv-rate 1
```

--------------------------------

### Use Zero-Knowledge Mode from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command demonstrates how to run a SHA-256 proof in zero-knowledge mode, which hides the witness from the verifier. It requires RUSTFLAGS to be set for SIMD optimizations.

```bash
# Use zero-knowledge mode (hides witness from verifier)
cargo run --release --example sha256 prove --max-len-bytes 1024 --zk
```

--------------------------------

### Run SHA-512 Preimage Proof from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command shows how to prove a SHA-512 preimage with a 65536-byte message using the binius-circuits CLI. It requires RUSTFLAGS to be set for SIMD optimizations.

```bash
# Prove a SHA-512 preimage
cargo run --release --example sha512 prove --max-len-bytes 65536 --exact-len
```

--------------------------------

### Display Circuit Statistics from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command demonstrates how to display circuit statistics for a SHA-256 circuit without performing a full proof. It requires RUSTFLAGS to be set for SIMD optimizations.

```bash
# Display circuit statistics without proving
cargo run --release --example sha256 stat --max-len-bytes 1024
```

--------------------------------

### Build SHA-256 Preimage Proof Circuit

Source: https://context7.com/binius-zk/binius64/llms.txt

This Rust code demonstrates how to construct a SHA-256 preimage proof circuit using binius-circuits. It sets up the circuit builder, defines input wires for message length, digest, and message content, and then populates the witness with specific message data and its corresponding hash.

```rust
use binius_circuits::sha256::Sha256;
use binius_frontend::{CircuitBuilder, Wire, WitnessFiller};
use binius_core::word::Word;
use sha2::Digest;
use std::array;

// Build a SHA-256 preimage proof circuit
let mut b = CircuitBuilder::new();
let max_len_words = 128;                           // handles up to 1024 bytes
let len_bytes: Wire  = b.add_witness();
let digest: [Wire; 4] = array::from_fn(|_| b.add_inout()); // 4 × 64-bit = 256-bit hash
let message: Vec<Wire> = (0..max_len_words).map(|_| b.add_inout()).collect();
let sha = Sha256::new(&mut b, len_bytes, digest, message.clone());

let circuit = b.build();
println!("AND constraints: {}", circuit.constraint_system().n_and_constraints());

// Populate witness: prove SHA-256("hello world") = known digest
let msg_bytes = b"hello world";
let hash = sha2::Sha256::digest(msg_bytes);
let mut padded = msg_bytes.to_vec();
padded.resize(max_len_words * 8, 0);

let mut filler = circuit.new_witness_filler();
sha.populate_len_bytes(&mut filler, msg_bytes.len());
sha.populate_message(&mut filler, &padded);
sha.populate_digest(&mut filler, hash.into());
circuit.populate_wire_witness(&mut filler).unwrap();
let witness = filler.into_value_vec();
// witness is now ready for binius_examples::prove_verify(...)
```

--------------------------------

### Clone binius.xyz Repository

Source: https://github.com/binius-zk/binius64/blob/main/AGENTS.md

Command to clone the binius.xyz repository if it does not exist locally, enabling direct access to protocol documentation.

```bash
git clone https://github.com/binius-zk/binius.xyz.git ../binius.xyz
```

--------------------------------

### Handle Variable vs. Fixed Size Wires

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Demonstrates how to add a constant wire for a fixed size or a witness wire for a variable size based on circuit parameters. This is crucial for circuits that need to handle inputs of different lengths.

```rust
let len_wire = if params.exact_len {
    builder.add_constant_64(params.max_len as u64)
} else {
    builder.add_witness()
};
```

--------------------------------

### Configure Release Profile for Optimizations (TOML)

Source: https://github.com/binius-zk/binius64/blob/main/README.md

Add these lines to your Cargo.toml to enable thin Link Time Optimization (LTO) for release builds, improving performance.

```toml
[profile.release]
lto = "thin"
```

--------------------------------

### Save Circuit Artifacts to Files

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Illustrates how to use the `save` subcommand with specific flags to write circuit artifacts like the constraint system, public witness, and non-public witness data to specified file paths. Parent directories are created automatically.

```bash
# Save only the constraint system
cargo run --release --example my_circuit -- save --cs-path out/cs.bin

# Save public values and non-public values
cargo run --release --example my_circuit -- save \
    --pub-witness-path out/public.bin \
    --non-pub-data-path out/non_public.bin

# Save all three
cargo run --release --example my_circuit -- save \
    --cs-path out/cs.bin \
    --pub-witness-path out/public.bin \
    --non-pub-data-path out/non_public.bin
```

--------------------------------

### Save Circuit State to Files from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command demonstrates saving the constraint system and witness to separate files for later use. It is part of a two-step process for proving circuits.

```bash
# Save constraint system and witness to files, then load and prove separately
cargo run --release --example sha256 save \
    --max-len-bytes 64 --exact-len \
    --cs-path /tmp/cs.bin \
    --pub-witness-path /tmp/pub.bin \
    --non-pub-data-path /tmp/priv.bin \
    --key-collection-path /tmp/keys.bin
```

--------------------------------

### Use Vision Hash Suite for Faster Merkle Tree from CLI

Source: https://context7.com/binius-zk/binius64/llms.txt

This bash command shows how to use the Vision hash suite for faster Merkle tree computations in a SHA-256 proof. It requires RUSTFLAGS to be set for SIMD optimizations.

```bash
# Use Vision hash suite for faster Merkle tree (vs default SHA-256)
cargo run --release --example sha256 prove --max-len-bytes 1024 --compression vision
```

--------------------------------

### License Identifier (SPDX)

Source: https://github.com/binius-zk/binius64/blob/main/README.md

This project is dual-licensed under Apache-2.0 or MIT. The SPDX license identifier clearly states this dual licensing.

```text
SPDX-License-Identifier: Apache-2.0 OR MIT
```

--------------------------------

### Regenerate Proof Reference Binary

Source: https://github.com/binius-zk/binius64/blob/main/crates/core/test_data/README.md

Use this command to regenerate the reference binary for Proof after incrementing its SERIALIZATION_VERSION. This test is ignored by default.

```bash
cargo test -p binius-core -- --ignored create_proof_reference_binary
```

--------------------------------

### Build R1CS Circuits and Generate Witnesses with Iron Spartan Frontend

Source: https://context7.com/binius-zk/binius64/llms.txt

This Rust code demonstrates building R1CS-style circuits over GF(2^128) using `CircuitBuilder` and compiling them. It also shows how to generate a witness using `WitnessGenerator` for concrete field values and validate it against the compiled circuit.

```rust
use binius_field::BinaryField128bGhash as B128;
use binius_spartan_frontend::{
    circuit_builder::{CircuitBuilder, ConstraintBuilder, WitnessGenerator},
    compiler::compile,
};

// Generic circuit function works for both constraint building and witness generation
fn dot_product<Builder: CircuitBuilder>(
    b: &mut Builder, xs: &[Builder::Wire], ys: &[Builder::Wire],
) -> Builder::Wire {
    let products: Vec<_> = xs.iter().zip(ys).map(|(&x, &y)| b.mul(x, y)).collect();
    products.into_iter().reduce(|a, v| b.add(a, v)).unwrap()
}

// Phase 1: Build constraint system
let mut cb = ConstraintBuilder::new();
let xs: Vec<_> = (0..4).map(|_| cb.alloc_inout()).collect();
let ys: Vec<_> = (0..4).map(|_| cb.alloc_inout()).collect();
let result_wire = cb.alloc_inout();
let dot = dot_product(&mut cb, &xs, &ys);
cb.assert_eq(dot, result_wire);
let (cs, layout) = compile(cb);

// Phase 2: Witness generation with concrete B128 values
let mut wg = WitnessGenerator::new(&layout);
let x_vals = [B128::new(1), B128::new(2), B128::new(3), B128::new(4)];
let y_vals = [B128::new(5), B128::new(6), B128::new(7), B128::new(8)];
for (&wire, &val) in xs.iter().zip(&x_vals) { wg.write_inout(wire, val); }
for (&wire, &val) in ys.iter().zip(&y_vals) { wg.write_inout(wire, val); }
// expected result: 1*5 ^ 2*6 ^ 3*7 ^ 4*8 in GF(2^128)
let dot_val = dot_product(&mut wg, &xs, &ys);
wg.write_inout(result_wire, dot_val);
let witness = wg.build().expect("witness is valid");

// Validate witness satisfies all constraints
cs.validate(&witness);
```

--------------------------------

### Run Pre-commit Hooks and Nightly Rustfmt

Source: https://github.com/binius-zk/binius64/blob/main/CONTRIBUTING.md

Use pre-commit hooks to run rustfmt and a specific nightly version of cargo fmt for consistent formatting, as required by CI.

```bash
$ pre-commit run rustfmt --all-files
$ cargo +nightly-2026-01-01 fmt  # see .pre-commit-config.yaml for the exact nightly version checked by CI
```

--------------------------------

### Verify Proof with Binius Verifier

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/README.md

Use the Binius verifier binary to check the integrity of a generated proof. This requires the constraint system, public witness, and the proof file. The verifier ensures the proof is valid and that the embedded challenger type matches HasherChallenger<Sha256>.

```bash
cargo run --release --bin verifier -- \
    --cs-path out/sha256/cs.bin \
    --pub-witness-path out/sha256/public.bin \
    --proof-path out/sha256/proof.bin \
    --log-inv-rate 1
```

--------------------------------

### Regenerate ConstraintSystem Reference Binary

Source: https://github.com/binius-zk/binius64/blob/main/crates/core/test_data/README.md

Use this command to regenerate the reference binary for ConstraintSystem after incrementing its SERIALIZATION_VERSION. This test is ignored by default.

```bash
cargo test -p binius-core -- --ignored create_reference_binary
```

--------------------------------

### Add Compile-Time Constants with CircuitBuilder

Source: https://context7.com/binius-zk/binius64/llms.txt

Shows how to add constants to a CircuitBuilder. Constants are deduplicated and do not incur constraint costs as they are known to both the prover and verifier. Supports zero, all ones, 64-bit values, and zero-extended 8-bit values.

```rust
use binius_frontend::CircuitBuilder;
use binius_core::word::Word;

let builder = CircuitBuilder::new();

let zero     = builder.add_constant(Word::ZERO);
let all_ones = builder.add_constant(Word::ALL_ONE);
let c1       = builder.add_constant_64(0xFF00FF00_FF00FF00u64);
let byte_val = builder.add_constant_zx_8(42u8); // zero-extended to 64 bits

// Constants with the same value are aliased (same Wire handle)
let c2 = builder.add_constant_64(0xFF00FF00_FF00FF00u64);
assert_eq!(c1, c2); // true — deduplicated
```

--------------------------------

### Run Automated Checks with Cargo

Source: https://github.com/binius-zk/binius64/blob/main/CONTRIBUTING.md

Execute Rustfmt for code formatting and Clippy for linting with warnings disabled. Ensure all features, tests, and benchmarks are included.

```bash
$ cargo fmt
$ cargo clippy --all --all-features --tests --benches --examples -- -D warnings
```

--------------------------------

### CircuitBuilder - Construct arithmetic circuits

Source: https://context7.com/binius-zk/binius64/llms.txt

CircuitBuilder is the primary interface for describing computations. Users can add wires (constants, public inputs/outputs, private witnesses) and gates (bitwise AND, XOR, addition, multiplication, shifts, comparisons) to build a directed acyclic graph. Calling `build()` compiles the graph into an optimized `Circuit` containing the `ConstraintSystem`.

```APIDOC
## CircuitBuilder - Construct arithmetic circuits

`CircuitBuilder` is the primary interface for describing computations. You add wires (constants, public inputs/outputs, private witnesses) and gates (bitwise AND, XOR, addition, multiplication, shifts, comparisons) to build a directed acyclic graph. Calling `build()` compiles the graph into an optimized `Circuit` containing the `ConstraintSystem`.

```rust
use binius_frontend::{CircuitBuilder, Wire, WitnessFiller};
use binius_core::word::Word;

// Build a simple circuit: prove knowledge of x s.t. (x & mask) == expected_output
let mut builder = CircuitBuilder::new();

// Public I/O visible to both prover and verifier
let mask:     Wire = builder.add_inout();
let expected: Wire = builder.add_inout();

// Private witness known only to the prover
let x: Wire = builder.add_witness();

// Gate operations
let masked = builder.band(x, mask);                 // 1 AND constraint
let diff   = builder.bxor(masked, expected);         // 1 linear constraint (free-ish)
builder.assert_zero("masked_equals_expected", diff); // 1 AND constraint

// Compile to constraint system
let circuit = builder.build();
println!("AND constraints: {}", circuit.constraint_system().n_and_constraints());
// Expected output: AND constraints: 2
```
```

--------------------------------

### Prover-Side Hints with CircuitBuilder::call_hint

Source: https://context7.com/binius-zk/binius64/llms.txt

Utilize hints for deterministic computations during witness generation. Ensure results are constrained using normal gates.

```rust
use binius_frontend::CircuitBuilder;

let b = CircuitBuilder::new();

// BigUint division hint: quotient, remainder (4-limb 256-bit values)
let dividend: Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let divisor:  Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let (quotient, remainder) = b.biguint_divide_hint(&dividend, &divisor);
// Must constrain: remainder + divisor * quotient == dividend (via bignum circuits)

// Modular exponentiation hint: base^exp mod modulus
let base:    Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let exp:     Vec<_> = (0..2).map(|_| b.add_witness()).collect();
let modulus: Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let result = b.biguint_mod_pow_hint(&base, &exp, &modulus);

// Modular inverse hint
let (quotient2, inverse) = b.mod_inverse_hint(&base, &modulus);
// Must constrain: base * inverse == 1 + quotient2 * modulus

// Secp256k1 scalar endomorphism split (for optimized ECDSA scalar multiplication)
let k: Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let (k1_neg, k2_neg, k1_abs, k2_abs) = b.secp256k1_endomorphism_split_hint(&k);
```

--------------------------------

### Check sha256 Circuit Snapshot

Source: https://github.com/binius-zk/binius64/blob/main/crates/examples/snapshots/README.md

Use this command to check the snapshot for the sha256 circuit with specific parameters. Ensure parameters match when checking and updating.

```bash
cargo run --example sha256 -- check-snapshot --max-len 64
```

--------------------------------

### CircuitBuilder::call_hint

Source: https://context7.com/binius-zk/binius64/llms.txt

Provides prover-side hints for deterministic computations during witness generation. Results must be separately constrained using normal gates.

```APIDOC
## CircuitBuilder::call_hint

### Description
Provides prover-side hints for deterministic computations during witness generation. Results must be separately constrained using normal gates.

### Available Hints
- `biguint_divide_hint`: Computes quotient and remainder for BigUint division.
- `biguint_mod_pow_hint`: Computes modular exponentiation (base^exp mod modulus).
- `mod_inverse_hint`: Computes modular inverse.
- `secp256k1_endomorphism_split_hint`: Splits a Secp256k1 scalar for optimized ECDSA scalar multiplication.

### Usage Example (biguint_divide_hint)
```rust
let dividend: Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let divisor:  Vec<_> = (0..4).map(|_| b.add_witness()).collect();
let (quotient, remainder) = b.biguint_divide_hint(&dividend, &divisor);
```
```