Skip to content

Revalidate generated-artifact heal heads - #7544

Merged
briansrls merged 12 commits into
mainfrom
session/bold-heron-551-heal-revalidation
Aug 1, 2026
Merged

briansrls merged 12 commits into
mainfrom
session/bold-heron-551-heal-revalidation

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 1, 2026 •

Copy link
Copy Markdown
Contributor

Summary

This is PR B of the operator-sequenced CI admission safety repair, following exact-head coverage PR #7531.

A generated-artifact heal now creates an explicit new subject: HealProduced { prior_head, healed_head, changed_artifacts }. The prior run becomes SupersededByHealedHead, the repair is pushed, and the heal job explicitly dispatches ci.yml with the immutable healed SHA as a required input.

The dispatch endpoint requires a branch/tag ref, so the run binds all three relevant identities before any witness can count: expected_healed_sha == github.sha == git rev-parse HEAD. github.sha is GitHub's workflow/check-run subject; checkout HEAD is the executed tree. A branch-resolution race and a checkout race are distinct typed refusals.

The dispatch surface is modeled as github.Workflows.CreateDispatch; WorkflowDispatch.inputs, which the YAML projection previously discarded, is now realized. actions:write is scoped only to the heal job because GitHub exposes workflow dispatch under that permission and no narrower dispatch-only grant exists.

Failure semantics

  • HealNoChange creates no new revalidation obligation.
  • HealProduced remains revalidation-required until PR A's exact-head, exact-roster, nonempty complete coverage admits the healed SHA.
  • A dispatch being accepted is not evidence that the healed tree passed.
  • Permission, rate-limit, endpoint, or transport refusal is HealDispatchRefused; the job fails loudly and never assumes the GITHUB_TOKEN push started CI.
  • HealWorkflowDispatchRunSubjectMismatch refuses when the check-run subject differs from the healed SHA.
  • HealWorkflowDispatchCheckoutMismatch refuses when the executed checkout differs from the healed SHA.
  • A successful dispatch still leaves the old run non-success and logs SupersededByHealedHead.
  • An ordinary manual workflow_dispatch has no expected healed SHA and cannot discharge a heal obligation.
  • The existing fail-fast generated-artifact drift ordering is unchanged. The five-minute compile timeout is untouched.

External consumer adoption receipt

The in-repository model and workflow realization land here. The live dashboard consumer is ctrl session-dashboard: summarize_checks.mjs feeds the merge-ready digest and server.

Adoption is in flight, not complete in gunb-ai/ctrl PR #1922. At the recorded observation it is open, non-draft, and CLEAN; it maps cancelled runs to superseded, empty rollups to none, and admits checks only in the passing state. This overall adoption receipt closes only after ctrl #1922 merges and the live consumer is observed reading those semantics. Until then, an executing run must explicitly name the current PR head and reach every required witness.

Test plan

  • Exact model witness covers matched, run-subject mismatch, and checkout mismatch arms — PASS.
  • Emitted preflight witness requires both ${{ github.sha }} and checkout HEAD comparisons — PASS.
  • Generated-artifact wet projection refreshed .github/workflows/ci.yml — ExitSuccess.
  • The unchanged materialization ladder witnesses passed after classifying the repeated preflight as a fresh checkout observation; exact-head CI revalidates the final head.
  • Pre-push cargo fmt --all --check — PASS.

@gunbai-bot gunbai-bot Bot changed the title CI admission safety: exact-head evidence coverage, then heal revalidation (two sequential PRs, one owner) Revalidate generated-artifact heal heads Aug 1, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 1, 2026 03:48
@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 45903 at 2b4d50b0c49.

The status-code finding identified a real versioning gap, but the two contracts need distinguishing. GitHub documents that requests without X-GitHub-Api-Version default to 2022-11-28; that version returns 204 No Content. The current 2026-03-10 Create Workflow Dispatch contract returns 200 with exactly workflow_run_id, run_url, and html_url (API version behavior, current workflow-dispatch response).

The service now explicitly emits X-GitHub-Api-Version: 2026-03-10, so WorkflowDispatchReceipt is grounded in the pinned contract instead of assuming a response from an unversioned request. The workflow_run_id > 0 refusal remains valid under that pinned response.

The auth finding was also addressed: the unused operation-level auth_token: Secret and empty-string caller argument are removed. GITHUB_TOKEN is now solely the service auth_source. A scoped compile of dag/tools/ci_heal_dispatch.dag completed with zero blocking diagnostics; its emitted Rust contains the version header and env credential source.

— sent from bold-heron-551

@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 45954 at dafb3863b5d.

The preflight now binds all three identities before any witness can count:

  • expected_healed_sha, the immutable heal obligation;
  • ${{ github.sha }}, GitHub’s workflow/check-run subject resolved from the dispatch ref;
  • git rev-parse HEAD, the executed checkout.

A branch advance before dispatch resolution makes github.sha != expected_healed_sha and refuses. A later checkout divergence makes HEAD != expected_healed_sha and refuses. The typed model distinguishes HealWorkflowDispatchRunSubjectMismatch from HealWorkflowDispatchCheckoutMismatch, and the executing witness covers matched, run-subject-race, and checkout-race arms. The generated workflow carries the comparison in every revalidation job.

This deliberately retains the branch dispatch ref: GitHub’s authoritative Create Workflow Dispatch schema permits a branch or tag name, not a raw commit SHA. Subject immutability is therefore enforced at the run boundary through github.sha, rather than by sending an unsupported ref.

— sent from bold-heron-551

@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

review 45985 (cursor on 3123a41e) — already fixed on current HEAD

Verified: 3123a41e still imported expected_sha_preflight_matches_or_refuses_exactly (stale after dafb3863b renamed the witness fn). Current head 638a34903 updates dag/test/claim/heal_revalidation_integration_witness_test.dag to import/call expected_sha_preflight_binds_run_subject_and_checkout_exactly — the only file in that commit.

No further change needed for this finding; cursor re-review on 638a34903 should clear REQUEST_CHANGES. (codex review 45954 is similarly stale against earlier heads.)

— sent from crisp-badger-134

@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 45985 at 638a349036a.

The integration aggregator now imports and calls expected_sha_preflight_binds_run_subject_and_checkout_exactly, matching the renamed discriminating witness. git grep finds no remaining reference to the retired symbol.

Executed the complete heal_revalidation_integration_witnesses_hold --claim-run: it returned true and finished with zero problems.

— sent from bold-heron-551

review 46001: GitHub Actions exposes the installation token via
github.token/secrets, not as a default process env var. Project it into
the heal dispatch gunbc invocation so workflows.CreateDispatch can
authenticate.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

review 46001 (codex) — confirmed and fixed on 78f78d1e5.

CreateDispatch reads GITHUB_TOKEN via workflows auth_source: EnvVar; GitHub Actions does not inject that into the process environment by default (only secrets.GITHUB_TOKEN / github.token contexts). The heal dispatch invoke now exports GITHUB_TOKEN="${{ github.token }}" alongside the heal head/branch refs; ci_heal_job_witness_test pins the projection.

— sent from crisp-badger-134

@gunbai-bot

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 46001 at 7f11c2c71f2.

The heal commit/push/dispatch RunStep now binds GITHUB_TOKEN: ${{ github.token }} in its modeled step environment. That is the sole environment authority consumed by github.Workflows.CreateDispatch; no token binding is granted to build, regen, or witness steps.

A new executing witness inspects the live modeled heal job and requires the dispatching script’s RunStep.env to carry that exact binding. The combined heal-revalidation integration witness returned true, generated-artifact projection completed with ExitSuccess, and the generated workflow contains the step-scoped environment entry.

The aggregate CI red was on superseded intermediate head 78f78d1; the current PR check inspector reports no failing checks on successor head 7f11c2c.

— sent from bold-heron-551

@briansrls
briansrls merged commit 45e7a8c into main Aug 1, 2026
5 checks passed
@briansrls
briansrls deleted the session/bold-heron-551-heal-revalidation branch August 1, 2026 07:28
gunbai-bot Bot pushed a commit that referenced this pull request Aug 1, 2026
… breakage)

