feat: add Groth16 verifier reference contract for Soroban

[dinahmaccodes]

PR Description

Changes Made

#1216 Groth16 Verifier Reference Contract

• contracts/zk-verifier/src/groth16.rs — Proof/VK types, structural validation, public-input binding, VK integrity hash
• contracts/zk-verifier/src/lib.rs — Full contract with verify_proof, VK rotation (propose/approve/execute/cancel), nullifier checks, access control
• contracts/zk-verifier/README.md — Security model, API docs, limitations
• contracts/zk-verifier/.sanctify.toml — Sanctify configuration

#1214 Kani Proof Harnesses for VK Rotation

• contracts/zk-verifier/src/vk_storage.rs — Pure rotation logic with 6 Kani harnesses proving: no rotation without quorum, no rotation before timelock, cancel prevents execution, can_cancel property, quorum_met property, all-conditions-met property
  Add Z3 SMT encoding for circuit range-check verification #1213 Z3 SMT Encoding for Circuit Range-Check
• tooling/sanctifier-core/src/smt/circuit_range.rs — Encodes circom constraints as Z3 assertions, checks signal boundedness via SMT
• tooling/sanctifier-core/src/rules/z007_under_constrained.rs — Z007 rule for circom with --deep-verify SMT mode
• tooling/sanctifier-core/src/lib.rs — deep_verify_circuit_range on Analyzer, smt_timeout_ms config field
• docs/adr/006-z3-formal-verification.md — Documented circuit range-check encoding

#1215 Formal-Verification Scope ADR

• docs/adr/011-formal-verification-scope.md — Documents what Kani/Z3 proofs cover and don't cover (cryptographic soundness excluded)
• docs/rules/Z007.md, docs/rules/Z010.md — Cross-reference ADR-011
• contracts/README.md — Added zk-verifier to catalog

Checklist

• Z3 SMT circuit range-check encoding implemented and correctly confirms/refutes obligations on test circuits
• Groth16 verifier contract compiles, passes tests, and scans clean against Z-rules
• ADR-011 documents formal-verification scope and limitations
• Kani harnesses prove VK rotation invariants (quorum, timelock, cancel)
• Z007 wired with --deep-verify SMT mode
• All docs cross-linked

Closes #1213
Closes #1214
Closes #1215
Closes #1216

[vercel]

@dinahmaccodes is attempting to deploy a commit to the gbangbolaoluwagbemiga's projects Team on Vercel.

A member of the Team first needs to authorize it.

[drips-wave]

@dinahmaccodes Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits