(proposal): preserve freshness-scoped polynomial auxiliaries before storage materialization

[1sgtpepper]

Summary

This proposal is the longer-term architecture behind #542.

The core design rule is:

Polynomial lowering should introduce compiler-generated existential SSA auxiliaries with an explicit dynamic freshness domain. It should not immediately materialize those auxiliaries as struct.member storage.

A later materialization layer should decide how each auxiliary is represented for a particular target: scalar component member, backend-private signal, static unrolled member, array element, column/trace cell, product-program value, deterministic witgen value, or diagnostic rejection.

The intent is not to make #542 wait for a large rewrite. The immediate #542 fix can be a conservative rejection in the current scalar-member path. This proposal explains the architecture that keeps that fix from becoming a chain of special cases.

Motivation

Polynomial lowering is an existential-introduction transform.

At the algebraic level, it changes:

P[E]

into:

exists a. (a = E) and P[a]

That is only sound when the scope of exists a matches the dynamic execution of E.

For a component-invariant expression, this may be sound:

exists a_component.
  a_component = E
  and P[a_component]

For an expression that depends on a loop-carried value, the required meaning is different:

forall i.
  exists a_i.
    a_i = E(i)
    and P_i[a_i]

The unsound form is:

exists a_component.
  forall i.
    a_component = E(i)
    and P_i[a_component]

That form adds constraints not present in the source program unless E(i) is proven identical for every iteration.

#542 demonstrates this exact failure. A loop-local expression depending on an scf.for loop-carried region argument is lowered to one component-scope auxiliary member. The source constraint is tautological, but the lowered constraints can require the same generated member to equal different per-iteration values.

Concrete current behavior

The current pass contract already points to the semantic mismatch. The pass documentation says polynomial lowering rewrites constraints into an observationally equivalent bounded-degree system, but also says high-degree subexpressions are factored into auxiliary struct members:

llzk-lib/include/llzk/Transforms/LLZKTransformationPasses.td

