diff --git a/README.md b/README.md
index cbdce151..f919305c 100644
--- a/README.md
+++ b/README.md
@@ -152,6 +152,20 @@ y = Square(x)
 
 Inputs are read-only — they flow in. Outputs flow out: the template may read one only after assigning it unconditionally, as in `sq = x * x` followed by `cube = sq * x`; before that, use a local. Read-only means the template cannot assign through the input name; it does not freeze a value shared with an output. A caller may reuse a variable as both argument and destination, `a = Square(a)`.
 
+Every body that runs assigns every output on every path. A write under a condition, from a value that can fail, or driven by a range that may be empty can be skipped, so it needs a default first. A function keeps an old value only through an input its caller passes:
+
+```python
+y = Fib(n)
+    y = n
+    y = n > 1 Fib(n - 1) + Fib(n - 2)
+
+out = Maybe(prev, x)
+    out = prev
+    out = x > 0 x
+```
+
+`a = Maybe(a, -1)` keeps `a`. A call therefore either writes all of its outputs or does not run at all: when an argument fails, when the statement's condition fails, or when its range is empty.
+
 ```python
 out, seen = Fold(current, item)
     out = current + item
@@ -219,14 +233,17 @@ lastSquare = Square(i)     # 16
 i                          # prints the descriptor: 0:5
 ```
 
-A bare range is a value: assignment copies it and print shows its descriptor.
-Using it in an operation creates a ranged computation: the assignment keeps
-the final yield, brackets materialize all yields into an array, and passing it
-to a template executes the call once for each value. The compiler can map
-these operations to SIMD instructions — this is range-driven
+A bare range is a value, written as a literal or held by a name: an assignment
+without a gate copies it, and print shows its descriptor unless another
+argument on the line loops over it. Using it under a gate or in an operation
+creates a ranged computation: the assignment keeps the final yield, brackets
+materialize all yields into an array, and passing it to a template executes
+the call once for each value. The
+compiler can map these operations to SIMD instructions — this is range-driven
 auto-vectorization. Each named Range binding is a distinct driver: different
 names form a cartesian domain when consumed together, even when their bounds
-are equal.
+are equal. A function cannot return a range; it returns the bounds, and the
+caller builds the range.
 
 Range-indexed array access follows the same rule:
 
diff --git a/compiler/bounds.go b/compiler/bounds.go
index f7dc1d22..1c6d43c5 100644
--- a/compiler/bounds.go
+++ b/compiler/bounds.go
@@ -481,14 +481,6 @@ func collectArrayIndexAccesses(expr ast.Expression, out *[]*ast.ArrayRangeExpres
 	}
 }
 
