Cowrie Research

helper-domain-proof-locality-and-output-canonicalization-discipline

14 min read

Helper-Domain Proof-Locality and Output Canonicalization Discipline

  • Name: helper-domain proof-locality and output canonicalization discipline
  • Category: zk-circuit reference / helper-gadget discipline / representation-safety checklist / statement-shaping design note
  • Summary: Healthy proof systems do not let helper-gadget safety live as folklore spread across distant call sites, comments, and reviewer memory. If a comparator only means anything for n-bit inputs, if a bigint helper only becomes semantically usable once quotient and remainder are both in proper representation, or if an index / nullifier derivation helper only stays one-to-one on a bounded domain, then those preconditions should be proved locally enough that reviewers can see the full semantic object in one place. This note exists to keep the positive design target explicit: helper domain assumptions, helper invocation, semantic-output canonicalization, and downstream consumption should stay one joined proof object rather than four facts the team hopes never drift apart.
  • Why this note exists:
    • Many zk bugs are not bad cryptography and not even bad helper bugs. They are good helper, split semantic boundary bugs: the helper was sound on its intended domain, but the surrounding circuit never proved that the witness object actually lived on that domain or that every helper output was canonical before the rest of the circuit treated it as money-good truth.
    • Reviewers often ask is the helper used? and is the output consumed? Those are necessary questions, but the persistent misses happen one step deeper: where exactly did we prove the helper's intended input/output object existed in the semantic form downstream code is about to trust?
    • The reusable healthy-side habit is to keep four things adjacent in code and in review: the domain promise, the helper call, the output canonicalization step, and the later authority or state transition that depends on the result.

Fast classifier: which helper-domain boundary is drifting apart?

  • helper input domain never became local proof truth — a comparator, range helper, or index gadget is called with values whose width or representation assumptions remain implicit. [[../incidents/proofs-verifiers/dark-forest-v0-3-rangeproof-lessthan-bit-length-precondition-omission-near-miss-2021-09-30|Dark Forest v0.3 RangeProof]] is the clean exemplar.
  • helper output relation proved, semantic output object never canonicalized — arithmetic equality or decomposition holds, but one output array or limb family is still wider or less canonical than downstream consumers assume. [[../incidents/proofs-verifiers/circom-ecdsa-bigmod-remainder-range-check-omission-noncanonical-remainder-near-miss-2022-03-30|circom-ecdsa BigMod]] is the clean exemplar.
  • helper semantics scattered across wrappers and callers — the low-level gadget is individually sound, but callers must remember invisible width, representation, or one-to-one mapping conditions at every reuse site.
  • helper output becomes authority before representation is sealed — nullifier derivation, note indexing, coordinate bounds, remainder reuse, or bigint comparison becomes trusted protocol truth before the helper’s semantic output object is fully canonicalized.
  • Use this note when the sharper design question is where should helper-domain assumptions and helper-output canonicalization become one local proof story rather than a repo-wide memory test?

What this note means by proof-locality

  • Proof-locality means reviewers can find the helper’s semantic preconditions and the constraints that discharge them close enough to the helper call that the meaning of the helper result is visible without reconstructing half the circuit from memory.
  • The design target is not literally every constraint must be on the next line, but it is stronger than somewhere upstream we probably bounded that already.
  • The useful claim is: at the place this helper output first starts to matter, the circuit has already proved the helper's live input object and already sealed the helper's live output object into the representation downstream code intends to consume.

Three helper-boundary promotions healthy designs keep separate

  1. A helper-shaped object exists at all

    • A comparator ran, a bigint helper produced outputs, an index was encoded, or an algebraic relation held for some witness values.
    • This is only the existence question: some helper-valid-looking object showed up.

  2. That object already counts as the canonical semantic object downstream code means to trust

    • The circuit treats the helper input or output as if width, representation, canonicalization, and one-to-one mapping have already all been proved tightly enough for later code to consume it as protocol truth.
    • This is the semantic-promotion question: the helper-shaped object is already the bounded, canonical object the protocol meant to talk about.

  3. That accepted semantic object already deserves authority

    • The now-accepted object is allowed to drive nullifier uniqueness, bounds truth, settlement, release, or some other economically meaningful branch.
    • This is the authority question: why was this accepted helper-boundary object allowed to matter this much here and now?

The four joints a healthy helper boundary should keep fused

1. Domain admission

  • If a helper only makes sense for n-bit values, proper limbs, bounded indices, or signed values inside one window, the circuit should make that admission rule explicit before or at the helper boundary.
  • This helper usually gets n-bit inputs is not a proof obligation discharged; it is a review warning.
  • The positive-design question is where does this witness stop being a raw field element and become a helper-valid semantic object?

