From 758616c97d393e74d61a3b556297334a3d1dd834 Mon Sep 17 00:00:00 2001
From: Tejas <tejasvph@gmail.com>
Date: Fri, 11 Sep 2026 19:05:29 +0530
Subject: [PATCH 1/3] fix(compiler): track callee seed reads beside write
 effects

A body whose last statement always writes can still depend on the
incoming output seed (`y = x > 0 x` then `y = y + 1`). The CFG treated
every all-MustWrite callee as reading no seed, so `a = 20` followed by
`a = MaybeIncrement(-1)` was rejected as an unused overwrite although
lowering already produced 21.

Publish a per-output SeedEffect (NoSeedRead/MaySeedRead) beside
BodyOutputEffects, derived by an order-sensitive fold: explicit reads,
resolved format markers, and calls to seed-reading callees count until
a raw MustWrite replaces the output, and the fact is sticky. Call sites
record CalleeReadsSeed for every named target whatever the ABI; the CFG
turns it into a pre-write read of a defined destination. ReadsSeed keeps
its boundary-resolution meaning, so the write fold still discounts
boundary-manufactured MustWrites and accumulators stay MustWrite. SCC
settlement requeues callers on seed growth as well as write weakening,
and an unpublished seed fact at a call site is an ICE.

Overwrite-before-read callees and fresh targets keep their existing
diagnostics. Lowering, public symbols, and prototypes are unchanged;
PIR is untouched.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
---
 compiler/cfg.go               |   9 +
 compiler/cfg_test.go          |  75 ++++++++
 compiler/effects.go           | 309 +++++++++++++++++++++++++++++----
 compiler/effects_test.go      | 314 +++++++++++++++++++++++++++++++++-
 compiler/solver.go            |   1 +
 compiler/solver_test.go       |   3 +
 compiler/types.go             |   8 +-
 docs/Pluto IR Plan.md         |  87 ++++++++--
 tests/seed/seed_read.exp      |  14 ++
 tests/seed/seed_read.pt       |  31 ++++
 tests/seed/seed_read.spt      |  36 ++++
 tests/seed/seed_read_warm.exp |   4 +
 tests/seed/seed_read_warm.spt |  14 ++
 13 files changed, 845 insertions(+), 60 deletions(-)
 create mode 100644 tests/seed/seed_read.exp
 create mode 100644 tests/seed/seed_read.pt
 create mode 100644 tests/seed/seed_read.spt
 create mode 100644 tests/seed/seed_read_warm.exp
 create mode 100644 tests/seed/seed_read_warm.spt

diff --git a/compiler/cfg.go b/compiler/cfg.go
index 8e8178d7..3191d7e8 100644
--- a/compiler/cfg.go
+++ b/compiler/cfg.go
@@ -376,6 +376,15 @@ func (cfg *CFG) typedStatementEvents(stmt ast.Statement, reads []VarEvent, effec
 		}
 		events = append(events, VarEvent{Name: target.Value, Kind: Read, Token: target.Tok()})
 	}