The publication gate reds on current main itself: #7544 (heal-revalidation)
merged after the P-B wall landed via #7560 but its CI raced the wall, so
its eight new files carry no PublicFilePublishGrant rows and every PR
merging current main inherits the failure. Rows added for all eight
(mechanical placement declarations for files already public on main);
cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses
green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 1, 2026
…de race)

Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall
CI run, adding three SCM-kernel files with no grant rows. Roster now
covers the full cutover..HEAD set including current main.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot mentioned this pull request Aug 1, 2026
6 tasks
gunbai-bot Bot pushed a commit that referenced this pull request Aug 1, 2026
Merging main (#7544, #7563, etc.) brought post-cutover Added paths onto HEAD
without roster envelopes; publication_placement_gate correctly refused. Declare
grants for the eleven main-side additions plus generic_item_clone_bound witness.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls pushed a commit that referenced this pull request Aug 1, 2026
…-schema) (#7572)

* WIP: compiler correctness

* Bind the guarantee-recovery analysis into the doc graph

The analysis note landed as an orphan doc: gunbc.doc_graph_roots states
that "an unbound doc is an orphan, loudly", and CI duly refused at
be1a001 with doc_graph_has_no_orphan_docs returning false in both the
dag/test/claim and src/v2/lens consumers.

Registered as two HandAuthoredDocBind rows rather than one, because the
analysis binds to two independent carriers and they dissolve on
different triggers:

- v1.compiler.infer module_skips_direct_call_arg_check — the one named
  violation of the dimension contract's "no escape hatch" clause
  (docs/thesis/correctness-dimensions.md), exempting v2.* and
  v1.compiler.* from direct-call argument checking.
- v2.std.constraints solve_constraints — passes graph.root as
  source_facts, algebra AND the sole candidate, so the grounding proof
  reduces to well_formed(root) and is relabelled CanonicalGrounding.

Green by execution, both directions: RED is the CI failure at be1a001;
GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag
plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing
locally against the live docs/ tree.

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

* WIP: compiler correctness

* Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified

Adopted (all verified on main this pass):
- Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not
  statically propagated: v2.std.refinement exists, NonEmptyList fixture +
  green cardinality_fold_propagation_test exist, and
  refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the
  carrier proves nothing). New Sec 4b: the operator independently
  re-directed this exact guarantee on 2026-07-04
  (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the
  language") — the intent is not lost; the lattice design pass (FLAG E)
  never started.
- Failure history rewritten (Sec 2): the exemption dates to 2026-06-08
  (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type
  safety "Yes (blocking)" while return position was unchecked — so the
  ledger overstated, then the auditable contract was deleted. The
  pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a
  deliberate total semantics, not a priced-out wall.
- Status vocabulary widened to the review's 11-state lattice; v2 terminal
  calibrated (validate_then_compile door + loop-bound wall are real;
  InferredTree is still not a proof boundary); application-arity row added
  (formal-driven walk, positional fallback for misspelled labels,
  ArityMismatch is constructor-arity); PatternLookupBlocked's silent []
  arm confirmed (PatternDynamic does diagnose — review corrected there).
- Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5
  behaviors" is stale against v2.std.node's six (Match) — the guarantee
  authority lands as .dag rows, never hand-edited prose.
- Sequencing reconciled to 7 stages: claims authority + expecting-red
  probe corpus together; zero-resolution method wall now, ambiguity wall
  census-first; cardinality vertical slice third.

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

* Status header: two audit passes complete, open items typed

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

* Align the bind's dissolution trigger with the doc's own authority model (review 45299)

The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as
its specification half" — wording that predates the reconciliation
pass's Sec 7b finding that DESIGN.md is a projection of
gunbc.design_document. As written, a direct DESIGN.md edit could have
satisfied the trigger, which is exactly the Sec 3 parallel-representation
failure Sec 7b names. Trigger now requires .dag claim rows projected via
gunbc.design_document and states explicitly that a hand edit does not
satisfy it.

All five doc-reachability witnesses re-run green by execution after the
edit.

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

* Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame

Review 45305, both findings verified correct and fixed:
- doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug),
  which the carrier's own note defines as the symbolic identity — one doc
  had two independently removable authority rows. Merged to ONE row whose
  trigger anchors both carriers (module_skips_direct_call_arg_check,
  solve_constraints) and gates dissolution on BOTH conditions, with the
  merge provenance recorded on the carrier. (Observed, not fixed here:
  module-identity-storage-binding-design and accelerator-demo-roundtrip
  also carry same-slug duplicate rows — pre-existing, follow-up material.)
- Sec 8b's example-0 block still said "unexpressible", contradicting the
  Sec 4 reclassification and mis-aiming the archetypal RED at inventing a
  carrier instead of sealing/propagating the one that exists. Rewritten:
  the RED exercises unforgeable construction + seam propagation, expected
  refusal at the 0..n -> 1..n seam.

Operator direction, same pass: the safety ladder is now Sec 1b, the
organizing frame — R3 structurally-impossible / R2 structural guarantee /
R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5).
Three rules: floor absolute; climb to a STATED ceiling
(mathematical / capability / price — the capability ceiling is
unforgeable construction, blocked on reference-level visibility: the
keyword set has no private/sealed/opaque); reported rung == measured
rung, lens-checked for inflation and stalls. Includes the specimen table
(the session's classes placed, cross-representation == as the exemplar
full climb) and the non-goals roster (external reality, arbitrary
predicates, budgets, optimality, self-governance, byte-identical
self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain
current_rung / ceiling / next_rung_trigger.

All five doc-reachability witnesses re-run green by execution after both
file changes.

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

* WIP: compiler correctness

* WIP: compiler correctness

* Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section

Corrections, each verified against main before adoption:

1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record
   specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque
   ... every proof-carrier is presently forgeable") was false as stated;
   corrected to an audited-status claim: sole_constructor is the
   candidate wall, completeness for generic carriers unverified. The
   earlier keyword-set inference is withdrawn in the Sec 10 ledger.
2. Subject grain: rung honesty is measured at a declared acceptance
   boundary; a class's rung is the MINIMUM across in-scope paths (the
   interpreter refuses the mislabeled call that order_typed_call_args
   reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1
   carrier gains subject_grain/acceptance_boundary/compile_mode/
   realization_target/covered_population.
3. Seed rungs demoted: return/data/generic, field-through-generics,
   exhaustiveness, cardinality, full ==-class, and L4 all to
   UnknownUnmeasured (compile admission proven is not runtime
   disposition proven); census marked specimen-denominated; unknown-
   method R0 scoped to the interpretation path.
4. Dissolution on climb amended in DESIGN 4b: production handling
   dissolves; the RED + positive controls REMAIN enrolled as the
   evidence the higher rung stays real.
5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows +
   witness-test fixture migrated); the guarantee-recovery row now
   carries BOTH anchors typed, not one typed + one in prose. Carrier
   note records that List admits [] — the exact cardinality gap the
   ladder tracks — with the doc-graph witnesses as the interim wall.
6. cardinality_fold_propagation_test relabeled everywhere as manual
   value-level specimens (length homomorphism over literals + runtime
   refine_byte); "not new design" softened to the accurate scope
   statement; the roadmap cardinality node re-briefed accordingly.
7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a
   generic dimension mechanism; extension-vs-redesign is an open audit
   question that roadmap pricing must carry.
8. Sec 1 "was not built" -> "never completed as an exhaustive
   acceptance contract"; Sec 11 queue updated (correctness-dimensions
   done; sole_constructor completeness audit added).

Additions (operator direction): ROADMAP gains the "Guarantee ladder —
climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes
in ticket format with dependency edges (probe corpus gates the four
floor walls; carrier gates cardinality slice, emitters, prevalence;
exemption removal gates on the call-shape + inhabitance walls). The
capability node is the sole_constructor completeness audit. State-vs-
work split recorded on the carrier: rung STATE lives in the Stage-1
claims carrier and is emitted (ladder-census-emitters node); roadmap
nodes track CLIMBS.

Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md
projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap
authority 35/35, model 9/9, focus 12/12.

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

* Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control

review 45336 was correct: works had a typed carrier and zero readers —
representation without a consumer is specification-without-execution
(DESIGN 5 / E-10), the exact defect class the guarantee analysis
documents, reproduced in its own fix.

Consumers now executing in dag/test/claim/doc_reachability_witness_test:
- doc_graph_binds_works_all_nonempty — an emptied works list reds
- doc_graph_works_refs_carry_symbols — a ref stripped of module_path or
  decl_name reds