Lines 66 to 79 in aced31c

	def PolyLoweringPass : LLZKPass<"llzk-poly-lowering-pass"> {
	let summary =
	"Lower the degree of all polynomial equations to a specified maximum";
	let description = [{
	Rewrites constraint expressions into an (observationally) equivalent system where the degree of
	every polynomial is less than or equal to the specified maximum.
	High-degree subexpressions are factored into auxiliary struct members. The pass also recurses
	through degree-neutral roots such as `felt.add`, `felt.sub`, and `felt.neg`, so composite
	equality operands and struct constrain call arguments satisfy their degree bounds.
	This pass is best used as part of the `-llzk-full-poly-lowering` pipeline, which includes
	additional cleanup passes to ensure correctness and optimal performance.
	}];

The implementation creates auxiliary struct.members during expression factoring:

llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

Lines 178 to 224 in aced31c

	// Optimization: If lhs == rhs, factor it only once
	if (lhs == rhs && eraseMul) {
	std::string auxName = AUXILIARY_MEMBER_PREFIX + std::to_string(this->auxCounter++);
	MemberDefOp auxMember = addAuxMember(structDef, auxName);
	auto auxVal = builder.create<MemberReadOp>(
	lhs.getLoc(), lhs.getType(), selfVal, auxMember.getNameAttr()
	);
	auxAssignments.push_back({auxName, lhs});
	Location loc = builder.getFusedLoc({auxVal.getLoc(), lhs.getLoc()});
	auto eqOp = builder.create<EmitEqualityOp>(loc, auxVal, lhs);
	// Memoize auxVal as degree 1
	degreeMemo[auxVal] = 1;
	rewrites[lhs] = auxVal;
	rewrites[rhs] = auxVal;
	// Now selectively replace subsequent uses of lhs with auxVal
	replaceSubsequentUsesWith(lhs, auxVal, eqOp);
	// Update lhs and rhs to use auxVal
	lhs = auxVal;
	rhs = auxVal;
	lhsDeg = rhsDeg = 1;
	}
	// While their product exceeds maxDegree, factor out one side
	while (lhsDeg + rhsDeg > maxDegree) {
	Value &toFactor = (lhsDeg >= rhsDeg) ? lhs : rhs;
	// Create auxiliary member for toFactor
	std::string auxName = AUXILIARY_MEMBER_PREFIX + std::to_string(this->auxCounter++);
	MemberDefOp auxMember = addAuxMember(structDef, auxName);
	// Read back as MemberReadOp (new SSA value)
	auto auxVal = builder.create<MemberReadOp>(
	toFactor.getLoc(), toFactor.getType(), selfVal, auxMember.getNameAttr()
	);
	// Emit constraint: auxVal == toFactor
	Location loc = builder.getFusedLoc({auxVal.getLoc(), toFactor.getLoc()});
	auto eqOp = builder.create<EmitEqualityOp>(loc, auxVal, toFactor);
	auxAssignments.push_back({auxName, toFactor});
	// Update memoization
	rewrites[toFactor] = auxVal;
	degreeMemo[auxVal] = 1; // stays same
	// replace the term with auxVal.
	replaceSubsequentUsesWith(toFactor, auxVal, eqOp);

It also creates auxiliary members for nonlinear struct constrain call arguments:

llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

Lines 253 to 278 in aced31c

	Value materializeCallArgument(
	Value val, StructDefOp structDef, FuncDefOp constrainFunc, CallOp callOp,
	DenseMap<Value, unsigned> &degreeMemo, DenseMap<Value, Value> &rewrites,
	SmallVector<AuxAssignment> &auxAssignments
	) {
	Value loweredVal =
	lowerExpression(val, structDef, constrainFunc, degreeMemo, rewrites, auxAssignments);
	DenseMap<Value, unsigned> checkMemo;
	if (getDegree(loweredVal, checkMemo) <= 1) {
	return loweredVal;
	}
	// Callees only receive SSA values, not the caller expression tree, so nonlinear
	// call arguments must be represented by an auxiliary member read.
	std::string auxName = AUXILIARY_MEMBER_PREFIX + std::to_string(this->auxCounter++);
	MemberDefOp auxMember = addAuxMember(structDef, auxName);
	OpBuilder builder(callOp);
	Value selfVal = constrainFunc.getSelfValueFromConstrain();
	auto auxVal = builder.create<MemberReadOp>(
	loweredVal.getLoc(), loweredVal.getType(), selfVal, auxMember.getNameAttr()
	);
	Location loc = builder.getFusedLoc({auxVal.getLoc(), loweredVal.getLoc()});
	builder.create<EmitEqualityOp>(loc, auxVal, loweredVal);
	auxAssignments.push_back({auxName, loweredVal});

llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

Lines 420 to 438 in aced31c

	DenseMap<Value, unsigned> callMemo;
	unsigned deg = getDegree(arg, callMemo);
	if (deg > 1) {
	arg = materializeCallArgument(
	arg, structDef, constrainFunc, callOp, degreeMemo, rewrites, auxAssignments
	);
	modified = true;
	}
	}
	if (modified) {
	OpBuilder builder(callOp);
	builder.create<CallOp>(
	callOp.getLoc(), callOp.getResultTypes(), callOp.getCallee(),
	CallOp::toVectorOfValueRange(callOp.getMapOperands()), callOp.getNumDimsPerMap(),
	newOperands
	);
	callOp->erase();

The pass records each auxiliary as an auxiliary member name plus the value to compute:

llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

Lines 51 to 54 in aced31c

	struct AuxAssignment {
	std::string auxMemberName;
	Value computedValue;
	};

At the end, it rebuilds the recorded expression in @compute and emits a struct.writem:

llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

Lines 453 to 464 in aced31c

	DenseMap<Value, Value> rebuildMemo;
	Block &computeBlock = computeFunc.getBody().front();
	OpBuilder builder(&computeBlock, computeBlock.getTerminator()->getIterator());
	Value selfVal = computeFunc.getSelfValueFromCompute();
	for (const auto &assign : auxAssignments) {
	Value rebuiltExpr =
	rebuildExprInCompute(assign.computedValue, computeFunc, builder, rebuildMemo);
	builder.create<MemberWriteOp>(
	assign.computedValue.getLoc(), selfVal, builder.getStringAttr(assign.auxMemberName),
	rebuiltExpr
	);

That means polynomial lowering currently makes three decisions at once:

1. which algebraic expression should be factored;
2. what freshness domain the generated existential should have;
3. how the generated value is stored and computed.

The bug comes from coupling those decisions too early.

Why loop-carried values make this unsound

MLIR scf.for body arguments are dynamic values for the current loop iteration. The induction variable is the first region argument, followed by one region argument per loop-carried variable:
https://mlir.llvm.org/docs/Dialects/SCFDialect/

So in #542, %acc is not merely “some degree-one felt value.” It is the loop-carried value for the current dynamic iteration.

An expression like:

%sq = felt.mul %acc, %acc : !felt.type, !felt.type

has per-iteration freshness when %acc changes per iteration.

A single component member has component-instance lifetime. It does not distinguish loop iterations. Therefore, using one generated member for %sq changes:

forall i. exists aux_i

into:

exists aux. forall i

That is the semantic break.

Why compute rebuilding is not the architectural fix

rebuildExprInCompute currently maps a BlockArgument by ordinal position into the compute function:

llzk-lib/lib/Transforms/LLZKLoweringUtils.cpp

Lines 29 to 40 in aced31c

	Value rebuildExprInCompute(
	Value val, FuncDefOp computeFunc, OpBuilder &builder, DenseMap<Value, Value> &memo
	) {
	if (auto it = memo.find(val); it != memo.end()) {
	return it->second;
	}
	if (auto barg = llvm::dyn_cast<BlockArgument>(val)) {
	unsigned index = barg.getArgNumber();
	Value mapped = computeFunc.getArgument(index - 1);
	return memo[val] = mapped;
	}

That is valid only for a narrow class of entry-block argument correspondences. It is not valid for nested region arguments such as:

• scf.for induction variables;
• scf.for loop-carried body arguments;
• branch block arguments;
• values derived from nested region-local values.

Making this helper smarter may fix some cases, but it does not solve the core issue. The core issue is that polynomial lowering should not assume that every generated existential can be represented as one component-lifetime member written in @compute.

Why use replacement must be dominance-aware

The current use-replacement helper is based on same-block order:

llzk-lib/lib/Transforms/LLZKLoweringUtils.cpp

Lines 102 to 118 in aced31c

	void replaceSubsequentUsesWith(Value oldVal, Value newVal, Operation *afterOp) {
	assert(afterOp && "afterOp must be a valid Operation*");
	for (auto &use : llvm::make_early_inc_range(oldVal.getUses())) {
	Operation *user = use.getOwner();
	// Skip uses that are:
	// - Before afterOp in the same block.
	// - Inside afterOp itself.
	if ((user->getBlock() == afterOp->getBlock()) &&
	(user == afterOp || user->isBeforeInBlock(afterOp))) {
	continue;
	}
	// Replace this use of oldVal with newVal.
	use.set(newVal);
	}

That is not enough for region-aware SSA rewriting.

MLIR values are governed by dominance, nested region scope, and hierarchical visibility:
https://mlir.llvm.org/docs/LangRef/

A replacement is valid only if the replacement value dominates the use and is visible from that use. Same-block textual ordering is a useful local fact, but it is not the semantic rule.

Core design rule

A polynomial auxiliary and a component member are different abstractions.

A polynomial auxiliary is:

an existential value with a required dynamic freshness domain

A component member is:

storage with component-instance lifetime

The compiler should preserve that distinction.

Poly lowering may introduce the auxiliary. A materialization pass may choose storage. Storage may be chosen only after proving it preserves the required freshness domain.

Required invariant

For every generated auxiliary A replacing expression E:

1. A must be fresh over a required dynamic domain D_required.
2. D_required must be at least as fine as every dynamic dependency of E.
3. Every replacement use of E by A must be dominated by A.
4. Every replacement use must remain inside a region where A is visible.
5. Chosen storage must have a domain D_storage equal to or finer than D_required.
6. Coarser storage is allowed only with an explicit proof that all dynamic instances are value-identical and that sharing does not add source-invisible constraints.
7. If no available representation is sound, compilation must fail with a diagnostic.

In short:

Never lower a fresh existential auxiliary directly to a component field.
First preserve freshness.
Then materialize only after proving the storage is sound.

Proposed architecture

Use three responsibilities that are currently mixed together.

1. PolyLoweringCore

This layer performs algebraic degree lowering only.

It should:

• compute polynomial degree;
• factor high-degree subexpressions;
• introduce compiler-generated existential SSA auxiliaries;
• emit equality constraints tying each auxiliary to the expression it replaces;
• replace only dominance-valid uses;
• preserve MLIR region validity;
• preserve the auxiliary's dynamic freshness.

It should not:

• add struct.member declarations;
• emit struct.writem operations in @compute;
• rebuild @constrain expressions in @compute;
• decide whether an auxiliary is a component member, backend signal, array cell, column cell, or public witness output;
• map nested BlockArguments to compute arguments by ordinal position.

A semantic lowering could look like:

%aux = llzk.aux : !felt.type
constrain.eq %aux, %expr : !felt.type

If %expr depends on the current loop iteration, %aux must be placed inside that loop body unless a separate pass proves hoisting is semantics-preserving.

2. AuxFreshnessAnalysis / AuxScopeAnalysis

This layer computes the minimum freshness domain required by each generated auxiliary.

It should classify dependencies on:

• scf.for induction variables;
• scf.for loop-carried region arguments;
• values derived from loop-local values;
• nested loop iteration vectors;
• branch-local values;
• dynamic array indices;
• dynamic member/table offsets;
• affine map operands;
• function calls without sufficient summaries;
• unknown region or control-flow constructs.

This must be dependency-based, not purely location-based.

Examples:

• An expression syntactically inside a loop may still be component-invariant.
• An expression with degree one may still be dynamically scoped because it depends on a loop IV, offset, affine operand, or branch-local value.
• A struct member read may be component-lifetime for one member path, but dynamic for another if table offsets or affine operands are dynamic.

3. AuxMaterialization

This layer chooses concrete representation.

Possible materialization targets include:

• private scalar component member;
• backend-private R1CS signal;
• one scalar member per statically unrolled dynamic instance;
• array cell;
• column/trace cell;
• product-program value;
• deterministic witgen computation;
• rejection diagnostic.

Every materializer must prove:

1. Domain soundness: storage granularity is equal to or finer than required freshness.
2. Constraint preservation: replacing the semantic auxiliary does not add or remove constraints.
3. Witness consistency: deterministic targets can compute the value in the same dynamic domain.
4. Visibility correctness: generated private auxiliaries do not become public outputs.
5. Backend legality: the resulting IR is legal for the selected pipeline.

Freshness domains

Freshness should be modeled as a partial order, not as a single boolean.

Useful dynamic axes include:

• component invocation;
• function call instance;
• loop iteration;
• nested loop iteration vector;
• branch execution;
• while iteration;
• dynamic table/trace row;
• unknown or unsupported dynamic execution.

Storage is sound when:

D_storage >= D_required

where >= means “equal or finer dynamic granularity.”

Examples:

component member        < loop iteration
outer loop iteration    < nested loop iteration vector
branch execution        incomparable with unrelated loop iteration
unknown                 unsupported unless proven by a target-specific analysis

For #542:

%sq depends on %acc
%acc is an scf.for loop-carried region argument
therefore %sq requires per-iteration freshness

one scalar struct.member has component-invocation freshness
component-invocation freshness is coarser than per-iteration freshness
therefore scalar component-member materialization is unsound

Compatibility scalar materialization

The current scalar-member representation can remain as a compatibility materializer. It just should not be the semantic representation of polynomial auxiliaries.

A scalar component member is valid only if all of these are proven:

1. The required freshness domain is component invocation, or all dynamic instances are value-identical.
2. The expression can be rebuilt in @compute.
3. The rebuild uses the same semantic inputs: arguments, member paths, constants, affine operands, offsets, and dynamic dependencies.
4. The generated member is written exactly once per component invocation, unless the target explicitly supports another write model.
5. The generated member is private.
6. The generated type is supported, initially !felt.type.

This compatibility path should reject #542.

A good diagnostic would be:

error: cannot materialize polynomial auxiliary as one scalar component member
note: factored expression depends on scf.for loop-carried region argument %acc
note: scalar struct.member storage has component-invocation freshness
note: required freshness domain is per dynamic iteration of this scf.for
note: use semantic llzk.aux lowering, static unrolling, product materialization,
      or an R1CS-private per-iteration auxiliary materializer

Why not reuse llzk.nondet

llzk.nondet is close, but it is not the right abstraction for generated polynomial auxiliaries.

The current op is documented as producing a nondeterministic SSA value and is marked AlwaysSpeculatable:

llzk-lib/include/llzk/Dialect/LLZK/IR/Ops.td

Lines 28 to 53 in aced31c

	def LLZK_NonDetOp
	: LLZKDialectOp<"nondet", [AlwaysSpeculatable,
	DeclareOpInterfaceMethods<
	OpAsmOpInterface, ["getAsmResultNames"]>]> {
	let summary = "uninitialized variable";
	let description = [{
	This operation produces an SSA variable of the specified type but with
	nondeterministic value.
	This op can be used in `@constrain()` functions in place of expressions that
	cannot be included in constraints. It may also be generated for a frontend
	language that supports uninitialized variables and can also be introduced by
	the `llzk-array-to-scalar` pass if there is a read from an array index
	that was not dominated by an earlier write to that same index.
	Example:
	```llzk
	%0 = llzk.nondet : !felt.type
	```
	Note that `llzk.nondet` does not have the `ConstantLike` or `NoMemoryEffect`
	traits because different SSA variables initialized with `llzk.nondet` may be
	constrained in different ways so they cannot be treated as identical values.
	However, it does have the `AlwaysSpeculatable` trait to denote that it is
	free to move, hoist, and sick without changing the semantics.

The same documentation already warns that merging distinct nondet values can change circuit semantics:

llzk-lib/include/llzk/Dialect/LLZK/IR/Ops.td

Lines 67 to 81 in aced31c

	In the above example, `%m` is effectively unconstrained, as it is only constrained
	to the nondet value `%1`. However, if `%0` and `%1` were treated as pure constants,
	`%0` and `%1` could be combined, resulting in:
	```llzk
	%0 = llzk.nondet : !felt.type
	%c1 = felt.const 1
	constrain.eq %0, %c1 : !felt.type
	%m = struct.readm %self[@m] : !struct.type<@S>, !felt.type
	constrain.eq %m, %0 : !felt.type
	```
	This transformation would constrain `%m` to be exactly equal to 1, thus changing
	the semantics of the circuit.

Generated polynomial auxiliaries need a placement-sensitive contract:

For each dynamic execution instance of this op, there exists a fresh compiler-generated witness value.

A loop-local generated auxiliary must not be freely hoisted out of the loop, because that changes:

forall i. exists aux_i

into:

exists aux. forall i

MLIR's side-effect and speculation model is the right place to express this kind of movement boundary:
https://mlir.llvm.org/docs/Rationale/SideEffectsAndSpeculation/

A dedicated llzk.aux op can carry the generated-auxiliary contract directly. V1 can be conservative: !felt.type only, not CSE-able, not Pure, and not freely hoistable across dynamic-scope boundaries.

Pipeline direction

The near-term safe behavior for existing users can be:

llzk-full-poly-lowering
  = scalar compatibility materialization when proven safe
  + diagnostic rejection otherwise
  + existing cleanup

That fits the current full poly lowering pipeline shape:

llzk-lib/lib/Transforms/LLZKTransformationPassPipelines.cpp

Lines 54 to 64 in aced31c

	PassPipelineRegistration<FullPolyLoweringOptions>(
	"llzk-full-poly-lowering",
	"Lower all polynomial constraints to a given max degree, then remove unnecessary operations "
	"and definitions.",
	[](OpPassManager &pm, const FullPolyLoweringOptions &opts) {
	// 1. Degree lowering
	pm.addPass(createPolyLoweringPass(PolyLoweringPassOptions {.maxDegree = opts.maxDegree}));
	// 2. Cleanup
	addRemoveUnnecessaryOpsAndDefsPipeline(pm);
	}

A semantic mode can be opt-in while backends are updated:

llzk-poly-lowering-pass="max-degree=2 aux-mode=semantic"

Semantic mode should:

• emit llzk.aux;
• emit constrain.eq %aux, %expr;
• place the auxiliary in the correct dynamic region;
• avoid mutating struct.def;
• avoid emitting @compute writes;
• require later materialization or backend support.

A target pipeline that cannot consume llzk.aux should run a verifier/materializer before backend lowering.

Backend note: R1CS

The R1CS lowering path currently maps struct members to signals:

llzk-lib/backends/r1cs/lib/r1cs/Transforms/R1CSLoweringPass.cpp

Lines 602 to 617 in aced31c

	// Step 4: For every struct member we a) create a signaldefop and b) add that signal to our
	// outputs
	DenseMap<StringRef, Value> memberSignalMap;
	uint32_t signalDefCntr = 0;
	for (auto member : structDef.getMemberDefs()) {
	r1cs::PublicAttr pubAttr;
	if (member.hasPublicAttr()) {
	pubAttr = bodyBuilder.getAttr<r1cs::PublicAttr>();
	}
	auto defOp = bodyBuilder.create<r1cs::SignalDefOp>(
	member.getLoc(), bodyBuilder.getType<r1cs::SignalType>(),
	bodyBuilder.getUI32IntegerAttr(signalDefCntr), pubAttr
	);
	signalDefCntr++;
	memberSignalMap.insert({member.getName(), defOp.getOut()});
	}

It also has its own auxiliary-member normalization path:

llzk-lib/backends/r1cs/lib/r1cs/Transforms/R1CSLoweringPass.cpp

Lines 257 to 352 in aced31c

	/// Normalize a felt-valued expression into R1CS-compatible form by rewriting
	/// only when strictly necessary. This function ensures the resulting expression:
	///
	/// - Has at most one multiplication per constraint (R1CS-compatible)
	/// - Avoids unnecessary introduction of auxiliary variables
	/// - Preserves semantic equivalence via auxiliary member equality constraints
	///
	/// Rewriting is done **bottom-up** using post-order traversal of the def-use chain.
	/// The transformation is minimal:
	/// - Only rewrites Add/Sub where both operands are degree-2
	/// - Leaves multiplications intact unless their operands require rewriting due to constants
	/// - Avoids rewriting expressions that are already linear or already normalized
	///
	/// The function memoizes all degrees and rewrites for efficiency and correctness,
	/// and records any auxiliary member assignments for later reconstruction in compute().
	///
	/// \param root The root felt-valued expression to normalize.
	/// \param structDef The enclosing struct definition (for adding aux members).
	/// \param constrainFunc The constrain() function containing the constraint logic.
	/// \param degreeMemo Memoized degrees of expressions (to avoid recomputation).
	/// \param rewrites Memoized rewrites of expressions.
	/// \param auxAssignments Records auxiliary member assignments introduced during normalization.
	/// \param builder Builder used to insert new ops in the constrain() block.
	/// \returns A Value representing the normalized (possibly rewritten) expression.
	Value normalizeForR1CS(
	Value root, StructDefOp structDef, FuncDefOp constrainFunc,
	DenseMap<Value, unsigned> &degreeMemo, DenseMap<Value, Value> &rewrites,
	SmallVectorImpl<AuxAssignment> &auxAssignments, OpBuilder &builder
	) {
	if (auto it = rewrites.find(root); it != rewrites.end()) {
	return it->second;
	}
	SmallVector<Value, 16> postOrder;
	getPostOrder(root, postOrder);
	// We perform a bottom up rewrite of the expressions. For any expression e := op(e_1, ...,
	// e_n) we first rewrite e_1, ..., e_n if necessary and then rewrite e based on op.
	for (Value val : postOrder) {
	if (rewrites.contains(val)) {
	continue;
	}
	Operation *op = val.getDefiningOp();
	if (!op) {
	// Block arguments, etc.
	degreeMemo[val] = 1;
	rewrites[val] = val;
	continue;
	}
	// Case 1: Felt constant op. The degree is 0 and no rewrite is needed.
	if (auto c = llvm::dyn_cast<FeltConstantOp>(op)) {
	degreeMemo[val] = 0;
	rewrites[val] = val;
	continue;
	}
	// Case 2: Member read op. The degree is 1 and no rewrite needed.
	if (auto fr = llvm::dyn_cast<MemberReadOp>(op)) {
	degreeMemo[val] = 1;
	rewrites[val] = val;
	continue;
	}
	// Helper function for getting degree from memo map
	auto getDeg = [&degreeMemo](Value v) -> unsigned {
	auto it = degreeMemo.find(v);
	assert(it != degreeMemo.end() && "Missing degree");
	return it->second;
	};
	// Case 3: lhs +/- rhs. There are three subcases cases to consider:
	// 1) If deg(lhs) <= degree(rhs) < 2 then nothing needs to be done
	// 2) If deg(lhs) = 2 and degree(rhs) < 2 then nothing further has to be done.
	// 3) If deg(lhs) = deg(rhs) = 2 then we lower one of lhs or rhs.
	auto handleAddOrSub = [&](Value lhsOrig, Value rhsOrig, bool isAdd) {
	Value lhs = rewrites[lhsOrig];
	Value rhs = rewrites[rhsOrig];
	unsigned degLhs = getDeg(lhs);
	unsigned degRhs = getDeg(rhs);
	if (degLhs == 2 && degRhs == 2) {
	builder.setInsertionPoint(op);
	std::string auxName = R1CS_AUXILIARY_MEMBER_PREFIX + std::to_string(auxCounter++);
	MemberDefOp auxMember = addAuxMember(structDef, auxName);
	Value aux = builder.create<MemberReadOp>(
	val.getLoc(), val.getType(), constrainFunc.getSelfValueFromConstrain(),
	auxMember.getNameAttr()
	);
	auto eqOp = builder.create<EmitEqualityOp>(val.getLoc(), aux, lhs);
	auxAssignments.push_back({auxName, lhs});
	degreeMemo[aux] = 1;
	rewrites[aux] = aux;
	replaceSubsequentUsesWith(lhs, aux, eqOp);

That can be supported during migration, but the final design should not require generated polynomial auxiliaries to become component-lifetime struct storage first.

A cleaner R1CS path is:

llzk.aux
  -> backend-private R1CS variable/signal

with one private value per required dynamic instance. If loops remain at that point, the R1CS materializer must either unroll, use a loop-aware representation, or reject. It must not silently collapse all dynamic instances into one signal.

Test plan

The regression suite should cover both the immediate bug and the architecture boundary.

Required tests:

1. Exact Poly lowering materializes loop-local expressions as one component-scope auxiliary #542 repro.

   • Compatibility scalar mode rejects.
   • Semantic mode emits llzk.aux inside the scf.for body.

2. Loop-carried dependency.

   • %acc-derived expression requires per-iteration freshness.

3. Loop-IV dependency.

   • %iv-derived expression requires per-iteration freshness.

4. Loop-invariant expression inside a loop.

   • Should not be rejected merely because it is syntactically inside a loop.
   • Scalar materialization is allowed only if component freshness and compute rebuildability are proven.

5. Nested loops.

   • %i-only dependency can be outer-loop fresh.
   • %i and %j dependency requires nested iteration freshness.

6. Branch-local expression.

   • Auxiliary remains branch-local unless conditional movement/materialization is proven.

7. Dynamic offset or affine operand.

   • Scalar member materialization rejects when dynamic offset freshness cannot be represented.

8. Nonlinear struct constrain call argument.

   • Caller-side auxiliary follows the argument's dynamic freshness.

9. llzk.nondet separation.

   • Generated llzk.aux does not merge with user llzk.nondet.
   • Two generated auxiliaries are not CSE'd together.

10. Cleanup/canonicalization stability.

    • Semantic auxiliaries are not hoisted out of loops.
    • Semantic auxiliaries are not sunk across branch boundaries.
    • Dominance remains valid.

Phased implementation plan

Phase 1: immediate safety patch

Before creating a scalar auxiliary member, prove:

• the factored expression is component-fresh;
• the expression is rebuildable in @compute;
• replacement uses are dominance-valid.

If not, emit a diagnostic and fail.

This phase prevents the #542 unsound lowering without requiring backend-wide changes.

Phase 2: dominance-aware replacement

Replace same-block “subsequent use” rewriting with MLIR dominance and region-scope checks.

This is needed even if scalar compatibility remains the default.

Phase 3: semantic auxiliary op

Add llzk.aux with generated existential semantics.

V1 constraints:

• result type !felt.type;
• not Pure;
• not ConstantLike;
• not freely CSE-able;
• not freely hoistable across loops or branches;
• optional origin/debug attributes only for diagnostics.

Phase 4: semantic poly lowering mode

Add an opt-in mode that emits llzk.aux and equality constraints, but does not mutate struct.def and does not emit @compute writes.

Phase 5: materializers

Add materializers incrementally:

1. component scalar materializer for proven-safe cases;
2. R1CS-private materializer for component/static-unrolled cases;
3. static unrolled materializer;
4. product/witgen materializers where deterministic witness computation is needed;
5. array/column materializers only when a target has a precise proof obligation for them.

Acceptance criteria

This design is successful when:

• Poly lowering materializes loop-local expressions as one component-scope auxiliary #542 cannot lower silently to one component-scope scalar auxiliary;
• scalar component-member materialization is guarded by freshness and compute-rebuildability proofs;
• region-dependent auxiliaries are represented with matching dynamic freshness or rejected;
• replacement uses MLIR dominance and region visibility;
• semantic mode can emit region-local llzk.aux without mutating struct.def;
• generated auxiliaries are not CSE'd or hoisted across dynamic-scope boundaries;
• backend pipelines either materialize llzk.aux deliberately or reject before unsupported lowering;
• tests cover loops, loop-carried args, nested loops, branches, dynamic offsets, nonlinear call arguments, nondet separation, and optimization stability.

References

Motivating issue:

• Poly lowering materializes loop-local expressions as one component-scope auxiliary #542: Poly lowering materializes loop-local expressions as one component-scope auxiliary #542

Current LLZK implementation:

• Poly lowering pass documentation:
  

  llzk-lib/include/llzk/Transforms/LLZKTransformationPasses.td

  Lines 66 to 79 in aced31c

  	def PolyLoweringPass : LLZKPass<"llzk-poly-lowering-pass"> {
  	let summary =
  	"Lower the degree of all polynomial equations to a specified maximum";
  	let description = [{
  	Rewrites constraint expressions into an (observationally) equivalent system where the degree of
  	every polynomial is less than or equal to the specified maximum.
  	High-degree subexpressions are factored into auxiliary struct members. The pass also recurses
  	through degree-neutral roots such as `felt.add`, `felt.sub`, and `felt.neg`, so composite
  	equality operands and struct constrain call arguments satisfy their degree bounds.
  	This pass is best used as part of the `-llzk-full-poly-lowering` pipeline, which includes
  	additional cleanup passes to ensure correctness and optimal performance.
  	}];

• Auxiliary member creation during expression factoring:
  

  llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

  Lines 178 to 224 in aced31c

  	// Optimization: If lhs == rhs, factor it only once
  	if (lhs == rhs && eraseMul) {
  	std::string auxName = AUXILIARY_MEMBER_PREFIX + std::to_string(this->auxCounter++);
  	MemberDefOp auxMember = addAuxMember(structDef, auxName);
  	auto auxVal = builder.create<MemberReadOp>(
  	lhs.getLoc(), lhs.getType(), selfVal, auxMember.getNameAttr()
  	);
  	auxAssignments.push_back({auxName, lhs});
  	Location loc = builder.getFusedLoc({auxVal.getLoc(), lhs.getLoc()});
  	auto eqOp = builder.create<EmitEqualityOp>(loc, auxVal, lhs);
  	// Memoize auxVal as degree 1
  	degreeMemo[auxVal] = 1;
  	rewrites[lhs] = auxVal;
  	rewrites[rhs] = auxVal;
  	// Now selectively replace subsequent uses of lhs with auxVal
  	replaceSubsequentUsesWith(lhs, auxVal, eqOp);
  	// Update lhs and rhs to use auxVal
  	lhs = auxVal;
  	rhs = auxVal;
  	lhsDeg = rhsDeg = 1;
  	}
  	// While their product exceeds maxDegree, factor out one side
  	while (lhsDeg + rhsDeg > maxDegree) {
  	Value &toFactor = (lhsDeg >= rhsDeg) ? lhs : rhs;
  	// Create auxiliary member for toFactor
  	std::string auxName = AUXILIARY_MEMBER_PREFIX + std::to_string(this->auxCounter++);
  	MemberDefOp auxMember = addAuxMember(structDef, auxName);
  	// Read back as MemberReadOp (new SSA value)
  	auto auxVal = builder.create<MemberReadOp>(
  	toFactor.getLoc(), toFactor.getType(), selfVal, auxMember.getNameAttr()
  	);
  	// Emit constraint: auxVal == toFactor
  	Location loc = builder.getFusedLoc({auxVal.getLoc(), toFactor.getLoc()});
  	auto eqOp = builder.create<EmitEqualityOp>(loc, auxVal, toFactor);
  	auxAssignments.push_back({auxName, toFactor});
  	// Update memoization
  	rewrites[toFactor] = auxVal;
  	degreeMemo[auxVal] = 1; // stays same
  	// replace the term with auxVal.
  	replaceSubsequentUsesWith(toFactor, auxVal, eqOp);

• Auxiliary member creation for nonlinear struct constrain call arguments:
  

  llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

  Lines 253 to 278 in aced31c

  	Value materializeCallArgument(
  	Value val, StructDefOp structDef, FuncDefOp constrainFunc, CallOp callOp,
  	DenseMap<Value, unsigned> &degreeMemo, DenseMap<Value, Value> &rewrites,
  	SmallVector<AuxAssignment> &auxAssignments
  	) {
  	Value loweredVal =
  	lowerExpression(val, structDef, constrainFunc, degreeMemo, rewrites, auxAssignments);
  	DenseMap<Value, unsigned> checkMemo;
  	if (getDegree(loweredVal, checkMemo) <= 1) {
  	return loweredVal;
  	}
  	// Callees only receive SSA values, not the caller expression tree, so nonlinear
  	// call arguments must be represented by an auxiliary member read.
  	std::string auxName = AUXILIARY_MEMBER_PREFIX + std::to_string(this->auxCounter++);
  	MemberDefOp auxMember = addAuxMember(structDef, auxName);
  	OpBuilder builder(callOp);
  	Value selfVal = constrainFunc.getSelfValueFromConstrain();
  	auto auxVal = builder.create<MemberReadOp>(
  	loweredVal.getLoc(), loweredVal.getType(), selfVal, auxMember.getNameAttr()
  	);
  	Location loc = builder.getFusedLoc({auxVal.getLoc(), loweredVal.getLoc()});
  	builder.create<EmitEqualityOp>(loc, auxVal, loweredVal);
  	auxAssignments.push_back({auxName, loweredVal});

  
  

  llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

  Lines 420 to 438 in aced31c

  	DenseMap<Value, unsigned> callMemo;
  	unsigned deg = getDegree(arg, callMemo);
  	if (deg > 1) {
  	arg = materializeCallArgument(
  	arg, structDef, constrainFunc, callOp, degreeMemo, rewrites, auxAssignments
  	);
  	modified = true;
  	}
  	}
  	if (modified) {
  	OpBuilder builder(callOp);
  	builder.create<CallOp>(
  	callOp.getLoc(), callOp.getResultTypes(), callOp.getCallee(),
  	CallOp::toVectorOfValueRange(callOp.getMapOperands()), callOp.getNumDimsPerMap(),
  	newOperands
  	);
  	callOp->erase();

• Compute-side auxiliary writes:
  

  llzk-lib/lib/Transforms/LLZKPolyLoweringPass.cpp

  Lines 453 to 464 in aced31c

  	DenseMap<Value, Value> rebuildMemo;
  	Block &computeBlock = computeFunc.getBody().front();
  	OpBuilder builder(&computeBlock, computeBlock.getTerminator()->getIterator());
  	Value selfVal = computeFunc.getSelfValueFromCompute();
  	for (const auto &assign : auxAssignments) {
  	Value rebuiltExpr =
  	rebuildExprInCompute(assign.computedValue, computeFunc, builder, rebuildMemo);
  	builder.create<MemberWriteOp>(
  	assign.computedValue.getLoc(), selfVal, builder.getStringAttr(assign.auxMemberName),
  	rebuiltExpr
  	);

• rebuildExprInCompute block-argument mapping:
  

  llzk-lib/lib/Transforms/LLZKLoweringUtils.cpp

  Lines 29 to 40 in aced31c

  	Value rebuildExprInCompute(
  	Value val, FuncDefOp computeFunc, OpBuilder &builder, DenseMap<Value, Value> &memo
  	) {
  	if (auto it = memo.find(val); it != memo.end()) {
  	return it->second;
  	}
  	if (auto barg = llvm::dyn_cast<BlockArgument>(val)) {
  	unsigned index = barg.getArgNumber();
  	Value mapped = computeFunc.getArgument(index - 1);
  	return memo[val] = mapped;
  	}

• Same-block replacement helper:
  

  llzk-lib/lib/Transforms/LLZKLoweringUtils.cpp

  Lines 102 to 118 in aced31c

  	void replaceSubsequentUsesWith(Value oldVal, Value newVal, Operation *afterOp) {
  	assert(afterOp && "afterOp must be a valid Operation*");
  	for (auto &use : llvm::make_early_inc_range(oldVal.getUses())) {
  	Operation *user = use.getOwner();
  	// Skip uses that are:
  	// - Before afterOp in the same block.
  	// - Inside afterOp itself.
  	if ((user->getBlock() == afterOp->getBlock()) &&
  	(user == afterOp || user->isBeforeInBlock(afterOp))) {
  	continue;
  	}
  	// Replace this use of oldVal with newVal.
  	use.set(newVal);
  	}

• llzk.nondet operation:
  

  llzk-lib/include/llzk/Dialect/LLZK/IR/Ops.td

  Lines 28 to 87 in aced31c

  	def LLZK_NonDetOp
  	: LLZKDialectOp<"nondet", [AlwaysSpeculatable,
  	DeclareOpInterfaceMethods<
  	OpAsmOpInterface, ["getAsmResultNames"]>]> {
  	let summary = "uninitialized variable";
  	let description = [{
  	This operation produces an SSA variable of the specified type but with
  	nondeterministic value.
  	This op can be used in `@constrain()` functions in place of expressions that
  	cannot be included in constraints. It may also be generated for a frontend
  	language that supports uninitialized variables and can also be introduced by
  	the `llzk-array-to-scalar` pass if there is a read from an array index
  	that was not dominated by an earlier write to that same index.
  	Example:
  	```llzk
  	%0 = llzk.nondet : !felt.type
  	```
  	Note that `llzk.nondet` does not have the `ConstantLike` or `NoMemoryEffect`
  	traits because different SSA variables initialized with `llzk.nondet` may be
  	constrained in different ways so they cannot be treated as identical values.
  	However, it does have the `AlwaysSpeculatable` trait to denote that it is
  	free to move, hoist, and sick without changing the semantics.
  	Example:
  	```llzk
  	%0 = llzk.nondet : !felt.type
  	%1 = llzk.nondet : !felt.type
  	%c1 = felt.const 1
  	constrain.eq %0, %c1 : !felt.type
  	%m = struct.readm %self[@m] : !struct.type<@S>, !felt.type
  	constrain.eq %m, %1 : !felt.type
  	```
  	In the above example, `%m` is effectively unconstrained, as it is only constrained
  	to the nondet value `%1`. However, if `%0` and `%1` were treated as pure constants,
  	`%0` and `%1` could be combined, resulting in:
  	```llzk
  	%0 = llzk.nondet : !felt.type
  	%c1 = felt.const 1
  	constrain.eq %0, %c1 : !felt.type
  	%m = struct.readm %self[@m] : !struct.type<@S>, !felt.type
  	constrain.eq %m, %0 : !felt.type
  	```
  	This transformation would constrain `%m` to be exactly equal to 1, thus changing
  	the semantics of the circuit.
  	}];
  	let results = (outs AnyLLZKType:$res);
  	let assemblyFormat = [{ `:` type($res) attr-dict }];
  	let hasCanonicalizer = 1;
  	}

• Full poly lowering pipeline:
  

  llzk-lib/lib/Transforms/LLZKTransformationPassPipelines.cpp

  Lines 54 to 64 in aced31c

  	PassPipelineRegistration<FullPolyLoweringOptions>(
  	"llzk-full-poly-lowering",
  	"Lower all polynomial constraints to a given max degree, then remove unnecessary operations "
  	"and definitions.",
  	[](OpPassManager &pm, const FullPolyLoweringOptions &opts) {
  	// 1. Degree lowering
  	pm.addPass(createPolyLoweringPass(PolyLoweringPassOptions {.maxDegree = opts.maxDegree}));
  	// 2. Cleanup
  	addRemoveUnnecessaryOpsAndDefsPipeline(pm);
  	}

• R1CS auxiliary/member interaction:
  

  llzk-lib/backends/r1cs/lib/r1cs/Transforms/R1CSLoweringPass.cpp

  Lines 257 to 352 in aced31c

  	/// Normalize a felt-valued expression into R1CS-compatible form by rewriting
  	/// only when strictly necessary. This function ensures the resulting expression:
  	///
  	/// - Has at most one multiplication per constraint (R1CS-compatible)
  	/// - Avoids unnecessary introduction of auxiliary variables
  	/// - Preserves semantic equivalence via auxiliary member equality constraints
  	///
  	/// Rewriting is done **bottom-up** using post-order traversal of the def-use chain.
  	/// The transformation is minimal:
  	/// - Only rewrites Add/Sub where both operands are degree-2
  	/// - Leaves multiplications intact unless their operands require rewriting due to constants
  	/// - Avoids rewriting expressions that are already linear or already normalized
  	///
  	/// The function memoizes all degrees and rewrites for efficiency and correctness,
  	/// and records any auxiliary member assignments for later reconstruction in compute().
  	///
  	/// \param root The root felt-valued expression to normalize.
  	/// \param structDef The enclosing struct definition (for adding aux members).
  	/// \param constrainFunc The constrain() function containing the constraint logic.
  	/// \param degreeMemo Memoized degrees of expressions (to avoid recomputation).
  	/// \param rewrites Memoized rewrites of expressions.
  	/// \param auxAssignments Records auxiliary member assignments introduced during normalization.
  	/// \param builder Builder used to insert new ops in the constrain() block.
  	/// \returns A Value representing the normalized (possibly rewritten) expression.
  	Value normalizeForR1CS(
  	Value root, StructDefOp structDef, FuncDefOp constrainFunc,
  	DenseMap<Value, unsigned> &degreeMemo, DenseMap<Value, Value> &rewrites,
  	SmallVectorImpl<AuxAssignment> &auxAssignments, OpBuilder &builder
  	) {
  	if (auto it = rewrites.find(root); it != rewrites.end()) {
  	return it->second;
  	}
  	SmallVector<Value, 16> postOrder;
  	getPostOrder(root, postOrder);
  	// We perform a bottom up rewrite of the expressions. For any expression e := op(e_1, ...,
  	// e_n) we first rewrite e_1, ..., e_n if necessary and then rewrite e based on op.
  	for (Value val : postOrder) {
  	if (rewrites.contains(val)) {
  	continue;
  	}
  	Operation *op = val.getDefiningOp();
  	if (!op) {
  	// Block arguments, etc.
  	degreeMemo[val] = 1;
  	rewrites[val] = val;
  	continue;
  	}
  	// Case 1: Felt constant op. The degree is 0 and no rewrite is needed.
  	if (auto c = llvm::dyn_cast<FeltConstantOp>(op)) {
  	degreeMemo[val] = 0;
  	rewrites[val] = val;
  	continue;
  	}
  	// Case 2: Member read op. The degree is 1 and no rewrite needed.
  	if (auto fr = llvm::dyn_cast<MemberReadOp>(op)) {
  	degreeMemo[val] = 1;
  	rewrites[val] = val;
  	continue;
  	}
  	// Helper function for getting degree from memo map
  	auto getDeg = [&degreeMemo](Value v) -> unsigned {
  	auto it = degreeMemo.find(v);
  	assert(it != degreeMemo.end() && "Missing degree");
  	return it->second;
  	};
  	// Case 3: lhs +/- rhs. There are three subcases cases to consider:
  	// 1) If deg(lhs) <= degree(rhs) < 2 then nothing needs to be done
  	// 2) If deg(lhs) = 2 and degree(rhs) < 2 then nothing further has to be done.
  	// 3) If deg(lhs) = deg(rhs) = 2 then we lower one of lhs or rhs.
  	auto handleAddOrSub = [&](Value lhsOrig, Value rhsOrig, bool isAdd) {
  	Value lhs = rewrites[lhsOrig];
  	Value rhs = rewrites[rhsOrig];
  	unsigned degLhs = getDeg(lhs);
  	unsigned degRhs = getDeg(rhs);
  	if (degLhs == 2 && degRhs == 2) {
  	builder.setInsertionPoint(op);
  	std::string auxName = R1CS_AUXILIARY_MEMBER_PREFIX + std::to_string(auxCounter++);
  	MemberDefOp auxMember = addAuxMember(structDef, auxName);
  	Value aux = builder.create<MemberReadOp>(
  	val.getLoc(), val.getType(), constrainFunc.getSelfValueFromConstrain(),
  	auxMember.getNameAttr()
  	);
  	auto eqOp = builder.create<EmitEqualityOp>(val.getLoc(), aux, lhs);
  	auxAssignments.push_back({auxName, lhs});
  	degreeMemo[aux] = 1;
  	rewrites[aux] = aux;
  	replaceSubsequentUsesWith(lhs, aux, eqOp);

  
  

  llzk-lib/backends/r1cs/lib/r1cs/Transforms/R1CSLoweringPass.cpp

  Lines 602 to 617 in aced31c

  	// Step 4: For every struct member we a) create a signaldefop and b) add that signal to our
  	// outputs
  	DenseMap<StringRef, Value> memberSignalMap;
  	uint32_t signalDefCntr = 0;
  	for (auto member : structDef.getMemberDefs()) {
  	r1cs::PublicAttr pubAttr;
  	if (member.hasPublicAttr()) {
  	pubAttr = bodyBuilder.getAttr<r1cs::PublicAttr>();
  	}
  	auto defOp = bodyBuilder.create<r1cs::SignalDefOp>(
  	member.getLoc(), bodyBuilder.getType<r1cs::SignalType>(),
  	bodyBuilder.getUI32IntegerAttr(signalDefCntr), pubAttr
  	);
  	signalDefCntr++;
  	memberSignalMap.insert({member.getName(), defOp.getOut()});
  	}

MLIR references:

• scf.for loop-carried region argument semantics:
  https://mlir.llvm.org/docs/Dialects/SCFDialect/
• Hierarchical dominance and value scope:
  https://mlir.llvm.org/docs/LangRef/
• Side effects and speculation:
  https://mlir.llvm.org/docs/Rationale/SideEffectsAndSpeculation/

[1sgtpepper]

For #542, this proposal does not need to land all at once.

A narrow fix can keep the current scalar-member path, but require proof that each generated scalar member is component-fresh and rebuildable in @compute. If the expression depends on a loop-carried value, loop IV, branch-local value, dynamic offset, or unsupported nested-region value, the pass should reject with a clear diagnostic.

That would stop the silent unsound lowering quickly, while the broader llzk.aux design gives a path to support those cases later through explicit materialization.

[1sgtpepper]

With #545 merged, and #560 applying the same conservative guard to @compute, I think the next incremental step can be smaller than adding public llzk.aux IR first.

The key refinement is to separate two facts for each factored expression E:

Value dependencies:
  which dynamic values can make E change

Placement:
  where aux = E may be emitted so it matches the original dominance/path context

These should not be treated as one freshness property. For example, inside an scf.for:

%sq = felt.mul %a, %a : !felt.type, !felt.type

can still be component-invariant if %a is a component/input argument:

deps(%a * %a) = {}
placement(%a * %a) = loop body

But the #542 case is different:

%sq = felt.mul %acc, %acc : !felt.type, !felt.type

where %acc is loop-carried:

deps(%acc * %acc) = {that scf.for}
placement(%acc * %acc) = loop body

A scalar component member maps all dynamic executions to one storage cell:

addr(i) = m

so it is sound only when sharing cannot add constraints:

forall i,j. E_i = E_j

A conservative scalar materializer can prove that only for expressions whose dynamic dependency set is empty, using a narrow whitelist:

felt.const             -> {}
entry constrain arg    -> {}
static self read       -> {}
felt.add/sub/mul/neg   -> union operand deps
loop IV/body arg       -> {loop}
branch block arg       -> {branch/control}
dynamic offset/read    -> dynamic/unknown
unsupported op         -> unknown

So the current scalar-member path could first build an internal plan, without mutating IR:

plans = planAuxiliaries(roots);        // no members/equalities/writes yet
if (failed(verifyScalarPlans(plans)))
  return failure();

for (AuxPlan &p : stableTopologicalOrder(plans))
  materializeScalarPlan(p);

For scalar mode, verifyScalarPlan should require:

dynamic deps are empty
expression is known pure/total
expression is rebuildable in @compute
replacement uses satisfy MLIR dominance and visibility
generated member is private

Unknown or dynamic cases would keep the current conservative rejection behavior until a semantic auxiliary/materializer mode exists.

One small efficiency improvement falls out of the same structure: reuse planned auxiliaries only for known pure expressions keyed by:

(ExprKey, dynamic deps, type, maxDegree)

That allows repeated component-invariant expressions like %a * %a to share one scalar aux, while preventing loop-carried, branch-local, dynamic-indexed, or unknown expressions from being merged into one component member.

This would make the first architecture step mostly internal: plan before mutation, prove scalar safety before creating members, and reuse only dependency-compatible pure expressions. llzk.aux still seems like the right longer-term semantic representation, but this gives the existing scalar-member path a smaller proof boundary first.

[1sgtpepper]

After investigating the current backend and lowering pipelines more thoroughly, I found that none needs polynomial lowering before flattening. The proposal remains a valid general solution to #542’s scope bug, but the existing flatten/reject contract covers the actual pipelines today. I’m closing this rather than adding IR with no current consumer.