Pre-phase design — Provenance Propagation

Status: DECISIONS RECORDED — revised 2026-05-12 after slice-2 recon (see “Design correction” below). Slice 0 of the Provenance Propagation phase. CTO delegated the scope call; this doc is the contract the multi-tier work executes against. Same role runtime-split-design.md played for 33J7b.

Filed: 2026-05-12. Revised: 2026-05-12 (slice-2 recon corrected a load-bearing premise — D1, D5, R6, and the slice plan changed; the original framing is preserved struck-through where it matters so the correction is auditable).

Origin: the corvid-differential-verify test corpus_scan_includes_deliberate_failure is red. Investigation traced it to a real tier-soundness divergence and tests/corpus/combined_all.cor has been byte-identical since Phase 20g, where it was committed as a program that should agree across all four tiers. The CTO call: don’t paper over it — close it as an invention, not a fix.

The slice-2 recon pass falsified this doc’s original premise before any code was written. What the original draft assumed: the typechecker sees Grounded<String> for a data: grounded prompt’s return and accepts String + Grounded<String> via the “legacy compatibility” assignability rule at types.rs:153-156.

What the recon found: Type::Grounded is only ever constructed from an explicit Grounded<T> type annotation a user writes by hand (checker/expr.rs:536, checker/types.rs:261). There is no path from a data: grounded effect to Type::Grounded in the checker. So:

audit() -> String uses audit_effect (effect carries data: grounded) returns plain Type::String to the typechecker. The grounding lives only in the effect row, never in the type.
first + second in combined_all.cor is String + String to the checker → it typechecks clean (confirmed: differential-verify’s error is “interpreter run failed”, not “typecheck failed” — so typecheck passed).
At runtime the interpreter wraps audit()’s result in Value::Grounded because of the effect → eval_arithmetic sees Value::String + Value::Grounded → TypeMismatch.

The divergence is not “checker permissive, interpreter strict.” It is the checker and the runtime disagree about whether the value is grounded at all. The type system is unsound here — it says String where the runtime produces Grounded<String>.

Consequence for the moat. @grounded_pure (D6) needs the compiler to reason about grounded-ness. A grounded-blind checker can never prove “no laundering.” So the real fix is not “teach the interpreter to tolerate Value::Grounded” (that would be Design Y — the rejected shortcut, since it leaves the moat impossible). The fix is Design X: make data: grounded a type-system property — a prompt/tool/agent whose effect row carries data: grounded returns Type::Grounded<T>. CTO call (delegated 2026-05-12): Design X, it is the only design that fixes the soundness hole and enables the moat. D1, D5, R6 and the slice plan below are revised accordingly.

The problem, precisely (revised)

Grounded<T> is Corvid’s provenance-carrying type — a value plus a ProvenanceChain proving where it came from. Today:

Typechecker is grounded-blind for effect-induced grounding. data: grounded never produces Type::Grounded; only an explicit Grounded<T> annotation does. The types.rs:153-156 “legacy compatibility: Grounded assignable to T” rule exists but only fires for hand-annotated grounded values — it is not what lets combined_all.cor pass (that passes because the checker never sees grounding at all).
IR lowering (corvid-ir/src/lower.rs:1172-1187) only emits UnwrapGrounded for an explicit .unwrap_discarding_sources() call. Implicit Grounded<T> → T coercions produce no IR node.
Interpreter (corvid-vm/src/interp/expr.rs) — eval_arithmetic pattern-matches concrete Value::Int/Float/String/List. A Value::Grounded falls through to TypeMismatch.
Native codegen / replay — the UnwrapGrounded IR node is handled, but since lowering never emits one for implicit coercions, those tiers face the same raw-grounded-operand gap.

The gap: data: grounded is a runtime-value fact the type system cannot see, so the four tiers cannot be made to agree on it — and the moat cannot be built on a fact the compiler is blind to.

The reframe: invention, not fix

A fix makes the tiers agree. An invention makes grounded values do something no other language or framework can. The phase ships:

Provenance Propagation — Grounded<T> is contagious through every operator, preserved end-to-end across all four tiers, and never silently dropped. The compiler can prove a boundary launders nothing.

The principled core: Grounded<T> is an applicative functor and provenance-merge is its monoid. State that law once and every pure operation lifts for free — it is one algebra, not a pile of per-operator special cases.

The pitch: in Corvid, “did this value come from an AI, how was it computed, and how confident is it” is a compile-time-decidable property that survives every operation. You cannot accidentally launder a model output into trusted data.

Scope — what ships, what defers

CTO call (delegated 2026-05-12). Ship the moat with discipline; do not bundle three inventions into one phase on an already-slipped launch track.

Ships in this phase:

Base contagion — Grounded<T> contagious through all operators (arithmetic, concat, comparison), all four tiers.
@grounded_pure — the compiler-enforced no-laundering boundary. The moat.
The Derived provenance representation — base contagion uses it from day one so how-provenance’s data model ships with the base and no migration is needed later.
The invention-shipping contract (README / tour / inventions.md / spec / tests).

Defers to follow-up phases (sequencing, not shortcutting — each ships fully later):

Pillar 1 polish — how-provenance DAG rendering. The Derived data ships here; the rich corvid trace dag rendering of the operation tree is a follow-up.
Pillar 2 — compile-time confidence budgets. Runtime confidence composition ships here (it has to — GroundedValue carries a confidence field). Compile-time @confidence(>= X) enforcement through arithmetic, and the question of whether * deserves a composition rule other than Min, is its own focused phase.

Decisions

D1 — Grounding is a type-system property + the contagion law (revised 2026-05-12)

Decision, part A — data: grounded produces Type::Grounded<T> (Design X). A prompt / tool / agent whose effect row carries data: grounded has its declared return type T wrapped to Type::Grounded<T> by the checker. The type system stops being blind to effect-induced grounding; the checker, interpreter, native codegen, and replay finally agree on which values are grounded. This is the soundness fix the recon surfaced as mandatory — without it the contagion law has nothing to operate on and @grounded_pure (D6) is uncheckable.

Decision, part B — the contagion law (uniform, all operators). Any operator application with at least one Grounded operand produces a Grounded result. No exceptions:

Grounded<T> ⊕ T → Grounded<T>
T ⊕ Grounded<T> → Grounded<T>
Grounded<T> ⊕ Grounded<T> → Grounded<T>
comparisons: Grounded<T> ⊗ T → Grounded<Bool> (and the two other operand shapes)

⊕ ranges over arithmetic (+ - * / %) and string/list concat; ⊗ over comparisons (== != < <= > >=). && / || are short-circuit and out of scope (they already route specially).

Ordering note. Parts A and B are coupled: shipping A without B would break combined_all.cor at the checker — check_binop matches concrete Type::Int/Type::String arms, so a Type::Grounded operand would fall through to its error arm. B (contagion in check_binop / check_unop) must land first (dormant — nothing produces Type::Grounded from effects yet), then A activates it. Both are corvid-types changes; the slice plan lands them as one slice for that reason.

Why uniform. A per-operator carve-out is the pile-of-special- cases anti-pattern. The applicative-functor framing demands one law. A stated law that the implementation only partially honors is exactly the spec/behavior drift the project forbids — so the phase implements the complete law, comparisons included.

D2 — `Grounded<Bool>` in control-flow conditions

Decision. if / while / match conditions accept Grounded<Bool>. The branch decision implicitly unwraps the bool — this implicit unwrap is recorded (the trace shows “branch taken under grounded condition”) and is IR-visible (see D5). It does NOT violate @grounded_pure: branching consumes the bool to pick a path, it does not emit a laundered value; the returned value’s provenance still tracks through whichever branch produced it.

Why. Contagion that stops at control flow is not contagion. “This code path was taken because of an AI output” is precisely the kind of fact provenance should capture. “Powerful, not powerless” — grounded values stay usable in control flow.

D3 — The `Derived` provenance representation