-func (c *Compiler) loopRangeValuesByName(ranges []*RangeInfo) map[string]llvm.Value {
-	bounds := make(map[string]llvm.Value, len(ranges))
-	for _, ri := range ranges {
-		bounds[ri.Name] = c.rangeAggregateForRI(ri)
-	}
-	return bounds
-}
-
 func (c *Compiler) arraySymbolForAffineGuard(arrayExpr ast.Expression) (*Symbol, Type, bool) {
 	ident, ok := arrayExpr.(*ast.Identifier)
 	if !ok {
@@ -511,7 +503,7 @@ func (c *Compiler) arraySymbolForAffineGuard(arrayExpr ast.Expression) (*Symbol,
 	return arraySym, arrType.ElemType, true
 }
 
-func (c *Compiler) affineVersioningGuard(exprs []ast.Expression, ranges []*RangeInfo) (llvm.Value, map[*ast.ArrayRangeExpression]struct{}, bool) {
+func (c *Compiler) affineVersioningGuard(exprs []ast.Expression, ranges []*RangeInfo, values []*Symbol) (llvm.Value, map[*ast.ArrayRangeExpression]struct{}, bool) {
 	if len(exprs) == 0 || len(ranges) == 0 {
 		return llvm.Value{}, nil, false
 	}
@@ -524,7 +516,10 @@ func (c *Compiler) affineVersioningGuard(exprs []ast.Expression, ranges []*Range
 		return llvm.Value{}, nil, false
 	}
 
-	boundsByName := c.loopRangeValuesByName(ranges)
+	boundsByName := make(map[string]llvm.Value, len(ranges))
+	for i, ri := range ranges {
+		boundsByName[ri.Name] = values[i].Val
+	}
 	fastAccess := make(map[*ast.ArrayRangeExpression]struct{})
 	guard := llvm.Value{}
 	hasGuard := false
diff --git a/compiler/cfg.go b/compiler/cfg.go
index 5233a16c..8732ea17 100644
--- a/compiler/cfg.go
+++ b/compiler/cfg.go
@@ -2,7 +2,6 @@ package compiler
 
 import (
 	"fmt"
-	"maps"
 	"slices"
 
 	"github.com/thiremani/pluto/ast"
@@ -37,7 +36,8 @@ type BasicBlock struct {
 	Stmts []*StmtNode
 }
 
-// CFG owns structural template validation and effect-sensitive dataflow.
+// CFG owns template validation, which classifies writes from the text, and
+// the script's effect-sensitive dataflow.
 type CFG struct {
 	CodeCompiler *CodeCompiler
 	Blocks       []*BasicBlock
@@ -185,21 +185,43 @@ func (cfg *CFG) collectSpecifierReads(value string, tok token.Token, runes []run
 	return reads, spec.end
 }
 
-// AnalyzeFuncs runs syntax-stable structural validation once for every
-// function template. Effect-sensitive diagnostics are deferred until a
-// concrete specialization is settled.
+// AnalyzeFuncs validates every function template once, whether or not
+// anything calls it: structural checks and a classification of each write
+// from the template's text alone, then dataflow checks over those writes.
+// The dataflow checks wait until every template passes the first two, since a
+// caller reads each call as returning values: a function rejected for holding
+// a range in an output would mislead its callers' checks.
 func (cfg *CFG) AnalyzeFuncs() {
+	cfg.CodeCompiler.rangeBindings = make(map[funcKey]map[string]struct{})
+	errorsBefore := len(cfg.Errors)
+
+	var templates []classifiedTemplate
 	for _, stmt := range cfg.CodeCompiler.Code.Statements {
 		fn, ok := stmt.(*ast.FuncStatement)
 		if !ok {
 			continue
 		}
 
-		cfg.validateFuncTemplate(fn)
+		templates = append(templates, cfg.validateFuncTemplate(fn))
+	}
+	if len(cfg.Errors) > errorsBefore {
+		return
+	}
+
+	for _, template := range templates {
+		cfg.checkTemplateFlow(template)
 	}
 }
 
-func (cfg *CFG) validateFuncTemplate(fn *ast.FuncStatement) {
+// classifiedTemplate keeps what the dataflow checks need from a validated
+// and classified template.
+type classifiedTemplate struct {
+	fn             *ast.FuncStatement
+	statementReads [][]VarEvent
+	writes         [][]textWrite
+}
+
+func (cfg *CFG) validateFuncTemplate(fn *ast.FuncStatement) classifiedTemplate {
 	PushScope(&cfg.Scopes, FuncScope)
 	defer PopScope(&cfg.Scopes)
 
@@ -214,7 +236,7 @@ func (cfg *CFG) validateFuncTemplate(fn *ast.FuncStatement) {
 
 	body := cfg.validateTemplateBody(fn.Body.Statements, identSet(fn.Parameters), identSet(fn.Outputs))
 	readInputs, assignedOutputs := body.readInputs, body.assignedOutputs
-	cfg.CodeCompiler.outputReads[funcKey{name: fn.Token.Literal, arity: len(fn.Parameters)}] = body.readOutputs
+	cfg.CodeCompiler.outputReads[templateKey(fn)] = body.readOutputs
 
 	for _, input := range fn.Parameters {
 		if _, wasRead := readInputs[input.Value]; wasRead {
@@ -230,6 +252,384 @@ func (cfg *CFG) validateFuncTemplate(fn *ast.FuncStatement) {
 
 		cfg.addError(output.Tok(), fmt.Sprintf("output parameter %q is never assigned", output.Value))
 	}
+
+	writes := cfg.classifyTemplateWrites(fn)
+	return classifiedTemplate{fn: fn, statementReads: body.statementReads, writes: writes}
+}
+
+// classifyTemplateWrites classifies every assignment's writes from the
+// template's text, indexed by statement, and records its range bindings for
+// settlement to check. It reports the text it cannot classify: a call that
+// names no template, an operator whose sides do not line up, and an
+// assignment whose values do not fill its targets. The solver rejects each of
+// these in any specialization; the flow checks, which would misread them, wait
+// until no template has one. It also reports an output that holds a range,
+// which a function cannot return.
+func (cfg *CFG) classifyTemplateWrites(fn *ast.FuncStatement) [][]textWrite {
+	// A scope of its own resolves each string's markers against the names
+	// defined before it, as the solver resolves them.
+	PushScope(&cfg.Scopes, FuncScope)
+	defer PopScope(&cfg.Scopes)
+	cfg.declareTargets(fn.Parameters)
+	cfg.declareTargets(fn.Outputs)
+
+	// ranges holds the bindings whose latest assignment gave them a range: a
+	// bare range literal or range name assigned without a gate. A parameter
+	// holds one element per run, and no call returns a range. A change between
+	// a range and a non-range value is the solver's to reject, like any other
+	// change of type.
+	ranges := make(map[string]struct{})
+	outputs := identSet(fn.Outputs)
+	writes := make([][]textWrite, len(fn.Body.Statements))
+	for i, stmt := range fn.Body.Statements {
+		cfg.rejectUnclassifiableExprs(statementExpressions(stmt))
+		let, ok := stmt.(*ast.LetStatement)
+		if !ok {
+			continue
+		}
+
+		letWrites, ok := cfg.classifyWrites(let, ranges)
+		if !ok {
+			cfg.addError(let.Token, assignmentMismatch(len(let.Name), cfg.valueCount(let.Value)))
+			continue
+		}
+		cfg.rejectRangeOutputs(outputs, let, letWrites)
+		cfg.declareTargets(let.Name)
+		updateRanges(ranges, let.Name, letWrites)
+		writes[i] = letWrites
+	}
+
+	cfg.CodeCompiler.rangeBindings[templateKey(fn)] = ranges
+	return writes
+}
+
+func (cfg *CFG) rejectUnclassifiableExprs(exprs []ast.Expression) {
+	for _, expr := range exprs {
+		switch e := expr.(type) {
+		case *ast.CallExpression:
+			if _, found := cfg.callTemplate(e); !found {
+				cfg.addError(e.Token, undefinedFunction(e.Function.Value))
+			}
+		case *ast.InfixExpression:
+			cfg.rejectMisalignedOperands(e)
+		}
+		cfg.rejectUnclassifiableExprs(ast.ExprChildren(expr))
+	}
+}
+
+// rejectMisalignedOperands reports an operator whose sides yield counts the
+// solver rejects.
+func (cfg *CFG) rejectMisalignedOperands(infix *ast.InfixExpression) {
+	left, right := cfg.valueSlots(infix.Left), cfg.valueSlots(infix.Right)
+	switch {
+	case !operandsLineUp(infix, left, right) && infix.IsLogicalAnd():
+		cfg.addError(infix.Token, logicalAndArityMismatch(left, right))
+	case !operandsLineUp(infix, left, right):
+		cfg.addError(infix.Token, operandMismatch(infix.Token.Literal, left, right))
+	}
+}
+
+// operandsLineUp reports whether an operator's sides yield counts the solver
+// accepts: equal counts, or for a && also a condition that folds onto one
+// value or broadcasts to several.
+func operandsLineUp(infix *ast.InfixExpression, left, right int) bool {
+	if infix.IsLogicalAnd() {
+		return left == right || left == 1 || right == 1
+	}
+	return left == right
+}
+
+// rejectRangeOutputs reports an output assigned a range. A function returns a
+// range's bounds instead, and its caller builds the range.
+func (cfg *CFG) rejectRangeOutputs(outputs map[string]struct{}, let *ast.LetStatement, writes []textWrite) {
+	for i, target := range let.Name {
+		if _, isOutput := outputs[target.Value]; !isOutput || !writes[i].holdsRange {
+			continue
+		}
+
+		cfg.addError(target.Tok(), fmt.Sprintf("output %q cannot hold a range; return its bounds and build the range where it is used", target.Value))
+	}
+}
+
+func undefinedFunction(name string) string {
+	return fmt.Sprintf("undefined function: %s", name)
+}
+
+func assignmentMismatch(targets, values int) string {
+	return fmt.Sprintf("assignment mismatch: %s but %s", countOf(targets, "target"), countOf(values, "value"))
+}
+
+func operandMismatch(operator string, left, right int) string {
+	return fmt.Sprintf("operand mismatch: %q has %s on its left but %s on its right", operator, countOf(left, "value"), countOf(right, "value"))
+}
+
+func logicalAndArityMismatch(left, right int) string {
+	return fmt.Sprintf("logical AND condition arity must match the value's, fold to one, or broadcast from one — got %d and %d", left, right)
+}
+
+// countOf writes n with its noun, in the plural unless n is one.
+func countOf(n int, noun string) string {
+	if n == 1 {
+		return "1 " + noun
+	}
+	return fmt.Sprintf("%d %ss", n, noun)
+}
+
+// checkTemplateFlow runs the dataflow checks once per template over the writes
+// classified from its text: an output is read only after a definite
+// assignment and is definitely assigned by the end of the body, and no write
+// is dead or overwrites a definite write that nothing read. It runs only on a
+// structurally valid body whose text classifies, so every output read follows
+// some write and every assignment has its writes.
+func (cfg *CFG) checkTemplateFlow(template classifiedTemplate) {
+	cfg.PushBlock()
+	defer cfg.PopBlock()
+
+	outputs := identSet(template.fn.Outputs)
+	cfg.forwardPass(template, outputs)
+	cfg.backwardPass(outputs)
+}
+
+// forwardPass runs the forward dataflow over a template's statements. An
+// output must be definitely assigned wherever it is read and by the end of the
+// body, where its caller reads it.
+func (cfg *CFG) forwardPass(template classifiedTemplate, outputs map[string]struct{}) {
+	assigned := make(map[string]struct{}, len(outputs))
+	lastWrites := make(map[string]VarEvent)
+
+	for i, stmt := range template.fn.Body.Statements {
+		cfg.rejectUnassignedOutputReads(template.statementReads[i], outputs, assigned)
+		events := append([]VarEvent(nil), template.statementReads[i]...)
+		if let, ok := stmt.(*ast.LetStatement); ok {
+			events = append(events, textWriteEvents(let, template.writes[i])...)
+		}
+		cfg.processDataflowEvents(stmt, events, lastWrites)
+
+		for _, event := range events {
+			if _, isOutput := outputs[event.Name]; isOutput && event.Kind == Write {
+				assigned[event.Name] = struct{}{}
+			}
+		}
+	}
+
+	cfg.rejectUnassignedOutputs(template.fn.Outputs, assigned)
+}
+
+func (cfg *CFG) rejectUnassignedOutputReads(reads []VarEvent, outputs, assigned map[string]struct{}) {
+	for _, read := range reads {
+		if _, isOutput := outputs[read.Name]; !isOutput {
+			continue
+		}
+		if _, ok := assigned[read.Name]; !ok {
+			cfg.addError(read.Token, fmt.Sprintf("output %q is read where it may still be unassigned; assign it unconditionally first, or pass the previous value as an input and initialize from it", read.Name))
+		}
+	}
+}
+
+func (cfg *CFG) rejectUnassignedOutputs(outputs []*ast.Identifier, assigned map[string]struct{}) {
+	for _, output := range outputs {
+		if _, ok := assigned[output.Value]; ok {
+			continue
+		}
+
+		cfg.addError(output.Tok(), fmt.Sprintf("output %q may be left unassigned; assign it unconditionally first, or pass the previous value as an input and initialize from it (%s = prev), with each caller passing its destination as that input", output.Value, output.Value))
+	}
+}
+
+// textWriteEvents turns an assignment's text classification into write events
+// at its named targets.
+func textWriteEvents(let *ast.LetStatement, writes []textWrite) []VarEvent {
+	var events []VarEvent
+	for i, target := range let.Name {
+		if isDiscard(target) {
+			continue
+		}
+
+		kind := ConditionalWrite
+		if writes[i].definite {
+			kind = Write
+		}
+		events = append(events, VarEvent{Name: target.Value, Kind: kind, Token: target.Tok()})
+	}
+	return events
+}
+
+// textWrite classifies one assignment target from the text: definite unless
+// the statement's gate, a value that can fail, or a range that may be empty
+// can skip the write; holdsRange when the target receives a Range descriptor.
+type textWrite struct {
+	definite   bool
+	holdsRange bool
+}
+
+// classifyWrites classifies every target of an assignment, discards included,
+// so the result lines up with its names. Values take targets by their output
+// counts; it reports false when those do not fill the targets.
+func (cfg *CFG) classifyWrites(let *ast.LetStatement, ranges map[string]struct{}) ([]textWrite, bool) {
+	if cfg.valueCount(let.Value) != len(let.Name) {
+		return nil, false
+	}
+
+	gated := len(let.Condition) > 0
+	writes := make([]textWrite, 0, len(let.Name))
+	for _, value := range let.Value {
+		definite := !gated && !cfg.maySkip(value, ranges)
+		isRange := !gated && assignsRange(value, ranges)
+		for slot := 0; slot < cfg.valueSlots(value); slot++ {
+			writes = append(writes, textWrite{definite: definite, holdsRange: isRange})
+		}
+	}
+
+	return writes, true
+}
+
+// maySkip reports whether a value can leave its targets unwritten: it can
+// fail (a value-position comparison, &&, a checked access, a || whose last
+// alternative can fail, or a call with such an argument), or a range that may
+// be empty drives it.
+func (cfg *CFG) maySkip(value ast.Expression, ranges map[string]struct{}) bool {
+	// A range literal assigned whole keeps the old value when a bound fails.
+	operands := []ast.Expression{value}
+	if lit, ok := value.(*ast.RangeLiteral); ok {
+		operands = ast.ExprChildren(lit)
+	}
+	for _, operand := range operands {
+		if treeCanFail(operand, textNodeFails) {
+			return true
+		}
+	}
+	return cfg.drivesValue(value, ranges)
+}
+
+func textNodeFails(expr ast.Expression) bool {
+	switch e := expr.(type) {
+	case *ast.InfixExpression:
+		return e.Token.IsComparison() || e.IsLogicalAnd()
+	case *ast.ArrayRangeExpression:
+		return true
+	}
+	return false
+}
+
+// assignsRange reports whether a value assigned without a gate gives its one
+// target a range: a bare range literal, or a bare range name whose range it
+// copies. Under a gate the value is a computation, so the range iterates.
+func assignsRange(value ast.Expression, ranges map[string]struct{}) bool {
+	switch v := value.(type) {
+	case *ast.RangeLiteral:
+		return true
+	case *ast.Identifier:
+		_, isRange := ranges[v.Value]
+		return isRange
+	}
+	return false
+}
+
+// updateRanges records which of an assignment's targets now hold a range:
+// exactly those it gives one.
+func updateRanges(ranges map[string]struct{}, targets []*ast.Identifier, writes []textWrite) {
+	for i, target := range targets {
+		if isDiscard(target) {
+			continue
+		}
+
+		if writes[i].holdsRange {
+			ranges[target.Value] = struct{}{}
+			continue
+		}
+		delete(ranges, target.Value)
+	}
+}
+
+// drivesValue reports whether a range that may be empty drives an
+// assignment's value: any range the value iterates, apart from a range it
+// assigns whole. A bare range name copies its range without a gate, and a
+// gated write can be skipped anyway.
+func (cfg *CFG) drivesValue(value ast.Expression, ranges map[string]struct{}) bool {
+	switch v := value.(type) {
+	case *ast.RangeLiteral:
+		return cfg.drivesAny(ast.ExprChildren(v), ranges)
+	case *ast.Identifier:
+		return false
+	case *ast.CallExpression:
+		return cfg.drivesAny(v.Arguments, ranges)
+	}
+	return cfg.drives(value, ranges)
+}
+
+// drives reports whether expr iterates a range that may be empty. Every range
+// in it is iterated, except inside an array literal, which settles its cells
+// itself, and in a string's main marker, which formats its range. Only a
+// range literal with constant, nonempty bounds always runs.
+func (cfg *CFG) drives(expr ast.Expression, ranges map[string]struct{}) bool {
+	switch e := expr.(type) {
+	case *ast.ArrayLiteral:
+		return false
+	case *ast.RangeLiteral:
+		return !rangeLiteralGuaranteedNonEmpty(e)
+	case *ast.Identifier:
+		_, isRange := ranges[e.Value]
+		return isRange
+	case *ast.StringLiteral:
+		// A width or precision operand consumes a range as numbers.
+		_, specs := formatMarkerIdentifiers(e.Token.Literal, cfg.isDefined)
+		for _, name := range specs {
+			if _, isRange := ranges[name]; isRange {
+				return true
+			}
+		}
+
+		return false
+	}
+	return cfg.drivesAny(ast.ExprChildren(expr), ranges)
+}
+
+func (cfg *CFG) drivesAny(exprs []ast.Expression, ranges map[string]struct{}) bool {
+	for _, expr := range exprs {
+		if cfg.drives(expr, ranges) {
+			return true
+		}
+	}
+
+	return false
+}
+
+// valueSlots counts the targets a value fills, read from the text the way the
+// solver counts a tuple: a call fills its template's outputs, and an operator
+// its right operand's. An operator whose sides do not line up fills one, as
+// the solver counts it after reporting the mismatch.
+func (cfg *CFG) valueSlots(value ast.Expression) int {
+	switch v := value.(type) {
+	case *ast.CallExpression:
+		if template, ok := cfg.callTemplate(v); ok {
+			return len(template.Outputs)
+		}
+	case *ast.InfixExpression:
+		left, right := cfg.valueSlots(v.Left), cfg.valueSlots(v.Right)
+		if operandsLineUp(v, left, right) {
+			return right
+		}
+	case *ast.PrefixExpression:
+		return cfg.valueSlots(v.Right)
+	}
+	return 1
+}
+
+// valueCount counts the values a list of expressions yields, as valueSlots
+// counts each.
+func (cfg *CFG) valueCount(values []ast.Expression) int {
+	count := 0
+	for _, value := range values {
+		count += cfg.valueSlots(value)
+	}
+
+	return count
+}
+
+// callTemplate finds a call's template by its name and arity, where an
+// argument counts once for each value it yields.
+func (cfg *CFG) callTemplate(call *ast.CallExpression) (*ast.FuncStatement, bool) {
+	return cfg.CodeCompiler.lookupFuncTemplate(call.Function.Value, cfg.valueCount(call.Arguments))
 }
 
 // templateBody is the structural summary of one template body.
@@ -309,57 +709,6 @@ func (cfg *CFG) validateScriptTemplate(statements []ast.Statement) [][]VarEvent
 	return cfg.validateTemplateBody(statements, nil, nil).statementReads
 }
 
-// AnalyzeSpecialization runs only typed dataflow over one type
-// specialization, with every input treated as its own value: a call that
-// shares an input with an output only adds reads, so a body valid here is
-// valid in every call. Structural diagnostics were already produced once
-// from the function template.
-func (cfg *CFG) AnalyzeSpecialization(template *ast.FuncStatement, info *FuncInfo) {
-	cfg.PushBlock()
-	defer cfg.PopBlock()
-	PushScope(&cfg.Scopes, FuncScope)
-	defer PopScope(&cfg.Scopes)
-
-	// Parameters must be in scope: the shared marker collector treats an
-	// unknown main marker as literal text and rejects unknown specifier names.
-	for _, param := range template.Parameters {
-		cfg.declareName(param)
-	}
-
-	outputs := identSet(template.Outputs)
-	cfg.typedForwardPass(template, info, outputs)
-	cfg.backwardPass(maps.Clone(outputs))
-}
-
-// typedForwardPass runs the forward dataflow over a body. Per statement, in
-// order: an explicit read of an output needs an earlier definite assignment;
-// the statement's events run; its definite targets become assigned for the
-// statements after it.
-func (cfg *CFG) typedForwardPass(template *ast.FuncStatement, info *FuncInfo, outputs map[string]struct{}) {
-	definitelyAssigned := make(map[string]struct{}, len(outputs))
-	lastWrites := make(map[string]VarEvent)
-	for _, stmt := range template.Body.Statements {
-		reads := cfg.collectStatementReads(stmt)
-		cfg.rejectUnassignedOutputReads(reads, outputs, definitelyAssigned)
-		cfg.processTypedStatement(stmt, reads, info.StatementEffects, lastWrites)
-
-		if let, ok := stmt.(*ast.LetStatement); ok {
-			maps.Copy(definitelyAssigned, definiteTargets(let, info.StatementEffects[let]))
-		}
-	}
-}
-
-func (cfg *CFG) rejectUnassignedOutputReads(reads []VarEvent, outputs, definitelyAssigned map[string]struct{}) {
-	for _, read := range reads {
-		if _, isOutput := outputs[read.Name]; !isOutput {
-			continue
-		}
-		if _, ok := definitelyAssigned[read.Name]; !ok {
-			cfg.addError(read.Token, fmt.Sprintf("output %q is read where it may still be unassigned; assign it unconditionally first, or pass the previous value as an input and initialize from it", read.Name))
-		}
-	}
-}
-
 func (cfg *CFG) typedScriptForwardPass(statements []ast.Statement, effects map[*ast.LetStatement]StatementEffect, statementReads [][]VarEvent) {
 	if len(statementReads) != len(statements) {
 		panic("internal: script CFG read count does not match statement count")
@@ -467,7 +816,8 @@ func (cfg *CFG) transferWrite(lastWrites map[string]VarEvent, event VarEvent) {
 	lastWrites[event.Name] = event
 }
 
-// backwardPass identifies unused values and dead stores.
+// backwardPass identifies unused values and dead stores. It walks back from
+// live, the names read after the body (a template's outputs), updating it.
 func (cfg *CFG) backwardPass(live map[string]struct{}) {
 	block := cfg.Blocks[len(cfg.Blocks)-1]
 	for i := len(block.Stmts) - 1; i >= 0; i-- {
@@ -495,8 +845,8 @@ func (cfg *CFG) backwardPass(live map[string]struct{}) {
 }
 
 // An output is readable once an earlier statement has assigned it; a
-// statement's reads precede its own writes. The typed pass narrows this per
-// specialization to writes that definitely assign.
+// statement's reads precede its own writes. The template's dataflow check
+// narrows this to writes that definitely assign.
 func (cfg *CFG) validateStructuralRead(event VarEvent, outputs, assigned map[string]struct{}) {
 	if _, isOutput := outputs[event.Name]; isOutput {
 		if _, isAssigned := assigned[event.Name]; !isAssigned {
diff --git a/compiler/cfg_replay_test.go b/compiler/cfg_replay_test.go
deleted file mode 100644
index e0ab280e..00000000
--- a/compiler/cfg_replay_test.go
+++ /dev/null
@@ -1,318 +0,0 @@
-package compiler
-
-import (
-	"testing"
-
-	"github.com/stretchr/testify/require"
-	"github.com/thiremani/pluto/token"
-	"tinygo.org/x/go-llvm"
-)
-
-func compileCFGReplayScript(t *testing.T, ctx llvm.Context, cc *CodeCompiler, name, source string) (*ScriptCompiler, []*token.CompileError) {
-	t.Helper()
-
-	sc := NewScriptCompiler(ctx, name, mustParseScript(t, source), cc)
-
-	return sc, sc.Compile()
-}
-
-func TestCFGReplayColdAndWarm(t *testing.T) {
-	code := mustParseCode(t, `result = Noisy(x)
-    unused = x + 1
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayColdWarm", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, coldErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Cold", "value = Noisy(1)\nvalue")
-	require.Len(t, coldErrors, 1)
-	require.Contains(t, coldErrors[0].Msg, `"unused"`)
-
-	noisyMangled := Mangle(cc.Compiler.MangledPath, "Noisy", []Type{I64})
-	coldInfo := cc.Compiler.FuncCache[noisyMangled]
-	require.NotNil(t, coldInfo)
-	require.True(t, coldInfo.Settled)
-	require.NotNil(t, coldInfo.CFGResult)
-	require.Len(t, coldInfo.CFGResult.Errors, 1)
-	require.Same(t, coldInfo.CFGResult.Errors[0], coldErrors[0],
-		"cold replay must return the immutable cached diagnostic")
-
-	coldResult := coldInfo.CFGResult
-	_, warmErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Warm", "value = Noisy(2)\nvalue")
-	require.Len(t, warmErrors, 1, "each script replay must report the reachable diagnostic")
-
-	warmInfo := cc.Compiler.FuncCache[noisyMangled]
-	require.Same(t, coldInfo, warmInfo, "the warm solve must reuse the settled specialization")
-	require.Same(t, coldResult, warmInfo.CFGResult, "the warm solve must not republish the CFG result")
-	require.Same(t, coldErrors[0], warmErrors[0],
-		"warm replay must return the same cached diagnostic pointer")
-}
-
-func TestCFGReplayDeduplicatesConcreteTypes(t *testing.T) {
-	code := mustParseCode(t, `result = NoisyTypes(x)
-    unused = x + 1
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayConcreteTypes", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, errors := compileCFGReplayScript(t, ctx, cc, t.Name(), `integer = NoisyTypes(1)
-floating = NoisyTypes(2.0)
-integer, floating`)
-	require.Len(t, errors, 1, "one template diagnostic must be reported once per script")
-
-	integerMangled := Mangle(cc.Compiler.MangledPath, "NoisyTypes", []Type{I64})
-	floatingMangled := Mangle(cc.Compiler.MangledPath, "NoisyTypes", []Type{F64})
-	integerInfo := cc.Compiler.FuncCache[integerMangled]
-	floatingInfo := cc.Compiler.FuncCache[floatingMangled]
-	require.Len(t, integerInfo.CFGResult.Errors, 1)
-	require.Len(t, floatingInfo.CFGResult.Errors, 1)
-	require.NotSame(t, integerInfo.CFGResult.Errors[0], floatingInfo.CFGResult.Errors[0],
-		"each specialization must retain its immutable analysis result")
-	require.Equal(t, integerInfo.CFGResult.Errors[0].Error(), floatingInfo.CFGResult.Errors[0].Error())
-	require.Same(t, integerInfo.CFGResult.Errors[0], errors[0],
-		"replay must retain the first source-ordered diagnostic")
-}
-
-func TestCFGReplayPreservesDistinctDiagnostics(t *testing.T) {
-	code := mustParseCode(t, `result = NoisyPair(x)
-    firstUnused = x + 1
-    secondUnused = x + 2
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayDistinctDiagnostics", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, errors := compileCFGReplayScript(t, ctx, cc, t.Name(), `integer = NoisyPair(1)
-floating = NoisyPair(2.0)
-integer, floating`)
-	require.Len(t, errors, 2, "distinct source diagnostics must survive specialization deduplication")
-	require.Contains(t, errors[0].Msg, `"secondUnused"`)
-	require.Contains(t, errors[1].Msg, `"firstUnused"`)
-
-	integerMangled := Mangle(cc.Compiler.MangledPath, "NoisyPair", []Type{I64})
-	floatingMangled := Mangle(cc.Compiler.MangledPath, "NoisyPair", []Type{F64})
-	integerInfo := cc.Compiler.FuncCache[integerMangled]
-	floatingInfo := cc.Compiler.FuncCache[floatingMangled]
-	require.Len(t, integerInfo.CFGResult.Errors, 2)
-	require.Len(t, floatingInfo.CFGResult.Errors, 2)
-	for index := range errors {
-		require.Same(t, integerInfo.CFGResult.Errors[index], errors[index])
-	}
-}
-
-func TestUnreachableCachedCFGDiagnosticsDoNotLeak(t *testing.T) {
-	code := mustParseCode(t, `result = Noisy(x)
-    unused = x + 1
-    result = x
-
-result = Clean(x)
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayUnreachable", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, noisyErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Noisy", "value = Noisy(1)\nvalue")
-	require.Len(t, noisyErrors, 1)
-
-	noisyMangled := Mangle(cc.Compiler.MangledPath, "Noisy", []Type{I64})
-	noisyInfo := cc.Compiler.FuncCache[noisyMangled]
-	require.NotNil(t, noisyInfo)
-	require.NotNil(t, noisyInfo.CFGResult)
-	require.Same(t, noisyInfo.CFGResult.Errors[0], noisyErrors[0])
-
-	_, cleanErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Clean", "value = Clean(1)\nvalue")
-	require.Empty(t, cleanErrors,
-		"a cached diagnostic must not replay when its specialization is unreachable")
-	require.Same(t, noisyInfo, cc.Compiler.FuncCache[noisyMangled])
-}
-
-func TestWrapperReplaysSettledCalleeDiagnostics(t *testing.T) {
-	code := mustParseCode(t, `result = NoisyLeaf(x)
-    leafDead = x + 1
-    result = x
-
-result = Wrapper(x)
-    result = NoisyLeaf(x)
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplaySettledCallee", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, leafErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Leaf", "value = NoisyLeaf(1)\nvalue")
-	require.Len(t, leafErrors, 1)
-
-	leafMangled := Mangle(cc.Compiler.MangledPath, "NoisyLeaf", []Type{I64})
-	leafInfo := cc.Compiler.FuncCache[leafMangled]
-	require.True(t, leafInfo.Settled)
-	require.NotNil(t, leafInfo.CFGResult)
-	require.Same(t, leafInfo.CFGResult.Errors[0], leafErrors[0])
-
-	_, wrapperErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Wrapper", "value = Wrapper(1)\nvalue")
-	require.Len(t, wrapperErrors, 1)
-	require.Same(t, leafErrors[0], wrapperErrors[0])
-
-	wrapperMangled := Mangle(cc.Compiler.MangledPath, "Wrapper", []Type{I64})
-	wrapperInfo := cc.Compiler.FuncCache[wrapperMangled]
-	require.True(t, wrapperInfo.Settled)
-	require.NotNil(t, wrapperInfo.CFGResult)
-	require.Equal(t, []string{leafMangled}, wrapperInfo.CFGResult.DirectCallees,
-		"persistent replay edges must include callees settled before the wrapper batch")
-}
-
-func TestPrintOnlyUserCallReplaysCFGDiagnostics(t *testing.T) {
-	code := mustParseCode(t, `result = NoisyPrint(x)
-    printDead = x + 1
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayPrintOnly", "", code)
-	require.Empty(t, cc.Compile())
-
-	sc, errors := compileCFGReplayScript(t, ctx, cc, t.Name(), "NoisyPrint(1)")
-	require.Len(t, errors, 1)
-	require.Contains(t, errors[0].Msg, `"printDead"`)
-
-	mangled := Mangle(cc.Compiler.MangledPath, "NoisyPrint", []Type{I64})
-	directCallees, _ := collectSpecializationCallEdges(sc.Compiler, sc.ScriptMangled, sc.Program.Statements)
-	require.Equal(t, []string{mangled}, directCallees,
-		"a user call reached only through print arguments must be a replay root")
-	require.Same(t, cc.Compiler.FuncCache[mangled].CFGResult.Errors[0], errors[0])
-}
-
-func TestCFGReplayDeduplicatesScalarCompanion(t *testing.T) {
-	code := mustParseCode(t, `result = GatherNoisy(arr)
-    i = 0:3
-    result = [ScaleNoisy(arr[i])]
-
-result = ScaleNoisy(x)
-    unusedScale = x
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayScalarCompanion", "", code)
-	require.Empty(t, cc.Compile())
-
-	sc, errors := compileCFGReplayScript(t, ctx, cc, t.Name(), `arr = [10 20 30]
-result = GatherNoisy(arr)
-result`)
-	require.Len(t, errors, 1, "a primary specialization and scalar companion share one source diagnostic")
-
-	gatherMangled := Mangle(cc.Compiler.MangledPath, "GatherNoisy", []Type{Array{ElemType: I64, Rank: 1}})
-	gatherTemplate, ok := cc.lookupFuncTemplate("GatherNoisy", 1)
-	require.True(t, ok)
-	gatherCalls := collectBodyCalls(gatherTemplate.Body.Statements)
-	require.Len(t, gatherCalls, 1)
-	gatherCall := gatherCalls[0]
-	callInfo := sc.Compiler.ExprCache[key(gatherMangled, gatherCall)]
-	require.True(t, callInfo.ScalarCallVariantEnsured)
-
-	primaryMangled := Mangle(cc.Compiler.MangledPath, "ScaleNoisy", callInfo.CallParamTypes)
-	scalarMangled := Mangle(cc.Compiler.MangledPath, "ScaleNoisy", callInfo.ScalarCallParamTypes)
-	require.NotEqual(t, primaryMangled, scalarMangled)
-	primaryInfo := cc.Compiler.FuncCache[primaryMangled]
-	scalarInfo := cc.Compiler.FuncCache[scalarMangled]
-	require.Len(t, primaryInfo.CFGResult.Errors, 1)
-	require.Len(t, scalarInfo.CFGResult.Errors, 1)
-	require.NotSame(t, primaryInfo.CFGResult.Errors[0], scalarInfo.CFGResult.Errors[0],
-		"both actual lowering targets must remain independently analyzed")
-	require.Equal(t, primaryInfo.CFGResult.Errors[0].Error(), scalarInfo.CFGResult.Errors[0].Error())
-	require.Same(t, primaryInfo.CFGResult.Errors[0], errors[0])
-}
-
-func TestDiamondCFGReplayIsOnceAndDeterministic(t *testing.T) {
-	code := mustParseCode(t, `result = Shared(x)
-    sharedDead = x + 1
-    result = x
-
-result = Left(x)
-    leftDead = x + 2
-    result = Shared(x)
-
-result = Right(x)
-    rightDead = x + 3
-    result = Shared(x)
-
-result = Diamond(x)
-    diamondDead = x + 4
-    left = Left(x)
-    right = Right(x)
-    result = left + right
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgReplayDiamond", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, errors := compileCFGReplayScript(t, ctx, cc, t.Name(), "value = Diamond(1)\nvalue")
-	require.Len(t, errors, 4)
-
-	for i, name := range []string{"diamondDead", "leftDead", "sharedDead", "rightDead"} {
-		require.Contains(t, errors[i].Msg, `"`+name+`"`,
-			"diagnostics must replay in root-first depth-first source order")
-	}
-
-	sharedMangled := Mangle(cc.Compiler.MangledPath, "Shared", []Type{I64})
-	sharedError := cc.Compiler.FuncCache[sharedMangled].CFGResult.Errors[0]
-	sharedOccurrences := 0
-	for _, cfgError := range errors {
-		if cfgError == sharedError {
-			sharedOccurrences++
-		}
-	}
-	require.Equal(t, 1, sharedOccurrences,
-		"the visited set must replay a shared diamond callee exactly once")
-}
-
-func TestCFGResultsAreIndependentPerType(t *testing.T) {
-	code := mustParseCode(t, `result = MaskOrKeep(x)
-    result = x
-    result = x > 0
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "cfgPerSpecialization", "", code)
-	require.Empty(t, cc.Compile())
-
-	_, scalarErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Scalar", "value = MaskOrKeep(1)\nvalue")
-	require.Empty(t, scalarErrors,
-		"a scalar comparison may skip its write, so the preceding output remains live")
-
-	scalarMangled := Mangle(cc.Compiler.MangledPath, "MaskOrKeep", []Type{I64})
-	scalarResult := cc.Compiler.FuncCache[scalarMangled].CFGResult
-	require.NotNil(t, scalarResult)
-	require.Empty(t, scalarResult.Errors)
-
-	_, arrayErrors := compileCFGReplayScript(t, ctx, cc, t.Name()+"Array", "value = MaskOrKeep([1 2])\nvalue")
-	require.NotEmpty(t, arrayErrors,
-		"an array comparison materializes unconditionally and overwrites the preceding output")
-
-	arrayMangled := Mangle(cc.Compiler.MangledPath, "MaskOrKeep", []Type{
-		Array{ElemType: I64, Rank: 1},
-	})
-	arrayResult := cc.Compiler.FuncCache[arrayMangled].CFGResult
-	require.NotNil(t, arrayResult)
-	require.NotSame(t, scalarResult, arrayResult)
-	require.NotEmpty(t, arrayResult.Errors)
-	require.Contains(t, arrayResult.Errors[0].Msg, `unconditional assignment to "result"`)
-}
diff --git a/compiler/cfg_test.go b/compiler/cfg_test.go
index 80732e67..83e27076 100644
--- a/compiler/cfg_test.go
+++ b/compiler/cfg_test.go
@@ -1,6 +1,9 @@
 package compiler
 
 import (
+	"fmt"
+	"maps"
+	"slices"
 	"strings"
 	"testing"
 
@@ -46,7 +49,9 @@ func TestCFGAnalysis(t *testing.T) {
 	})
 }
 
-func TestFunctionDataflowWaitsForSpecialization(t *testing.T) {
+// Flow checks run once per template, from its text, whether or not anything
+// calls it.
+func TestFunctionDataflowRunsOncePerTemplate(t *testing.T) {
 	code := `r = Unreachable(x)
     temporary = x + 1
     temporary = x + 2
@@ -57,10 +62,6 @@ func TestFunctionDataflowWaitsForSpecialization(t *testing.T) {
 
 	cc := NewCodeCompiler(ctx, "unreachableLocalDeadStore", "", mustParseCode(t, code))
 	errs := cc.Compile()
-	require.Empty(t, errs)
-
-	sc := NewScriptCompiler(ctx, t.Name(), mustParseScript(t, "result = Unreachable(1)\nresult"), cc)
-	errs = sc.Compile()
 	require.Len(t, errs, 3)
 	assertHasExpectedError(t, errs, `unconditional assignment to "temporary" overwrites a previous value that was never used`)
 
@@ -329,12 +330,22 @@ value, kept, echo`,
 			input: `"Value: -x%s"`,
 		},
 		{
-			// The callee may skip its write, leaving the destination's previous
-			// value in place, so that previous write is live.
-			name: "Write then Skippable Call Root",
-			code: `res = maybeWrite(x)
+			// The callee keeps the old value through an input, so the call
+			// reads the earlier write.
+			name: "Write then Call Keeping Old Value",
+			code: `res = maybeWrite(prev, x)
+    res = prev
     res = x > 0 42`,
-			input: "x = 7\nx = maybeWrite(-1)\nx",
+			input: "x = 7\nx = maybeWrite(x, -1)\nx",
+		},
+		{
+			// One body serves scalar and array arguments: the comparison counts
+			// as possibly skipping for both, so the default stays live.
+			name: "Default Before Comparison For Scalar And Array",
+			code: `out = Pos(prev, x)
+    out = prev
+    out = x > 0`,
+			input: "s = Pos(9, -1)\nm = Pos([]0, [1 -2 3])\ns, m",
 		},
 		{
 			// A condition below the value root still leaves the whole RHS able
@@ -356,13 +367,14 @@ value, kept, echo`,
 		{
 			// Writing an output twice never reads it, and a call may target it.
 			name: "Output Rewritten And Targeted By Nested Call",
-			code: `res = maybe(x)
+			code: `res = maybe(prev, x)
+    res = prev
     res = x > 0 x
 
 res = refine(x)
     res = x
     res = x > 5 x * x
-    res = maybe(x)`,
+    res = maybe(res, x)`,
 			input: "x = refine(3)\nx",
 		},
 		{
@@ -480,8 +492,9 @@ func getErrorTestCases() []cfgTestCase {
 			errorContains: `output "res" is read where it may still be unassigned`,
 		},
 		{
-			// A call that may leave its output unwritten does not assign it.
-			name: "Output Read After Skippable Call",
+			// A body that can skip its write is rejected at its definition, so
+			// a caller can count on the call writing its output.
+			name: "Skippable Body Rejected At Definition",
 			code: `res = maybe(x)
     res = x > 0 x
 
@@ -489,21 +502,7 @@ res = chained(x)
     res = maybe(x)
     res = res + 1`,
 			input:         "x = chained(-1)\nx",
-			errorContains: `output "res" is read where it may still be unassigned`,
-		},
-		{
-			// Two seed-preserving calls in a row still leave the caller's seed
-			// in place, so the read after them is rejected.
-			name: "Output Read After Two Seed Preserving Calls",
-			code: `res = maybe(x)
-    res = x > 0 x
-
-res = twice(x)
-    res = maybe(x)
-    res = maybe(x)
-    res = res + 1`,
-			input:         "x = twice(-1)\nx",
-			errorContains: `output "res" is read where it may still be unassigned`,
+			errorContains: `output "res" may be left unassigned`,
 		},
 		{
 			// A marker naming an output is a read even before any assignment,
@@ -883,62 +882,15 @@ func TestFormattingReadsRemainStructural(t *testing.T) {
 	}
 }
 
-func TestSpecializationReadsSeedBeforeWrite(t *testing.T) {
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-
-	code := mustParseCode(t, `res = Seeded(x)
-    res = x
-    res = Preserve(x)`)
-	template := code.Statements[0].(*ast.FuncStatement)
-	first := template.Body.Statements[0].(*ast.LetStatement)
-	second := template.Body.Statements[1].(*ast.LetStatement)
-	info := &FuncInfo{
-		StatementEffects: map[*ast.LetStatement]StatementEffect{
-			first: {
-				Writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}},
-			},
-			second: {
-				Writes:    []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}},
-				ReadsSeed: []int{0},
-			},
-		},
-	}
-	cc := NewCodeCompiler(ctx, "seededSpecialization", "", code)
-	cfg := NewCFG(cc)
-
-	cfg.AnalyzeSpecialization(template, info)
-
-	require.Empty(t, cfg.Errors)
-}
-
-func TestSpecializationPrintReadKeepsLocalLive(t *testing.T) {
+func TestTemplatePrintReadKeepsLocalLive(t *testing.T) {
 	ctx := llvm.NewContext()
 	defer ctx.Dispose()
 
-	code := mustParseCode(t, `res = Printed(x)
+	cc := NewCodeCompiler(ctx, "printedTemplate", "", mustParseCode(t, `res = Printed(x)
     local = x + 1
     local
-    res = x`)
-	template := code.Statements[0].(*ast.FuncStatement)
-	local := template.Body.Statements[0].(*ast.LetStatement)
-	output := template.Body.Statements[2].(*ast.LetStatement)
-	info := &FuncInfo{
-		StatementEffects: map[*ast.LetStatement]StatementEffect{
-			local: {
-				Writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}},
-			},
-			output: {
-				Writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}},
-			},
-		},
-	}
-	cc := NewCodeCompiler(ctx, "printedSpecialization", "", code)
-	cfg := NewCFG(cc)
-
-	cfg.AnalyzeSpecialization(template, info)
-
-	require.Empty(t, cfg.Errors)
+    res = x`))
+	require.Empty(t, cc.Compile())
 }
 
 func TestTypedEventsUseSparseTargetIndices(t *testing.T) {
@@ -972,15 +924,12 @@ func TestCFGRejectsMissingStatementEffects(t *testing.T) {
 	ctx := llvm.NewContext()
 	defer ctx.Dispose()
 
-	code := mustParseCode(t, `res = MissingEffects(x)
-    res = x`)
-	template := code.Statements[0].(*ast.FuncStatement)
-	info := &FuncInfo{StatementEffects: make(map[*ast.LetStatement]StatementEffect)}
-	cc := NewCodeCompiler(ctx, "missingEffects", "", code)
+	cc := NewCodeCompiler(ctx, t.Name(), "", ast.NewCode())
+	program := mustParseScript(t, "value = 1\nvalue")
 	cfg := NewCFG(cc)
 
-	require.PanicsWithValue(t, `internal: missing CFG effects for statement "res = x"`, func() {
-		cfg.AnalyzeSpecialization(template, info)
+	require.PanicsWithValue(t, `internal: missing CFG effects for statement "value = 1"`, func() {
+		cfg.AnalyzeScript(program.Statements, make(map[*ast.LetStatement]StatementEffect))
 	})
 }
 
@@ -1136,3 +1085,714 @@ func assertMessageFound(t *testing.T, messages []string, expectedMessage string)
 	}
 	assert.True(t, found, "expected an error containing %q, got: %v", expectedMessage, messages)
 }
+
+func unassignedOutputMessage(name string) string {
+	return fmt.Sprintf("output %q may be left unassigned; assign it unconditionally first, or pass the previous value as an input and initialize from it (%s = prev), with each caller passing its destination as that input", name, name)
+}
+
+// Every body that runs writes every output. The template check reads the
+// text: a statement gate, a value that can fail, or a range that may be empty
+// can skip a write, for every argument type.
+func TestOutputsMustBeDefinitelyAssigned(t *testing.T) {
+	tests := []struct {
+		name       string
+		code       string
+		unassigned []string
+	}{
+		{
+			name: "Gated",
+			code: `out = Maybe(x)
+    out = x > 0 x`,
+			unassigned: []string{"out"},
+		},
+		{
+			// A comparison counts as possibly skipping even where an array
+			// argument would make it a mask.
+			name: "Comparison",
+			code: `out = Less(x, y)
+    out = x < y`,
+			unassigned: []string{"out"},
+		},
+		{
+			name: "CheckedAccess",
+			code: `out = At(arr, i)
+    out = arr[i]`,
+			unassigned: []string{"out"},
+		},
+		{
+			// Complementary conditions are not recognized: for floats, a NaN
+			// fails both.
+			name: "ComplementaryGates",
+			code: `y = Fib(n)
+    y = n <= 1 n
+    y = n > 1 Fib(n - 1) + Fib(n - 2)`,
+			unassigned: []string{"y"},
+		},
+		{
+			name: "DefaultThenOverride",
+			code: `y = Fib(n)
+    y = n
+    y = n > 1 Fib(n - 1) + Fib(n - 2)`,
+		},
+		{
+			name: "PrevThenComparison",
+			code: `out = Pos(prev, x)
+    out = prev
+    out = x > 0`,
+		},
+		{
+			name: "LocalAbsorbsCheckedAccess",
+			code: `out = At(arr, i)
+    t = arr[i]
+    out = t`,
+		},
+		{
+			// A caller counts a call as writing every output, so only the
+			// body that can skip is reported.
+			name: "CallerIsNotReportedAgain",
+			code: `res = maybe(x)
+    res = x > 0 x
+
+out = chained(x)
+    out = maybe(x)
+    out = out + 1`,
+			unassigned: []string{"res"},
+		},
+		{
+			name: "EveryOutputIsChecked",
+			code: `x, y = IsEven(n)
+    x, y = n != 0 IsOdd(n - 1)
+    x = n == 0 "yes"
+
+x, y = IsOdd(n)
+    x, y = "no", "yes"
+    x, y = n != 0 IsEven(n - 1)`,
+			unassigned: []string{"x", "y"},
+		},
+		{
+			name: "LocalRangeMayBeEmpty",
+			code: `out = Tail(n)
+    j = 0:n
+    out = j * 2`,
+			unassigned: []string{"out"},
+		},
+		{
+			name: "InlineRangeMayBeEmpty",
+			code: `out = Shift(n)
+    out = n + (0:n)`,
+			unassigned: []string{"out"},
+		},
+		{
+			name: "NonemptyRangeLiteralAlwaysRuns",
+			code: `out = Last(x)
+    out = x + (0:3)`,
+		},
+		{
+			name: "LocalRangeWithDefault",
+			code: `out = F(prev, n)
+    r = 0:n
+    out = prev
+    out = r * 2`,
+		},
+		{
+			name: "ScalarCallOutput",
+			code: `y = Helper(x)
+    y = x + 1
+
+out = F(x)
+    y = Helper(x)
+    out = y + 1`,
+		},
+		{
+			// A gate that names a range iterates it, so the value reads the
+			// element and the binding holds a scalar.
+			name: "GateIteratesItsRange",
+			code: `out = F(n)
+    stream = 0:n
+    last = stream > 2 stream
+    out = last + 1`,
+		},
+		{
+			// A gate makes its value a computation, so a range the condition
+			// does not name iterates too and kept holds an element.
+			name: "GateIteratesAnotherRange",
+			code: `out = F(n)
+    other = 0:3
+    stream = 0:n
+    kept = other > 1 stream
+    out = kept * 2`,
+		},
+		{
+			// A literal or binding under && is iterated.
+			name: "AndIteratesLiteral",
+			code: `out = F(n)
+    last = n > 0 && 0:5
+    out = last + 1`,
+		},
+		{
+			name: "AndIteratesBinding",
+			code: `out = F(n)
+    stream = 0:n
+    last = n > 0 && stream
+    out = last + 1`,
+		},
+		{
+			// A main marker formats the range it names, so the write always
+			// happens.
+			name: "MainMarkerFormatsItsRange",
+			code: `out = F(n)
+    r = 0:n
+    out = "v -r"`,
+		},
+		{
+			// A width or precision consumes a range as numbers.
+			name: "SpecifierRangeIterates",
+			code: `out = F(n)
+    w = 1:n
+    out = "-n%(-w)d"`,
+			unassigned: []string{"out"},
+		},
+		{
+			// An input's marker takes the specifier after it, so w is a width
+			// and iterates.
+			name: "InputMarkerTakesItsSpecifier",
+			code: `out = Show(p)
+    w = 1:p
+    out = "-p%(-w)d"`,
+			unassigned: []string{"out"},
+		},
+		{
+			// A name defined further down is plain text, so the -w after it is
+			// a main marker and formats its range.
+			name: "LaterNameIsText",
+			code: `out, later = Late(p)
+    w = 1:p
+    out = "-q%(-w)d"
+    q = p + 1
+    later = q`,
+		},
+		{
+			// A && fills its right operand's targets.
+			name: "AndTakesRightOperandSlots",
+			code: `a, b = Pair(x)
+    a, b = x, x
+
+a, b, c = F(x)
+    a, b, c = x > 0 && Pair(x), x`,
+			unassigned: []string{"a", "b"},
+		},
+		{
+			// A call's arity counts every value its arguments yield, so the
+			// targets line up with Count's outputs and only c can be skipped.
+			name: "TargetsFollowCallOutputs",
+			code: `left, right = Tags(n)
+    left, right = n, n + 1
+
+out, tag = Count(left, right, n)
+    out = n + 1
+    tag = left + right
+
+a, b, c = F(arr, n)
+    a, b, c = Count(Tags(n), n), arr[0]`,
+			unassigned: []string{"c"},
+		},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			ctx := llvm.NewContext()
+			defer ctx.Dispose()
+
+			cc := NewCodeCompiler(ctx, test.name, "", mustParseCode(t, test.code))
+			want := make([]string, len(test.unassigned))
+			for i, name := range test.unassigned {
+				want[i] = unassignedOutputMessage(name)
+			}
+
+			require.Equal(t, want, extractErrorMessages(cc.Compile()))
+		})
+	}
+}
+
+func TestUnassignedOutputIsReportedAtTheHeader(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, t.Name(), "", mustParseCode(t, `out = Maybe(x)
+    out = x > 0 x`))
+	errs := cc.Compile()
+
+	require.Len(t, errs, 1)
+	require.Equal(t, unassignedOutputMessage("out"), errs[0].Msg)
+	require.Equal(t, 1, errs[0].Token.Line)
+	require.Equal(t, 1, errs[0].Token.Column)
+}
+
+// The template checks classify each write from the text, so they first report
+// text the classification cannot read, which the solver rejects in any
+// specialization, and check no flow over it.
+func TestUnclassifiableTemplateTextIsReported(t *testing.T) {
+	tests := []struct {
+		name   string
+		code   string
+		errors []string
+	}{
+		{
+			// The value that can fail does not mark the targets as possibly
+			// skipped.
+			name: "ValueCountMismatch",
+			code: `a, b = Pair(x)
+    a, b = x, x
+
+a, b, c = F(arr, x)
+    a, b, c = Pair(x), arr[0], x`,
+			errors: []string{"assignment mismatch: 3 targets but 4 values"},
+		},
+		{
+			name: "OneValueForTwoTargets",
+			code: `a, b = F(x)
+    a, b = x`,
+			errors: []string{"assignment mismatch: 2 targets but 1 value"},
+		},
+		{
+			name: "UndefinedFunction",
+			code: `y = F(x)
+    y = Missing(x)`,
+			errors: []string{"undefined function: Missing"},
+		},
+		{
+			// A call names a template by the number of values its arguments
+			// yield.
+			name: "WrongArgumentCount",
+			code: `a, b = Pair(x)
+    a, b = x, x
+
+y = F(x)
+    y = Pair(x, x)`,
+			errors: []string{"undefined function: Pair"},
+		},
+		{
+			name: "UndefinedFunctionInConditionAndArgument",
+			code: `y = F(x)
+    y = x
+    y = Check(x) > 0 Inc(Next(x))
+
+out = Inc(n)
+    out = n + 1`,
+			errors: []string{"undefined function: Check", "undefined function: Next"},
+		},
+		{
+			name: "UndefinedFunctionInPrint",
+			code: `y = F(x)
+    y = x
+    Missing(x)`,
+			errors: []string{"undefined function: Missing"},
+		},
+		{
+			// The solver counts an unknown call as one value and reports both.
+			name: "UndefinedFunctionInTuple",
+			code: `a, b = F(x)
+    a, b = Missing(x)`,
+			errors: []string{"undefined function: Missing", "assignment mismatch: 2 targets but 1 value"},
+		},
+		{
+			// An operator whose sides do not line up yields one value, as the
+			// solver counts it, so the assignment does not line up either.
+			name: "OperandCountMismatch",
+			code: `p, q = Pair(n)
+    p, q = n, n + 1
+
+a, b = F(n)
+    a, b = Pair(n) * 2`,
+			errors: []string{`operand mismatch: "*" has 2 values on its left but 1 value on its right`, "assignment mismatch: 2 targets but 1 value"},
+		},
+		{
+			name: "OrAlternativesCountMismatch",
+			code: `p, q = Pair(n)
+    p, q = n, n + 1
+
+y = Inc(n)
+    y = n + 1
+
+a, b = F(n)
+    a, b = Pair(n > 0) || Inc(3)`,
+			errors: []string{`operand mismatch: "||" has 2 values on its left but 1 value on its right`, "assignment mismatch: 2 targets but 1 value"},
+		},
+		{
+			name: "NestedMismatchCountsOneValue",
+			code: `p, q = Pair(n)
+    p, q = n, n + 1
+
+y = F(n)
+    y = (Pair(n) * 2) + 1`,
+			errors: []string{`operand mismatch: "*" has 2 values on its left but 1 value on its right`},
+		},
+		{
+			// A && condition folds onto one value or broadcasts to several,
+			// but two conditions cannot gate three values.
+			name: "AndArityMismatch",
+			code: `p, q = Pair(n)
+    p, q = n, n + 1
+
+a, b, c = Three(n)
+    a, b, c = n, n, n
+
+a, b, c = F(n)
+    a, b, c = Pair(n > 0) && Three(n)`,
+			errors: []string{"logical AND condition arity must match the value's, fold to one, or broadcast from one — got 2 and 3", "assignment mismatch: 3 targets but 1 value"},
+		},
+		{
+			// y's gated write waits until the template's text classifies.
+			name: "NoFlowChecksOverUnclassifiableText",
+			code: `y, z = F(x)
+    y = x > 0 x
+    z = Missing(x)`,
+			errors: []string{"undefined function: Missing"},
+		},
+		{
+			// Every template's text is checked, and Maybe's flow error waits
+			// until all of it classifies.
+			name: "FlowChecksWaitForEveryTemplate",
+			code: `y = F(x)
+    y = Missing(x)
+
+out = Maybe(x)
+    out = x > 0 x
+
+z = G(x)
+    z = Gone(x)`,
+			errors: []string{"undefined function: Missing", "undefined function: Gone"},
+		},
+		{
+			// The text is read even when the structure is invalid; the flow
+			// is not.
+			name: "ReportedWithStructuralErrors",
+			code: `y = F(x, unused)
+    y = Missing(x)`,
+			errors: []string{`input parameter "unused" is never read`, "undefined function: Missing"},
+		},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			ctx := llvm.NewContext()
+			defer ctx.Dispose()
+
+			cc := NewCodeCompiler(ctx, test.name, "", mustParseCode(t, test.code))
+			require.Equal(t, test.errors, extractErrorMessages(cc.Compile()))
+		})
+	}
+}
+
+// Unclassifiable text is reported where the solver reports it: an assignment
+// at its = and a call at its parenthesis.
+func TestUnclassifiableTemplateTextPositions(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, t.Name(), "", mustParseCode(t, `a, b = F(x)
+    a, b = Missing(x)`))
+	errs := cc.Compile()
+
+	require.Len(t, errs, 2)
+	positions := make([][2]int, len(errs))
+	for i, err := range errs {
+		positions[i] = [2]int{err.Token.Line, err.Token.Column}
+	}
+	require.Equal(t, [][2]int{{2, 19}, {2, 10}}, positions)
+}
+
+func rangeOutputMessage(name string) string {
+	return fmt.Sprintf("output %q cannot hold a range; return its bounds and build the range where it is used", name)
+}
+
+// A function cannot return a range: it returns the bounds, and its caller
+// builds the range.
+func TestFunctionsCannotReturnRanges(t *testing.T) {
+	tests := []struct {
+		name   string
+		code   string
+		errors []string
+	}{
+		{
+			name: "RangeLiteralOutput",
+			code: `r = MakeRange(n)
+    r = 0:n`,
+			errors: []string{rangeOutputMessage("r")},
+		},
+		{
+			name: "OneOutputOfSeveral",
+			code: `r, k = Two(n)
+    r, k = 0:n, n`,
+			errors: []string{rangeOutputMessage("r")},
+		},
+		{
+			// Under a gate a range literal iterates, so the output receives an
+			// element, and the gate can skip the write.
+			name: "GatedRangeLiteralIterates",
+			code: `out = F(n)
+    out = n > 0 0:n`,
+			errors: []string{unassignedOutputMessage("out")},
+		},
+		{
+			name: "CopiedRangeOutput",
+			code: `out = F(n)
+    r = 0:n
+    out = r`,
+			errors: []string{rangeOutputMessage("out")},
+		},
+		{
+			name: "IteratedRangeOutput",
+			code: `out = F(prev, n)
+    r = 0:n
+    out = prev
+    out = r * 2`,
+		},
+		{
+			name: "CollectedRangeOutput",
+			code: `out = F(n)
+    out = [0:n]`,
+		},
+		{
+			name: "BoundsOutputs",
+			code: `lo, hi = Bounds(n)
+    lo, hi = 0, n
+
+out = F(n)
+    lo, hi = Bounds(n)
+    r = lo:hi
+    out = [r]`,
+		},
+		{
+			// G's checks read the call as a value, which would make its
+			// default a dead store, so they wait for MakeRange's error.
+			name: "CallerAfterRangeOutput",
+			code: `res = MakeRange(n)
+    res = 0:n
+
+out = G(n)
+    out = 0
+    out = MakeRange(n) + 1`,
+			errors: []string{rangeOutputMessage("res")},
+		},
+		{
+			name: "CallerBeforeRangeOutput",
+			code: `out = G(n)
+    out = 0
+    out = MakeRange(n) + 1
+
+res = MakeRange(n)
+    res = 0:n`,
+			errors: []string{rangeOutputMessage("res")},
+		},
+		{
+			// Fwd takes the call's value, so H's call to Fwd misleads it too.
+			name: "CallerThroughForwardingCall",
+			code: `res = MakeRange(n)
+    res = 0:n
+
+v = Fwd(n)
+    v = MakeRange(n)
+
+out = H(n)
+    out = 0
+    out = Fwd(n) + 1`,
+			errors: []string{rangeOutputMessage("res")},
+		},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			ctx := llvm.NewContext()
+			defer ctx.Dispose()
+
+			cc := NewCodeCompiler(ctx, test.name, "", mustParseCode(t, test.code))
+			want := test.errors
+			if want == nil {
+				want = []string{}
+			}
+			require.Equal(t, want, extractErrorMessages(cc.Compile()))
+		})
+	}
+}
+
+// A range literal assigned whole always writes, even an empty one, so
+// overwriting it unread is reported as for any definite write.
+func TestRangeLiteralWriteIsDefinite(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, t.Name(), "", mustParseCode(t, `out = F(n)
+    r = 0:n
+    r = 1:n
+    out = [r]`))
+	require.Equal(t, []string{
+		`unconditional assignment to "r" overwrites a previous value that was never used. It was previously written at line 2:5`,
+		`value assigned to "r" is never used`,
+	}, extractErrorMessages(cc.Compile()))
+}
+
+// Copying a range always writes, even an empty one, so overwriting a copy
+// unread is reported as for any definite write.
+func TestRangeCopyWriteIsDefinite(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, t.Name(), "", mustParseCode(t, `out = F(n)
+    r = 0:n
+    c = r
+    c = r
+    out = [c]`))
+	require.Equal(t, []string{
+		`unconditional assignment to "c" overwrites a previous value that was never used. It was previously written at line 3:5`,
+		`value assigned to "c" is never used`,
+	}, extractErrorMessages(cc.Compile()))
+}
+
+func TestRangeOutputIsReportedAtItsAssignment(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, t.Name(), "", mustParseCode(t, `r, k = Two(n)
+    k = n
+    r = 0:n`))
+	errs := cc.Compile()
+
+	require.Len(t, errs, 1)
+	require.Equal(t, 3, errs[0].Token.Line)
+	require.Equal(t, 5, errs[0].Token.Column)
+}
+
+// The template checks read from the text which bindings hold a Range, and
+// settlement checks that the solved types agree, so each way a value holds
+// or iterates a range is pinned here against the solver.
+func TestTextRangeSummaryAgreesWithSolver(t *testing.T) {
+	tests := []struct {
+		name   string
+		code   string
+		ranges []string
+	}{
+		{
+			name: "DescriptorCopy",
+			code: `out = F(n)
+    stream = 0:n
+    kept = stream
+    out = [kept]`,
+			ranges: []string{"kept", "stream"},
+		},
+		{
+			name: "OperationIterates",
+			code: `out = F(n)
+    stream = 0:n
+    out = n
+    out = stream + 0`,
+			ranges: []string{"stream"},
+		},
+		{
+			name: "GateIteratesItsRange",
+			code: `out = F(n)
+    stream = 0:n
+    out = n
+    out = stream > 2 stream`,
+			ranges: []string{"stream"},
+		},
+		{
+			name: "GateIteratesAnotherRange",
+			code: `out = F(n)
+    other = 0:3
+    stream = 0:n
+    kept = other > 1 stream
+    out = [kept]`,
+			ranges: []string{"other", "stream"},
+		},
+		{
+			name: "GatedLiteralIterates",
+			code: `out = F(n)
+    stream = 0:n
+    kept = stream > 1 0:9
+    out = [kept]`,
+			ranges: []string{"stream"},
+		},
+		{
+			// The condition only collects stream, but the gated value still
+			// iterates it.
+			name: "CollectorInGate",
+			code: `n = Size(xs)
+    t = xs[0]
+    n = t + 2
+
+out = F(n)
+    stream = 0:n
+    kept = Size([stream]) > 1 stream
+    out = [kept]`,
+			ranges: []string{"stream"},
+		},
+		{
+			name: "SpecifierInGateIterates",
+			code: `out = F(n)
+    w = 0:n
+    kept = "-n%(-w)d" > "" w
+    out = [kept]`,
+			ranges: []string{"w"},
+		},
+		{
+			name: "AndIteratesLiteral",
+			code: `out = F(n)
+    last = n > 0 && 0:5
+    out = [last]`,
+		},
+		{
+			name: "AndIteratesBinding",
+			code: `out = F(n)
+    stream = 0:n
+    last = n > 0 && stream
+    out = [last]`,
+			ranges: []string{"stream"},
+		},
+		{
+			// A range in one value of a tuple holds only that target.
+			name: "RangeInOneSlotOfATuple",
+			code: `out = F(n)
+    kept, k = 0:n, n
+    out = [kept] ⊕ [k]`,
+			ranges: []string{"kept"},
+		},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			ctx := llvm.NewContext()
+			defer ctx.Dispose()
+
+			cc := NewCodeCompiler(ctx, test.name, "", mustParseCode(t, test.code))
+			require.Empty(t, cc.Compile())
+
+			ranges := slices.Sorted(maps.Keys(cc.rangeBindings[funcKey{name: "F", arity: 1}]))
+			if test.ranges == nil {
+				require.Empty(t, ranges)
+			} else {
+				require.Equal(t, test.ranges, ranges)
+			}
+
+			sc := NewScriptCompiler(ctx, t.Name(), mustParseScript(t, "v = F(5)\nv"), cc)
+			require.Empty(t, sc.Compile())
+		})
+	}
+}
+
+func TestSettledRangeDisagreementIsInternalError(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, t.Name(), "", mustParseCode(t, `out = F(n)
+    stream = 0:n
+    out = [stream]`))
+	require.Empty(t, cc.Compile())
+	delete(cc.rangeBindings[funcKey{name: "F", arity: 1}], "stream")
+
+	ts := NewTypeSolver(NewScriptCompiler(ctx, t.Name(), mustParseScript(t, "v = F(5)\nv"), cc))
+	require.PanicsWithValue(t,
+		fmt.Sprintf("internal: F solves %q as %s, which disagrees with its template's text range summary", "stream", Range{Iter: I64}),
+		ts.Solve,
+	)
+}
diff --git a/compiler/codecompiler.go b/compiler/codecompiler.go
index 7fa50411..58ed05a5 100644
--- a/compiler/codecompiler.go
+++ b/compiler/codecompiler.go
@@ -18,6 +18,10 @@ type CodeCompiler struct {
 	// at owned storage, so every read and every nested call it feeds see
 	// the representation lowering stores.
 	outputReads map[funcKey]map[string]struct{}
+	// rangeBindings records, per template, which bindings hold a Range
+	// descriptor, as the template checks read them from the text. Settlement
+	// checks the solved types agree.
+	rangeBindings map[funcKey]map[string]struct{}
 }
 
 type funcKey struct {
@@ -25,6 +29,10 @@ type funcKey struct {
 	arity int
 }
 
+func templateKey(fn *ast.FuncStatement) funcKey {
+	return funcKey{name: fn.Token.Literal, arity: len(fn.Parameters)}
+}
+
 func NewCodeCompiler(ctx llvm.Context, modName, relPath string, code *ast.Code) *CodeCompiler {
 	mangledPath := MangleDirPath(modName, relPath)
 	cc := &CodeCompiler{
@@ -63,7 +71,7 @@ func (cc *CodeCompiler) indexDeclarations() []*token.CompileError {
 				}
 			}
 		case *ast.FuncStatement:
-			key := funcKey{name: s.Token.Literal, arity: len(s.Parameters)}
+			key := templateKey(s)
 			previous, exists := cc.funcTemplates[key]
 			if !exists {
 				cc.funcTemplates[key] = s
diff --git a/compiler/compiler.go b/compiler/compiler.go
index 30012878..4d4cf8a0 100644
--- a/compiler/compiler.go
+++ b/compiler/compiler.go
@@ -1171,7 +1171,7 @@ func (c *Compiler) compileExprAssigns(writeIdents []*ast.Identifier, ownershipId
 	i := 0
 	for _, expr := range exprs {
 		guardPtr := c.pushBoundsGuard("assign_bounds_guard")
-		res := c.compileExpression(expr, writeIdents[i:])
+		res := c.compileAssignedValue(expr, writeIdents[i:])
 		var bit llvm.Value
 		if c.stmtBoundsUsed() {
 			bit = c.createLoad(guardPtr, Int{Width: 1}, "assign_bounds_ok")
@@ -1184,6 +1184,35 @@ func (c *Compiler) compileExprAssigns(writeIdents []*ast.Identifier, ownershipId
 	return assigns
 }
 
+// compileAssignedValue compiles one assignment value. A bare range that a
+// gate makes a computation iterates and keeps its final element, as an
+// operation over it would; inside a loop that already binds the range, it
+// reads that iteration's element.
+func (c *Compiler) compileAssignedValue(expr ast.Expression, dest []*ast.Identifier) []*Symbol {
+	switch expr.(type) {
+	case *ast.Identifier, *ast.RangeLiteral:
+	default:
+		return c.compileExpression(expr, dest)
+	}
+	info := c.ExprCache[key(c.FuncNameMangled, expr)]
+	if len(c.pendingLoopRanges(info.Ranges)) == 0 {
+		return c.compileExpression(expr, dest)
+	}
+
+	PushScope(&c.Scopes, BlockScope)
+	defer c.popScope()
+
+	outputs := c.makeSeededTempOutputs(dest, info.OutTypes)
+	c.bindRangedTempOutputs(dest, outputs)
+	output := outputs[0]
+	c.withLoopNest(info.Ranges, func() {
+		value := c.compileIdentifier(info.Rewrite.(*ast.Identifier))
+		c.storeRangedOutput(output, value.Val, value.Type)
+	})
+
+	return c.loadOutputValues(outputs, "range_final")
+}
+
 // newExprAssign zips one expression's compiled results with its destination
 // slots; the ident and old-value slices start at the expression's first slot.
 func (c *Compiler) newExprAssign(expr ast.Expression, bit llvm.Value, res []*Symbol, dests, owners []*ast.Identifier, olds []*Symbol) exprAssign {
@@ -1527,10 +1556,14 @@ func (c *Compiler) compileExpression(expr ast.Expression, dest []*ast.Identifier
 	case *ast.RangeLiteral:
 		info := c.ExprCache[key(c.FuncNameMangled, e)]
 		// A consuming expression can lower this literal inside the loop that
-		// already bound its iterator rewrite. Complete descriptor assignments
-		// clear the rewrite and materialize the Range aggregate below.
-		if rewIdent, ok := info.Rewrite.(*ast.Identifier); ok && len(c.pendingLoopRanges(info.Ranges)) == 0 {
-			return []*Symbol{c.compileIdentifier(rewIdent)}
+		// already bound its iterator rewrite, and a call that runs the loop
+		// itself gets the range built as for any loop. Complete descriptor
+		// assignments clear the rewrite and materialize the Range aggregate below.
+		if rewIdent, ok := info.Rewrite.(*ast.Identifier); ok {
+			if len(c.pendingLoopRanges(info.Ranges)) == 0 {
+				return []*Symbol{c.compileIdentifier(rewIdent)}
+			}
+			return []*Symbol{c.rangeLiteralValue(e)}
 		}
 		res = c.compileRangeExpression(e)
 		return
diff --git a/compiler/compiler_test.go b/compiler/compiler_test.go
index 324c09f0..f272a3ab 100644
--- a/compiler/compiler_test.go
+++ b/compiler/compiler_test.go
@@ -202,6 +202,7 @@ a, b`
 
 func TestRangedArrayOutputMarksIndirectWrite(t *testing.T) {
 	code := `res = LastRow(matrix)
+    res = []0
     i = 0:2
     res = matrix[i]`
 	script := `matrix = [
@@ -545,7 +546,8 @@ func TestRangedCallDoesNotCopyUnrelatedArrayInput(t *testing.T) {
 	// per iteration would make the call quadratic.
 	code := `count, value = Read(data, index)
     count = index
-    value = data[index]`
+    t = data[index]
+    value = t`
 	script := `data = [0:8]
 count, value = Read(data, 0:8)
 count, value`
@@ -1411,7 +1413,8 @@ x`
 
 func TestAffineArrayIndexStmtInFuncUsesCheckedPath(t *testing.T) {
 	code := `out = pick(arr, i)
-    out = arr[i + 1]
+    t = arr[i + 1]
+    out = t
 `
 	script := `arr = [10 20 30 40 50]
 i = 0:4
@@ -1453,7 +1456,8 @@ x`
 
 func TestNonAffineArrayIndexStmtInFuncUsesCheckedPath(t *testing.T) {
 	code := `out = pick_poly(arr, i)
-    out = arr[i * i - 2i + 3]
+    t = arr[i * i - 2i + 3]
+    out = t
 `
 	script := `arr = [10 20 30 40 50]
 i = 0:2
diff --git a/compiler/cond.go b/compiler/cond.go
index 37d70552..68bb68e0 100644
--- a/compiler/cond.go
+++ b/compiler/cond.go
@@ -539,6 +539,14 @@ func broadcastConds(cond llvm.Value, n int) []llvm.Value {
 func (c *Compiler) extractSlotConds(expr ast.Expression, temps []condTemp) ([]llvm.Value, []condTemp) {
 	info := c.ExprCache[key(c.FuncNameMangled, expr)]
 
+	// An iterated range literal resolves its bounds where its range is built
+	// (rangeLiteralValue), so they are no condition of the value around it.
+	if _, ok := expr.(*ast.RangeLiteral); ok {
+		if _, iterated := info.Rewrite.(*ast.Identifier); iterated {
+			return nil, temps
+		}
+	}
+
 	// Array-literal cells are local-resolution boundaries: each cell resolves
 	// its own condition at its own level. Statement-level extraction must stop
 	// here — descending in would lift a cell's comparison into a gate over the
diff --git a/compiler/effects.go b/compiler/effects.go
index aac2754b..8c297396 100644
--- a/compiler/effects.go
+++ b/compiler/effects.go
@@ -8,20 +8,18 @@ import (
 )
 
 // WriteEffect describes whether one named target is guaranteed to receive a
-// value. Uncomputed and Invalid are publication states, not lattice members.
+// value. Invalid marks a target whose facts could not be derived; it is not a
+// lattice member.
 type WriteEffect uint8
 
 const (
-	WriteUncomputed WriteEffect = iota
-	WriteInvalid
+	WriteInvalid WriteEffect = iota
 	MustWrite
 	MayWrite
 )
 
 func (effect WriteEffect) String() string {
 	switch effect {
-	case WriteUncomputed:
-		return "Uncomputed"
 	case WriteInvalid:
 		return "Invalid"
 	case MustWrite:
@@ -69,27 +67,13 @@ type TargetWriteEffect struct {
 }
 
 // StatementEffect contains the target facts derived for one assignment.
-// ReadsSeed holds LHS indices whose existing value is consumed by a direct
-// MayWrite callee output at the assignment boundary.
+// ReadsSeed holds LHS indices whose existing value a direct call keeps at the
+// assignment boundary when its call-owned domain may run no iteration.
 type StatementEffect struct {
 	Writes    []TargetWriteEffect
 	ReadsSeed []int
 }
 
-func validPublishedEffects(effects []WriteEffect, count int) bool {
-	if len(effects) != count {
-		return false
-	}
-
-	for _, effect := range effects {
-		if effect != MustWrite && effect != MayWrite {
-			return false
-		}
-	}
-
-	return true
-}
-
 func joinYield(left, right YieldEffect) YieldEffect {
 	if left == YieldInvalid || right == YieldInvalid {
 		return YieldInvalid
@@ -103,8 +87,8 @@ func joinYield(left, right YieldEffect) YieldEffect {
 	return MustYield
 }
 
-// classifyWriteEffect keeps analysis states outside the yield lattice invalid
-// so function publication cannot turn missing facts into MayWrite.
+// classifyWriteEffect keeps analysis states outside the yield lattice invalid,
+// so missing facts never pass as MayWrite.
 func classifyWriteEffect(yield YieldEffect, maySkip bool) WriteEffect {
 	if yield != MustYield && yield != MayYield {
 		return WriteInvalid
@@ -120,16 +104,12 @@ func classifyWriteEffect(yield YieldEffect, maySkip bool) WriteEffect {
 type effectAnalyzer struct {
 	compiler        *Compiler
 	funcNameMangled string
-	graph           *specializationCallGraph
-	working         [][]WriteEffect
 }
 
-func newEffectAnalyzer(compiler *Compiler, mangled string, graph *specializationCallGraph, working [][]WriteEffect) *effectAnalyzer {
+func newEffectAnalyzer(compiler *Compiler, mangled string) *effectAnalyzer {
 	return &effectAnalyzer{
 		compiler:        compiler,
 		funcNameMangled: mangled,
-		graph:           graph,
-		working:         working,
 	}
 }
 
@@ -256,6 +236,9 @@ func yieldSlot(effects []YieldEffect, index int) YieldEffect {
 	return effects[index]
 }
 
+// deriveCall yields every output of a call that is invoked, since every body
+// that runs writes every output. Its arguments can still fail, and a range
+// that may run no iteration can keep it from being invoked.
 func (analyzer *effectAnalyzer) deriveCall(expr *ast.CallExpression) []YieldEffect {
 	info := analyzer.exprInfo(expr)
 	invocation := analyzer.callInvocationEffect(expr)
@@ -263,47 +246,10 @@ func (analyzer *effectAnalyzer) deriveCall(expr *ast.CallExpression) []YieldEffe
 		invocation = joinYield(invocation, MayYield)
 	}
 
-	callee := analyzer.callBodyOutputEffects(expr)
-	if len(callee) != len(info.OutTypes) {
-		panic(fmt.Sprintf("internal: call %s has %d output effects for %d typed outputs", expr.Function.Value, len(callee), len(info.OutTypes)))
-	}
-
-	info.YieldEffects = make([]YieldEffect, len(info.OutTypes))
-
-	for i, effect := range callee {
-		switch effect {
-		case MustWrite:
-			info.YieldEffects[i] = invocation
-		case MayWrite:
-			info.YieldEffects[i] = joinYield(invocation, MayYield)
-		default:
-			info.YieldEffects[i] = YieldInvalid
-		}
-	}
-
+	info.YieldEffects = slices.Repeat([]YieldEffect{invocation}, len(info.OutTypes))
 	return info.YieldEffects
 }
 
-func (analyzer *effectAnalyzer) callBodyOutputEffects(expr *ast.CallExpression) []WriteEffect {
-	info := analyzer.exprInfo(expr)
-	mangled := Mangle(analyzer.compiler.MangledPath, expr.Function.Value, info.CallParamTypes)
-	f := analyzer.compiler.FuncCache[mangled]
-	if f.Settled {
-		return f.BodyOutputEffects
-	}
-
-	if analyzer.graph == nil {
-		panic(fmt.Sprintf("internal: unsettled callee %s outside effect settlement", mangled))
-	}
-
-	id, ok := analyzer.graph.byMangled[mangled]
-	if !ok {
-		panic(fmt.Sprintf("internal: unsettled callee %s missing from effect graph", mangled))
-	}
-
-	return analyzer.working[id]
-}
-
 // hasPossiblyEmptyRange ignores named drivers already owned by an enclosing
 // domain, such as a statement condition around a call.
 func hasPossiblyEmptyRange(ranges, excluded []*RangeInfo) bool {
@@ -361,21 +307,18 @@ func (analyzer *effectAnalyzer) callInvocationEffect(expr *ast.CallExpression) Y
 	return effect
 }
 
-func (analyzer *effectAnalyzer) seedResolvedYield(expr ast.Expression, slot int, targetExists bool, conditionRanges []*RangeInfo) (YieldEffect, bool) {
+func (analyzer *effectAnalyzer) seedResolvedYield(expr ast.Expression, targetExists bool, conditionRanges []*RangeInfo) (YieldEffect, bool) {
 	call, ok := expr.(*ast.CallExpression)
 	if !ok || !targetExists {
 		return YieldUncomputed, false
 	}
 
-	// Direct-return eligibility depends only on output types. Check it before
-	// resolving callee effects because indirect calls cannot consume a seed.
+	// Every body that runs writes every output, so only a call-owned domain
+	// that may run no iteration leaves a direct return's seed in place.
 	if _, direct := directScalarABIReturnType(analyzer.exprInfo(call).OutTypes); !direct {
 		return YieldUncomputed, false
 	}
-
-	callee := analyzer.callBodyOutputEffects(call)
-	needsSeed := callee[slot] == MayWrite || analyzer.callOwnsPossiblyEmptyDomain(call, conditionRanges)
-	if !needsSeed {
+	if !analyzer.callOwnsPossiblyEmptyDomain(call, conditionRanges) {
 		return YieldUncomputed, false
 	}
 
@@ -400,13 +343,8 @@ func (analyzer *effectAnalyzer) callOwnsPossiblyEmptyDomain(call *ast.CallExpres
 	return false
 }
 
-func (analyzer *effectAnalyzer) deriveStatements(statements []ast.Statement, initiallyDefined map[string]struct{}) map[*ast.LetStatement]StatementEffect {
-	defined := make(map[string]struct{}, len(initiallyDefined))
-
-	for name := range initiallyDefined {
-		defined[name] = struct{}{}
-	}
-
+func (analyzer *effectAnalyzer) deriveStatements(statements []ast.Statement) map[*ast.LetStatement]StatementEffect {
+	defined := make(map[string]struct{})
 	results := make(map[*ast.LetStatement]StatementEffect)
 
 	for _, statement := range statements {
@@ -442,7 +380,7 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 		yields := analyzer.deriveExpr(expr)
 		maySkip := len(stmt.Condition) > 0 || analyzer.expressionUsesLocalDomain(expr)
 
-		for slot, yield := range yields {
+		for _, yield := range yields {
 			index := targetIndex
 			target := stmt.Name[index]
 			targetIndex++
@@ -451,7 +389,7 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 			}
 
 			_, targetExists := defined[target.Value]
-			if seededYield, readsSeed := analyzer.seedResolvedYield(expr, slot, targetExists, condRanges); readsSeed {
+			if seededYield, readsSeed := analyzer.seedResolvedYield(expr, targetExists, condRanges); readsSeed {
 				result.ReadsSeed = append(result.ReadsSeed, index)
 				yield = seededYield
 			}
@@ -501,362 +439,10 @@ func validStatementEffect(stmt *ast.LetStatement, effect StatementEffect) bool {
 	return true
 }
 
-func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.LetStatement]StatementEffect) []WriteEffect {
-	effects := make([]WriteEffect, len(template.Outputs))
-
-	for i := range effects {
-		effects[i] = MayWrite
-	}
-
-	outputIndex := make(map[string]int, len(template.Outputs))
-
-	for i, output := range template.Outputs {
-		outputIndex[output.Value] = i
-	}
-
-	for _, statement := range template.Body.Statements {
-		stmt, ok := statement.(*ast.LetStatement)
-		if !ok {
-			continue
-		}
-
-		statementEffect, exists := statements[stmt]
-		if !exists || !validStatementEffect(stmt, statementEffect) {
-			return slices.Repeat([]WriteEffect{WriteInvalid}, len(template.Outputs))
-		}
-
-		for name := range definiteTargets(stmt, statementEffect) {
-			if index, isOutput := outputIndex[name]; isOutput {
-				effects[index] = MustWrite
-			}
-		}
-	}
-
-	return effects
-}
-
-// definiteTargets is the set of targets a statement leaves holding its own
-// value on every path: unconditional writes that do not merely preserve the
-// target's seed.
-func definiteTargets(stmt *ast.LetStatement, effect StatementEffect) map[string]struct{} {
-	targets := make(map[string]struct{}, len(effect.Writes))
-	for _, write := range effect.Writes {
-		if write.Effect == MustWrite && !slices.Contains(effect.ReadsSeed, write.TargetIndex) {
-			targets[stmt.Name[write.TargetIndex].Value] = struct{}{}
-		}
-	}
-	return targets
-}
-
-type specializationNodeID int
-
-type specializationNode struct {
-	mangled        string
-	effectCallees  []specializationNodeID
-	effectCallers  []specializationNodeID
-	directCallees  []string
-	componentIndex int
-}
-
-// specializationCallGraph interns the newly walked batch once. Dense effect
-// edges drive SCC settlement, while complete mangled edges persist for CFG
-// diagnostic replay across warm-cache scripts.
-type specializationCallGraph struct {
-	nodes     []specializationNode
-	byMangled map[string]specializationNodeID
-}
-
-func newSpecializationCallGraph(walked map[string]walkedSpecialization) *specializationCallGraph {
-	graph := &specializationCallGraph{
-		nodes:     make([]specializationNode, len(walked)),
-		byMangled: make(map[string]specializationNodeID, len(walked)),
-	}
-
-	for mangled, walkedFunc := range walked {
-		id := specializationNodeID(walkedFunc.walkIndex)
-		graph.byMangled[mangled] = id
-		graph.nodes[id] = specializationNode{mangled: mangled}
-	}
-
-	return graph
-}
-
-// collectSpecializationCallEdges returns stable unique lowering and replay
-// targets plus source-order primary effect dependencies. Each direct primary
-// precedes its distinct scalar companion.
-func collectSpecializationCallEdges(compiler *Compiler, callerMangled string, statements []ast.Statement) ([]string, []string) {
-	seen := make(map[string]struct{})
-	var directCallees []string
-	var effectCallees []string
-
-	for _, call := range collectBodyCalls(statements) {
-		if _, builtin := Builtins[call.Function.Value]; builtin {
-			continue
-		}
-
-		info := compiler.ExprCache[key(callerMangled, call)]
-		primary := Mangle(compiler.MangledPath, call.Function.Value, info.CallParamTypes)
-		requireSpecializationCallTarget(compiler, callerMangled, primary)
-		effectCallees = append(effectCallees, primary)
-		directCallees = appendUniqueMangled(directCallees, seen, primary)
-
-		if !info.ScalarCallVariantEnsured {
-			continue
-		}
-
-		scalar := Mangle(compiler.MangledPath, call.Function.Value, info.ScalarCallParamTypes)
-		if scalar == primary {
-			panic(fmt.Sprintf("internal: call %s in %s marks a non-distinct scalar specialization", call.Function.Value, callerMangled))
-		}
-		requireSpecializationCallTarget(compiler, callerMangled, scalar)
-		directCallees = appendUniqueMangled(directCallees, seen, scalar)
-	}
-
-	return directCallees, effectCallees
-}
-
-func appendUniqueMangled(names []string, seen map[string]struct{}, mangled string) []string {
-	if _, exists := seen[mangled]; exists {
-		return names
-	}
-
-	seen[mangled] = struct{}{}
-	return append(names, mangled)
-}
-
-func requireSpecializationCallTarget(compiler *Compiler, callerMangled, calleeMangled string) {
-	if compiler.FuncCache[calleeMangled] == nil {
-		panic(fmt.Sprintf("internal: typed call from %s targets missing specialization %s", callerMangled, calleeMangled))
-	}
-}
-
-func (ts *TypeSolver) addSpecializationGraphEdges(graph *specializationCallGraph, callerID specializationNodeID) {
-	caller := &graph.nodes[callerID]
-	walked := ts.walkedFuncs[caller.mangled]
-	compiler := ts.ScriptCompiler.Compiler
-	directCallees, effectCallees := collectSpecializationCallEdges(compiler, caller.mangled, walked.template.Body.Statements)
-	caller.directCallees = directCallees
-
-	for _, callee := range effectCallees {
-		if calleeID, inGraph := graph.byMangled[callee]; inGraph {
-			caller.effectCallees = append(caller.effectCallees, calleeID)
-		}
-	}
-
-	slices.Sort(caller.effectCallees)
-	caller.effectCallees = slices.Compact(caller.effectCallees)
-
-	for _, calleeID := range caller.effectCallees {
-		graph.nodes[calleeID].effectCallers = append(graph.nodes[calleeID].effectCallers, callerID)
-	}
-}
-
-func (ts *TypeSolver) buildSpecializationCallGraph() *specializationCallGraph {
-	graph := newSpecializationCallGraph(ts.walkedFuncs)
-
-	for id := range graph.nodes {
-		ts.addSpecializationGraphEdges(graph, specializationNodeID(id))
-	}
-
-	return graph
-}
-
-func collectBodyCalls(statements []ast.Statement) []*ast.CallExpression {
-	var calls []*ast.CallExpression
-
-	for _, statement := range statements {
-		switch stmt := statement.(type) {
-		case *ast.LetStatement:
-			for _, condition := range stmt.Condition {
-				calls = append(calls, collectExprCalls(condition)...)
-			}
-
-			for _, value := range stmt.Value {
-				calls = append(calls, collectExprCalls(value)...)
-			}
-		case *ast.PrintStatement:
-			for _, argument := range stmt.Expression.Arguments {
-				calls = append(calls, collectExprCalls(argument)...)
-			}
-		}
-	}
-
-	return calls
-}
-
-func collectExprCalls(expr ast.Expression) []*ast.CallExpression {
-	var calls []*ast.CallExpression
-	if call, ok := expr.(*ast.CallExpression); ok {
-		calls = append(calls, call)
-	}
-
-	for _, child := range ast.ExprChildren(expr) {
-		calls = append(calls, collectExprCalls(child)...)
-	}
-
-	return calls
-}
-
-type tarjanState struct {
-	graph      *specializationCallGraph
-	index      int
-	indices    []int
-	lowlink    []int
-	stack      []specializationNodeID
-	onStack    []bool
-	components [][]specializationNodeID
-}
-
-func (graph *specializationCallGraph) calleeFirstComponents() [][]specializationNodeID {
-	state := &tarjanState{
-		graph:   graph,
-		indices: make([]int, len(graph.nodes)),
-		lowlink: make([]int, len(graph.nodes)),
-		onStack: make([]bool, len(graph.nodes)),
-	}
-
-	for id := range graph.nodes {
-		if state.indices[id] == 0 {
-			state.visit(specializationNodeID(id))
-		}
-	}
-
-	return state.components
-}
-
-func (state *tarjanState) visit(id specializationNodeID) {
-	state.index++
-	state.indices[id] = state.index
-	state.lowlink[id] = state.index
-	state.stack = append(state.stack, id)
-	state.onStack[id] = true
-
-	for _, calleeID := range state.graph.nodes[id].effectCallees {
-		if state.indices[calleeID] == 0 {
-			state.visit(calleeID)
-			state.lowlink[id] = min(state.lowlink[id], state.lowlink[calleeID])
-		} else if state.onStack[calleeID] {
-			state.lowlink[id] = min(state.lowlink[id], state.indices[calleeID])
-		}
-	}
-
-	if state.lowlink[id] != state.indices[id] {
-		return
-	}
-
-	componentIndex := len(state.components)
-	var component []specializationNodeID
-
-	for {
-		last := len(state.stack) - 1
-		member := state.stack[last]
-		state.stack = state.stack[:last]
-		state.onStack[member] = false
-		state.graph.nodes[member].componentIndex = componentIndex
-		component = append(component, member)
-		if member == id {
-			break
-		}
-	}
-
-	slices.Sort(component)
-	state.components = append(state.components, component)
-}
-
-// deriveEffectNode refreshes one specialization and reports whether any output
-// weakened from MustWrite to MayWrite.
-func (ts *TypeSolver) deriveEffectNode(graph *specializationCallGraph, working [][]WriteEffect, id specializationNodeID) bool {
-	node := &graph.nodes[id]
-	walked := ts.walkedFuncs[node.mangled]
-	initial := functionInitialBindings(walked.template)
-	analyzer := newEffectAnalyzer(ts.ScriptCompiler.Compiler, node.mangled, graph, working)
-	statements := analyzer.deriveStatements(walked.template.Body.Statements, initial)
-	derived := deriveBodyOutputEffects(walked.template, statements)
-
-	if !validPublishedEffects(derived, len(walked.info.Sig.OutTypes)) {
-		panic(fmt.Sprintf("internal: invalid effects for specialization %s", node.mangled))
-	}
-
-	changed := false
-	for outputIndex, effect := range derived {
-		if working[id][outputIndex] == MustWrite && effect == MayWrite {
-			working[id][outputIndex] = MayWrite
-			changed = true
-		}
-	}
-
-	walked.info.StatementEffects = statements
-
-	return changed
-}
-
-func enqueueRecursiveEffectCallers(graph *specializationCallGraph, id specializationNodeID, pending []specializationNodeID, queued []bool) []specializationNodeID {
-	componentIndex := graph.nodes[id].componentIndex
-
-	for _, callerID := range graph.nodes[id].effectCallers {
-		if graph.nodes[callerID].componentIndex != componentIndex || queued[callerID] {
-			continue
-		}
-		pending = append(pending, callerID)
-		queued[callerID] = true
-	}
-
-	return pending
-}
-
-// settleEffectComponent weakens one SCC to a fixed point and publishes all
-// members only after their shared worklist drains.
-func (ts *TypeSolver) settleEffectComponent(graph *specializationCallGraph, working [][]WriteEffect, component []specializationNodeID, queued []bool) {
-	pending := slices.Clone(component)
-
-	for _, id := range pending {
-		queued[id] = true
-	}
-
-	for next := 0; next < len(pending); next++ {
-		id := pending[next]
-		queued[id] = false
-		if ts.deriveEffectNode(graph, working, id) {
-			pending = enqueueRecursiveEffectCallers(graph, id, pending, queued)
-		}
-	}
-
-	for _, id := range component {
-		node := &graph.nodes[id]
-		ts.walkedFuncs[node.mangled].info.BodyOutputEffects = slices.Clone(working[id])
-	}
-}
-
-func (ts *TypeSolver) settleEffects(graph *specializationCallGraph) {
-	working := make([][]WriteEffect, len(graph.nodes))
-
-	for id := range graph.nodes {
-		walked := ts.walkedFuncs[graph.nodes[id].mangled]
-		working[id] = slices.Repeat([]WriteEffect{MustWrite}, len(walked.info.Sig.OutTypes))
-	}
-
-	components := graph.calleeFirstComponents()
-	queued := make([]bool, len(graph.nodes))
-
-	for _, component := range components {
-		ts.settleEffectComponent(graph, working, component, queued)
-	}
-}
-
-func functionInitialBindings(template *ast.FuncStatement) map[string]struct{} {
-	defined := make(map[string]struct{}, len(template.Parameters))
-
-	for _, parameter := range template.Parameters {
-		defined[parameter.Value] = struct{}{}
-	}
-
-	return defined
-}
-
 func (ts *TypeSolver) deriveScriptEffects() {
 	root := ts.ScriptCompiler.Script.Root
-	analyzer := newEffectAnalyzer(ts.ScriptCompiler.Compiler, ts.ScriptCompiler.ScriptMangled, nil, nil)
-	root.StatementEffects = analyzer.deriveStatements(ts.ScriptCompiler.Program.Statements, nil)
+	analyzer := newEffectAnalyzer(ts.ScriptCompiler.Compiler, ts.ScriptCompiler.ScriptMangled)
+	root.StatementEffects = analyzer.deriveStatements(ts.ScriptCompiler.Program.Statements)
 
 	for _, statement := range ts.ScriptCompiler.Program.Statements {
 		stmt, ok := statement.(*ast.LetStatement)
diff --git a/compiler/effects_test.go b/compiler/effects_test.go
index ef0b8862..391bf6d4 100644
--- a/compiler/effects_test.go
+++ b/compiler/effects_test.go
@@ -161,48 +161,32 @@ nonempty, empty`)
 	requireTargetEffects(t, ts.ScriptCompiler.Script.Root.StatementEffects[empty], TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
 }
 
-func TestDirectCallSeedEffects(t *testing.T) {
+func TestDirectCallEffects(t *testing.T) {
 	ctx := llvm.NewContext()
 	defer ctx.Dispose()
 
 	cc := NewCodeCompiler(ctx, "callEffects", "", mustParseCode(t, `y = Always(x)
-    y = x
-
-y = Maybe(x)
-    y = x > 0 x`))
+    y = x`))
 	require.Empty(t, cc.Compile())
 
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), `seeded = 7
-seeded = Maybe(1)
-fresh = Maybe(1)
-always = 4
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `always = 4
 always = Always(1)
 arr = [1]
 failed = 9
 failed = Always(arr[2])
 gated = 8
-gated = 1 > 0 Maybe(1)
-seeded, always, failed, gated`)
+gated = 1 > 0 Always(1)
+always, failed, gated`)
 
 	program := ts.ScriptCompiler.Program
-	seeded := program.Statements[1].(*ast.LetStatement)
-	fresh := program.Statements[2].(*ast.LetStatement)
-	always := program.Statements[4].(*ast.LetStatement)
-	failed := program.Statements[7].(*ast.LetStatement)
-	gated := program.Statements[9].(*ast.LetStatement)
-
-	seededEffect := ts.ScriptCompiler.Script.Root.StatementEffects[seeded]
-	requireTargetEffects(t, seededEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
-	require.Equal(t, []int{0}, seededEffect.ReadsSeed)
-	require.Equal(t, []YieldEffect{MayYield}, ts.ExprCache[key(ts.FuncNameMangled, seeded.Value[0])].YieldEffects)
-
-	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
-	requireTargetEffects(t, freshEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
-	require.Empty(t, freshEffect.ReadsSeed)
+	always := program.Statements[1].(*ast.LetStatement)
+	failed := program.Statements[4].(*ast.LetStatement)
+	gated := program.Statements[6].(*ast.LetStatement)
 
 	alwaysEffect := ts.ScriptCompiler.Script.Root.StatementEffects[always]
 	requireTargetEffects(t, alwaysEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
 	require.Empty(t, alwaysEffect.ReadsSeed)
+	require.Equal(t, []YieldEffect{MustYield}, ts.ExprCache[key(ts.FuncNameMangled, always.Value[0])].YieldEffects)
 
 	failedEffect := ts.ScriptCompiler.Script.Root.StatementEffects[failed]
 	requireTargetEffects(t, failedEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
@@ -210,63 +194,15 @@ seeded, always, failed, gated`)
 
 	gatedEffect := ts.ScriptCompiler.Script.Root.StatementEffects[gated]
 	requireTargetEffects(t, gatedEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
-	require.Equal(t, []int{0}, gatedEffect.ReadsSeed)
+	require.Empty(t, gatedEffect.ReadsSeed)
 
-	maybeFunc := cc.Compiler.FuncCache[Mangle(cc.Compiler.MangledPath, "Maybe", []Type{I64})]
 	alwaysFunc := cc.Compiler.FuncCache[Mangle(cc.Compiler.MangledPath, "Always", []Type{I64})]
-
-	require.Equal(t, []WriteEffect{MayWrite}, maybeFunc.BodyOutputEffects)
-	require.Equal(t, []WriteEffect{MustWrite}, alwaysFunc.BodyOutputEffects)
-	require.True(t, maybeFunc.Settled)
 	require.True(t, alwaysFunc.Settled)
 }
 
-func TestFunctionOutputIsNotInitiallyWritten(t *testing.T) {
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-
-	cc := NewCodeCompiler(ctx, "wrapperEffects", "", mustParseCode(t, `y = Maybe(x)
-    y = x > 0 x
-
-y = Wrap(x)
-    y = Maybe(x)
-    y = Maybe(x)`))
-	require.Empty(t, cc.Compile())
-
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), `fresh = Wrap(1)
-existing = 7
-existing = Wrap(1)
-fresh, existing`)
-
-	wrap := cc.Compiler.FuncCache[Mangle(cc.Compiler.MangledPath, "Wrap", []Type{I64})]
-
-	require.NotNil(t, wrap)
-	require.Equal(t, []WriteEffect{MayWrite}, wrap.BodyOutputEffects)
-
-	template, ok := cc.lookupFuncTemplate("Wrap", 1)
-	require.True(t, ok)
-	firstBodyStmt := template.Body.Statements[0].(*ast.LetStatement)
-	firstBodyEffect := wrap.StatementEffects[firstBodyStmt]
-	requireTargetEffects(t, firstBodyEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
-	require.Empty(t, firstBodyEffect.ReadsSeed)
-
-	secondBodyStmt := template.Body.Statements[1].(*ast.LetStatement)
-	secondBodyEffect := wrap.StatementEffects[secondBodyStmt]
-	requireTargetEffects(t, secondBodyEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
-	require.Equal(t, []int{0}, secondBodyEffect.ReadsSeed)
-
-	fresh := ts.ScriptCompiler.Program.Statements[0].(*ast.LetStatement)
-	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
-	requireTargetEffects(t, freshEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
-	require.Empty(t, freshEffect.ReadsSeed)
-
-	existing := ts.ScriptCompiler.Program.Statements[2].(*ast.LetStatement)
-	existingEffect := ts.ScriptCompiler.Script.Root.StatementEffects[existing]
-	requireTargetEffects(t, existingEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
-	require.Equal(t, []int{0}, existingEffect.ReadsSeed)
-}
-
-func TestCallDomainComposesWithBodyOutputEffects(t *testing.T) {
+// A call that runs writes every output, so only its own domain decides
+// whether it writes: an empty range keeps an existing destination.
+func TestCallDomainDecidesCallWrites(t *testing.T) {
 	ctx := llvm.NewContext()
 	defer ctx.Dispose()
 
@@ -280,17 +216,6 @@ empty = Increment(0:0)
 nonempty = Increment(0:2)
 existing, empty, nonempty`)
 
-	mangled := Mangle(cc.Compiler.MangledPath, "Increment", []Type{Range{Iter: I64}})
-	increment := cc.Compiler.FuncCache[mangled]
-
-	require.NotNil(t, increment)
-	require.Equal(t, []WriteEffect{MustWrite}, increment.BodyOutputEffects)
-
-	template, ok := cc.lookupFuncTemplate("Increment", 1)
-	require.True(t, ok)
-	bodyStmt := template.Body.Statements[0].(*ast.LetStatement)
-	requireTargetEffects(t, increment.StatementEffects[bodyStmt], TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
-
 	existing := ts.ScriptCompiler.Program.Statements[1].(*ast.LetStatement)
 	existingEffect := ts.ScriptCompiler.Script.Root.StatementEffects[existing]
 	requireTargetEffects(t, existingEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
@@ -339,145 +264,6 @@ existing`)
 	}
 }
 
-func TestConditionalBodyRemainsMayWriteAcrossNonemptyDomain(t *testing.T) {
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-
-	cc := NewCodeCompiler(ctx, "conditionalDomainEffects", "", mustParseCode(t, `y = ConditionalSquare(x)
-    y = x > 5 x * x`))
-	require.Empty(t, cc.Compile())
-
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), `fresh = ConditionalSquare(0:5)
-existing = 9
-existing = ConditionalSquare(0:5)
-fresh, existing`)
-
-	mangled := Mangle(cc.Compiler.MangledPath, "ConditionalSquare", []Type{Range{Iter: I64}})
-	conditional := cc.Compiler.FuncCache[mangled]
-
-	require.NotNil(t, conditional)
-	require.Equal(t, []WriteEffect{MayWrite}, conditional.BodyOutputEffects)
-
-	fresh := ts.ScriptCompiler.Program.Statements[0].(*ast.LetStatement)
-	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
-	requireTargetEffects(t, freshEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
-	require.Empty(t, freshEffect.ReadsSeed)
-
-	existing := ts.ScriptCompiler.Program.Statements[2].(*ast.LetStatement)
-	existingEffect := ts.ScriptCompiler.Script.Root.StatementEffects[existing]
-	requireTargetEffects(t, existingEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
-	require.Equal(t, []int{0}, existingEffect.ReadsSeed)
-}
-
-func TestRecursiveBodyOutputEffectsConvergeAcrossSCC(t *testing.T) {
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-
-	cc := NewCodeCompiler(ctx, "recursiveEffects", "", mustParseCode(t, `y = A(n)
-    y = B(n)
-
-y = B(n)
-    y = n > 0 A(n - 1)
-    y = n == 0 "done"`))
-	require.Empty(t, cc.Compile())
-
-	solveScriptTypes(t, ctx, cc, t.Name(), `result = A(2)
-result`)
-
-	a := cc.Compiler.FuncCache[Mangle(cc.Compiler.MangledPath, "A", []Type{I64})]
-	b := cc.Compiler.FuncCache[Mangle(cc.Compiler.MangledPath, "B", []Type{I64})]
-
-	require.Equal(t, []WriteEffect{MayWrite}, a.BodyOutputEffects)
-	require.Equal(t, []WriteEffect{MayWrite}, b.BodyOutputEffects)
-	require.True(t, a.Settled)
-	require.True(t, b.Settled)
-}
-
-func TestCallGraphWalkOrderAndEdgeViews(t *testing.T) {
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-
-	cc := NewCodeCompiler(ctx, "effectGraphIDs", "", mustParseCode(t, `y = Z(x)
-    y = B(x)
-    C(x)
-    y = B(x)
-
-y = B(x)
-    y = C(x)
-
-y = C(x)
-    y = x`))
-	require.Empty(t, cc.Compile())
-
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), `result = Z(1)
-result`)
-
-	walkOrder := []string{
-		Mangle(cc.Compiler.MangledPath, "Z", []Type{I64}),
-		Mangle(cc.Compiler.MangledPath, "B", []Type{I64}),
-		Mangle(cc.Compiler.MangledPath, "C", []Type{I64}),
-	}
-
-	graph := ts.buildSpecializationCallGraph()
-
-	for index, name := range walkOrder {
-		id := specializationNodeID(index)
-		require.Equal(t, id, graph.byMangled[name])
-		require.Equal(t, name, graph.nodes[id].mangled)
-	}
-
-	zID := graph.byMangled[Mangle(cc.Compiler.MangledPath, "Z", []Type{I64})]
-	bID := graph.byMangled[Mangle(cc.Compiler.MangledPath, "B", []Type{I64})]
-	cID := graph.byMangled[Mangle(cc.Compiler.MangledPath, "C", []Type{I64})]
-
-	require.Equal(t, []specializationNodeID{bID, cID}, graph.nodes[zID].effectCallees)
-	require.Equal(t, []specializationNodeID{zID}, graph.nodes[bID].effectCallers)
-	require.Equal(t, []specializationNodeID{cID}, graph.nodes[bID].effectCallees)
-	require.Equal(t, []specializationNodeID{zID, bID}, graph.nodes[cID].effectCallers)
-	require.Equal(t, [][]specializationNodeID{{cID}, {bID}, {zID}}, graph.calleeFirstComponents())
-	require.Equal(t, []string{walkOrder[1], walkOrder[2]}, graph.nodes[zID].directCallees)
-	require.Equal(t, []string{walkOrder[2]}, graph.nodes[bID].directCallees)
-	require.Empty(t, graph.nodes[cID].directCallees)
-}
-
-func TestCallGraphExcludesScalarEffectEdge(t *testing.T) {
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-
-	cc := NewCodeCompiler(ctx, "scalarCompanionEdges", "", mustParseCode(t, `result = Gather(arr)
-    i = 0:3
-    result = [Scale(arr[i])]
-
-result = Scale(x)
-    result = x`))
-	require.Empty(t, cc.Compile())
-
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), `arr = [10 20 30]
-result = Gather(arr)
-result`)
-	gatherMangled := Mangle(cc.Compiler.MangledPath, "Gather", []Type{Array{ElemType: I64, Rank: 1}})
-	gatherTemplate, ok := cc.lookupFuncTemplate("Gather", 1)
-	require.True(t, ok)
-	gatherCall := gatherTemplate.Body.Statements[1].(*ast.LetStatement).Value[0].(*ast.ArrayLiteral).Rows[0][0].(*ast.CallExpression)
-	callInfo := ts.ExprCache[key(gatherMangled, gatherCall)]
-	require.True(t, callInfo.ScalarCallVariantEnsured)
-
-	primaryMangled := Mangle(cc.Compiler.MangledPath, "Scale", callInfo.CallParamTypes)
-	scalarMangled := Mangle(cc.Compiler.MangledPath, "Scale", callInfo.ScalarCallParamTypes)
-	require.NotEqual(t, primaryMangled, scalarMangled)
-
-	graph := ts.buildSpecializationCallGraph()
-	gatherID, gatherInBatch := graph.byMangled[gatherMangled]
-	primaryID, primaryInBatch := graph.byMangled[primaryMangled]
-	_, scalarInBatch := graph.byMangled[scalarMangled]
-	require.True(t, gatherInBatch)
-	require.True(t, primaryInBatch)
-	require.True(t, scalarInBatch)
-	require.Equal(t, []specializationNodeID{primaryID}, graph.nodes[gatherID].effectCallees)
-	require.Equal(t, []string{primaryMangled, scalarMangled}, graph.nodes[gatherID].directCallees)
-	require.Equal(t, []string{primaryMangled, scalarMangled}, cc.Compiler.FuncCache[gatherMangled].CFGResult.DirectCallees)
-}
-
 func TestScriptEffectsRejectInvalidExpressionFacts(t *testing.T) {
 	ctx := llvm.NewContext()
 	defer ctx.Dispose()
@@ -497,15 +283,15 @@ value`)
 	)
 }
 
-func TestMayWriteCallPreservesInvalidInvocationEffect(t *testing.T) {
+func TestCallPreservesInvalidInvocationEffect(t *testing.T) {
 	ctx := llvm.NewContext()
 	defer ctx.Dispose()
 
-	cc := NewCodeCompiler(ctx, "invalidCallEffects", "", mustParseCode(t, `y = Maybe(x)
-    y = x > 0 x`))
+	cc := NewCodeCompiler(ctx, "invalidCallEffects", "", mustParseCode(t, `y = Always(x)
+    y = x`))
 	require.Empty(t, cc.Compile())
 
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), `value = Maybe(1 + 1)
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `value = Always(1 + 1)
 value`)
 
 	stmt := ts.ScriptCompiler.Program.Statements[0].(*ast.LetStatement)
@@ -513,7 +299,7 @@ value`)
 	argument := call.Arguments[0]
 	ts.ExprCache[key(ts.FuncNameMangled, argument)].OutTypes = []Type{Unresolved{}}
 
-	analyzer := newEffectAnalyzer(ts.ScriptCompiler.Compiler, ts.ScriptCompiler.ScriptMangled, nil, nil)
+	analyzer := newEffectAnalyzer(ts.ScriptCompiler.Compiler, ts.ScriptCompiler.ScriptMangled)
 
 	require.Equal(t, []YieldEffect{YieldInvalid}, analyzer.deriveExpr(call))
 }
diff --git a/compiler/loop.go b/compiler/loop.go
index ad4a3f7e..66bc6434 100644
--- a/compiler/loop.go
+++ b/compiler/loop.go
@@ -34,56 +34,55 @@ func (c *Compiler) rangeSymbol(sym *Symbol, name string) *Symbol {
 	panic(fmt.Sprintf("internal: %q is not a Range during lowering (got %s)", name, sym.Type.String()))
 }
 
-func (c *Compiler) rangeAggregateFromSymbol(sym *Symbol, name string) llvm.Value {
-	return c.rangeSymbol(sym, name).Val
-}
-
-func (c *Compiler) iterOverDriverSymbol(sym *Symbol, name string, body func(*Symbol)) {
-	rangeSym := c.rangeSymbol(sym, name)
-	c.iterOverRange(rangeSym.Type.(Range), rangeSym.Val, func(iter llvm.Value, iterType Type) {
-		body(&Symbol{
-			Val:      iter,
-			Type:     iterType,
-			FuncArg:  rangeSym.FuncArg,
-			Borrowed: true,
-		})
-	})
-}
-
-// rangeAggregateForRI builds the {start,stop,step} aggregate for a driver.
-func (c *Compiler) rangeAggregateForRI(ri *RangeInfo) llvm.Value {
-	if ri.RangeLit != nil {
-		return c.ToRange(ri.RangeLit, Range{Iter: Int{Width: 64}})
-	}
+// loopRangeValues builds each driver's range once, ahead of its loop nest. A
+// range literal's bounds resolve there like any operands: when one fails to
+// yield, its range is empty and its loop runs no iterations.
+func (c *Compiler) loopRangeValues(ranges []*RangeInfo) []*Symbol {
+	values := make([]*Symbol, len(ranges))
+	for i, ri := range ranges {
+		if ri.RangeLit != nil {
+			values[i] = c.rangeLiteralValue(ri.RangeLit)
+			continue
+		}
 
-	sym, ok := c.getRawSymbol(ri.Name)
-	if !ok {
-		panic(fmt.Sprintf("internal: range driver %q not found in scope (should have been caught by type solver)", ri.Name))
+		sym, ok := c.getRawSymbol(ri.Name)
+		if !ok {
+			panic(fmt.Sprintf("internal: range driver %q not found in scope (should have been caught by type solver)", ri.Name))
+		}
+		values[i] = c.rangeSymbol(sym, ri.Name)
 	}
-	return c.rangeAggregateFromSymbol(sym, ri.Name)
+	return values
 }
 
-// iterOverRangeInfo iterates a single driver, binding its per-iteration scalar value.
-func (c *Compiler) iterOverRangeInfo(ri *RangeInfo, body func(*Symbol)) {
-	if ri.RangeLit != nil {
-		rangeType := Range{Iter: Int{Width: 64}}
-		rangeVal := c.ToRange(ri.RangeLit, rangeType)
-		c.iterOverRange(rangeType, rangeVal, func(iter llvm.Value, iterType Type) {
-			body(&Symbol{Val: iter, Type: iterType, Borrowed: true})
-		})
-		return
-	}
-
-	sym, ok := c.getRawSymbol(ri.Name)
-	if !ok {
-		panic(fmt.Sprintf("internal: range driver %q not found in scope (should have been caught by type solver)", ri.Name))
-	}
-	c.iterOverDriverSymbol(sym, ri.Name, body)
+// rangeLiteralValue builds an iterated range literal's range: empty unless
+// every bound yields, through its conditions and checked accesses alike.
+func (c *Compiler) rangeLiteralValue(lit *ast.RangeLiteral) *Symbol {
+	rangeType := Range{Iter: Int{Width: 64}}
+	empty := c.makeZeroValue(rangeType).Val
+	slot := c.createEntryBlockAlloca(c.mapToLLVMType(rangeType), "range_lit")
+	c.createStore(empty, slot, rangeType)
+
+	c.compileCondOperands(lit, func() {
+		guardPtr := c.pushBoundsGuard("range_bounds_guard")
+		rangeVal := c.ToRange(lit, rangeType)
+		if c.stmtBoundsUsed() {
+			inBounds := c.createLoad(guardPtr, Int{Width: 1}, "range_bounds_ok")
+			rangeVal = c.builder.CreateSelect(inBounds, rangeVal, empty, "range_or_empty")
+		}
+		c.popBoundsGuard()
+		c.createStore(rangeVal, slot, rangeType)
+	})
+	return &Symbol{Val: c.createLoad(slot, rangeType, "range_lit_val"), Type: rangeType}
 }
 
 // Build a nested loop over specs; at each level shadow specs[i].Name with the scalar iter; run body at innermost.
 func (c *Compiler) withLoopNest(ranges []*RangeInfo, body func()) {
 	ranges = c.pendingLoopRanges(ranges)
+	c.withLoopNestOver(ranges, c.loopRangeValues(ranges), body)
+}
+
+// withLoopNestOver runs a loop nest over driver ranges built ahead of it.
+func (c *Compiler) withLoopNestOver(ranges []*RangeInfo, values []*Symbol, body func()) {
 	if len(ranges) == 0 {
 		body()
 		return
@@ -94,9 +93,10 @@ func (c *Compiler) withLoopNest(ranges []*RangeInfo, body func()) {
 			body()
 			return
 		}
-		c.iterOverRangeInfo(ranges[i], func(iterSym *Symbol) {
+		rangeSym := values[i]
+		c.iterOverRange(rangeSym.Type.(Range), rangeSym.Val, func(iter llvm.Value, iterType Type) {
 			PushScope(&c.Scopes, BlockScope)
-			Put(c.Scopes, ranges[i].Name, iterSym)
+			Put(c.Scopes, ranges[i].Name, &Symbol{Val: iter, Type: iterType, FuncArg: rangeSym.FuncArg, Borrowed: true})
 			rec(i + 1)
 			c.popScope()
 		})
@@ -166,9 +166,10 @@ func (c *Compiler) withLoopNestVersioned(ranges []*RangeInfo, probes []ast.Expre
 		return
 	}
 
-	guard, fastAccess, ok := c.affineVersioningGuard(probes, pending)
+	values := c.loopRangeValues(pending)
+	guard, fastAccess, ok := c.affineVersioningGuard(probes, pending, values)
 	if !ok {
-		c.withLoopNest(ranges, body)
+		c.withLoopNestOver(pending, values, body)
 		return
 	}
 
@@ -176,13 +177,13 @@ func (c *Compiler) withLoopNestVersioned(ranges []*RangeInfo, probes []ast.Expre
 
 	c.builder.SetInsertPointAtEnd(fastBlock)
 	c.pushLoopBoundsMode(loopBoundsModeAffineFast, fastAccess)
-	c.withLoopNest(ranges, body)
+	c.withLoopNestOver(pending, values, body)
 	c.popLoopBoundsMode()
 	c.builder.CreateBr(contBlock)
 
 	c.builder.SetInsertPointAtEnd(checkedBlock)
 	c.pushLoopBoundsMode(loopBoundsModeChecked, nil)
-	c.withLoopNest(ranges, body)
+	c.withLoopNestOver(pending, values, body)
 	c.popLoopBoundsMode()
 	c.builder.CreateBr(contBlock)
 
diff --git a/compiler/scriptcompiler.go b/compiler/scriptcompiler.go
index dd7960f3..d2a9b7f1 100644
--- a/compiler/scriptcompiler.go
+++ b/compiler/scriptcompiler.go
@@ -24,13 +24,6 @@ type Script struct {
 	Root *FuncInfo
 }
 
-type cfgDiagnosticKey struct {
-	fileName string
-	line     int
-	column   int
-	message  string
-}
-
 func NewScriptCompiler(ctx llvm.Context, name string, program *ast.Program, cc *CodeCompiler) *ScriptCompiler {
 	compiler := NewCompiler(ctx, cc.Compiler.MangledPath, cc)
 	script := &Script{
@@ -62,8 +55,6 @@ func (sc *ScriptCompiler) Compile() []*token.CompileError {
 
 	cfg := NewCFG(sc.Compiler.CodeCompiler)
 	cfg.AnalyzeScript(sc.Program.Statements, sc.Script.Root.StatementEffects)
-	directCallees, _ := collectSpecializationCallEdges(sc.Compiler, sc.ScriptMangled, sc.Program.Statements)
-	cfg.Errors = replaySpecializationCFG(sc.Compiler, directCallees, cfg.Errors)
 	if len(cfg.Errors) > 0 {
 		return cfg.Errors
 	}
@@ -102,55 +93,3 @@ func (sc *ScriptCompiler) compileStatements() {
 		c.compileStatement(stmt)
 	}
 }
-
-// replaySpecializationCFG reports the settled dataflow diagnostics of every
-// specialization the script reaches, root-first and depth-first in source
-// order, deduplicated by location and message. A body is analyzed once per
-// type specialization at settlement, independent of its callers: sharing an
-// input with an output only adds reads, so it can never make a body invalid,
-// and a body must be valid without it.
-func replaySpecializationCFG(compiler *Compiler, roots []string, errors []*token.CompileError) []*token.CompileError {
-	visited := make(map[string]struct{})
-	reported := make(map[cfgDiagnosticKey]struct{}, len(errors))
-	for _, compileError := range errors {
-		reported[cfgDiagnosticKeyFor(compileError)] = struct{}{}
-	}
-
-	for _, mangled := range roots {
-		errors = replaySpecializationCFGNode(compiler, mangled, visited, reported, errors)
-	}
-
-	return errors
-}
-
-func replaySpecializationCFGNode(compiler *Compiler, mangled string, visited map[string]struct{}, reported map[cfgDiagnosticKey]struct{}, errors []*token.CompileError) []*token.CompileError {
-	if _, seen := visited[mangled]; seen {
-		return errors
-	}
-	visited[mangled] = struct{}{}
-
-	info := compiler.FuncCache[mangled]
-	for _, compileError := range info.CFGResult.Errors {
-		key := cfgDiagnosticKeyFor(compileError)
-		if _, seen := reported[key]; seen {
-			continue
-		}
-
-		reported[key] = struct{}{}
-		errors = append(errors, compileError)
-	}
-	for _, callee := range info.CFGResult.DirectCallees {
-		errors = replaySpecializationCFGNode(compiler, callee, visited, reported, errors)
-	}
-
-	return errors
-}
-
-func cfgDiagnosticKeyFor(compileError *token.CompileError) cfgDiagnosticKey {
-	return cfgDiagnosticKey{
-		fileName: compileError.Token.FileName,
-		line:     compileError.Token.Line,
-		column:   compileError.Token.Column,
-		message:  compileError.Msg,
-	}
-}
diff --git a/compiler/solver.go b/compiler/solver.go
index 73285be6..2aba0881 100644
--- a/compiler/solver.go
+++ b/compiler/solver.go
@@ -128,11 +128,8 @@ type pendingAssignment struct {
 }
 
 type walkedSpecialization struct {
-	// walkIndex is dense within the current solver pass and becomes the
-	// specialization call graph node ID.
-	walkIndex int
-	info      *FuncInfo
-	template  *ast.FuncStatement
+	info     *FuncInfo
+	template *ast.FuncStatement
 }
 
 type TypeSolver struct {
@@ -676,11 +673,12 @@ func rangeDriverNamed(ranges []*RangeInfo, name string) bool {
 	return false
 }
 
-// resolveBareRangeAssignment distinguishes Range descriptor copies from uses of
-// a Range that an enclosing statement condition has already bound as an
-// iterator. `copy = source` and `copy = 0:n` preserve the descriptor; in
-// `filtered = source > 2 source`, the RHS reads the current scalar yield.
-func (ts *TypeSolver) resolveBareRangeAssignment(expr ast.Expression, types []Type, condRanges []*RangeInfo) {
+// resolveBareRangeAssignment settles a bare range value at an assignment root.
+// Without a gate, a range literal constructs the descriptor and a range name
+// copies it (`r = 0:n`, `copy = r`). Under a gate the value is a computation
+// like any other: the range iterates and the assignment keeps its final
+// element (`last = n > 0 r`).
+func (ts *TypeSolver) resolveBareRangeAssignment(expr ast.Expression, types []Type, gated bool) {
 	if len(types) != 1 {
 		return
 	}
@@ -690,22 +688,22 @@ func (ts *TypeSolver) resolveBareRangeAssignment(expr ast.Expression, types []Ty
 		return
 	}
 
+	switch expr.(type) {
+	case *ast.Identifier, *ast.RangeLiteral:
+	default:
+		return
+	}
+
 	info := ts.ExprCache[key(ts.FuncNameMangled, expr)]
-	switch e := expr.(type) {
-	case *ast.Identifier:
-		if !rangeDriverNamed(condRanges, e.Value) {
-			info.Ranges = nil
-			info.HasRanges = false
-			info.Rewrite = nil
-			return
-		}
-		types[0] = rangeType.Iter
-		info.OutTypes[0] = rangeType.Iter
-	case *ast.RangeLiteral:
+	if !gated {
 		info.Ranges = nil
 		info.HasRanges = false
 		info.Rewrite = nil
+		return
 	}
+	info.HasRanges = true
+	types[0] = rangeType.Iter
+	info.OutTypes[0] = rangeType.Iter
 }
 
 func (ts *TypeSolver) TypeStatement(stmt ast.Statement) {
@@ -823,10 +821,11 @@ func (ts *TypeSolver) isRangeDriverCond(expr ast.Expression, condTypes []Type) b
 
 // treeCanFail reports whether a value-position expression can propagate a
 // failed yield to its parent, asking nodeFails to classify each node. An array
-// literal settles a failed cell locally, and a || fails only when its final
-// fallback does.
+// literal settles a failed cell locally, a range literal a failed bound with
+// its range, and a || fails only when its final fallback does.
 func treeCanFail(expr ast.Expression, nodeFails func(ast.Expression) bool) bool {
-	if _, ok := expr.(*ast.ArrayLiteral); ok {
+	switch expr.(type) {
+	case *ast.ArrayLiteral, *ast.RangeLiteral:
 		return false
 	}
 	if infix, ok := ast.IsLogicalOr(expr); ok {
@@ -972,7 +971,7 @@ func (ts *TypeSolver) TypeLetStatement(stmt *ast.LetStatement) {
 	exprIdxs := make([]int, 0, len(stmt.Name))
 	for _, expr := range stmt.Value {
 		exprTypes := ts.TypeExpression(expr, true)
-		ts.resolveBareRangeAssignment(expr, exprTypes, condRanges)
+		ts.resolveBareRangeAssignment(expr, exprTypes, len(stmt.Condition) > 0)
 		ts.mergeCondRangesIntoValue(expr, condRanges)
 		for idx := range exprTypes {
 			types = append(types, exprTypes[idx])
@@ -984,7 +983,7 @@ func (ts *TypeSolver) TypeLetStatement(stmt *ast.LetStatement) {
 	if len(stmt.Name) != len(types) {
 		ce := &token.CompileError{
 			Token: stmt.Token,
-			Msg:   fmt.Sprintf("Statement lhs identifiers are not equal to rhs values!!! lhs identifiers: %d. rhs values: %d. Stmt %q", len(stmt.Name), len(types), stmt),
+			Msg:   assignmentMismatch(len(stmt.Name), len(types)),
 		}
 		ts.Errors = append(ts.Errors, ce)
 		return
@@ -1986,7 +1985,7 @@ func (ts *TypeSolver) typeLogicalAndExpression(expr *ast.InfixExpression, left,
 	if len(left) != len(right) && len(left) != 1 && len(right) != 1 {
 		ts.Errors = append(ts.Errors, &token.CompileError{
 			Token: expr.Token,
-			Msg:   fmt.Sprintf("logical AND condition arity must match the value's, fold to one, or broadcast from one — got %d and %d", len(left), len(right)),
+			Msg:   logicalAndArityMismatch(len(left), len(right)),
 		})
 		types := []Type{Unresolved{}}
 		ts.ExprCache[key(ts.FuncNameMangled, expr)] = &ExprInfo{OutTypes: types, ExprLen: 1}
@@ -2053,7 +2052,7 @@ func (ts *TypeSolver) TypeInfixExpression(expr *ast.InfixExpression) (types []Ty
 	if len(left) != len(right) {
 		ce := &token.CompileError{
 			Token: expr.Token,
-			Msg:   fmt.Sprintf("left expression and right expression have unequal lengths! Left expr: %s, length: %d. Right expr: %s, length: %d. Operator: %q", expr.Left, len(left), expr.Right, len(right), expr.Token.Literal),
+			Msg:   operandMismatch(expr.Token.Literal, len(left), len(right)),
 		}
 		ts.Errors = append(ts.Errors, ce)
 		types = []Type{Unresolved{}}
@@ -2546,7 +2545,7 @@ func (ts *TypeSolver) lookupCallTemplate(ce *ast.CallExpression, args []Type) (*
 	if !ok {
 		cerr := &token.CompileError{
 			Token: ce.Token,
-			Msg:   fmt.Sprintf("undefined function: %s", ce.Function.Value),
+			Msg:   undefinedFunction(ce.Function.Value),
 		}
 		ts.Errors = append(ts.Errors, cerr)
 		return nil, "", false
@@ -2564,9 +2563,7 @@ func newFunc(name string, bodyArgs []Type, template *ast.FuncStatement) *FuncInf
 			Params:   bodyArgs,
 			OutTypes: make([]Type, len(template.Outputs)),
 		},
-		Vars:              make(map[string]Type),
-		StatementEffects:  make(map[*ast.LetStatement]StatementEffect),
-		BodyOutputEffects: slices.Repeat([]WriteEffect{WriteUncomputed}, len(template.Outputs)),
+		Vars: make(map[string]Type),
 	}
 	for i := range f.Sig.OutTypes {
 		f.Sig.OutTypes[i] = Unresolved{}
@@ -2645,8 +2642,7 @@ func (ts *TypeSolver) TypeScriptFunc(mangled string, template *ast.FuncStatement
 					panic(fmt.Sprintf("internal: cannot settle incomplete specialization %s", mangled))
 				}
 			}
-			graph := ts.buildSpecializationCallGraph()
-			ts.settleSpecializationBatch(graph)
+			ts.settleSpecializationBatch()
 			return f.Sig.OutTypes
 		}
 
@@ -2664,29 +2660,29 @@ func (ts *TypeSolver) TypeScriptFunc(mangled string, template *ast.FuncStatement
 	}
 }
 
-// settleSpecializationBatch publishes reusable analysis facts atomically with
-// respect to Settled: every CFG result is staged and installed before any
-// specialization in the batch becomes visible as settled.
-func (ts *TypeSolver) settleSpecializationBatch(graph *specializationCallGraph) {
-	ts.settleEffects(graph)
-	staged := make([]*SpecializationCFGResult, len(graph.nodes))
-
-	for id, node := range graph.nodes {
-		walked := ts.walkedFuncs[node.mangled]
-		cfg := NewCFG(ts.ScriptCompiler.Compiler.CodeCompiler)
-		cfg.AnalyzeSpecialization(walked.template, walked.info)
-		staged[id] = &SpecializationCFGResult{
-			DirectCallees: slices.Clone(node.directCallees),
-			Errors:        slices.Clone(cfg.Errors),
-		}
+// settleSpecializationBatch publishes the walked specializations atomically
+// with respect to Settled: each is checked against its template's text range
+// summary before any becomes visible as settled.
+func (ts *TypeSolver) settleSpecializationBatch() {
+	rangeBindings := ts.ScriptCompiler.Compiler.CodeCompiler.rangeBindings
+	for _, walked := range ts.walkedFuncs {
+		checkSettledRanges(rangeBindings[templateKey(walked.template)], walked.info)
 	}
 
-	for id, node := range graph.nodes {
-		ts.walkedFuncs[node.mangled].info.CFGResult = staged[id]
+	for _, walked := range ts.walkedFuncs {
+		walked.info.Settled = true
 	}
+}
 
-	for _, node := range graph.nodes {
-		ts.walkedFuncs[node.mangled].info.Settled = true
+// checkSettledRanges panics when a settled specialization types a binding as
+// a Range where its template's text summary does not, or the reverse: the
+// template checks classified the body's writes from that summary.
+func checkSettledRanges(textRanges map[string]struct{}, info *FuncInfo) {
+	for name, typ := range info.Vars {
+		_, textRange := textRanges[name]
+		if textRange != (typ.Kind() == RangeKind) {
+			panic(fmt.Sprintf("internal: %s solves %q as %s, which disagrees with its template's text range summary", info.Sig.Name, name, typ))
+		}
 	}
 }
 
@@ -2695,19 +2691,14 @@ func (ts *TypeSolver) settleSpecializationBatch(graph *specializationCallGraph)
 func (ts *TypeSolver) TypeFunc(mangled string, template *ast.FuncStatement) bool {
 	f := ts.ScriptCompiler.Compiler.FuncCache[mangled]
 	if f.Settled {
-		if f.CFGResult == nil {
-			panic(fmt.Sprintf("internal: settled specialization %s has no CFG result", mangled))
-		}
-
 		return true
 	}
 	if _, ok := ts.walkedFuncs[mangled]; ok {
 		return f.OutputTypesInferred()
 	}
 	ts.walkedFuncs[mangled] = walkedSpecialization{
-		walkIndex: len(ts.walkedFuncs),
-		info:      f,
-		template:  template,
+		info:     f,
+		template: template,
 	}
 	revision := ts.storageRevision
 	previousSlots := ts.previousSlotTypes
@@ -2758,7 +2749,7 @@ func (ts *TypeSolver) TypeBlock(template *ast.FuncStatement, f *FuncInfo) {
 		}
 	}
 
-	readOutputs := ts.ScriptCompiler.Compiler.CodeCompiler.outputReads[funcKey{name: f.Sig.Name, arity: len(template.Parameters)}]
+	readOutputs := ts.ScriptCompiler.Compiler.CodeCompiler.outputReads[templateKey(template)]
 	for i, id := range template.Outputs {
 		outArg, ok := Get(ts.Scopes, id.Value)
 		if !ok {
diff --git a/compiler/solver_test.go b/compiler/solver_test.go
index a2b6d697..9eb96fe2 100644
--- a/compiler/solver_test.go
+++ b/compiler/solver_test.go
@@ -34,16 +34,20 @@ func numberedNames(prefix string, count int) string {
 func TestMutualRecursion(t *testing.T) {
 	codeStr := `# define isEven: returns (x, y) = (is-even?, is-odd?)
 x, y = isEven(n)
-    # recursive step: if n≠0, flip the pair returned by isOdd(n-1)
-    x, y = n != 0 isOdd(n - 1)
+    # recursive step: if n≠0, flip the pair returned by isOdd(n-1); a
+    # skipped step leaves the locals empty, and every output is still written
+    odd, even = n != 0 isOdd(n - 1)
+    x, y = odd, even
     # base case: 0 is even, not odd
     x = n == 1 "no"
     x = n == 0 "yes"
 
 # define isOdd: returns (x, y) = (is-odd?, is-even?)
+# this function infers x only through isEven
 x, y = isOdd(n)
     # recursive step: if n≠0, flip the pair returned by isEven(n-1)
-    x, y = n != 0 isEven(n - 1)
+    even, odd = n != 0 isEven(n - 1)
+    x, y = even, odd
     # base case: 0 is not odd, but even
     y = n == 1 "no"
     y = n == 0 "yes"`
@@ -76,14 +80,12 @@ x, y`
 	require.True(t, ok)
 	isEvenFunc := newFunc(call.Function.Value, args, template)
 	cc.Compiler.FuncCache[isEvenMangled] = isEvenFunc
-	require.Equal(t, []WriteEffect{WriteUncomputed, WriteUncomputed}, isEvenFunc.BodyOutputEffects)
 	isOddMangled := Mangle(cc.Compiler.MangledPath, "isOdd", args)
 
 	ts.Converging = false
 	ts.firstUnresolved = nil
 	clear(ts.walkedFuncs)
 	require.True(t, ts.TypeFunc(isEvenMangled, template))
-	require.Equal(t, []WriteEffect{WriteUncomputed, WriteUncomputed}, isEvenFunc.BodyOutputEffects)
 	isOddFunc := cc.Compiler.FuncCache[isOddMangled]
 	require.NotNil(t, isOddFunc)
 	require.True(t, isEvenFunc.AllTypesInferred())
@@ -110,8 +112,6 @@ x, y`
 	require.False(t, ts.Converging)
 	require.True(t, isEvenFunc.Settled)
 	require.True(t, isOddFunc.Settled)
-	require.Equal(t, []WriteEffect{MayWrite, MayWrite}, isEvenFunc.BodyOutputEffects)
-	require.Equal(t, []WriteEffect{MayWrite, MayWrite}, isOddFunc.BodyOutputEffects)
 
 	ts.Solve()
 	require.Empty(t, ts.Errors)
@@ -632,6 +632,42 @@ func TestArrayConcatTypeErrors(t *testing.T) {
 	}
 }
 
+// A script reports a count mismatch or an unknown call in the words a
+// template's text check uses.
+func TestScriptSharesTemplateTextMessages(t *testing.T) {
+	const pairs = `p, q = Pair(n)
+    p, q = n, n + 1
+
+a, b, c = Three(n)
+    a, b, c = n, n, n`
+	tests := []struct {
+		name   string
+		script string
+		err    string
+	}{
+		{name: "AssignmentMismatch", script: "a, b = 1\na", err: "assignment mismatch: 2 targets but 1 value"},
+		{name: "UndefinedFunction", script: "a = Missing(1)\na", err: "undefined function: Missing"},
+		{name: "OperandMismatch", script: "a = Pair(1) * 2\na", err: `operand mismatch: "*" has 2 values on its left but 1 value on its right`},
+		{name: "AndArityMismatch", script: "a = Pair(1 > 0) && Three(1)\na", err: "logical AND condition arity must match the value's, fold to one, or broadcast from one — got 2 and 3"},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			ctx := llvm.NewContext()
+			defer ctx.Dispose()
+
+			cc := NewCodeCompiler(ctx, test.name, "", mustParseCode(t, pairs))
+			require.Empty(t, cc.Compile())
+			sc := NewScriptCompiler(ctx, test.name, mustParseScript(t, test.script), cc)
+			ts := NewTypeSolver(sc)
+			ts.Solve()
+
+			require.NotEmpty(t, ts.Errors)
+			require.Equal(t, test.err, ts.Errors[0].Msg)
+		})
+	}
+}
+
 func TestArrayToScalarAssignmentError(t *testing.T) {
 	ctx := llvm.NewContext()
 	cc := NewCodeCompiler(ctx, "arrayToScalar", "", ast.NewCode())
@@ -764,7 +800,7 @@ out, before = Fold(current, item)
 		require.True(t, wrapper.Settled)
 		require.True(t, IsStrH(wrapper.Vars["current"]))
 		require.True(t, IsStrH(wrapper.Sig.OutTypes[1]))
-		require.Equal(t, []string{foldKey}, wrapper.CFGResult.DirectCallees)
+		require.Contains(t, cc.Compiler.FuncCache, foldKey)
 		info := ts.ExprCache[key(wrapperKey, call)]
 		require.True(t, IsStrH(info.CallParamTypes[0]))
 		require.True(t, IsStrH(info.OutTypes[1]))
@@ -832,7 +868,7 @@ func TestMergeBindingSlotTypeIsMonotonic(t *testing.T) {
 
 func TestFunctionOutputBindingRejectsIncompatibleReassignment(t *testing.T) {
 	code := mustParseCode(t, `res = Bad(k)
-    res = k == 0 1
+    res = 1
     res = k != 0 "later"
 `)
 	ctx := llvm.NewContext()
@@ -857,6 +893,60 @@ func TestFunctionOutputBindingRejectsIncompatibleReassignment(t *testing.T) {
 	require.Equal(t, "test.pt:3:5", err.Token.Location())
 }
 
+// A body that reassigns a name between a range and a non-range value, and
+// passes the flow checks as written, gets the solver's retype error, as for
+// any other type. The per-template pass reads each name by its latest
+// assignment: read as a range, r would make res a range output in
+// RangeToNonRange.
+func TestFunctionRangeRetypeIsReportedBySolver(t *testing.T) {
+	tests := []struct {
+		name     string
+		code     string
+		msg      string
+		location string
+	}{
+		{
+			name: "RangeToNonRange",
+			code: `res = Retype(n)
+    r = 0:n
+    t = 0
+    t = t + r
+    r = t + 1
+    res = r`,
+			msg:      `cannot reassign type to identifier. Old Type: I64:I64:I64. New Type: I64. Identifier "r"`,
+			location: "test.pt:5:5",
+		},
+		{
+			name: "NonRangeToRange",
+			code: `res = Retype(n)
+    r = n
+    res = r + 1
+    r = 1:n
+    res = res + r`,
+			msg:      `cannot reassign type to identifier. Old Type: I64. New Type: I64:I64:I64. Identifier "r"`,
+			location: "test.pt:4:5",
+		},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			ctx := llvm.NewContext()
+			defer ctx.Dispose()
+
+			cc := NewCodeCompiler(ctx, test.name, "", mustParseCode(t, test.code))
+			require.Empty(t, cc.Compile())
+
+			sc := NewScriptCompiler(ctx, test.name, mustParseScript(t, "value = Retype(4)\nvalue"), cc)
+			ts := NewTypeSolver(sc)
+			ts.Solve()
+
+			require.Len(t, ts.Errors, 1)
+			require.Equal(t, test.msg, ts.Errors[0].Msg)
+			require.Equal(t, test.location, ts.Errors[0].Token.Location())
+		})
+	}
+}
+
 func TestRangeBoundsCannotDependOnRangeValues(t *testing.T) {
 	ctx := llvm.NewContext()
 	cc := NewCodeCompiler(ctx, "rangeBoundsDepend", "", ast.NewCode())
@@ -1145,6 +1235,13 @@ func TestLogicalAndDiagnostics(t *testing.T) {
 			script:      "n = 5\nx = n && 10",
 			expectError: "logical AND in value position requires a conditional left operand",
 		},
+		{
+			// A failed bound empties its range rather than failing the value
+			// around it.
+			name:        "RangeBoundCannotFailItsValue",
+			script:      "n = 3\nx = (0:(n > 0) + 0) && 99",
+			expectError: "logical AND in value position requires a conditional left operand",
+		},
 		{
 			// An always-yielding || (a > 0 || a always yields a value) cannot
 			// gate a &&.
@@ -1222,6 +1319,13 @@ func TestLogicalOrDiagnostics(t *testing.T) {
 			script:      "x = 1 || 2",
 			expectError: "logical OR in value position requires a conditional left operand",
 		},
+		{
+			// A failed bound empties its range rather than failing the value
+			// around it, as for a range built before the statement.
+			name:        "RangeBoundCannotFailItsValue",
+			script:      "n = 3\nx = (0:(n > 0) + 0) || 99",
+			expectError: "logical OR in value position requires a conditional left operand",
+		},
 		{
 			name:        "FallbackTypesMustMatch",
 			script:      "a = 1\nx = a > 0 || \"fallback\"",
@@ -1345,27 +1449,34 @@ res = [idx]`
 	require.IsType(t, &ast.ArrayLiteral{}, info.Rewrite)
 }
 
-func TestBareRangeAssignmentsCopyDescriptors(t *testing.T) {
+// A bare range assigned without a gate is the range itself: a name copies it,
+// beside other values too. Under a gate the value is a computation, so the
+// range iterates whether or not the condition names it. A main marker
+// formats the range it names.
+func TestBareRangeAssignmentsCopyOnlyWithoutAGate(t *testing.T) {
 	ctx := llvm.NewContext()
 	cc := NewCodeCompiler(ctx, "bareRangeCopies", "", ast.NewCode())
 	program := mustParseScript(t, `source = 0:5
 copy = (source)
 last = source + 0
 outer = 0:2
-gatedCopy = outer < 2 source
-filtered = source > 2 source`)
+gatedName = outer < 2 source
+filtered = source > 2 source
+pairCopy, pairSum = source, source + 0
+marked = "v -source"
+gatedLiteral = outer < 2 0:3`)
 
 	sc := NewScriptCompiler(ctx, t.Name(), program, cc)
 	ts := NewTypeSolver(sc)
 	ts.Solve()
 	require.Emptyf(t, ts.Errors, "unexpected type errors: %v", ts.Errors)
 
-	for _, name := range []string{"source", "copy", "gatedCopy"} {
+	for _, name := range []string{"source", "copy", "pairCopy"} {
 		typ, ok := ts.GetIdentifier(name)
 		require.Truef(t, ok, "expected %s binding", name)
 		require.Equal(t, Range{Iter: I64}, typ)
 	}
-	for _, name := range []string{"last", "filtered"} {
+	for _, name := range []string{"last", "gatedName", "filtered", "pairSum", "gatedLiteral"} {
 		typ, ok := ts.GetIdentifier(name)
 		require.Truef(t, ok, "expected %s binding", name)
 		require.Equal(t, I64, typ)
@@ -1377,17 +1488,53 @@ filtered = source > 2 source`)
 	require.Empty(t, copyInfo.Ranges)
 	require.Nil(t, copyInfo.Rewrite)
 
-	gatedCopyExpr := program.Statements[4].(*ast.LetStatement).Value[0]
-	gatedCopyInfo := ts.ExprCache[key(ts.FuncNameMangled, gatedCopyExpr)]
-	require.Equal(t, []Type{Range{Iter: I64}}, gatedCopyInfo.OutTypes)
-	require.Len(t, gatedCopyInfo.Ranges, 1)
-	require.Equal(t, "outer", gatedCopyInfo.Ranges[0].Name)
+	gatedNameExpr := program.Statements[4].(*ast.LetStatement).Value[0]
+	gatedNameInfo := ts.ExprCache[key(ts.FuncNameMangled, gatedNameExpr)]
+	require.Equal(t, []Type{I64}, gatedNameInfo.OutTypes)
+	gatedDrivers := make([]string, len(gatedNameInfo.Ranges))
+	for i, driver := range gatedNameInfo.Ranges {
+		gatedDrivers[i] = driver.Name
+	}
+	require.ElementsMatch(t, []string{"outer", "source"}, gatedDrivers)
 
 	filteredExpr := program.Statements[5].(*ast.LetStatement).Value[0]
 	filteredInfo := ts.ExprCache[key(ts.FuncNameMangled, filteredExpr)]
 	require.Equal(t, []Type{I64}, filteredInfo.OutTypes)
 	require.Len(t, filteredInfo.Ranges, 1)
 	require.Equal(t, "source", filteredInfo.Ranges[0].Name)
+
+	markedExpr := program.Statements[7].(*ast.LetStatement).Value[0]
+	markedInfo := ts.ExprCache[key(ts.FuncNameMangled, markedExpr)]
+	require.False(t, markedInfo.HasRanges)
+	require.Empty(t, markedInfo.Ranges)
+}
+
+// A string's width and precision operands drive in the order they appear,
+// and a main marker formats its range without driving.
+func TestSpecifierDriversFollowTextOrder(t *testing.T) {
+	ctx := llvm.NewContext()
+	cc := NewCodeCompiler(ctx, "specifierOrder", "", ast.NewCode())
+	program := mustParseScript(t, `n = 1.5
+w = 1:3
+p = 2:4
+j = 7:9
+s = "|-n%(-w).(-p)f| -j"
+t = "-j |-n%(-p).(-w)f|"`)
+
+	sc := NewScriptCompiler(ctx, t.Name(), program, cc)
+	ts := NewTypeSolver(sc)
+	ts.Solve()
+	require.Emptyf(t, ts.Errors, "unexpected type errors: %v", ts.Errors)
+
+	for i, want := range [][]string{{"w", "p"}, {"p", "w"}} {
+		lit := program.Statements[4+i].(*ast.LetStatement).Value[0]
+		info := ts.ExprCache[key(ts.FuncNameMangled, lit)]
+		drivers := make([]string, len(info.Ranges))
+		for k, driver := range info.Ranges {
+			drivers[k] = driver.Name
+		}
+		require.Equal(t, want, drivers)
+	}
 }
 
 func TestRangedArrayAccessTypesAsElementStream(t *testing.T) {
@@ -1580,7 +1727,7 @@ func closureLeafWalks(t *testing.T, depth, callSites int) int {
 	for i := range depth {
 		fmt.Fprintf(&b, "res = F%d(k)\n    a = F%d(k)\n    b = F%d(k + 1)\n    res = a + b\n\n", i, i+1, i+1)
 	}
-	fmt.Fprintf(&b, "res = F%d(k)\n    i = 0:2\n    res = k + i\n", depth)
+	fmt.Fprintf(&b, "res = F%d(k)\n    res = k + (0:2)\n", depth)
 
 	l := lexer.New("TestFuncClosureCode", b.String())
 	cp := parser.NewCodeParser(l)
@@ -1976,13 +2123,6 @@ scaled`)
 	primaryMangled := Mangle(cc.Compiler.MangledPath, "Scale", callInfo.CallParamTypes)
 	scalarMangled := Mangle(cc.Compiler.MangledPath, "Scale", []Type{I64})
 	require.True(t, callInfo.ScalarCallVariantEnsured)
-	directCallees, _ := collectSpecializationCallEdges(sc.Compiler, sc.ScriptMangled, program.Statements)
-	require.Equal(t, []string{primaryMangled, scalarMangled}, directCallees)
-	callInfo.ScalarCallVariantEnsured = false
-	directCallees, _ = collectSpecializationCallEdges(sc.Compiler, sc.ScriptMangled, program.Statements)
-	require.Equal(t, []string{primaryMangled}, directCallees,
-		"a scalar key already present in the shared cache must not create an edge without a call-local ensured fact")
-	callInfo.ScalarCallVariantEnsured = true
 	require.Contains(t, cc.Compiler.FuncCache, primaryMangled)
 	require.Contains(t, cc.Compiler.FuncCache, scalarMangled)
 	template, ok := cc.lookupFuncTemplate("Scale", 1)
@@ -1993,84 +2133,6 @@ scaled`)
 		"diagnostic frames must retain the actual specialization key when body parameter types collapse")
 }
 
-func TestCFGDiagnosticsDoNotFailSolver(t *testing.T) {
-	code := mustParseCode(t, `result = Noisy(x)
-    unused = x
-    result = x
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "specializationCFGDiagnostics", "", code)
-	require.Empty(t, cc.Compile())
-
-	ts := solveScriptTypes(t, ctx, cc, t.Name(), "value = Noisy(1)\nvalue")
-	mangled := Mangle(cc.Compiler.MangledPath, "Noisy", []Type{I64})
-	info := cc.Compiler.FuncCache[mangled]
-
-	require.Empty(t, ts.Errors, "function CFG diagnostics must not become type-solver failures")
-	require.True(t, info.Settled)
-	require.NotNil(t, info.CFGResult)
-	require.Len(t, info.CFGResult.Errors, 1)
-	require.Contains(t, info.CFGResult.Errors[0].Msg, `"unused"`)
-}
-
-func TestCFGRecordsSettledDirectCallee(t *testing.T) {
-	code := mustParseCode(t, `result = Leaf(x)
-    result = x
-
-result = Wrapper(x)
-    result = Leaf(x)
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "settledCFGEdge", "", code)
-	require.Empty(t, cc.Compile())
-
-	solveScriptTypes(t, ctx, cc, t.Name()+"Leaf", "value = Leaf(1)\nvalue")
-	leafMangled := Mangle(cc.Compiler.MangledPath, "Leaf", []Type{I64})
-	leaf := cc.Compiler.FuncCache[leafMangled]
-	require.True(t, leaf.Settled)
-	require.NotNil(t, leaf.CFGResult)
-	require.Empty(t, leaf.CFGResult.Errors)
-	require.Empty(t, leaf.CFGResult.DirectCallees)
-
-	solveScriptTypes(t, ctx, cc, t.Name()+"Wrapper", "value = Wrapper(1)\nvalue")
-	wrapperMangled := Mangle(cc.Compiler.MangledPath, "Wrapper", []Type{I64})
-	wrapper := cc.Compiler.FuncCache[wrapperMangled]
-
-	require.True(t, wrapper.Settled)
-	require.NotNil(t, wrapper.CFGResult)
-	require.Equal(t, []string{leafMangled}, wrapper.CFGResult.DirectCallees)
-}
-
-func TestSettledSpecializationRequiresCFG(t *testing.T) {
-	code := mustParseCode(t, `result = Leaf(x)
-    result = x
-
-result = Wrapper(x)
-    result = Leaf(x)
-`)
-
-	ctx := llvm.NewContext()
-	defer ctx.Dispose()
-	cc := NewCodeCompiler(ctx, "missingSettledCFG", "", code)
-	require.Empty(t, cc.Compile())
-
-	solveScriptTypes(t, ctx, cc, t.Name()+"Leaf", "value = Leaf(1)\nvalue")
-	leafMangled := Mangle(cc.Compiler.MangledPath, "Leaf", []Type{I64})
-	cc.Compiler.FuncCache[leafMangled].CFGResult = nil
-
-	program := mustParseScript(t, "value = Wrapper(1)\nvalue")
-	sc := NewScriptCompiler(ctx, t.Name()+"Wrapper", program, cc)
-	ts := NewTypeSolver(sc)
-	require.PanicsWithValue(t,
-		"internal: settled specialization "+leafMangled+" has no CFG result",
-		ts.Solve,
-	)
-}
-
 func TestNonConvergingCalleeIsBlamed(t *testing.T) {
 	codeStr := `y = m(x)
     y = bad(x)
@@ -2209,7 +2271,8 @@ p = Keep(q, n)
         1
         prior
     ]
-    z = tab.a[0]`,
+    t = tab.a[0]
+    z = t`,
 			script: "half, first = Mixed(2)\nhalf, first",
 			want:   map[string]Type{"half": F64, "first": F64},
 		},
@@ -2221,7 +2284,8 @@ p = Keep(q, n)
       : a b
         prior x
     ]
-    y = tab.b[0]`,
+    t = tab.b[0]
+    y = t`,
 			script: "v = Pick(2, 7)\nv",
 			want:   map[string]Type{"v": I64},
 		},
@@ -2276,7 +2340,8 @@ p = Keep(q, n)
         prior
     ]
     col = x > 3 && tab.a || [x]
-    y = col[0] + 1`,
+    t = col[0] + 1
+    y = t`,
 			script: "v = Pad(2, 5)\nv",
 			want:   map[string]Type{"v": I64},
 		},
@@ -2289,7 +2354,8 @@ p = Keep(q, n)
         prior
     ]
     col = x > 3 && [x] || tab.a
-    y = col[0] + 1`,
+    t = col[0] + 1
+    y = t`,
 			script: "v = PadRight(2, 5)\nv",
 			want:   map[string]Type{"v": I64},
 		},
@@ -2336,7 +2402,8 @@ func TestNonConvergingCalleeIsBlamedThroughCheckedUse(t *testing.T) {
 	defer ctx.Dispose()
 
 	cc := NewCodeCompiler(ctx, "test", "", mustParseCode(t, `y = m(x)
-    y = bad(x)[0]
+    t = bad(x)[0]
+    y = t
 
 y = bad(x)
     y = bad(x - 1)`))
@@ -2347,7 +2414,7 @@ y = bad(x)
 
 	require.Len(t, ts.Errors, 1)
 	require.Contains(t, ts.Errors[0].Msg, "Function bad is not converging")
-	require.Equal(t, 4, ts.Errors[0].Token.Line, "must point at bad's definition, not the index in m")
+	require.Equal(t, 5, ts.Errors[0].Token.Line, "must point at bad's definition, not the index in m")
 }
 
 // A check that waited for a recursive result still runs once the result is
@@ -2384,7 +2451,7 @@ func TestRecursiveResultChecksRunOnceTyped(t *testing.T) {
 			code: `y = R(n)
     y = n
     prior = n > 0 R(n - 1)
-    y = prior.age`,
+    y = y + prior.age`,
 			script: "v = R(3)\nv",
 			want:   "field access expects a struct or table value, got I64",
 		},
diff --git a/compiler/types.go b/compiler/types.go
index b902d3a0..0932ffe2 100644
--- a/compiler/types.go
+++ b/compiler/types.go
@@ -255,27 +255,14 @@ func (f Func) OutputTypesInferred() bool {
 	return true
 }
 
-// SpecializationCFGResult is the dataflow result and persistent direct-call
-// reachability for one settled function specialization. Errors is the
-// specialization's diagnostics, produced once at settlement and replayed by
-// every script that reaches it.
-type SpecializationCFGResult struct {
-	DirectCallees []string
-	Errors        []*token.CompileError
-}
-
-// FuncInfo holds the mutable facts for one function specialization. Settled
-// means all reusable type, effect, and CFG facts have been published; a settled
-// function specialization always has a non-nil CFG result.
+// FuncInfo holds the mutable facts for one function specialization or the
+// script root. Settled means a specialization's reusable type facts have been
+// published; StatementEffects are derived for the script root only.
 type FuncInfo struct {
 	Sig              Func
 	Vars             map[string]Type
 	StatementEffects map[*ast.LetStatement]StatementEffect
-	// BodyOutputEffects summarizes the typed scalar body before a call-owned
-	// Range or ArrayRange domain determines whether that body executes.
-	BodyOutputEffects []WriteEffect
-	CFGResult         *SpecializationCFGResult
-	Settled           bool
+	Settled          bool
 }
 
 func (f *FuncInfo) AllTypesInferred() bool {
diff --git a/docs/Pluto ABI Optimization Plan.md b/docs/Pluto ABI Optimization Plan.md
index 9ec0ae26..df1bf08e 100644
--- a/docs/Pluto ABI Optimization Plan.md	
+++ b/docs/Pluto ABI Optimization Plan.md	
@@ -29,17 +29,17 @@ Pluto's source-level semantics stay unchanged:
 
 - assignments copy
 - input names are read-only and keep their values for the whole call; today
-  they can observe writes through a shared output, which #123 (decided)
+  they can observe writes through a shared output, which #144 (decided)
   removes
-- every body that runs writes every output (#123, decided); output names are
-  readable only once definitely assigned, and results reach the caller at
-  assignment commit
+- every body that runs writes every output (#123); output names are readable
+  only once definitely assigned, and results reach the caller at assignment
+  commit
 
 These are **language semantics**. How values physically move across a call
 boundary is the **lowered calling convention** — a separate concern. An `I64`
 input can be passed by value provided the call site's alias pattern (the
 private `_aN` variant) redirects each read to its shared output when required;
-after #123 no read needs redirecting. A single `I64` output can be returned in a
+once inputs are stable (#144) no read needs redirecting. A single `I64` output can be returned in a
 register while still behaving like a Pluto output.
 
 ## 3. Architecture
@@ -115,9 +115,10 @@ wrong argument list. Write-effect information may still eliminate seed use
 inside Pluto code; a seedless fast path needs a distinctly named private clone
 behind the stable public entry point.
 
-#123 (decided) keeps that rule while removing the seed: whether a function
-keeps it depends on whether it has a range parameter, never on its write
-effects. The C ABI Spec §5.3 describes ABI 3.0.
+ABI 3.0 (#69) keeps that rule while removing the seed, which #123 left unused
+outside callee-owned domains: whether a function keeps it depends on whether
+it has a range parameter, never on its write effects. The C ABI Spec §5.3
+describes ABI 3.0.
 
 This was the highest-value initial optimization because it benefits all scalar-heavy code, not just specific patterns. It reduces stack traffic, simplifies IR, and materially improved `fib`, `fib_tail`, and `harmonic`.
 
diff --git a/docs/Pluto C ABI Spec.md b/docs/Pluto C ABI Spec.md
index 3f2d0da9..5dbf1197 100644
--- a/docs/Pluto C ABI Spec.md	
+++ b/docs/Pluto C ABI Spec.md	
@@ -333,15 +333,17 @@ types:
 - `I64` and `F64` parameters are passed directly. Ranges, internal
   `ArrayRange` descriptors, and other values are passed indirectly.
 - A function with exactly one `I64` or `F64` output returns that scalar
-  directly and receives one hidden seed value. The seed preserves the caller's
-  staged value when the callee does not write its output, including a failed
-  conditional assignment or an empty `Range`/internal `ArrayRange`.
+  directly and receives one hidden seed value. Every body that runs writes
+  every output (#123), so the seed preserves the caller's staged value only
+  when a `Range` or internal `ArrayRange` parameter runs no iteration; a
+  function without one never reads its seed.
 - All other output lists use an indirect `void` return. Argument zero points
   to a carrier whose first `N` fields are output pointers and whose next `N`
   fields are pointers to `i1` write markers.
 - The caller initializes every write marker to false. A callee sets the marker
-  only when that output is actually written. This lets an empty range or
-  skipped conditional preserve an existing caller destination.
+  when it writes that output, which every body that runs does. A marker left
+  false therefore means an empty range parameter, and the caller keeps its
+  existing destination.
 - Output expressions are staged independently at the call site, so one output
   cannot mutate a destination before a sibling right-hand side reads its
   statement-start value.
@@ -373,8 +375,8 @@ may-write—cannot alter the prototype of an existing symbol. A future seedless
 internal fast path must therefore use a distinct private symbol behind this
 stable boundary.
 
-The planned ABI 3.0 (§5.3) removes the seed and the write markers from every
-function without a `Range` or `ArrayRange` parameter.
+The planned ABI 3.0 (§5.3, #69) removes the seed and the write markers from
+every function without a `Range` or `ArrayRange` parameter.
 
 Conceptually, a two-output indirect call uses:
 
@@ -474,14 +476,14 @@ first parameter sharing its first output, which is therefore an `I64`.
 `Demangle` renders it as `math.Fold(I64 -> 1, StrH)`.
 
 The public specialization symbol is unchanged by the variant. C callers
-never see a variant and cannot request one. Under the planned ABI 3.0, a
+never see a variant and cannot request one. Once inputs are stable (#144), a
 variant can no longer change what a body reads within one invocation (§5.3).
 
-### 5.3 Planned: ABI 3.0 (#123)
+### 5.3 Planned: ABI 3.0 (#69)
 
-Decided in #123 and not yet implemented. Every body that runs will write every
-output, so no function needs its destination's old value as an implicit
-input. ABI 3.0 removes the hidden seed and the write markers from every
+Every body that runs writes every output (#123), so no function needs its
+destination's old value as an implicit input. ABI 3.0, tracked in #69 and not
+yet implemented, removes the hidden seed and the write markers from every
 function without a `Range` or `ArrayRange` parameter: a direct return takes
 only its source parameters, and the indirect carrier holds only output
 pointers. `Square` becomes `int64_t Pt_Square_I64(int64_t x)`.
@@ -497,9 +499,9 @@ function such as `Acc` must still report that no iteration ran, since zero
 iterations mean no assignment; it keeps its seed until PIR Step 7 chooses
 between one "did execute" bit and a caller-side emptiness check.
 
-Inputs become stable within each scalar invocation, so within one invocation
-a private variant (§5.2) may only let a shared input and output use one slot
-where no read can tell. Across iterations, a variant must produce what
+Once inputs are stable within each scalar invocation (#144), a private
+variant (§5.2) may only let a shared input and output use one slot within one
+invocation where no read can tell. Across iterations, a variant must produce what
 repeated scalar invocations of the bare specialization produce, with each
 iteration's shared argument rebound to the destination's current value. With
 `out = a + i`, `sum = Acc(sum, 1:5)` from 0 gives 10, while an unshared
diff --git a/docs/Pluto Conditional Value Semantics.md b/docs/Pluto Conditional Value Semantics.md
index a4c58760..e2e0800a 100644
--- a/docs/Pluto Conditional Value Semantics.md	
+++ b/docs/Pluto Conditional Value Semantics.md	
@@ -126,9 +126,8 @@ An unresolved failure that reaches an **invocation boundary** merges lanes
 there: a failed call argument suppresses that call's complete output tuple,
 and a failed print argument suppresses the complete print invocation and its
 newline (see "Print invocation atomicity" under Status). A call that did run
-writes every output (#123, decided and not yet implemented), so a failure
-inside a callee never reaches its caller. Until then, each output of a call
-that ran resolves independently per flattened output slot.
+writes every output (#123), so a failure inside a callee never reaches its
+caller.
 
 ```pluto
 y > 2          # yields y when y > 2, else fails    (the value is the left operand)
@@ -217,6 +216,19 @@ keep-old rule, reached by propagation or by the gate. The removed bracket form
 `y = (a > 2 10)` was the odd one out (it always assigned, zero on failure);
 spell that `y = a > 2 && 10 || 0`.
 
+They also agree on ranges: a bare range in either value iterates (#146). They
+differ in how often the condition runs. A statement gate's condition runs once
+for each point of the statement's outer iteration domain, before the values,
+whose RHS-local ranges run inside each admitted point; an `&&` condition is
+part of its value, so it runs once for each element the value iterates. With
+`Check` printing its argument and returning 1:
+
+```pluto
+i = 0:3
+a = Check("gate") > 0 i       # prints gate once; a is 2
+b = Check("and") > 0 && i     # prints and three times; b is 2
+```
+
 ## Arrays
 
 A collector cell is a value position, so the same rule applies: a failed cell is
@@ -424,12 +436,10 @@ shape — unresolved meaning no closer resolver claimed it first: in
   failed one. Ordinary calls are currently lazy in exactly the way print
   is, and PIR Step 6 is the behavior change for both. The
   out-of-bounds case changes too: today it materializes a zero and prints. A
-  suppressed invocation still releases its owned temporaries. Today an
-  unwritten direct-return argument resolves to its seed, which is zero in a
-  print, and always yields, because the result carries no validity bit.
-  #123 (decided) removes the case instead of adding a bit: a body that runs
-  writes every output, so a print argument that is a call either yields or
-  failed before the call ran.
+  suppressed invocation still releases its owned temporaries. A
+  direct-return argument carries no validity bit, and #123 removed the need
+  for one instead of adding it: a body that runs writes every output, so a
+  print argument that is a call either yields or failed before the call ran.
 - **Checked-access fallback (decided, not yet implemented):** the nearest
   resolver wins, so `x = arr[oob] || -1` assigns `-1`, and in print position
   `arr[oob] || -1, val1` emits `-1 val1`. The fallback tests the
diff --git a/docs/Pluto Effects and Follow-up Plan.md b/docs/Pluto Effects and Follow-up Plan.md
index 0b3c91b5..8651ed25 100644
--- a/docs/Pluto Effects and Follow-up Plan.md	
+++ b/docs/Pluto Effects and Follow-up Plan.md	
@@ -23,8 +23,10 @@ Resolved by a language rule instead of an analysis
 ([PR #104](https://github.com/thiremani/pluto/pull/104), superseding the closed
 [PR #102](https://github.com/thiremani/pluto/pull/102)): a declared output is
 readable inside its template only after it is definitely assigned, so a body
-that writes `y = x > 0 x` and then `y = y + 1` is rejected at the read. The hidden seed and destination-seeded staging slots continue to
-preserve outputs that are not written. A caller can explicitly connect an
+that writes `y = x > 0 x` and then `y = y + 1` is rejected at the read. Since
+#123, every body that runs writes every output, so the hidden seed and
+destination-seeded staging slots preserve a destination only when a
+callee-owned range runs no iteration. A caller can explicitly connect an
 input to an output by reusing the same binding: later statements then observe
 writes through that output, in ordinary and ranged calls alike. Inputs are
 read-only bindings, not frozen values. No per-iteration input snapshot is
@@ -57,11 +59,13 @@ it, are not planned ([issue #105](https://github.com/thiremani/pluto/issues/105)
 a function that needs its destination's previous value takes it as an input,
 and the caller shares the destination with it.
 
-**Decided 2026-09-28 ([issue #123](https://github.com/thiremani/pluto/issues/123);
-not yet implemented).** Every body that runs writes every output, sharing is
-decided only at the call site, and inputs keep their values within an
-invocation, which reverses the live references described above. Flow checks
-run once per template, the same for every argument type. The Memory
+**Decided 2026-09-28 ([issue #123](https://github.com/thiremani/pluto/issues/123)).**
+Every body that runs writes every output, sharing is decided only at the call
+site, and inputs keep their values within an invocation, which reverses the
+live references described above. Definite outputs and the per-template flow
+checks are implemented; stable inputs
+([#144](https://github.com/thiremani/pluto/issues/144)) and ABI 3.0
+([#69](https://github.com/thiremani/pluto/issues/69)) are not. The Memory
 Model's "Parameters and Outputs" and "Call Site" state the rules and what
 master still does differently, and the C ABI Spec §5.3 describes ABI 3.0.
 
@@ -117,7 +121,7 @@ and [ABI stability plan](./Pluto%20ABI%20Optimization%20Plan.md).
 
 | Work | Completion criterion / existing reference |
 | --- | --- |
-| Seed/effect correctness | Section 1; resolved by the definite-assignment rule for output reads in [PR #104](https://github.com/thiremani/pluto/pull/104); flow-versus-slot call specialization is [#103](https://github.com/thiremani/pluto/issues/103). Definite outputs, stable inputs and ABI 3.0 are decided in [#123](https://github.com/thiremani/pluto/issues/123) and land before PIR Step 4's call slice |
+| Seed/effect correctness | Section 1; resolved by the definite-assignment rule for output reads in [PR #104](https://github.com/thiremani/pluto/pull/104); flow-versus-slot call specialization is [#103](https://github.com/thiremani/pluto/issues/103). Definite outputs and per-template flow checks are done ([#123](https://github.com/thiremani/pluto/issues/123)); stable inputs ([#144](https://github.com/thiremani/pluto/issues/144)) and ABI 3.0 ([#69](https://github.com/thiremani/pluto/issues/69)) land before PIR Step 4's call slice |
 | `%n` effect contract | Done: `%n` removed (section 2, #109) |
 | Output path protection | Done ([#80](https://github.com/thiremani/pluto/issues/80)): a script's executable replaces only a missing path or a native executable, never `pt.mod`, a source file, a directory or a symlink, and links through a fresh directory renamed into place |
 | Numeric edge behavior | Define and guard integer divide/remainder faults and invalid shift counts; audit range/count/allocation arithmetic |
diff --git a/docs/Pluto IR Plan.md b/docs/Pluto IR Plan.md
index c1cd2efa..a1a28ffd 100644
--- a/docs/Pluto IR Plan.md	
+++ b/docs/Pluto IR Plan.md	
@@ -39,10 +39,10 @@ Pluto source
 Responsibilities stay decoupled: the solver owns types, ranges, output shapes,
 and effects; the CFG owns cross-statement dataflow legality; PIR owns how an
 already-valid statement executes; LLVM owns SSA, storage, optimization, and
-ABI. The CFG never reads PIR. Today both consume the solver's effect summary
-independently (§15). Under #123 the CFG checks function templates with its
-own conservative classification of the source instead, and whether script
-checks follow is still open (§15, CFG consumption).
+ABI. The CFG never reads PIR. The CFG checks function templates with its own
+conservative classification of the source (#123), while the script root's
+checks still consume the solver's statement effects until they move to the
+same classification (§15, CFG consumption).
 
 PIR may refer to solved AST expressions, but LLVM lowering must not reclassify
 their range, conditional, OOB, collector, affine, or commit behavior.
@@ -50,8 +50,8 @@ their range, conditional, OOB, collector, affine, or commit behavior.
 **ABI note.** Per-slot effects are an internal analysis, never a public ABI
 classifier: a body-only edit must never change the C prototype of a
 type-mangled symbol. Today every exported direct `I64`/`F64` return keeps a
-hidden seed parameter. #123 (decided) requires every body that runs to write
-every output, so ABI 3.0 removes the seed and the write markers from every
+hidden seed parameter. #123 requires every body that runs to write every
+output, so ABI 3.0 (#69) removes the seed and the write markers from every
 function without a `Range` or `ArrayRange` parameter. That removal depends
 only on whether a parameter is a range, and the complete prototype only on the
 solved parameter and output types, so a prototype still never depends on the
@@ -293,7 +293,7 @@ If one owned source feeds multiple targets, at most one consumer takes it; the
 others require a derived copy.
 
 At a call boundary, `a = F(a)` passes `a`'s value as an input that stays
-stable for the whole invocation (#123, decided): the output starts unassigned
+stable for the whole invocation (#144, decided): the output starts unassigned
 in its own staging slot, and the lowering may place both in one slot only
 where no read can tell. The real `a` changes only at the outer assignment's
 commit, so sibling RHS expressions continue to read the pre-commit binding.
@@ -497,9 +497,8 @@ Checked accesses have one canonical representation — `eval` with an explicit
 `[on-oob=...]` scope — regardless of which legacy path produced them. A
 **caller-side** failure — a failed invocation or argument — is atomic: the
 call's whole output tuple keeps its old values. A call that actually ran
-writes every output (#123, decided; today it may omit outputs independently,
-§15), so per-slot divergence exists only where slots carry independent
-conditions.
+writes every output (#123), so per-slot divergence exists only where slots
+carry independent conditions.
 
 ## 10. Collectors
 
@@ -760,9 +759,10 @@ relevant PIR excerpt.
 
 ## 15. Solver Effects
 
-Effects are solver-side facts consumed independently by the CFG and by PIR
-(under #123 the CFG's function checks use their own classification instead;
-see CFG consumption, below).
+Effects are solver-side facts derived for the script root, whose CFG checks
+consume them; PIR consumes them as its steps migrate. Function templates use
+the CFG's own classification of their text instead (#123; see CFG
+consumption, below).
 They are **per LHS slot**, not per statement, because a mixed assignment can
 skip one target while another always writes: `a, b = arr[i], i + 1` is
 `[]WriteEffect{MayWrite, MustWrite}`. The target-effect vector stays aligned to
@@ -828,10 +828,9 @@ Calls are where the two effects interact. A failure evaluating the invocation
 or its arguments suppresses the **whole tuple** — the call-merge rule — so
 every slot of that call becomes `MayYield` together.
 
-**Definite outputs (#123, decided; not yet implemented).** Every body that
-runs writes every output. The template-level flow check (CFG consumption,
-below) decides this from the function's text, the same for every argument
-type. Callee-internal non-writing therefore disappears, and the
+**Definite outputs (#123).** Every body that runs writes every output. The
+template-level flow check (CFG consumption, below) decides this from the
+function's text, the same for every argument type. Callee-internal non-writing therefore disappears, and the
 transfer rule reduces to `rawYield[i] = invocationYield`. A caller-side
 failure, such as the failed argument in `Id(arr[oob])`, makes every slot skip:
 the commit is skipped and the target stays `MayWrite`. Otherwise every slot
@@ -841,66 +840,49 @@ zero iterations, which means no assignment. Until Step 7 chooses between one
 "did execute" bit and a caller-side emptiness check, that case keeps the seed
 resolution below.
 
-**Today.** Master still lets a body skip a write, so the callee's output slots
-keep independent `WriteEffect`s, and two failure sources must not be
-conflated: a **caller-side failure** is a tuple fact, and **callee-internal
-non-writing**, where the callee ran but did not write an output, is a
-per-output fact. The transfer rule is conceptually
-`rawYield[i] = invocationYield && didWrite[i]`, but a direct `I64`/`F64`
-result carries no validity bit: it is seeded from the destination
-(`compileCallInner`), so a callee that wrote nothing returns the seed. After a
-successful invocation, seed resolution applies as a **contextual resolver at
-the assignment boundary** for a direct `MayWrite` output resolved at an
-existing target: the seed *is* the keep-old outcome, so the consumer sees
-`MustYield`. A caller-side failure is **never** converted into a seeded
-`MustYield`. A nested or targetless call is seeded with zero, so it reads an
-unwritten output as zero.
+**Seeds until Step 7.** A direct `I64`/`F64` result carries no validity bit:
+it is seeded from the destination (`compileCallInner`), so a call-owned domain
+that runs no iteration returns the seed. After a successful invocation, seed
+resolution applies as a **contextual resolver at the assignment boundary**
+for such a call at an existing target: the seed *is* the keep-old outcome, so
+the consumer sees `MustYield`. A caller-side failure is **never** converted
+into a seeded `MustYield`. A nested or targetless call is seeded with zero.
 
 Boundary resolution implies an **implicit read of the destination seed**, and
 only where the dependency is real: after a successful invocation, at an
-*existing* target whose direct callee output is `MayWrite` (today) or whose
-call owns a possibly empty domain, resolved at `=`. A fresh destination, a
-discard, a nested or targetless call, or an all-`MustWrite` callee introduces
-no implicit seed read. A declared output is readable inside its template only
-after a statement that definitely assigns it (the structural CFG rejects a
-read before any assignment, including a formatting marker, and the typed pass
-rejects a read after only conditional or seed-preserving writes), so the body
-cannot read the hidden seed through an output name. Step 2A records boundary
+*existing* target whose call owns a possibly empty domain, resolved at `=`. A
+fresh destination, a discard, a nested or targetless call, or a call without
+a call-owned domain introduces no implicit seed read. A declared output is
+readable inside its template only after a statement that definitely assigns
+it (the template check rejects an earlier read, including a formatting
+marker), so the body cannot read the hidden seed through an output name. Step 2A records boundary
 resolution as a `ReadsSeed` fact on the call site — the CFG is untouched in
 2A — and Step 2B converts the fact into an ordinary CFG read event, so a
 `MustWrite` classification cannot let backward liveness kill the prior value.
 
 An earlier revision of this plan added a private `{value, didWrite}`
 direct-call variant in Step 4, so that print and other failure-propagating
-contexts could see a skipped direct return. #123 removes the skipped write
+contexts could see a skipped direct return. #123 removed the skipped write
 instead, so the variant is not built.
 
 ### Convergence and publication
 
-**Folding a body into an output summary.** A declared output's body summary is
-the sequential fold of the body's per-slot effects for that output, in
-statement order: the output starts `MayWrite` (nothing has written it), a
-`MustWrite` statement slot sets it to `MustWrite`, and a `MayWrite` statement
-slot leaves it unchanged — a later conditional write cannot un-guarantee an
-earlier unconditional one. A boundary `MustWrite` obtained by reading the
-destination seed (`ReadsSeed`) also leaves the summary unchanged: preserving
-an earlier value does not prove that the body wrote one. Under #123 this
-precise summary no longer decides whether a template is valid; it stays an
-execution fact for routing, ownership and optimization. The published
-`BodyOutputEffects` deliberately stop before a call-owned domain: a `Range` or
-`ArrayRange` parameter controls whether
-the scalar body executes, not what the body does when it executes. Each call
-combines that reusable body summary with its solved domain. A provably
-non-empty literal can therefore preserve `MustWrite`, while an empty or unknown
-domain weakens the call to `MayWrite`. A range created *inside* the body still
-weakens only the outputs its statements drive — a possibly empty local range
-makes those slots `MayWrite`, so `UpperTriRowTail` publishes `MayWrite` for
-`res` — while unrelated outputs keep their effects.
-
-**Finite specialization closure.** SCC settlement assumes discovery has already
-produced a finite graph. It cannot catch
+**No body summary.** Every body that runs writes every output (#123), so a
+call's slots yield exactly when the call is invoked: its arguments' yields,
+joined with `MayYield` when a range that may run no iteration drives it. A
+call-owned `Range` or `ArrayRange` domain controls whether the scalar body
+executes, not what the body does when it executes, so a provably non-empty
+literal keeps the call `MustYield` while an empty or unknown domain weakens it.
+Statement effects therefore need no per-specialization summary and no fixed
+point across recursive calls: the script root derives them in one pass. An
+earlier revision folded each body into a `BodyOutputEffects` summary settled
+callee-first over the call graph's strongly connected components; #123 made
+every summary `MustWrite`, and both are gone.
+
+**Finite specialization closure.** Settlement assumes discovery has already
+produced a finite set of specializations. It cannot catch
 `f(T) -> f(Array<T>) -> f(Array<Array<T>>) -> ...`: every specialization is a
-new node, so Tarjan never runs. Before Step 2B, discovery caps active
+new one, so discovery never closes. Before Step 2B, discovery caps active
 specialization frames in one **recursive inference region** while attempting to
 allocate a missing candidate. The region starts at the earliest active frame
 whose function template repeats in the candidate path; flat sibling calls and
@@ -921,117 +903,88 @@ transformation. The fuse guarantees controlled compiler failure for unbounded
 specialization discovery, not runtime termination; totality remains a separate
 future analysis.
 
-After discovery closes, effects and CFG share one
-`specializationCallGraph` for each stable newly walked batch. Its dense,
-batch-local primary-call edges drive effect SCC settlement; its separate
-source-ordered mangled direct-call keys include settled callees and distinct
-scalar companions actually ensured for lowering. CFG reuses node enumeration
-and persistent reachability, not Tarjan state, effect worklists, or lattice
-working vectors.
-
-**Fixed point.** Function-body output effects, and only those, need one: a
-recursive callee can refine its outputs after types settle, and
-`TypeScriptFunc` today converges on types alone. Condense the typed
-specialization call graph into its strongly connected components and process
-them **callee-first** in reverse topological order — this is what lets a
-component assume every callee outside it has already published. Within one
-component:
-
-1. Seed every member's outputs with a provisional `MustWrite` working vector. A
-   recursive call reads that provisional value — which is why `Uncomputed`
-   cannot be a lattice element, as there would be nothing to read.
-2. Iterate the component, recomputing outputs from rebuilt statement effects
-   and callees' current values. Callees outside the component contribute their
-   published summaries.
-3. Weaken monotonically, `MustWrite → MayWrite` only. The working vector
-   **persists across body walks** within the component; it is not cleared with
-   `FuncInfo.Vars`.
-4. Stop when nothing changes — at most one weakening per slot.
-5. Publish one coherent snapshot for the whole component at once.
-
-An `Invalid` output blocks publication for its entire component; provisional
-values are never read outside it.
-
 Only reusable function specializations publish, through `FuncInfo.Settled`,
-which requires type convergence, the effect fixed point, complete direct-call
-keys, and a non-nil cached specialization CFG result. Every batch CFG result is
-staged and installed before any member becomes settled; a diagnostic-bearing
-result is complete and settles just like an empty successful result. A script
-root owns its current compilation facts and is consumed immediately after
-solving, so it needs no settled-publication step. Reading an unpublished or
-`Invalid` effect, or a settled specialization with no CFG result, is an ICE,
-never a default.
+which requires type convergence and agreement with the template's text range
+summary (CFG consumption, below); a disagreement is an ICE. A script root owns
+its current compilation facts and is consumed immediately after solving, so it
+needs no settled-publication step.
 
 Snapshot analysis such as `FuncInfo.Vars` is cleared and rebuilt whenever a
 body is walked and becomes reusable only once settled. `ExprCache` is not a
 precedent for append-only analysis: stable AST entries are overwritten while
 generated rewrite nodes may add entries across walks. Issue #71's
 compile-order-dependent wrong output came from reusing some body facts while
-discarding others. Specialization CFG success or diagnostics are likewise
-cached on `FuncInfo` and replayed when a later script reuses a settled body.
-Under #123, flow checks run once per template (CFG consumption, below), so
-settlement no longer requires a CFG result and nothing is replayed.
+discarding others. Flow checks run once per template (CFG consumption, below),
+so nothing about a specialization's diagnostics is cached or replayed.
 
 ### CFG consumption
 
-**Decided (#123; not yet implemented): flow checks per template.** Output
-initialization, reads before definite assignment, dead stores and
-write-after-write move to one pass per template, which runs whether or not
-anything calls it. The pass classifies writes from the text alone and
-conservatively: a statement gate, a range that may be empty, or a value that
-can fail (a value-position comparison, `&&`, a checked access, a `||` whose
-last alternative can fail, a call with such an argument) makes a write
-possibly skipped, even where a specialization's types would make it always
-write, as an array mask does. This classification stays separate from the
-solver's effects, which remain precise per specialization for routing,
-ownership and optimization; a specialization may drop a default its precise
-effects prove dead without reporting it.
+**Flow checks per template (#123).** Output initialization, reads before
+definite assignment, dead stores and write-after-write run in one pass per
+template, which runs whether or not anything calls it. The pass classifies
+writes from the text alone and conservatively: a statement gate, a range that
+may be empty, or a value that can fail (a value-position comparison, `&&`, a
+checked access, a `||` whose last alternative can fail, a call with such an
+argument) makes a write possibly skipped, even where a specialization's types
+would make it always write, as an array mask does. Only a range literal
+written with constant, nonempty bounds always runs; a range bound to a name
+may be empty. A call counts as writing every output, since its callee passes
+the same check, so a caller of a rejected template is not reported again.
 
 The pass also reads from the text which values are ranges, and so which
 statements a range drives. A parameter never holds a range, since a range
-argument drives the whole body, and struct fields, constants and array
-elements cannot hold one (`[r]` collects `r`'s values). A value is therefore
-a range only when it is a range literal, a binding whose assigned value is a
-range (`x = r`, not `x = r * 2`), a `||` or value-position `&&` that yields
-a range (`MakeRange(n > 0) || MakeRange(3)` forwards whichever alternative
-succeeds, and `c > 0 && MakeRange(3)` its right operand), or a call output
-that its template assigns a range. Before checking any body, the pass
-computes that last fact for every template output, iterating to a fixed
-point across templates that call each other: an output assigned `t` after
-`t = MakeRange(n)` is a range as well. A range that arrives through a call
-counts as possibly empty.
-Every check then uses the same classification, and none waits for a type:
-after `r = MakeRange(n)`, `out = r * 2` does not kill an earlier
-`out = prev`, does not definitely assign `out`, and so cannot by itself make
-a later read of `out` valid. A settled specialization's range types must
-agree with this summary; a disagreement is an ICE rather than a diagnostic.
+argument drives the whole body; no call yields one, since a function cannot
+return a range (an output assigned one is rejected at the definition, #146);
+and struct fields, constants and array elements cannot hold one (`[r]`
+collects `r`'s values). A value holds a range only when it is a bare range
+literal or binding assigned without a gate (`x = r`, not `x = r * 2` or
+`x = n > 0 r`): a gate makes its values computations, so a range in them
+iterates (#146). A range literal or binding operand of `||` and `&&` is
+iterated too (`n > 0 && 0:5` gives an element). A template's own text
+therefore decides all of this, without looking at another template. Every
+check then uses the same classification, and none waits for a type: after
+`r = 0:n`, `out = r * 2` does not kill an earlier `out = prev`, does not
+definitely assign `out`, and so cannot by itself make a later read of `out`
+valid. Settlement panics when a specialization's Range-typed bindings
+disagree with this summary.
+
+The flow checks run after every template's structural checks: explicit
+use-before-definition, illegal input/global writes, unused inputs,
+syntactically unassigned outputs, formatting structure, and discard behavior.
+Those collect all reads before declaring a statement's destinations, so a
+fresh `x = x + 1` cannot define its own RHS. An unknown main format marker
+remains literal text; malformed specifiers and missing dynamic width/precision
+variables on a resolved marker remain structural errors. Alongside them, the
+pass reports text it cannot classify, each an error the solver reports in any
+specialization: a call that names no template, an operator whose sides do not
+line up (value counts the solver rejects), and an assignment whose values do
+not fill its targets. The flow checks run only once every template passes
+both kinds of check, so they misread neither such a template nor a call to a
+function rejected for holding a range in an output, which its callers read
+as returning values. A template nothing calls gets these errors too. A name
+reassigned between a range and a non-range value is left to the solver,
+like any other change of type. The pass reads each name by its latest
+assignment, so its flow checks follow the text as written and the solver
+reports the retype only once they pass: a body with `r = n`, a print of `r`,
+then `r = 0:n` and `res = r + 1` is reported only for leaving `res` possibly
+unassigned. A template nothing calls is not checked for it. An error in any
+template fails the code module before any script compiles.
 
 This partly reverses Step 2B, which moved dead-store and write-after-write
-checks to specializations, and the per-specialization diagnostic cache and
-replay go with it. Whether a script's dead-store and write-after-write checks
-join this pass or keep the effect-sensitive dataflow described below is still
-open. The rest of this section describes the current design.
-
-`.pt` functions run `AnalyzeFuncs` once before any specialization exists. That
-pass is structural only: explicit use-before-definition, illegal input/global
-writes, unused inputs, syntactically unassigned outputs, formatting structure,
-and discard behavior. It collects all reads before declaring a statement's
-destinations, so a fresh `x = x + 1` cannot define its own RHS. An unknown main
-format marker remains literal text; malformed specifiers and missing dynamic
-width/precision variables on a resolved marker remain structural errors.
-
-After a stable specialization batch reaches its effect SCC fixed point, each
-node runs effect-sensitive CFG dataflow exactly once and caches its diagnostics.
-For a let, event order is condition reads, RHS reads, `ReadsSeed` destination
-reads, then sparse `StatementEffect.Writes` mapped by `TargetIndex`; all reads
+checks to specializations; the per-specialization diagnostic cache and replay
+are gone. Scripts move to the same classification in a follow-up (decided
+2026-10-07). Until then, after a script solve succeeds, CFG treats the script
+as a zero-input, zero-output template for structural validation, then runs
+effect-sensitive dataflow over the typed body with a fresh scope. For a let,
+event order is condition reads, RHS reads, `ReadsSeed` destination reads,
+then sparse `StatementEffect.Writes` mapped by `TargetIndex`; all reads
 therefore observe the simultaneous assignment's pre-commit snapshot. Print
 arguments contribute ordinary reads even though prints have no statement
-effect entry. An unreachable template gets structural and parser checks only:
-effects cannot be derived without types. Consequently, a library-only package
-whose templates are never instantiated receives no dead-store or
-write-after-write diagnostics in that build.
+effect entry. Structural diagnostics do not gate that typed pass: its
+already-collected explicit reads are reused so one compile reports all
+independent CFG diagnostics without repeating formatting errors.
 
-The two diagnostics consume effects differently:
+Both passes consume write kinds the same way:
 
 - *Backward (dead store).* A write is dead when its destination is not live
   afterward, and that holds for `MayWrite` as well as `MustWrite`. What
@@ -1045,45 +998,23 @@ The two diagnostics consume effects differently:
   explicitly when its value is semantically required. Under #123's
   template-level check, an `out = prev` default before a comparison override
   is live for every argument type, so it needs no exemption.
-- *Shared inputs.* A body is analyzed once per type specialization at
-  settlement, with every input treated as its own value, and every script
-  that reaches the specialization replays its diagnostics. Sharing an input
-  with an output at a call only adds reads today, and none once #123 makes
-  inputs stable, so it can never make a body invalid, and a body must be
-  valid without it: `out = current + 1` written
-  twice is reported for `x = Twice(x)` as well as for `y = Twice(x)`, because
-  the body never reads `out`. A body that means to build on its own write
-  says so by naming the output, `out = out + 1`, which is readable once
-  definitely assigned. Diagnostics are deduplicated by location and message,
-  and unused-write errors are errors rather than warnings throughout.
-
-After a script solve succeeds, CFG first treats the script as a zero-input,
-zero-output template for structural validation, then runs effect-sensitive
-dataflow over the typed body with a fresh scope. Structural diagnostics do not
-gate that typed pass: its already-collected explicit reads are reused so one
-compile reports all independent CFG diagnostics without repeating formatting
-errors. The compiler then traverses
-the script's complete
-direct-callee keys and each cached `DirectCallees` slice depth-first with a
-visited set. Every specialization remains analyzed and cached independently;
-the script presents their diagnostics as a first-seen, source-stable set union
-keyed by source location and message, so two type variants of one template do
-not print the same defect twice. Warm scripts need no body rewalk, and
-unreachable cached diagnostics never leak. Persistent edges use
-`CallParamTypes` plus a distinct
-`ScalarCallParamTypes` key only when the final source-call `ExprInfo` records
-that the companion was actually ensured; shared-cache membership alone never
-creates reachability.
+- *Shared inputs.* A body is analyzed once per template, with every input
+  treated as its own value. Sharing an input with an output at a call only
+  adds reads today, and none once #144 makes inputs stable, so it can never
+  make a body invalid, and a body must be valid without it:
+  `out = current + 1` written twice is reported for `x = Twice(x)` as well as
+  for `y = Twice(x)`, because the body never reads `out`. A body that means to
+  build on its own write says so by naming the output, `out = out + 1`, which
+  is readable once definitely assigned. Unused-write errors are errors rather
+  than warnings throughout.
 
 Inside a function body, domain ownership decides which statements an empty
 domain can skip. A `Range` or `ArrayRange` **parameter** establishes a
-function-level domain driving the whole body, contributing one shared effect at
-the function boundary rather than making every statement that reads it
-independently conditional. A locally created range owns only the statements it
-drives — `res = a[i * n + j]` under a body-local `j = (i + 1):n` has an
+function-level domain driving the whole body: it decides whether the body runs
+at all, not what a body that runs writes, so the template check never treats
+a parameter as a range. A locally created range owns only the statements it
+drives — `t = a[i * n + j]` under a body-local `j = (i + 1):n` has an
 RHS-local domain, not a function-owned one.
-Structural template CFG deliberately makes neither distinction — typed
-per-specialization effects resolve it when the function becomes reachable.
 
 The CFG pass itself stays: dataflow legality is a different question from
 ownership checking. This fix does not depend on PIR and lands before it.
@@ -1111,9 +1042,9 @@ Pluto has no users yet, so migration optimizes for the clean end state:
    `compileCondExprStatement` handles ranged logical trees; `compileCondStatement`
    feeds the general assignment path. Axes: gate (none/scalar/ranged); RHS
    capabilities as **composable flags** (conditional, checked, ranged,
-   collector, call — one RHS can be several at once); callee output effect for
-   call rows (all-`MustWrite` versus any-`MayWrite`, which after #123 only a
-   possibly empty callee-owned domain produces); value kind
+   collector, call — one RHS can be several at once); for call rows, whether
+   a possibly empty callee-owned domain can leave the outputs unwritten (the
+   only way left after #123); value kind
    (scalar/heap/multi-output/self-referential/descriptor/struct/table); target
    kind (local/output/discard); statement form.
    Each range domain also carries a role: descriptor value, RHS-local, shared
@@ -1176,8 +1107,9 @@ Two PRs, implementing §15.
   `ReadsSeed` facts become ordinary pre-write CFG reads; templates keep only
   structural checks; each specialization caches immutable diagnostics and
   complete direct-call keys; scripts replay the reachable closure once; and
-  the duplicated syntactic effect classifiers are deleted. #123 moves these
-  diagnostics back to one conservative pass per template (§15).
+  the duplicated syntactic effect classifiers are deleted. #123 moved these
+  diagnostics back to one conservative pass per template, and removed the
+  per-specialization caches, the replay and the effect fixed point (§15).
 
 Step 2 fixes the conditional-write false positive without depending on PIR.
 The Step 2B regression and leak suites pass, so PIR implementation can resume.
@@ -1226,8 +1158,8 @@ both); suite output is unchanged.
   `person.name` and `%t0#1.name` goldens of §17 land here.
 - The ownership elaboration pass (§8), with generic cleanup lowering and
   the consuming-operand promotion; its copy-loud goldens are listed in §17.
-- **Calls split by argument yield.** #123 (decided) lands before this slice:
-  every body that runs writes every output, and ABI 3.0 removes the seed and
+- **Calls split by argument yield.** #123 landed before this slice: every
+  body that runs writes every output, and ABI 3.0 (#69) removes the seed and
   the write markers from functions without a range parameter, so every
   non-ranged callee is all-`MustWrite`. An argument whose conditional or
   checked failure remains unresolved still makes the invocation `MayYield`,
@@ -1238,7 +1170,7 @@ both); suite output is unchanged.
   separately. Argument yield is therefore a router axis, recorded in the
   capability matrix (rows 6, 6b, 6c). The earlier plan also split on callee
   output effect and built a `{value, didWrite}` variant for print; #123
-  removes both for every call without a callee-owned domain.
+  removed both for every call without a callee-owned domain.
 
 **First slice landed — heap values and ownership elaboration.** The router
 admits heap value kinds (both string flavours, arrays, tables) and struct
@@ -1460,8 +1392,9 @@ generic plan lowerer, the existing reusable primitives, and no duplicated
 statement classification or specialized conditional orchestration. Surviving
 reorganized rather than deleted: loop and guard emission, generic storage
 across branches and iterations, the expression compiler for `eval` regions, the
-CFG pass (one flow pass per template under #123, whose text-only write
-classification deliberately stays separate from the solver's effects, §15),
+CFG pass (one flow pass per template, scripts included once they move to it,
+whose text-only write classification deliberately stays separate from the
+solver's effects, §15),
 and the runtime.
 
 Per-step deletions are targets, not guarantees — each lands only when its step
@@ -1526,17 +1459,21 @@ immediate deletion at the last consumer.
 - #123: flow checks run once per template, including one nothing calls: a
   body that can leave an output unwritten is rejected at the definition;
   `out = x > 0` alone is rejected for every argument type; `out = prev` then
-  `out = x > 0` is accepted for scalar and array `x`, and the array
-  specialization drops the dead default without a diagnostic; after
-  `r = MakeRange(n)`, `out = prev` then `out = r * 2` is accepted and
-  `F(y, 0)` keeps `y`, while without the default both the body and a read
-  of `out` after `out = r * 2` are rejected; a range passed on through
-  another template's output, or forwarded by `||` or value-position `&&` as
-  in `r = MakeRange(n > 0) || MakeRange(3)`, counts the same; and
-  `y = Helper(x)` then
-  `out = y + 1`, where `Helper` returns a scalar, is a definite write
-- summaries are rebuilt per specialization walk and published only on
-  `Settled`; transitive effects reach a fixed point across recursive closures
+  `out = x > 0` is accepted for scalar and array `x`, with no diagnostic for
+  the array specialization's dead default; after `r = 0:n`, `out = prev`
+  then `out = r * 2` is accepted and `F(y, 0)` keeps `y`, while without the
+  default both the body and a read of `out` after `out = r * 2` are
+  rejected; `y = Helper(x)` then `out = y + 1`, where `Helper` returns a
+  scalar, is a definite write; each way a value holds or iterates a range (a
+  copy, a gate, a literal or binding under `&&`) agrees with the solved
+  types; an output assigned a range is rejected (#146), with no
+  flow error in any template, so none in a caller declared before or after
+  it or calling it through a function that forwards the call; a call that
+  names no template, an operator whose sides do not line up, or an
+  assignment whose values do not fill its targets is reported where the
+  solver reports it, with no flow error in any template; and a body that
+  reassigns a name between a range and a non-range value, and passes the
+  flow checks as written, gets only the solver's retype error
 
 ### Loop-carried tests
 
diff --git a/docs/Pluto Memory Model.md b/docs/Pluto Memory Model.md
index 0c4fcbfc..cc5bf002 100644
--- a/docs/Pluto Memory Model.md	
+++ b/docs/Pluto Memory Model.md	
@@ -10,9 +10,11 @@ This document describes Pluto's semantic model and compares it with other major
 3. **Range Selections are Streams:** `s = arr[i]` keeps the final selected
    value (an element or owned subarray); `s = [arr[i]]` materializes every
    selected value.
-4. **Ranges are Descriptor Values:** `j = i` copies a Range; consuming it in
-   `x = i + 1`, `arr[i]`, a call, or `[]` drives a loop. Print and main
-   interpolation markers format the descriptor itself.
+4. **Ranges are Descriptor Values:** `j = i` copies a Range when the
+   assignment has no gate; under a gate, or consumed in `x = i + 1`, `arr[i]`,
+   a call, or `[]`, it drives a loop. Print and main interpolation markers
+   format the descriptor itself unless another argument on the line loops
+   over the name. A function cannot return a Range (#146).
 5. **Empty-Domain Initialization:** An empty Range descriptor still assigns.
    An empty ranged computation leaves an existing destination unchanged and a
    fresh destination at its type's zero value.
@@ -22,8 +24,8 @@ This document describes Pluto's semantic model and compares it with other major
 7. **Read-Only Function Arguments:** Inputs are read-only and keep their
    values for the whole call, even when the caller also passes the argument
    as a destination. Every body that runs writes every output, and results
-   reach the caller's destinations when the assignment commits. Master does
-   not enforce these rules yet (#123); see "Status" under Call Site.
+   reach the caller's destinations when the assignment commits. Stable
+   inputs are not implemented yet (#144); see "Status" under Call Site.
 8. **Function Locking:** Input arguments hold read locks, outputs hold write locks (automatic concurrency safety).
 9. **Memory Management:** Automatic scope-based deallocation (no GC pauses).
 
@@ -275,8 +277,9 @@ res = sum(a, b)
   or a call with such an argument. A comparison counts even where an array
   argument would make it a mask that always writes. Complementary conditions
   such as `n <= 1` and `n > 1` are not recognized either; for floats they need
-  not cover every case, since both fail for a NaN. A range with literal
-  bounds that is not empty always runs.
+  not cover every case, since both fail for a NaN. Only a range literal
+  written with constant, nonempty bounds, such as `0:3`, always runs; a range
+  bound to a name may be empty.
 - **Reading outputs**: A body may read an output (as a value, a condition, a
   call argument, a print, a formatting marker, or an empty array's sample)
   only after it is definitely assigned, judged from the text as above. A read
@@ -315,22 +318,25 @@ out = Pos(prev, x)
 
 For a scalar `x`, the value-position comparison `x > 0` yields `x` or fails,
 so `out` keeps `prev`. For an array `x`, it yields a mask and always writes,
-so the default is never read: the compiler drops it in that specialization
-and reports nothing. A statement gate such as `Maybe`'s `out = x > 0 x`
-serves only a scalar `x`, since a statement condition must be a scalar.
+so the default is never read, and the check reports nothing for it; the
+array specialization still copies the default before the mask replaces it.
+A statement gate such as `Maybe`'s `out = x > 0 x` serves only a scalar `x`,
+since a statement condition must be a scalar.
 
 The text also decides which values are ranges. A parameter never holds one,
 since a range argument runs the function once per element: `Wrap(1:5)`,
-where `Wrap` returns its input, gives `4`. Whether a function returns a
-range follows from its text, as with `MakeRange` below, and a range that
-arrives through a call counts as possibly empty, so `F` needs its default:
+where `Wrap` returns its input, gives `4`. A function cannot return a range
+either: an output assigned one is rejected, and the function returns the
+bounds for its caller to build the range from (#146). A range bound to a
+name counts as possibly empty, so `F` below needs its default. A gate makes
+its values computations, so a bare range in them iterates: in
+`kept = n > 2 s`, `kept` gets an element of `s`. Under `||` and `&&`, a range
+literal or binding operand is iterated too, so `n > 0 && 0:5` gives an
+element.
 
 ```python
-r = MakeRange(n)
-    r = 0:n
-
 out = F(prev, n)
-    r = MakeRange(n)
+    r = 0:n
     out = prev
     out = r * 2
 ```
@@ -416,24 +422,14 @@ give the input and the output one slot where no read can tell the
 difference: in `a = Maybe(a, -1)`, the body reads `prev` only in its first
 write to `out`, so `out = prev` needs no copy.
 
-**Status (#123, decided 2026-09-28; not yet implemented).** Master still
-differs in three ways:
-
-- A body may leave an output unwritten. `x = F()` then keeps `x` through a
-  hidden seed parameter, and a fresh `x` gets 0, while a nested call such as
-  `c = F(c) + 0` reads the unwritten output as zero.
-- A shared input is a live reference: each read observes earlier writes to
-  the shared output. `value, seen = FoldAfter(value, 5)` gives `15 15`,
-  `p, q = Swap(p, q)` with the sequential body gives `2 2`,
-  `value, seen, old = FoldAfter(value, 5), value` gives `15 15 10`, and
-  `FoldAfter(value, 1:3)` gives `13 13`.
-- Flow checks run per specialization, so their result can depend on the
-  argument types: `out = prev` followed by `out = x > 0` is rejected as a
-  dead store for an array `x`. A function nothing calls gets only structural
-  checks.
-
-The #123 implementation removes these differences, migrates the fixtures
-(`tests/alias_input` among them), and updates the README.
+**Status.** Definite outputs and the per-template checks are implemented
+(#123). Stable inputs are decided and not yet implemented (#144): a shared
+input is still a live reference, so each read observes earlier writes to the
+shared output. `value, seen = FoldAfter(value, 5)` gives `15 15`,
+`p, q = Swap(p, q)` with the sequential body gives `2 2`,
+`value, seen, old = FoldAfter(value, 5), value` gives `15 15 10`, and
+`FoldAfter(value, 1:3)` gives `13 13`. #144 removes this difference, migrates
+`tests/alias_input`, and updates the README's sharing example.
 
 ### Range Parameters
 
diff --git a/docs/Pluto PIR Capability Matrix.md b/docs/Pluto PIR Capability Matrix.md
index 8103f2bf..15e2cf70 100644
--- a/docs/Pluto PIR Capability Matrix.md	
+++ b/docs/Pluto PIR Capability Matrix.md	
@@ -35,8 +35,7 @@ combination migratable. A fallback that resolves every failure leaves the
 argument `MustYield` and outside this rule, though the router may still defer
 it until its node is supported.
 
-**After #123 (decided; lands before Step 4's call slice).** A body that runs
-writes every output, so every non-ranged callee is all-`MustWrite`, and
+**After #123.** A body that runs writes every output, so every non-ranged callee is all-`MustWrite`, and
 any-`MayWrite` remains only where a possibly empty callee-owned domain can
 leave the outputs unwritten (Step 7). The split rows 5c, 6, 6b, 8b, 35d and
 36d then cut over in Step 4 whenever their arguments are `MustYield`, and
@@ -116,7 +115,7 @@ two together rather than treating any single row as a deletion trigger.
 | 7e | none | checked, conditional (fallback), ranged | scalar | local | RHS-local | — | **S (decided; semantics doc)** | 7 |
 | 7f | none | checked, conditional (fallback), collector | scalar | local | collector-local | — | **S (decided; semantics doc)** | 8 |
 | 8 | none | ordinary | Range descriptor | local | — (no domain) | — | R | 3 |
-| 8b | none | call | Range descriptor | local | — (no domain) | split: all-`MustWrite` outputs and `MustYield` arguments → 4, otherwise → 6 | R | 4, 6 |
+| 8b | none | call | Range descriptor | local | — | rejected at the definition: a function cannot return a range (#146) | — | — |
 | 9 | none | ranged | scalar, self-ref | local | RHS-local | — | R | 7 |
 | 10 | none | ranged, checked | scalar | local | RHS-local | — | S | 7, fast path 10 |
 | 11 | none | collector, ranged | scalar, heap | local | collector-local | — | S | 8 |
@@ -163,7 +162,7 @@ two together rather than treating any single row as a deletion trigger.
 - **4** — `commitAssignments` copy/move marking; **now planned**: `pir.Elaborate` promotes a borrow to transfer when its owner is replaced in the group and copies every later borrow of that owner. *Tests:* `mem/mem.spt:64,78`; goldens `TestPlanGoldenHeapSwap`, `TestPlanGoldenDuplicateSource`, `TestPlanGoldenReplaceAndDiscard`. *Helpers:* `markCopyRequirements`, `freeExprOldValues`, `deepCopyIfNeeded`
 - **5** — per-slot sink: never bound, never typed (`isDiscard`), CFG-exempt. *Tests:* `discard`; the bare Range-descriptor discard is pinned by `TestPlanGoldenRangeDiscard` in `compiler/pir_test.go`
 - **5b** — per-slot sink; a discarded temporary is dropped (`drop`), a discarded named value stays borrowed; **now planned** for ordinary heap expressions: the derived `drop %tN` appears in expanded PIR. *Tests:* `discard`; golden `TestPlanGoldenReplaceAndDiscard`
-- **5c** — discarded call outputs keep their yield/write validity for cleanup, and the whole-call rule holds even when every output is discarded. The Step 1 inventory sent any-`MayWrite` calls to Step 6; after #123 no non-ranged callee may skip a write, so the only deferral left here is a call whose argument can fail, in Step 6. A possibly empty callee-owned domain is a ranged call, handled in Step 7 (row 5f). *Tests:* `discard`: all-`MustWrite` multi-output, both scalar (`FOuter`) and heap (`twoStr`); any-`MayWrite` heap (`maybeStr`, writing and non-writing paths). *Missing:* all-`MustWrite` direct-scalar (single-output) call; a discarded call whose argument can fail, such as `_ = mkTag(arr[9])`
+- **5c** — discarded call outputs keep their yield/write validity for cleanup, and the whole-call rule holds even when every output is discarded. The Step 1 inventory sent any-`MayWrite` calls to Step 6; after #123 no non-ranged callee may skip a write, so the only deferral left here is a call whose argument can fail, in Step 6. A possibly empty callee-owned domain is a ranged call, handled in Step 7 (row 5f). *Tests:* `discard`: all-`MustWrite` multi-output, both scalar (`FOuter`) and heap (`twoStr`); a heap callee that starts from a default and overrides it under a gate (`maybeStr`, both paths). *Missing:* all-`MustWrite` direct-scalar (single-output) call; a discarded call whose argument can fail, such as `_ = mkTag(arr[9])`
 - **5d** — a blank needs no seed on the skip path, so `ensureSeededDest` leaves it unbound. *Tests:* `discard` (failed and admitted, scalar and heap element). *Helpers:* `commitAssignmentsPerExpr`
 - **5e** — `commitConditionalOutputs` frees the blank's temp instead of binding it, on both the admitted and skipped paths. *Tests:* `discard`: all-`MustWrite` heap multi-output call (`twoStr`), gate admitting and rejecting. *Missing:* scalar-valued and ordinary-RHS gated blanks; a gated call to a callee that starts from a default, the #123 form of a conditional callee. *Helpers:* `compileCondStatement`
 - **5f** — `bindRangedTempOutputs` skips blanks, so ranged staging leaves no transient binding; the discarded value is released per iteration. *Tests:* `discard`: `_ = mkTag(i)` (single output), `_, _ = twoStr(mkTag(i), "z")` (multi-output). *Missing:* both fixtures are heap-valued, so the all-`MustWrite` scalar ranged call is uncovered, as is a call over a possibly empty range with its outputs discarded. *Helpers:* `compileAssignments`
@@ -178,7 +177,7 @@ two together rather than treating any single row as a deletion trigger.
 - **7e** — ranged checked fallback: the fallback resolves per iteration inside the loop nest. *Missing:* regressions when implemented. *Helpers:* condLHS spine, ranged staging
 - **7f** — collector-cell fallback: in `[arr[oob] \|\| -1]` the `\|\|` resolves before the cell's zero-fill. *Missing:* regressions when implemented. *Helpers:* collector rewrite, condLHS spine
 - **8** — plain value copy; the solver clears `Ranges`/`HasRanges`, so this is not an active ranged RHS. *Tests:* `range_finalize:2-21` (literal, identifier copy, empty, reassign), `compiler/solver_test.go`. *Helpers:* `compileAssignments`
-- **8b** — call lowering + indirect-return ABI, not descriptor copying. *Tests:* `range_finalize:38` (`makeRange`), `mem/gate_heap`. *Missing:* a Range return that starts from a default and is overwritten conditionally, the form #123 requires of a conditional output
+- **8b** — no longer arises: a function cannot return a range (#146), so an output assigned one is rejected at its definition. A function returns the bounds instead (`range_finalize`'s `rangeBounds`, `mem/gate_heap`'s `mkBounds`), and the caller's range literal is row 8. *Tests:* `TestFunctionsCannotReturnRanges`
 - **9** — `compileAssignments` → expression loop nest (passes nil conditions). *Tests:* `math/range_expr`, `math/range.spt`, `range_shadow.spt`, `cond/domain_activation`. *Helpers:* `compileAssignments`, `withCollectorPreparedLoopNest`, `compileCondOperands`
 - **10** — as #9 + `withLoopNestVersioned` affine probe. *Tests:* `array/affine_bounds_stmt`, `math/affine_bounds_expr`. *Helpers:* affine decision helpers
 - **11** — `compileArrayExpression` → `compileArray` → `withCollectorDomain`. *Tests:* `range`, `array/array_capture`, `mem/gate_heap`. *Helpers:* collector rewrite
@@ -187,11 +186,11 @@ two together rather than treating any single row as a deletion trigger.
 - **13** — callee body iterates: `compileCallInner` for direct returns, destination-seeded staged outputs for indirect and multi-output. *Tests:* `math/acc.spt`, `math/acc_desc`, `array/array_range.spt:89-96` (heap via indirect ABI)
 - **14** — ordinary function-body statement; a direct `I64`/`F64` output is an SSA value with **no** runtime write flag. *Tests:* `math/acc.pt`
 - **14i** — ordinary function-body statement; an indirect output has a runtime write flag set on commit. *Tests:* `mem/mem_alias_refine.pt`, `mem/mem.pt`
-- **14a** — gated function-body statement: the output is conditionally written, which is what makes the callee `MayWrite` at its boundary (`IsEven`/`IsOdd` conditionally write their indirect output pair). Under #123 such a body writes a default first, so the gate no longer weakens the boundary. *Tests:* `math/math.pt`, `math/rec.pt`, `mem/mem_cmp_lhs.pt`. *Helpers:* `compileCondStatement`
+- **14a** — gated function-body statement after a default: under #123 a body writes its output first and overrides it under the gate (`IsEven`/`IsOdd` start from their base values), so the gate no longer weakens the boundary. *Tests:* `math/math.pt`, `math/rec.pt`, `mem/mem_cmp_lhs.pt`. *Helpers:* `compileCondStatement`
 - **14c** — a body-local collector domain, i.e. a collector driven by a range created inside the body rather than by a parameter. *Missing:* **uncovered**: `cache_reuse.pt` uses fixed literals, `array_scalar_assign.pt` is parameter-driven (row 14b). *Helpers:* collector rewrite
 - **14b** — body driven by a `Range`/`ArrayRange` **parameter**, whose domain wraps the whole body and may execute zero times — this is what weakens the output to `MayWrite` at the boundary. *Tests:* `array/array_range.pt`
 - **14e** — as 14b with an inner collector: `ArraySetAdd(1:4)` runs a function-owned outer domain around a collector-local `[0:i]`, so full cutover needs collectors. *Tests:* `array/array_scalar_assign.pt` (`ArraySetAdd`), `array/array_func.pt`. *Helpers:* collector rewrite
-- **14d** — a range created **inside** the body drives one statement; the output is still `MayWrite` at the boundary because that local range can be empty — only the blanket function-owned weakening is absent. Under #123 the output needs a default before that statement. *Tests:* `math/dependent_range.pt` (`j = (i + 1):n`)
+- **14d** — a range created **inside** the body drives one statement, which may then run no iteration. Under #123 the output needs a default before that statement, or the statement writes a local first: `UpperTriRowTail` assigns `t = a[i * n + j]` under `j = (i + 1):n`, then `res = t`, and `DoubleLast` starts from `prev` before a range from a call. *Tests:* `math/dependent_range.pt`
 - **15** — `compileCondStatement`. *Tests:* `assign`, `initialize`, `zero_val`, `partial_returns`. *Helpers:* `compileCondStatement`
 - **16** — `compileCondStatement` + `prePromoteConditionalCallArgs`. *Tests:* `cond_copy`, `mem/mem_str.spt`, `math/math.pt`. *Helpers:* staging family
 - **17** — `compileCondStatement` + `aliasCondDests`. *Tests:* `tests/cond/expr_forms`. *Helpers:* `aliasCondDests`
@@ -241,7 +240,7 @@ two together rather than treating any single row as a deletion trigger.
 
 - **7d** — print-position fallback: `arr[oob] \|\| -1, val1` emits `-1 val1` — the fallback resolves before the invocation boundary, letting the whole line print. *Missing:* regressions when implemented, incl. a heap-valued print fallback. *Helpers:* condLHS spine
 - **29** — `compilePrintStatement` direct arm. *Tests:* `helloworld`, `str`, `1.2-report`. *Helpers:* `printAllExpressions`, `compilePrintStatement`
-- **29b** — non-ranged direct call argument in print. Today an unwritten result prints its seed; after #123 a call that runs writes every output, so no `{value, didWrite}` variant is needed. *Tests:* `math/print_func.spt:4` (`Square(3)`). *Missing:* a call argument whose own argument fails
+- **29b** — non-ranged direct call argument in print. A call that runs writes every output (#123), so no `{value, didWrite}` variant is needed. *Tests:* `math/print_func.spt:4` (`Square(3)`). *Missing:* a call argument whose own argument fails
 - **29c** — non-ranged indirect call argument in print. *Missing:* **uncovered**: multi-output and heap call results printed directly
 - **30** — `compileCondOperands` ANDs every argument's conditions and gates the one `printAllExpressions` call. *Tests:* `mem/mem_cmp_lhs.spt`, `array/oob_print`. *Missing:* side-effecting or owned-heap sibling of a failed conditional (add with Step 6). *Helpers:* `compileCondOperands`
 - **31** — no active bounds guard: prints the materialized zero today; Step 6 makes an unresolved OOB suppress the complete invocation and newline. *Tests:* `array/oob_print`. *Missing:* a suppressed invocation whose arguments own heap temporaries (add with Step 6). *Helpers:* §5
@@ -284,7 +283,7 @@ clock.
 | 27 | Ranged gate whose value is a heap-returning call — the per-iteration free-before-overwrite path had no test | `tests/mem/gate_heap/` (leak-checked) |
 | 11, 23, 24 | Empty and fully-rejected domains: what a collector and a carry commit | `tests/cond/domain_activation.spt` |
 | 5 | Blank targets: **zero** coverage in the entire corpus before this step | `tests/discard.spt` |
-| 11, 23 | A function-returned `Range` driving a collector domain and a shared statement gate | `tests/mem/gate_heap/` |
+| 11, 23 | A range built from a function's returned bounds, driving a collector domain and a shared statement gate | `tests/mem/gate_heap/` |
 | 30, 31 | Out-of-bounds and failed-conditional print arguments | `tests/array/oob_print.spt` |
 
 Confirmed by these fixtures and now normative in the plan (plan §7, plan §10):
@@ -375,10 +374,10 @@ to a **gated print** (`arr[oob] val1, val2`) — scheduled syntax that
 does not parse today (`PrintStatement` has no gate field) and lands in its
 own required PR before Step 6, with semantics-doc entry and capability rows.
 
-An unwritten direct-return argument cannot suppress the invocation today,
-since a direct `I64`/`F64` result carries no validity bit, so it prints its
-seed. #123 (decided) removes the case instead of adding a
-`{value, didWrite}` variant: a call that runs writes every output (plan §15).
+A direct `I64`/`F64` result carries no validity bit, and none is needed:
+#123 removed the unwritten direct return instead of adding a
+`{value, didWrite}` variant, since a call that runs writes every output
+(plan §15).
 
 ## 6. Correction to the plan's deletion order
 
diff --git a/docs/Pluto Range Semantics.md b/docs/Pluto Range Semantics.md
index d7e81992..c3fc6811 100644
--- a/docs/Pluto Range Semantics.md	
+++ b/docs/Pluto Range Semantics.md	
@@ -3,7 +3,7 @@
 ## Core Model
 
 A `Range<T>` is a descriptor value. A range literal constructs one, and a
-complete Range-valued assignment copies it:
+complete Range-valued assignment without a gate copies it:
 
 ```pluto
 i = 0:5
@@ -29,6 +29,9 @@ There are two explicit closing steps for a ranged computation:
 
 A Range descriptor assignment is not a closing step and does not iterate.
 This keeps descriptor copying, collection, and final-value selection separate.
+A bare range name behaves like the literal it holds: an assignment without a
+gate copies its descriptor, and under a gate, like any other use, it iterates
+(#146).
 
 ## Migration From Bare-Range Finalization
 
@@ -40,7 +43,8 @@ This change can be silent for a fresh destination. A later call, index, or
 collector consumes the copied Range and runs its whole domain, while print and
 interpolation format the descriptor itself. Assigning a Range
 to an existing scalar is instead rejected as a type-changing reassignment.
-Descriptor copies are unconditional writes and participate in the ordinary
+Descriptor copies happen only without a gate, so they are unconditional
+writes, even of an empty descriptor, and participate in the ordinary
 dead-store checks. Range-indexed expressions such as `last = data[i]` are
 unchanged because indexing is already a ranged computation.
 
@@ -60,14 +64,24 @@ Range `start`/`stop`/`step` fields are not part of the language.
 The bound values are captured when the range is constructed, so later changes
 to the source variables do not mutate the existing range. Functions that need
 those bounds as data should currently receive the scalar values explicitly.
+A range literal that drives a loop is constructed once, before its loop nest
+starts, so its bounds run once: even when an outer range is empty, and even
+when they read a value the loop writes. Every bound must yield: when one
+fails, through a condition or an out-of-bounds read, the range is empty and
+its loop runs no iterations. A failed bound never fails the value around the
+range, so `(0:(n > 0) + 0) || 99` is rejected, like `(0:n + 0) || 99`: its
+left side cannot fail.
 
 Range is nameable and copyable, but is not yet a fully first-class container
 element. Arrays and tables contain scalar/string elements rather than Range
 descriptors, so `[i]` consumes `i` and collects its yields. Passing a Range to a
 function likewise consumes it as a driver rather than passing inert metadata.
-A function may return a Range descriptor to a binding, but anonymous
-Range-returning expressions are not yet accepted uniformly by every consuming
-context; bind the result before consuming it.
+A function cannot return a Range either: an output assigned one is rejected
+at the function's definition (#146). The function returns the bounds instead,
+and the caller builds the range: `lo, hi = Bounds(n)`, then `r = lo:hi`. A
+gate makes a range iterate, so a range is chosen conditionally through its
+bounds: `lo, hi = n > 0 a, b`, then `r = lo:hi`. When the condition fails,
+`lo` and `hi` keep their previous values, and `r` is rebuilt from them.
 
 Range-indexed arrays follow the same rule:
 
@@ -145,15 +159,13 @@ as in `F(i, j)`, still form their normal cartesian domain. These choices do not
 change the results visible to source code.
 
 Function outputs are staged independently before the call. A body that runs
-writes every output (#123, decided and not yet implemented), so a destination
-keeps its value only when no invocation is admitted: the driver is empty, an
-argument fails at every point, or the statement's gate is false. Zero
-iterations always mean no assignment, wherever the loop is placed. Today a
-skipped condition inside the body can also leave an output unwritten, and its
-staged value is preserved. At
-representation boundaries, such as a static string result being assigned
-into an owned-string destination, the callee receives its declared zero value
-and the caller commits the adapted result only when the callee writes it.
+writes every output (#123), so a destination keeps its value only when no
+invocation is admitted: the driver is empty, an argument fails at every
+point, or the statement's gate is false. Zero iterations always mean no
+assignment, wherever the loop is placed. At representation boundaries, such as
+a static string result being assigned into an owned-string destination, the
+callee receives its declared zero value and the caller commits the adapted
+result once the callee writes it.
 
 Examples:
 
@@ -458,8 +470,8 @@ x, y = i < 2 [1], j + 0
 The statement condition `i < 2` is shared.
 `x` collects once for each admitted `i`, producing `[1 1]`.
 `y`'s operation uses its own local `j` driver inside that shared gate and ends
-with the final result `1`. A bare `j` in this position would instead copy the
-Range descriptor because only `i` belongs to the active statement domain.
+with the final result `1`. A bare `j` in this position iterates the same way
+and also ends with `1`.
 
 Likewise:
 
@@ -481,11 +493,11 @@ the statement condition opens that outer loop first.
 Inside the RHS, the same name refers to the current scalar iterator value, not
 to a fresh nested loop.
 
-Consequently, `filtered = i > 2 i` keeps the final admitted scalar, while
-`copy = outer > 2 i` copies `i` when only `outer` belongs to the statement
-domain. If the statement domain is empty, it performs no write: an existing
-Range destination stays unchanged and a fresh one keeps the zero Range
-descriptor.
+Consequently, `filtered = i > 2 i` keeps the final admitted scalar, and
+`cross = outer > 2 i` iterates `i` inside each admitted `outer` point and
+keeps the final yield. If the statement domain is empty, it performs no
+write: an existing destination stays unchanged and a fresh one keeps its zero
+value.
 
 For non-collector tuple outputs, one admitted statement iteration is still one
 shared scalar update step, but each RHS has its own local yield outcome. If one
diff --git a/docs/Pluto String and Formatting Semantics.md b/docs/Pluto String and Formatting Semantics.md
index 5c623686..a1568a5b 100644
--- a/docs/Pluto String and Formatting Semantics.md	
+++ b/docs/Pluto String and Formatting Semantics.md	
@@ -66,9 +66,10 @@ width = 5
 A main marker formats its value whatever the type, so a bare `Range` formats
 its descriptor and contributes no iteration: the string is a single value in
 assignment and in print alike. A Range identifier used for dynamic width or
-precision is consumed as a number, which makes it an iteration driver. An
-explicit numeric conversion such as `-i%d` is a compile error while `i` is an
-undriven Range descriptor — a descriptor is not a number.
+precision is consumed as a number, which makes it an iteration driver, and
+several such ranges nest in the order the string names them, the first
+outermost. An explicit numeric conversion such as `-i%d` is a compile error
+while `i` is an undriven Range descriptor — a descriptor is not a number.
 
 ```pluto
 i = 0:3
diff --git a/llvm_pipeline_test.go b/llvm_pipeline_test.go
index 654fe81a..168d1239 100644
--- a/llvm_pipeline_test.go
+++ b/llvm_pipeline_test.go
@@ -344,7 +344,7 @@ y = Fib(n)
     y = FibAux(n, 0, 1)
 
 y = FibAux(n, a, b)
-    y = n == 0 a
+    y = a
     y = n != 0 FibAux(n - 1, b, a + b)
 `,
 		"main.spt": `
diff --git a/tests/alias_input/self_alias.exp b/tests/alias_input/self_alias.exp
index b5105643..f2451b5a 100644
--- a/tests/alias_input/self_alias.exp
+++ b/tests/alias_input/self_alias.exp
@@ -24,7 +24,7 @@ NestedRange: 13 13
 NestedRangeTwice: 20 20
 NestedArrayTwice: [10 1 2 3 4] [10 1 2 3 4]
 ConditionalNested: 15 15
-ConditionalNestedSkipped: 10 0
+ConditionalNestedSkipped: 10 10
 StagedString: helloabc helloabc hello
 ResetArray: [
 ] [1 2] [
@@ -38,7 +38,6 @@ Powers: 9 27
 PowersShared: 9 81
 ReadTwice: second first second
 SharedPair: 105 10
-NextRange: 2:3
 CondCount: 11 11 lr
 re:storage: (0x[0-9a-f]+) (?!\1$)0x[0-9a-f]+
 re:storage: (0x[0-9a-f]+) \1
diff --git a/tests/alias_input/self_alias.pt b/tests/alias_input/self_alias.pt
index 839fff05..130489e5 100644
--- a/tests/alias_input/self_alias.pt
+++ b/tests/alias_input/self_alias.pt
@@ -54,6 +54,7 @@ out, seen = NestedArrayDeep(current, item)
     out, seen = ArrayAfter(current, item)
 
 out, seen = ConditionalFold(current, item)
+    out = current
     out = item > 0 current + item
     seen = current
 
@@ -74,6 +75,7 @@ out, seen = NestedArrayTwice(current)
 # A conditional call writes through synthetic destinations that stand in for
 # the outputs; sharing follows them to the real output.
 out, seen = ConditionalNested(current, item)
+    out, seen = current, current
     out, seen = item > 0 FoldAfter(current, item)
 
 out = BumpTwice(current, item)
@@ -116,16 +118,12 @@ out, before = SharedPair(a, b)
     before = b
     out = AddBoth(a, b, (1:3) + 0)
 
-# A shared range parameter is iterated by a scalar bound to the same name;
-# that scalar must not inherit the range's alias.
-out = NextRange(i)
-    out = i:(i+1)
-
 # A conditional call promotes its indirect arguments before branching. The
 # scalar after a two-valued argument binds a later parameter and must keep
 # its live alias.
 left, right = Tags(n)
     left = "l"
+    right = ""
     right = n > 0 "r"
 
 out, tag = Count(left, right, n)
@@ -133,6 +131,7 @@ out, tag = Count(left, right, n)
     tag = left ⊕ right
 
 out, seen, tag = CondCount(current)
+    out, tag = current, ""
     out, tag = 1 > 0 Count(Tags(current), current)
     seen = current
 
diff --git a/tests/alias_input/self_alias.spt b/tests/alias_input/self_alias.spt
index b6c64324..c07b44a9 100644
--- a/tests/alias_input/self_alias.spt
+++ b/tests/alias_input/self_alias.spt
@@ -147,10 +147,6 @@ pair = 10
 pair, before = SharedPair(pair, pair)
 "SharedPair:", pair, before
 
-nextRange = 1:3
-nextRange = NextRange(nextRange)
-"NextRange:", nextRange
-
 condCount = 10
 condCount, condCountSeen, condTag = CondCount(condCount)
 "CondCount:", condCount, condCountSeen, condTag
diff --git a/tests/alias_input/staging.pt b/tests/alias_input/staging.pt
index 61557fb3..e94e6027 100644
--- a/tests/alias_input/staging.pt
+++ b/tests/alias_input/staging.pt
@@ -1,18 +1,23 @@
 # A range-gated statement stages its output, and an input sharing that output
 # follows the staged value whether it is passed by value or by pointer.
 out = GateInt(current)
+    out = current
     out = (1:4) > 0 current + 1
 
 out = GateStr(current)
+    out = current
     out = (1:4) > 0 current ⊕ "."
 
 out = GateArr(current)
+    out = current
     out = (1:4) > 0 current ⊕ current
 
 out, seen = GateSibInt(current)
+    out, seen = current, current
     out, seen = (1:4) > 0 current + 1, current
 
 out, seen = GateSibStr(current)
+    out, seen = current, current
     out, seen = (1:4) > 0 current ⊕ ".", current
 
 out = Shrink(arr, v)
@@ -20,10 +25,12 @@ out = Shrink(arr, v)
 
 # The loop replaces the shared array with a shorter one.
 out, seen = ShrinkShared(current)
+    out = current
     out = Shrink(current, current[(0:8) + 0])
     seen = current
 
 # The conditional stages the output, then the ranged call inside it stages it
 # again; the nested call must keep sharing through both.
 out, after = GatedFold(current)
+    out, after = current, current
     out, after = 1 > 0 FoldAfter(current, (1:3) + 0)
diff --git a/tests/array/array_func.pt b/tests/array/array_func.pt
index 031ab565..93a663ce 100644
--- a/tests/array/array_func.pt
+++ b/tests/array/array_func.pt
@@ -29,16 +29,19 @@ res = ConcatArrays(a, b)
     res = a ⊕ b
 
 # An empty matrix can reset an established matrix destination.
-res = ResetArray(x)
+res = ResetArray(prev, x)
+    res = prev
     res = x > -1 [
     ]0
 
-# A ranged collector can leave an indirect output unwritten.
-res = KeepRangedArray(i)
+# A ranged collector can leave an indirect output at its starting value.
+res = KeepRangedArray(prev, i)
+    res = prev
     res = i < 0 [i]
 
 # A typed empty table can conditionally reset an established table.
-res = ResetTable(x)
+res = ResetTable(prev, x)
+    res = prev
     res = x > -1 [
       : Name("") Score(0)
     ]
diff --git a/tests/array/array_func.spt b/tests/array/array_func.spt
index 76f7953a..bdd0c038 100644
--- a/tests/array/array_func.spt
+++ b/tests/array/array_func.spt
@@ -60,9 +60,9 @@ conditionalTable = [
     "Grace" 30
 ]
 "ConditionalTableBefore: -conditionalTable"
-conditionalTable = ResetTable(-1)
+conditionalTable = ResetTable(conditionalTable, -1)
 "ConditionalTableSkipped: -conditionalTable"
-conditionalTable = ResetTable(1)
+conditionalTable = ResetTable(conditionalTable, 1)
 "ConditionalTableWritten: -conditionalTable"
 
 arr1 = []0 ⊕ [0]
@@ -96,7 +96,7 @@ resetMatrix = [
     3 4
 ]
 resetDriver = 0:2
-resetMatrix = ResetArray(resetDriver)
+resetMatrix = ResetArray(resetMatrix, resetDriver)
 "RangedRankReset: -resetMatrix"
 
 keptMatrix = [
@@ -104,7 +104,7 @@ keptMatrix = [
     7 8
 ]
 emptyResetDriver = 0:0
-keptMatrix = ResetArray(emptyResetDriver)
+keptMatrix = ResetArray(keptMatrix, emptyResetDriver)
 "RangedRankResetEmpty: -keptMatrix"
 
 # A statement condition stages a ranged call through a synthetic destination.
@@ -114,7 +114,7 @@ gatedWrittenMatrix = [
     43 44
 ]
 gatedResetDriver = 0:2
-gatedWrittenMatrix = 1 > 0 ResetArray(gatedResetDriver + 0)
+gatedWrittenMatrix = 1 > 0 ResetArray(gatedWrittenMatrix, gatedResetDriver + 0)
 "GatedRangedRankResetWritten: -gatedWrittenMatrix"
 
 # With an empty driver, the staged slot must retain its rank-2 value.
@@ -123,22 +123,23 @@ gatedKeptMatrix = [
     33 34
 ]
 gatedEmptyResetDriver = 0:0
-gatedKeptMatrix = 1 > 0 ResetArray(gatedEmptyResetDriver + 0)
+gatedKeptMatrix = 1 > 0 ResetArray(gatedKeptMatrix, gatedEmptyResetDriver + 0)
 "GatedRangedRankResetEmpty: -gatedKeptMatrix"
 
-# A blocked ranged collector inside a function leaves its caller's output intact.
+# A blocked ranged collector inside a function leaves the caller's value,
+# passed in as prev, intact.
 rangedArrayKept = [4 5]
-rangedArrayKept = KeepRangedArray(0:3)
+rangedArrayKept = KeepRangedArray(rangedArrayKept, 0:3)
 "RangedArrayKept: -rangedArrayKept"
 
 # An ordinary conditional empty return keeps an established matrix destination
-# when the callee leaves its output unwritten.
+# when the callee keeps the value it was passed.
 conditionalResetMatrix = [
     11 12
     13 14
 ]
 "ConditionalRankResetBefore: -conditionalResetMatrix"
-conditionalResetMatrix = ResetArray(-1)
+conditionalResetMatrix = ResetArray(conditionalResetMatrix, -1)
 "ConditionalRankResetSkipped: -conditionalResetMatrix"
 
 rangedConditionalResetMatrix = [
@@ -146,14 +147,14 @@ rangedConditionalResetMatrix = [
     23 24
 ]
 "RangedConditionalRankResetBefore: -rangedConditionalResetMatrix"
-rangedConditionalResetMatrix = ResetArray(-1:0)
+rangedConditionalResetMatrix = ResetArray(rangedConditionalResetMatrix, -1:0)
 "RangedConditionalRankResetSkipped: -rangedConditionalResetMatrix"
 
 zeroWidthMatrix = [[]0 []0]
 "ZeroWidthRankResetBefore: -zeroWidthMatrix"
-zeroWidthMatrix = ResetArray(-1)
+zeroWidthMatrix = ResetArray(zeroWidthMatrix, -1)
 "ZeroWidthRankResetSkipped: -zeroWidthMatrix"
-zeroWidthMatrix = ResetArray(1)
+zeroWidthMatrix = ResetArray(zeroWidthMatrix, 1)
 "ZeroWidthRankResetWritten: -zeroWidthMatrix"
 
 lockedArray = [9]
diff --git a/tests/array/array_range.pt b/tests/array/array_range.pt
index c3cb0cbf..57725935 100644
--- a/tests/array/array_range.pt
+++ b/tests/array/array_range.pt
@@ -3,7 +3,8 @@ res = Double(x)
 
 word = LocalWord(i)
     words = ["zero" "one" "two"]
-    word = words[i]
+    t = words[i]
+    word = t
 
 plane = LocalPlane(i)
     cube = [
@@ -11,4 +12,5 @@ plane = LocalPlane(i)
         [5 6] [7 8]
         [9 10] [11 12]
     ]
-    plane = cube[i]
+    t = cube[i]
+    plane = t
diff --git a/tests/array/cond_accum.exp b/tests/array/cond_accum.exp
index 3bce1d8f..4eaefa4c 100644
--- a/tests/array/cond_accum.exp
+++ b/tests/array/cond_accum.exp
@@ -37,11 +37,12 @@ MultiCell: [0 10 1 11]
 ScalarArith: 3
 4
 ScalarElem: 20
-CrossRange: [0 1 2 3 4]
-LitCross: [0 1 2 3 4]
 30
-SeedLit: [8 9]
-FreshLit: []
+SeedLit: 8
+FreshLit: 0
+GatedName: 4
+GatedLiteral: 3
+GatedEmpty: 7
 77
 StrSelection: c
 ["a" "b"]
diff --git a/tests/array/cond_accum.spt b/tests/array/cond_accum.spt
index adea5774..a929911c 100644
--- a/tests/array/cond_accum.spt
+++ b/tests/array/cond_accum.spt
@@ -205,36 +205,34 @@ q = 0:3
 elem = q < 2 arr4[q]
 "ScalarElem: -elem"
 
-# A statement driver gates a distinct bare Range descriptor without consuming it.
-r = 0:3
-i = 0:5
-cross = r < 4 i
-crossValues = [cross]
-"CrossRange: -crossValues"
-
-# A direct bare Range literal is likewise assigned as a descriptor.
-r = 0:3
-litcross = r < 2 0:5
-litcrossValues = [litcross]
-"LitCross: -litcrossValues"
-
 # Scalar conditional iteration: direct range-indexed array expression
 arr5 = [10 20 30 40]
 r = 0:3
 selectionCross = r < 2 arr5[0:3]
 selectionCross
 
-# A rejected descriptor assignment keeps the existing Range value.
-seedlit = 8:10
+# A rejected gated range literal keeps the existing value.
+seedlit = 8
 r = 0:3
 seedlit = r < 0 0:5
-seedlitValues = [seedlit]
-"SeedLit: -seedlitValues"
+"SeedLit: -seedlit"
 
-# A fresh rejected descriptor assignment keeps the zero Range descriptor.
+# A fresh rejected one keeps zero.
 freshlit = r < 0 0:5
-freshlitValues = [freshlit]
-"FreshLit: -freshlitValues"
+"FreshLit: -freshlit"
+
+# A gate with no range of its own makes a bare range iterate too: the
+# assignment keeps the final element, and an empty range keeps the old value.
+gateN = 3
+gateRange = 0:5
+gatedName = gateN > 2 gateRange
+"GatedName: -gatedName"
+gatedLiteral = gateN > 2 0:4
+"GatedLiteral: -gatedLiteral"
+gateEmpty = 0:0
+gatedEmpty = 7
+gatedEmpty = gateN > 2 gateEmpty
+"GatedEmpty: -gatedEmpty"
 
 # A rejected direct range-indexed array expression keeps the old value
 seedSelection = 77
diff --git a/tests/cond/empty_range.exp b/tests/cond/empty_range.exp
index 07b33c6f..a00b6fcb 100644
--- a/tests/cond/empty_range.exp
+++ b/tests/cond/empty_range.exp
@@ -8,3 +8,22 @@ CondLiteralRangeExisting: 7
 CondLiteralRangeNew: 0
 CondMixedExisting: 5 123
 CondMixedNew: 0 123
+BoundYields: 2 4 2 [0 1 2] 13
+BoundFails: 7 0 7 0 [] 10 0
+BoundPicks: 30 9 0 ""
+SelfBound: 2
+called 1
+called 2
+called 3
+called 2
+BoundCounts: 0 2 30 [0 1 1 2 2 3]
+called 6
+BoundEager: []
+called 4
+BoundMixed: 3
+called 5
+called 4
+BoundCallee: 20 10
+BoundReads: 99 99 10
+HeapBound: 2
+BoundStored: 2 1
diff --git a/tests/cond/empty_range.pt b/tests/cond/empty_range.pt
index e1172835..bc5c381f 100644
--- a/tests/cond/empty_range.pt
+++ b/tests/cond/empty_range.pt
@@ -6,3 +6,10 @@ out = HeapSuffix(s)
 
 out = RangeTail(x)
     out = x
+
+# The first range stays in use when the second one's bound fails.
+out = KeepRange(n)
+    r = 0:2
+    r = 0:(n > 0)
+    out = 0
+    out = r + 0
diff --git a/tests/cond/empty_range.spt b/tests/cond/empty_range.spt
index 46c1145a..a75969c2 100644
--- a/tests/cond/empty_range.spt
+++ b/tests/cond/empty_range.spt
@@ -38,3 +38,93 @@ a, b = 1 > 0 Accum(a, 0:-2), 123
 
 m, n = 1 > 0 Accum(1, 0:-2), 123
 "CondMixedNew: -m -n"
+
+# A range literal's bounds resolve before its loop, like any operands, so a
+# conditional bound works under a gate, in an operation, in a collector and in
+# a call.
+boundN = 3
+boundGated = boundN > 0 0:(boundN > 0 && boundN)
+boundOr = boundN > 0 0:(boundN < 0 || 5)
+boundSum = 0:(boundN > 0 && boundN) + 0
+boundCells = [0:(boundN > 0 && boundN)]
+boundCall = 10
+boundCall = Accum(boundCall, 0:(boundN > 0 && boundN))
+"BoundYields: -boundGated -boundOr -boundSum -boundCells -boundCall"
+
+# A bound that fails to yield leaves the loop with no iterations: existing
+# values stay, new ones keep their zero value, and a collector gets no cells.
+failGated = 7
+failGated = boundN > 0 0:(boundN < 0 && boundN)
+freshGated = boundN > 0 0:(boundN < 0 && boundN)
+failSum = 7
+failSum = 0:(boundN < 0 && boundN) + 0
+freshSum = 0:(boundN < 0 && boundN) + 0
+failCells = [0:(boundN < 0 && boundN)]
+failCall = 10
+failCall = Accum(failCall, 0:(boundN < 0 && boundN))
+freshCall = Accum(10, 0:(boundN < 0 && boundN))
+"BoundFails: -failGated -freshGated -failSum -freshSum -failCells -failCall -freshCall"
+
+# Indexing through such a range reads one element per index it yields.
+boundArr = [10 20 30 40]
+boundWords = ["ten" "twenty" "thirty" "forty"]
+boundPick = boundArr[0:(boundN > 0 && boundN)]
+failPick = 9
+failPick = boundArr[0:(boundN < 0 && boundN)]
+freshPick = boundArr[0:(boundN < 0 && boundN)]
+freshWord = boundWords[0:(boundN < 0 && boundN)]
+"BoundPicks: -boundPick -failPick -freshPick -freshWord%q"
+
+# The bounds run once, before the loop, so a bound that reads the destination
+# sees its value from before the statement.
+selfBound = 0
+selfBound = 1 > 0 0:(selfBound < 1 && 3)
+"SelfBound: -selfBound"
+
+# A bound runs once whatever its form, also when its range indexes an array or
+# nests inside another range's loop.
+countI = 0:3
+countCmp = 7
+countCmp = 1 > 0 0:(Loud(1) > 0)
+countAnd = 1 > 0 0:(Loud(2) > 0 && 3)
+countPick = boundArr[0:Loud(3)]
+countInner = [countI + 0:Loud(2)]
+"BoundCounts: -countCmp -countAnd -countPick -countInner"
+
+# Every range in a nest is built before the nest starts, so an inner bound runs
+# even when an outer range is empty.
+eagerI = 0:0
+eagerCells = [eagerI + 0:Loud(6)]
+"BoundEager: -eagerCells"
+
+# The value's own conditions run per element, without the bounds.
+countMixed = (boundN > 0 && 1) + 0:(Loud(4) > 0 && 3)
+"BoundMixed: -countMixed"
+
+# A call that runs the loop itself gets the range built the same way.
+calleeCmp = 10
+calleeCmp = Accum(calleeCmp, 0:(Loud(5) > 2))
+calleeFail = 10
+calleeFail = Accum(calleeFail, (Loud(4) > 5):3)
+"BoundCallee: -calleeCmp -calleeFail"
+
+# Every bound must yield before the loop starts, out-of-bounds reads included:
+# the loops run no iterations, so nothing is written or printed.
+oobBounds = [2]
+oobSum = 99
+oobSum = oobBounds[1]:(boundN > 0 && 3) + 0
+oobPick = 99
+oobPick = boundArr[oobBounds[1]:(boundN > 0 && 3)]
+oobCall = 10
+oobCall = Accum(oobCall, oobBounds[1]:3)
+"BoundReads: -oobSum -oobPick -oobCall"
+oobBounds[1]:3 + 0
+
+# A heap value compared in a bound is freed once the bound resolves.
+heapBound = 1 > 0 0:(HeapSuffix("a") > "a" && 3)
+"HeapBound: -heapBound"
+
+# A range assigned whole keeps its old range when a bound fails.
+storedYields = KeepRange(3)
+storedFails = KeepRange(0)
+"BoundStored: -storedYields -storedFails"
diff --git a/tests/cond/promoted_bindings.pt b/tests/cond/promoted_bindings.pt
index 8e96b764..e730d59e 100644
--- a/tests/cond/promoted_bindings.pt
+++ b/tests/cond/promoted_bindings.pt
@@ -4,7 +4,8 @@ y = Twice(v)
     y = v ⊕ v
 
 y = First(v)
-    y = v[0]
+    t = v[0]
+    y = t
 
 y = SI(t, j)
     y = t
diff --git a/tests/cond/value_cond_expr.pt b/tests/cond/value_cond_expr.pt
index 3fce3382..7dd1fcb7 100644
--- a/tests/cond/value_cond_expr.pt
+++ b/tests/cond/value_cond_expr.pt
@@ -39,4 +39,5 @@ a, b = MixK(x)
     b = x + 10
 
 s = Sum3(xs)
-    s = xs[0] + xs[1] + xs[2]
+    t = xs[0] + xs[1] + xs[2]
+    s = t
diff --git a/tests/discard.exp b/tests/discard.exp
index b80db782..40ec3447 100644
--- a/tests/discard.exp
+++ b/tests/discard.exp
@@ -9,4 +9,4 @@ GatedBlank: done
 RangedBlank: done
 RangedMultiBlank: done
 CheckedBlank: done
-MayWriteBlank: done
+DefaultBlank: done
diff --git a/tests/discard.pt b/tests/discard.pt
index 7452f07c..3857e5c2 100644
--- a/tests/discard.pt
+++ b/tests/discard.pt
@@ -5,4 +5,5 @@ tag = mkTag(v)
     tag = "tag-v"
 
 res = maybeStr(k)
+    res = ""
     res = k > 0 "big" ⊕ "value"
diff --git a/tests/discard.spt b/tests/discard.spt
index 8ed09c50..d739bb02 100644
--- a/tests/discard.spt
+++ b/tests/discard.spt
@@ -60,8 +60,8 @@ _ = arr[1]
 _ = sarr[1]
 "CheckedBlank: done"
 
-# A conditionally-writing callee with its output discarded, on both the
-# writing and non-writing paths.
+# A callee that overrides its default conditionally, with its output
+# discarded, on both paths.
 _ = maybeStr(1)
 _ = maybeStr(-1)
-"MayWriteBlank: done"
+"DefaultBlank: done"
diff --git a/tests/math/acc.exp b/tests/math/acc.exp
index ea9e9b29..840b7509 100644
--- a/tests/math/acc.exp
+++ b/tests/math/acc.exp
@@ -4,5 +4,7 @@
 10
 10
 13
+FilterShared: 2
+FilterUnshared: 0
 16 3
 ReversedHalf: 1.5 ReversedSum: 7
diff --git a/tests/math/acc.pt b/tests/math/acc.pt
index f55dfba5..b770da91 100644
--- a/tests/math/acc.pt
+++ b/tests/math/acc.pt
@@ -9,8 +9,15 @@ res = Acc(a, x)
     res = a + x
 
 res = ConditionalAcc(a, x)
+    res = a
     res = x > 0 a + x
 
+# A filter keeps its value through prev. Shared, each iteration starts from the
+# value the last one kept; unshared, each starts from the same prev.
+res = Filter(prev, x)
+    res = prev
+    res = x < 3 x
+
 sum, last = AccPair(a, x)
     sum = a + x
     last = x
diff --git a/tests/math/acc.spt b/tests/math/acc.spt
index deffa3ad..a18fe8bb 100644
--- a/tests/math/acc.spt
+++ b/tests/math/acc.spt
@@ -22,6 +22,13 @@ res = 10
 res = ConditionalAcc(res, -2:3)
 res
 
+kept = 0
+kept = Filter(kept, 1:5)
+"FilterShared: -kept"
+
+fresh = Filter(0, 1:5)
+"FilterUnshared: -fresh"
+
 sum = 10
 sum, last = AccPair(sum, 1:4)
 sum, last
diff --git a/tests/math/dependent_range.pt b/tests/math/dependent_range.pt
index 00fcd6cf..6c9ed3a0 100644
--- a/tests/math/dependent_range.pt
+++ b/tests/math/dependent_range.pt
@@ -1,3 +1,11 @@
 res = UpperTriRowTail(a, n, i)
     j = (i + 1):n
-    res = a[i * n + j]
+    t = a[i * n + j]
+    res = t
+
+# A named range may be empty, so the output starts from prev, and an empty
+# range keeps the caller's value.
+out = DoubleLast(prev, n)
+    r = 0:n
+    out = prev
+    out = r * 2
diff --git a/tests/math/dependent_range_fn.exp b/tests/math/dependent_range_fn.exp
index 04b230ab..b28c6029 100644
--- a/tests/math/dependent_range_fn.exp
+++ b/tests/math/dependent_range_fn.exp
@@ -1 +1,2 @@
 UpperTriRows: 4 8 12
+DoubleLast: 7 4
diff --git a/tests/math/dependent_range_fn.spt b/tests/math/dependent_range_fn.spt
index 3bf080cb..111217a1 100644
--- a/tests/math/dependent_range_fn.spt
+++ b/tests/math/dependent_range_fn.spt
@@ -6,3 +6,8 @@ r1 = UpperTriRowTail(a, n, 1)
 r2 = UpperTriRowTail(a, n, 2)
 
 "UpperTriRows: -r0 -r1 -r2"
+
+kept = 7
+kept = DoubleLast(kept, 0)
+doubled = DoubleLast(0, 3)
+"DoubleLast: -kept -doubled"
diff --git a/tests/math/func.exp b/tests/math/func.exp
index cf452f67..235532b5 100644
--- a/tests/math/func.exp
+++ b/tests/math/func.exp
@@ -39,3 +39,6 @@ SumSquaresRangeBothTrue: 18
 SumSquaresRangeAllFalse: 0
 SumSquaresRangeKeepPrev: 77
 SumSquaresRangeTailFalse: 8
+PosKeep: 9
+PosWrite: 5
+PosMask: [1 0 3]
diff --git a/tests/math/func.spt b/tests/math/func.spt
index 4752b9b4..d401fca1 100644
--- a/tests/math/func.spt
+++ b/tests/math/func.spt
@@ -9,19 +9,19 @@ arrVal = Square(arr)
 "SquareFloat: -floatVal"
 "SquareArr: -arrVal\n"
 
-# A skipped direct-scalar function output preserves an existing caller
-# destination, while a fresh destination keeps its zero seed.
+# A function keeps an old value through an input: the caller passes its
+# destination, and a fresh destination passes the zero it starts from.
 conditionalSquareKeep = 14
-conditionalSquareKeep = ConditionalSquare(conditionalSquareKeep - 12)
+conditionalSquareKeep = ConditionalSquare(conditionalSquareKeep, conditionalSquareKeep - 12)
 conditionalSquareWrite = 14
-conditionalSquareWrite = ConditionalSquare(conditionalSquareWrite - 7)
-conditionalSquareFresh = ConditionalSquare(2)
+conditionalSquareWrite = ConditionalSquare(conditionalSquareWrite, conditionalSquareWrite - 7)
+conditionalSquareFresh = ConditionalSquare(0, 2)
 conditionalSquareForwarded = 14
-conditionalSquareForwarded = ForwardConditionalSquare(conditionalSquareForwarded - 12)
+conditionalSquareForwarded = ForwardConditionalSquare(conditionalSquareForwarded, conditionalSquareForwarded - 12)
 conditionalSquareFloatKeep = 14.5
-conditionalSquareFloatKeep = ConditionalSquare(conditionalSquareFloatKeep - 12.5)
-conditionalSquareFloatWrite = ConditionalSquare(7.5)
-conditionalSquareFloatFresh = ConditionalSquare(2.0)
+conditionalSquareFloatKeep = ConditionalSquare(conditionalSquareFloatKeep, conditionalSquareFloatKeep - 12.5)
+conditionalSquareFloatWrite = ConditionalSquare(0.0, 7.5)
+conditionalSquareFloatFresh = ConditionalSquare(0.0, 2.0)
 
 "ConditionalSquareKeep: -conditionalSquareKeep"
 "ConditionalSquareWrite: -conditionalSquareWrite"
@@ -107,3 +107,12 @@ sumRangeTailFalse = SumSquares(m > 1, m < 3)
 "SumSquaresRangeAllFalse: -sumRangeAllFalse"
 "SumSquaresRangeKeepPrev: -sumRangeKeepPrev"
 "SumSquaresRangeTailFalse: -sumRangeTailFalse"
+
+# The comparison counts as possibly skipping for every argument type, so the
+# default before it stays, and a failed scalar comparison keeps it.
+posKeep = Pos(9, -1)
+posWrite = Pos(9, 5)
+posMask = Pos([]0, [1 -2 3])
+"PosKeep: -posKeep"
+"PosWrite: -posWrite"
+"PosMask: -posMask"
diff --git a/tests/math/math.pt b/tests/math/math.pt
index f9166b25..06fb8e57 100644
--- a/tests/math/math.pt
+++ b/tests/math/math.pt
@@ -7,11 +7,12 @@ greeting = "hello"
 res = Square(x)
     res = x * x
 
-res = ConditionalSquare(x)
+res = ConditionalSquare(prev, x)
+    res = prev
     res = x > 5 x * x
 
-res = ForwardConditionalSquare(x)
-    res = ConditionalSquare(x)
+res = ForwardConditionalSquare(prev, x)
+    res = ConditionalSquare(prev, x)
 
 z = SumSquares(a, b)
     z = Square(a) + Square(b)
@@ -29,3 +30,9 @@ x, y = F(i)
 
 a, b = G(i)
     a, b = 2.3 * i, 5.6 * i
+
+# One body serves scalar and array arguments: a scalar comparison can fail
+# and keep prev, while an array comparison is a mask that always writes.
+out = Pos(prev, x)
+    out = prev
+    out = x > 0
diff --git a/tests/math/rec.pt b/tests/math/rec.pt
index 50fe0c8d..3badbb93 100644
--- a/tests/math/rec.pt
+++ b/tests/math/rec.pt
@@ -1,28 +1,24 @@
 y = Fac(n)
+    y = 1
     y = n != 1 && n != 0 n * Fac(n-1)
-    y = n == 0 1
-    y = n == 1 1
 
 y = Fib(n)
     y = FibAux(n, 0, 1)
 
 y = FibAux(n, a, b)
-    y = n == 0 a
+    y = a
     y = n != 0 FibAux(n - 1, b, a + b)
 
 # define IsEven: returns (x, y) = (is-even?, is-odd?)
 x, y = IsEven(n)
+    # base case: 0 is even, not odd
+    x, y = "yes", "no"
     # recursive step: if n≠0, flip the pair returned by IsOdd(n-1)
     x, y = n != 0 IsOdd(n - 1)
-    # base case: 0 is even, not odd
-    x = n == 1 "no"
-    x = n == 0 "yes"
 
 # define IsOdd: returns (x, y) = (is-odd?, is-even?)
-# this function only infers type for y
 x, y = IsOdd(n)
-    # recursive step: if n≠0, flip the pair returned by IsEven(n-1)
-    x, y = n != 0 IsEven(n - 1)
     # base case: 0 is not odd, but even
-    y = n == 1 "no"
-    y = n == 0 "yes"
\ No newline at end of file
+    x, y = "no", "yes"
+    # recursive step: if n≠0, flip the pair returned by IsEven(n-1)
+    x, y = n != 0 IsEven(n - 1)
\ No newline at end of file
diff --git a/tests/math/rec_infer.pt b/tests/math/rec_infer.pt
index e3f0ad92..a9dd63dd 100644
--- a/tests/math/rec_infer.pt
+++ b/tests/math/rec_infer.pt
@@ -49,7 +49,8 @@ y, z = Mixed(n)
         1
         prior
     ]
-    z = tab.a[0] + tab.a[1]
+    t = tab.a[0] + tab.a[1]
+    z = t
 
 # An operator waits for a column the result still leaves pending.
 y = Bump(n, x)
diff --git a/tests/mem/gate_heap/gate_heap.pt b/tests/mem/gate_heap/gate_heap.pt
index a93b45b6..090851a8 100644
--- a/tests/mem/gate_heap/gate_heap.pt
+++ b/tests/mem/gate_heap/gate_heap.pt
@@ -1,5 +1,5 @@
 tag = mkTag(v)
     tag = "tag-v"
 
-r = mkRange(n)
-    r = 0:n
+start, stop = mkBounds(n)
+    start, stop = 0, n
diff --git a/tests/mem/gate_heap/gate_heap.spt b/tests/mem/gate_heap/gate_heap.spt
index 8b5b3809..14a08f4b 100644
--- a/tests/mem/gate_heap/gate_heap.spt
+++ b/tests/mem/gate_heap/gate_heap.spt
@@ -12,9 +12,10 @@ z = "keepme"
 z = q > 9 mkTag(q)
 "RangedGateHeapCallNoAdmit: -z"
 
-# A Range returned by a function is an ordinary descriptor: it drives a
-# collector domain and a statement gate like any locally created range.
-fr = mkRange(3)
+# A range built from a function's bounds drives a collector domain and a
+# statement gate like any other range.
+frStart, frStop = mkBounds(3)
+fr = frStart:frStop
 fc = [fr]
 "FnRangeCollector: -fc"
 
diff --git a/tests/mem/mem_alias_refine.pt b/tests/mem/mem_alias_refine.pt
index f13d3726..eb09f759 100644
--- a/tests/mem/mem_alias_refine.pt
+++ b/tests/mem/mem_alias_refine.pt
@@ -3,4 +3,5 @@
 # observes the replacement even though its expression produces a static string.
 out, echo = RefineEcho(s, x)
     out = "static"
+    echo = ""
     echo = x > -1 s ⊕ "!"
diff --git a/tests/mem/mem_cmp_lhs.pt b/tests/mem/mem_cmp_lhs.pt
index fd167560..2c9c8635 100644
--- a/tests/mem/mem_cmp_lhs.pt
+++ b/tests/mem/mem_cmp_lhs.pt
@@ -2,4 +2,5 @@
 # named binding permanently borrowed, or scope cleanup never frees its payload.
 out = pickByHeapCompare(k)
     label = "he" ⊕ "llo"
+    out = 0
     out = label > "abc" k
diff --git a/tests/mem/mem_str.exp b/tests/mem/mem_str.exp
index 4095782c..cb2e5150 100644
--- a/tests/mem/mem_str.exp
+++ b/tests/mem/mem_str.exp
@@ -25,10 +25,10 @@ reset
 heap from func
 static from func
 keep_heap
-CallStaticSeedKeep: keep_heap
-CallStaticSeedWrite: static changed
+CallStaticPrevKeep: keep_heap
+CallStaticPrevWrite: static changed
 CallStaticShareBefore: < shared_left > < shared_right >
-CallStaticShareSkipped: < shared_left > < shared_right >
+CallStaticShareSkipped: <  > <  >
 CallStaticShareWritten: < shared static > < shared static >
 slot
 plain
diff --git a/tests/mem/mem_str.pt b/tests/mem/mem_str.pt
index 934b7eb2..227aae5a 100644
--- a/tests/mem/mem_str.pt
+++ b/tests/mem/mem_str.pt
@@ -9,20 +9,23 @@ s = getStatic()
 
 # Return a static string while consuming a scalar/range argument.
 s = getStaticAt(x)
+    s = ""
     s = x > -1 "static ranged"
 
-# Conditionally replace a caller-supplied heap output with a static string.
-s = maybeStatic(flag)
+# Start from the caller's value and conditionally replace it with a static string.
+s = maybeStatic(prev, flag)
+    s = prev
     s = flag > 0 "static changed"
 
 # Write one conditionally chosen static value into two outputs.
 s, t = shareStaticOutput(flag)
     shared = flag > 0 "shared static"
-    s = flag > 0 shared
-    t = flag > 0 shared
+    s = shared
+    t = shared
 
 # Mixed indirect outputs exercise one widened string slot and one exact scalar slot.
 s, n = getStaticPair(x)
+    s = ""
     s = x > -1 "pair static"
     n = x
 
@@ -34,7 +37,8 @@ s = getHeap()
 # Tests that: 1) local array is cleaned up, 2) returned string is owned copy
 s = getArrayElem(idx)
     arr = ["zero" "one" "two"]
-    s = arr[idx]
+    t = arr[idx]
+    s = t
 
 # Use array element inside function without returning it
 # Tests that temporary from arr[i] is freed after use
diff --git a/tests/mem/mem_str.spt b/tests/mem/mem_str.spt
index 579bdcf4..b9ec3ec4 100644
--- a/tests/mem/mem_str.spt
+++ b/tests/mem/mem_str.spt
@@ -81,18 +81,18 @@ callReset
 callReset = getStatic()
 callReset
 
-# A StrG-returning conditional callee still sees the established StrH
-# destination seed when its write is skipped.
-staticCallSeed = "keep" ⊕ "_heap"
-staticCallSeed
-staticCallSeed = maybeStatic(0)
-"CallStaticSeedKeep: -staticCallSeed"
-staticCallSeed = maybeStatic(1)
-"CallStaticSeedWrite: -staticCallSeed"
-
-# Refinement adapters are ABI-zero-seeded inside the callee. An unwritten StrG
-# output preserves its established StrH destination, while an explicit sibling
-# copy of that ABI value commits the empty StrG value safely.
+# A callee that starts from the caller's heap value, passed in as prev, keeps
+# it when its static override is skipped.
+staticCallPrev = "keep" ⊕ "_heap"
+staticCallPrev
+staticCallPrev = maybeStatic(staticCallPrev, 0)
+"CallStaticPrevKeep: -staticCallPrev"
+staticCallPrev = maybeStatic(staticCallPrev, 1)
+"CallStaticPrevWrite: -staticCallPrev"
+
+# Static outputs reach owned destinations through refinement adapters. With the
+# flag off the gated local stays empty, and both outputs commit that empty
+# static value safely.
 sharedStaticLeft = "shared" ⊕ "_left"
 sharedStaticRight = "shared" ⊕ "_right"
 "CallStaticShareBefore: < -sharedStaticLeft > < -sharedStaticRight >"
diff --git a/tests/range.exp b/tests/range.exp
index d4e337d7..ccb48867 100644
--- a/tests/range.exp
+++ b/tests/range.exp
@@ -1,6 +1,7 @@
 [0 1 2 3 4] [1 2 3 4 5 6 7 8 9] [0 2] [-3 -2 -1 0 1 2 3 4] [0 1 2 3 4 5]
 [0 1 2 3 4 5] [1 2 3 4 5 6 7] [6] [0 3 6]
 Descriptors 0:2 2:4
+Names 0:2 2:4
 Cartesian 0 2
 Cartesian 0 3
 Cartesian 1 2
diff --git a/tests/range.spt b/tests/range.spt
index a1453771..63d6382d 100644
--- a/tests/range.spt
+++ b/tests/range.spt
@@ -17,9 +17,10 @@ u = 0:b:d
 
 [i], [j], [k], [u]
 
-# Bare descriptors print as values on one line; computations over distinct
-# drivers still form a cartesian iteration domain.
+# Bare range literals and range names print as written, on one line.
+# Computations over distinct names form a cartesian iteration domain.
 p = 0:2
 q = 2:4
-"Descriptors", p, q
+"Descriptors", 0:2, 2:4
+"Names", p, q
 "Cartesian", p + 0, q + 0
diff --git a/tests/range_finalize.exp b/tests/range_finalize.exp
index 49591e22..ac07bf36 100644
--- a/tests/range_finalize.exp
+++ b/tests/range_finalize.exp
@@ -5,7 +5,7 @@ EmptyRangeExisting: [0 1] -> []
 EmptyComputeFresh: 0
 EmptyComputeExisting: 91
 CallFinal: 20
-ReturnedRange: [2 3 4]
+BuiltRange: [2 3 4]
 MarkerFinal: Marker 0:3
 MarkerDescriptor 0:3
 MarkerWidthFinal: |  7|
diff --git a/tests/range_finalize.spt b/tests/range_finalize.spt
index aff7855d..e8eb669d 100644
--- a/tests/range_finalize.spt
+++ b/tests/range_finalize.spt
@@ -34,10 +34,11 @@ existing = emptyRange + 1
 callFinal = useShadow(ascending)
 "CallFinal: -callFinal"
 
-# A Range returned by a function is a descriptor once bound.
-returnedRange = makeRange()
-returnedValues = [returnedRange]
-"ReturnedRange: -returnedValues"
+# A function returns a range's bounds, and the caller builds the range.
+boundsStart, boundsStop = rangeBounds()
+builtRange = boundsStart:boundsStop
+builtValues = [builtRange]
+"BuiltRange: -builtValues"
 
 # A bare Range in a main marker formats the descriptor: the string is one
 # value with no drivers, in interpolation exactly as in assignment.
diff --git a/tests/range_shadow.pt b/tests/range_shadow.pt
index 6248129f..a26ec3f3 100644
--- a/tests/range_shadow.pt
+++ b/tests/range_shadow.pt
@@ -6,5 +6,5 @@ res = AddMul(x, y)
     i = 10
     res = i * x + y
 
-res = makeRange()
-    res = 2:5
+start, stop = rangeBounds()
+    start, stop = 2, 5