+	// A callee that reads its seed observes an existing destination. A fresh
+	// destination supplies a zero seed, so there is nothing to read.
+	for _, targetIndex := range effect.CalleeReadsSeed {
+		target := let.Name[targetIndex]
+		if !cfg.isDefined(target.Value) {
+			continue
+		}
+		events = append(events, VarEvent{Name: target.Value, Kind: Read, Token: target.Tok()})
+	}
 	for _, write := range effect.Writes {
 		target := let.Name[write.TargetIndex]
 		var kind EventType
diff --git a/compiler/cfg_test.go b/compiler/cfg_test.go
index bafab129..8850560b 100644
--- a/compiler/cfg_test.go
+++ b/compiler/cfg_test.go
@@ -142,6 +142,48 @@ func getValidTestCases() []cfgTestCase {
 			name:  "Failable Value Protects Only Its Own Destination",
 			input: "x = 7\na = 10\na, b = x < 5, 30\na, b",
 		},
+		{
+			// The callee always writes, but its value depends on the incoming
+			// seed, so the prior value is read rather than overwritten.
+			name: "Seed Dependent Call Reads Prior Value",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1`,
+			input: "x = 20\nx = maybeIncrement(-1)\nx",
+		},
+		{
+			// The dependency composes through a wrapper whose only statement
+			// forwards the output to a seed-reading callee.
+			name: "Nested Seed Dependent Call Reads Prior Value",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1
+
+res = outer(x)
+    res = maybeIncrement(x)`,
+			input: "x = 20\nx = outer(-1)\nx",
+		},
+		{
+			// Inside a body, the inner call reads the reset value, which keeps
+			// that unconditional write live.
+			name: "Reset Before Seed Dependent Call Inside Body",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1
+
+res = resetThenIncrement(x)
+    res = 0
+    res = maybeIncrement(x)`,
+			input: "x = resetThenIncrement(-1)\nx",
+		},
+		{
+			// An indirect output reads its destination-seeded staging slot.
+			name: "Indirect Seed Dependent Call Reads Prior Value",
+			code: `s = maybeTag(n, t)
+    s = n > 0 t
+    s = s ⊕ "!"`,
+			input: "w = \"hi\"\nw = maybeTag(-1, \"x\")\nw",
+		},
 	}
 }
 
@@ -210,6 +252,39 @@ func getErrorTestCases() []cfgTestCase {
 			input:         "x = 7\nx = alwaysWrite(0:2)\nx",
 			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
 		},
+		{
+			// A definite overwrite before the read removes the seed dependency,
+			// so the prior value really is unused.
+			name: "Overwrite Before Seed Read Still Overwrites Prior Value",
+			code: `res = overwrite(x)
+    res = x
+    res = res + 1`,
+			input:         "x = 7\nx = overwrite(3)\nx",
+			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
+		},
+		{
+			// The nested read observes the reset, never the caller's value.
+			name: "Reset Before Nested Seed Read Overwrites Prior Value",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1
+
+res = resetThenIncrement(x)
+    res = 0
+    res = maybeIncrement(x)`,
+			input:         "x = 7\nx = resetThenIncrement(-1)\nx",
+			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
+		},
+		{
+			// A fresh destination supplies a zero seed; the callee's read does
+			// not make the result used.
+			name: "Fresh Seed Dependent Result Is Unused",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1`,
+			input:         "x = maybeIncrement(-1)",
+			errorContains: `value assigned to "x" is never used`,
+		},
 		{
 			// A || yields whenever its final fallback does, so the resolver
 			// boundary holds and this write is unconditional.
diff --git a/compiler/effects.go b/compiler/effects.go
index fad03c9f..57d4ca8c 100644
--- a/compiler/effects.go
+++ b/compiler/effects.go
@@ -60,6 +60,35 @@ func (effect YieldEffect) String() string {
 	}
 }
 
+// SeedEffect describes whether a scalar body can observe one output's
+// incoming value before that output is definitely replaced. It is independent
+// of WriteEffect: an unconditional computed update reads its seed, while a
+// conditional write may leave preservation entirely to the caller. Uncomputed
+// and Invalid are publication states, not lattice members.
+type SeedEffect uint8
+
+const (
+	SeedUncomputed SeedEffect = iota
+	SeedInvalid
+	NoSeedRead
+	MaySeedRead
+)
+
+func (effect SeedEffect) String() string {
+	switch effect {
+	case SeedUncomputed:
+		return "Uncomputed"
+	case SeedInvalid:
+		return "Invalid"
+	case NoSeedRead:
+		return "NoSeedRead"
+	case MaySeedRead:
+		return "MaySeedRead"
+	default:
+		return fmt.Sprintf("SeedEffect(%d)", effect)
+	}
+}
+
 // TargetWriteEffect is one entry in a sparse, position-preserving target
 // vector. Discard targets have no entry; TargetIndex keeps later entries tied
 // to their original LHS slots.
@@ -69,11 +98,23 @@ 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 resolves a direct MayWrite
+// callee output at the assignment boundary; such a write preserves a value
+// rather than producing one. CalleeReadsSeed holds LHS indices whose incoming
+// value the callee body itself may read before definitely replacing it,
+// whatever the write effect. It is recorded for every named target because a
+// fresh destination supplies a zero seed: consumers decide whether an
+// existing value is involved.
 type StatementEffect struct {
-	Writes    []TargetWriteEffect
-	ReadsSeed []int
+	Writes          []TargetWriteEffect
+	ReadsSeed       []int
+	CalleeReadsSeed []int
+}
+
+// replacesTarget reports whether the statement definitely stores a value the
+// body produced: a MustWrite not manufactured by reading the destination seed.
+func (effect StatementEffect) replacesTarget(write TargetWriteEffect) bool {
+	return write.Effect == MustWrite && !slices.Contains(effect.ReadsSeed, write.TargetIndex)
 }
 
 func validPublishedEffects(effects []WriteEffect, count int) bool {
@@ -90,6 +131,20 @@ func validPublishedEffects(effects []WriteEffect, count int) bool {
 	return true
 }
 
+func validPublishedSeedEffects(effects []SeedEffect, count int) bool {
+	if len(effects) != count {
+		return false
+	}
+
+	for _, effect := range effects {
+		if effect != NoSeedRead && effect != MaySeedRead {
+			return false
+		}
+	}
+
+	return true
+}
+
 func joinYield(left, right YieldEffect) YieldEffect {
 	if left == YieldInvalid || right == YieldInvalid {
 		return YieldInvalid
@@ -117,14 +172,22 @@ func classifyWriteEffect(yield YieldEffect, maySkip bool) WriteEffect {
 	return MustWrite
 }
 
+// bodyEffects pairs the write and seed facts of one specialization's outputs:
+// the published summary of a settled callee, or the provisional working
+// values of a component still being settled.
+type bodyEffects struct {
+	writes []WriteEffect
+	seeds  []SeedEffect
+}
+
 type effectAnalyzer struct {
 	compiler        *Compiler
 	funcNameMangled string
 	graph           *specializationCallGraph
-	working         [][]WriteEffect
+	working         []bodyEffects
 }
 
-func newEffectAnalyzer(compiler *Compiler, mangled string, graph *specializationCallGraph, working [][]WriteEffect) *effectAnalyzer {
+func newEffectAnalyzer(compiler *Compiler, mangled string, graph *specializationCallGraph, working []bodyEffects) *effectAnalyzer {
 	return &effectAnalyzer{
 		compiler:        compiler,
 		funcNameMangled: mangled,
@@ -263,7 +326,7 @@ func (analyzer *effectAnalyzer) deriveCall(expr *ast.CallExpression) []YieldEffe
 		invocation = joinYield(invocation, MayYield)
 	}
 
-	callee := analyzer.callBodyOutputEffects(expr)
+	callee := analyzer.callBodyEffects(expr).writes
 	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)))
 	}
@@ -284,12 +347,12 @@ func (analyzer *effectAnalyzer) deriveCall(expr *ast.CallExpression) []YieldEffe
 	return info.YieldEffects
 }
 
-func (analyzer *effectAnalyzer) callBodyOutputEffects(expr *ast.CallExpression) []WriteEffect {
+func (analyzer *effectAnalyzer) callBodyEffects(expr *ast.CallExpression) bodyEffects {
 	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
+		return bodyEffects{writes: f.BodyOutputEffects, seeds: f.BodySeedEffects}
 	}
 
 	if analyzer.graph == nil {
@@ -373,7 +436,7 @@ func (analyzer *effectAnalyzer) seedResolvedYield(expr ast.Expression, slot int,
 		return YieldUncomputed, false
 	}
 
-	callee := analyzer.callBodyOutputEffects(call)
+	callee := analyzer.callBodyEffects(call).writes
 	needsSeed := callee[slot] == MayWrite || analyzer.callOwnsPossiblyEmptyDomain(call, conditionRanges)
 	if !needsSeed {
 		return YieldUncomputed, false
@@ -400,6 +463,23 @@ func (analyzer *effectAnalyzer) callOwnsPossiblyEmptyDomain(call *ast.CallExpres
 	return false
 }
 
+// calleeSeedEffects returns the callee's per-output seed facts for a resolved
+// call and nil for every other expression, which reads no destination. An
+// unpublished fact is an ICE: unknown analysis must not mean no seed reads.
+func (analyzer *effectAnalyzer) calleeSeedEffects(expr ast.Expression) []SeedEffect {
+	call, ok := expr.(*ast.CallExpression)
+	if !ok || !typesResolved(analyzer.exprInfo(call).OutTypes) {
+		return nil
+	}
+
+	seeds := analyzer.callBodyEffects(call).seeds
+	if !validPublishedSeedEffects(seeds, len(analyzer.exprInfo(call).OutTypes)) {
+		panic(fmt.Sprintf("internal: call %s has unpublished seed effects %v", call.Function.Value, seeds))
+	}
+
+	return seeds
+}
+
 func (analyzer *effectAnalyzer) deriveStatements(statements []ast.Statement, initiallyDefined map[string]struct{}) map[*ast.LetStatement]StatementEffect {
 	defined := make(map[string]struct{}, len(initiallyDefined))
 
@@ -441,6 +521,7 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 	for _, expr := range stmt.Value {
 		yields := analyzer.deriveExpr(expr)
 		maySkip := len(stmt.Condition) > 0 || analyzer.expressionUsesLocalDomain(expr)
+		calleeSeeds := analyzer.calleeSeedEffects(expr)
 
 		for slot, yield := range yields {
 			index := targetIndex
@@ -455,6 +536,9 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 				result.ReadsSeed = append(result.ReadsSeed, index)
 				yield = seededYield
 			}
+			if calleeSeeds != nil && calleeSeeds[slot] == MaySeedRead {
+				result.CalleeReadsSeed = append(result.CalleeReadsSeed, index)
+			}
 			result.Writes = append(result.Writes, TargetWriteEffect{
 				TargetIndex: index,
 				Effect:      classifyWriteEffect(yield, maySkip),
@@ -486,8 +570,13 @@ func validStatementEffect(stmt *ast.LetStatement, effect StatementEffect) bool {
 		return false
 	}
 
+	return validSeedTargets(stmt, effect.ReadsSeed) && validSeedTargets(stmt, effect.CalleeReadsSeed)
+}
+
+// validSeedTargets requires ascending, unique, named LHS indices.
+func validSeedTargets(stmt *ast.LetStatement, targets []int) bool {
 	lastTarget := -1
-	for _, targetIndex := range effect.ReadsSeed {
+	for _, targetIndex := range targets {
 		if targetIndex <= lastTarget || targetIndex >= len(stmt.Name) {
 			return false
 		}
@@ -501,19 +590,20 @@ 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
-	}
-
+func outputIndices(template *ast.FuncStatement) map[string]int {
 	outputIndex := make(map[string]int, len(template.Outputs))
 
 	for i, output := range template.Outputs {
 		outputIndex[output.Value] = i
 	}
 
+	return outputIndex
+}
+
+func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.LetStatement]StatementEffect) []WriteEffect {
+	effects := slices.Repeat([]WriteEffect{MayWrite}, len(template.Outputs))
+	outputIndex := outputIndices(template)
+
 	for _, statement := range template.Body.Statements {
 		stmt, ok := statement.(*ast.LetStatement)
 		if !ok {
@@ -526,7 +616,7 @@ func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.Le
 		}
 
 		for _, write := range statementEffect.Writes {
-			if write.Effect != MustWrite || slices.Contains(statementEffect.ReadsSeed, write.TargetIndex) {
+			if !statementEffect.replacesTarget(write) {
 				continue
 			}
 			index, isOutput := outputIndex[stmt.Name[write.TargetIndex].Value]
@@ -539,6 +629,142 @@ func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.Le
 	return effects
 }
 
+// seedFold walks one body in statement order and records which outputs are
+// read while they may still hold their incoming value. Reads precede writes
+// within a statement, and a recorded read is permanent: a seed copied to a
+// local before the output is replaced still reaches the body's results.
+type seedFold struct {
+	outputIndex map[string]int
+	replaced    []bool
+	effects     []SeedEffect
+	defined     map[string]struct{}
+	isGlobal    func(string) bool
+}
+
+func newSeedFold(template *ast.FuncStatement, isGlobal func(string) bool) *seedFold {
+	fold := &seedFold{
+		outputIndex: outputIndices(template),
+		replaced:    make([]bool, len(template.Outputs)),
+		effects:     slices.Repeat([]SeedEffect{NoSeedRead}, len(template.Outputs)),
+		defined:     functionInitialBindings(template),
+		isGlobal:    isGlobal,
+	}
+
+	// Outputs are bound to their seeds before the body runs, so a marker
+	// naming one resolves like the solver and lowering resolve it.
+	for _, output := range template.Outputs {
+		fold.defined[output.Value] = struct{}{}
+	}
+
+	return fold
+}
+
+func (fold *seedFold) isDefined(name string) bool {
+	if _, exists := fold.defined[name]; exists {
+		return true
+	}
+
+	return fold.isGlobal(name)
+}
+
+func (fold *seedFold) read(name string) {
+	index, isOutput := fold.outputIndex[name]
+	if isOutput && !fold.replaced[index] {
+		fold.effects[index] = MaySeedRead
+	}
+}
+
+func (fold *seedFold) replace(name string) {
+	if index, isOutput := fold.outputIndex[name]; isOutput {
+		fold.replaced[index] = true
+	}
+}
+
+func (fold *seedFold) foldStatement(stmt *ast.LetStatement, effect StatementEffect) {
+	for _, targetIndex := range effect.CalleeReadsSeed {
+		fold.read(stmt.Name[targetIndex].Value)
+	}
+
+	for _, write := range effect.Writes {
+		if effect.replacesTarget(write) {
+			fold.replace(stmt.Name[write.TargetIndex].Value)
+		}
+	}
+
+	for _, target := range stmt.Name {
+		if !isDiscard(target) {
+			fold.defined[target.Value] = struct{}{}
+		}
+	}
+}
+
+// deriveBodySeedEffects summarizes, per output, whether the scalar body may
+// read that output's incoming value. Explicit reads come from conditions,
+// values, print arguments, and resolved formatting markers; implicit reads
+// come from callees that read their own seed. A boundary-resolved write only
+// preserves the seed, so it does not replace the output.
+func deriveBodySeedEffects(template *ast.FuncStatement, statements map[*ast.LetStatement]StatementEffect, isGlobal func(string) bool) []SeedEffect {
+	fold := newSeedFold(template, isGlobal)
+
+	for _, statement := range template.Body.Statements {
+		for _, name := range statementReadNames(statement, fold.isDefined) {
+			fold.read(name)
+		}
+
+		stmt, ok := statement.(*ast.LetStatement)
+		if !ok {
+			continue
+		}
+
+		effect, exists := statements[stmt]
+		if !exists || !validStatementEffect(stmt, effect) {
+			return slices.Repeat([]SeedEffect{SeedInvalid}, len(template.Outputs))
+		}
+		fold.foldStatement(stmt, effect)
+	}
+
+	return fold.effects
+}
+
+// statementReadNames returns every identifier a statement reads in source
+// order, including resolved formatting markers and their dynamic width and
+// precision operands.
+func statementReadNames(statement ast.Statement, isDefined func(string) bool) []string {
+	var names []string
+
+	switch stmt := statement.(type) {
+	case *ast.LetStatement:
+		for _, condition := range stmt.Condition {
+			names = appendExprReadNames(names, condition, isDefined)
+		}
+		for _, value := range stmt.Value {
+			names = appendExprReadNames(names, value, isDefined)
+		}
+	case *ast.PrintStatement:
+		for _, argument := range stmt.Expression.Arguments {
+			names = appendExprReadNames(names, argument, isDefined)
+		}
+	}
+
+	return names
+}
+
+func appendExprReadNames(names []string, expr ast.Expression, isDefined func(string) bool) []string {
+	switch e := expr.(type) {
+	case *ast.Identifier:
+		return append(names, e.Value)
+	case *ast.StringLiteral:
+		mains, specs := formatMarkerIdentifiers(e.Token.Literal, isDefined)
+		return append(append(names, mains...), specs...)
+	}
+
+	for _, child := range ast.ExprChildren(expr) {
+		names = appendExprReadNames(names, child, isDefined)
+	}
+
+	return names
+}
+
 type specializationNodeID int
 
 type specializationNode struct {
@@ -755,23 +981,31 @@ func (state *tarjanState) visit(id specializationNodeID) {
 }
 
 // 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 {
+// weakened from MustWrite to MayWrite or grew from NoSeedRead to MaySeedRead.
+// Both directions are conservative, and either one must requeue callers.
+func (ts *TypeSolver) deriveEffectNode(graph *specializationCallGraph, working []bodyEffects, 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)
+	compiler := ts.ScriptCompiler.Compiler
+	analyzer := newEffectAnalyzer(compiler, node.mangled, graph, working)
 	statements := analyzer.deriveStatements(walked.template.Body.Statements, initial)
-	derived := deriveBodyOutputEffects(walked.template, statements)
+	writes := deriveBodyOutputEffects(walked.template, statements)
+	seeds := deriveBodySeedEffects(walked.template, statements, compiler.CodeCompiler.isGlobalBinding)
 
-	if !validPublishedEffects(derived, len(walked.info.Sig.OutTypes)) {
+	outputs := len(walked.info.Sig.OutTypes)
+	if !validPublishedEffects(writes, outputs) || !validPublishedSeedEffects(seeds, outputs) {
 		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
+	for outputIndex := range outputs {
+		if working[id].writes[outputIndex] == MustWrite && writes[outputIndex] == MayWrite {
+			working[id].writes[outputIndex] = MayWrite
+			changed = true
+		}
+		if working[id].seeds[outputIndex] == NoSeedRead && seeds[outputIndex] == MaySeedRead {
+			working[id].seeds[outputIndex] = MaySeedRead
 			changed = true
 		}
 	}
@@ -795,9 +1029,10 @@ func enqueueRecursiveEffectCallers(graph *specializationCallGraph, id specializa
 	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) {
+// settleEffectComponent drives one SCC to a fixed point and publishes all
+// members' write and seed facts together, only after their shared worklist
+// drains.
+func (ts *TypeSolver) settleEffectComponent(graph *specializationCallGraph, working []bodyEffects, component []specializationNodeID, queued []bool) {
 	pending := slices.Clone(component)
 
 	for _, id := range pending {
@@ -813,17 +1048,21 @@ func (ts *TypeSolver) settleEffectComponent(graph *specializationCallGraph, work
 	}
 
 	for _, id := range component {
-		node := &graph.nodes[id]
-		ts.walkedFuncs[node.mangled].info.BodyOutputEffects = slices.Clone(working[id])
+		info := ts.walkedFuncs[graph.nodes[id].mangled].info
+		info.BodyOutputEffects = slices.Clone(working[id].writes)
+		info.BodySeedEffects = slices.Clone(working[id].seeds)
 	}
 }
 
 func (ts *TypeSolver) settleEffects(graph *specializationCallGraph) {
-	working := make([][]WriteEffect, len(graph.nodes))
+	working := make([]bodyEffects, 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))
+		outputs := len(ts.walkedFuncs[graph.nodes[id].mangled].info.Sig.OutTypes)
+		working[id] = bodyEffects{
+			writes: slices.Repeat([]WriteEffect{MustWrite}, outputs),
+			seeds:  slices.Repeat([]SeedEffect{NoSeedRead}, outputs),
+		}
 	}
 
 	components := graph.calleeFirstComponents()
diff --git a/compiler/effects_test.go b/compiler/effects_test.go
index ef0b8862..1f8ee0be 100644
--- a/compiler/effects_test.go
+++ b/compiler/effects_test.go
@@ -28,24 +28,30 @@ func TestValidStatementEffectShape(t *testing.T) {
 		{TargetIndex: 2, Effect: MayWrite},
 	}
 	tests := []struct {
-		name      string
-		writes    []TargetWriteEffect
-		readsSeed []int
-		valid     bool
+		name            string
+		writes          []TargetWriteEffect
+		readsSeed       []int
+		calleeReadsSeed []int
+		valid           bool
 	}{
 		{name: "valid direct writes", writes: directWrites, valid: true},
 		{name: "valid mixed write effects", writes: mixedWrites, valid: true},
 		{name: "valid seed targets", writes: directWrites, readsSeed: []int{0, 2}, valid: true},
+		{name: "valid callee seed targets", writes: mixedWrites, calleeReadsSeed: []int{0, 2}, valid: true},
+		{name: "valid overlapping seed facts", writes: directWrites, readsSeed: []int{0}, calleeReadsSeed: []int{0}, valid: true},
 		{name: "missing named target", writes: directWrites[:1]},
 		{name: "write targets discard", writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}, {TargetIndex: 1, Effect: MustWrite}}},
 		{name: "invalid write state", writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}, {TargetIndex: 2, Effect: WriteInvalid}}},
 		{name: "duplicate seed target", writes: directWrites, readsSeed: []int{0, 0}},
 		{name: "seed targets discard", writes: directWrites, readsSeed: []int{1}},
+		{name: "descending callee seed targets", writes: directWrites, calleeReadsSeed: []int{2, 0}},
+		{name: "callee seed targets discard", writes: directWrites, calleeReadsSeed: []int{1}},
+		{name: "callee seed target out of range", writes: directWrites, calleeReadsSeed: []int{3}},
 	}
 
 	for _, test := range tests {
 		t.Run(test.name, func(t *testing.T) {
-			effect := StatementEffect{Writes: test.writes, ReadsSeed: test.readsSeed}
+			effect := StatementEffect{Writes: test.writes, ReadsSeed: test.readsSeed, CalleeReadsSeed: test.calleeReadsSeed}
 
 			require.Equal(t, test.valid, validStatementEffect(stmt, effect))
 		})
@@ -194,6 +200,7 @@ seeded, always, failed, gated`)
 	seededEffect := ts.ScriptCompiler.Script.Root.StatementEffects[seeded]
 	requireTargetEffects(t, seededEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
 	require.Equal(t, []int{0}, seededEffect.ReadsSeed)
+	require.Empty(t, seededEffect.CalleeReadsSeed)
 	require.Equal(t, []YieldEffect{MayYield}, ts.ExprCache[key(ts.FuncNameMangled, seeded.Value[0])].YieldEffects)
 
 	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
@@ -217,6 +224,10 @@ seeded, always, failed, gated`)
 
 	require.Equal(t, []WriteEffect{MayWrite}, maybeFunc.BodyOutputEffects)
 	require.Equal(t, []WriteEffect{MustWrite}, alwaysFunc.BodyOutputEffects)
+	// Skipping a write leaves preservation to the caller; neither body reads
+	// its incoming value.
+	require.Equal(t, []SeedEffect{NoSeedRead}, maybeFunc.BodySeedEffects)
+	require.Equal(t, []SeedEffect{NoSeedRead}, alwaysFunc.BodySeedEffects)
 	require.True(t, maybeFunc.Settled)
 	require.True(t, alwaysFunc.Settled)
 }
@@ -242,6 +253,9 @@ fresh, existing`)
 
 	require.NotNil(t, wrap)
 	require.Equal(t, []WriteEffect{MayWrite}, wrap.BodyOutputEffects)
+	// The inner boundary resolution only passes the seed through; nothing in
+	// the body consumes it.
+	require.Equal(t, []SeedEffect{NoSeedRead}, wrap.BodySeedEffects)
 
 	template, ok := cc.lookupFuncTemplate("Wrap", 1)
 	require.True(t, ok)
@@ -249,11 +263,13 @@ fresh, existing`)
 	firstBodyEffect := wrap.StatementEffects[firstBodyStmt]
 	requireTargetEffects(t, firstBodyEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
 	require.Empty(t, firstBodyEffect.ReadsSeed)
+	require.Empty(t, firstBodyEffect.CalleeReadsSeed)
 
 	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)
+	require.Empty(t, secondBodyEffect.CalleeReadsSeed)
 
 	fresh := ts.ScriptCompiler.Program.Statements[0].(*ast.LetStatement)
 	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
@@ -517,3 +533,291 @@ value`)
 
 	require.Equal(t, []YieldEffect{YieldInvalid}, analyzer.deriveExpr(call))
 }
