R1CS Verification

Lof validates its generated R1CS through cross-validation against equivalent Circom circuits. The goal is to test mathematical behavior with repeatable inputs and explicit failure cases.

What equivalence means

Two circuit implementations are treated as mathematically equivalent when they have:

1. The same witness assignments for the same inputs.
2. The same constraint satisfaction behavior.
3. Valid proof generation and verification.
4. Consistent rejection of invalid inputs.

Cross-validation workflow

Each verification case contains a Lof circuit, an equivalent Circom circuit, and shared test vectors.

verification/
├── circuits/01_basic/
│   ├── multiply.lof
│   └── multiply.circom
├── test_cases/01_basic/
│   └── multiply_tests.json
├── scripts/
│   ├── compile_both.sh
│   ├── generate_witnesses.sh
│   ├── compare_results.py
│   └── run_verification.sh
└── artifacts/

Example circuit

proof Multiply {
    input a: field;
    input b: field;
    witness c: field;

    let product = a * b in
    assert product === c
}

The reference circuit is compiled independently, then both implementations are evaluated with the same valid and invalid test vectors.

Validation stages

Basic framework

• Define structured test vectors.
• Compile equivalent circuits in both languages.
• Generate witnesses independently.
• Compare assignments and constraint satisfaction.

Regression suite

• Cover arithmetic, equality, comparisons, arrays, and more complex circuits.
• Record constraint counts for efficiency comparisons.
• Run the full suite in CI to catch breaking changes.
• Publish clear pass or fail output for every test case.

Cross-validation does not replace formal verification, but it provides concrete and repeatable evidence that the compiler preserves the intended circuit behavior as the language evolves.