Cowrie Research

proof-validation-output-consumption-and-statement-binding-discipline

16 min read

Proof Validation-Output Consumption and Statement-Binding Discipline

  • Name: proof validation-output consumption and statement-binding discipline
  • Category: zk-circuit reference / statement-binding checklist / validator-gadget discipline / proof-authority review note
  • Summary: Healthy proof systems do not stop at instantiating the right validator gadgets. They make every mandatory validation result, and every hidden helper precondition that makes that result meaningful, become explicit statement truth. If a circuit depends on a range check, parser accept state, subgroup test, selector-legitimacy check, bigint formatting admission, or width-bounded comparator, the success condition for that check and the domain assumptions that give it semantic meaning should be forced immediately into the proved relation or encoded fail-closed inside the helper itself. This note exists to keep the positive design target visible instead of making readers reconstruct it only by inverting circom-pairing, Dark Forest, circom-ecdsa, and similar under-constrained-validator incidents.
  • Why this note exists:
    • Proof reviews often over-credit visible validation code. In ordinary software that instinct is usually directionally right; in constraint systems it is dangerously incomplete because a computed isValid bit that never reaches a hard equality is not yet security.
    • Many proof bugs are not wrong validator bugs. They are right validator, wrong statement bugs: the helper exists, the output is computed, and the surrounding proof still authenticates a weaker claim than the team thinks it does.
    • A second recurring mistake is to stop once the success bit is consumed. A helper output can be wired into the statement correctly and still be semantically weak if the circuit never proved the narrower width, range, or representation assumptions that make that output trustworthy.
    • The design habit worth preserving is simple and portable: if the protocol needs a validation result to move money or authority, reviewers should be able to point both to the exact constraint that makes that result part of the statement and to the exact constraints that make the helper’s domain assumptions true.

Fast classifier: which validator-output story are you trying to prevent?

  • helper exists, success bit never required — the circuit instantiates the correct validator and maybe even computes the correct answer, but no constraint ever forces success. Validation-output nonconsumption is the direct exploit-side family, and [[../incidents/proofs-verifiers/circom-pairing-coreverifypubkeyg1-biglessthan-output-omission-forged-signature-near-miss-2022-11-25|circom-pairing CoreVerifyPubkeyG1()]] is the clean exemplar.
  • several checks are computed, aggregate never bound — validation counters, conjunctions, or summary values are built, but the final all passed fact never becomes statement truth.
  • validator output enters a dead lane — the success bit is routed into an intermediate or branch that looks security-relevant in code review yet never constrains the live relation.
  • mandatory check exposed as optional API — helper design leaves it too easy for callers to instantiate safety-critical validators without consuming the result.
  • Use this note when the sharper design question is where exactly should every mandatory validator result become unavoidable proof statement truth?

What this note means by statement binding

  • Statement binding means a validation result is not merely computed somewhere inside the circuit graph; it is forced into the final proved claim that the verifier accepts.
  • The positive-design target is stronger than the helper looked correct in isolation. It is the live statement cannot be satisfied unless the validation succeeded.
  • The useful review question is concrete: if this validator returned 0, what exact equality, boolean conjunction, or fail-closed helper design would make proof generation or verification fail?

Three helper-validation questions reviewers should not collapse

  • Did the helper run at all?
    • This is the shallowest question: the range check, parser, subgroup test, LessThan(bits), or bigint helper is visibly instantiated.
    • circom-pairing-style bugs often fail even here in the practical sense that the helper existed, but the proof never had to care what it said.
  • Did the live statement require the helper’s success output?
    • This is the classic statement-binding question preserved by validation-output nonconsumption.
    • A computed ok = 0 living in a dead lane, summary variable, or unconstrained branch is still commentary, not proof truth.
  • Did the circuit also prove the helper’s hidden domain assumptions?
    • This is the adjacent question preserved by bit-length precondition omission: a consumed helper output can still be semantically weak if the circuit never proved the width, range, limb-canonicality, or representation assumptions that make that output meaningful.
    • Review should therefore stop neither at helper exists nor at success bit consumed; it should also ask whether the surrounding circuit proved the narrower preconditions under which the helper’s result deserves authority.

The six joints a healthy validator result should keep fused

