Backend selection & execution receipts

The v0.6 replacement-backend cutover (#652) introduces a second compiler backend: the Body IR replacement backend tracked by #653, alongside the current Rust-source-emission backend (IrCodegen in loaves/compiler/incan_emit/) that this document calls the legacy backend. #988 provides the first deliberately partial direct-execution profile. Every request still declares the intended backend, records the backend that actually ran, and refuses unsupported source visibly rather than quietly falling back to legacy. incan_emit::selection (#986) is the compiler-owned boundary that makes that possible.

This is a different axis from Oven's own receipt, described in Oven Alpha: Oven's receipt selects how an already-generated artifact is compiled (its legacy-Cargo-vs-direct-rustc build boundary), and never influences which compiler backend produced that artifact in the first place. Legacy builds hand generated source to Oven; the #988 direct replacement profile does not create generated source or an Oven plan.

The two records

BackendSelection is a versioned, content-identified record of what was decided before execution: the requested backend, its implementation revision, the compatibility profile it declares for this compilation, a content identity of the source being compiled, why that backend was selected (the compiler-owned default, or an explicit --backend request), and the declared fallback policy. It is built by select_backend before any codegen starts.

BackendExecutionReceipt is a versioned, content-identified record of what actually happened after execution: the backend that actually ran, whether a declared fallback occurred, the shadow-comparison outcome (always present and explicit, even when the comparison could not run), the diagnostic-contract version in force, and a content identity of the produced output. It embeds the BackendSelection it is bound to.

Both types are plain, I/O-free data — building and executing them does not touch IrCodegen or any other execution machinery directly. Both carry a content-derived sha256: identity, verified with verify_identity(), the same pattern Oven's own receipt uses: a later stage that only holds a serialized copy does not need to re-derive trust from the fields themselves.

No silent fallback

Every successful incan build exposes a selection and a receipt, including the default path: selecting the legacy backend with no flags produces an explicit selection_reason: "default" record rather than an implicit, unrecorded choice. A source-current completed-output reuse is eligible only when its immutable Loaf already carries and verifies that same implicit-default receipt; it republishes the verified receipt after materialization rather than inventing a new execution record.

The first #988 replacement profile produces a visible outcome, never a silent legacy execution:

• incan build --backend replacement --backend-fallback refuse creates one CompilationSession for the selected entry and the project's selected package-feature projection, then lowers only that session's projected AST and checked TypeCheckInfo Body-IR bridge. It directly executes an admitted zero-argument main; an admitted main may call permitted local-module functions and covered public declarations from built packages. Package calls consume the selected producer's published executable representation; their original source and generated Rust do not define a second execution route. The runtime never reconstructs a call from source or routes it through generated Rust, and an unsupported profile remains a visible refusal rather than a legacy fallback. Its receipt records executed_backend: "replacement", fallback_outcome: "not_needed", and an output identity over the actual Body-IR result, exact per-stream output bytes, and execution evidence; this path does not construct generated Rust or an Oven plan.

The direct JSON report and its persisted backend receipt both carry semantic_module provenance from that same analysis: the checked module id and module path, plus content identities for its source and semantic snapshot. The report's Body-IR snapshot, source spans, ownership reads, runtime requirements, and task lifecycle remain execution evidence for that selected semantic module; they do not widen the supported profile. - The supported profile is deliberately partial: scalar arithmetic, scalar local bindings, including compiler-resolved let/mut shadowing and reassignment through retained local identities, returns, compiler-owned string concatenation, normalized range/while branches and loops, assertions, and source-local recursive tuple/list values. Body IR retains an exact declaration-span identity for each same-module named call, so direct dispatch selects the typechecker-chosen sibling body rather than scanning by name; targets without a retained declaring identity refuse. It also admits a source-local, undecorated, non-generic plain model with no traits, methods, method aliases, partials, properties, or field aliases when every field is explicitly supplied with an already-admitted recursive structural value: execution verifies its declaration identity and canonical field layout before materializing a value, then permits one read-only named-field projection and an exact-identity match pattern using canonical named fields. Floats, callables, generator values, and nested nominal values are not structural model fields in this profile. Separately, it admits a source-local int or str value enum only when it is undecorated and non-generic, has no traits, methods, aliases, or payload fields, and every member carries a matching literal scalar: Body IR preserves exact enum and member declaration identities, materializes only that carrier, and exposes the raw scalar solely through the compiler-provided zero-argument .value() surface. It also admits a source-local, undecorated, non-generic fieldless normal enum with no value backing, traits, methods, aliases, or payload: direct execution materializes an exact unit-member carrier, permits equality or inequality between two carriers of that same retained enum identity, and dispatches exact-identity unit-member patterns when an identity-retained carrier reaches the match (for example through a same-module direct call). Intrinsic Result construction retains the checked Ok or Err variant and one admitted data payload; direct calls may return that carrier to a same-module caller, match may dispatch its one payload, and ? executes only when Body IR records an exact same-error-type route. Cross-error-type conversion, unresolved routing, imported or shadowed constructor spellings, nested Result carriers, and non-data payloads refuse at the original source span. Omitted model defaults, field writes, nested nominal values or projections, classes, generic or decorated models, traits, methods, aliases, payload enums, enum aliases, non-retained enum patterns, generated from_value lookup, custom enum methods, and Result conversions remain visible refusals. One numeric tuple-field projection, one integer list-index projection, and one list-index assignment are admitted; nested projection, slices, named projections outside that plain-model exception, and a selected-entrypoint aggregate output remain visible refusals. Source-local structural-list iteration and compiler-recorded range iteration remain admitted. The profile also admits compiler-selected global enumerate(list) over one checked structural-list operand, retaining zero-based (int, T) pairs, and compiler-selected global zip(list, list) over two checked structural-list operands, retaining exact (L, R) pair items. Structural leaves are int, bool, str, or unit recursively through tuples and lists, including typed empty lists. Zip evaluates its left operand before its right, pairs items in that order, and stops as soon as either list is exhausted. The checked global builtin target is required: a same-module declaration, imported spelling, unresolved spelling, or nominal iterator type never borrows this rule, and the profile does not admit general iterator dispatch. The compiler records the recognized range builtin as an explicit Body-IR target fact, while a same-module declaration named range has its own declaration identity and dispatches as that declaration; an imported or unresolved range never borrows the builtin rule. The profile also executes the admitted callable vocabulary retained in Body IR: captured local closures, partial presets, source-evaluable declaration defaults, identity-selected sibling-function calls, generator expressions and generator functions consumed by .collect(), plus their lazy .map() and .filter() adapters when their callbacks are admitted local callables. Generator frames resume from retained Body-IR state; adapters do not poll their source until collection consumes them. The compiler currently records adapter calls as positional method calls, which the runtime accepts only for the two-operand map/filter profile; it does not infer a general stdlib signature. The one async exception is private, unaliased top-level import std.async, which is syntax activation only: a source-local async def may construct an explicit direct task frame, and an async body may consume that frame only through a direct same-module await or a race for that constructs every arm before polling in source order, selects the first ready arm, and cancels every loser. Task construction, polling, suspend/resume, winner selection, and loser cancellation appear in the replacement JSON report's receipt-bound task_lifecycle evidence; a losing race-arm body never runs. Aliased, from, relative, absolute, package, Rust, provider, task-handle, timer, channel, method, closure, stored/repeated-await, and imported-call surfaces remain visible refusals or source-owned typecheck refusals. Package calls require declared executable coverage and an admitted body/value profile; coverage failures name the package and unmet requirement. Other unsupported imports, Rust interop, callable/default forms and general destructuring remain visible refusals. Repeated source spellings do not grant execution by themselves: admitted shadowing and reassignment consume the exact local identities already selected by Body IR. A refusal emits no new receipt; it does not remove a receipt written by an earlier successful build. Direct execution and its selection/execution receipts leave the #987 structural-value, nominal-value, enum-value, pattern, Result, and async rows non-green: #1154 and #1155 respectively own producing exact paired source-observable evidence through #1146's completed route before any parity claim can turn green. - Source-local sets and dictionaries admit hashed membership with checked int, bool, str, or unit keys, including typed-empty Set() and Dict() constructors. Dictionary membership tests keys rather than values. The four compiler-owned membership helpers use actual hash tables, and compiler-selected len returns the distinct set-entry or dict-key count after duplicate collapse. Container iteration, indexing, projection, mutation, equality, ordering, printing, formatting, and selected-entrypoint container results remain outside this profile. The same-source replacement-body-v0-020 case compares all four key kinds, ordinary output, and a separate boolean result; replacement-body-v0-026 separately compares populated, duplicate, and typed-empty entry counts with exact streams and an integer result. These bounded cases do not establish general collection parity. - Selected source-local string calls admit ordinary positional upper(), lower(), strip(), replace(old, new), join(parts), split() or split(separator), and contains(needle). String in uses the same normalized containment helper; not in remains outside this admitted helper profile. The typechecker retains the selected helper identity; direct execution consumes that identity and the existing shared string runtime. Named arguments, unpacked arguments, explicit type arguments, missing or inconsistent identities, and non-admitted methods refuse at their original call span. Case replacement-body-v0-021 compares the seven helpers and their assertion comparisons across independent routes with exact program streams and a separate boolean result. The unchanged examples/simple/strings.incn also executes directly, but this does not establish general string formatting or arbitrary-method parity. - Compiler-selected global len(value) and checked source-local value.len() count Unicode scalar values when value is a string. Both forms consume retained compiler identity, so a same-spelled source declaration or non-string helper does not borrow this rule. Case replacement-body-v0-024 compares both forms across five Unicode inputs with exact streams and a separate boolean result. This is not a byte count or grapheme-cluster count, and it does not widen the other bounded Len operand profiles. - Compiler-selected json_stringify(value) serializes only directly represented int, bool, str, and None values in this profile. It evaluates the operand once, preserves the shared runtime's exact escaping and Unicode bytes, and requires the retained builtin identity; a same-spelled source declaration keeps its lexical declaration behavior. Floats, lists, dictionaries, nominal values, and the broader serialization surface remain visible call-span refusals. Case replacement-body-v0-025 compares the exact returned JSON bytes and empty program streams through independent native and direct receipts; it does not make general JSON serialization parity-green. - The checked str, int, and float builtin identities have a separate scalar-conversion subset. A same-spelled source declaration retains its direct declaration identity; only the compiler-selected builtin target can enter this subset. It accepts ordinary int, bool, str, and normalized binary float values only where the selected conversion has a matching Rust-emission operation. Source literals and runtime int(str) or float(str) conversions consume one language-owned underscore-separator policy: a separator is valid only between ASCII digits, and normalization happens only after validation. A failed int(str) or float(str) reports the canonical ValueError, including the original unnormalized input, at the selected call span; a source-observable comparison retains that classified failure and its exact raw streams rather than calling it parity. - The #1279 typed-numeric carrier admits exact signed and unsigned widths, f32, f64, aliases resolved to those canonical numeric identities, and decimal[precision, scale] through checked literals and constants, locals, lossless widening, source-local call parameters and results, direct entry arguments and results, str, print/println, and Display f-strings. Decimal movement and Display preserve the checked precision, scale, coefficient, and written literal scale; decimal-to-int/float conversion is not admitted. Binary numeric int/float casts follow the existing native scalar-cast contract. Exact f32/f64 values are finite-only: native exact arithmetic validates each result before any later store, return, comparison, or output, and public direct and shadow carriers reject NaN and infinities before execution or source synthesis with the same canonical ValueError. This does not change ordinary float parsing, whose existing non-finite results and casts remain separately compared. Receipts and output identities bind the exact carrier, the direct JSON report names its result_type, and the source-observable comparison transports and validates that same result kind instead of widening it to int or float. Case replacement-body-v0-029 proves representative u8 minimum/maximum, i128 minimum, and u128 maximum endpoints, an f32 rounded value, fixed-scale decimal output, exact streams, and two independent route receipts. The direct carrier matrix separately covers minimum, maximum, and wrong-family validation for every sized integer kind; its out-of-range payload checks cover the narrower kinds for which the public carrier can represent a value beyond the target domain, while full-width i128 and u128 are bounded by their carrier representation. - Typed-numeric operations remain deliberately non-green. Arithmetic on exact-width and decimal carriers, their unary operations and resize methods, Debug formatting, aggregates and hashing, match/pattern use, iteration/generators, and other unproved builtin or method behavior refuse at the original source span before program output, naming #988 as the owner. Ordinary int/float scalar arithmetic remains admitted. This is an admitted exact-carrier-and-movement contract, not a claim of complete numeric execution. Package/import execution remains separately outside the profile under #989. - Compiler-selected bool(value) has a bounded truthiness subset for directly represented bool, int, str, list, set, and dict values. It observes zero and empty values as false and nonzero or nonempty values as true, evaluating the operand once. A source declaration named bool retains its own declaration identity and never borrows this rule. Float, tuple, bytes/frozen values, Option/Result, range/generator, nominal, custom __bool__/__len__, and implicit-condition coercion remain outside this subset. Case replacement-body-v0-027 compares exact streams and the separate boolean result across independent no-fallback routes; it does not make the broader numeric or aggregate feature parity-green. - Compiler-selected sorted(values) has a separate nonempty list[int] subset. It evaluates the list operand once, retains duplicates and negative values, returns a fresh ascending list with a new cursor, and does not mutate the source list. Empty lists refuse because this runtime carrier alone cannot distinguish an empty list[int] from another frontend-accepted ordering domain; booleans, strings/frozen strings, floats/NaN, frozen lists, nominal/custom ordering, keys/reverse, and arbitrary iterables remain outside the subset. Case replacement-body-v0-028 compares the exact output and an integer checksum that encodes both original and sorted order; it does not establish general aggregate or ordering parity. - Compiler-owned isinstance(value, Target) has a bounded int, bool, str, and ordinary binary float target subset when the checked value type is one of those scalars or a nonempty union containing only them. The typechecker retains that checked value type together with the alias-expanded target type, any proven nominal declaration identity, and the target expression's exact source span; Body IR carries a dedicated typed test, so the executor neither parses a type name nor materializes a runtime type value. Ambient and explicit std.builtins.isinstance(...) calls consume the same compiler-selected identity, while a source function named isinstance keeps its own direct-call identity. The boolean tags remain distinct (true is not an int). Unsupported nominal, generic, bytes/frozen, collection, numeric-width, decimal, Rust-interop, unknown, missing, or corrupted target evidence, and checked value types outside the bounded scalar/union set, refuse before effects at the retained target span or trusted call span as appropriate. Case replacement-body-v0-030 compares true and false union-member branches, direct expression use, the typed boolean result, and exact stdout/stderr across direct and native receipts. This is not general reflection or arbitrary runtime type-value support. Closed #1154 supplied the current direct nominal/value substrate; open #988 owns broader replacement execution, while package/import execution remains #989. - The #988 CLI surface accepts only --backend-fallback refuse. It has no receipt-bound legacy execution path for an unavailable source profile, so users must choose --backend legacy explicitly when the source is outside the profile.

A --shadow request on a build remains {"unavailable": {"reason": "..."}}, never "matched". The reason names the boundary: a build executes the module's main, and a program entrypoint's return value is not observable from the produced legacy process, so there is nothing for the two routes to agree or disagree about. It is deliberately non-green — generated-Rust token shape is not a semantic comparison. The comparison that does run is described in Source-observable shadow comparison below.

Any explicit backend request, fallback policy, or shadow request bypasses completed-output reuse and takes the source-based path appropriate to the declared backend. This prevents a cached default result from being presented as the outcome of a different declared selection.

Abs and Sum overflow behavior

Compiler-selected integer abs and builtin sum use checked arithmetic in every build profile. An unrepresentable result is a runtime failure rather than a wrapped value. Replacement execution retains the original builtin call span and any program output accepted before the failure; generated Rust uses explicit checked operations so Rust's debug/release overflow settings cannot change the result. This bounded contract does not yet define overflow for ordinary integer operators. Native and direct failure diagnostics can still differ on stderr, so a shadow comparison reports that diagnostic difference rather than calling it parity.

Provider-host availability

Embedders using provider-aware replacement preparation must supply a host for each admitted provider operation in the selected computation. Preparation checks the retained operation identity before program execution, including source defaults, stored closures, generator bodies, and identity-selected same-module callees. A missing host refuses at the original provider-call span before program output, provider invocation, or a successful execution receipt.

This check is conservative, not a liveness analysis: it inspects both branches, supplied-away defaults and unpolled frames without running them. It follows retained same-module call identities, including recursive calls, but does not scan unrelated functions or admit imported execution. Host availability is separate from authority: a matching host does not grant permission, and a governed denial still occurs at invocation through the existing authority and operation-receipt contracts. This does not add CLI provider configuration or a filesystem host.

Source-observable shadow comparison

The source-observable comparator observes one named free function in a source-only module, called with concrete scalar arguments. The driver's shadow_support module (loaves/compiler/incan_driver/src/shadow_support.rs) owns source-session and provider orchestration; loaves/compiler/incan_driver/src/backend/shadow/ owns the prepared-materialization comparison core. Its current profile is incan.shadow_comparison.direct_scalar_free_function.v2: checked arguments and results may be int, ordinary float, bool, str, None, an exact canonical sized numeric, or a checked decimal, and the source must fit the admitted direct-execution profile. Exact f32 and f64 arguments and results are finite-only in this public comparison carrier; ordinary float retains its separately compared parsing behavior. The typed report grammar records the exact result kind and validates its canonical range or decimal shape before comparison. A module containing main is outside this harness profile because the comparator supplies its own entrypoint. Direct rust::std::process imports are also outside the profile, keeping source exit behavior distinct from the harness's private transport-failure statuses. Printing is supported; it is not a reason to exclude a comparison.

Both routes observe that same source, independently:

• The replacement route typechecks the module, lowers it to Body IR, and executes the named function directly. It generates nothing and spawns nothing.
• The legacy route runs the module plus a generated Incan entrypoint that calls the same function with the same arguments and publishes a separate typed result file. That program goes through Oven, the adopted build and execution authority: IrCodegen emits Rust, an Oven receipt authorizes those exact bytes, an immutable direct-rustc plan selected from the bounded Oven store compiles them with no Cargo process, and the produced binary runs as a separate process.

What is compared is what the two routes did, never the Rust one of them was built from.

The result is transported losslessly

Neither program stream carries the function-result protocol. The Incan-authored entrypoint writes a typed report to a uniquely reserved workspace, then renames its staged file to publish the complete result. A successful process exit must provide that exact report; a failed process never contributes a partial result. Decoding checks the version and checked result kind without trimming whitespace or using lossy UTF-8 conversion. A string result ending in a newline therefore remains distinct from the same string without that newline.

A failed report write or rename returns unavailable without writing a transport diagnostic to either program stream. The harness uses private process statuses for these two failures and retains any output the source already produced; it does not misclassify report publication failure as a program assertion or arithmetic failure.

The legacy process's stdout and stderr are retained separately as raw bytes. The direct route uses explicit capture writers, so comparison does not leak program output into its caller's streams. This test capture does not change ordinary direct execution: CLI output is still delivered during execution, before receipt persistence.

What agreement is allowed to mean

Agreement requires the same typed return value or classified failure, plus byte-for-byte equality of stdout and stderr independently. Within-stream ordering and trailing newlines matter; no total order is inferred between the two streams. The recognized failure classes are assertion, division/modulo by zero, arithmetic overflow, and canonical int/float conversion failures. Unclassifiable or incomplete evidence remains unavailable.

Matching failure classes alone are insufficient. The current assertion and division failure checks preserve output printed before the failure on both routes, but report diverged: native execution emits a runtime diagnostic to stderr, while the direct execution API returns an error without emitting that diagnostic. These checks prove honest divergence reporting and output retention, not successful failure parity.

Every comparison records exactly one of three outcomes, and only the first is green:

• matched — both routes ran and produced the same outcome and exact per-stream bytes. Its summary names the outcome and each stream's length and digest; raw bytes remain in route evidence.
• diverged — both routes ran and produced different observables, with both sides named. This is a regression signal on the backend-selection axis, never a reason to prefer one route's answer.
• unavailable — no comparison was made, with the concrete boundary that stopped it. A legacy program that fails to build lands here rather than in diverged: a comparison that could not run has proven nothing, so build success is never allowed to stand in for a semantic verdict.

Both ran states record two profile facts. profile_kind names the comparison contract, currently incan.shadow_comparison.direct_scalar_free_function.v2; this version adds exact typed-numeric argument/result transport to the exact-stream comparison contract. profile_identity is the content identity of the exact instance: this source, this observed function, and these typed arguments. Recording only the hash would leave a consumer unable to identify the comparison contract; recording only the kind would let different executions claim the same evidence.

Receipts, and what survives an unavailable comparison

Each route that executed is selected and finalized through the same select_backend / resolve_execution / finalize_receipt sequence a build uses, and both are declared FallbackPolicy::Refuse, so neither route can quietly become the other. Both receipts carry the same source_identity and the same comparison outcome; they differ, correctly, in selected_backend, executed_backend, and output_identity, because each route's output identity covers what that route actually produced, including source-observable output. Treating the two receipts as interchangeable would erase the independence the comparison depends on.

The legacy route's output identity additionally covers the Oven authority that permitted the run — the project receipt identity, the reusable build-unit identity, the direct-rustc plan identity, and the produced output digest — so "which authority produced this legacy answer" is recorded rather than assumed.

An unavailable comparison does not discard work that really happened. When direct execution succeeds but the legacy route cannot run, direct execution keeps its own receipt and Body-IR evidence alongside the unavailable state. Accepted stream bytes also remain available when direct execution fails or its failure cannot be classified; those partial observations are not a successful execution result. A profile rejected before execution, such as a module containing main, runs neither route.

The same rule covers receipt finalization. If a route executed but its receipt could not be finalized, the comparison is no longer verifiable and the verdict is withdrawn to unavailable naming the failure — but the route's observation is still reported, because an execution that really happened must not disappear because its record could not be written.

Receipts recording a comparison use selection/receipt schema_version: 2. Version 1 could only ever record not_requested or unavailable, so no version-1 receipt carries a comparison payload.

Staging the legacy route

A source-observable comparison binds its named function's exact source identity to a caller-prepared source-session context before either route executes. That context retains the session's final SDK/provider plan and canonical Oven build-unit inputs. An Oven receipt's reusable build unit comes from build intent and those build-unit inputs, never from generated source, so the adopted staged receipt must have exactly the same inputs as the context before the comparison materializes its program and records new generated-source evidence. A different source, a missing source-session provider context, or mismatched build-unit inputs leaves the comparison unavailable before materialization or execution. The native route then requires an immutable direct-rustc plan already published by an explicit incan oven bake. A compatible context can still fail this later native-plan discovery; that is also unavailable and preserves any direct observation that actually completed. Neither case is approximated by invoking a compiler directly, because an unauthorized build produces a result no receipt can account for.

Because an unstaged run is honestly non-green everywhere, a default test run cannot tell a comparison that was never staged from one that was never implemented. make shadow-comparison-evidence closes that gap: it prepares the SDK providers, bakes a throwaway project with that same inventory to publish a plan, then runs the comparison, bounded list-iteration, and parity-corpus suites with INCAN_SHADOW_REQUIRE_LEGACY_ROUTE=1, so a missing or failing comparison is a hard failure rather than a reported skip. CI runs it as the Shadow comparison evidence (#1146) job and uploads the resulting parity summary.

CLI surface

incan build accepts three flags:

• --backend <legacy|replacement> — declare the backend for this build. Defaults to legacy.
• --backend-fallback <refuse> — declare that an unavailable backend must stop visibly. Omitting this flag means refuse.
• --shadow — request a comparison against the replacement backend alongside normal execution.

A successful build publishes its receipt to .incan/backend/receipt.json in the project root (parallel to Oven's own .incan/oven/receipt.json), and embeds it as the backend field of incan build --report json output. The #988 direct path has the explicit incan.replacement_execution.v1 report schema: alongside status, mode, and entrypoint, its replacement_execution payload projects the Body-IR result and exact result_type, exact stdout_bytes and stderr_bytes byte arrays, the completed-print emitted_output projection, receipt-bound output identity, snapshot, canonical ownership reads, runtime requirements, and a canonical task lifecycle array of every direct transition the execution observed. result remains the source Display spelling; result_type prevents an exact f32, u128, or decimal result from being mistaken for an ordinary float or int. Direct replacement execution writes program output to its ordinary streams immediately, and each print call flushes before execution continues. A later runtime or receipt-writing failure leaves prior output visible; it produces no new success receipt. --backend replacement --report json therefore requires --report-output <PATH> and is rejected before execution if that path is absent. Report metadata never occupies program stdout or redirects it to stderr. Embedders can supply their own stdout and stderr writers through ProgramIo and inspect accepted bytes even when execution returns an error. The task lifecycle is empty when no direct task was constructed; otherwise it records the observed construction, polling, suspend/resume, completion, winner, or cancellation transitions. A same-module task call that is constructed and dropped without being polled therefore records constructed only. It intentionally has no generated-artifact or Oven fields. An eligible completed-output reuse republishes its verified sealed receipt at the same path. Inspect a persisted receipt directly with:

incan inspect backend-selection --receipt .incan/backend/receipt.json
incan inspect backend-selection --receipt .incan/backend/receipt.json --format json

inspect backend-selection reads the receipt, calls verify_identity() on it (and, transitively, on the selection it embeds), and refuses to render a receipt whose recorded identity does not match its own content — the same tamper/staleness detection Oven's inspect oven performs on its receipt.

Provenance for Oven and other clients

Oven and other clients can key provenance on the pre-execution BackendSelection.identity and attach the post-execution BackendExecutionReceipt to their own outputs, without reading private HIR or Body IR structures: the receipt is a public, versioned projection of "what backend produced this," independent of how either backend represents a program internally. diagnostic_contract_version on the receipt ties it to the diagnostics schema (incan_syntax::diagnostics::stable::DIAGNOSTIC_SCHEMA_VERSION, in loaves/kernel/incan_syntax/src/diagnostics/stable.rs) in force when it was produced, so a consumer can tell whether a receipt's diagnostics are still interpretable under its own contract version.