- guarantee_recovery_bind_pins_both_anchors — deleting or renaming
  either of the two anchors (module_skips_direct_call_arg_check,
  solve_constraints) reds; row multiplicity pinned to one
- doc_graph_works_empty_red_control — synthetic empty-works bind fails
  the predicate, proving the consumer discriminates

Predicates live on the authority (gunbc.doc_graph_roots) so the witness
consumes the carrier's own definition. Residue named on the carrier
note: staleness against the live tree (a ref naming a decl that no
longer exists) is NOT witnessed — v1.compiler.* is outside the witness
compile pool, so ref-vs-tree resolution is exactly the
feature:cited-symbol-resolution lens DESIGN 3 already names; the refs
are symbolic citations and inherit that trigger.

All 11 doc-reachability witnesses green by execution.

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

* De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census

review 45349, third correct catch in this lane: the census demoted
method existence (R0 interpretation-path-only), inhabitance
(UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the
roadmap nodes, authored before the demotion pass, kept "R0 -> R2"
headlines, re-inflating the same claims the same day at the canonical
authority. The section's own note says rung STATE lives in the claims
carrier, never these nodes; the headlines now name only the TARGET rung
and point at the census for current state, per DESIGN 4b's
minimum-across-paths rule.

ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35;
drift witnesses 4/4, by execution.

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

* WIP: compiler correctness

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored

Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and
tidy-deer-730's measured receipts:

- guarantee_ladder_section() deleted; 16 nodes + 23 edges enter
  declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/
  guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until
  closing contracts). Page visibility is the typed focus policy (lane added to
  roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED.
- Graph corrections: probe corpus → carrier → baseline-prevalence → walls;
  prevalence split baseline/residual; new floor-generic-field-constraint-wall and
  floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the
  general method wall (measured: kernel algebra profiles vs interpreter dispatch fork,
  tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability
  node repointed off the parked visibility-grants doc.
- Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to
  the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across
  paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the
  roadmap node (review 45367); five recovered vocabularies kept orthogonal.
- HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable);
  empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows
  merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED.
- Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser
  silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger.

Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8,
doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet.

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

* WIP: compiler correctness

* Trim the three over-budget ladder briefs to the operator's 100-word ticket law

witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier,
method-existence, and cardinality briefs ran 169/128/111 words. The old
section-local placement had escaped this law entirely (the exact
ghost-universe defect the verdict named — the budget never saw those nodes);
in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut
fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2
amendment / the census), which each node links as its carrier. The budget
itself is untouched — widening the declaration to satisfy the check is the
DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean.

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

* WIP: compiler correctness

* Containment predicates consume doc_all_nodes, the one canonical walker (review 45412)

document_rendered_nodes was a traversal fork beside roadmap_spawner's
doc_all_nodes — same semantics, second walker. The predicates (whole-value
ghost count + both RED probes) move INTO roadmap_spawner, the walker's
module, because the spawner already imports roadmap_authority and the
reverse import would cycle. The authority sheds the walker and its
now-unused SectionElement imports; the containment note records both
refused first cuts (identity-only membership, review 45406; the duplicate
walker, review 45412) since each was this wall violating a law it
enforces. Authority 38/38, spawner 16/16, page 28/28.

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

* Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door

Executes all six items of the operator's post-merge verdict on #7489, each
verified against live state first (#7484 and #7485 confirmed OPEN; the anchor
confirmed as the #7489 squash; Behavior confirmed six-membered):

1. Every "#7484 landed" claim replaced with open-candidate wording — main's
   disposition stated separately from candidate branch evidence (the ladder's
   rung-inflation rule applied to open-PR state; my transcription error).
2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed,
   reproducible after in-flight merges; walls no longer race a live tree).
3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary,
   evidence} — typed/located/counted but still Accepted; specimens
   MethodExistenceUndecided and GroundingNotDerived.
4. Graph: floor-parse-formation-wall + floor-record-construction-wall +
   compiler-accepted-obligation-closure added; v2-phase-carriers split into
   five staged nodes (self-grounding frontier → Translate refusal → inferred-
   tree completeness → per-kind derivation coverage → target realization gate)
   with the registry's FIRST TOMBSTONE (superseded_by the frontier node);
   method←join edge deleted per the zero-via-union nuance (join gates only
   the >1 wall and realization completeness); residual reroutes through the
   closure door.
5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors,
   matching v2.std.node.Behavior (the decidability denominator).
6. §1d provisional guarantee grid emitted as hand-authored interim,
   dissolve-on the carrier-emitted projection.

Witnesses: authority 38/38, identity 9/9 (first tombstone passes the
count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23
ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11.
ROADMAP.md and DESIGN.md regenerated via main_wet.

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

* WIP: compiler correctness

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Route the ambiguity wall and cardinality seam through the closure door (review 45545)

The first edge set let compiler-accepted-obligation-closure land while
floor-method-ambiguity-wall and cardinality-vertical-slice stayed open —
the door would have certified "every required judgment established" over
two required-open judgments (the grid marks the cardinality seam P0.2
minimum-R2 and ambiguity part of resolved identity; the verdict's spine
routes ALL P0 obligations through the door). Both are now prerequisites
of the closure; residual prevalence depends on the door alone. Authority
38/38, focus 12/12, page 28/28, drift 8/8; regen clean.

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

* Reconcile the sec-7b behavior-count passage to past tense (review 45558)

Sec 7b still described the 5-behaviors drift as current after this PR
corrected the authority — the stale-claim problem the PR closes elsewhere.
The passage now records the drift as found-and-corrected, keeps the
specimen's evidentiary value (the denominator drifted silently in prose),
and leaves the Match-promotion adjudication question with the queue.

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

* WIP: compiler correctness

* Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement)

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

* WIP: compiler correctness

* Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract

The compile seam was silent on both classes call_function_inner refuses at
runtime, and the emitter reordered mislabeled args positionally — two
realizations of one program disagreeing silently. direct_call_shape_diags
(v1.compiler.infer) closes both, blocking, exemption-free (a label has no
representation gap). Census before landing refused 28 live rename fossils in
5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list
init->empty, path->path_opt), all relabeled to their declared authority; +3
fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled
ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0,
whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with
triggers (interpreter-first parity pair next). Roadmap node + census rows
amended; ROADMAP regenerated.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Roster the call-shape witness blob in the scaffold index (review 45655)

ct_call_shape_wall_witness_test joined compiler_tests_rust without its
LanguageSourceScaffoldRow, so the exact-equality enrollment witness
(compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered)
would red on CI. Row added with the same hand-assertion scaffold trigger as
its peers and enrolled in the roster; witness re-run green by execution.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes

d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster,
dropping the shape check its enrolled negative control pins — Symbol<Float>
became BTreeSet-eligible by name, and the RED sat invisible for ten days
because the Rust unit suite left CI on 2026-07-11. Childless gate restores the
shape constraint (zero corpus impact; regen fixed point holds); incident +
dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9
(operator decision, priced by this incident). Found by tidy-deer-730 during
the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Dedupe the call-shape witness aggregator entry after the main merge

The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test
into compiler_tests_source(); a duplicate generates the #[test] twice.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door

Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap
authority and the gap analysis:

- ladder-measurement-schema precedes probes AND carrier (the receipt protocol
  both meet through; breaks the probes/carrier protocol cycle).
- The three merged P0 slices recut at their actual grain, identities
  tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted,
  #7519) + missing/duplicate + signature-resolution siblings;
  floor-method-existence-wall -> method-established-surface-wall (accepted,
  #7484) + receiver-normalization + zero-resolution siblings;
  floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted,
  #7484) + grounding + general-wall siblings.
- The Accepted door split mechanism/floor/extended
  (compiler-accepted-obligation-closure tombstoned): the audit form lands
  with the carrier; refusal never turns on over a known-open judgment
  (review 45545's substance preserved in the activation nodes).
- Exemption removal re-grounded on argument-type-compatibility grounding +
  declared-conformance grounding (labels never gated it).
- guarantee_ladder_edges rewritten wholesale; emitters parallel with the
  baseline; baseline defined as a two-revision execution.
- Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b);
  stale dissolution triggers repointed (doc_graph_roots,
  doc_reachability_witness_test); tombstone-note staleness fixed.
- ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS
  (brief budgets, edge endpoints, acyclicity, identity registry with five
  tombstones); regen_stage0 --verify divergence 0.

The branch additionally carries the ord-eligibility silent-red repair
(childless gate on name-grain arms + incident note) and the clean regen of
the generated stage0 files after the origin/main merge.

Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference
diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag
(landed with #7508, byte-identical to origin/main; handed off to the
occurrence lane).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Recut the extended activation as per-class admissions (review 45918)

The first cut kept requires-all edges on one extended-activation node while
its prose promised class-by-class widening — the graph would have deferred
every admission behind the slowest climb, preserving the monolithic deferral
the door split dissolves. Now: four per-class admission nodes
(extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate,
each <- floor-closure + its own climb, ready the day that climb lands) and
accepted-extended-obligation-closure recut as the terminal
roster-completeness certification, where requires-all honestly belongs.
Same closure identity (no slug change, no tombstone); four fresh identities
minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP
regenerated; graph/budget/identity witnesses 26 PASS.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Trim the ord name-grain note to its structural constraint (review 45929)

The in-code note duplicated the incident narrative the gap analysis already
records (sixth-pass ledger + queue item 9) — a parallel ledger realized into
the emitted seed with no executable consumer. The carrier keeps only the
constraint the code cannot show: why name-grain arms admit childless nodes
only, the discriminating RED's symbol, and the shape-examining sibling path.
regen_stage0 divergence 0.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Spine A Stage 0: the guarantee measurement schema — evidence identifies its subject before anyone measures

gunbc.guarantee_measurement carries the vocabulary probes and claims meet
through, and nothing else (roadmap node ladder-measurement-schema; operator
spine verdict 2026-08-01): GuaranteeClassId/PathId/ProbeId brands;
GuaranteePath over four closed minimal axes (subject grain, acceptance
boundary incl. the InferToEval/InferToTranslate phase boundaries the
containment workstream consumes, compile mode, realization target with
GuaranteeTargetName deferred-grounding brand); GuaranteeMeasurementReceipt
with every field required (subject_revision x harness_revision x
probe_set_digest, reusing std.types.CommitSha and std.content_hash);
ProbeObservation as the raw outcome sum with ProbeNotRunnable structurally
separated from verdicts (top-as-ignorance never readable as pass/fail);
exactly-one path resolution and a receipt->path join that refuses unknown
and duplicate. Registry mechanism without a registry population - no probe
executes, no class rows, no disposition, no rung.

An initial ObservedOutcome name collided with gunbc.output_policy's
process-outcome type (whole-tree census caught the bare-reference break);
renamed to ProbeObservation, census back to 0 blocking.

Receipts: 8/8 synthetic-row witnesses green by execution (round-trip join,
unknown-path refusal, duplicate-registry refusal never-first-pick,
exactly-one resolution across four boundary variants, both uniqueness REDs,
digest input-determinism incl. order sensitivity, verdict/ignorance
separation); whole-tree compile 0 blocking; regen_divergence_count=0;
generated artifacts zero drift.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Record the second-consumer re-grounding trigger for observed_is_verdict (review 46075)

The predicate/walker dissolution rule triggers where a canonical fold
already exists (nat_cata) or a substrate walk is extended; neither holds
for a freshly declared domain sum whose only query this is. The note now
records the named trigger: when the claims carrier lands as the sum's
second consumer, a probe_observation fold becomes the canonical surface
and observed_is_verdict re-expresses through it.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Grant publication for the eight ungranted #7544 files (main-side gate breakage)

The publication gate reds on current main itself: #7544 (heal-revalidation)
merged after the P-B wall landed via #7560 but its CI raced the wall, so
its eight new files carry no PublicFilePublishGrant rows and every PR
merging current main inherits the failure. Rows added for all eight
(mechanical placement declarations for files already public on main);
cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses
green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Grant publication for the three ungranted #7563 files (second main-side race)

Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall
CI run, adding three SCM-kernel files with no grant rows. Roster now
covers the full cutover..HEAD set including current main.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Thread GuaranteePathId through resolution and its refusal variants (review 46179)

The resolver's key and both refusal-variant payloads carry the brand
end-to-end; join_receipt_to_path no longer erases receipt.path to String.
Measured the enforcement honestly: two executed controls show the checker
accepting a bare String at a branded parameter and a branded record field,
so the note records this as model-correctness and erasure-removal, with
brand acceptance-enforcement handed to the probe corpus as its own class.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Merge origin/main; dedupe the roster union and grant the two #7550 lean files

The alphabetized roster body on main already carried the 11 straggler
paths, so #7580's tail block duplicated every one of them; the union
keeps exactly one row per path, with this branch's two guarantee rows
slotted alphabetically. Coverage against the cutover then caught a
fourth race instance: #7550 merged two new files with no grant rows
(dag/extdeps/languages/lean/overflow.dag and its witness), redding
main's gate again - swept into the same roster here.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Observation counts are Nat, with the enforcement gap measured (review 46287)

RefusedTyped.count and AcceptedCounted.count carry the cardinal type,
and the fold's arm signatures follow. An executed control shows the
checker still accepting a negative at the Nat field today, so the note
records the swap as model-correctness with refusal owed to the
numeric-refinement acceptance class, not claimed as a wall.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Orthogonalize the path axes instead of enumerating families (review 46308)

InterpreterRun renames to RuntimeRun: run-level acceptance happens IN
the path's realization, so which runtime is the realization axis's
fact and an emitted-run path (the divergence probes' subject) is
expressible rather than contradictory. The compile_mode axis deletes:
every landed control derives its pipeline from its boundary, so the
stored mode was a second representation whose only writable novelty
was the contradiction; it returns as a stored axis with the first
path measured under two pipelines at one boundary. Both review-named
contradictions are now unwritable without a family coproduct, whose
rows would restate the orthogonal axes per combination (the N-by-M
shape DESIGN 2 folds into axes).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

---------

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>
Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
briansrls pushed a commit that referenced this pull request Aug 2, 2026
…air, probe-adequacy mandate (#7643)

* WIP: compiler correctness

* Bind the guarantee-recovery analysis into the doc graph

The analysis note landed as an orphan doc: gunbc.doc_graph_roots states
that "an unbound doc is an orphan, loudly", and CI duly refused at
be1a001 with doc_graph_has_no_orphan_docs returning false in both the
dag/test/claim and src/v2/lens consumers.

Registered as two HandAuthoredDocBind rows rather than one, because the
analysis binds to two independent carriers and they dissolve on
different triggers:

- v1.compiler.infer module_skips_direct_call_arg_check — the one named
  violation of the dimension contract's "no escape hatch" clause
  (docs/thesis/correctness-dimensions.md), exempting v2.* and
  v1.compiler.* from direct-call argument checking.
- v2.std.constraints solve_constraints — passes graph.root as
  source_facts, algebra AND the sole candidate, so the grounding proof
  reduces to well_formed(root) and is relabelled CanonicalGrounding.

Green by execution, both directions: RED is the CI failure at be1a001;
GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag
plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing
locally against the live docs/ tree.

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

* WIP: compiler correctness

* Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified

Adopted (all verified on main this pass):
- Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not
  statically propagated: v2.std.refinement exists, NonEmptyList fixture +
  green cardinality_fold_propagation_test exist, and
  refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the
  carrier proves nothing). New Sec 4b: the operator independently
  re-directed this exact guarantee on 2026-07-04
  (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the
  language") — the intent is not lost; the lattice design pass (FLAG E)
  never started.
- Failure history rewritten (Sec 2): the exemption dates to 2026-06-08
  (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type
  safety "Yes (blocking)" while return position was unchecked — so the
  ledger overstated, then the auditable contract was deleted. The
  pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a
  deliberate total semantics, not a priced-out wall.
- Status vocabulary widened to the review's 11-state lattice; v2 terminal
  calibrated (validate_then_compile door + loop-bound wall are real;
  InferredTree is still not a proof boundary); application-arity row added
  (formal-driven walk, positional fallback for misspelled labels,
  ArityMismatch is constructor-arity); PatternLookupBlocked's silent []
  arm confirmed (PatternDynamic does diagnose — review corrected there).
- Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5
  behaviors" is stale against v2.std.node's six (Match) — the guarantee
  authority lands as .dag rows, never hand-edited prose.
- Sequencing reconciled to 7 stages: claims authority + expecting-red
  probe corpus together; zero-resolution method wall now, ambiguity wall
  census-first; cardinality vertical slice third.

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

* Status header: two audit passes complete, open items typed

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

* Align the bind's dissolution trigger with the doc's own authority model (review 45299)

The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as
its specification half" — wording that predates the reconciliation
pass's Sec 7b finding that DESIGN.md is a projection of
gunbc.design_document. As written, a direct DESIGN.md edit could have
satisfied the trigger, which is exactly the Sec 3 parallel-representation
failure Sec 7b names. Trigger now requires .dag claim rows projected via
gunbc.design_document and states explicitly that a hand edit does not
satisfy it.

All five doc-reachability witnesses re-run green by execution after the
edit.

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

* Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame

Review 45305, both findings verified correct and fixed:
- doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug),
  which the carrier's own note defines as the symbolic identity — one doc
  had two independently removable authority rows. Merged to ONE row whose
  trigger anchors both carriers (module_skips_direct_call_arg_check,
  solve_constraints) and gates dissolution on BOTH conditions, with the
  merge provenance recorded on the carrier. (Observed, not fixed here:
  module-identity-storage-binding-design and accelerator-demo-roundtrip
  also carry same-slug duplicate rows — pre-existing, follow-up material.)
- Sec 8b's example-0 block still said "unexpressible", contradicting the
  Sec 4 reclassification and mis-aiming the archetypal RED at inventing a
  carrier instead of sealing/propagating the one that exists. Rewritten:
  the RED exercises unforgeable construction + seam propagation, expected
  refusal at the 0..n -> 1..n seam.

Operator direction, same pass: the safety ladder is now Sec 1b, the
organizing frame — R3 structurally-impossible / R2 structural guarantee /
R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5).
Three rules: floor absolute; climb to a STATED ceiling
(mathematical / capability / price — the capability ceiling is
unforgeable construction, blocked on reference-level visibility: the
keyword set has no private/sealed/opaque); reported rung == measured
rung, lens-checked for inflation and stalls. Includes the specimen table
(the session's classes placed, cross-representation == as the exemplar
full climb) and the non-goals roster (external reality, arbitrary
predicates, budgets, optimality, self-governance, byte-identical
self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain
current_rung / ceiling / next_rung_trigger.

All five doc-reachability witnesses re-run green by execution after both
file changes.

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

* WIP: compiler correctness

* WIP: compiler correctness

* Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section

Corrections, each verified against main before adoption:

1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record
   specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque
   ... every proof-carrier is presently forgeable") was false as stated;
   corrected to an audited-status claim: sole_constructor is the
   candidate wall, completeness for generic carriers unverified. The
   earlier keyword-set inference is withdrawn in the Sec 10 ledger.
2. Subject grain: rung honesty is measured at a declared acceptance
   boundary; a class's rung is the MINIMUM across in-scope paths (the
   interpreter refuses the mislabeled call that order_typed_call_args
   reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1
   carrier gains subject_grain/acceptance_boundary/compile_mode/
   realization_target/covered_population.
3. Seed rungs demoted: return/data/generic, field-through-generics,
   exhaustiveness, cardinality, full ==-class, and L4 all to
   UnknownUnmeasured (compile admission proven is not runtime
   disposition proven); census marked specimen-denominated; unknown-
   method R0 scoped to the interpretation path.
4. Dissolution on climb amended in DESIGN 4b: production handling
   dissolves; the RED + positive controls REMAIN enrolled as the
   evidence the higher rung stays real.
5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows +
   witness-test fixture migrated); the guarantee-recovery row now
   carries BOTH anchors typed, not one typed + one in prose. Carrier
   note records that List admits [] — the exact cardinality gap the
   ladder tracks — with the doc-graph witnesses as the interim wall.
6. cardinality_fold_propagation_test relabeled everywhere as manual
   value-level specimens (length homomorphism over literals + runtime
   refine_byte); "not new design" softened to the accurate scope
   statement; the roadmap cardinality node re-briefed accordingly.
7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a
   generic dimension mechanism; extension-vs-redesign is an open audit
   question that roadmap pricing must carry.
8. Sec 1 "was not built" -> "never completed as an exhaustive
   acceptance contract"; Sec 11 queue updated (correctness-dimensions
   done; sole_constructor completeness audit added).

Additions (operator direction): ROADMAP gains the "Guarantee ladder —
climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes
in ticket format with dependency edges (probe corpus gates the four
floor walls; carrier gates cardinality slice, emitters, prevalence;
exemption removal gates on the call-shape + inhabitance walls). The
capability node is the sole_constructor completeness audit. State-vs-
work split recorded on the carrier: rung STATE lives in the Stage-1
claims carrier and is emitted (ladder-census-emitters node); roadmap
nodes track CLIMBS.

Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md
projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap
authority 35/35, model 9/9, focus 12/12.

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

* Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control

review 45336 was correct: works had a typed carrier and zero readers —
representation without a consumer is specification-without-execution
(DESIGN 5 / E-10), the exact defect class the guarantee analysis
documents, reproduced in its own fix.

Consumers now executing in dag/test/claim/doc_reachability_witness_test:
- doc_graph_binds_works_all_nonempty — an emptied works list reds
- doc_graph_works_refs_carry_symbols — a ref stripped of module_path or
  decl_name reds
- guarantee_recovery_bind_pins_both_anchors — deleting or renaming
  either of the two anchors (module_skips_direct_call_arg_check,
  solve_constraints) reds; row multiplicity pinned to one
- doc_graph_works_empty_red_control — synthetic empty-works bind fails
  the predicate, proving the consumer discriminates

Predicates live on the authority (gunbc.doc_graph_roots) so the witness
consumes the carrier's own definition. Residue named on the carrier
note: staleness against the live tree (a ref naming a decl that no
longer exists) is NOT witnessed — v1.compiler.* is outside the witness
compile pool, so ref-vs-tree resolution is exactly the
feature:cited-symbol-resolution lens DESIGN 3 already names; the refs
are symbolic citations and inherit that trigger.

All 11 doc-reachability witnesses green by execution.

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

* De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census

review 45349, third correct catch in this lane: the census demoted
method existence (R0 interpretation-path-only), inhabitance
(UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the
roadmap nodes, authored before the demotion pass, kept "R0 -> R2"
headlines, re-inflating the same claims the same day at the canonical
authority. The section's own note says rung STATE lives in the claims
carrier, never these nodes; the headlines now name only the TARGET rung
and point at the census for current state, per DESIGN 4b's
minimum-across-paths rule.

ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35;
drift witnesses 4/4, by execution.

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

* WIP: compiler correctness

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored

Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and
tidy-deer-730's measured receipts:

- guarantee_ladder_section() deleted; 16 nodes + 23 edges enter
  declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/
  guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until
  closing contracts). Page visibility is the typed focus policy (lane added to
  roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED.
- Graph corrections: probe corpus → carrier → baseline-prevalence → walls;
  prevalence split baseline/residual; new floor-generic-field-constraint-wall and
  floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the
  general method wall (measured: kernel algebra profiles vs interpreter dispatch fork,
  tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability
  node repointed off the parked visibility-grants doc.
- Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to
  the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across
  paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the
  roadmap node (review 45367); five recovered vocabularies kept orthogonal.
- HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable);
  empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows
  merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED.
- Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser
  silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger.

Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8,
doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet.

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

* WIP: compiler correctness

* Trim the three over-budget ladder briefs to the operator's 100-word ticket law

witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier,
method-existence, and cardinality briefs ran 169/128/111 words. The old
section-local placement had escaped this law entirely (the exact
ghost-universe defect the verdict named — the budget never saw those nodes);
in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut
fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2
amendment / the census), which each node links as its carrier. The budget
itself is untouched — widening the declaration to satisfy the check is the
DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean.

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

* WIP: compiler correctness

* Containment predicates consume doc_all_nodes, the one canonical walker (review 45412)

document_rendered_nodes was a traversal fork beside roadmap_spawner's
doc_all_nodes — same semantics, second walker. The predicates (whole-value
ghost count + both RED probes) move INTO roadmap_spawner, the walker's
module, because the spawner already imports roadmap_authority and the
reverse import would cycle. The authority sheds the walker and its
now-unused SectionElement imports; the containment note records both
refused first cuts (identity-only membership, review 45406; the duplicate
walker, review 45412) since each was this wall violating a law it
enforces. Authority 38/38, spawner 16/16, page 28/28.

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

* Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door

Executes all six items of the operator's post-merge verdict on #7489, each
verified against live state first (#7484 and #7485 confirmed OPEN; the anchor
confirmed as the #7489 squash; Behavior confirmed six-membered):

1. Every "#7484 landed" claim replaced with open-candidate wording — main's
   disposition stated separately from candidate branch evidence (the ladder's
   rung-inflation rule applied to open-PR state; my transcription error).
2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed,
   reproducible after in-flight merges; walls no longer race a live tree).
3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary,
   evidence} — typed/located/counted but still Accepted; specimens
   MethodExistenceUndecided and GroundingNotDerived.
