Floor: a prepared EFFECT INPUT, acquired once and carried into nullary warm rows (PR two of the #10994 chain)

[gunbai-bot]

What this is

PR two of the #10994 chain: the floor gains a third fill disposition — a prepared effect input, acquired once and carried into a nullary warm row.

The gap, stated at the key rather than at taste

v2.workflow.floor_pure_producer_share admitted two dispositions and only two: a WARM row is nullary and preparation-forceable, a CLAIM-FORCED row has claim-shaped arguments and fills inside the fold. A producer whose value depends on one read of a committed carrier fits neither, and the reason is mechanical: a stored entry is keyed on (resolved fn node, portable argument row), and a nullary call that reaches a read contributes nothing about what it read to that key. Warming it would let two different carrier contents share one entry — the content form of the ctx-blind homonym class this file already refuses by resolving every spelling to a node. So such a producer could only be CLAIM-FORCED, where it re-derives once per claim frame: the rostered shared_precondition_re_derived_once_per_claim_frame.

The live instance is gunbc.roadmap_authority.roadmap_authority_projection — one Filesystem.Read of the acceptance-event carrier followed by a pure fold, demanded by seven required-lane claims and by #10994, whose merge path is blocked by an enrolment margin sitting on exactly this shared precondition.

Why carrying it is binding an input and not caching an effect

This is the whole licence for the row kind, and it is a fact of the existing substrate rather than a new assertion: hermetic evaluation already classifies this read as INPUT ACCESS. The checkout-input carve-out in v1_interpreter::eval_service_call dispatches a readonly Filesystem.Read/List wet when hermetic_checkout_input_disposition confirms the path under the checkout root, and refuses — typed and located — everything it cannot confirm (out-of-root, a .git/target component, unresolvable). The value is therefore a function of the commit the run prepared, and a producer reaching host state that wall cannot confirm is never carryable, because that wall refuses it first.

The shape

Two roster declarations beside the existing two lists, plus CarriedInputDependence = BoundParameter { parameter } | ImplicitAcquisition — two arms because there are exactly two ways a producer reaches the acquisition (taking it as an argument, which is where #11303 is moving the roadmap projections; or reaching it inside itself, which is the shape on main today).

Preparation gains one phase, ordered before the plain warm loop: resolve the acquisition to its node, refuse any acquisition that is not nullary, evaluate it once under observe_shared_build (so it is billed to preparation and adjudicated by the same preparation refusal as every other shared build), reify it totally to its portable form — the same total walk publication already performs — take its structural digest as the carried content identity, and bind it for the prepared subject's lifetime, cleared with the tier.

No stale serve is unwritable rather than guarded. The carried content IS the key material: a changed carrier produces a different portable argument row, the stored row fails to match, and the producer recomputes. There is no staleness check to forget to run.

The pure memo's effect_dispatch_count refusal is untouched — it is correct and stays. A prepared input is served by a different, roster-declared admission keyed on resolved fn-node identity, and it is served in eval_call rather than one tier down, because a declaration that reaches the world may declare uses and a fn with non-empty uses never reaches the pure path at all.

The effect wall on the implicit arm, which is what separates "its only input is this carrier" from "we hope it is": with the carry installed, the producer's warm must dispatch no effect. One that still reaches the world has an input the key does not represent, and the row is refused (PreparedEffectInputProducerStillDispatchesEffect) rather than stored under a key that cannot see what it read.

Adjudication, and the three conditions

Both decisions were sent as a model before any code (docs/plans/prepared-effect-input-carry.md) and approved by eager-raven-113, fierce-lark-661 and bright-boar-435 on 2026-09-14.

1. A domain refusal arm is carried faithfully. When the acquisition succeeds and returns its own coproduct's refusal, every claim receives the identical typed value it would have computed for itself — propagation, not widening: no claim passes where it would otherwise have failed. The floor stops the line only on evaluation failure, non-portability, non-nullary and unresolved rows, and never substitutes an empty default. Condition (bright-boar): print the disposition. The phase=prepared-effect-input-acquire line carries the carried value's outermost variant name beside its content digest, so a run whose carrier refused is diagnosable instead of reading as a corpus problem.
2. No new ArtifactRequest variant. That algebra keys durable cross-run artifacts by digest with a realization receipt naming a provider; the carried input is an in-process value bound for one prepared subject. Condition (fierce-lark, eager-raven): cite std.materialization_ladder in source, with the four obligations as typed values rather than prose. v2.workflow.floor_prepared_effect_input_ladder states the provider (MemoTier { ContentKeyed }, scoped to the preparation frame, retention released at scope exit with the tier's exact 256 MiB ceiling) and the demands (the acquisition a WorldRead with its envelope declared — the envelope IS the prepared subject; the producer a PureComputation), and every_carried_identity_is_discharged is decided by the ladder's own fold. The four are derived from the row, not transcribed beside it: copying scope and retention per row would be one fact in two places (§3) and the transcription §6 forbids; the roster header names each of the four and the symbol that derives it.
3. Condition (eager-raven): a control that the binding is absent after tier clear. the_prepared_input_binding_is_absent_after_the_tier_is_cleared.

Evidence

cargo test --release -p v1-compiler --lib pure_producer_share — 17 passed, 0 failed (remote, BuildBuddy). Five are this change's: the acquire-once-and-warm positive; the changed-carrier RED; the binding-cleared control; a row naming an unprepared input stopping the line; a non-nullary acquisition refused.

Three controls found real defects, which is why they are worth more than their green:

1. The first cut evaluated the producer through run_in_context, which calls call_function directly and reaches neither the tier nor the binding — so it asserted a value recompute also produces. Discovered by planting the wrong implementation and watching the RED stay green. The controls now evaluate through an ordinary call site and assert an observed serve from the tier's own hit observer.
2. With that fixed, the changed-carrier RED went red on the real implementation: the producer-to-carry map held a clone of the carry, so re-binding the acquisition left the key unchanged and the producer was served a value derived from the previous carrier. It now holds the acquisition node and reads its current binding at every key derivation.
3. The ladder refused the first conformance witness, and was right to (run 34854251612, the_carry_is_discharged_at_the_preparation_lca → Bool(false)). At a SHARED-STATE obligation LCA, group_redundant_verdict answers AuthoredDuplication and never reaches a provider at all — because §2's repair there is to carry the first value, not to cache it: "caching a later request only makes redundant work cheap and suppresses the signal that would make it rank for deletion". Asserting Discharged was asking the ladder to bless the move it exists to refuse. The witness now states the transition this mechanism performs — AuthoredDuplication over the claim-sited demands before, AcceptedSingleRecompute and every verdict green over the minimized graph after — which is a stronger statement than the one it replaced, and it is the ladder's own words rather than mine.

Discrimination receipt for the RED (executed, both arms): with cross_claim_key_args returning None — the empty-argument-row implementation this control targets — a_changed_carrier_content_is_not_served_the_value_derived_from_the_old_one FAILS with "the producer must not be SERVED under a changed carrier"; with the real implementation all 17 pass. A control that only asserted "the carried value is served" would pass on both.

What is owed at live grain, stated as owed

The live row is enrolled (roadmap_acceptance_event_history_load as the prepared input; roadmap_authority_projection as an ImplicitAcquisition warm row), so the required floor executes the whole path over the real corpus on this PR. What is not claimed here is the present-vs-absent measurement: it needs two workflow_dispatch runs on a branch ref pinned to an exact sha (the corrected procedure in the roster's own header — a pushed side branch triggers nothing and a PR pair measures two different merge refs), read over required_floor_claim_cost.tsv and the run's [floor-shared-fill] ledger. The row is admitted only on serve-below-recompute at identity grain; if it does not clear that, it is withdrawn into floor_cross_claim_refused_candidates rather than defended by a family aggregate.

Wind-down state at 36c54cde2e9 (2026-09-14, handed off by gentle-ram-506)

Added after the adjudication above (ruling relayed by eager-raven-113 and fierce-lark-661, from warm-heron-775's duplicate model on the closed #11381):

• Full form confirmed. The acquisition itself is carried, and claims are served the carried value; nothing re-reads or re-parses the history file per claim. ImplicitAcquisition already was this form, so no mechanism change was needed.
• Effect guard on the plain warm path. warm_cross_claim_pure_producer stored with no effect-dispatch guard, so an effectful nullary row rostered as a plain warm row was stored under the empty argument row, blind to what it read. It now refuses with cause=PureProducerShareWarmDispatchedEffect producer=… effects=N through a typed PureProducerWarmRefusal. RED: a_plain_warm_row_that_dispatches_an_effect_stops_the_line performs one real hermetic checkout read. All 10 pure_producer_share_tests pass remotely. Discrimination receipt: with the guard disabled, the test fails at expect_err because the row stored without refusal. Positive control: a_carried_roster_warms_and_stores_its_nullary_rows.
• The carried-input serve is recorded in the hit ledger as prepared-effect-input/<name>, named apart from a share hit.

Pending, not claimed:

1. CI at this head (the witnesses run was pending at hand-off) and at least one approving review. There were 0 reviews with 1 active.
2. The sha-pinned present-vs-absent workflow_dispatch pair described above, and the serve-below-recompute admission decision for roadmap_authority_projection. If the row does not clear it, it is withdrawn into floor_cross_claim_refused_candidates.
3. warm-heron's optional items, not done: (a) a sentence in the roster header saying an absent file under the checkout root is determined by the commit, so it needs no floor refusal (the value-digest key already separates LoadRefused from Loaded); (b) a shared-fill ledger COUNT for serves refused because the binding changed.

#11303 (PR one) is further out than this chain assumed — it was evicted from the merge queue over an unrelated eval-steps ceiling. This PR does not depend on it: the live row uses the ImplicitAcquisition arm, which is the shape on main. When #11303 lands, the row becomes BoundParameter — a row edit, not a mechanism change.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-14T15:59:16.125756Z	ce0614c	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ce0614ce96

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Include carried inputs in the tier's byte budget

When a prepared-input roster contains a large or currently unused acquisition, this inserts its complete value into CROSS_CLAIM_PREPARED_INPUT without checking either the 4096-entry cap or the 256 MiB byte budget enforced by store_cross_claim_pure_memo. Such carries remain resident for the entire prepared run even if no producer row subsequently accounts for them, so roster growth or a large checkout input can bypass the tier's stated retention bound and exhaust memory; measure the portable carry and refuse or charge it before retaining it.

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Record acquisition fills before reporting their hits

In every carried-input warm, the producer calls the bound acquisition and this reports a cross_claim_pure_share hit, but acquisition setup only creates a SharedBuildObservation and never calls the ledger's matching record_fill for the acquisition key. Consequently shared_fill::record_hit takes its no-fill branch and increments unattributed_hits even on a correctly instrumented run, while direct acquisition consumers are omitted from the per-key consumer set; this corrupts the [floor-shared-fill] evidence used by the roster's present-vs-absent measurement.

Useful? React with 👍 / 👎.