Repository navigation
P3b PR2 overflow semantics - #7550
Merged
Merged
Conversation
|
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. |
Contributor
|
Addressing review 45945 (REQUEST_CHANGES): OverflowUndefined fabrication (lean.dag): Fixed in Parallel Parser scaffold note updated per operator ruling — sent from crisp-seal-116 |
Contributor
|
Follow-up — sent from crisp-seal-116 |
Contributor
|
Addressing review 45964 (REQUEST_CHANGES): replaced mis-copied — sent from crisp-seal-116 |
Contributor
|
Addressing review 45979 (REQUEST_CHANGES): — sent from crisp-seal-116 |
Contributor
|
Addressing review 45997 (REQUEST_CHANGES): — sent from crisp-seal-116 |
The multi-line data declaration for lean_catalog_fixed_width_overflow tripped the v1 parser (expected expression, found Newline); collapse it to one line. Regenerate stage0 after dag/std/integer.dag gains IntegerOverflowSemantics<E>. Co-authored-by: Cursor <cursoragent@cursor.com>
Root-cause the CI parse error: v1 parse_let/parse_data_after_kw call parse_expr without skip_newlines after '=', so a next-line initializer hits expected expression, found Newline. Reproduced on witness test line 32 and lean.dag data decl line 215 — not generic multiline-ness. Single-line initializers remain with a declared scaffold note naming the deficit. Co-authored-by: Cursor <cursoragent@cursor.com>
…notes. Overflow semantics live on LeanIntegerScalar only — BoolScalar and width-refused rows no longer fabricate OverflowUndefined (review 45943, 45945). Expand lean_overflow_parse_continuation_note per operator ruling: both parse_let arms, 02_parse.dag authority, parse_return sibling suspect. Strengthen std_integer_overflow_semantics_note for bounded parallel-authority deferral with named dissolve-on. Co-authored-by: Cursor <cursoragent@cursor.com>
Multi-line &&/!= continuations hit parse_expr prefix (expected expression, found Ne) — same parse_let continuation class. Collapse discriminating comparisons to one line. Bind overflow: _ in lean_scalar_algebra_inhabitance after LeanIntegerScalar gained the field. Co-authored-by: Cursor <cursoragent@cursor.com>
Review 45964: feature:content-hash-family-grounded-shaped was a mis-copy from the ContentHash open thread. Enroll feature:overflow-disposition-defork so the parallel OverflowDisposition debt is grep-discoverable. Co-authored-by: Cursor <cursoragent@cursor.com>
Review 45979: route catalog construction through lean_admit_fixed_width_overflow_semantics; LeanIntegerScalar.overflow is now the sole_constructor admitted carrier, not raw semantics. Overflow refusal stops at LeanOverflowAdmissionRefused (parallel to width refused). Co-authored-by: Cursor <cursoragent@cursor.com>
Review 45997: LeanWidthAdmissionRefused and LeanOverflowAdmissionRefused return Absent from lean_scalar_algebra_inhabitance_optional instead of fabricating BooleanAlgebra inhabitance. lean_model_core_inhabitance_decls folds only Present declarations. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot
Bot
force-pushed
the
session/crisp-seal-116
branch
from
August 1, 2026 06:15
de3de33 to
2c8a263
Compare
Downstream consumer that distinguishes E today: lean_overflow_semantics_node
(spec-facts projection) — content_hash differs when substituting Panics for
Traps. Admission still collapses OverflowRaises { effect: _ } (witness asserts
trap refused with same reason as panic). Remove cosmetic tag != test.
Co-authored-by: Cursor <cursoragent@cursor.com>
lean_overflow_raise_effect_admission_debt_note names dissolve-on trigger feature:lean-overflow-raise-effect-admission for per-E admission when a Lean surface admits OverflowRaises. Witness records collapse as evidence. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
|
Addressing review 46041 (codex REQUEST_CHANGES) in Finding 1 — ungrounded upstream overflow fact Fixed. Added Finding 2 — positional citations in scaffold receipt Fixed. — sent from crisp-seal-116 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…an 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>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 1, 2026
Merged
briansrls
added a commit
that referenced
this pull request
Aug 1, 2026
* WIP: srv1 work
* Compile pool as an explicit budget row; per-slot caps no longer assumed to bound compile RSS
sccache executes cache-miss compiles as CHILDREN OF THE SERVER, so compile RSS is
charged to the server's cgroup, not the slot that issued the compile. A per-slot
memory cap therefore does not bound compile memory. Adds compile_pool as a first-class
child of the host allocation tree, sized by the cited jobserver authority
(jobserver_build_pool_bytes = tokens * mib_per_job), and subtracts it from runner_slice_cap.
Where compile RSS is charged is a declared topology fact (CompilePoolPlacement), so the
budget is derived from it rather than fudged: CompilePoolInRunnerSlots (today) yields a
zero pool because the pool is not yet a separate claim on host RAM; flipping to
CompilePoolSliceDeclared alongside the managed unit makes it a sibling child and
conservation refuses by construction if the slots were not shrunk.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* Realizer observes placement: stats-ok alone is no longer a success exit
* Fix unbalanced if in emitted provision script (read-back never closed its fi)
* DESIGN: record placement-as-verdict-axis and the compile_pool budget row
* WIP: srv1 work
* Regenerate DESIGN.md; tidy match-arm indentation
* WIP: srv1 work
* Fix review finding: missing compile_pool arg + de-fork the compile-pool authority
Two fleet_host_budget_tree test callers were not updated to the new signature
(review 40934). Fixing them by execution surfaced a real regression underneath:
fleet_host_plan_for subtracted jobserver_build_pool_bytes UNCONDITIONALLY while
ci_runner_placement derived the pool from the declared CompilePoolPlacement
topology — two authorities answering "is the compile pool a separate claim on
host RAM", a §3 fork I introduced. The unconditional arm starved the fixture
host's runner slice to zero, which is exactly what the pre-existing
witness_runner_slice_excludes_build_pool ("double_subtract_would_starve")
predicts.
Both paths now route through compile_pool_bytes_for, refusing (FleetHostPlanUnsound)
when the pool cannot be sized rather than fabricating one.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* WIP: srv1 work
* Placement probe: refuse on ambiguity instead of picking an arbitrary sccache process
Review 40959 (non-blocking): pgrep -x sccache also matches CLIENT invocations —
under RUSTC_WRAPPER every in-flight compile has a process named sccache — so
head -1 could read a transient client's cgroup and produce a FALSE refusal.
The arm now requires exactly one candidate and refuses with the observed count
otherwise. This observation runs at provisioning/converge time when no compile
should be in flight, so exactly-one is the expected state and >1 is genuine
ambiguity.
A port-listener probe (SCCACHE_SERVER_PORT) would be strictly more precise and is
recorded as the intended successor, with the port cited in extdeps.cache.sccache.
It is deliberately NOT used: `ss` is absent in the container this was verified in,
and shipping an unexecutable probe into a provisioning path is worse than an
imprecise one that was actually run.
Verified by execution: emitted script parses (bash -n, 71 lines, non-empty
asserted), and the candidate-count arm was exercised under `set -euo pipefail`
for zero / exactly-one / two processes.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
* WIP: srv1 work
* WIP: srv1 work
* WIP: srv1 work
* Resolve the #7019 revival merge; keep placement at the model grain
The dashboard auto-committed mid-merge, landing conflict markers in four
files. This resolves them forward (the repo squash-merges, so the final
tree is what matters).
Resolutions:
- extdeps.cache.sccache: kept both sides. Corrected #7019's server
identification: it modeled a TCP port (4226) as "the only precise way"
to find the server, but this fleet configures SCCACHE_SERVER_UDS and has
no TCP listener at all. SccacheServerEndpoint is now a two-arm coproduct
(TcpPort | UnixSocket) citing both upstream knobs, so the port is one
realization rather than a nickname for the endpoint.
- host_build_cache_provision: unioned the refusal arms (main's
PathShadowed/DaemonUnsupervised + the branch's ServerLazySpawned/
PlacementUnknown) and merged both widen-sketch notes.
- host_build_cache_provision_script: took main's version wholesale. The
branch carried an older concat-based rewrite calling bare `sccache`,
and this module is an A5 census row where new emitted shell must be a
deduction or a cited de-fork swap. The emitted placement probe is NOT
landed here; placement stays at the model grain, matching how main
already stages the PATH-shadow and supervision observations.
- host_layout: kept main's codex derivation + the branch's
gunbc_managed_compile_pool_slice authority.
- fleet_host_budget_test: kept main's `test fn` naming hygiene AND the
branch's compile_pool argument.
- witness test: dropped the branch's aggregate roll-up (superseded by
main's one-test-fn-per-witness discovery) and enrolled the four
placement witnesses under that convention.
- ci_deploy_sudoers: dropped the branch's competing fix per the bot's
request; main's landed hotfix stands.
- DESIGN.md regenerated from design_document.dag via main_wet.
Green by execution: the four placement witnesses return true; all touched
entries compile with 0 blocking errors.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: debug build flake
* WIP: debug build flake
* Placement observer: endpoint ownership, deployed-instance identity, live receipt
Step 1 of the ctrl -> gunbc host-control-plane subsumption lane. Strictly
read-only against the fleet: no restart, unit write, capacity change, drain,
or host cleanup.
ROOT CAUSE, confirmed live rather than inferred. srv1's CI cache endpoint
(/var/lib/ctrl/sccache-ci/server.sock) is held by pid 3975946, 31.2 days old,
whose cgroup is RETIRED runner slot actions-runner@srv1-10.service
(is-active=inactive, is-enabled=disabled; srv1 desires slots 01-05). Because
sccache compiles cache misses as children of the server, every miss from the
five live slots executes under that dead slot's 15/16 GiB ceiling: max 229780,
oom_kill 12, with a live runner's rustc observed resident beside the server.
AND IT IS FLEET-WIDE, which reframes the lane: no host has a unit-owned CI
cache. srv2's owner sits in active slot srv2-05, srv3's in active srv3-01.
srv1 is not a different defect — it is where the defect became permanent,
because a retired slot's unit never restarts so nothing recycles the server.
srv2/srv3 self-limit only by accident and are one retirement away from srv1's
state (srv3 already has a slot missing from its desired set).
Model (new authority gunbc.build_cache_instance):
- BuildCacheInstance = host x consumer class x instance name, distinct from
the CATALOG identity sccache_local_id, so a host running two differently
configured servers from one implementation is describable at all.
- ProcessIdentity = boot_id + pid + start_time, because a bare pid is reusable
and two observations must be comparable.
- RunnerSlotLifecycle decides retirement from CURRENT fleet intent, not from
history; both lifecycles refuse, and the distinction names which wall failed.
- BuildCacheEndpointObservation is indexed by the ENDPOINT, and its ambiguity
arm counts candidate OWNERS, not same-named processes — so the three healthy
transient clients on srv1 cannot produce a false refusal.
- BuildCacheServerPlacement moved here and gained arms. ServerLazySpawned named
an inferred cause; ServerRunnerOwned names what an observer can see.
gunbc.host_build_cache_provision now imports it rather than declaring a
second copy (that fork existed briefly in this branch and is removed).
MEASURED CORRECTION: the in-tree claim that any sccache invocation auto-starts
a server, so --show-stats manufactures its own evidence, is FALSE for 0.15.0.
Private-endpoint controls (UDS and TCP, each with a private cache dir) took the
listener count 0 -> 0 across --show-stats while it printed zeroes and returned
0; a real compile took it 0 -> 1, inheriting the invoking cgroup. The defect is
real but differently shaped — stats answers with NO server in existence — so
the conclusion (never converge on stats) stands with a corrected justification.
Fixed at extdeps.cache.sccache, host_build_cache_provision, and
readback_independence.
Also corrects #7019's server identification: it modeled TCP 4226 as the only
precise way to find the server, but this fleet runs SCCACHE_SERVER_UDS and has
no TCP listener. SccacheServerEndpoint is now TcpPort | UnixSocket.
Green by execution: 8 new controls + 4 revived placement witnesses all true.
Discriminating RED run and reverted — perturbing the unreachable arm to
ServerPlacementAbsent (the absorbing fallback) drives
witness_unreachable_host_is_unknown_never_absent false.
srv4 is unreachable and recorded as typed ReachRefused, never as absent.
Receipt: docs/plans/build-cache-placement-receipt.md
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Address review 46182: correct the stale managed_compile_pool_slice_note citations
The review flagged that the note cites ServerUnitOwned.slice_unit, which this
PR renamed and moved. Verifying it showed all THREE of the note's claims had
gone stale in one edit:
1. ServerUnitOwned.slice_unit -> ServerManagedUnitOwned { unit } in
gunbc.build_cache_instance, and placement is decided against the instance's
intended_unit (a service) rather than this slice.
2. 'the emitted shell greps the observed cgroup for it' — the script carries
ZERO compile-pool references; the branch's emitted placement probe was
deliberately not landed (A5 census row: emitted shell may shrink, not grow).
3. The two-consumer drift hazard and the import-cycle homing rationale were
both premised on that missing consumer.
Rewritten against the real consumers (build_cache_instance's two instance
constructors plus the provision-module fixture) and stating that nothing
provisions this slice yet, so the row is not misread as describing the fleet.
Also deletes srv1_stranded_server_cgroup_fixture, orphaned when its only
consumer moved to an inline RunnerSlotIdentity. It was additionally wrong:
it guessed ghrunner@srv1-10.service where the observed cgroup is
actions-runner@srv1-10.service.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Grant publication placement for the three paths this PR adds
Main landed the P-B publication placement gate (#7560) after this branch's
merge-base, so the three files added here reached CI with no roster envelope
and the gate correctly refused: AddedPathPublishGrantAbsent on
build_cache_instance.dag, build_cache_placement_observation_test.dag and
docs/plans/build-cache-placement-receipt.md.
These are ordinary public substrate and docs, so the fix is to declare the
grants rather than to touch the gate. The gate's own discriminating controls
stay green either way: added_granted_public_path_greens_gate and
added_ungranted_public_path_reds_gate both true.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: debug build flake
* Couple slot+lifecycle into a coproduct; dissolve the gate's second verdict mapping
Two findings from review 46217, both confirmed against the code.
EndpointOwnerObserved carried `unit` beside `owning_runner_slot:
RunnerSlotIdentity?` and `runner_slot_lifecycle: RunnerSlotLifecycle?`.
Three loose fields admitted states no observation can produce, and one of
them was live: placement_of_owner matched the slot first, so an Absent slot
carrying a Present lifecycle skipped the runner arm entirely and reached the
unit comparison, where a cgroup whose unit equalled intended_unit returned
ServerManagedUnitOwned. A runner-owned endpoint could be reported correctly
placed because two fields disagreed.
Replaced by EndpointOwnerContext = OwnerInRunnerSlot { slot, lifecycle }
| OwnerInSystemdUnit { unit } | OwnerContextUndecided { detail }. The
contradictory state is now unwritable rather than checked (DESIGN 4b/5,
construction over validation), and the unclassifiable cgroup gets a positive
arm carrying its own located reason instead of a half-filled record.
build_cache_provision_gate_accepts was a full second traversal of
BuildCacheDaemonObservation and, inside DaemonStatsOk, of
BuildCacheServerPlacement -- the same observation-to-verdict mapping that
provision_build_cache_verdict and placement_verdict already compute, written
twice with either copy free to drift (DESIGN 2/3). It now takes catalog_id,
calls the fold, and compares shapes: converged-vs-refused plus the refusal
cause via discriminant, leaving the located reason string as diagnostic
payload rather than contract. A placement arm added to the coproduct can no
longer be forgotten here, because there is nowhere left to forget it.
Green by execution: 42/42 witnesses across both modules, both entries
compile at 0 blocking errors. The new control
witness_undecided_owner_context_refuses_and_keeps_the_located_reason asserts
the replacement arm refuses and preserves the observer's reason; there is
deliberately no witness for the contradictory state, since the type no
longer admits it.
Also completes 2f1ff43, a mid-edit dashboard auto-commit that captured the
coproduct without its fixtures (review 46224).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: debug build flake
* Resolve roster conflict by dedup; grant #7550's two lean paths
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 1, 2026
…6281) Diff-grain sibling of tools.publication_placement_gate: refuses any freeze..HEAD-added dag/extdeps .dag file outside carriers-union- machinery (scope_placement_refused_paths, pure kernel on gunbc.extdeps_scope_frontier with hermetic RED/GREEN controls) and any frozen-manifest row naming a post-freeze-added file; diff failure and parse truncation refuse, never skip. Enrolled as a cheap-floor wet gate (roster 49->50, gates 10->11, cheap membership 4->5). One recorded freeze re-anchor to the gate-landing base (0ec3c10), admitting lean/overflow.dag which merged inside the wall-less interim (#7550); documented in legacy_manifest_freeze_sha_note. Live-cover witness dedupes its diff observation onto the gate module. Law note and preflight bullet updated to state both directions per-PR. RED proven by execution: a committed unrostered dag/extdeps probe file turns extdeps_scope_placement_gate_passes red; removing it greens. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…6281) Diff-grain sibling of tools.publication_placement_gate: refuses any freeze..HEAD-added dag/extdeps .dag file outside carriers-union- machinery (scope_placement_refused_paths, pure kernel on gunbc.extdeps_scope_frontier with hermetic RED/GREEN controls) and any frozen-manifest row naming a post-freeze-added file; diff failure and parse truncation refuse, never skip. Enrolled as a cheap-floor wet gate (roster 49->50, gates 10->11, cheap membership 4->5). One recorded freeze re-anchor to the gate-landing base (0ec3c10), admitting lean/overflow.dag which merged inside the wall-less interim (#7550); documented in legacy_manifest_freeze_sha_note. Live-cover witness dedupes its diff observation onto the gate module. Law note and preflight bullet updated to state both directions per-PR. RED proven by execution: a committed unrostered dag/extdeps probe file turns extdeps_scope_placement_gate_passes red; removing it greens. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
6 tasks done
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
added a commit
that referenced
this pull request
Aug 1, 2026
…ng preflight + ExternalModelScope carrier (operator verdict on #7556) (#7571) * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * chore: regenerate drifted generated artifacts (ci auto-heal) * DESIGN §3 external-upstream-decomposition + extdeps modeling preflight + ExternalModelScope carrier/gate (operator verdict on #7556) - design_document.dag §3: verbatim 'External upstream decomposition' subsection; DESIGN.md regenerated - gunbc.plans.extdeps_modeling_preflight: 8 typed preflight rows (single authority), registered Plan renders the table from them - extdeps.external_authority: ExternalSubjectRef/ExternalRevision/ExternalModelScope (citations nonempty by construction), FactAuthorityOverride.fact -> DeclarationRef; admit_external_model_scope gate with ForeignSubjectRow/ConsumerCoverageInUpstream refusals - gunbc.extdeps_scope_frontier: staged fail-closed enrollment — 2 carriers + 17 machinery-exempt + 397 counted frontier rows over all 416 dag/extdeps files; live-tree cover witness refuses unrostered or stale rows - extdeps.vendor.{microsoft,atlassian} adopt extdeps_model_scope (admitted by execution) - extdeps.browser: loud non-precedent disposition note naming the eventual split - dag/test/claim/external_model_scope_witness_test.dag: 12 claims incl. operator RED (generic browser + Chromium scope + Chrome|Firefox|Safari rows -> refused) and GREEN (shared shape + separate modules + downstream roster -> admitted); stage0 seed + ci.yml + plan doc regenerated Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Consume the module's own anchor in extdeps_model_scope (review 46077), qualified against silent same-name capture cursor review 46077: first_citation re-minted the anchor URI — parallel representation. Fixing it by BARE sibling reference was proven WRONG by execution: atlassian's bare extdeps_external_authority_anchor reference silently captured microsoft's same-named decl (first-occurrence-wins pooling; the duplicate-toplevel-decl fail-open, now witnessed on data decls). The landed spelling is the module-QUALIFIED reference (extdeps.vendor.<m>.extdeps_external_authority_anchor), single authority with no capture; the adopter witness now discriminates per-module citation locators so a future capture regression reds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Regenerate ci.yml on merged tree (extdeps-modeling-preflight rows on top of main) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Roster the two extdeps modules main added mid-flight (review 46111): git/inspect + github/workflows, frontier count 397 -> 399 The live cover witness red exactly as designed on the merged tree; frontier claims re-run green (418 files = 2 carriers + 17 machinery-exempt + 399 frontier). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Rework carrier/enforcement per operator handback on #7571 (also codex review 46118) (1) ExternalSubjectRef carries a DeclarationRef (symbolic subject identity; vendor scopes point at their existing microsoft/atlassian declarations, no restated legal names). (2) module-grain revision removed — revisions belong on build/release/fact rows. (3) the synthetic function is no longer presented as an admission gate: renamed to the external_model_scope_decision KERNEL over DeclaredScopeFacts with a loud honesty boundary; the mechanical wall today is scope PRESENCE; subject-content-derived enforcement is the named frontier feature:extdeps-subject-content-derived (dissolves when a Node-tree projection derives DeclaredScopeFacts from the real module and feeds the same kernel). (4) the 399-row legacy population moved out of the semantic module into the frozen manifest dag/gunbc/legacy_extdeps_scope_frontier.tsv (one path per line, remove-only, count DERIVED by parse_frontier_manifest, exact bidirectional live diff enforced by the cover witness). (5) consumer coverage identity is DeclarationRef, not free text. 12/12 witness claims green by execution incl. the live 418-file cover against the manifest; stage0 seed regenerated; drift gates PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * Consume std.roster_frontier's declaration_ref_eq instead of re-minting it (review 46136); register std_roster_frontier.rs in the seed roster Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * Merge main; enroll publication grants for this PR's 6 added paths + 11 ungranted main-side additions (publication_placement_gate green) The new Stage-0 publication wall (P-B) requires a PublicFilePublishGrant row for every path added after the cutover commit. This PR's six additions are enrolled, plus the eleven paths merged to main since cutover without rows (heal_revalidation, source_integration_proof_kernel, workflow-dispatch, github/workflows lanes) — main's own floor is red on the gate without them, and the roster is one shared carrier. publication_placement_gate_passes PASS locally by wet execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Make the presence wall mechanical (codex review 46215): carrier rows content-verified, manifest frozen against a git anchor Half 1: scope_carrier_paths membership was path-asserted; the cover witness now filesystem_reads every carrier file and refuses one whose bytes lack the extdeps_model_scope declaration (declared text-scan scaffold, corpus_scan precedent, dissolves with the storage-grain frontier). Half 2: the manifest's remove-only lifecycle was review discipline; every manifest row must now name a file that existed at the pinned legacy_manifest_freeze_sha — the witness diffs freeze..HEAD via git.Core.DiffNameStatus (the publication-gate pattern) and refuses any manifest row in the added/copied/renamed set, with diff failure and parse truncation typed as refusals (PostFreezeObservation coproduct), never skips. 17/17 claims green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * Split the wet live observations out of hermetic discovery (d4bef96 floor red) Hermetic discovery executed the three wet-only fns (Filesystem.List walk, git.Core.DiffNameStatus freeze diff) against the mock corpus, where those operations are unpublished — ReadsLiveTree does not exclude fns from discovery. Structural fix, not a widened mock: - pure decision fns (scope_cover_holds, carrier_content_declares_scope, PostFreezeObservation, manifest_freeze_holds) move to their single authority gunbc.extdeps_scope_frontier; the hermetic witness imports them (also discharges cursor review 46245 both findings) - new dag/test/claim/external_model_scope_live_cover_witness_test.dag (ReadsLiveTree) holds the live walk + freeze diff; discovery-excluded via witness_exclusion_frontier (OfflineLocalRecipe, substantiated reason + dissolve-on + local recipe, artifact_store precedent) and granted in publication_grant - hermetic file keeps all RED controls, kernel controls, manifest accounting, and the filesystem_read carrier-content check per-PR Verified by execution: 14/14 hermetic PASS, 3/3 wet PASS, publication_placement_gate_passes PASS, generated-artifact gate PASS, fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Fix the mainline scm_compatibility homonym capture blocking CI (5 floor reds on origin/main d552ff4) Top-level fn names are not module-scoped in the assembled closure, so native_scm_interaction_scenario_fixture's parametered fixture_projection collided with the zero-arg fixture_projection homonyms in pijul/mercurial_upstream_model_witness_test once #7563 linked their closures — native_scm_receipt_for's internal call then dispatched to a zero-arg winner: 'call contract mismatch: no parameter named scenario'. Fix: rename the parametered helper to the unique prefixed native_scm_scenario_fixture_projection (both references are file-internal; no external caller exists, verified by corpus grep). Verified by execution: all 5 previously failing witnesses PASS, plus 63 witnesses across every other importer of the fixture module (native_scm_interaction_contract 14/14, mercurial compat 6/6, git compat 7/7, roadmap_validation_oracle 36/36). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * State the enforcement grain honestly and gate the roster-to-disk direction per-PR (codex review 46258) Finding 1: the preflight doc and frontier law claimed the population cover as 'the mechanical wall today' while the cover runs only on the discovery-excluded wet lane — grain inflation. Fixed both ways: - new per-PR hermetic test roster_paths_resolve_on_disk: every rostered path across all three rosters (2 carriers + 17 machinery + 399 manifest rows) must resolve in the checkout via the filesystem_read carve-out (22ms for 418 reads); a stale or fabricated roster row reds per-PR via the interpreter's typed hermetic Read refusal (verified by execution on a nonexistent probe path) - law note + preflight bullets now state the grain explicitly: per-PR merge-gated = roster-to-disk resolution, roster disjointness, carrier byte-content, RED controls; wet-lane = live enumeration (disk-to- roster new-file detection) and the freeze diff, with per-PR gating of that direction arriving at the mandatory_tag region promotion the frontier dissolves into 15/15 hermetic witnesses PASS; plan doc regenerated same commit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the publication roster after merging main (gate-red duplication on main itself) origin/main 06d7aea lists the eleven pre-wall repair paths TWICE: once from #7565's branch-side enrollment block and once from #7580's repair block — the same enrollment race #7580's own note describes, re-entered by the next concurrent pair. The placement gate refuses repeated grants, so main is currently gate-red and every PR merge ref inherits it. This branch resolves the merge by keeping #7580's repair block (with its note) as the single occurrence and re-adding only this PR's own seven paths; publication_placement_gate_passes PASS by execution on the merged tree (42 unique rows, zero duplicates). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Land the per-PR merge-gated ExtdepsScopePlacementGate (codex review 46281) Diff-grain sibling of tools.publication_placement_gate: refuses any freeze..HEAD-added dag/extdeps .dag file outside carriers-union- machinery (scope_placement_refused_paths, pure kernel on gunbc.extdeps_scope_frontier with hermetic RED/GREEN controls) and any frozen-manifest row naming a post-freeze-added file; diff failure and parse truncation refuse, never skip. Enrolled as a cheap-floor wet gate (roster 49->50, gates 10->11, cheap membership 4->5). One recorded freeze re-anchor to the gate-landing base (0ec3c10), admitting lean/overflow.dag which merged inside the wall-less interim (#7550); documented in legacy_manifest_freeze_sha_note. Live-cover witness dedupes its diff observation onto the gate module. Law note and preflight bullet updated to state both directions per-PR. RED proven by execution: a committed unrostered dag/extdeps probe file turns extdeps_scope_placement_gate_passes red; removing it greens. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Expose std_roster_frontier in the derived stage0 crate partition (codex review 46329) extdeps_external_authority.rs imports crate::std_roster_frontier, but the partition source authority (v2.workflow.rust_crate_partition) never rostered the new module, so the partitioned crates could not resolve it. Fix at the authority: std_roster_frontier joins the std-core primitive roster with its module-dag edges (extdeps_external_authority -> std_roster_frontier -> std_decl_ref); partition artifacts and the stage0 seed regenerated to fixed point (two regen generations — the renderer bakes the partition rows at its own build time), and stage0_core/src/lib.rs (tracked but outside every regen path — the lifecycle scaffold's open partition contradiction) gains the matching declaration directly. Disclosed, not fixed here: v1-stage0-std-core has four OTHER unresolved modules (std_occurrence_identity, extdeps_units_{dimensionless, iec_80000_13,iso8601}) byte-identical on origin/main — pre-existing partition rot from other lanes (the #7109 class; no CI job compiles these crates). Rostering them correctly requires re-cutting the std/extdeps crate boundary (extdeps_uri + extdeps_external_authority would move below std_measure, emptying v1-stage0-extdeps-base) — the deferred emitted-crate-partition lane's re-cut, not a one-line roster fix; attempted and reverted here after it surfaced that knot. Verified: cargo check -p v1-stage0-std-core no longer reports std_roster_frontier (remaining errors = the four pre-existing, same as main); generated-artifact gate PASS; fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Reconcile freeze anchor with merged main 5669d42 (cpm_pert joined the interim manifest) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Make the manifest's remove-only lifecycle mechanical at line grain (codex review 46378) manifest_freeze_holds judges file CREATION dates, so a pre-freeze file migrated out of the manifest could later be re-added (scope decl deleted, carrier row dropped, manifest row restored) and the freeze check would pass — the escape hatch re-opened after migration. Closed: tools.extdeps_scope_placement_gate now also observes git.Core.DiffUnified0(origin/main...HEAD) and refuses any line the change itself ADDS to the manifest (manifest_line_observation / manifest_remove_only_holds on gunbc.extdeps_scope_frontier). The one admitted arm is ManifestIntroduced — the file absent at the merge base (the unified diff's /dev/null old side), exactly the PR that first lands the manifest, unforgeable once it exists on main (a delete-and- rewrite inside a branch still diffs as modification). Unreadable diff text and failed diffs refuse, never skip; removals stay free, so the manifest is monotonically shrinking by construction at the merge gate. Hermetic controls: red_manifest_remove_only_refuses_added_row, green_manifest_remove_only_admits_removal_and_unrelated_edits, green_manifest_introduction_admitted_once, red_manifest_unreadable_refuses. Verified by execution: 21/21 hermetic witnesses PASS, both placement gates PASS wet on this tree (the introduction arm exercising the live path), fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Reach the unreadable arm from the parser and collapse the verdict to one surface (codex review 46387) Finding 1: manifest_line_observation never constructed ManifestDiffUnreadable — malformed or truncated diff text fell through to ManifestUntouched, which the gate accepts (fail-open), and the RED control bypassed the parser by constructing the variant directly. Closed: the fold tracks whether any line MENTIONS the manifest path and whether its recognized new-side header was ever ENTERED; mention without entry yields ManifestDiffUnreadable — covering truncation mid- header AND making a manifest deletion refuse conservatively (old-side header mentions the path, no new-side header follows; the promotion PR that legitimately deletes the manifest deletes this gate in the same change). New REDs go THROUGH the parser: a truncated header diff and a whole-file deletion diff both yield ManifestDiffUnreadable. Finding 2: manifest_remove_only_holds hand-matched the same coproduct the gate matched into ProcessExit — two verdict authorities. The Bool predicate is deleted; the ONE surface is the pure manifest_remove_only_exit(observation) -> ProcessExit on the gate module, consumed by both the wet gate wrapper and every hermetic control (which assert on its ExitSuccess/failure arms). Verified by execution: 22/22 hermetic witnesses PASS (incl. the two new parser-reaching REDs), extdeps_scope_placement_gate_passes PASS wet, fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Disambiguate decl_ref in the #7549 witness (floor red on 2a04481: ambiguous across std.primitive_identity and std.roster_frontier) Both modules declare an identical top-level decl_ref helper on main; the ambiguity is latent there and fired in this PR's closure, which is the first to link them (extdeps.external_authority imports std.roster_frontier). Minimal fix at the red site only: the six call sites in dag/test/claim/primitive_identity_join_witness_test.dag are module-qualified to std.primitive_identity.decl_ref and the named import row is dropped. 15/15 witnesses in the file PASS by execution. The root defect is a DESIGN section-3 fork: std.primitive_identity re-mints the decl_ref constructor std.roster_frontier already owns (the same re-mint cursor review 46136 removed from this PR's own carrier). Deduplicating it belongs to the primitive-identity lane on main; this commit only unblocks the floor at the site that reds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Post-merge reconcile: fix stale sibling citations after #7591 deleted the publication gate Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
PR 2 of 2 (width/signedness was #7511).
std.integer.IntegerOverflowSemantics<E>with three distinct arms:OverflowReturns(wrapping/saturating by value rule),OverflowRaises(parameterized effectE— panic and trap stay separate inhabitants), andOverflowUndefined(not folded into either).lean_admit_fixed_width_overflow_semanticsadmission boundary;LeanOverflowPanicsandLeanOverflowTrapsmodel distinct raise effects.OverflowDisposition/OverflowActiondefork; Nat authority.Test plan
lean_overflow_semantics_witness_test.dag— arm discrimination (returns vs raises vs undefined), panic≠trap, admission accepts wrapping / RED refuses undefined and raisesregen_stage0green locally afterdag/std/integer.dagchangelean_catalog_fixed_width_overflowdata decl)