+
+// requireBodyEffects checks the published write and seed facts of every
+// settled specialization named name; a ranged call also settles the scalar
+// companion, and both summarize the same body.
+func requireBodyEffects(t *testing.T, cc *CodeCompiler, name string, writes []WriteEffect, seeds []SeedEffect) {
+	t.Helper()
+
+	found := 0
+	for mangled, f := range cc.Compiler.FuncCache {
+		if f.Sig.Name != name {
+			continue
+		}
+		found++
+		require.True(t, f.Settled, mangled)
+		require.Equal(t, writes, f.BodyOutputEffects, mangled)
+		require.Equal(t, seeds, f.BodySeedEffects, mangled)
+	}
+	require.NotZero(t, found, "missing specialization of %s", name)
+}
+
+func scriptStatementEffect(t *testing.T, ts *TypeSolver, index int) StatementEffect {
+	t.Helper()
+
+	stmt := ts.ScriptCompiler.Program.Statements[index].(*ast.LetStatement)
+	effect, exists := ts.ScriptCompiler.Script.Root.StatementEffects[stmt]
+	require.True(t, exists)
+	return effect
+}
+
+func bodyStatementEffect(t *testing.T, cc *CodeCompiler, name string, index int) StatementEffect {
+	t.Helper()
+
+	template, ok := cc.lookupFuncTemplate(name, 1)
+	require.True(t, ok)
+	stmt := template.Body.Statements[index].(*ast.LetStatement)
+
+	for _, f := range cc.Compiler.FuncCache {
+		if f.Sig.Name != name {
+			continue
+		}
+		effect, exists := f.StatementEffects[stmt]
+		require.True(t, exists)
+		return effect
+	}
+
+	require.Fail(t, "missing specialization", name)
+	return StatementEffect{}
+}
+
+func TestSeedDependentMustWriteReadsDestination(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "seedDependentEffects", "", mustParseCode(t, `y = MaybeIncrement(x)
+    y = x > 0 x
+    y = y + 1
+
+y = Overwrite(x)
+    y = x
+    y = y + 1`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `seeded = 20
+seeded = MaybeIncrement(-1)
+fresh = MaybeIncrement(-1)
+replaced = 7
+replaced = Overwrite(3)
+seeded, fresh, replaced`)
+
+	// The write effect is the same; only the seed dependency differs.
+	requireBodyEffects(t, cc, "MaybeIncrement", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "Overwrite", []WriteEffect{MustWrite}, []SeedEffect{NoSeedRead})
+
+	seeded := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, seeded, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, seeded.ReadsSeed)
+	require.Equal(t, []int{0}, seeded.CalleeReadsSeed)
+
+	// The fact describes the callee; a fresh destination has no value for the
+	// CFG to read.
+	fresh := scriptStatementEffect(t, ts, 2)
+	requireTargetEffects(t, fresh, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, fresh.ReadsSeed)
+	require.Equal(t, []int{0}, fresh.CalleeReadsSeed)
+
+	replaced := scriptStatementEffect(t, ts, 4)
+	requireTargetEffects(t, replaced, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, replaced.ReadsSeed)
+	require.Empty(t, replaced.CalleeReadsSeed)
+}
+
+func TestSeedReadSurvivesCopyConditionAndPrint(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "stickySeedEffects", "", mustParseCode(t, `y = CopyThenReplace(x)
+    y = x > 0 x
+    saved = y
+    y = x
+    y = y + saved
+
+y = GatedRead(x)
+    y = x > 0 x
+    y = y > 0 x
+    y = x
+
+y = PrintedRead(x)
+    y = x > 0 x
+    y
+    y = x
+
+y = MarkerRead(x)
+    y = x > 0 x
+    "seed -y"
+    y = x
+
+y = WidthRead(x)
+    y = x > 0 x
+    "-x%(-y)d"
+    y = x`))
+	require.Empty(t, cc.Compile())
+
+	solveScriptTypes(t, ctx, cc, t.Name(), `a = CopyThenReplace(1)
+b = GatedRead(1)
+c = PrintedRead(1)
+d = MarkerRead(1)
+e = WidthRead(1)
+a, b, c, d, e`)
+
+	for _, name := range []string{"CopyThenReplace", "GatedRead", "PrintedRead", "MarkerRead", "WidthRead"} {
+		requireBodyEffects(t, cc, name, []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	}
+}
+
+func TestNestedSeedReadsCompose(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "nestedSeedEffects", "", mustParseCode(t, `y = MaybeIncrement(x)
+    y = x > 0 x
+    y = y + 1
+
+y = Outer(x)
+    y = MaybeIncrement(x)
+
+y = ResetThenIncrement(x)
+    y = 0
+    y = MaybeIncrement(x)`))
+	require.Empty(t, cc.Compile())
+
+	solveScriptTypes(t, ctx, cc, t.Name(), `a = Outer(1)
+b = ResetThenIncrement(1)
+a, b`)
+
+	requireBodyEffects(t, cc, "Outer", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "ResetThenIncrement", []WriteEffect{MustWrite}, []SeedEffect{NoSeedRead})
+
+	// The output is unpublished at its first statement, so the callee's read
+	// is recorded without a boundary resolution.
+	outerCall := bodyStatementEffect(t, cc, "Outer", 0)
+	requireTargetEffects(t, outerCall, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, outerCall.ReadsSeed)
+	require.Equal(t, []int{0}, outerCall.CalleeReadsSeed)
+
+	// The inner call reads the reset value, which keeps that write live.
+	resetCall := bodyStatementEffect(t, cc, "ResetThenIncrement", 1)
+	requireTargetEffects(t, resetCall, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, resetCall.ReadsSeed)
+	require.Equal(t, []int{0}, resetCall.CalleeReadsSeed)
+}
+
+func TestCrossOutputSeedReads(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "crossOutputSeedEffects", "", mustParseCode(t, `a, b = Cross(x)
+    a = x > 0 x
+    b = a + 1
+    a = x`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `p = 20
+p, q = Cross(-1)
+p, q`)
+
+	requireBodyEffects(t, cc, "Cross", []WriteEffect{MustWrite, MustWrite}, []SeedEffect{MaySeedRead, NoSeedRead})
+
+	call := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, call,
+		TargetWriteEffect{TargetIndex: 0, Effect: MustWrite},
+		TargetWriteEffect{TargetIndex: 1, Effect: MustWrite},
+	)
+	require.Empty(t, call.ReadsSeed)
+	require.Equal(t, []int{0}, call.CalleeReadsSeed)
+}
+
+func TestRecursiveSeedReadsConvergeAcrossSCC(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	// A reads its seed only through B, so the fact must grow across the
+	// component after B's own read is discovered.
+	cc := NewCodeCompiler(ctx, "recursiveSeedEffects", "", mustParseCode(t, `y = A(n)
+    y = B(n)
+
+y = B(n)
+    y = n == 0 1
+    y = n > 0 A(n - 1)
+    y = y + 1`))
+	require.Empty(t, cc.Compile())
+
+	solveScriptTypes(t, ctx, cc, t.Name(), `result = A(2)
+result`)
+
+	requireBodyEffects(t, cc, "A", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "B", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+}
+
+func TestIndirectCalleeSeedReadsCompose(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "indirectSeedEffects", "", mustParseCode(t, `s = MaybeTag(n, t)
+    s = n > 0 t
+    s = s ⊕ "!"
+
+s = GatedTag(n, t)
+    s = n > 0 t
+    s = n > 1 s ⊕ "!"`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `w = "hi"
+w = MaybeTag(-1, "x")
+v = "hi"
+v = GatedTag(-1, "x")
+w, v`)
+
+	requireBodyEffects(t, cc, "MaybeTag", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "GatedTag", []WriteEffect{MayWrite}, []SeedEffect{MaySeedRead})
+
+	// Indirect outputs never resolve at the boundary, but the dependency on
+	// the destination-seeded staging slot composes all the same.
+	mustWrite := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, mustWrite, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, mustWrite.ReadsSeed)
+	require.Equal(t, []int{0}, mustWrite.CalleeReadsSeed)
+
+	mayWrite := scriptStatementEffect(t, ts, 3)
+	requireTargetEffects(t, mayWrite, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
+	require.Empty(t, mayWrite.ReadsSeed)
+	require.Equal(t, []int{0}, mayWrite.CalleeReadsSeed)
+}
+
+func TestFunctionDomainSeedReadsKeepBoundaryFacts(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "domainSeedEffects", "", mustParseCode(t, `y = AccRange(r)
+    y = r > 5 r
+    y = y + r`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `existing = 20
+existing = AccRange(0:3)
+empty = 20
+empty = AccRange(0:0)
+fresh = AccRange(0:3)
+existing, empty, fresh`)
+
+	requireBodyEffects(t, cc, "AccRange", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+
+	existing := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, existing, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, existing.ReadsSeed)
+	require.Equal(t, []int{0}, existing.CalleeReadsSeed)
+
+	// A possibly empty call-owned domain still resolves at the boundary; the
+	// two facts coexist on one target.
+	empty := scriptStatementEffect(t, ts, 3)
+	requireTargetEffects(t, empty, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Equal(t, []int{0}, empty.ReadsSeed)
+	require.Equal(t, []int{0}, empty.CalleeReadsSeed)
+
+	fresh := scriptStatementEffect(t, ts, 4)
+	requireTargetEffects(t, fresh, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, fresh.ReadsSeed)
+	require.Equal(t, []int{0}, fresh.CalleeReadsSeed)
+}
diff --git a/compiler/solver.go b/compiler/solver.go
index 10176250..2dffb34b 100644
--- a/compiler/solver.go
+++ b/compiler/solver.go
@@ -2468,6 +2468,7 @@ func newFunc(name string, bodyArgs []Type, template *ast.FuncStatement) *FuncInf
 		Vars:              make(map[string]Type),
 		StatementEffects:  make(map[*ast.LetStatement]StatementEffect),
 		BodyOutputEffects: slices.Repeat([]WriteEffect{WriteUncomputed}, len(template.Outputs)),
+		BodySeedEffects:   slices.Repeat([]SeedEffect{SeedUncomputed}, len(template.Outputs)),
 	}
 	for i := range f.Sig.OutTypes {
 		f.Sig.OutTypes[i] = Unresolved{}
diff --git a/compiler/solver_test.go b/compiler/solver_test.go
index aea3b290..ab90ed86 100644
--- a/compiler/solver_test.go
+++ b/compiler/solver_test.go
@@ -77,6 +77,7 @@ x, y`
 	isEvenFunc := newFunc(call.Function.Value, args, template)
 	cc.Compiler.FuncCache[isEvenMangled] = isEvenFunc
 	require.Equal(t, []WriteEffect{WriteUncomputed, WriteUncomputed}, isEvenFunc.BodyOutputEffects)
+	require.Equal(t, []SeedEffect{SeedUncomputed, SeedUncomputed}, isEvenFunc.BodySeedEffects)
 	isOddMangled := Mangle(cc.Compiler.MangledPath, "isOdd", args)
 
 	ts.Converging = false
@@ -112,6 +113,8 @@ x, y`
 	require.True(t, isOddFunc.Settled)
 	require.Equal(t, []WriteEffect{MayWrite, MayWrite}, isEvenFunc.BodyOutputEffects)
 	require.Equal(t, []WriteEffect{MayWrite, MayWrite}, isOddFunc.BodyOutputEffects)
+	require.Equal(t, []SeedEffect{NoSeedRead, NoSeedRead}, isEvenFunc.BodySeedEffects)
+	require.Equal(t, []SeedEffect{NoSeedRead, NoSeedRead}, isOddFunc.BodySeedEffects)
 
 	ts.Solve()
 	require.Empty(t, ts.Errors)
diff --git a/compiler/types.go b/compiler/types.go
index b187de81..07057eb0 100644
--- a/compiler/types.go
+++ b/compiler/types.go
@@ -284,8 +284,12 @@ type FuncInfo struct {
 	// 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
+	// BodySeedEffects records, per output, whether that body may read the
+	// output's incoming value before definitely replacing it. It is published
+	// together with BodyOutputEffects; the two facts are independent.
+	BodySeedEffects []SeedEffect
+	CFGResult       *SpecializationCFGResult
+	Settled         bool
 }
 
 func (f *FuncInfo) AllTypesInferred() bool {
diff --git a/docs/Pluto IR Plan.md b/docs/Pluto IR Plan.md
index c5f35aff..8bfe7843 100644
--- a/docs/Pluto IR Plan.md	
+++ b/docs/Pluto IR Plan.md	
@@ -849,11 +849,14 @@ consume the raw, validity-carrying result and see the skip.
 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`, resolved at `=`.
-A fresh destination, a discard, a nested or targetless call, or an
-all-`MustWrite` callee reads nothing. Step 2A records this 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.
+A fresh destination, a discard, or a nested or targetless call resolves
+nothing at the boundary. An all-`MustWrite` callee needs no boundary
+resolution either, but its body may still read the seed; that is the separate
+`SeedEffect` fact below, and the two must not be conflated. 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.
 
 The validity-carrying result comes from a **private direct-call variant**
 behind the stable seeded entry point (§1). The clone **keeps the seed
@@ -874,6 +877,47 @@ The variant lands in Step 4; letting print treat a resolved seed as always
 yielded was rejected, since an unwritten output would then print stale data
 instead of suppressing the invocation.
 
+### SeedEffect
+
+`SeedEffect` records, per declared output, whether the scalar body can read
+that output's **incoming value** before definitely replacing it: `NoSeedRead`
+or `MaySeedRead`, with `Uncomputed` and `Invalid` as publication states
+outside the lattice. It is independent of `WriteEffect`. `y = x > 0 x` then
+`y = y + 1` is `MustWrite` and `MaySeedRead`: the last statement always
+writes, but its value depends on the seed, so `a = 20` followed by that call
+must print 21 and compile without an intervening read. `y = x` then
+`y = y + 1` is `MustWrite` and `NoSeedRead`: the definite overwrite comes
+first. A conditionally writing body may inspect its seed or leave preservation
+entirely to the caller; `MayWrite` alone says nothing about which.
+
+Three facts stay separate, each with its own consumer:
+
+| Fact | Question | Where |
+| --- | --- | --- |
+| Body write effect | Does this output receive a body-produced value whenever the scalar body runs? | `BodyOutputEffects`; yield propagation and call routing |
+| Seed-read dependency | Can the body read this output's incoming value before it is definitely replaced? | `BodySeedEffects`; caller liveness and future scheduling |
+| Boundary resolution | Does this assignment use its existing destination to resolve a non-writing direct result? | `StatementEffect.ReadsSeed`; keep-old at `=` |
+
+The body fold is order-sensitive. Explicit reads — conditions, values, print
+arguments, and resolved formatting markers with their dynamic width and
+precision operands — and implicit reads through a callee whose output is
+`MaySeedRead` happen before the statement's writes. An output stops being
+observable once a raw `MustWrite` replaces it; a boundary-resolved write only
+preserves the seed and replaces nothing. The fact is sticky: copying the seed
+to a local before the overwrite keeps the dependency, as does a read only in a
+condition or a printed string. Reads feeding another output count, so
+`a, b = F(x)` with `b = a + 1` before `a = x` reads `a`'s seed. A
+function-owned `Range` domain needs no special case: the first iteration is
+the body, and a zero-iteration call is already resolved at the boundary.
+
+At a call site the callee's fact composes into `StatementEffect.CalleeReadsSeed`
+for every named target, whatever the ABI: an indirect output reads its
+destination-seeded staging slot exactly as a direct return reads its hidden
+seed parameter. Only boundary resolution is direct-ABI specific. A fresh
+destination supplies a zero seed, so the CFG emits a read only for a defined
+binding, while the enclosing body's fold treats a call at a not-yet-replaced
+output as a read of that output.
+
 ### Convergence and publication
 
 **Folding a body into an output summary.** A declared output's body summary is
@@ -886,8 +930,10 @@ destination seed (`ReadsSeed`) also leaves the summary unchanged: preserving
 an earlier value does not prove that the body wrote one. 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
+the scalar body executes, not what the body does when it executes. The seed
+fold runs beside the write fold over the same statement effects, and the two
+summaries publish together as `BodyOutputEffects` and `BodySeedEffects`. 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
@@ -934,17 +980,20 @@ 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.
+1. Seed every member's outputs with provisional `MustWrite` and `NoSeedRead`
+   working vectors. A recursive call reads those provisional values — 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
+3. Move monotonically toward the conservative side only: `MustWrite →
+   MayWrite` and `NoSeedRead → MaySeedRead`. Either change requeues the
+   member's callers within the component. The working vectors **persist across
+   body walks** within the component; they are 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.
+4. Stop when nothing changes — at most one change per slot and fact.
+5. Publish one coherent snapshot of both facts for the whole component at once.
 
 An `Invalid` output blocks publication for its entire component; provisional
 values are never read outside it.
@@ -980,8 +1029,9 @@ 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
-therefore observe the simultaneous assignment's pre-commit snapshot. Print
+reads, `CalleeReadsSeed` destination reads for defined bindings, 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
@@ -998,8 +1048,9 @@ The two diagnostics consume effects differently:
   value requires **both** writes to be `MustWrite`. This cures the former
   conditional-write false positive that forced tests to interleave reads merely
   to silence it. A prior seed overwritten by a proven-`MustWrite` call output
-  without being read is instead a true positive: remove the seed or read it
-  explicitly when its value is semantically required.
+  that neither the caller nor the callee body reads is instead a true
+  positive: remove the seed or read it explicitly when its value is
+  semantically required.
 
 After a script solve succeeds, CFG first treats the script as a zero-input,
 zero-output template for structural validation, then runs effect-sensitive
diff --git a/tests/seed/seed_read.exp b/tests/seed/seed_read.exp
new file mode 100644
index 00000000..65475692
--- /dev/null
+++ b/tests/seed/seed_read.exp
@@ -0,0 +1,14 @@
+Seeded: 21
+Fresh: 1
+Written: 6
+Nested: 21
+Reset: 1
+Cross: -1 21
+inside 20
+Printed: -1
+Zero: 20
+One: 20
+Many: 23
+ManyFresh: 3
+Tag: hi!
+TagWritten: x!
diff --git a/tests/seed/seed_read.pt b/tests/seed/seed_read.pt
new file mode 100644
index 00000000..5c3a17e1
--- /dev/null
+++ b/tests/seed/seed_read.pt
@@ -0,0 +1,31 @@
+# A body whose last statement always writes can still depend on the incoming
+# output seed. Each caller below assigns such a call over an existing value
+# without reading it first; the analysis keeps that value live.
+y = MaybeIncrement(x)
+    y = x > 0 x
+    y = y + 1
+
+y = Outer(x)
+    y = MaybeIncrement(x)
+
+y = ResetThenIncrement(x)
+    y = 0
+    y = MaybeIncrement(x)
+
+a, b = Cross(x)
+    a = x > 0 x
+    b = a + 1
+    a = x
+
+y = Printed(x)
+    y = x > 0 x
+    "inside -y"
+    y = x
+
+y = AccRange(r)
+    y = r > 5 r
+    y = y + r
+
+s = MaybeTag(n, t)
+    s = n > 0 t
+    s = s ⊕ "!"
diff --git a/tests/seed/seed_read.spt b/tests/seed/seed_read.spt
new file mode 100644
index 00000000..90fd29b7
--- /dev/null
+++ b/tests/seed/seed_read.spt
@@ -0,0 +1,36 @@
+seeded = 20
+seeded = MaybeIncrement(-1)
+"Seeded: -seeded"
+fresh = MaybeIncrement(-1)
+"Fresh: -fresh"
+written = 20
+written = MaybeIncrement(5)
+"Written: -written"
+nested = 20
+nested = Outer(-1)
+"Nested: -nested"
+reset = ResetThenIncrement(-1)
+"Reset: -reset"
+crossA = 20
+crossA, crossB = Cross(-1)
+"Cross: -crossA -crossB"
+printed = 20
+printed = Printed(-1)
+"Printed: -printed"
+zero = 20
+zero = AccRange(0:0)
+"Zero: -zero"
+one = 20
+one = AccRange(0:1)
+"One: -one"
+many = 20
+many = AccRange(0:3)
+"Many: -many"
+manyFresh = AccRange(0:3)
+"ManyFresh: -manyFresh"
+tag = "hi"
+tag = MaybeTag(-1, "x")
+"Tag: -tag"
+tagWritten = "hi"
+tagWritten = MaybeTag(1, "x")
+"TagWritten: -tagWritten"
diff --git a/tests/seed/seed_read_warm.exp b/tests/seed/seed_read_warm.exp
new file mode 100644
index 00000000..173af044
--- /dev/null
+++ b/tests/seed/seed_read_warm.exp
@@ -0,0 +1,4 @@
+WarmSeeded: 21
+WarmNested: 21
+WarmMany: 23
+WarmTag: hi!
diff --git a/tests/seed/seed_read_warm.spt b/tests/seed/seed_read_warm.spt
new file mode 100644
index 00000000..34625981
--- /dev/null
+++ b/tests/seed/seed_read_warm.spt
@@ -0,0 +1,14 @@
+# Compiled after seed_read.spt in the same run, so every callee is already
+# settled and its seed facts are replayed from the shared cache.
+seeded = 20
+seeded = MaybeIncrement(-1)
+"WarmSeeded: -seeded"
+nested = 20
+nested = Outer(-1)
+"WarmNested: -nested"
+many = 20
+many = AccRange(0:3)
+"WarmMany: -many"
+tag = "hi"
+tag = MaybeTag(-1, "x")
+"WarmTag: -tag"

From 0fe19f3623903f01da1d1e9b694ef03f2b30e48f Mon Sep 17 00:00:00 2001
From: Tejas <tejasvph@gmail.com>
Date: Fri, 11 Sep 2026 19:06:31 +0530
Subject: [PATCH 2/3] docs(effects): record PR #102 as the seed dependency
 resolution

Tick the section 1 acceptance criteria, point the backlog row at the
PR, and defer the canonical description to PIR plan section 15.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
---
 docs/Pluto Effects and Follow-up Plan.md | 27 ++++++++++++++----------
 1 file changed, 16 insertions(+), 11 deletions(-)

diff --git a/docs/Pluto Effects and Follow-up Plan.md b/docs/Pluto Effects and Follow-up Plan.md
index c4a7070b..6e1a69d2 100644
--- a/docs/Pluto Effects and Follow-up Plan.md	
+++ b/docs/Pluto Effects and Follow-up Plan.md	
@@ -19,6 +19,11 @@ type, and stored type separately, as the corrected code comment already does.
 
 ## 1. Next compiler PR: seed dependency analysis
 
+Resolved by [PR #102](https://github.com/thiremani/pluto/pull/102), which
+publishes a per-output `SeedEffect` beside `BodyOutputEffects`, records
+`StatementEffect.CalleeReadsSeed` at call sites, and consumes both in the CFG;
+[PIR plan, section 15](./Pluto%20IR%20Plan.md) is the canonical description.
+
 Preserve the existing seeded-output semantics and public ABI. Correct the
 analysis before deciding whether a later language version should change those
 semantics.
@@ -92,27 +97,27 @@ discipline. Unknown analysis must not silently mean no seed reads.
 
 ### Acceptance criteria
 
-- [ ] The reproducer compiles without a redundant print and produces 21; the
+- [x] The reproducer compiles without a redundant print and produces 21; the
   fresh-target variant produces 1.
-- [ ] Unconditional seed-dependent writes remain `MustWrite`, with the old
+- [x] Unconditional seed-dependent writes remain `MustWrite`, with the old
   destination live where needed.
-- [ ] A definite overwrite before any read removes the incoming-seed dependency;
+- [x] A definite overwrite before any read removes the incoming-seed dependency;
   a conditional overwrite does not. Copying the seed to a local first preserves
   the dependency even if the output is subsequently overwritten.
-- [ ] A seed read only in a condition or printed string still counts when the
+- [x] A seed read only in a condition or printed string still counts when the
   output is later unconditionally overwritten. Seed reads are not limited to
   dependencies of the returned value.
-- [ ] Nested calls, recursive summaries, multiple outputs, cross-output seed
+- [x] Nested calls, recursive summaries, multiple outputs, cross-output seed
   reads, and zero/one/many-iteration cases are covered.
-- [ ] Fresh targets, discards, incompatible-storage zero seeds, caller argument
+- [x] Fresh targets, discards, incompatible-storage zero seeds, caller argument
   failure, and caller-side retention keep their existing distinct behavior.
-- [ ] CFG and PIR consume settled solver facts rather than independently
+- [x] CFG and PIR consume settled solver facts rather than independently
   rediscovering dependencies. Existing unused-write diagnostics still work.
-- [ ] Direct and indirect calls preserve staging and alias-input regressions.
+- [x] Direct and indirect calls preserve staging and alias-input regressions.
   Public symbols and prototypes do not change with body effects; every public
   direct scalar return retains its existing hidden seed parameter.
-- [ ] Cold and warm caches agree on summaries, diagnostics, and output.
-- [ ] Effect tests, CFG regression tests, ABI/IR checks, race tests, and relevant
+- [x] Cold and warm caches agree on summaries, diagnostics, and output.
+- [x] Effect tests, CFG regression tests, ABI/IR checks, race tests, and relevant
   leak checks pass. Run the full leak suite before submitting the compiler PR.
 
 ## 2. Formatting: model `%n` as an explicit write operand
@@ -198,7 +203,7 @@ and [ABI stability plan](./Pluto%20ABI%20Optimization%20Plan.md).
 
 | Work | Completion criterion / existing reference |
 | --- | --- |
-| Seed/effect correctness | Section 1; next compiler PR before broadening call routing |
+| Seed/effect correctness | Section 1; resolved by [PR #102](https://github.com/thiremani/pluto/pull/102) |
 | `%n` effect contract | Section 2; separate bounded change with formatting semantics updated |
 | Output path protection | [Issue #80](https://github.com/thiremani/pluto/issues/80): compilation cannot overwrite source/configuration through name collisions or unsafe path resolution |
 | Numeric edge behavior | Define and guard integer divide/remainder faults and invalid shift counts; audit range/count/allocation arithmetic |

From d638c3fc5c7b8c73320e24ee796d0bdcd88ee522 Mon Sep 17 00:00:00 2001
From: Tejas <tejasvph@gmail.com>
Date: Fri, 11 Sep 2026 19:35:36 +0530
Subject: [PATCH 3/3] fix(compiler): compose callee seed reads only through
 compatible storage

An indirect callee reads its destination only when lowering seeds the
staging slot from it, which makeCallOutputAdapters does only for
identical storage types. A StrH destination for a StrG output gets an
ABI-typed zero seed, so the callee never observes the caller's value,
yet CalleeReadsSeed recorded a read and suppressed the true
unused-overwrite diagnostic. Gate the composed read on TypeEqual between
the destination's slot type and the callee output, the same authority
destSlotType consults; direct scalar returns always match.

Un-tick the PIR half of the consumption criterion: PIR does not route
calls yet, so its consumption of the seed facts is owed by Step 4.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
---
 compiler/cfg_test.go                     | 12 ++++++
 compiler/effects.go                      | 53 +++++++++++++++++-------
 compiler/effects_test.go                 | 33 +++++++++++++++
 docs/Pluto Effects and Follow-up Plan.md |  4 +-
 docs/Pluto IR Plan.md                    | 11 +++--
 tests/seed/seed_read.exp                 |  5 +++
 tests/seed/seed_read.pt                  |  5 +++
 tests/seed/seed_read.spt                 |  7 ++++
 8 files changed, 111 insertions(+), 19 deletions(-)

diff --git a/compiler/cfg_test.go b/compiler/cfg_test.go
index 8850560b..94027ffb 100644
--- a/compiler/cfg_test.go
+++ b/compiler/cfg_test.go
@@ -275,6 +275,18 @@ res = resetThenIncrement(x)
 			input:         "x = 7\nx = resetThenIncrement(-1)\nx",
 			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
 		},
+		{
+			// A heap destination cannot seed a static-string output: the
+			// callee's staging slot gets an ABI-typed zero seed, so the
+			// destination's value is never observed and the overwrite is real.
+			name: "Incompatible Storage Seed Does Not Reach Callee",
+			code: `s = readStatic(n)
+    s = n > 0 "x"
+    "seen <-s>"
+    s = "done"`,
+			input:         "value = \"never\" ⊕ \"read\"\nvalue = readStatic(0)\nvalue",
+			errorContains: `unconditional assignment to "value" overwrites a previous value that was never used`,
+		},
 		{
 			// A fresh destination supplies a zero seed; the callee's read does
 			// not make the result used.
diff --git a/compiler/effects.go b/compiler/effects.go
index 57d4ca8c..6b0cdc77 100644
--- a/compiler/effects.go
+++ b/compiler/effects.go
@@ -100,11 +100,11 @@ type TargetWriteEffect struct {
 // StatementEffect contains the target facts derived for one assignment.
 // ReadsSeed holds LHS indices whose existing value resolves a direct MayWrite
 // callee output at the assignment boundary; such a write preserves a value
-// rather than producing one. CalleeReadsSeed holds LHS indices whose incoming
-// value the callee body itself may read before definitely replacing it,
-// whatever the write effect. It is recorded for every named target because a
-// fresh destination supplies a zero seed: consumers decide whether an
-// existing value is involved.
+// rather than producing one. CalleeReadsSeed holds LHS indices whose value the
+// callee body itself may read before definitely replacing it, whatever the
+// write effect: the callee may read its seed and the destination's storage
+// lets that seed reach it. A fresh destination still supplies a zero seed, so
+// consumers decide whether an existing value is involved.
 type StatementEffect struct {
 	Writes          []TargetWriteEffect
 	ReadsSeed       []int
@@ -463,21 +463,45 @@ func (analyzer *effectAnalyzer) callOwnsPossiblyEmptyDomain(call *ast.CallExpres
 	return false
 }
 
-// calleeSeedEffects returns the callee's per-output seed facts for a resolved
-// call and nil for every other expression, which reads no destination. An
-// unpublished fact is an ICE: unknown analysis must not mean no seed reads.
-func (analyzer *effectAnalyzer) calleeSeedEffects(expr ast.Expression) []SeedEffect {
+// calleeReadsSeed reports whether a resolved call's callee may read the
+// destination of one output slot. Only a call reads a destination, and an
+// unpublished seed fact is an ICE: unknown analysis must not mean no seed
+// reads. The read composes only when the seed reaches the callee. Lowering
+// seeds an indirect output's staging slot from the destination only when the
+// two storage types are identical (makeCallOutputAdapters); a mismatched
+// flavor gets an ABI-typed zero seed, so the callee never observes the
+// destination's value. A direct scalar return always matches its destination.
+func (analyzer *effectAnalyzer) calleeReadsSeed(expr ast.Expression, slot int, target string) bool {
 	call, ok := expr.(*ast.CallExpression)
-	if !ok || !typesResolved(analyzer.exprInfo(call).OutTypes) {
-		return nil
+	if !ok {
+		return false
+	}
+
+	info := analyzer.exprInfo(call)
+	if !typesResolved(info.OutTypes) {
+		return false
 	}
 
 	seeds := analyzer.callBodyEffects(call).seeds
-	if !validPublishedSeedEffects(seeds, len(analyzer.exprInfo(call).OutTypes)) {
+	if !validPublishedSeedEffects(seeds, len(info.OutTypes)) {
 		panic(fmt.Sprintf("internal: call %s has unpublished seed effects %v", call.Function.Value, seeds))
 	}
+	if seeds[slot] != MaySeedRead {
+		return false
+	}
+
+	return TypeEqual(analyzer.bindingSlotType(target), info.OutTypes[slot])
+}
+
+// bindingSlotType returns the solver's slot type for a named target, the
+// same authority lowering's destSlotType consults for an assignment.
+func (analyzer *effectAnalyzer) bindingSlotType(name string) Type {
+	slotType, recorded := analyzer.compiler.FuncCache[analyzer.funcNameMangled].Vars[name]
+	if !recorded {
+		panic(fmt.Sprintf("internal: target %s of %s has no recorded slot type", name, analyzer.funcNameMangled))
+	}
 
-	return seeds
+	return slotType
 }
 
 func (analyzer *effectAnalyzer) deriveStatements(statements []ast.Statement, initiallyDefined map[string]struct{}) map[*ast.LetStatement]StatementEffect {
@@ -521,7 +545,6 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 	for _, expr := range stmt.Value {
 		yields := analyzer.deriveExpr(expr)
 		maySkip := len(stmt.Condition) > 0 || analyzer.expressionUsesLocalDomain(expr)
-		calleeSeeds := analyzer.calleeSeedEffects(expr)
 
 		for slot, yield := range yields {
 			index := targetIndex
@@ -536,7 +559,7 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 				result.ReadsSeed = append(result.ReadsSeed, index)
 				yield = seededYield
 			}
-			if calleeSeeds != nil && calleeSeeds[slot] == MaySeedRead {
+			if analyzer.calleeReadsSeed(expr, slot, target.Value) {
 				result.CalleeReadsSeed = append(result.CalleeReadsSeed, index)
 			}
 			result.Writes = append(result.Writes, TargetWriteEffect{
diff --git a/compiler/effects_test.go b/compiler/effects_test.go
index 1f8ee0be..c8ce62c8 100644
--- a/compiler/effects_test.go
+++ b/compiler/effects_test.go
@@ -821,3 +821,36 @@ existing, empty, fresh`)
 	require.Empty(t, fresh.ReadsSeed)
 	require.Equal(t, []int{0}, fresh.CalleeReadsSeed)
 }
+
+func TestCalleeSeedReadRequiresCompatibleStorage(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "storageSeedEffects", "", mustParseCode(t, `s = ReadStatic(n)
+    s = n > 0 "x"
+    "seen <-s>"
+    s = "done"`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `static = "hi"
+static = ReadStatic(0)
+heap = "never" ⊕ "read"
+heap = ReadStatic(0)
+static, heap`)
+
+	requireBodyEffects(t, cc, "ReadStatic", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+
+	// A static destination shares the callee's storage, so its value seeds
+	// the callee's staging slot and is read there.
+	static := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, static, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, static.ReadsSeed)
+	require.Equal(t, []int{0}, static.CalleeReadsSeed)
+
+	// A heap destination gets an ABI-typed zero seed instead, so nothing of
+	// the destination reaches the callee and no read is recorded.
+	heap := scriptStatementEffect(t, ts, 3)
+	requireTargetEffects(t, heap, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, heap.ReadsSeed)
+	require.Empty(t, heap.CalleeReadsSeed)
+}
diff --git a/docs/Pluto Effects and Follow-up Plan.md b/docs/Pluto Effects and Follow-up Plan.md
index 6e1a69d2..5ae9ec51 100644
--- a/docs/Pluto Effects and Follow-up Plan.md	
+++ b/docs/Pluto Effects and Follow-up Plan.md	
@@ -111,8 +111,10 @@ discipline. Unknown analysis must not silently mean no seed reads.
   reads, and zero/one/many-iteration cases are covered.
 - [x] Fresh targets, discards, incompatible-storage zero seeds, caller argument
   failure, and caller-side retention keep their existing distinct behavior.
-- [x] CFG and PIR consume settled solver facts rather than independently
+- [ ] CFG and PIR consume settled solver facts rather than independently
   rediscovering dependencies. Existing unused-write diagnostics still work.
+  PR #102 covers the CFG; PIR does not route calls yet, so its consumption of
+  `BodySeedEffects`/`CalleeReadsSeed` is owed by Step 4 call routing.
 - [x] Direct and indirect calls preserve staging and alias-input regressions.
   Public symbols and prototypes do not change with body effects; every public
   direct scalar return retains its existing hidden seed parameter.
diff --git a/docs/Pluto IR Plan.md b/docs/Pluto IR Plan.md
index 8bfe7843..95480c8f 100644
--- a/docs/Pluto IR Plan.md	
+++ b/docs/Pluto IR Plan.md	
@@ -911,9 +911,14 @@ function-owned `Range` domain needs no special case: the first iteration is
 the body, and a zero-iteration call is already resolved at the boundary.
 
 At a call site the callee's fact composes into `StatementEffect.CalleeReadsSeed`
-for every named target, whatever the ABI: an indirect output reads its
-destination-seeded staging slot exactly as a direct return reads its hidden
-seed parameter. Only boundary resolution is direct-ABI specific. A fresh
+whatever the ABI, but only when the seed reaches the callee: an indirect
+output reads its destination-seeded staging slot exactly as a direct return
+reads its hidden seed parameter, and lowering seeds that slot from the
+destination only when the two storage types are identical
+(`makeCallOutputAdapters`). A mismatched flavor — a `StrH` destination for a
+`StrG` output, say — gets an ABI-typed zero seed, so the callee never observes
+the destination's value and no read is recorded; the prior value stays an
+overwrite candidate. Only boundary resolution is direct-ABI specific. A fresh
 destination supplies a zero seed, so the CFG emits a read only for a defined
 binding, while the enclosing body's fold treats a call at a not-yet-replaced
 output as a read of that output.
diff --git a/tests/seed/seed_read.exp b/tests/seed/seed_read.exp
index 65475692..127c316c 100644
--- a/tests/seed/seed_read.exp
+++ b/tests/seed/seed_read.exp
@@ -12,3 +12,8 @@ Many: 23
 ManyFresh: 3
 Tag: hi!
 TagWritten: x!
+seen <hi>
+Static: done
+neverread
+seen <>
+Heap: done
diff --git a/tests/seed/seed_read.pt b/tests/seed/seed_read.pt
index 5c3a17e1..f4530ae1 100644
--- a/tests/seed/seed_read.pt
+++ b/tests/seed/seed_read.pt
@@ -29,3 +29,8 @@ y = AccRange(r)
 s = MaybeTag(n, t)
     s = n > 0 t
     s = s ⊕ "!"
+
+s = ReadStatic(n)
+    s = n > 0 "x"
+    "seen <-s>"
+    s = "done"
diff --git a/tests/seed/seed_read.spt b/tests/seed/seed_read.spt
index 90fd29b7..ef10e1ef 100644
--- a/tests/seed/seed_read.spt
+++ b/tests/seed/seed_read.spt
@@ -34,3 +34,10 @@ tag = MaybeTag(-1, "x")
 tagWritten = "hi"
 tagWritten = MaybeTag(1, "x")
 "TagWritten: -tagWritten"
+static = "hi"
+static = ReadStatic(0)
+"Static: -static"
+heap = "never" ⊕ "read"
+heap
+heap = ReadStatic(0)
+"Heap: -heap"