Decision. Add a fifth ProvenanceKind variant:

ProvenanceKind::Derived {
    op: String,                  // "add", "concat", "lt", ...
    inputs: Vec<ProvenanceChain>, // recursive — a real tree
}

When an operator produces a grounded result, the result’s ProvenanceChain is a single ProvenanceEntry whose kind is Derived { op, inputs }. inputs holds the operand chains in operand order; an ungrounded operand contributes an empty ProvenanceChain (self-describing as “(ungrounded)” to renderers — no new Literal variant needed).

Mechanical consequence — shipped in slice 1. ProvenanceKind derived Eq; ProvenanceChain / ProvenanceEntry did not. The recursive Vec<ProvenanceChain> payload needs the whole tree Eq. Slice 1 added Eq to the chain types — sound because they carry no floats (confidence lives on the VM’s GroundedValue, not core’s ProvenanceChain). Also shipped: a ProvenanceChain::derived(op, inputs, timestamp_ms) constructor as the single mint point all four tiers call. ✅ Done — see slice 1 in the plan.

Why a tree, not a flat merge. ProvenanceChain already has a flat merge() — it stays, for cases that legitimately accumulate sources (agent handoffs). But operator results want how-provenance: the operation tree, not just the leaf set. Flat-merging at operator sites would lose which sources fed which operand — and recovering that later would be a representation migration. Shipping Derived now means how-provenance’s data model is permanent from day one; only the rich DAG rendering defers.

D4 — Runtime confidence composition: `Min`, uniform

Decision. A grounded operator result’s confidence = Min over the operands’ confidences; an ungrounded operand contributes 1.0. Uniform across all operators in this phase.

Why. GroundedValue already documents confidence as “composed via Min through the call graph” — this extends the existing, shipped rule to operators rather than inventing a new one. Whether specific operators (notably *, where independent confidences might multiply) deserve a different rule is the deferred Pillar 2 design question. Using the shipped rule is not a shortcut; refining it is the deferred pillar’s job, and refining it later is non-breaking (it only tightens runtime confidence values, never types).

D5 — The legacy `Grounded<T> → T` rule: load-bearing now, keep it, make it visible (revised 2026-05-12)

Decision. Keep the types.rs:153-156 legacy assignability rule. Under Design X (D1 part A) it is no longer “legacy cruft to retire” — it is load-bearing: when data: grounded starts producing Type::Grounded<T>, every existing consumer of a grounded prompt/tool result suddenly sees Grounded<T> where it saw T. The legacy rule is what keeps that from breaking every program — it lets Grounded<T> keep flowing into T positions (return, args, bindings, struct fields). Removing it would turn Design X into a workspace-wide breaking change. It stays.

But it must not stay invisible. Make every implicit Grounded<T> → T coercion IR-visible: when the legacy coercion fires, IR lowering inserts an explicit discard node (reuse UnwrapGrounded, or a dedicated CoerceGroundedDiscard — slice 3 decides which is cleaner). Operator operands do not need this — D1’s contagion law covers them (the result stays grounded; nothing is dropped).

Consequence:

Normal agents: implicit coercion still compiles and runs. Near-zero blast radius on existing code — the coercion still works, it is just no longer invisible. (Exact blast radius is measured in slice 2 — see R6.)
@grounded_pure agents: the checker sees the discard node and refuses to compile (D6).
The provenance drop becomes greppable in the IR and visible in traces — closing the “silent” part of the gap without a breaking removal.

Why. This is the powerful-and-safe resolution. Removing the rule outright (the option the chat rejected as “powerless”) would now — post-Design-X — be a workspace-wide break, not just “ceremony on existing code.” Keeping it invisible (the rejected “shortcut”) leaves silent laundering. Keeping it visible gives normal code its ergonomics back AND gives @grounded_pure something concrete to forbid AND makes every drop auditable. Best of three.

D6 — `@grounded_pure` — the moat attribute

Decision. A new agent attribute, sibling of @deterministic / @replayable. @grounded_pure agent foo(...) compiles iff the checker proves foo’s body contains no provenance-stripping site: no UnwrapGrounded node and no implicit-coercion discard node (D5) is reachable. It is a reachability check over the IR — the same proof shape @deterministic already uses for “no nondeterministic source reachable.”

Composition with sibling attributes is orthogonal: an agent may be any subset of @deterministic / @replayable / @grounded_pure; each is an independent proof obligation. @grounded_pure says nothing about determinism and vice versa.

Why this is the moat. Base contagion alone is “provenance propagates” — nice. @grounded_pure makes it load-bearing: mark a boundary and the compiler guarantees no AI output is laundered into trusted data across it. That is the approve-moat shape — a compile-time refusal — applied to data flow. It is the most on-thesis thing in the whole set, and it is cheap once contagion and D5’s visible-discard node exist.

D7 — `combined_all.cor` becomes idiomatic

Decision. Change tests/corpus/combined_all.cor’s main() signature from -> String to -> Grounded<String>. The program genuinely produces a grounded value (audit() is grounded, + propagates per D1); the signature should say so. The corpus shows idiomatic Corvid. The legacy-coercion-discard path (D5) gets its own dedicated fixture rather than being demonstrated ambiguously by combined_all.cor.

D8 — Effect rows unchanged

Decision. Contagion is a type-and-value-level property. It does not alter effect rows. data: grounded on an effect is what originates a Grounded<T> value; operator contagion propagates it downstream. The agent’s effect profile — what the differential- verify tool compares across tiers — is unchanged by this phase. The tiers must agree on types and values, which is what D1–D6 deliver.

Risk mitigations

R1 — native codegen is the hardest tier. Grounded values through the C ABI. Mitigation: the corvid-differential-verify 4-tier check IS the mitigation — if native diverges from interpreter, the tool catches it. Slice 5 is gated by re-running the differential verifier; native ships only when it agrees with interpreter byte-for-byte.
R2 — recursive Derived chains grow with expression depth. Mitigation: depth is bounded by source expression nesting — not unbounded. Note it; do not optimize during the feature. If it ever becomes a perf problem, that is a separate, measured slice.
R3 — the Grounded<Bool> control-flow cascade may ripple wider than expected. Mitigation: sequence it (slice 6) behind the load-bearing arithmetic/concat slices. If it ripples past its slice, it splits — it does not block the rest of the phase.
R4 — D5’s visible-discard change could surface existing silent coercions. Mitigation: the slice-7 discard node is additive — the coercion still compiles and runs, it just gains an IR node. Only @grounded_pure agents are affected, and there are none until slice 8. Confirmed by the full workspace test run + corpus baseline staying green through slices 3–7.
R5 — @grounded_pure interaction with @deterministic / @replayable. Mitigation: D6 specifies orthogonal composition up front; slice 9 includes a test matrix over the attribute subsets.
R6 — Design X blast radius (added 2026-05-12). Making data: grounded produce Type::Grounded<T> means every consumer of a grounded prompt/tool result now sees Grounded<T>. The legacy rule (D5) absorbs most positions (return / args / bindings / fields — anything governed by is_assignable_to). The positions it does NOT absorb are operator operands (check_binop / check_unop match concrete arms) — which D1 part B covers — and any position with a hard concrete-type match elsewhere in the checker. Mitigation: slice 2 includes an explicit blast-radius measurement — after wiring Design X, run the full workspace test suite + verify --corpus + every examples/ program, and enumerate every new failure. The expectation is that legacy-rule
- D1-contagion cover essentially all of it and the residue is a countable handful of sites needing explicit Grounded<T> annotations or .unwrap_discarding_sources(). If the residue is large or structural, slice 2 stops and the phase re-scopes — that is the recon gate, not a thing to patch around.

Slice plan

One commit per slice. Validation gate between every commit (workspace check + targeted tests + corvid-runtime-core wasm32 build + corpus baseline). Push every slice. Wait for acknowledgement at slice boundaries.