4. Graph: floor-parse-formation-wall + floor-record-construction-wall +
   compiler-accepted-obligation-closure added; v2-phase-carriers split into
   five staged nodes (self-grounding frontier → Translate refusal → inferred-
   tree completeness → per-kind derivation coverage → target realization gate)
   with the registry's FIRST TOMBSTONE (superseded_by the frontier node);
   method←join edge deleted per the zero-via-union nuance (join gates only
   the >1 wall and realization completeness); residual reroutes through the
   closure door.
5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors,
   matching v2.std.node.Behavior (the decidability denominator).
6. §1d provisional guarantee grid emitted as hand-authored interim,
   dissolve-on the carrier-emitted projection.

Witnesses: authority 38/38, identity 9/9 (first tombstone passes the
count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23
ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11.
ROADMAP.md and DESIGN.md regenerated via main_wet.

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

* WIP: compiler correctness

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Route the ambiguity wall and cardinality seam through the closure door (review 45545)

The first edge set let compiler-accepted-obligation-closure land while
floor-method-ambiguity-wall and cardinality-vertical-slice stayed open —
the door would have certified "every required judgment established" over
two required-open judgments (the grid marks the cardinality seam P0.2
minimum-R2 and ambiguity part of resolved identity; the verdict's spine
routes ALL P0 obligations through the door). Both are now prerequisites
of the closure; residual prevalence depends on the door alone. Authority
38/38, focus 12/12, page 28/28, drift 8/8; regen clean.

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

* Reconcile the sec-7b behavior-count passage to past tense (review 45558)

Sec 7b still described the 5-behaviors drift as current after this PR
corrected the authority — the stale-claim problem the PR closes elsewhere.
The passage now records the drift as found-and-corrected, keeps the
specimen's evidentiary value (the denominator drifted silently in prose),
and leaves the Match-promotion adjudication question with the queue.

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

* WIP: compiler correctness

* Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement)

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

