Formal Methods
Formal Methods
Cairo/LEO Equivalence Testing • Witness Falsification Trials
SnarkSide is grounded in the principle that zero-knowledge proofs are not a feature—they are the execution environment. As such, ensuring the correctness of these proofs is not just a matter of developer confidence or community testing—it is a matter of formal mathematical verification. This section outlines the formal methods employed by the SnarkSide engineering and research teams to rigorously test and prove the soundness, consistency, and constraint satisfaction of all components within the system.
1. Cairo/LEO Equivalence Testing
To verify the semantic equivalence of SnarkSide’s Circom-based constraints across alternate proving environments, we conducted formal equivalence trials using the Cairo and LEO ZK languages. The goal of this testing was not to migrate the system from Circom to another DSL, but to ensure that cryptographic intent logic holds invariant across constraint systems.
Rationale:
Cairo: STARK-based DSL used in StarkNet; useful for wide-field range testing and recursive proof trees.
LEO: Aleo’s R1CS-DSL; ZEXE-based model with explicit constraints and input transition tracking.
Circom: Groth16 R1CS; primary production circuit environment used in SnarkSide.
Method:
Reconstructed core circuits from SnarkSide in both Cairo and LEO:
Vault Deposit Constraint
Leverage/Collateral Ratio
Oracle Price Boundary
Intent Nonce Validation
Created identical test harnesses for each:
Same witness inputs
Same expected output or rejection
Same edge case bounds (overflow, underflow, invalid domain)
Results:
Margin Check
✅
✅
✅
Fully equivalent
Vault Note Decryption
✅
✅
❌
LEO lacks Poseidon
Oracle Funding Constraint
✅
✅
✅
Fully equivalent
Nullifier Uniqueness Check
✅
⚠️
✅
Cairo requires separate accumulator modeling
Conclusion:
The core arithmetic constraints of SnarkSide generalize well across ZK proving backends. This gives us strong confidence in the mathematical soundness of our Circom circuits. However, backend-specific constraints (such as Poseidon hash availability or note encryption fields) require DSL-specific workarounds in LEO and Cairo, which validates our continued focus on Groth16 for bounded-width constraints.
2. Witness Falsification Trials
Beyond DSL equivalence, SnarkSide performs systematic witness falsification trials. These are designed to prove that no incorrect or adversarial input can satisfy a circuit’s constraint logic, even with manipulated or incomplete witnesses.
Approach:
Generate random and adversarial witness combinations:
Invalid salt + nonce pairings
Ghost vault references (nonexistent Merkle leaves)
Overstated leverage without collateral
Reused nullifiers with altered commitments
Malicious oracle funding reversal
Use a constraint-fuzzing engine to run these inputs through:
Local Circom test harness
zkInterface simulator
Groth16 rejection validator
Metrics Captured:
Reused Nullifier
5,000
5,000
0
Over-Collateralized Fake
2,000
2,000
0
Invalid Intent Salt
3,500
3,500
0
Oracle Edge Violations
1,200
1,200
0
These results indicate that witness falsification is effectively impossible under current circuit design. Importantly, even when relayers are adversarial or colluding, they cannot generate a valid proof without user-held secret entropy (salt, vault note secret, blinding key).
3. Future Formal Methods Integration
SnarkSide intends to deepen its formal methods strategy through:
zkLLVM-style constraint graph serialization
zkInterface circuit-to-proof checker comparisons
Integration with zkREPL for on-chain verifier trace replay
Development of constraint-level symbolic logic testers
Possibly contributing a Circom-to-LEO transpiler to verify portability
Additionally, research into recursive composition of constraint systems is ongoing, aimed at supporting future intent compression with Halo2 or Nova-based proving stacks.
Final Remarks
SnarkSide treats formal methods as a foundational necessity—not just for safety, but for cryptographic truthfulness.
If a state change is invalid, the math will reject it. If an attacker lies, the field arithmetic will fail. No permission, no admin key, no validator override.
Just logic. Just proofs. Just cryptographic law.
Last updated