Slice 0 — design doc. This document. Commit: docs(grounded-prop-0): record provenance-propagation design.
Slice 1 — Derived representation. ✅ shipped. ProvenanceKind::Derived { op, inputs: Vec<ProvenanceChain> } landed in corvid-runtime-core/src/provenance.rs. Eq added to ProvenanceChain + ProvenanceEntry (the recursive tree needs it; no floats in core’s chain types so total equality is sound). ProvenanceChain::derived(op, inputs, timestamp_ms) constructor — the single mint point all four tiers will use. 5 round-trip tests (incl. recursive-tree survival + empty ungrounded-operand chain + Eq). Gate green: wasm32 build clean, core 20/20, runtime 257/257, workspace check clean, corpus baseline unchanged.
Slice 2 — typechecker: contagion law + Design X (revised 2026-05-12). corvid-types, landed in two coupled steps within one slice per D1’s ordering note:
- 2a — contagion law, dormant. ✅ shipped. check_binop / check_unop strip Grounded<> from operands, run the normal rule on the inner types, re-wrap if any operand was grounded (ungrounded() helper). Mid-slice finding: the contagion law has a second enforcement site in the checker — the provenance-reachability analysis effects/grounded.rs:: expr_is_grounded, which proves a -> Grounded<T> agent’s return actually traces to a data: grounded source. Its _ => false arm swallowed BinOp / UnOp, so a grounded operand’s grounding did not reach the return. 2a fixes both halves: the type rule and the reachability walk. && / || scoped out of both (D1). 8 checker tests (every operand shape + a conditional-not-blanket guard + an ordinary-arithmetic regression guard); each positive test fails without 2a. Dormant confirmed: full workspace test sweep stays green except the one pre-existing corpus_scan_includes_deliberate_failure (the failure this phase exists to fix — unchanged).
- 2b — Design X. ✅ shipped. The EffectRegistry is now built before the main check pass and threaded into Checker (it was built only for the post-passes before). check_tool_call / check_prompt_call / check_agent_call call ground_if_effect_grounded: if the callee’s effect row carries data: grounded, the call-site return type is wrapped to Type::Grounded<T> (already-grounded returns are not double-wrapped). A shared effect_row_is_grounded helper was extracted in effects/grounded.rs (one source of truth, also used by the reachability analysis). 2 Design-X tests added (effect-induced grounding via a non-retrieval user effect + a conditional guard).
- 2c — blast-radius measurement (R6). ✅ ZERO residue. cargo check --workspace --tests: 0 errors. cargo test --workspace --lib: only the pre-existing corpus_scan_includes_deliberate_failure red (unchanged — goes green at slice 10). corvid-types: 222/222. verify --corpus: baseline unchanged. Every examples/*.cor clean except refund_bot.cor, which fails identically on HEAD (pre-existing python import effect-constraint issue, unrelated to grounding). The legacy rule (D5) + 2a’s contagion law absorbed the entire blast radius — not “a countable handful,” nil. R6’s stop-and-rescope gate does NOT trigger.
Slice plan reshaped (2026-05-12, after slice-3 recon). The recon found two things: (1) “operator nodes carry grounded-result info” is already done — IrExpr carries ty: Type and lower_expr copies it from the typechecker’s self.types, which slice 2 made contagion-aware; nothing to build. (2) The D5 discard node is real work (~4 coercion-site categories — return / call-args / typed-bindings / struct-fields — and lowering has no central coercion point today), but it is a @grounded_pure prerequisite, not an execution prerequisite: slices 4/5/6 (interpreter / native / control-flow) do not need it (combined_all.cor runs once eval_arithmetic handles Value::Grounded operands — the runtime does not type-check returns). So D5 moves to its own dedicated slice adjacent to its only consumer. Decisions D1–D8 untouched; execution ordering now tracks the real dependency graph. Phase grows 11 → 12 slices.
Slice 3 — IR carries grounded-result info (verification). ✅ shipped. corvid-ir: 2 lowering tests confirming slice 2’s contagion law flows end-to-end into IrExpr.ty — a contagious operator’s IR BinOp node has ty: Grounded<Int>, an ordinary one keeps the plain inner type. The IR-tier checkpoint. No production code: lower_expr already copies the typechecker’s per-span type into IrExpr.ty, so slice 2’s contagion result flows in for free; this slice proves it and guards against regression. Gate green: corvid-ir 34/34, workspace check clean, wasm build clean, corpus baseline unchanged.
Slice 4 — interpreter. ✅ shipped. corvid-vm: a single contagion lift at the top of eval_binop — if either operand is Value::Grounded, strip the wrappers (unwrap_for_op, fully recursive), run the normal operator on the inner values, re-wrap with the Derived chain (D3) and Min confidence (D4). Applicative-functor framing: arithmetic, equality, and ordering all lift through the one site. 4 unit tests + full workspace sweep green.

Finding — corpus_scan_includes_deliberate_failure went green here, not at slice 10 as the plan predicted. Why: that test was red because verify_corpus aborted the whole scan when the interpreter run of combined_all.cor crashed (the original eval_arithmetic TypeMismatch). The test only ever needed the interpreter crash unblocked — not all four tiers. The differential verifier compares effect profiles, and per D8 contagion does not touch effect rows, so once the interpreter run completes, all four tiers agree on combined_all.cor’s profile. This does not mean the phase is done: the test going green is a weaker property than “the contagion law executes correctly on all four tiers.” Native codegen producing correct grounded values (slice 5), control-flow (6), the @grounded_pure moat (7–9), the D7 fixture (10), and the invention contract (11) are all still required deliverables — the profile-level differential verifier simply does not exercise them.
Slice 5 — native codegen: value-correctness (reshaped 2026-05-12 after recon; CTO decision). Recon found the native grounded model is structurally degenerate: a Grounded<T> is a bare machine value (grounded_attest_* returns value_ty unchanged, registering provenance into a single global “last scalar attestation” slot). It has no per-value provenance tracking, so it cannot build the byte-identical Derived tree the contagion law (D3) requires — that needs grounded values to carry runtime identity (handles), a native-ABI rework rippling through native codegen + the C runtime + the attestation store + possibly the Phase 22 FFI surface. That is phase-sized, and per CLAUDE.md needs its own pre-phase design chat.

CTO decision: honest sequencing, not a shortcut. Slice 5 ships native grounded-scalar value-correctness. ✅ shipped.

Recon during execution sharpened the scope. The initial plan was “strip Grounded<> before all native operand-routing decisions.” Two of those landed cleanly; one did not:
- ✅ is_wrapping_int_binop / is_wrapping_int_unop (corvid-ir) were grounded-blind — under @wrapping, a grounded-Int operator lowered to the overflow-trapping BinOp instead of WrappingBinOp. Fixed with the shared Type::ungrounded() method. Grounded scalars (Int/Bool/Float) are now value-correct at native — and they were the only cleanly-tractable case, because scalars are not refcounted, so there is no ownership entanglement.
- ❌ The BinOp string-routing fix (matches!(left.ty, Type::String) → see through Grounded) produces correct values but leaks: the dataflow / dup-drop passes treat Grounded<...> as opaque (ownership::is_refcounted returns false for it — deliberately; making it see through Grounded double-frees, proven by a broken parity test). So grounded-refcounted-type (String / List / Struct) operator value-correctness is entangled with the native grounded ownership model — the same model the follow-up phase reworks. Reverted; the string-routing site keeps a NOTE comment recording why it is deliberately grounded-blind.
Net slice-5 scope: grounded-scalar value-correctness (the @wrapping IR fix) + the shared Type::ungrounded() method (used by checker/ops.rs, corvid-ir, and available to corvid-codegen-cl). Grounded-refcounted-type operator value-correctness joins the native grounded-handle rework in the native-grounded-handles follow-up phase — an #[ignore]d grounded_string_concat parity test is filed as that phase’s executable spec. Verified by corvid-ir unit tests + the pre-existing grounded parity tests staying green (the profile-level differential verifier does not catch grounded-value correctness — see the slice-4 finding).

The native grounded-handle rework — per-value provenance, the Derived DAG at native — is a dedicated follow-up phase, with a pre-phase stub at docs/meta/native-grounded-handles-design.md. The “all four tiers” acceptance criterion is amended accordingly: native is value-contagious in this phase; native’s provenance-DAG-through-operators is the follow-up phase’s deliverable.
Slice 6 — control-flow conditions. ✅ shipped. Recon found Corvid has only Stmt::If (and Stmt::For, but for iterates, not Bool-conditions); while and match/when don’t exist as stmts — D2’s “if/while/match” was partially aspirational. Slice 6 covers every Bool-condition site that exists today:
- Typechecker Stmt::If (checker/stmt.rs) and eval-decl assert <expr> (checker/decl_eval.rs) now use cond_ty.ungrounded() so Grounded<Bool> flows through.
- Interpreter require_bool strips Value::Grounded recursively (the centralised Bool-extraction helper); the if-stmt evaluator refactored to call require_bool instead of its inline grounded-blind match (DRY).
- Native: no change needed. Grounded<Bool> is machine-identical to Bool (a bare i8), Bool is not refcounted (no ownership entanglement like slice 5’s refcounted-type case), and brif on a bare bool already works.
- 1 corvid-types test (if_condition_accepts_grounded_bool) + 1 corvid-vm test (require_bool_strips_grounded_for_control_flow). Workspace sweep stays 0 failures.
D2’s “recorded + IR-visible” condition-unwrap defers to slice 7: the trace event + the IR-visible discard node ride on D5’s general discard-node mechanism, which slice 7 ships across all implicit-coercion sites (return / args / bindings / fields / conditions). Slice 6 makes the condition path work; slice 7 makes its drop visible for @grounded_pure (slice 9).

Out-of-scope follow-up: && / || operators still reject a Grounded<Bool> operand (the design doc’s existing non-scope for &&/|| contagion); if grounded_bool && other therefore still errors at the operator, not the condition.
Slice 7 — D5 discard node. corvid-ir: lowering inserts the visible discard node (reuse UnwrapGrounded or a dedicated CoerceGroundedDiscard) at every implicit Grounded<T> → T coercion site — return, call-args, typed bindings, struct fields. This is the @grounded_pure prerequisite: it makes every silent provenance drop greppable in the IR. Must be complete across all coercion sites or @grounded_pure (slice 9) is unsound.

Shipped 2026-05-15/16 as a sub-split (commits 6bad408, 942c7e7):
- 7a — typechecker side table. Checked.grounded_coercion_sites: HashSet<Span> populated by a record_if_grounded_coercion helper called at every value-flow is_assignable_to site: return / let-with-annotation / yield / call-arg / struct-field-init (free + imported) / Some(...) against an Option<T> expectation / list-element flowing into an inferred-bare element type / replay-arm + else-arm bodies / if-condition (D2 grounded-tolerant but still IR-visible). Operator unification and signature compatibility sites are intentionally NOT recorded — those aren’t value-flow sites. Test coverage pins exact-span equality at the four most visible sites so any new site added without a recorder call breaks the test, not the moat.
- 7b — IR insertion + runtime alignment. corvid-ir’s lower_expr wraps the produced IrExpr in IrExprKind::UnwrapGrounded at every recorded span. The inner expression keeps its Grounded<T> type; the wrapper carries the stripped inner type. Inserting the node surfaced a pre-existing soundness gap: the runtime only wrapped tool results in Value::Grounded when the literal effect name was "retrieval", but Design X (slice 2b) had promoted ANY data: grounded effect’s return to Type::Grounded. Closing the gap inside 7b (required by the validation gate):
  - IrTool.produces_grounded / IrPrompt.produces_grounded computed once at lower time via the now-public corvid_types::effects::effect_row_is_grounded helper.
  - maybe_ground_tool_result reads the field instead of name-matching "retrieval"; idempotent on already-Grounded values so adversarial double-wrap paths stay safe.
  - New maybe_ground_prompt_result mirrors the tool path for non-stream prompt finalisation in corvid-vm::interp::prompt::finalize_prompt_result. Stream prompts are explicit non-scope here — chunk-by-chunk grounding is a larger contract.
  - UnwrapGrounded runtime semantics preserve confidence while discarding provenance: Value::Grounded(v, chain, conf) strips to bare v when conf == 1.0, otherwise re-wraps as Value::Grounded(v, EMPTY_CHAIN, conf). The split honours slice 7’s intent — “where it came from” is what’s being discarded; “how trusty it is” is a separate concern downstream confidence-gate checks still need. Defensive no-op on already-bare values keeps an out-of-sync tier from panicking the interpreter.
Slice 8 — @grounded_pure front end. corvid-syntax / corvid-ast / corvid-resolve: parse + represent + resolve the attribute.
Slice 9 — @grounded_pure proof. corvid-types / corvid-ir: the reachability proof obligation (D6) — no UnwrapGrounded and no slice-7 discard node reachable in a @grounded_pure agent’s body — plus the attribute-composition test matrix (R5).
Slice 10 — corpus fixtures (D7). combined_all.cor’s main() → -> Grounded<String> so the corpus shows idiomatic Corvid (the program genuinely produces a grounded value); new dedicated legacy-coercion fixture exercising the slice-7 discard node. Note: corpus_scan_includes_deliberate_failure already went green at slice 4 (see that slice’s finding) — this slice is now just the fixture work, not the test-revival.
Slice 11 — invention-shipping contract. README catalog entry, corvid tour --topic provenance-propagation demo, inventions.md proof-matrix row, spec section, learnings.md closeout, ROADMAP tick.

Estimated ~3 weeks. The phase is large because it is honest: a language capability that is not end-to-end across all four tiers is not shipped.

Invention-shipping contract (CLAUDE.md)

Provenance Propagation is a nameable Corvid capability. Before the phase closes, slice 11 must deliver:

README catalog entry — “Provenance Propagation” with the contagion law + the @grounded_pure guarantee.
corvid tour --topic provenance-propagation — a demo whose source compiles through the normal driver pipeline, showing Grounded<T> flowing through operators and a @grounded_pure boundary refusing a laundering attempt.
docs/reference/inventions.md row — shipped status, runnable command, test coverage, spec link, explicit non-scope (Pillars 1 & 2 deferred).
Spec section — defines the contagion law, the Derived representation, @grounded_pure’s proof obligation.
Tests — validate every claim the catalog entry makes.

Acceptance criteria for closing the phase

All 12 slices (0–11) on main.
Grounded<T> contagious through arithmetic, concat, and comparison — verified across checker, interpreter, and native (native = value-correctness; native’s byte-identical provenance-DAG is the native-grounded-handles follow-up phase per the slice-5 CTO decision). Replay consistency verified for the tiers in scope.
@grounded_pure compiles clean agents and refuses laundering agents; orthogonal composition with @deterministic / @replayable tested.
tests/corpus/combined_all.cor compiles + runs consistently across all four tiers; corpus_scan_includes_deliberate_failure green.
cargo test --workspace green; corpus baseline otherwise unchanged.
corvid-runtime-core still builds to wasm32-unknown-unknown (the Derived addition must stay wasm-clean).
Invention-shipping contract delivered (slice 11).
learnings.md + ROADMAP updated.

What’s out of scope

Pillar 1 polish — rich how-provenance DAG rendering in corvid trace dag. Data model ships here; rendering is a follow-up.
Pillar 2 — compile-time @confidence budget enforcement through arithmetic, and per-operator confidence-composition rules. Runtime Min composition ships here; the compile-time pillar is its own phase.
&& / || contagion — short-circuit booleans route specially today; folding them into the contagion law is a small follow-up if it proves worth it.
Performance — the Derived chain’s memory footprint is measured-not-optimized; a separate slice if it becomes real.