* WIP: compiler correctness

* Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract

The compile seam was silent on both classes call_function_inner refuses at
runtime, and the emitter reordered mislabeled args positionally — two
realizations of one program disagreeing silently. direct_call_shape_diags
(v1.compiler.infer) closes both, blocking, exemption-free (a label has no
representation gap). Census before landing refused 28 live rename fossils in
5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list
init->empty, path->path_opt), all relabeled to their declared authority; +3
fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled
ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0,
whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with
triggers (interpreter-first parity pair next). Roadmap node + census rows
amended; ROADMAP regenerated.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Roster the call-shape witness blob in the scaffold index (review 45655)

ct_call_shape_wall_witness_test joined compiler_tests_rust without its
LanguageSourceScaffoldRow, so the exact-equality enrollment witness
(compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered)
would red on CI. Row added with the same hand-assertion scaffold trigger as
its peers and enrolled in the roster; witness re-run green by execution.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes

d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster,
dropping the shape check its enrolled negative control pins — Symbol<Float>
became BTreeSet-eligible by name, and the RED sat invisible for ten days
because the Rust unit suite left CI on 2026-07-11. Childless gate restores the
shape constraint (zero corpus impact; regen fixed point holds); incident +
dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9
(operator decision, priced by this incident). Found by tidy-deer-730 during
the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Dedupe the call-shape witness aggregator entry after the main merge

The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test
into compiler_tests_source(); a duplicate generates the #[test] twice.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door

Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap
authority and the gap analysis:

- ladder-measurement-schema precedes probes AND carrier (the receipt protocol
  both meet through; breaks the probes/carrier protocol cycle).