2. Helper invocation

  • The helper should be called on the admitted object, not on a looser pre-image that later code merely hopes was already normalized.
  • This is where call-site wrappers matter. The safest API is often one where the helper cannot be invoked except on an already-bounded or already-canonical object.
  • If the call site still accepts raw witness material, the helper boundary is already wider than reviewers think.

3. Output canonicalization

  • A helper result that satisfies an algebraic relation is not always the same thing as a helper result that is semantically reusable downstream.
  • Quotients, remainders, limb arrays, indices, comparator operands after shifting, and other structured outputs often need their own width or representation sealing step.
  • The positive-design target is helper returned a semantic output object rather than merely helper returned values that make one equality hold.

4. Authority consumption

  • Once a helper result becomes a nullifier input, spend gate, state-transition proof, coordinate admission, or payout unlock, the semantic object should already be sealed.
  • The recurring mistake is to let the circuit spend against helper-shaped arithmetic witness while reviewers think it is already spending against canonical semantic object.
  • Healthy designs do not promote helper output into authority until the representation story is finished.

What sound design looks like

  • The three promotions stay explicit
    • Healthy designs keep helper-shaped object exists, helper-shaped object became canonical semantic truth, and canonical object gained authority as separate review gates instead of one mushy helper seems fine conclusion.
  • Helper preconditions are discharged where helper trust begins
    • Reviewers can point to the exact width, range, or representation constraints that make the helper invocation meaningful without searching distant templates or comments.
  • Checked wrapper shapes dominate raw helper reuse
    • The safer API shape is CanonicalBigMod, BoundedLessThan, or CheckedIndexDomain rather than remember to add the missing proofs around a raw helper later.
  • Output objects are canonical before reuse
    • A quotient / remainder pair, shifted comparator operand, or derived index is not treated as reusable semantic state until each downstream-relevant output object is in the representation family later gadgets expect.
  • Helper semantics survive refactors
    • Template extraction, optimization, and library swaps do not push domain admission farther away from helper use or quietly drop output-canonicalization steps from one sibling output family.
  • Authority only spends canonical objects
    • Replay protection, bounds checks, note consumption, and state updates depend on already-sealed helper outputs, not on raw arithmetic witnesses that merely looked close enough under honest use.

Useful positive design shapes

1. Admitted-object wrappers

  • Create local wrapper templates or helper layers whose constructor boundary proves the object’s width or representation once.
  • Then pass the admitted object, not raw witness elements, into the lower-level helper.
  • This is the clean answer to LessThan(bits)-style folklore dependencies.

2. Symmetric output sealing

  • When a helper returns multiple semantically meaningful outputs, canonicalize them symmetrically unless the design can explain why only one output will ever matter.
  • Quotient bounded, remainder informal is usually not a coherent semantic contract.
  • The same review habit applies to carries, borrows, indices, decomposition limbs, and other sibling arrays.

3. Semantic output types, not just algebraic outputs

  • Distinguish field elements satisfying relation from proper remainder, bounded index, field-safe nullifier input, or in-range shifted coordinate.
  • Even when the host DSL cannot express rich types directly, the review artifacts and wrapper structure should.
  • This makes later authority consumption easier to audit because the circuit no longer silently upgrades one into the other.

4. Local negative-boundary corpora

  • Keep adversarial tests at the helper boundary itself: widened operands, non-canonical limbs, alternate encodings, and x + 2^n variants should fail before the rest of the application logic gets a chance to reuse them.
  • This is stronger than application-only negative tests because it proves the semantic object was already dead before business logic began.

5. Refactor-resistant boundary maps

  • Maintain a reviewer-readable map from helper call to domain proof to output-canonicalization step to later authority use.
  • This matters because helper-boundary regressions often arrive as cleanup or optimization work rather than as feature work.
  • If the team cannot redraw the boundary map after a refactor, the semantic story is probably already weaker than before.

Design questions worth asking first

  • What exact semantic object does this helper assume at its input boundary?
  • Where is that assumption proved close enough to the helper call that a reviewer can verify it without reconstructing a hidden proof path?
  • Which helper outputs are later treated as semantic objects rather than transient arithmetic scaffolding?
  • For each such output, where is canonical representation, width, or one-to-one mapping actually sealed before reuse?
  • Could one semantic object still reach the helper under multiple witness encodings because admission happened too late or too loosely?
  • If a refactor split input-domain admission, helper invocation, and output canonicalization across different templates, what evidence says the joined semantic story still holds?
  • Where does helper output first become authority — replay protection, bounds truth, state transition validity, or spend permission — and was canonicalization complete before that point?

Red flags that usually mean helper semantics are still folklore

  • helper docs say expects n-bit inputs or proper representation but the call site still consumes raw witness material without one nearby admission proof
  • one output of a decomposition helper is width-checked while a sibling output is left informal even though both later affect protocol meaning
  • range- and comparison-style helpers used under names like RangeProof even though the actual width proof lives only in reviewer intuition
  • comments that say this remainder is canonical or this index is safe without one visible constraint family proving it
  • helper wrappers whose safe use requires each caller to remember hidden preconditions manually
  • tests that show honest proofs succeed but never probe non-canonical or widened helper-boundary objects directly
  • optimization or modularization work that preserved algebraic equalities while quietly moving or deleting representation-sealing constraints

