feat(ssa): check purity contracts during SSA interpretation

[asterite]

Description

Problem

Purity analysis classifies every function as Pure, PureWithPredicate, or Impure, and LICM, DIE, and constant-folding deduplication act on those results — but nothing verified that a function's actual behavior matches its recorded purity. This contract has silently broken four times recently, each one a miscompilation or near-miss:

• a vector mutator hoisted by LICM out of its loop (fixed in fix: vector_push_front is PureWithPredicate #13445),
• a vector-mutator wrapper function classified predicate_pure and deduplicated,
• function purities lost while cloning functions (fixed in fix(ssa): store function purities on the Ssa so entry-point clones keep their purity #13493),
• Brillig functions calling a vector mutator on an array input considered pure (fix(ssa): mark Brillig functions calling a vector mutator on an array input as impure #13479, merged just days ago).

All of these were found late, by a fuzzer roll or corpus luck, because the existing oracle (pass_vs_prev differential testing) only fires on the consequence: a pass has to actually exploit the wrong purity and the divergence has to reach an output. For the LICM bug that meant aligning spare vector capacity, a specific loop shape, and no pre-loop use of the vector.

Summary

The SSA interpreter now enforces the purity contract on every interpreted call — firing on the precondition (recorded purity contradicts observed behavior) instead, deterministically, on any program that exercises the misclassified function:

• Pure and PureWithPredicate functions must not mutate caller-visible memory. On call entry the storage identities reachable from the arguments are captured (via a new Shared::as_ptr — Shared's PartialEq compares contents, not identity); every in-place write (store through a reference, mutable array_set, vector intrinsics writing through their input) and every global's storage is checked against the active scopes. Local allocations are in no scope's set, so local mutation passes freely, matching purity analysis' "local mutations are not impure" rule.
• Pure functions must not fail: execution failures escaping a Pure call (failed constraints, overflow, division by zero, out-of-bounds indexing, ...) are violations, since passes may deduplicate or remove such calls. Interpretation artifacts (step budget, missing oracles, malformed SSA) are excluded.
• Foreign calls are forbidden inside any function with a recorded non-Impure purity.
• Intrinsic mutation labels are validated (second commit): the interpreter's in-place vector mutation point requires the intrinsic to be listed in Intrinsic::mutates_array_operand_in_brillig. That list is an input to purity analysis, so an unlisted mutator poisons every containing function's recorded purity without any function-level contract observably breaking — exactly the LICM-bug shape, which the function-level checks alone cannot see.

Violations surface as InterpreterError::PurityViolation / IntrinsicPurityViolation, naming the offending function or intrinsic and its recorded contract. Purity is observed through the caller's runtime (DataFlowGraph::purity_of), matching what optimization passes see; when no purity analysis has run, the checks are skipped.

Value

The interpreter runs inside every assert_pass_does_not_affect_execution SSA pass unit test, nargo interpret (after every pass), and both fuzzers — so drift between purity analysis and actual behavior now fails loudly at every one of those points, with the cause named, instead of waiting for a pass to miscompile and a divergence to be bisected. Three of the four historical bugs above would have been caught directly at the misclassification stage (the wrapper bug, #13479, and the dangerous direction of the purity-cloning bug); the intrinsic-label check covers the remaining bare-intrinsic shape (the LICM bug).

Verification

• Red-green: the five violation tests failed before the implementation (wrong purities are injected via FunctionPurities, since the SSA parser validates hand-written annotations); the intrinsic-label wiring was verified end-to-end by temporarily unlisting VectorPushBack, which makes the existing in-place push test fail with IntrinsicPurityViolation.
• False-positive sweep, all clean: full noirc_evaluator suite (1968 tests), nargo_cli interpret test, AST fuzzer smoke test, and aztec-packages protocol circuits (private-kernel-inner, rollup-tx-base-private) under nargo interpret.
• Performance: interleaved release-build timing of nargo interpret --force on those circuits shows no measurable overhead (private-kernel-inner 10.06s → 10.10s; rollup-tx-base-private within noise in both directions).

🤖 Generated with Claude Code

[asterite]

CI diagnosis and fix (81cbae3):

All 21 test-partition violations were one flavor — predicate_pure functions flagged for an in-place array_set, always appearing right after the Mutable Array Set Optimizations pass. That pass marks an array_set mutable only when the old array value is dead, so in a constrained context the interpreter's in-place write just reuses that dead value's backing store under ACIR's value semantics. It is not a caller-visible mutation, and purity analysis rightly ignores it — the check was treating an implementation detail of the interpreter's array representation as an observable side effect. The mutation check is now scoped to Brillig frames, where the reference count governs genuine sharing and in-place writes through argument-reachable storage really are observable (the shape of the recent purity bugs this PR targets).

The cargo doc failure was an intra-doc link from the public IntrinsicPurityViolation docs to a pub(crate) item; now plain code formatting.

Verified locally: the new regression test (ACIR predicate_pure function doing array_set mut on its parameter, classified by the real analysis) fails against the unexempted check and passes now; all 3831 interpret_execution tests (the failing CI workload) pass, full noirc_evaluator suite passes, and cargo doc is clean with CI's flags.

🤖 Generated with Claude Code