Noir Circuit Detectors

Overview

Noir differs from Circom in two ways that matter for soundness tooling. First, it has an explicit unconstrained keyword: functions annotated with it run only during witness generation and emit no ACIR constraints. Second, it has oracles — external functions that return values from the prover’s environment at witness time, again without constraints. Both mechanisms are intended as hints that the rest of the circuit re-derives through assert statements. When that re-derivation is missing or incomplete, the caller inherits prover-controlled data without knowing it.

The Noir detector family groups several related checks under one umbrella. Each one targets a different way of accidentally trusting an unconstrained value:

• Unconstrained return used in constrained context — a value produced by unconstrained fn flows into a Field used by main without an assert that rebinds it.
• Missing assert after oracle — an oracle result is used in arithmetic or control flow without any verification.
• Assert on mutable state modified by unconstrained code — an assert depends on a variable that an unconstrained helper updates between the assignment and the check.
• Brillig escape — a value computed in Brillig (Noir’s unconstrained VM) is returned to ACIR without entering the constraint system.
• Oracle value consumed without range validation — an oracle result is used as an array index, counter, or bit-width parameter without a bound.

Why This Is an Issue

Noir’s ergonomics encourage authors to treat unconstrained as an optimisation: “this computation is too expensive to express as constraints, so I’ll hint it and assert the cheap half”. The trap is that the assertion has to exist and has to be strong enough to rebind the hint. In practice, authors write let x = unconstrained_helper(input); and then use x directly, confident that because unconstrained_helper looks pure, its result must be trustworthy. It is not: the prover supplies whatever x they want, and main signs off on it.

Oracles are worse because the value does not even originate from user code. An oracle can return arbitrary data, and the only thing the verifier sees is the asserts the author wrote around the return value. A missing assert here is indistinguishable from “the prover claims this oracle said 42”.

How to Resolve

Treat every unconstrained return and every oracle result as untrusted data. Follow the assignment with assert calls that recompute the property you care about using only constrained inputs.

// Vulnerable: the root is trusted without verification
unconstrained fn sqrt_hint(x: Field) -> Field { /* witness-only */ }

fn main(x: pub Field) {
    let root = sqrt_hint(x);
    // BUG: nothing ties `root` to `x`.
}

// Fixed: the unconstrained hint is rebound by a constrained assert
unconstrained fn sqrt_hint(x: Field) -> Field { /* witness-only */ }

fn main(x: pub Field) {
    let root = sqrt_hint(x);
    assert(root * root == x);          // re-derives the property in ACIR
}

For oracles, the same rule applies: every oracle return must appear on the left-hand side of at least one assert that the verifier can check.

Examples

Sample Sigvex Output

{
  "detector": "noir-missing-assert-after-oracle",
  "severity": "critical",
  "confidence": 0.85,
  "title": "Oracle result `price` used without an `assert`",
  "function": "process_transfer",
  "line": 8,
  "value": "price",
  "description": "Return value of oracle call at line 8 is used at line 12 in `amount * price` without any `assert` in between. The prover controls `price`.",
  "recommendation": "Add an `assert` that ties `price` to a verifier-visible commitment (for example, a Pedersen hash of the oracle response against a public root)."
}

Detection Methodology

The Noir front-end is parsed into a typed AST on which the detector runs several dataflow passes. Sources are every unconstrained fn return and every oracle call; sinks are the arguments to constrained operations, including arithmetic in main, the condition of an assert, array indices, and arguments to other constrained functions. A taint flow from a source to a sink without an intervening assert that binds the sink back to constrained inputs produces a finding.

For the assert-on-mutable-state variant the detector tracks writes to each local variable inside unconstrained blocks and checks whether any subsequent assert reads a variable that was modified without re-reading a constrained quantity. The Brillig-escape variant operates at the IR level, checking whether values produced by Brillig opcodes reach ACIR without passing through a constraint-emitting instruction.

Limitations

• The detector does not model oracle semantics; any oracle that internally verifies its own output (rare) is still reported.
• Asserts written in helper functions are recognised only when the helper is inlined or marked with a known attribute; deeply nested helpers may cause false positives.
• Taint tracking through generic functions uses a conservative summary, which occasionally reports a finding on monomorphisations where the concrete type makes the flow safe.

Related Detectors

• Under-Constrained Signal — the Circom analogue
• Nondeterministic Witness — nondeterministic hints in Circom
• Unchecked Component — disconnected sub-circuits

References

• Noir Documentation
• Noir: Unconstrained Functions
• Noir: Oracles
• noir-lang/noir on GitHub