1. Helper semantics

  • Reviewers should know whether a helper is advisory or mandatory.
  • If a validator returns out, ok, accepted, or lt, the helper API should make clear whether callers are expected to constrain that output themselves.
  • Security-critical validation helpers should bias toward fail-closed semantics whenever practical.

2. Call-site consumption

  • The safest shape is usually immediate local binding: instantiate validator, wire inputs, then constrain success on the next line.
  • Spreading validator here, assertion later across distant templates or layers makes omission bugs much easier to miss.
  • If a check is mandatory for soundness, out === 1 should feel structurally adjacent to the helper call.

3. Aggregate validation truth

  • When several validators jointly protect one invariant, the circuit still needs one explicit final constraint that proves the whole set passed.
  • sum, count, allValid, or acceptedState variables are only scaffolding until the statement actually requires the expected value.
  • A proof should not be able to carry a perfectly computed summary of failed checks while still satisfying the business logic.

4. Dead-lane elimination

  • Validator results should not be allowed to disappear into unused branches, unconstrained intermediates, or debug-only outputs.
  • Optimization, refactoring, and modularization are high-risk moments because they preserve the appearance of validation while quietly severing the last binding edge.
  • Healthy review treats every validator output like a value-moving authorization bit: if it can go dead, the proof may be proving the wrong thing.

5. Negative-proof regression

  • Validation consumption should be demonstrated with invalid inputs, not inferred from happy-path proofs.
  • For each validator family — range, parser, subgroup, selector, formatting — the suite should prove invalid input => proof failure, not merely invalid input => helper computes 0.
  • Regression corpora matter because statement-binding edges are easy to lose during performance work and template reuse.

6. Audit visibility

  • Auditors should be able to map every mandatory validator output to the exact enforcing constraint without mentally simulating the whole circuit.
  • A short reviewer-readable table from validator output to statement-binding edge is often more valuable than another page of gadget-level prose.
  • If the team cannot produce that map, omission bugs are probably still plausible.

What sound design looks like

  • Mandatory validators fail closed or are consumed immediately
    • If a range check, parser, or subgroup test is security-critical, the circuit either enforces it inside the helper or constrains the success output immediately at the call site.
  • The statement says what reviewers think it says
    • The proved claim should explicitly include the validation facts the protocol relies on, rather than merely containing code that appears to compute them.
  • Aggregates end in one hard truth
    • If multiple sub-checks matter jointly, one explicit final equality or conjunction proves they all passed.
  • Refactors preserve validator-to-statement edges
    • Modularization, inlining, and optimization cannot be allowed to turn live constraints into commentary.
  • Negative tests guard the binding boundary
    • The proof suite carries adversarial malformed-input cases that fail only if statement binding remains intact.

Useful positive design shapes

1. Fail-closed helper templates

  • The cleanest helper API for mandatory checks is often one that leaves no optional success bit to ignore.
  • If the only correct use of a validator is must pass, encode that obligation inside the helper or wrap it in a mandatory-check template.
  • This reduces review load and narrows the forgot to bind the output class directly.

2. Immediate assertion adjacency

  • When fail-closed helper design is not practical, keep the binding line physically adjacent to helper instantiation.
  • The design target is that a reviewer scanning locally can see both validator wired and validator required without chasing distant templates.
  • Adjacency is not just style; it is omission resistance.

3. Statement-binding ledgers for audits

  • Maintain a compact map of validator name -> output signal -> enforcing constraint -> hidden precondition constraints for every mandatory check family.
  • This is especially valuable in pairing, parser, comparator, bigint, and compositional circuits where many helpers can create the illusion of safety.
  • It also makes regression review after optimization tractable.

4. Precondition-carrying helper wrappers

  • Where helper correctness depends on bounded-width inputs, canonical limbs, or other domain assumptions, wrap the helper in a local primitive that proves those assumptions and consumes the success output as one joined object.
  • The healthy API shape is not remember to add the width proof somewhere else later; it is this checked helper is only constructible from well-formed inputs and already fails closed if the semantic preconditions do not hold.
  • This is the cleanest positive-design bridge between validation-output nonconsumption and bit-length-precondition omission.