Failure-prevention checklist

  • For every helper with domain assumptions, write down the semantic input object it expects and the exact constraints that prove that object before the helper result can matter.
  • Write design and review notes in promotion order: helper-shaped object exists, canonical semantic object exists, canonical object gets authority. That keeps helper-boundary discussions from stopping at satisfiability.
  • Prefer project-local checked wrappers around raw comparators, bigint helpers, and index gadgets so unsafe-by-default helper reuse is not the easiest path.
  • Canonicalize every semantically reused output of a helper, not merely the output currently featured in the most obvious equality.
  • Keep domain admission and helper invocation review-local. If they must live in different templates, maintain an explicit trace showing the admission proof still dominates the helper call on every path.
  • Add adversarial tests at the helper boundary for widened operands, non-canonical limbs, alternate encodings, and boundary-overflow variants; require proof failure before business logic consumes the result.
  • Review refactors for semantic drift, not only algebraic drift. If a code change preserves satisfiability but weakens input admission or output canonicalization, treat it as a security regression.
  • When helper output feeds replay prevention or one-time-right consumption, prove one semantic object has one admitted encoding before hashing or indexing it.
  • Require symmetric review of sibling outputs like quotient/remainder, carry/borrow, index/path, or shifted value/bound pairs; asymmetry is a standing smell.
  • Keep a short helper-boundary risk inventory in zk-heavy repos naming the gadgets whose semantics depend on hidden domain assumptions so audits start from the real suspicion magnets.
  • Before shipping, ask the blunt question: what exact canonical object are we spending against here, and where did it become canonical?

Audit prompts

  • What does this helper promise semantically beyond the bare algebraic relation, and where is that stronger promise proved?
  • Am I collapsing helper-shaped object exists into canonical semantic object exists anywhere just because the local algebra already looks right?
  • Could the same logical input reach this helper under two witness encodings because width or representation admission happens too late?
  • Which helper outputs later influence protocol meaning, and are all of them sealed into the representation family downstream code assumes?
  • If one output array lost its range checks tomorrow but the top-level equation still held, what concrete test would fail?
  • Are reviewers expected to remember hidden call-site obligations from library docs, or can they see the admission proof and output sealing near the helper boundary itself?
  • Does any authority path consume helper output while it is still merely an arithmetic witness rather than a canonical semantic object?
  • During template extraction or optimization, what preserved evidence shows helper-domain proofs still dominate every live call site?
  • If the protocol says out-of-range inputs are impossible or remainders are canonical, what exact negative tests prove those claims at the helper boundary rather than only at the application boundary?
  • Where is the shortest code path from raw witness material to spendable / authoritative helper output, and which constraints along that path prove the semantic upgrade is deserved?

Lessons that should already be standard

  • Good helper libraries do not remove the need to prove the helper’s semantic domain. They concentrate the risk where that proof is forgotten.
  • A helper ran is not the same claim as a canonical semantic object exists, and that is not the same claim as that object deserves authority.
  • Algebraic correctness and semantic-output correctness are different claims. Many zk bugs arise when a team proves the first and quietly assumes the second.
  • One sibling output is checked is not a meaningful safety story when the other sibling output still carries protocol meaning.
  • The right place to kill malformed-width or non-canonical helper objects is the helper boundary, not deep in later business logic.
  • Refactors that preserve equations can still break semantics. In proof systems, representation and domain proofs are part of the product, not implementation detail.
  • The clean design mantra is short: admit one helper-valid object, call the helper on that object, seal every semantically relevant output, and only then spend authority against it.

Negative exemplar cluster: what no helper-domain proof-locality looks like

  • [[../incidents/proofs-verifiers/dark-forest-v0-3-rangeproof-lessthan-bit-length-precondition-omission-near-miss-2021-09-30|Dark Forest v0.3 RangeProof]] preserves the comparator-side version: the helper output was consumed, but the compared object never became a locally proved bounded-width input.
  • [[../incidents/proofs-verifiers/circom-ecdsa-bigmod-remainder-range-check-omission-noncanonical-remainder-near-miss-2022-03-30|circom-ecdsa BigMod]] preserves the output-side version: the modulo relation held, but one semantically reused output object never became canonical.
  • bit-length-precondition-omission preserves the exploit-family framing that connects comparator-width, bigint-output, and bounded-index variants.
  • The preserved common lesson is not merely missing range checks. It is helper-domain truth and helper-output truth were split across too many places to remain reliable under adversarial witnesses.

How this note complements the exploit corpus

Internal linkages

Control surface

Graph View

Backlinks