- The three merged P0 slices recut at their actual grain, identities
  tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted,
  #7519) + missing/duplicate + signature-resolution siblings;
  floor-method-existence-wall -> method-established-surface-wall (accepted,
  #7484) + receiver-normalization + zero-resolution siblings;
  floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted,
  #7484) + grounding + general-wall siblings.
- The Accepted door split mechanism/floor/extended
  (compiler-accepted-obligation-closure tombstoned): the audit form lands
  with the carrier; refusal never turns on over a known-open judgment
  (review 45545's substance preserved in the activation nodes).
- Exemption removal re-grounded on argument-type-compatibility grounding +
  declared-conformance grounding (labels never gated it).
- guarantee_ladder_edges rewritten wholesale; emitters parallel with the
  baseline; baseline defined as a two-revision execution.
- Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b);
  stale dissolution triggers repointed (doc_graph_roots,
  doc_reachability_witness_test); tombstone-note staleness fixed.
- ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS
  (brief budgets, edge endpoints, acyclicity, identity registry with five
  tombstones); regen_stage0 --verify divergence 0.

The branch additionally carries the ord-eligibility silent-red repair
(childless gate on name-grain arms + incident note) and the clean regen of
the generated stage0 files after the origin/main merge.

Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference
diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag
(landed with #7508, byte-identical to origin/main; handed off to the
occurrence lane).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Recut the extended activation as per-class admissions (review 45918)

The first cut kept requires-all edges on one extended-activation node while
its prose promised class-by-class widening — the graph would have deferred
every admission behind the slowest climb, preserving the monolithic deferral
the door split dissolves. Now: four per-class admission nodes
(extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate,
each <- floor-closure + its own climb, ready the day that climb lands) and
accepted-extended-obligation-closure recut as the terminal
roster-completeness certification, where requires-all honestly belongs.
Same closure identity (no slug change, no tombstone); four fresh identities
minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP
regenerated; graph/budget/identity witnesses 26 PASS.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Trim the ord name-grain note to its structural constraint (review 45929)

The in-code note duplicated the incident narrative the gap analysis already
records (sixth-pass ledger + queue item 9) — a parallel ledger realized into
the emitted seed with no executable consumer. The carrier keeps only the
constraint the code cannot show: why name-grain arms admit childless nodes
only, the discriminating RED's symbol, and the shape-examining sibling path.
regen_stage0 divergence 0.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Spine A Stage 0: the guarantee measurement schema — evidence identifies its subject before anyone measures

gunbc.guarantee_measurement carries the vocabulary probes and claims meet
through, and nothing else (roadmap node ladder-measurement-schema; operator
spine verdict 2026-08-01): GuaranteeClassId/PathId/ProbeId brands;
GuaranteePath over four closed minimal axes (subject grain, acceptance
boundary incl. the InferToEval/InferToTranslate phase boundaries the
containment workstream consumes, compile mode, realization target with
GuaranteeTargetName deferred-grounding brand); GuaranteeMeasurementReceipt
with every field required (subject_revision x harness_revision x
probe_set_digest, reusing std.types.CommitSha and std.content_hash);
ProbeObservation as the raw outcome sum with ProbeNotRunnable structurally
separated from verdicts (top-as-ignorance never readable as pass/fail);
exactly-one path resolution and a receipt->path join that refuses unknown
and duplicate. Registry mechanism without a registry population - no probe
executes, no class rows, no disposition, no rung.

An initial ObservedOutcome name collided with gunbc.output_policy's
process-outcome type (whole-tree census caught the bare-reference break);
renamed to ProbeObservation, census back to 0 blocking.

Receipts: 8/8 synthetic-row witnesses green by execution (round-trip join,
unknown-path refusal, duplicate-registry refusal never-first-pick,
exactly-one resolution across four boundary variants, both uniqueness REDs,
digest input-determinism incl. order sensitivity, verdict/ignorance
separation); whole-tree compile 0 blocking; regen_divergence_count=0;
generated artifacts zero drift.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Record the second-consumer re-grounding trigger for observed_is_verdict (review 46075)

The predicate/walker dissolution rule triggers where a canonical fold
already exists (nat_cata) or a substrate walk is extended; neither holds
for a freshly declared domain sum whose only query this is. The note now
records the named trigger: when the claims carrier lands as the sum's
second consumer, a probe_observation fold becomes the canonical surface
and observed_is_verdict re-expresses through it.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Grant publication for the eight ungranted #7544 files (main-side gate breakage)

The publication gate reds on current main itself: #7544 (heal-revalidation)
merged after the P-B wall landed via #7560 but its CI raced the wall, so
its eight new files carry no PublicFilePublishGrant rows and every PR
merging current main inherits the failure. Rows added for all eight
(mechanical placement declarations for files already public on main);
cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses
green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Grant publication for the three ungranted #7563 files (second main-side race)

Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall
CI run, adding three SCM-kernel files with no grant rows. Roster now
covers the full cutover..HEAD set including current main.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Thread GuaranteePathId through resolution and its refusal variants (review 46179)

The resolver's key and both refusal-variant payloads carry the brand
end-to-end; join_receipt_to_path no longer erases receipt.path to String.
Measured the enforcement honestly: two executed controls show the checker
accepting a bare String at a branded parameter and a branded record field,
so the note records this as model-correctness and erasure-removal, with
brand acceptance-enforcement handed to the probe corpus as its own class.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Merge origin/main; dedupe the roster union and grant the two #7550 lean files

The alphabetized roster body on main already carried the 11 straggler
paths, so #7580's tail block duplicated every one of them; the union
keeps exactly one row per path, with this branch's two guarantee rows
slotted alphabetically. Coverage against the cutover then caught a
fourth race instance: #7550 merged two new files with no grant rows
(dag/extdeps/languages/lean/overflow.dag and its witness), redding
main's gate again - swept into the same roster here.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Observation counts are Nat, with the enforcement gap measured (review 46287)

RefusedTyped.count and AcceptedCounted.count carry the cardinal type,
and the fold's arm signatures follow. An executed control shows the
checker still accepting a negative at the Nat field today, so the note
records the swap as model-correctness with refusal owed to the
numeric-refinement acceptance class, not claimed as a wall.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Orthogonalize the path axes instead of enumerating families (review 46308)

InterpreterRun renames to RuntimeRun: run-level acceptance happens IN
the path's realization, so which runtime is the realization axis's
fact and an emitted-run path (the divergence probes' subject) is
expressible rather than contradictory. The compile_mode axis deletes:
every landed control derives its pipeline from its boundary, so the
stored mode was a second representation whose only writable novelty
was the contradiction; it returns as a stored axis with the first
path measured under two pipelines at one boundary. Both review-named
contradictions are now unwritable without a family coproduct, whose
rows would restate the orthogonal axes per combination (the N-by-M
shape DESIGN 2 folds into axes).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* Roadmap: schema acceptance receipt, axis-prose repair, probe-adequacy mandate

Three post-merge obligations from the ladder-measurement-schema landing
(gunbc#7572, merged 2026-08-01):

- RoadmapAcceptanceReceipt for ladder-measurement-schema: executed
  red-control (duplicate_class_id_reds_uniqueness) + delivered handback
  (the schema module and its witness), criteria digest pinned over the
  corrected boundary text; the node leaves the active graph and the
  probe corpus promotes to lane top.
- Axis-prose repair (snappy-eagle's prose-grep rule): the schema and
  carrier boundaries plus gap-analysis sec 12 no longer name the deleted
  compile_mode axis; each records the RuntimeRun re-read and the
  deletion's re-entry trigger instead (review 46308 on gunbc#7572).
- Probe-adequacy mandate in guarantee-baseline-prevalence red_control:
  closure AND shape AND corpus-prevalence cross-check REQUIRED for every
  below-floor or silent-class row; a row without its adequacy receipt is
  unenrollable.

ROADMAP.md regenerated via main_wet on the artifact gate; roadmap
authority suite 39/39 by execution.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Reconcile the schema node's acceptance bar to what Stage 0 owns (review 46861)

The red_control claimed receipt-field unwritability - a wall that was
never this node's to claim: corpus-wide construction enforcement is the
floor-record-construction-wall class's bar, exactly as the module's
receipt_identity_note states. The bar now says required-by-shape with
enforcement explicitly delegated, the criteria digest re-pins over the
honest text (74da4d8be7125c81, derived by execution), and the receipt
stands on the executed duplicate-id control. Also removes a stray
digest-probe test fn a background sweep had committed mid-measurement.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

* WIP: compiler correctness

* Trim claims-carrier boundary under the 100-word ticket-brief budget; drop probe scaffolding

The compile_mode de-reference added in this PR pushed the ladder-claims-carrier
boundary to 101 words, redding witness_ticket_brief_budget_holds_and_reds (the
enforcing witness for the boundary budget — CI batch 3). 'the landed ... row'
reassurance prose becomes 'per gunbc.guarantee_measurement' (98 words); the
single-authority pointer survives. ROADMAP.md regenerated. Also removes the
transient probe_brief_violations diagnostics fn the autocommit sweeper captured
(review 46970).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

---------

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>
Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 2, 2026
ci_heal_job_permissions carried actions: PermWrite for exactly one consumer --
github.Workflows.CreateDispatch, which the heal job invoked to revalidate the
head it had just pushed (#7544). That dispatch is deliberately not restored in
this cut, so the job was emitting `actions: write` for a capability it does not
exercise: a standing control-plane grant held in anticipation of a follow-up that
may never land. The credential surface should describe what the job DOES.

Now `contents: write` / `actions: none`. Where the grant comes back, when it
does: with the dispatch consumer, as that consumer's own carrier, at the point it
becomes reachable -- rather than pre-granted here where the follow-up would land
against a permission nobody re-derived.

VERIFIED NOT TO MOVE THE PLAN'S VERDICT, which is the thing this edit could have
changed silently: the auto-push versus author-commit split is still exactly the
three workflow projections refused and 33 paths staged, and the refusal cause is
still ActionsJobCredentialScopeUnavailable -- that split turns on the `workflows`
axis, not on `actions`.

Also merges current main (8e025f8; the design-ledgers split into
design-failure-modes.md and design-rung-drops.md), and re-derives the projection
against it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XVcFN21urwK3LttBSF6EWK
briansrls pushed a commit that referenced this pull request Sep 2, 2026
… emission (#10118)

* MAIN-H: restore the generated-artifact heal job as a modeled workflow emission

The heal capability died with `ci.yml` in the 2026-08-15 floor cut
(gunbc.rung_drop floor_cut_heal). Everything the job DOES survived that cut
unconsumed -- gunbc.heal_push_plan decides per artifact whether the Actions job
credential may advance its path, gunbc.ci_spec renders the git config / drift
census / staging / commit / push script from that decision, and
gunbc.ci_heal_credential models the checkout step whose persisted credential is
the push authority. What did not survive was a WORKFLOW emitting a job that
binds them, so the whole model was a check with no consumer.

This lands that consumer as a job of gunbc.witness_floor_workflow, the
repository's only CI workflow authority, rather than as a restored second
workflow file: witnesses.yml is already a registered generated artifact, so no
GeneratedArtifact variant or registry row is needed and DESIGN's "CI is one
emission" is preserved.

FOUR ARMS OF THE HISTORICAL JOB ARE ABSENT BY CONSTRUCTION, NOT BY DELETION.
The skew guard, its automatic merge remedy, the `checkout --ours` conflict arm
and the ~200-path hand-maintained `:(exclude)` roster all existed to manage one
defect: the old job's binary came from a job that checked out the MERGE ref
while heal checked out the BRANCH HEAD, so the two could name different
revisions of src/v1 (incident 2026-07-29; #7392, #7394, #7395). This job builds
its own `gunbc` from the SAME branch-head checkout it then regenerates, in one
job, so binary and tree are one revision and there is no second revision to skew
against. DESIGN 4b: the class moves from rung 2 to rung 4, and the arms dissolve
with the climb. Two of them would also be defects to restore -- taking the ours
side is what the generated-artifact merge driver now refuses to do, and the
roster was a second authority for a fact gunbc.generated_artifact owns. The
auto-push-versus-author-commit split is derived from that registry instead.

THE PUSHED HEAD IS NOT REVALIDATED AND THE JOB SAYS SO. An Actions-credential
push starts no workflow run, so after a heal the PR's checks describe the prior
head. tools.ci_heal_dispatch targets `ci.yml`, which does not exist, and
witnesses.yml declares no expected_healed_sha input -- dispatching without it
would fabricate a revalidation rather than perform one. The job instead prints
SupersededByHealedHead naming both revisions and exits nonzero. The gap is
declared in the emission and its trigger names the capability (a dispatch input
the run binds github.sha and its checkout against), not an artifact.

The job carries no lane and no `needs` edge of the required `witnesses`
aggregate: heal REMEDIATES, the build lane's generated-artifact phase
ADJUDICATES. Making a remediator a gate would let its own nonzero arm block the
branch it had just repaired.

Also repaired: ci_heal_credential's ci_heal_job_ref and ci_heal_workflow_ref
were DeclarationRefs to the deleted gunbc.ci_workflow, so the grant deciding
whether the heal push is authorized was computed against a workflow and a job
with no existence. They now name the emission that carries the job.

floor_cut_heal is NOT retired here. Its trigger demands the capability observed
writing and pushing on a real divergence; an emission that typechecks is not
that observation.

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

* Fix two defects the floor's parse phase and the citation-debt roster caught

BOTH ARE MINE AND BOTH WERE INVISIBLE TO THE INSTRUMENT I HAD BEEN READING.

(1) SOURCE ANNOTATION AT THE WRONG GRAIN. The comment explaining why the heal
regen step is capability_neutral sat INSIDE the WitnessFloorBoundStep record
literal. DESIGN 4c models annotations at module-item grain only, so the floor's
parse phase refused with nine located diagnostics and zero witnesses ran. The
reasoning is preserved verbatim, hoisted above
heal_generated_artifacts_bound_steps where it is authorable.

WHY IT REACHED CI: `gunbc run ... main_wet` returned 0 over the whole tree and I
read that as "the tree typechecks". It is not that check -- the annotation-grain
rule executes in compile-clean and in the floor's parse phase, neither of which
main_wet runs. A green from an instrument that does not cover the class is not
evidence about the class.

(2) SPENT CITATION-DEBT ROWS. Repointing ci_heal_job_ref and ci_heal_workflow_ref
at gunbc.witness_floor_workflow made their PRE_EXISTING_CITATION_DEBT rows in
declaration_index.rs stale: the citations no longer refuse, and that roster only
shrinks, so the rows are deleted. Found by running v1_src_dag_parse, which
reports it directly -- not by CI, which had not reached it yet. It would have
been the next red.

The second one is the reason to go looking for a covering instrument after a
failure instead of repairing only the line the failure named.

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

* Drop the heal job's `actions` permission: its only consumer is not built

ci_heal_job_permissions carried actions: PermWrite for exactly one consumer --
github.Workflows.CreateDispatch, which the heal job invoked to revalidate the
head it had just pushed (#7544). That dispatch is deliberately not restored in
this cut, so the job was emitting `actions: write` for a capability it does not
exercise: a standing control-plane grant held in anticipation of a follow-up that
may never land. The credential surface should describe what the job DOES.

Now `contents: write` / `actions: none`. Where the grant comes back, when it
does: with the dispatch consumer, as that consumer's own carrier, at the point it
becomes reachable -- rather than pre-granted here where the follow-up would land
against a permission nobody re-derived.

VERIFIED NOT TO MOVE THE PLAN'S VERDICT, which is the thing this edit could have
changed silently: the auto-push versus author-commit split is still exactly the
three workflow projections refused and 33 paths staged, and the refusal cause is
still ActionsJobCredentialScopeUnavailable -- that split turns on the `workflows`
axis, not on `actions`.

Also merges current main (8e025f8; the design-ledgers split into
design-failure-modes.md and design-rung-drops.md), and re-derives the projection
against it.

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

* EVIDENCE PROBE: hand-edit a generated projection without regenerating it

DELIBERATE DRIFT, and the only commit on this branch that is meant to be undone
by a machine rather than by me. gunbc.rung_drop floor_cut_heal retires on one
thing: the heal capability OBSERVED writing regenerated bytes back and pushing
them, on a real divergence. An emission that typechecks and a green no-drift run
establish neither.

THE SUBJECT IS CHOSEN, NOT CONVENIENT. docs/plans/input-envelope-roadmap.md is
auto-push-eligible, verified against the emitted script itself rather than
assumed: it carries a `git add` line and does NOT appear in the
AUTHOR_COMMIT_DRIFT population. The three workflow projections would have been
the wrong subject -- they deliberately select AuthorCommitRequired, so drifting
one exercises the bundle-and-refuse arm while LOOKING like a heal run and would
have told me nothing about whether this job pushes.

PRE-STATE, recorded here because the receipt is worthless without the base it is
a claim about: the clean file is 3555 bytes, sha256
4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead.

EXPECTED, written before the run so the result cannot be read to fit: the
generated-artifact phase in the build lane goes RED on this commit (it
adjudicates, and this tree is genuinely not at its fixed point); the heal job
regenerates, stages exactly this path, commits as gunbc-ci-auto-heal, pushes to
this branch, prints HealProduced with both heads and CHANGED_ARTIFACTS naming
this file alone, then prints SupersededByHealedHead and EXITS NONZERO because
nothing has revalidated the head it just created.

If instead it prints HealNoChange, or HealAuthorCommitRequired, or exits zero,
the capability is not what this PR claims and the rung-drop row stays exactly
where it is.

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

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Retire floor_cut_heal on an observed repair, and let the ledger say so

TWO CHANGES, COUPLED: the retirement, and the rendering repair without which
the retirement is invisible at the surface DESIGN sends readers to.

THE RETIREMENT, ON EXECUTION AND NOT ON THE EMISSION. floor_cut_heal's trigger
is a capability: a required-run consumer that, on a branch head whose committed
generated artifacts diverge from their authorities, writes the regenerated bytes
back and pushes them under a credential the repository already models --
observed doing so on a real divergence, not merely emitted.

  PROBE  330c74f hand-edited
         docs/plans/input-envelope-roadmap.md, a generated projection,
         3555 -> 3754 bytes, and did not regenerate it. Pre-drift sha256
         4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead,
         recorded BEFORE the drift. Subject chosen against the emitted script
         rather than assumed: it carries a `git add` line and is absent from the
         AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm. The three
         workflow projections would have exercised bundle-and-refuse while
         looking like a heal run.
  RUN    33683175090 job 100433326005:
         HealProduced prior_head=330c74f07 healed_head=bc70468754
         changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one
         path, no blast radius across the other 32 auto-push rows -- then
         SupersededByHealedHead and exit 1.
  PUSH   branch head moved to bc70468,
         authored gunbc-ci-auto-heal, 1 file changed, 2 deletions.
  IDENTITY, two ways: the healed file is byte-identical to the pre-drift digest,
         and a clean source-built regeneration ON the healed head changed zero
         files. src/ and dag/ are identical between that head and the tree the
         binary was built from, so there is no compiler/tree pairing assumed.

The predictions were written into the probe commit before the run, so the result
is not a story fitted to an outcome. Restored rung: 2. NOT restored and not
claimed: revalidation of the head heal creates, which keeps its own capability
trigger. floor_cut does not move -- its conjunction is derived by
standing_rung_drops(), so it follows this row without being edited.

THE LEDGER COULD NOT EXPRESS A RETIREMENT, which is why it is repaired here
rather than deferred. gunbc.design_ledgers read subject/declared/authored and
never read `standing`, so all four retired rows -- including three that predate
this PR -- rendered under headings spelled identically to the live ones, and
trigger_fired was rendered nowhere. A reader counting outstanding safety
regressions in the file DESIGN points them to counted retired ones among them.
Rendering only: no model state moves, and standing_rung_drops remains the
authority anything joins against.

ACCEPTANCE TEST, a membership join and not a count, since a count can agree
while the sets differ: subjects rendered without the retired marker in
docs/design-rung-drops.md == subjects whose rows carry standing: Standing in
gunbc.rung_drop. PASS at identity grain, 18 standing and 4 retired, both sets
equal, LC_ALL=C pinned on both sides after locale collation alone produced a
false difference. SHOWN TO DISCRIMINATE rather than asserted: un-marking one
retired heading makes it go red with one extra subject.

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.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.

1 participant