5. Invalid-input proof corpora

  • Keep reusable negative vectors for malformed coordinates, out-of-range limbs, impossible parser states, illegal selectors, width-overflow witnesses, and other obviously invalid objects.
  • Run them after refactors and optimization passes, not just after initial implementation.
  • The right expectation is hard failure of proof generation or verification.

6. Aggregate-finalization patterns

  • If a circuit accumulates several validator results into one summary, the summary should terminate in one obvious final assertion.
  • We computed all the right bits is not yet meaningful until one constraint forces the all-pass outcome.
  • This is the positive-design answer to validation sum exists, but no one ever asked if it had to equal full success.

Design questions worth asking first

  • Which validator gadgets in this circuit produce outputs that callers must consume explicitly?
  • For each mandatory validator, where is the exact constraint that forces success rather than merely computing it?
  • What hidden width, range, or representation assumptions make each helper output meaningful, and where are those assumptions themselves proved?
  • Could malformed input still satisfy the rest of the circuit if one validator returned 0 or if the validator operated outside its intended domain?
  • Are several validation results being accumulated, and what final assertion proves the aggregate had to pass?
  • Did optimization, template extraction, or helper reuse move validator outputs farther away from their binding constraints or separate helper calls from their precondition proofs?
  • If a reviewer had to produce a one-page map from validator outputs to statement-binding edges and from helper preconditions to enforcing constraints, could they do it today?

Red flags that usually mean validation truth is still split

  • The validator is definitely there used as if visible instantiation were equivalent to statement enforcement
  • helpers named Check, IsValid, LessThan, accept, or belongsToField whose outputs do not obviously hit a hard equality
  • consumed validator outputs whose surrounding circuit still never proves the narrower width, range, or canonical-representation assumptions the helper documentation quietly relies on
  • validation outputs routed into intermediate variables, debug traces, or branch selectors with no final constraint proving the branch meaning mattered
  • comments that say ensure X or expects n-bit inputs while the actual relation never requires X or never proves the stated domain assumption
  • negative tests that inspect helper output values but never prove malformed or widened inputs fail to generate or verify proofs
  • performance or modularity changes merged without re-running malformed-input regression suites

Failure-prevention checklist

  • Inventory every validator gadget that returns a success bit, accept-state flag, comparison result, or validation summary, and classify whether each one is advisory or mandatory. Mandatory outputs must have a visible binding edge into the proved statement.
  • Prefer fail-closed helper APIs for mandatory checks. If callers should never be allowed to ignore a result, do not make ignore result the default or easiest integration path.
  • Inventory hidden helper preconditions too: width bounds, canonical-limb requirements, parser-domain assumptions, subgroup expectations, or representation-family constraints. If a helper is only meaningful on a narrower domain, that domain must be proved somewhere equally visible.
  • When helpers must return success bits, constrain those outputs immediately at the call site unless a nearby aggregate-finalization pattern makes the binding edge equally explicit.
  • Where possible, wrap mandatory helpers in local checked adapters that prove domain assumptions and consume success outputs as one joined object instead of relying on distant caller discipline.
  • Require one final hard assertion for every aggregate validator story: counters, conjunctions, accept-state summaries, or all-pass accumulators should end in one obvious equality that the statement cannot evade.
  • Maintain a reviewer-readable map from mandatory validator outputs to the exact enforcing constraints that consume them, plus the exact constraints that prove the helper’s domain assumptions, and update it after helper refactors, template extraction, or optimization work.
  • Add malformed-input regression vectors for each validator family and require proof generation or verification to fail under those vectors, not merely to compute 0 internally.
  • Re-run the negative corpus after every optimization pass, helper reuse change, or circuit modularization step. Statement-binding regressions are often introduced as performance or readability work.
  • Treat dead outputs and unproved domain assumptions as security findings, not cleanup nits. An unconsumed validation result or a consumed result operating outside its intended domain both mean the statement may already be proving less than the team believes.
  • Keep validator semantics and economic authority aligned. If a proof will move assets, authenticate identities, or release withdrawals, the validators guarding those meanings should be the easiest outputs and preconditions to trace into the final statement.
  • During audits, ask for the shortest explanation of why invalid input must fail here. If the answer depends on vibes, helper names, or code presence rather than one binding constraint plus one proved domain story, the design is not done.

Audit prompts

  • Which helpers in this circuit return outputs that are security-critical only if the caller consumes them correctly?
  • For each such output, what exact equality, boolean conjunction, or fail-closed helper semantics forces the intended success value?
  • What hidden width, range, subgroup, or representation assumptions make each helper output semantically meaningful, and where are those assumptions proved rather than merely documented?
  • Can malformed coordinates, parser states, selectors, widened comparator operands, or non-canonical bigint limbs still prove because the corresponding validator output is computed but unconstrained or because the helper ran outside its intended domain?
  • If validation outputs are aggregated, where is the final constraint that proves the aggregate had to equal full success rather than merely being calculated?
  • Did any helper refactor, optimization, or template boundary make validator outputs or their precondition proofs harder to trace into the live statement?
  • Are there comments, audit notes, or code structure cues that imply validation happened even though the statement never actually depends on the validator result or never proves the helper’s semantic domain?
  • Which negative tests prove invalid input => proof failure today for each mandatory validator family?
  • If one surprising proof landed in production, which validator outputs and hidden helper preconditions would you inspect first to confirm they still bind into the current statement rather than only into dead side lanes or folklore assumptions?
  • Could a reviewer unfamiliar with the circuit produce a map from each mandatory validator output to its consuming constraint and from each hidden helper precondition to its enforcing constraints without reverse-engineering the entire graph?
  • If the protocol claims a validation result protects economic authority, where exactly does that result and the domain assumptions beneath it become unavoidable in the same statement that unlocks that authority?

Lessons that should already be standard

  • In proof systems, computed is not enforced. A validator output is only security once the statement depends on it.
  • The right helper exists is a weak review fact. The stronger and necessary fact is the proof cannot succeed if that helper says fail.
  • Even the proof cannot succeed if that helper says fail is not always the whole story. A consumed helper output can still be semantically weak if the circuit never proved the narrower domain assumptions that make the helper trustworthy.
  • One missing equality on a validator output can be a full soundness bug, not a polish issue.
  • Modular, reusable helper libraries are valuable and dangerous at the same time: they improve local correctness while increasing the risk that call sites quietly stop binding the last security bit or silently lose the width/range proofs the helper expected upstream.
  • Negative malformed-input proofs are the natural test for this family. Happy-path proving is often compatible with a catastrophically weak statement.
  • Aggregate validation stories deserve the same suspicion as single missing checks. We summed everything still proves nothing until the sum is forced to mean all passed.
  • The clean mantra is short: if the protocol relies on the validation result, make that result and its semantic preconditions statement truth immediately and visibly.

Negative exemplar cluster: what no statement-binding discipline looks like

  • Validation-output nonconsumption preserves the exploit-side family where mandatory validator outputs existed but never became statement truth.
  • [[../incidents/proofs-verifiers/circom-pairing-coreverifypubkeyg1-biglessthan-output-omission-forged-signature-near-miss-2022-11-25|circom-pairing CoreVerifyPubkeyG1()]] preserves the clean modern example: BigLessThan validators were instantiated for BLS12-381 coordinate admission, yet none of their success bits were asserted, so malformed points could satisfy the surrounding signature relation.
  • The preserved common lesson is not merely range check missing. It is that the circuit visibly computed the intended admission result while proving a weaker statement that never required that result to hold.

How this note complements the exploit corpus

  • Start with validation-output-nonconsumption when the sharper exploit-side question is did the circuit instantiate the right validator but forget to consume its output?
  • Keep bit-length-precondition-omission nearby when the validator output was consumed but the surrounding circuit never proved the narrower width or representation assumptions that made that output meaningful.
  • Pair with proof-element-admission-boundary-discipline when the broader healthy-side question is where malformed proof-facing objects should die before arithmetic or authority starts.
  • Pair with proof-facing-field-domain-canonicalization-discipline when the sharper design issue is that caller-boundary and verifier-side domains already disagree before validator-output consumption even becomes the key seam.
  • Pair with proof-effect-truth-security-object when validation outputs are properly bound but the later settlement or consumer path may still honor a different economically relevant effect object.
  • Use this note when the healthy-side question is specifically what code and review discipline keeps mandatory validator results, and the hidden domain assumptions beneath them, fused to the live statement instead of leaving them as unconstrained commentary or folklore?

Internal linkages

Control surface

Graph View

Backlinks