Cross-Template Constraint Gap

Overview

The cross-template constraint gap detector finds places where one template’s output signal flows into another template’s input signal, but the wiring between them does not carry a constraint. Circom composes circuits out of template instances, and each instance exposes its inputs and outputs as signals. When those signals are connected with <-- instead of <==, or when the receiving input is assigned from an expression that the parent template never constrains, the R1CS inside each template remains valid while the edge between them is free.

The gap is subtle because every template in isolation looks correct. Template A constrains its own output, template B constrains its own input — each in terms of signals internal to itself. The value that actually crosses the boundary is a third signal declared in the parent, and the parent is the only place where the binding can be stated. If the parent uses an unconstrained assignment, the two internal constraint systems become disconnected: the prover can pick one value for A’s output in the witness and a different value for B’s input, as long as each half still satisfies its own R1CS.

Severity is High because gaps of this kind usually affect the circuit’s top-level security property: they sit on exactly the edges a reviewer trusts most.

Why This Is an Issue

Template composition is the primary abstraction mechanism in Circom. A hash is one template, a range check is another, a signature verification is a third; the main circuit wires them together. Reviewers and auditors read the main template as a data-flow diagram and assume that hash.out is the same value that verifier.msg will see. That assumption holds only when the wiring is constrained.

Under a broken wiring, the prover can:

• Feed a valid preimage into the hash template, then claim a different digest was passed to the verifier.
• Run a range check on one value and use a larger value in the subsequent arithmetic.
• Bypass a nullifier check entirely by decoupling the nullifier computed from the witness from the one submitted to the Merkle-membership component.

Because each sub-template still produces a satisfying assignment in isolation, the proof verifies and the defect is invisible on-chain.

How to Resolve

Use <== for every signal that moves between template instances. Reserve <-- for the narrow cases where a witness hint is followed, in the same scope, by an explicit === that re-binds the hint.

// Vulnerable: hash output wired with an unconstrained hint
template Main() {
    signal input preimage;
    signal input expected;
    component h = Poseidon(1);
    h.inputs[0] <== preimage;

    component v = Verifier();
    v.digest <-- h.out;        // gap: prover chooses any v.digest
    v.expected <== expected;
}

// Fixed: the inter-template edge carries a constraint
template Main() {
    signal input preimage;
    signal input expected;
    component h = Poseidon(1);
    h.inputs[0] <== preimage;

    component v = Verifier();
    v.digest <== h.out;        // R1CS edge: v.digest == h.out
    v.expected <== expected;
}

Examples

Sample Sigvex Output

{
  "detector": "cross-template-constraint-gap",
  "severity": "high",
  "confidence": 0.78,
  "title": "Broken constraint edge between `Poseidon` and `Verifier`",
  "template": "Main",
  "line": 15,
  "source_component": "h",
  "sink_component": "v",
  "description": "Output `h.out` flows into input `v.digest` via `<--`. The value crossing the template boundary is not fixed by any R1CS constraint in `Main`.",
  "recommendation": "Replace `<--` with `<==` so the inter-template edge is bound in the parent's R1CS."
}

Detection Methodology

The detector treats each parent template as a bipartite graph whose nodes are component ports (inputs and outputs of instantiated sub-templates) and whose edges are the assignments in the parent body. Each edge is labelled constrained (<==, or <-- followed by a matching ===) or unconstrained (bare <--, array writes through an unconstrained index, or assignments inside an unconstrained branch).

For every edge whose source is a sub-component output and whose sink is another sub-component input, the detector walks the parent’s constraint list to check whether the two ports are transitively equated. If no chain of constrained assignments exists between them, the edge is reported. Security-sensitive sub-templates (hash functions, comparators, bit decomposition, signature verifiers) are recognised by name and boost the finding’s confidence.

Limitations

• Wiring that passes through intermediate arithmetic in the parent (v.digest <-- h.out + 0) is normalised only for trivial identities; more elaborate laundering is not recognised.
• Detection is local to one parent template; a gap spread across three levels of nesting may be missed if each level looks locally constrained.
• Custom sub-templates whose names do not match known security primitives receive a lower confidence score even when the gap is real.

Related Detectors

• Under-Constrained Signal — signals that carry no constraint at all
• Unchecked Component — component instances whose ports are never read
• Template Misuse — templates applied outside their documented preconditions

References

• Circom Documentation: Templates and Components
• iden3/circomlib
• Pailoor, S., Wang, Y., Wang, X., Dillig, I. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IACR ePrint 2023/512.