Skip to content

Propagate DirectSNARK synthesis errors and enforce the step circuit arity contract - #517

Open
somasoil wants to merge 1 commit into
microsoft:mainfrom
somasoil:fix/direct-snark-error-propagation
Open

somasoil wants to merge 1 commit into
microsoft:mainfrom
somasoil:fix/direct-snark-error-propagation

Conversation

@somasoil

@somasoil somasoil commented Oct 3, 2026

Copy link
Copy Markdown

Summary

DirectSNARK swallowed every error raised while synthesizing the step circuit, and never
checked that the circuit honors the arity it declares. setup / prove now return a proper
NovaError in all of those cases.

Changes

  • src/spartan/direct.rs
    • DirectCircuit no longer discards the two inputize results; they are propagated with ?.
    • Added DirectCircuit::synthesize_inner, which returns NovaError and enforces the
      StepCircuit arity contract:
      • supplied inputs must have exactly arity() elements, otherwise NovaError::InvalidInputLength;
      • the step circuit must return exactly arity() outputs, otherwise
        NovaError::InvalidStepOutputLength.
    • DirectSNARK::setup and DirectSNARK::prove call synthesize_inner(&mut cs)? instead of
      let _ = circuit.synthesize(&mut cs);, so synthesis failures are surfaced as
      NovaError::SynthesisError { .. } through the existing From<SynthesisError> impl.
    • The Circuit impl is kept and is now a thin wrapper over synthesize_inner, so there are no
      public API changes and the existing call sites in src/neutron/{nifs,relation}.rs keep working.

Why a private synthesize_inner

Circuit::synthesize must return SynthesisError, so a check placed inside it cannot surface the
existing typed NovaError::InvalidInputLength / NovaError::InvalidStepOutputLength.
synthesize_inner returns NovaError and is what setup / prove call, which makes each failure
mode directly assertable in tests (same style as the existing
assert_eq!(pp.err(), Some(NovaError::InvalidStepCircuitIO)) in src/nova/mod.rs).

Tests

Added to src/spartan/direct.rs:

  • FailingCircuit — a step circuit whose synthesize always returns
    Err(SynthesisError::Unsatisfiable(..)). Both setup and prove now return
    Err(NovaError::SynthesisError { .. }).
  • WrongOutputArityCircuit — declares arity() == 2 but returns a single output. setup returns
    Err(NovaError::InvalidStepOutputLength).
  • prove with an input that is too long (2 elements for arity() == 1) returns
    Err(NovaError::InvalidInputLength); with an empty input it returns the same error instead of
    panicking (previously an index-out-of-bounds panic).

Verified:

  • cargo test --release --lib spartan::direct — 3 passed
  • cargo test --release --features experimental neutron — 10 passed (DirectCircuit is also used there)
  • cargo clippy --all-targets -- -D warnings — clean
  • cargo fmt --all -- --check — clean

Checklist

  • cargo fmt --all -- --check
  • cargo clippy --all-targets -- -D warnings
  • cargo test --release

…rity contract

Signed-off-by: somasoil <somasoil@outlook.com>
@somasoil

somasoil commented Oct 3, 2026

Copy link
Copy Markdown
Author

@microsoft-github-policy-service agree

@somasoil

somasoil commented Oct 9, 2026

Copy link
Copy Markdown
Author

Srinath Setty (@srinathsetty) Could you please take a look when you have a chance? Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant