Skip to content

WalkPlan success stages + in-executor floor finalization (INCOMPLETE — see known gaps) - #7470

Merged
briansrls merged 6 commits into
mainfrom
claude/walk-plan-success-stages
Jul 30, 2026
Merged

briansrls merged 6 commits into
mainfrom
claude/walk-plan-success-stages

Conversation

@briansrls

@briansrls briansrls commented Jul 30, 2026 •

Copy link
Copy Markdown
Contributor

Not ready to merge. Do not approve on the current head. Review 2026-07-30 requested changes and asked that this stay draft until the admission occupants and their runtime controls are complete. This body states what is done, what is knowingly incomplete, and what is still owed — the branch should not read as finished.

Five commits: the WalkPlan carrier, the witness migration, in-executor floor finalization, the attempt-scoped admission carrier, and a rebase onto current main.

What is done

The carrier. WalkPlan { batches, on_success_stages } — two populations with different ordering laws, because a bare List<List<Runnable>> has exactly one ordering primitive and green-only work needs a second. All four plan functions return it (_batches → _plan); the parser is strict, with no fallback to a bare list, since that fallback would run a malformed plan with its stages silently dropped.

Floor finalization in-executor. The resolve-count law and materialization disclosure law moved out of two GitHub shell steps into run_walk, validated after receipts write and before any stage. This closes the ordering defect where a receipt gate could red after admission had already stamped. Both gate scripts, both step constructors, and their Scaffold rows are deleted — not unwired. #7467's per-component receipt is folded into the ordinary verdict through the rebase.

Attempt-scoped admission carrier (model only, no consumer yet): receipt v2 with the attempt identity in the payload, TestedSubject, and MergeDeniedWrongAttempt checked first — a foreign receipt is not stale or fresh, it is not the subject.

Arm-time stage validation — refuses discovery runnables, empty entry/function, and heavy-resolve claims before the governor arms, so a malformed plan cannot spend a 20–30 minute floor to report a parse-time error.

Known gaps — named, not hidden

The carrier note (std.realization_schedule.walk_plan_note) states these in-tree rather than promising behavior the executor lacks:

  1. Stage members run serially, though the contract permits concurrency. Serial is a stronger order, so no current caller is misled — but wall time, peak memory, and overlap are resource facts a future author would measure wrongly.
  2. Stages bypass the ordinary unit-lane partition, so no governor admission, batch clamps, or resource-profile enforcement. Safe for the negligible admission claims; unsafe for the substantial claim the generic carrier permits. The arm-time validator walls the one resource fact the Rust Runnable retains (use_walk_memo) and says so — the other two are not carried through parsing.
  3. One aggregate stage receipt is written after the sequence, not one per stage before the next.

The repair for all three is extracting the ordinary batch machinery into a reusable run_stage, so both populations share one executor and differ only in ordering and failure policy.

Also outstanding from review: the finalization policy is still selected by plan-function name rather than carried by WalkPlan (the same convention the carrier was meant to remove), and schedule lenses do not yet see the stage population.

Still owed before the merge bar

  • run_stage extraction: real intra-stage concurrency, governor admission, per-stage receipts
  • WalkFinalization in the carrier, replacing the name-based selection
  • Schedule-lens projections over OrdinaryBatch / OnSuccessStage
  • The discriminating executor control set (including a latch-based barrier test, not timing)
  • The admission occupants: capture_tested_subject as first ordinary batch (declared count 1→2, dated), stamp_tested_floor binding the captured subject, refresh_target_and_gate as one sequenced claim — never [fetch, gate] in one stage, since stage siblings are concurrent by contract
  • Task Refactor tool acquisition: env node provides resources via edges #12 dead-emitter deletion, atomic with the migration — its still-green tests assert the freshness property the live path lost
  • Timeout as the derived two-budget sum

Merge bar: no end-to-end behavior owed to the run — a green CI log showing capture → floor → finalization → stamp → refresh+gate, a synthetic FullLedger red with no receipt and no stages started, a temp-repo freshness refusal, exact ordinary and on-success resolve receipts, and zero consumers of the retired script web.

Cost honesty

This head buys almost no wall time yet. The deleted steps were millisecond receipt reads; the real opportunity is the still-live cold stamp and cold gate (measured ~117s and ~116s in the last completed run, ~3m53s combined). The 100→90 timeout is a reduced backstop, not a measured saving. The saving arrives when admission actually moves into the warm process, and a fresh end-to-end run confirms it.

Verification on this head

cargo test 37/37 including both floor-finalization arms; the WalkPlan parser RED refuses a bare-list plan; 13/13 attempt-carrier witnesses including the precedence proof; existing admission witnesses regress clean (15/15, 13/13, 8/8); generated artifacts regenerate byte-stable; fmt clean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

claude added 3 commits July 30, 2026 08:44
…ctly

Foundation commit of the success-stages redesign (operator design ruling
2026-07-30). This lands the carrier, the strict parser, the renames, and
sequential fail-fast stage execution in the executor. Every plan declares
on_success_stages: [] today, so runtime behavior is unchanged until the
merge-admission migration populates the floor plan's stages in a
follow-up commit on this branch.

THE CARRIER. std.realization_schedule gains

  type WalkPlan {
    batches: List<List<Runnable>>
    on_success_stages: List<List<Runnable>>
  }

Two populations with different ordering laws, and the type says so where
a bare List<List<Runnable>> could not: batches are the ordinary floor
under FloorBatchStopPolicy; on_success_stages run only after the ordinary
floor completed AND its receipts wrote, each stage a barrier, always
fail-fast between stages — FullLedger is an ordinary-floor policy and
never applies between stages. The carrier note records BOTH prior
defects: the trailing-batch fail-open, and its sibling — members WITHIN a
stage run concurrently, so anything sequential must be ONE claim whose
body sequences its steps (the first repair draft re-created exactly that
bug and the note names it so the next author does not).

THE RENAMES, because a function whose value now carries postcondition
stages must not keep a name that says it returns only batches:

  gunbc_ci_floor_batches         -> gunbc_ci_floor_plan
  gunbc_ci_regen_floor_batches   -> gunbc_ci_regen_floor_plan
  gunbc_ci_plan_artifact_batches -> gunbc_ci_plan_artifact_plan
  gunbc_falsifier_batches        -> gunbc_falsifier_plan

The four argv/step consumers followed automatically because they derive
from the floor_plan_function / plan_artifact_plan_function /
regen_floor_plan_function / falsifier_plan_function constants — the
constants are the single naming authority and were renamed with the
functions; ci.yml and falsifier.yml regenerate with the new names at all
three invocation sites. The internal batch builders survive as
*_ordinary_batches, which the structural witnesses now target. The
budget_red_control fixture renames with the floor fn it impersonates (the
clamp arms by name). Executor string keys (clamp gate, falsifier budget
flag, eager compile-clean install, arm-time refusal roster) renamed in
the same motion.

THE PARSER is one and strict. walk_plan_from_plan requires BOTH fields;
a plan with no postconditions declares an empty list, never omits the
field, and there is deliberately NO fallback from a failed record parse
to a bare-list reading — that fallback would run a malformed plan with
its success stages silently dropped, the silent-widen arm section 5
forbids.

STAGE EXECUTION in run_walk: gated on the whole ordinary floor contract
this process owns — batch verdicts AND every receipt write — not just
any_failed. Members execute serially in-process via run_memo_shared_claims
with a stage-local memo, so an entry shared by stages resolves once and
is reused; serial execution provides more order than the contract
promises, which is safe, while the contract itself promises none. A
non-claim runnable in a stage is a typed refusal, never a widen. Stage
materialization is structurally NOT folded into the floor materialization
receipt: stage memo contexts drop after it is written. A new receipt
class, target/floor-on-success-receipt.txt, records declared/run counts,
per-stage verdicts, and on_success_resolves_total — separate from the
ordinary resolve receipt BY LIFECYCLE, so ci_floor_declared_resolve_count
measures exactly the population it always did. On a red ordinary floor
the receipt still writes, loudly, with skipped=ordinary_floor_failed and
zero stages run — a typed diagnostic, never an admission artifact.

VERIFIED BY EXECUTION:

  RED  a bare-list plan fn refuses: "malformed plan value
       (gunbc_ci_floor_ordinary_batches): WalkPlan missing field
       `batches`", exit 1 — no fallback. (This control also caught a
       missed internal call site at ci_floor_plan.dag:1360.)
  GREEN gunbc_ci_floor_plan parses to the same 5 batches, then this
       container's pre-existing FloorBudgetBelowMinimumFootprint
       fail-fast — which itself proves the parse ran first.
  ci_floor_plan_witness_test 14/14 · ci_spec_witness_test 27/27 ·
  falsifier_workflow_witness_test 11/11 · gunbc_invoke_witness_test 7/7 ·
  pr_native_batch_test 2/2 · realization_schedule_witness 4/4.
  Generated artifacts regenerate; cargo fmt --check clean; claim_executor
  and gunbc build clean. (Workspace-wide cargo build fails in
  v1-stage0-std-core with 7 pre-existing errors, present on clean
  origin/main with this change stashed; CI builds named bins only.)

REMAINING ON THIS BRANCH, per the settled design: executor-level floor
finalization (resolve law + materialization disclosure in-process, the
two GitHub gate steps deleted), the tools.merge_admission entry
(capture_tested_subject as the first ordinary batch, stamp_tested_floor,
refresh_target_and_gate), attempt-scoped receipt schema v2, the task #12
dead-emitter deletion, timeout derivation as the two-budget sum, and the
operator's witness list including the stage-barrier latch test.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
Phase 1 of the success-stages redesign (operator ruling 2026-07-30): the
resolve-count law and the materialization disclosure law now run INSIDE
claim_executor as ordinary-floor finalization, after the receipts write
and before any on-success stage. The old shape ran them as two GitHub
shell steps AFTER the floor step, so a receipt-law violation could red
the job after admission had already stamped — the can-red-after-admission
hole. In here, a violation is an ordinary-floor failure and blocks every
on-success stage by construction.

MECHANISM. The floor plan projects its law into its own closure:
gunbc_ci_floor_declared_resolve_count in ci_floor_plan.dag reads the
ci_materialization authority (single authority; the projection is a read,
not a second declaration). The executor reads it fail-closed at arm time
for the floor plan only — a floor-named plan whose law cannot be read
refuses the run rather than walking without its contract — and validates:

  law 1: resolves_total (recomputed from batch_records by the SAME
         nonzero-resolve_nanos rule the receipt writer uses, never
         re-parsed from the file we just wrote) equals the declared count
  law 2: the materialization receipt exists, keyed/unkeyed/duplicated
         parse, and keyed_calls is nonzero

Violations are typed FLOOR-FINALIZATION-REFUSED lines, counted into
failure_details. Regen, falsifier, and plan-artifact declare no
finalization and are byte-unchanged in behavior.

DELETED, NOT UNWIRED: both gate scripts and their Scaffold rows in
ci_materialization, both step constructors in ci_workflow, and the two
aux terms in the ci job backstop (100 -> 90, still the exact step-sum +
prelude). A surviving script would be a second representation of the
floor-completion rule whose still-green tests could mask a live-path
regression — the exact shape that hid the lost admission fetch. The
receipt FILES keep writing; they are observability, and only the shell
re-validation of them is gone. ci_spec_witness_test gains the negative
witness that both step names are absent from the emitted workflow.

THE FIXTURE follows the name it impersonates: budget_red_control_plan
declares the law (1 — it runs exactly one single-claim batch) because the
floor name now arms finalization as well as the clamp; before that row
landed, running it WITHOUT the law was the executable RED of the
fail-closed read.

ONE MORE TRANSCRIPTION DELETED, caught by this change redding it:
ci_job_backstop_equals_one_hundred_minutes mirrored the derived step-sum
as a literal 100, so this correct change reported as a failure and the
reviewer move would have been editing the number to 90 — the same class
as the roadmap 63-declared pin, deleted under the same ruling. The
magnitude-independent invariants stay: exact step-sum + prelude (its
conscious double-entry copy updated to the four remaining aux terms) and
the dropped selection-control term.

VERIFIED BY EXECUTION:
  projection reads 1 from the plan closure (gunbc run)
  RED  fixture without the law: "gunbc_ci_floor_declared_resolve_count
       unavailable (fail-closed)", exit 1, before any batch walks
  unit arms (cargo test, 2 new): count mismatch refuses in BOTH
       directions; matching count leaves exactly the missing-receipt
       refusal when no materialization file exists — absence never passes
  ci_spec_witness_test 28/28 · ci_workflow_witness_holds PASS
  ci.yml regenerates: both gate steps gone, ci job timeout 100 -> 90

NOT PROVEN HERE: the full-floor green path through finalization — the
fixture walk now proceeds past the arm into the eager whole-tree
compile-clean install (~72min class) and was killed at a local 10-minute
cap, and the real floor fail-fasts on this container's memory. Owed to
the fleet run with the rest of the merge bar.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
@cursor

cursor Bot commented Jul 30, 2026

Copy link
Copy Markdown

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

claude added 2 commits July 30, 2026 18:00
…empt

Phase 3 slice of the success-stages redesign (operator ruling 2026-07-30):
the pure carrier for attempt-scoped merge admission, landed add-replacement
beside the live v1 format. No consumer migrates yet — the wet entry, the
plan wiring, and the v1/emitter-web deletion follow on this branch — so
runtime behavior is unchanged; this slice is the vocabulary the migration
will speak, proven hermetically before anything wet depends on it.

THE CARRIER. MergeAdmissionReceiptV2 carries the walk-attempt identity IN
THE PAYLOAD, not just the path: a misrouted read must fail on content too.
TestedSubject {attempt_id, head_sha, base_ref, base_tree_hash} is the
subject the floor tested, captured pre-floor and bound into the receipt by
the stamp — the stamp must never re-read HEAD or re-observe the target at
stamp time, because main can advance during a tens-of-minutes floor and a
post-floor observation would claim the floor tested a tree it never saw.

THE VERDICT gains MergeDeniedWrongAttempt, checked FIRST: a receipt from
another attempt is neither stale nor fresh — it is not the subject, and
asking whether a foreign receipt's base is current answers a question
about the wrong run. Growing the coproduct forced every exhaustive match
to take a position (non-fold residue, no wildcards): the gate's
verdict_reason, would_block, and the enforcement/actuator witnesses each
gained the arm consciously, and the compiler's exhaustiveness refusal
located the one site the sweep missed (receipt_is_admissible) — the
coproduct growth is complete by construction, not by grep.

ATTEMPT IDENTITY composes from GITHUB_RUN_ID + RUN_ATTEMPT + JOB, pure
composition here, env observation deferred to the wet entry. Every part
must be nonempty or the composition refuses — never a silent 'local'
constant, which would make every non-GitHub run one attempt and leave the
wrong-attempt refusal unreachable off CI (the unreachable-arm shape §5
forbids). Non-GitHub execution supplies GUNBC_WALK_ATTEMPT_ID explicitly,
same nonempty law.

WIRES are self-identifying (schema tag line 1), unlike positional v1: a
v1 wire fed to the v2 parser refuses on the tag rather than mis-binding
fields by position, and the two v2 wire kinds refuse each other. Paths
are attempt-scoped: .gunbc/merge-admission/<attempt-id>/{tested-subject,
floor-receipt}.wire.

VERIFIED BY EXECUTION — 13/13 new hermetic witnesses, including the
ordering proof (a receipt that is simultaneously foreign, Failure, stale-
base, AND stale-roster classifies WrongAttempt — precedence, not
coincidence), both cross-parser refusals, both roundtrips, the nonempty
refusals, and path distinctness across attempts. Existing admission
witnesses regress clean: producer 15/15, enforcement 13/13, actuator 8/8.
Generated artifacts unchanged (model + tests only).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
…e stages at arm time

Step 0 of the review disposition, plus the two findings fixable without the
run_stage extraction. The remaining findings are named, not silently
carried.

REBASE, and the conflict was load-bearing exactly as predicted. #7467 added
floor_component_receipt_ok to the walk verdict; this branch had replaced
that composition with ordinary_failed || on_success_failed. Resolved by
folding the component receipt INTO ordinary_failed, so a component-receipt
construction or write failure is an ordinary-floor failure that blocks
every success stage — dropping it would have reopened the very ordering
defect this branch exists to close. The test fixture also gained #7467's
new BatchRecord label/selection_tag fields.

THE CARRIER NOW DESCRIBES THE EXECUTOR IT HAS, not the one it wants. The
note claimed members within a stage run concurrently and that each stage
writes its receipt before the next begins; neither is true today — members
run serially and one aggregate receipt is written after the whole
sequence. A carrier promising a guarantee its executor does not provide is
the defect this type exists to end, and I had reintroduced it. The note
now states the barrier that IS real (stage N completes before N+1; a
failed stage prevents every later one) and names three gaps: serial
members, stages bypassing the ordinary unit-lane partition and therefore
governor admission and clamps, and the aggregate receipt. The repair —
extracting the ordinary batch machinery into a reusable run_stage so both
populations share one executor — is named on the carrier as the next step.

ARM-TIME STAGE VALIDATION. Success-stage admissibility is checked
immediately after the plan parses, BEFORE the governor arms and before any
ordinary batch runs: a plan-shape error is knowable at parse time, and
discovering it after a 20-30 minute floor spends the whole walk to report
something the parse already had. Refuses discovery runnables (no defined
green-only meaning), empty entry/function, and heavy-whole-tree-resolve
claims (which would bypass governor admission through the weaker route).

ONE HONEST NARROWING: I first wrote the validator against
profile.spawns_host_compiler and profile.memory — fields the Rust Runnable
does not carry. Only use_walk_memo (the parsed form of
heavy_whole_tree_resolve) and execution_mode survive parsing, so the
validator walls the heavy-resolve case and says so; walling the other two
requires retaining them on Runnable, which lands with the run_stage
extraction. The wall is narrower than intended and the code says which
part is missing rather than implying full coverage.

VERIFIED: cargo test 37/37 (including both floor-finalization arms against
the rebased BatchRecord); the WalkPlan parser RED still refuses a bare-list
plan post-rebase; generated artifacts regenerate clean; fmt clean.

STILL OWED, from the review and unstarted: run_stage extraction with real
intra-stage concurrency and per-stage receipts; finalization policy carried
by WalkPlan rather than selected by plan-function name; schedule-lens
projections that see the stage population; the discriminating executor
control set; then the admission occupants and the task #12 deletion.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
@briansrls briansrls changed the title Move floor receipt gates into claim_executor (ruling 2026-07-30) WalkPlan success stages + in-executor floor finalization (INCOMPLETE — see known gaps) Jul 30, 2026
Two halves: review finding 4, and the fix for the regen red CI just
reported on this branch.

WALKFINALIZATION IN THE CARRIER. The finalization policy was selected by
plan-function name — `if plan_function == "gunbc_ci_floor_plan" read the
law from the closure` — which is the same hidden seed-roster convention
the WalkPlan carrier was built to remove, reintroduced in the same PR.
The RED fixture made the coupling visible: it had to impersonate the
production plan name and then define a projection fn because that name
silently enrolled the contract.

The policy is now a FIELD:

  type WalkFinalization
    = NoWalkFinalization
    | FloorFinalization {
        declared_resolve_count: Int
        require_materialization_disclosure: Bool
      }

  type WalkPlan { batches, finalization, on_success_stages }

Every plan declares it explicitly — the floor carries its law, regen /
plan-artifact / falsifier say NoWalkFinalization, never omission. The
strict parser requires the field, so a floor plan without its law is now
UNWRITABLE rather than discovered missing at arm time — the fail-closed
arm-time read this replaces is deleted along with the projection fn and
the fixture's name-impersonated law. Schedule lenses and plan artifacts
can now see the policy, because it is part of the parsed value.

THE REGEN RED, diagnosed from the job log: regen_verify_gate_passes
returned false on this branch's previous head because the WalkPlan
carrier change touched dag/std/realization_schedule.dag, which is in
v1's regen input closure, and the committed stage0 seed was stale
against it. regen_stage0 confirms the diagnosis exactly: of 108 written
files, precisely ONE differs — std_realization_schedule.rs, the emitted
Rust of the carrier — now regenerated against the current tree
(including WalkFinalization, so one seed covers both changes) and
proven byte-stable on a second regen run.

VERIFIED: cargo build clean; the two floor-finalization unit arms pass
against the field-carried struct; gunbc-eval of gunbc_ci_floor_plan
shows the plan value carrying FloorFinalization { declared_resolve_count
1, require_materialization_disclosure true }; generated artifacts
regenerate clean; fmt clean. Local executor parse probes of the fixture
and regen plans were killed by this container's timeout during the
multi-minute prelude, before reaching the parse line — inconclusive, not
failing; the pushed run is the parse evidence.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
@briansrls
briansrls merged commit b01cdf4 into main Jul 30, 2026
5 checks passed
@briansrls
briansrls deleted the claude/walk-plan-success-stages branch July 30, 2026 21:14
briansrls pushed a commit that referenced this pull request Jul 31, 2026
…ng produces (#7482)

* Read the walk's own infra fault as data, and drop a matcher arm nothing produces

Sibling of #7476, found by looking for the same shape elsewhere: a typed fact
formatted into prose and then recovered by grepping that prose.

THE ROUND-TRIP. `handle.join()` returning `Err(_)` means a claim thread panicked
— the walk KNOWS this. That bool became `format!("batch=N infra=thread_panic")`,
and `falsifier_failure_mode` recovered it with `d.contains("infra=")`. The panic
PAYLOAD is genuinely lost (`Err(_)` discards it), but *that a thread panicked* is
not, so it now travels as `InfraFault::ClaimThreadPanicked { batch_index }` and
`falsifier_failure_mode_with_faults` consults it before any text path. The
rendered line goes back to being for humans.

A MATCHER ARM THAT COULD NEVER FIRE. `d.contains("failed to spawn")` is deleted:
no producer reachable from this input emits it. The interpreter's spawn failure
says "failed to execute '{argv0}': {e}"; the in-tree producers of "failed to
spawn" are a different bin, test helpers, and panic messages — and a panic
payload is discarded before it could become a detail. A substring its own input
cannot contain only looks like coverage.

KEPT AS TEXT, DELIBERATELY. "Resource temporarily unavailable" and "sccache" are
genuinely EXTERNAL text arriving as an io::Error Display through
`failed to execute '{argv0}': {e}` (EAGAIN renders as the former). Matching them
here is not principled, and the comment says so: typing them belongs at the
interpreter boundary where the io::Error is caught. Not silently left as if it
were the same kind of thing as the fact above.

ALSO FIXES A LIVE MAIN RED, unrelated to the above but caught by it.
`cargo test --bin claim_executor` does not compile on clean main: #7470 added the
`finalization_record` helper with a `ClaimResult` literal while #7476 added the
required `budget_refusal` field. Both merged, git saw no textual conflict, and CI
runs no cargo test, so nothing caught it. Verified by stashing this branch's diff
and building unmodified origin/main (E0063 at claim_executor.rs:4526). My field
made it required, so the one-line fix rides here.

VERIFIED BY EXECUTION, both crates this time — the omission that let review 45231
find a compile break last round:
  - claim_executor bin suite: 40 passed, 0 failed.
  - `cargo build --tests -p v1-compiler-tests`: Finished.
  - `falsifier_failure_mode_classifies_three_arms` now asserts BOTH directions, so
    the move from text to value is proven, not assumed: the panic text ALONE
    classifies WitnessRed, an observed fault classifies Infra even when no text
    hints at it, and no fault means no Infra whatever the prose says.
  - Proven discriminating: with the typed arm neutered the test FAILS; restored it
    passes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: affected set is red again

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 31, 2026
…n the emitter (#7481)

* Harden the finalization and admission carriers; fix CR/NUL escaping in the emitter

Follow-up to #7470, addressing its review. Five separable pieces.

FINALIZATION CARRIER. WalkPlan is now WalkPlan<F>: gunbc_ci_floor_plan returns
WalkPlan<FloorFinalization>, the other three return WalkPlan<NoWalkFinalization>.
FloorFinalization moves out of std.realization_schedule to gunbc.ci_materialization,
beside the count it is about, so the generic carrier stops owning a growing coproduct
of gunbc-specific receipt policies. declared_resolve_count becomes Nat.

The review asked for this as a construction wall. It is not one, and the note says so
rather than claiming it: probed by execution, substituting NoFinalizationDeclared into
the floor while its signature still reads WalkPlan<FloorFinalization> TYPECHECKS and
fails only at the first field access. A narrower probe isolates the general defect --
the typechecker does not check a declared return type against the body at all
(fn f() -> Int returning a string typechecks), nor a data annotation against its value,
while argument position IS checked. So this is a wall-after-grounding whose dissolve-on
is return-position typechecking, and the enforcement today is the enrolled witness.

require_materialization_disclosure: Bool is deleted. Its false arm skipped the
materialization law while the success line still reported that disclosure held -- a
writable bypass with a lie attached, pre-authored for a consumer that does not exist.
Disclosure is intrinsic to FloorFinalization now.

FINALIZATION WITNESSES. Two rows that execute: the floor projects
ci_floor_declared_resolve_count, and a forked-by-one count is refused by the same
predicate. The other four the review listed are not written, deliberately: matching a
one-inhabitant type returns true for every input.

ATTEMPT SUBJECT. WalkAttemptId is a PathSegment brand with one constructor, testing
std.types.path_segment_is_safe -- the single authority for what makes a string safe to
concatenate as a path segment. ../other-attempt, a/b, ".", "..", backslash, CR, LF and
NUL now refuse through BOTH producers. The v2 wire parsers require EXACT arity (5 / 6 /
7 lines) and route every required field through its domain constructor; a seventh line
that is not an integer refuses the whole receipt instead of becoming pr_number: none.

The gate consumes the CAPTURED subject, not a self-describing receipt: tested_head_sha
was carried and never read, so a receipt could restate which subject it certified and
be believed. Three bindings precede any freshness question, and a mismatch is
MergeDeniedSubjectMismatch, its own state. The tested base tree grounds on the existing
extdeps.git.object_store.GitObjectId rather than ContentHash, which DESIGN already
records as one brand over two unrelated hash families.

EMITTER, CR AND NUL. escape_string_literal_body split on the delimiter "\r", but this
language's tokenizer has no \r escape -- its table is \" \\ \n \t \{ \} and \xHH -- so
that delimiter was the two characters backslash and r, and carriage returns have passed
through unescaped into every emitted target for as long as the function has existed.
Dead in practice only because no corpus string carried one; the first that did turned
it into a hard emit failure. Fixed in the .dag authority and the seed, with NUL added
beside it. Regen is a fixed point over two runs.

Also: the duplicate unreachable MergeDeniedWrongAttempt arm, and the stale diagnostics
that still described finalization as read from the plan closure at arm time or the
WalkPlan record as { batches, on_success_stages }. A resolve-count mismatch now locates
itself at <entry>::<function> WalkPlan.finalization.declared_resolve_count rather than
always pointing at the production authority.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

* Work the #7481 review: honest wall language, value witnesses, validated object ids, cross-target escapes

Six items from the review, plus the CI floor failure the first head hit.

THE CI FAILURE, first, because it is the one defect rather than a refinement.
`claim_executor: WalkPlan.finalization: must be a NoFinalizationDeclared or
FloorFinalization value, got FloorFinalization { declared_resolve_count: 1 }`. Moving
FloorFinalization out of the WalkFinalization sum into a standalone record changed its
RUNTIME shape from Value::Variant to Value::Record, and the parser only matched
variants. The .dag witnesses stayed green throughout because field access works fine on
a record -- the executor's parser was never executed against the new shape, which is
exactly the specification-without-execution trap. Both shapes are matched now, by TYPE
NAME rather than by "has a field called declared_resolve_count", and the repair is
proven by running claim_executor against the budget RED-control fixture: "floor contract
finalized -- resolve count matches declared 1 and materialization disclosure holds".

1. Every residual construction-wall overclaim is gone. floor_finalization_note,
walk_plan_uniformity_note, the RED fixture's note and two seed doc comments all said the
signature rejects the empty policy or that plans cannot acquire the laws by picking a
value. They now say what is true: WalkPlan<F> DECLARES the intended family and removes
the std-level coproduct fork; the enrolled value witnesses and the runtime parser are the
wall until return-position typechecking lands.

2. The three no-finalization witnesses are added, and the reasoning that omitted them was
wrong. It assumed the declared return type bounds the runtime value; the probe shows it
does not, so matching the actual value is load-bearing rather than a match over a
one-inhabitant type. regen, plan-artifact and falsifier each carry NoFinalizationDeclared,
witnessed.

3. The duplicate MergeDeniedSubjectMismatch arm is deleted -- the same residue class as
the duplicate WrongAttempt arm this branch already removed, reintroduced by the mechanical
pass that added the new variant.

4. Git object ids are now VALIDATED, not merely branded. git_sha1_object_id /
git_sha256_object_id land beside GitObjectId in extdeps.git.object_store, checking exact
length (40/64) and canonical lowercase hex through the existing
git_decode_lower_hex_octets rather than a second hex reader. Before this, sha1:x,
sha1:not-hex and a 64-digit value labelled sha1 all parsed: family without length and
syntax is not identification. git_object_id_eq moves there too -- it is generic Git
behaviour and holding it in the admission consumer was a fork. Seven REDs.

5. The escape replacement was itself target-specific. Fixing the CR DELIMITER was only
half: emitting \r and \0 is Rust-shaped, and escape_string_literal_body is
target-independent -- emit_string_literal invokes it for Rust, Dag, Go and Python alike
and never sees a RenderTarget -- so \r into a Dag literal reproduces the exact
backslash-r bug the delimiter half just fixed. The spelling is \x0d and \x00, the hex
form all four grammars accept. Proven by an inverse-pair round trip through the
tokenizer's own process_escapes, with a control asserting the characters are actually
replaced (identity round-trips perfectly). Rust is proven by compilation; Go and Python
are NOT proven and the test says so -- no toolchain here, no modeled escape grammar,
dissolve-on named.

Also: path_segment_is_safe is a predicate rather than a constructor, so std holds the law
and each brand constructs itself through it -- a generic constructor would put the
branding cast in std, where the emitter cannot render it, and every caller would re-cast
into its own brand anyway.

Not fixed here, recorded: cargo build fails on the v1-stage0-std-core crate at this
branch's merge base too (7 errors, unresolved extdeps_units_* / std_occurrence_identity
imports), and compiler_tests::rust_btree_set_ord_eligibility_requires_nominal_carrier_shape
was already red before these changes. Neither is caused by this PR.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

* Add the SubjectMismatch arm the census missed, and import the object-id equality from its definer

The floor's compile-clean gate reported one hard diagnostic:

  dag/tools/merge_admission_gate.dag:28:3: error: non-exhaustive match:
    missing variant(s) MergeDeniedSubjectMismatch

Adding MergeDeniedSubjectMismatch to MergeAdmissionVerdict obligates every total match
over it, and one consumer was missed. The miss is the same shape as the false
"zero consumers" claim earlier in this arc: the census searched dag/gunbc, dag/test/claim
and src/v2 and never looked in dag/tools, so the one consumer outside those three was
invisible to it. The re-census is whole-tree and untruncated, and finds exactly four
consumers, all now exhaustive.

Two process corrections behind this, since the same class has now cost three round trips:

  - The exhaustiveness check is doing its job. Adding a variant SHOULD break every total
    match; that is the fail-closed behaviour, and the defect is entirely in the census
    that failed to enumerate them.
  - Local verification was narrower than CI twice over. Witness-closure runs resolve only
    each entry's own imports, so a consumer in an unrelated subtree is never compiled.
    This change was verified by running the same whole-tree `--target dag` compile the
    gate runs, which is green.

Also: the attempt witness imported git_object_id_eq through gunbc.merge_admission, which
re-exports it, rather than from extdeps.git.object_store where it is defined. Import from
the definer -- a re-export chain is the shape DESIGN's import-strip cascade diagnosis
names as resolving by pool-membership coincidence.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

* Delete the stale FilePermissions inert-carrier row that main's live consumer obsoleted

The floor reached the witness corpus and one row of 5498 failed:

  inert_carrier_no_unrostered_or_stale (src/v2/lens/inert_carrier_test.dag)

Bisected by execution: 1 STALE roster entry, 0 unrostered, and the stale one is
FilePermissions. The cause is not in this PR. main's aaa3e8a added
dag/gunbc/managed_directory.dag, which consumes FilePermissions to derive a directory
mode from its declared dependents, and that module's own note states the consequence it
did not carry out -- "it is named on the inert-carrier roster (v2.lens.inert_carrier)
for exactly that reason, and this module is the live consumer that takes it off, the
same way RbacPolicy came off when extdeps/bmc/access.dag started using it". The row is
deleted here because this PR is the next one to merge main, and it blocks on it.

The ratchet worked; the PR that should have tripped it never ran it. Both RED controls
in that witness file stay green (count_not_in_roster_detects_unrostered,
count_stale_roster_detects_stale_entry), so the mechanism still discriminates rather
than having been quieted.

WHY MAIN MERGED RED, recorded because the roster row is the symptom and this is the
defect. src/v2/lens/inert_carrier_test.dag declares live_tree_disposition:
SubstrateInputsOnly, but its verdict comes from inert_carrier_names_live() -- a host
builtin that walks the whole corpus on disk (build_inert_carrier_data,
cli_run.rs:27382). Its inputs are therefore NOT its import closure, and
managed_directory.dag is not in that closure, so affected-set selection on a .dag-only
diff will not select the one witness whose entire job is to notice that diff. CI's own
note names the right treatment -- "ReadsLiveTree rows (doc-graph wall, corpus-read
host-fed lenses) always run" -- and this is a corpus-read host-fed lens declared as
substrate-inputs-only.

The disposition is NOT changed here. Making it always-run is a per-PR cost decision of
the same class as a declared-resolve-count bump, it belongs to the affected-set lane
rather than to a carrier-hardening PR, and the scheduled falsifier is designed to
surface exactly this as a counted divergence within one cadence window -- so the
question of whether that already fired and went unread should be answered before adding
standing cost.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

---------

Co-authored-by: Claude <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 2, 2026
…name missed (#7642)

* WIP: falsifier is red again

* Regenerate falsifier.yml for the renamed native-cache plan function

The auto-heal job regenerates this correctly but cannot push it: GitHub
refuses to let a GitHub App create or update .github/workflows/* without
`workflows` permission, so any change to a generated WORKFLOW artifact must
be regenerated and committed by the authoring session. Receipt: run
30722802575 job 91429923479, which ran main_wet successfully and then failed
only at the push step with `refusing to allow a GitHub App to create or
update workflow .github/workflows/falsifier.yml`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: falsifier is red again

* Close the plan-target roster by construction: PlanFunction coproduct

Review finding: repairing only the missed rename leaves intact the mechanism
that let the fifth consumer escape a migration claiming to cover "all four".
plan_function was an unconstrained String crossing the modeled boundary, so
plan identity was an argv token nothing could check and completeness could
only ever be a hand-maintained count.

gunbc.cli_invoke PlanFunction is now a closed coproduct; claim_executor_run_
plan_shell and _transport_argv take a variant. An inline string literal at a
plan_function argument is a TYPE ERROR, and a new production target cannot be
authored without adding a variant, which makes every exhaustive match over
PlanFunction fail to compile until it is handled.

The interim naming constants added in the previous commit are DELETED rather
than kept beside the wall (4b dissolution-on-climb); floor_plan_function and
friends survive only as name projections for the floor predicates that still
compare a String, and say so.

New witness rows in v2.test.claim.ci_floor_plan_witness: an exhaustive match
proving every declared target's plan value carries its declared finalization,
the emitted-argv rows tying each variant to what CI actually runs, and a
permanent regression control that the pre-repair literal is absent from both
generated workflows. No fake control was written for the exhaustiveness
itself: that guarantee is compile-time, and a runtime row for it would be a
tautology that cannot go red -- recorded in plan_roster_control_placement_note.

Emission is byte-identical: regenerating after the refactor changes no
artifact, so the type work altered no CI behavior.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Stop overclaiming the roster guarantee (review 46883)

The finding is correct and is a rung-inflation defect in my own notes, which
DESIGN 4b calls worse than sitting low: an inflated class never ranks for
climbing. Adding a PlanFunction variant forces a match ARM TO EXIST; it does
NOT force that arm to be EXECUTED, because the witness roster is a
hand-authored list. Since a declared return type is not checked against its
body, a malformed new arm could sit unexecuted while the row stayed green.
The note claimed "the set of targets and the set of proofs are the same set,
by construction". That was false.

Corrected, not softened:
- every_production_plan_target_is_walk_plan_shaped renamed
  declared_plan_targets_are_walk_plan_shaped; it no longer claims universality
  in its own name.
- the roster is extracted to plan_target_roster so the hand-authored set is a
  named carrier rather than an inline literal hidden in the assertion.
- plan_roster_exhaustiveness_note now states enforced / not-enforced
  separately, and points at the rows with real teeth for this incident class:
  the emitted-argv rows, which read the generated workflows CI actually runs.
- the same overclaim is corrected where I repeated it in
  gunbc.cli_invoke plan_function_closed_roster_note and in
  v2.workflow.ci_floor_plan walk_plan_uniformity_note.

Full structural closure needs variant enumeration over a closed coproduct,
which the language does not offer; that is recorded as the dissolve-on rather
than implied, per 4b's no-untracked-stall rule. The production type wall is
unchanged and regeneration remains byte-identical.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: falsifier is red again

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 5, 2026
§4.I — ci_native_cache_root_toolchain_segment_command
  DELETED #7436 (003d960). CASE 1 dissolution — toolchain segment
  computation reordered after setup-rust-toolchain; fallback table entry
  struck through as RESOLVED.

§4.J.A — ci_floor_stamp_merge_admission_script
  All three raw leaves (ci_floor_stamp_ambient_exit_command,
  ci_floor_stamp_root_command, merge_admission_stamp_command) DELETED
  #7522 (87a4af3). CASE 1 dissolution. 'PARTIAL #7293' status stale.

§4.J.B — ci_floor_materialization_receipt_gate_script,
  ci_floor_resolve_receipt_gate_script
  DELETED #7470 (b01cdf4). CASE 1 dissolution — WalkPlan success
  stages finalization dissolved both receipt gates.

§4.J.C (ci_spec.dag table):
  - gunbc_ci_floor_only_script DELETED #9252 — CASE 1
  - ci_regen_floor_skip_shortcut_script DELETED #8406 — CASE 1
  - gunbc_ci_regen_floor_only_script DELETED #8406 — CASE 1
  - scheduler_invoke/scheduler_invoke_with DELETED #9252 — CASE 1
  - git_fetch_script RENAMED #6833 — CASE 3 (successor:
    git_fetch_no_tags_shell / git_fetch_prune_shell)

§4.J.D (ownership table):
  - Merge-admission row: all three raw leaves struck #7522 (CLOSED)
  - CI materialization row: both receipt gates struck #7470 (CLOSED)
  - CI-spec row: stale symbols struck through individually
  - Already-routed row: ci_selection_control_script #8283,
    gunbc_ci_run_script #9252, ci_regen_ensure_rustfmt_path_script
    #8406 (and 11 rustfmt raw leaves) struck through
  - Runtime terminal row: host_effect_plan_placeholder_effect
    DELETED #10509
  - Deferred srv3 row: srv3_chown_directory_to_current_user struck
    #8796 (ref §4.D), all 4 host_hygiene_reap_*_body + liveness body
    struck #8583 (ref §4.A)

All deletion commits verified as ancestors of origin/main ✅.

Part of #10537's per-row adjudication program.
briansrls added a commit that referenced this pull request Sep 5, 2026
….E, §4.I, §4.J (#10576)

* Correct §4.A hygiene-reaper row: CASE 2 — four host_hygiene_reap_*_body symbols deleted by #8583

The §4.A row at L379 described host_hygiene_reaper_script.dag's 4
body symbols as A5-deferred. The file was deleted by ffa16a5
(#8583, Migrate host-hygiene reaper and liveness onto typed observation)
and the construction was migrated to typed host_hygiene_reaper_observe.dag
/ host_hygiene_reaper_remediate.dag / host_hygiene_liveness_observe.dag.
No direct successor body names exist — CASE 2 (file deletion upstream)
with hybrid CASE 1 (body names dissolved).

Verification:
- ffa16a5 is ancestor of origin/main ✅
- host_hygiene_reaper_script.dag: D in #8583's diff
- zero files define host_hygiene_reap_install_units_body et al.
- observe/remediate files present at dag/gunbc/host/

Part of #10537's per-row adjudication program.

* Correct §4.D srv3_chown_directory_to_current_user: CASE 4 — renamed AND climbed

The row at §4.D L436 listed srv3_chown_directory_to_current_user
as A5-deferred (srv3). It was actually renamed AND climbed by
20ad5b3 (#8796): successor is
gunbc.host_effect_realize.srv3_ensure_directory_owned_by_current_user.
New name has a stronger guarantee (readback-based, not chown exit-status
based).

This is CASE 4 (rename plus climb) — distinct from CASE 1 (dissolution)
because the construction did not disappear; it acquired a better name
and a stronger guarantee.

Verification:
- 20ad5b3 is ancestor of origin/main ✅
- srv3_chown_directory_to_current_user: 0 declaration files
- srv3_ensure_directory_owned_by_current_user: 2 declaration files

Part of #10537's per-row adjudication program.

* Correct §4.E: 4 stale foreign-executor rows

Four symbols claimed as 'already on emit' are no longer present in the
corpus. Each is struck through with its deletion commit:

1. ci_selection_control_script — DELETED by 611fd02 (#8283, CI floor cut).
   CASE 1/2: the ci.yml file was deleted and its selection-control script
   dissolved with it. Successor workflow is witnesses.yml via
   gunbc.witness_floor_workflow.

2. gunbc_ci_run_script — DELETED by 489346f (#9252, plan/walk CLI delete).
   CASE 1: the gunbc ci verb was deleted, taking its run script.

3. ci_regen_ensure_rustfmt_path_script — DELETED by 3b431f3 (#8406,
   REGEN ROOT CUT). CASE 1: regen_stage0 root deleted; rustfmt path
   script was zero-consumer machinery.

4. expected_live_deploy_retract_script — DELETED by d409b75 (#7909,
   Phase A release identity refactor). CASE 1: recategorized to
   runtime-present, then dissolved.

All four deletion commits are ancestors of origin/main ✅.

Part of #10537's per-row adjudication program.

* Correct §4.I, §4.J, §4.D ownership table: 18+ stale symbols

§4.I — ci_native_cache_root_toolchain_segment_command
  DELETED #7436 (003d960). CASE 1 dissolution — toolchain segment
  computation reordered after setup-rust-toolchain; fallback table entry
  struck through as RESOLVED.

§4.J.A — ci_floor_stamp_merge_admission_script
  All three raw leaves (ci_floor_stamp_ambient_exit_command,
  ci_floor_stamp_root_command, merge_admission_stamp_command) DELETED
  #7522 (87a4af3). CASE 1 dissolution. 'PARTIAL #7293' status stale.

§4.J.B — ci_floor_materialization_receipt_gate_script,
  ci_floor_resolve_receipt_gate_script
  DELETED #7470 (b01cdf4). CASE 1 dissolution — WalkPlan success
  stages finalization dissolved both receipt gates.

§4.J.C (ci_spec.dag table):
  - gunbc_ci_floor_only_script DELETED #9252 — CASE 1
  - ci_regen_floor_skip_shortcut_script DELETED #8406 — CASE 1
  - gunbc_ci_regen_floor_only_script DELETED #8406 — CASE 1
  - scheduler_invoke/scheduler_invoke_with DELETED #9252 — CASE 1
  - git_fetch_script RENAMED #6833 — CASE 3 (successor:
    git_fetch_no_tags_shell / git_fetch_prune_shell)

§4.J.D (ownership table):
  - Merge-admission row: all three raw leaves struck #7522 (CLOSED)
  - CI materialization row: both receipt gates struck #7470 (CLOSED)
  - CI-spec row: stale symbols struck through individually
  - Already-routed row: ci_selection_control_script #8283,
    gunbc_ci_run_script #9252, ci_regen_ensure_rustfmt_path_script
    #8406 (and 11 rustfmt raw leaves) struck through
  - Runtime terminal row: host_effect_plan_placeholder_effect
    DELETED #10509
  - Deferred srv3 row: srv3_chown_directory_to_current_user struck
    #8796 (ref §4.D), all 4 host_hygiene_reap_*_body + liveness body
    struck #8583 (ref §4.A)

All deletion commits verified as ancestors of origin/main ✅.

Part of #10537's per-row adjudication program.

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants