diff --git a/.gitattributes b/.gitattributes index e46959ff478..b2d96f0bacb 100644 --- a/.gitattributes +++ b/.gitattributes @@ -51,6 +51,7 @@ docs/plans/fold-ergonomics.md merge=generated-artifact docs/plans/format-model-reconciliation.md merge=generated-artifact docs/plans/host-effect-orchestration.md merge=generated-artifact docs/plans/idea-machine.md merge=generated-artifact +docs/plans/import-namespace-program.md merge=generated-artifact docs/plans/inert-layer-lens.md merge=generated-artifact docs/plans/input-envelope-roadmap.md merge=generated-artifact docs/plans/intent-linearity-design-draft.md merge=generated-artifact @@ -75,6 +76,7 @@ docs/plans/structural-quadratic-wall-coverage-audit.md merge=generated-artifact docs/plans/testgen-oracle.md merge=generated-artifact docs/plans/typescript-gap-census.md merge=generated-artifact docs/plans/v2-complexity-capability-parity.md merge=generated-artifact +docs/plans/v2-corpus-self-host.md merge=generated-artifact docs/plans/v2-self-hosting.md merge=generated-artifact docs/plans/value-null-split.md merge=generated-artifact docs/plans/wiring-liveness-preflight.md merge=generated-artifact @@ -101,6 +103,7 @@ src/v1/stage0/src/required_regen_host.rs !merge src/v1/stage0/src/resolved_graph_cache.rs !merge src/v1/stage0/src/shared_typecheck_store.rs !merge src/v1/stage0/src/std_lens_verdict.rs !merge +src/v1/stage0/src/target_invocation_host.rs !merge src/v1/stage0/src/usv_pilot_v2_std_algebra.rs !merge src/v1/stage0/src/usv_pilot_v2_std_collection.rs !merge src/v1/stage0/src/usv_pilot_v2_std_node.rs !merge diff --git a/dag/gunbc/design_document.dag b/dag/gunbc/design_document.dag index 47a4f851c29..babbd5a4e3c 100644 --- a/dag/gunbc/design_document.dag +++ b/dag/gunbc/design_document.dag @@ -117,7 +117,7 @@ fn section_4b_blocks() -> List { [ h2(text: "4b. Safety: the guarantee ladder (every error class climbs from runtime harm toward unwritability)"), p(text: "**Placed here because it is what §4's decidability buys, before §5 legislates the floor (operator directive 2026-07-31; worked examples and the rung census live in the recovery analysis linked below).** Safety is not the presence of diagnostics or the absence of crashes — it is the reduction of the state space in which a program can silently do the wrong thing. Every discovered error class sits on one ordered ladder and is obligated to climb it: **mitigatable** (the failure occurs; harm is contained by total operations, typed outcomes, bounds, rollback, isolation) → **mechanically preventable** (a generated test, lens, or gate reliably exposes and blocks it — but the invalid state remains writable, and safety depends on that mechanism executing and staying enrolled) → **structurally guaranteed** (the source can still describe the invalid state, but no `Accepted` program contains it: the compiler derives a proof or refusal from modeled structure) → **structurally impossible** (the invalid state has no constructor or representation in the canonical model — validation is unnecessary because the bad state cannot be written, and a refusal at the source boundary is then a symptom of the carrier's shape, not a separate check). **At this rung, ask whether the check's RED is authorable before writing the check** (2026-08-22): if the forbidden state cannot be expressed *anywhere the check could run*, the check is not a weak wall but a decoration — permanently green *by construction*, carrying no information, and worse than absent because it will be cited as coverage. **That question has two boundaries and only the second decides it**, a distinction an earlier revision of this clause collapsed: a state unrepresentable in the ACCEPTED corpus may still be perfectly representable as SOURCE HANDED TO THE COMPILER BY A FIXTURE, and a compiler is precisely a thing whose regression probes are invalid programs. So the rule fires only after checking the fixture boundary: if the refusal is still authorable there, the evidence is enrollable there and declining it is the specification-without-execution failure, not a saving. Where no fixture harness can express the subject, that missing harness is the class's next-rung trigger (§4b(2)) rather than a permanent ceiling. That is a sharper objection than redundancy: a redundant check can still fail, this one cannot. It does **not** contradict meta-obligation (4) below — that clause keeps evidence whose RED stays authorable at the source boundary (the compiler still admits the text and refuses it), which is exactly the case where the probe can flip; the rule here bites only where no source text expresses the violation, so nothing can flip it. Receipt, carried through BOTH boundaries because the first alone would have been the collapse this clause warns about: the reach roster's placement is enforced by §3's acyclicity law — measured on a two-module discriminating pair, the acyclic direction compiling with 0 diagnostics and one back-edge refusing with `circular dependency detected` naming both modules — so the annotation was corrected to say *enforced*. No witness was authored, and the reason is the FIXTURE boundary rather than the corpus one: `gunbc.compile_diagnostic_census` takes a single source string, and measured by execution a two-module string returns `BLOCKING: ParseError` — for the ACYCLIC control as well as the cyclic one, so the harness refuses the shape and could never reach the cycle wall. The missing multi-module compile fixture is therefore this class's next-rung trigger, not a ceiling. The higher rung subsumes the lower — construction over proof, proof over validation, validation over mitigation; §5's construction-before-validation preference is this ladder's top two rungs, and its fail-closed doctrine is the law of the floor. Below the floor sits **silent wrongness, which is not a rung: it is outside the ladder and forbidden outright** (§5). Adjacent — and deliberately **not a fifth rung** — is **outside the modeled guarantee**: external reality, undecidable properties, undeclared intent. That column is observed, refused, or mitigated at a declared boundary, never fabricated (§5), and keeping it off the ladder prevents \"we do not model this\" from masquerading as a weak implementation that should climb."), - p(text: "Every class carries an **attainable ceiling — derived, not aspirational**: a decidable, fully modeled class may reach structural impossibility; a decidable class missing its authority is §5's *wall after grounding*; a class blocked on a missing-or-unverified language capability names the capability as its trigger (the live one: **unforgeable construction** for carrier-borne invariants — `sole_constructor` is a real, executing wall for a census-unique plain-record type — on the source→`.dag`-acceptance path specifically, confirmed by execution to refuse a cross-module record literal at four positions (fn body, module-scope `data` initializer, list-element, map-value) and at `ExprCast` (including generic instantiation) — and confirmed by execution to leave three further gaps open on that same path (named below: one name-resolution gap, one unwired construction form, and one unrefused construction position), so the mapped boundary is a mix, not a clean coverage claim even before crossing to another realization target. A second, distinct per-function `admit_callers` admission wall confirmed alongside it (`sole_constructor` gates WHO MAY CONSTRUCT; `admit_callers` gates WHO MAY CALL the mint; a caller-supplied validator decides WHAT IS PROVEN and is separately defeasible, below). The compiler-module check exemption `module_skips_direct_call_arg_check` was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere. On the source→`.dag`-acceptance path the audit closed with three confirmed structural holes, not a clean ceiling: a census-AMBIGUOUS type name resolves by silent last-import-wins instead of refusing; coproduct/variant construction of a `sole_constructor` type is entirely unwired; and a record literal in a parameter's declared default-value expression gets no diagnostic at all (all three 0 live exposure today by targeted grep, all three decidable fixes once scoped, not ratchets). Separately, and more severely, on the source→Rust-emission path: a production `sole_constructor` type's own emitted mirror is confirmed by execution to be silently forgeable — `extdeps.uri` `UriValidatedScalar` (fixed-law mint `uri_validated_scalar_construction`, no caller-supplied validator) emits as a `pub` struct with a `pub` field deriving `serde::Deserialize`, and both `serde_json::from_value` and a direct struct literal admit one representative from each of the mint's three refusal partitions — negative, surrogate, and above the Unicode maximum (the mint refuses whole ranges; the receipt executes a representative per branch, not every refused value), confirmed against a shape-control discriminator so the admits are load-bearing, not a harness artifact (no production caller established to have exercised this — mechanism confirmed, no confirmed victim). Executed downstream, the forgery is not inert: passed to the carrier's percent-encoding consumer `uri_percent_encode_admitted_scalar_wire` (not its only declared consumer — `uri_validated_scalar_code_point` also takes the type, as an accessor returning the raw code point; \"sole\" was an unverified quantifier in an earlier revision of this clause), the surrogate and above-maximum representatives reach output as invalid UTF-8 percent-encoding (`%ED%A0%80`, `%F4%90%80%80`), while the negative representative is refused there by `uri_utf8_octet_construction` — so the consumer independently catches one of the three partitions, and for the other two the wall's absence is a PRODUCED-OUTPUT defect rather than merely a constructible-value one. This is below floor (§5), not a rung on the ladder, and it is categorically worse than the three `.dag`-path holes above, which are decidable zero-exposure gaps in an otherwise-real wall. And one confirmed scope boundary, more consequential than any single hole above: even where the wall fires with full coverage it confines only WHO/WHERE constructs the carrier, establishing nothing about WHAT invariant a sanctioned caller's own predicate enforces, so a mint lacking a fixed, module-owned validator gives no guarantee beyond confinement — `std.interval` `closed_interval` takes a caller-supplied `le` and accepts reversed bounds under a lying predicate (the failing case); `std.interval` `degenerate_interval` is total and needs no predicate at all (the working case). These two findings are complementary, not duplicative, on one claim from opposite directions: one shows a caller-supplied validator can lie; the other shows a FIXED validator with zero caller freedom can still be defeated once the carrier crosses into a realization where confinement itself doesn't survive — neither is a defect in `sole_constructor` as specified. A reconstruction path that bypasses source construction also exists in the interpreter; that audit is IN FLIGHT as PR #8658 (not yet merged), so its row is not yet in the linked document — named here so the claim is verifiable and the gap is expected, not a broken pointer. **THE PROBES BEHIND THIS AUDIT DO NOT CURRENTLY EXECUTE** — its 26 witness identities sit in the required floor's `DeclinedLiveTree` arm, discovered every run and folded never, so what is written above was measured once and is re-measured by nothing; the population, the specimen and the single deletion that ends it are gap-analysis §11 item 28. Full audit: `docs/plans/compiler-guarantee-recovery-gap-analysis.md`; an earlier revision of this paragraph claimed no such capability exists, refuted by review 2026-07-31, a later revision called its completeness unverified, and this 2026-08-20 revision folds in a second, independently-ruled realization path (ARM 3, PR #8661, also not yet merged) that changes rather than extends that result: a mapped boundary per path, not one closed ceiling); an undecidable property honestly remains a ratchet or validator; an external fact remains a boundary obligation. **Below ceiling is a correctness gap, never optional elegance** — this clause is what keeps §6's purity trap from pricing out mandatory walls, the exact failure mode by which the recovered guarantee decayed unnoticed. Four meta-obligations make the ladder operational: (1) **rung honesty, at a declared subject grain** — the reported rung must equal the rung established by executed evidence, a discriminating RED refused on the real acceptance path plus an accepted positive control, **measured against a declared boundary** (source→interpretation, source→each emission target, phase-carrier→phase-carrier are different paths with independently different rungs: the interpreter refuses a mislabeled call that the emitter reorders into positional leftovers); a class's current rung is the **minimum across its in-scope paths**, or one row per structurally distinct path — citing the strongest path while another stays silent is inflation, and a type name, diagnostic variant, inert lens, or plan establishes nothing. **Rung inflation** (a carrier named for the top rung while occupying the bottom; a status ledger's \"DONE\") is the fabricated-plausible-output failure applied to the compiler's self-description — worse than sitting low, because an inflated class never ranks for climbing. (2) **no untracked stall** — a class below its ceiling must name its next-rung trigger, separating *cannot climb further* from *can climb after one grounding* from *can climb now but unbuilt*; only the first is permanent. (3) **no silent regression** — a change may lower a rung only by declaring previous rung, temporary rung, reason, bounded population, and restoration trigger; a compatibility exemption is not bootstrap glue, it is a visible safety regression with a finite runway. (4) **dissolution on climb — production handling only, never the evidence** — a climb deletes the redundant lower-rung *production* machinery it obsoletes (§2/§3: the proof that makes a state unwritable replaces the validator of the writable form, never accumulates beside it, unless that machinery independently guards an external boundary), but the class's discriminating RED and positive control **remain enrolled as the executing evidence that the higher rung stays real** — deleting them would recreate specification-without-execution one rung up; an expecting-red probe that greens when its wall lands flips to a permanent regression control, it does not retire (correction per review 2026-07-31: an earlier revision would have deleted the evidence with the machinery). Every newly discovered error class — incident, review finding, runtime exception, falsifier divergence — files or updates one row: invalid state, harm, distinguishing facts, rung found at, ceiling with reason, next trigger. That is how \"any class we find climbs\" is a repository rule rather than a cultural preference."), + p(text: "Every class carries an **attainable ceiling — derived, not aspirational**: a decidable, fully modeled class may reach structural impossibility; a decidable class missing its authority is §5's *wall after grounding*; a class blocked on a missing-or-unverified language capability names the capability as its trigger (the live one: **unforgeable construction** for carrier-borne invariants — `sole_constructor` is a real, executing wall for a census-unique plain-record type — on the source→`.dag`-acceptance path specifically, confirmed by execution to refuse a cross-module record literal at four positions (fn body, module-scope `data` initializer, list-element, map-value) and at `ExprCast` (including generic instantiation) — and confirmed by execution to leave three further gaps open on that same path (named below: one name-resolution gap, one unwired construction form, and one unrefused construction position), so the mapped boundary is a mix, not a clean coverage claim even before crossing to another realization target. A second, distinct per-function `admit_callers` admission wall confirmed alongside it (`sole_constructor` gates WHO MAY CONSTRUCT; `admit_callers` gates WHO MAY CALL the mint; a caller-supplied validator decides WHAT IS PROVEN and is separately defeasible, below). The compiler-module check exemption `module_skips_direct_call_arg_check` was found (code read, not execution) to be scoped entirely to the direct-call argument-type judgment and does not reach `sole_constructor`'s construction check at either call site — a positive finding that retires this axis, not an absence of any exemption anywhere. On the source→`.dag`-acceptance path the audit closed with three confirmed structural holes, not a clean ceiling: a census-AMBIGUOUS type name resolves by silent last-import-wins instead of refusing; coproduct/variant construction of a `sole_constructor` type is entirely unwired; and a record literal in a parameter's declared default-value expression gets no diagnostic at all (all three 0 live exposure today by targeted grep, all three decidable fixes once scoped, not ratchets). Separately, and more severely, on the source→Rust-emission path: a production `sole_constructor` type's own emitted mirror is confirmed by execution to be silently forgeable — `extdeps.uri` `UriValidatedScalar` (fixed-law mint `uri_validated_scalar_construction`, no caller-supplied validator) emits as a `pub` struct with a `pub` field deriving `serde::Deserialize`, and both `serde_json::from_value` and a direct struct literal admit one representative from each of the mint's three refusal partitions — negative, surrogate, and above the Unicode maximum (the mint refuses whole ranges; the receipt executes a representative per branch, not every refused value), confirmed against a shape-control discriminator so the admits are load-bearing, not a harness artifact (no production caller established to have exercised this — mechanism confirmed, no confirmed victim). Executed downstream, the forgery is not inert: passed to the carrier's percent-encoding consumer `uri_percent_encode_admitted_scalar_wire` (not its only declared consumer — `uri_validated_scalar_code_point` also takes the type, as an accessor returning the raw code point; \"sole\" was an unverified quantifier in an earlier revision of this clause), the surrogate and above-maximum representatives reach output as invalid UTF-8 percent-encoding (`%ED%A0%80`, `%F4%90%80%80`), while the negative representative is refused there by `uri_utf8_octet_construction` — so the consumer independently catches one of the three partitions, and for the other two the wall's absence is a PRODUCED-OUTPUT defect rather than merely a constructible-value one. This is below floor (§5), not a rung on the ladder, and it is categorically worse than the three `.dag`-path holes above, which are decidable zero-exposure gaps in an otherwise-real wall. And one confirmed scope boundary, more consequential than any single hole above: even where the wall fires with full coverage it confines only WHO/WHERE constructs the carrier, establishing nothing about WHAT invariant a sanctioned caller's own predicate enforces, so a mint lacking a fixed, module-owned validator gives no guarantee beyond confinement — `std.interval` `closed_interval` takes a caller-supplied `le` and accepts reversed bounds under a lying predicate (the failing case); `std.interval` `degenerate_interval` is total and needs no predicate at all (the working case). These two findings are complementary, not duplicative, on one claim from opposite directions: one shows a caller-supplied validator can lie; the other shows a FIXED validator with zero caller freedom can still be defeated once the carrier crosses into a realization where confinement itself doesn't survive — neither is a defect in `sole_constructor` as specified. A reconstruction path that bypasses source construction also exists in the interpreter; that audit is IN FLIGHT as PR #8658 (not yet merged), so its row is not yet in the linked document — named here so the claim is verifiable and the gap is expected, not a broken pointer. **THE PROBES BEHIND THIS AUDIT DO NOT CURRENTLY EXECUTE** — its 26 witness identities sit in the required floor's `DeclinedLiveTree` arm, discovered every run and folded never, so what is written above was measured once and is re-measured by nothing; the population, the specimen and the single deletion that ends it are gap-analysis §11 item 28. Full audit: `docs/plans/compiler-guarantee-recovery-gap-analysis.md`; an earlier revision of this paragraph claimed no such capability exists, refuted by review 2026-07-31, a later revision called its completeness unverified, and this 2026-08-20 revision folds in a second, independently-ruled realization path (ARM 3, PR #8661, also not yet merged) that changes rather than extends that result: a mapped boundary per path, not one closed ceiling); an undecidable property honestly remains a ratchet or validator; an external fact remains a boundary obligation. **Below ceiling is a correctness gap, never optional elegance** — this clause is what keeps §6's purity trap from pricing out mandatory walls, the exact failure mode by which the recovered guarantee decayed unnoticed. Four meta-obligations make the ladder operational: (1) **rung honesty, at a declared subject grain** — the reported rung must equal the rung established by executed evidence, a discriminating RED refused on the real acceptance path plus an accepted positive control, **measured against a declared boundary** (source→interpretation, source→each emission target, phase-carrier→phase-carrier are different paths with independently different rungs: the interpreter refuses a mislabeled call that the emitter reorders into positional leftovers); a class's current rung is the **minimum across its in-scope paths**, or one row per structurally distinct path — citing the strongest path while another stays silent is inflation, and a type name, diagnostic variant, inert lens, or plan establishes nothing. **Rung inflation** (a carrier named for the top rung while occupying the bottom; a status ledger's \"DONE\") is the fabricated-plausible-output failure applied to the compiler's self-description — worse than sitting low, because an inflated class never ranks for climbing. (2) **no untracked stall** — a class below its ceiling must name its next-rung trigger, separating *cannot climb further* from *can climb after one grounding* from *can climb now but unbuilt*; only the first is permanent. (3) **no silent regression** — a change may lower a rung only by declaring previous rung, temporary rung, reason, bounded population, and restoration trigger; a compatibility exemption is not bootstrap glue, it is a visible safety regression with a finite runway. **AND THE TRIGGER MUST NAME THE CAPABILITY, NOT AN ARTIFACT THAT WOULD CONTRIBUTE TO ONE (2026-08-26).** A declared drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, so the trigger *is* the whole check, and a trigger naming less than the capability it restores is the one direction this machinery structurally cannot see: **it will be satisfied while the capability stays dead.** What makes it invisible is that no step is wrong — the instrument author builds exactly what the trigger asked, the trigger fires honestly, the row retires correctly, and the thing the row existed to protect is still gone. Nobody has to be careless for this to happen, which is why it needs a rule rather than diligence. Receipt, and it is this document's own row: the measurement-bankruptcy entry above records losing *the only executable route to a self-host emission BOARD measurement* and then writes a trigger naming *a `.dag` entry point that emits, assembles and compiles ONE ENTRY* — a board is per-entry across MANY entries, so the two halves sit five lines apart in one row at different grains, and the row then declares the trigger fired. Measured by code read, the instrument that fired it takes a fresh temporary directory per invocation and path-depends on the whole stage0 crate, so every entry rebuilds the bootstrap compiler cold and the cost is entry-INDEPENDENT — one entry is the only thing it can do. **The rule:** a restoration trigger states the CAPABILITY, in the same words the drop used to describe the loss; where a trigger names an artifact instead, the row must state what that artifact must be SUFFICIENT FOR, and the artifact retires the row only when that sufficiency is shown. **The review tell is a grain mismatch between the loss sentence and the trigger sentence** — a plural loss with a singular trigger, a corpus loss with a per-module trigger, a route loss with a single-call trigger. Found by `loyal-lark-254` and verified against this document's text by `smart-ram-730`, and it is downstream of a refusal to report a number they could not stand behind: a pricing run that had returned any plausible figure would have closed the question and left the trigger defect standing. (4) **dissolution on climb — production handling only, never the evidence** — a climb deletes the redundant lower-rung *production* machinery it obsoletes (§2/§3: the proof that makes a state unwritable replaces the validator of the writable form, never accumulates beside it, unless that machinery independently guards an external boundary), but the class's discriminating RED and positive control **remain enrolled as the executing evidence that the higher rung stays real** — deleting them would recreate specification-without-execution one rung up; an expecting-red probe that greens when its wall lands flips to a permanent regression control, it does not retire (correction per review 2026-07-31: an earlier revision would have deleted the evidence with the machinery). Every newly discovered error class — incident, review finding, runtime exception, falsifier divergence — files or updates one row: invalid state, harm, distinguishing facts, rung found at, ceiling with reason, next trigger. That is how \"any class we find climbs\" is a repository rule rather than a cultural preference."), p(text: "**The floor first, the differentiator above it.** gunbc must first hold the ordinary compiler floor — names resolve, applications bind in exact bijection, values inhabit declared types, fields exist, closed variants eliminate exhaustively — and a failure there is a **below-baseline safety regression**, never compensated by higher-order capability. The differentiating claim begins above that floor: because the substrate carries causal, cardinality, algebraic, effect, ownership, cost, and realization facts structurally, the same ladder applies to classes ordinary compilers leave to tests, review, profiling, or production postmortems — a possibly-empty collection flowing into a nonempty consumer, recursion without a descent proof, a non-idempotent effect under automatic retry, a computation exceeding its declared complexity bound, operations whose declared algebra shows cancellation or duplication, a partially applied infrastructure change without convergence, a realization that does not preserve modeled behavior. The promise is **not** that every property becomes impossible; it is that every modeled class climbs to the highest honest rung its facts and decidability permit, with the ceiling and the residual risk explicit. Stated beside the ladder so a low ceiling is never mistaken for a gap: the compiler does not invent unstated intent (declared bound violated → refusal; declared algebra proves equivalence → derive; undeclared preference → never fabricated); does not prove unmodeled external reality (observe → typed evidence → admit or refuse → mitigate); does not lift arbitrary predicates to proof (the closed decidable cardinality fragment climbs where a general `fn(T) -> Bool` refinement cannot); and richer type names are not safety (a brand, wrapper, or `Validated` is cosmetic until construction and acceptance enforce the distinction). Runtime mechanisms — typed refusal, totality, rollback, budgets — remain real and necessary at honest boundaries; they must only never be mislabeled as construction. The rung census over the recovered claims, the worked floor/differentiating/boundary examples, and the climb plan: → [compiler-guarantee recovery gap analysis](docs/plans/compiler-guarantee-recovery-gap-analysis.md); its Stage 1 lands the executable claims carrier (per-path disposition **derived** from executed measurements — no stored rung field exists, so a transcribed rung is unrepresentable rather than lens-caught — with ceiling + typed reason, next trigger, consumer-in-`Accepted`; corrected per review 45367, which caught this clause reading as a stored per-class rung column; the dispositions include `FrontierAccepted`, the typed-located-counted diagnostic whose phase result is still `Accepted` — distinct from silent below-floor AND from a refusal, per the 2026-07-31 post-merge verdict, whose live specimens are the open candidates' `MethodExistenceUndecided` and `GroundingNotDerived`), grounding the enforcement-intent thread below rather than minting a second registry beside it."), ] } diff --git a/dag/gunbc/plans/cli_run_hollowing_plan.dag b/dag/gunbc/plans/cli_run_hollowing_plan.dag index a7e59e0c960..4cbe45ccbcd 100644 --- a/dag/gunbc/plans/cli_run_hollowing_plan.dag +++ b/dag/gunbc/plans/cli_run_hollowing_plan.dag @@ -14,8 +14,8 @@ fn cli_run_hollowing_plan_body() -> List { ThematicBreak, h2(text: "0. Scale receipt (live tree)"), ul(items: [ - li(text: "**Live whole file (measured by execution, 2026-07-23):** `wc -l src/v1/stage0/src/cli_run.rs` → **26,773 lines**; `rg -c '^\\s*(pub\\s+)?(async\\s+)?fn\\s+' src/v1/stage0/src/cli_run.rs` → **976 fns** (22 `test_*` inline modules; remainder production-scope). The §7 seed is **not** stable — it grew ~6× since the census snapshot."), - li(text: "**`seed-shrink-census.md` Chunk F (~4,165 LOC)** names the **dissolution sign-off unit** (CI orchestration → workflow `host_effect_apply`), not a live whole-file count. The other **~22.6k LOC** are the same file's interim seed body: classified by the **16 functional areas in §2** below, and tracked as managed seed growth in ROADMAP **§7 Seed interim** ([`ts-seed-interim`](../../ROADMAP.md) in `dag/gunbc/roadmap_authority.dag`) — host bridges, lens host feeds, floor/discovery machinery absorbed while v2 lanes land."), + li(text: "**THIS SECTION CARRIES NO NUMBERS, DELIBERATELY.** It previously transcribed a whole-file line and fn count measured 2026-07-23. Both had gone stale by roughly 83 percent before anyone noticed, because nothing re-derives a number copied into prose. DESIGN's standing rule (2026-08-24) is *name the instrument, never transcribe its output*, and a plan's own scale receipt is the worst place to break it: a reader sequencing work against it budgets against a file that no longer exists at that size. **The instrument:** `git show origin/main:src/v1/stage0/src/cli_run.rs | wc -l` for scale, and the same stream through `grep -cE '^[[:space:]]*(pub )?(async )?fn '` for the fn count. Read them from the tree at the moment you need them. The DIRECTION is the durable fact and it needs no magnitude: the file has GROWN at every measurement taken so far, because v1 lanes absorb host bridges and floor machinery faster than v2 lanes subsume them."), + li(text: "**Chunk F in `seed-shrink-census.md` names the dissolution SIGN-OFF UNIT** (CI orchestration to workflow `host_effect_apply`), which is a different subject from the whole file. That distinction is the load-bearing half and it survives; the LOC split that used to accompany it here is deleted for the reason above. The remainder is the file's interim seed body, classified by the functional areas in section 2 and tracked as managed seed growth in ROADMAP **section 7 Seed interim** ([`ts-seed-interim`](../../ROADMAP.md) in `dag/gunbc/roadmap_authority.dag`) -- host bridges, lens host feeds, floor and discovery machinery absorbed while v2 lanes land."), li(text: "**Sign-off order:** Chunk F runs **after** emitter chunks A–E and de-fork G per census §4 — orchestration dissolves once the compiler pipeline and host-effect spine can carry the floor without a hand-written driver."), ]), h2(text: "1. Area map (summary)"), @@ -42,7 +42,7 @@ fn cli_run_hollowing_plan_body() -> List { ]), row(cells: [ cell(text: "Corpus discovery & file walk"), - cell(text: "`gunbc.ci_spec` discovery_scan_dirs · `gunbc.ci_floor_plan`"), + cell(text: "`gunbc.ci_spec` discovery_scan_dirs (NOTE: `gunbc.ci_floor_plan` was DELETED by the 2026-08-15 floor cut; discovery now runs inside the required fold, so this row has no plan-node authority to subsume onto and needs re-derivation)"), cell(text: "emit-when"), cell(text: "CI native routing (#7069) + witness-realization"), ]), @@ -84,7 +84,7 @@ fn cli_run_hollowing_plan_body() -> List { ]), row(cells: [ cell(text: "Floor / witness execution"), - cell(text: "`claim_executor` · `src/v2/workflow/ci_floor_plan.dag` · [witness-realization-plan.md](witness-realization-plan.md)"), + cell(text: "`v2.workflow.required_floor` policy + `v1_compiler.cli_run` `run_required_floor` (NOTE: `src/v2/workflow/ci_floor_plan.dag` was DELETED by the 2026-08-15 floor cut and `claim_executor` is itself being deleted by the move-off-claim-executor lane, so BOTH former subsumption targets are gone) · [witness-realization-plan.md](witness-realization-plan.md)"), cell(text: "emit-when"), cell(text: "Workflow `host_effect_apply` replaces HAND driver"), ]), @@ -96,7 +96,7 @@ fn cli_run_hollowing_plan_body() -> List { ]), row(cells: [ cell(text: "Regen oracle & self-host scope"), - cell(text: "`regen_stage0` (the `v2.compiler.self_host.frontier` half of this scope is deleted with the roster)"), + cell(text: "`v2.workflow.required_regen` / `v1_compiler.required_regen_host` (NOTE: the `regen_stage0` binary this row named was DELETED at the root by the regen cut; the fixed point is now answered by `claim_executor --required-regen-fixed-point` and by nothing else, which is itself on the deletion path)"), cell(text: "delete-with-v1"), cell(text: "Wave 4 real-fixpoint cutover (`5-real-fixpoint`)"), ]), @@ -146,11 +146,11 @@ fn cli_run_hollowing_plan_body() -> List { h3(text: "2.9 Affected-set & diff provenance"), p(text: "**Today:** git-diff observation, import-closure shard compile, `ReadsLiveTree` inference bridge, declared-source-ref selection — decides what the floor runs on a PR. **Subsumes:** `gunbc.ci_spec` selection + `v2.lens.effect_reach`. **Disposition:** emit-when. **Trigger:** module-identity-storage-binding Phase 0 enrollment + provenance ingest (`affected_set_reading_from_git_diff_provenance`)."), h3(text: "2.10 Floor / witness execution"), - p(text: "**Today:** `run_discovery_corpus`, parallel witness scheduling, governor width — the CI floor runtime. **Subsumes:** `claim_executor` workflow + witness-realization plan. **Disposition:** emit-when. **Trigger:** `host_effect_apply` workflow realization replaces HAND loop ([host-effect-orchestration.md](host-effect-orchestration.md)). **In motion (2026-07-22+):** witness-realization scheduling + host-effect transport lanes (shell→intent Phase 2) and #7090 returning work on floor execution paths."), + p(text: "**Today:** `run_discovery_corpus`, parallel witness scheduling, governor width — the CI floor runtime. **Subsumes:** the required-floor fold (`v2.workflow.required_floor` policy, `v1_compiler.cli_run` `run_required_floor` host) + witness-realization plan. **Disposition:** emit-when. **STALE-TRIGGER CORRECTION (2026-08-27):** this row named `claim_executor` as the subsuming authority. That inverts the current direction -- `claim_executor` is the thing being DELETED, so it cannot be what this area dissolves onto. **Trigger:** `host_effect_apply` workflow realization replaces HAND loop ([host-effect-orchestration.md](host-effect-orchestration.md)). **In motion (2026-07-22+):** witness-realization scheduling + host-effect transport lanes (shell→intent Phase 2) and #7090 returning work on floor execution paths."), h3(text: "2.11 Compile-clean shard scope"), p(text: "**Today:** decides whole-tree vs import-closure compile for `dag_compile_clean_gate` on PR diffs. **Subsumes:** `tools.dag_compile_clean_scope` + compile gate in `v2.compiler.compile`. **Disposition:** partial — policy modeled, HAND still executes scope walk. **Trigger:** single `module_graph` closure authority end-to-end."), h3(text: "2.12 Regen oracle & self-host scope"), - p(text: "**Today:** `regen_input_sources`, regen skip on PR diffs, self-host staleness inputs. **Subsumes:** `regen_stage0` + frontier carrier. **Disposition:** delete-with-v1 — bulk GENERATED cutover, not piecemeal. **Trigger:** `5-real-fixpoint` gate ([v2-self-hosting.md](v2-self-hosting.md) Wave 4)."), + p(text: "**Today:** `regen_input_sources`, regen skip on PR diffs, self-host staleness inputs. **Subsumes:** `v2.workflow.required_regen` + frontier carrier (the `regen_stage0` binary this row named was DELETED at the root by the regen cut). **Disposition:** delete-with-v1 — bulk GENERATED cutover, not piecemeal. **Trigger:** `5-real-fixpoint` gate ([v2-self-hosting.md](v2-self-hosting.md) Wave 4)."), h3(text: "2.13 Host builtin bridge"), p(text: "**Today:** dispatches `filesystem_read`, fact builtins, measurement counters from `.dag` eval into Rust host physics. **Subsumes:** interpreter kernel D + witness realization. **Disposition:** seed-kernel-retained — irreducible host physics shrinks but does not hit zero. **Trigger:** per-builtin dissolution rows on frontier carrier."), h3(text: "2.14 Lens census / hygiene host feeds"), diff --git a/docs/plans/cli-run-hollowing-plan.md b/docs/plans/cli-run-hollowing-plan.md index d1fb955d385..941aebd6d79 100644 --- a/docs/plans/cli-run-hollowing-plan.md +++ b/docs/plans/cli-run-hollowing-plan.md @@ -8,8 +8,8 @@ ## 0. Scale receipt (live tree) -- **Live whole file (measured by execution, 2026-07-23):** `wc -l src/v1/stage0/src/cli_run.rs` → **26,773 lines**; `rg -c '^\s*(pub\s+)?(async\s+)?fn\s+' src/v1/stage0/src/cli_run.rs` → **976 fns** (22 `test_*` inline modules; remainder production-scope). The §7 seed is **not** stable — it grew ~6× since the census snapshot. -- **`seed-shrink-census.md` Chunk F (~4,165 LOC)** names the **dissolution sign-off unit** (CI orchestration → workflow `host_effect_apply`), not a live whole-file count. The other **~22.6k LOC** are the same file's interim seed body: classified by the **16 functional areas in §2** below, and tracked as managed seed growth in ROADMAP **§7 Seed interim** ([`ts-seed-interim`](../../ROADMAP.md) in `dag/gunbc/roadmap_authority.dag`) — host bridges, lens host feeds, floor/discovery machinery absorbed while v2 lanes land. +- **THIS SECTION CARRIES NO NUMBERS, DELIBERATELY.** It previously transcribed a whole-file line and fn count measured 2026-07-23. Both had gone stale by roughly 83 percent before anyone noticed, because nothing re-derives a number copied into prose. DESIGN's standing rule (2026-08-24) is *name the instrument, never transcribe its output*, and a plan's own scale receipt is the worst place to break it: a reader sequencing work against it budgets against a file that no longer exists at that size. **The instrument:** `git show origin/main:src/v1/stage0/src/cli_run.rs | wc -l` for scale, and the same stream through `grep -cE '^[[:space:]]*(pub )?(async )?fn '` for the fn count. Read them from the tree at the moment you need them. The DIRECTION is the durable fact and it needs no magnitude: the file has GROWN at every measurement taken so far, because v1 lanes absorb host bridges and floor machinery faster than v2 lanes subsume them. +- **Chunk F in `seed-shrink-census.md` names the dissolution SIGN-OFF UNIT** (CI orchestration to workflow `host_effect_apply`), which is a different subject from the whole file. That distinction is the load-bearing half and it survives; the LOC split that used to accompany it here is deleted for the reason above. The remainder is the file's interim seed body, classified by the functional areas in section 2 and tracked as managed seed growth in ROADMAP **section 7 Seed interim** ([`ts-seed-interim`](../../ROADMAP.md) in `dag/gunbc/roadmap_authority.dag`) -- host bridges, lens host feeds, floor and discovery machinery absorbed while v2 lanes land. - **Sign-off order:** Chunk F runs **after** emitter chunks A–E and de-fork G per census §4 — orchestration dissolves once the compiler pipeline and host-effect spine can carry the floor without a hand-written driver. ## 1. Area map (summary) @@ -18,16 +18,16 @@ | --- | --- | --- | --- | | Workspace & repo paths | `gunbc.cli_run_workspace_root_scaffold` · `gunbc.cli_run_repo_grant` · [effect-namespace-grants.md](effect-namespace-grants.md) | emit-when | Chunk F → GENERATED `host_effect_apply`; grant presets land | | CLI argv & bin dispatch | `gunbc` bins + `src/v2/workflow/*` orchestration rows | seed-kernel-retained | Wave 4 pinned bootstrap (~8–15k LOC) | -| Corpus discovery & file walk | `gunbc.ci_spec` discovery_scan_dirs · `gunbc.ci_floor_plan` | emit-when | CI native routing (#7069) + witness-realization | +| Corpus discovery & file walk | `gunbc.ci_spec` discovery_scan_dirs (NOTE: `gunbc.ci_floor_plan` was DELETED by the 2026-08-15 floor cut; discovery now runs inside the required fold, so this row has no plan-node authority to subsume onto and needs re-derivation) | emit-when | CI native routing (#7069) + witness-realization | | Resolve / typecheck entry orchestration | v2.compiler pipeline (GENERATED) · [cli-run-reconcile-defork.md](cli-run-reconcile-defork.md) | emit-when | Reconcile-defork Phase 1–3 + closure equivalence receipt | | Reconcile & env merge | `v2.compiler` reconcile stage (GENERATED) | already-subsumed | Orchestration wrapper deletes with Chunk F | | Typed module cache / memo | `std.materialize` / duplicate-work lattice ([duplicate-work-graph-lens-design.md](duplicate-work-graph-lens-design.md)) | emit-when | ComputationIdentity qualifier lands on materialize spine | | Import & module-graph host facts | `v2.lens.module_graph` · `import_resolution_facts` host seam | emit-when | Reconcile-defork Phase 1 repoint + namespace SymbolIndex | | Reference / cross-tree edges | `v2.std.cross_tree.resolution` · [namespace-resolution-design.md](namespace-resolution-design.md) | emit-when | Reference-deps B3 + import grammar deletion (B4) | | Affected-set & diff provenance | `gunbc.ci_spec` selection · `v2.lens.effect_reach` · [module-identity-storage-binding-design.md](module-identity-storage-binding-design.md) | emit-when | Declared `SourceRef` boundary + provenance ingest | -| Floor / witness execution | `claim_executor` · `src/v2/workflow/ci_floor_plan.dag` · [witness-realization-plan.md](witness-realization-plan.md) | emit-when | Workflow `host_effect_apply` replaces HAND driver | +| Floor / witness execution | `v2.workflow.required_floor` policy + `v1_compiler.cli_run` `run_required_floor` (NOTE: `src/v2/workflow/ci_floor_plan.dag` was DELETED by the 2026-08-15 floor cut and `claim_executor` is itself being deleted by the move-off-claim-executor lane, so BOTH former subsumption targets are gone) · [witness-realization-plan.md](witness-realization-plan.md) | emit-when | Workflow `host_effect_apply` replaces HAND driver | | Compile-clean shard scope | `tools.dag_compile_clean_scope` · `v2.compiler.compile` | partial | Import-closure authority unified on `module_graph` | -| Regen oracle & self-host scope | `regen_stage0` (the `v2.compiler.self_host.frontier` half of this scope is deleted with the roster) | delete-with-v1 | Wave 4 real-fixpoint cutover (`5-real-fixpoint`) | +| Regen oracle & self-host scope | `v2.workflow.required_regen` / `v1_compiler.required_regen_host` (NOTE: the `regen_stage0` binary this row named was DELETED at the root by the regen cut; the fixed point is now answered by `claim_executor --required-regen-fixed-point` and by nothing else, which is itself on the deletion path) | delete-with-v1 | Wave 4 real-fixpoint cutover (`5-real-fixpoint`) | | Host builtin bridge (interpreter seam) | `v1_interpreter` builtins · per-lens `*_live` projections | seed-kernel-retained | Node-tree readers dissolve seams (#5364 class); kernel keeps physics | | Lens census / hygiene host feeds | `v2.lens.*` tables · `non_fold_residue` · `fact_cardinality` | emit-when | Each lens lands node-tree reader or explicit host row retires | | Floor observability & width | `gunbc.floor_materialization` · `dag/std/realization_width.dag` · [realization-measurement-loop.md](realization-measurement-loop.md) | partial | Scheduler emits receipts; HAND timing deletes with floor native routing | @@ -73,7 +73,7 @@ ### 2.10 Floor / witness execution -**Today:** `run_discovery_corpus`, parallel witness scheduling, governor width — the CI floor runtime. **Subsumes:** `claim_executor` workflow + witness-realization plan. **Disposition:** emit-when. **Trigger:** `host_effect_apply` workflow realization replaces HAND loop ([host-effect-orchestration.md](host-effect-orchestration.md)). **In motion (2026-07-22+):** witness-realization scheduling + host-effect transport lanes (shell→intent Phase 2) and #7090 returning work on floor execution paths. +**Today:** `run_discovery_corpus`, parallel witness scheduling, governor width — the CI floor runtime. **Subsumes:** the required-floor fold (`v2.workflow.required_floor` policy, `v1_compiler.cli_run` `run_required_floor` host) + witness-realization plan. **Disposition:** emit-when. **STALE-TRIGGER CORRECTION (2026-08-27):** this row named `claim_executor` as the subsuming authority. That inverts the current direction -- `claim_executor` is the thing being DELETED, so it cannot be what this area dissolves onto. **Trigger:** `host_effect_apply` workflow realization replaces HAND loop ([host-effect-orchestration.md](host-effect-orchestration.md)). **In motion (2026-07-22+):** witness-realization scheduling + host-effect transport lanes (shell→intent Phase 2) and #7090 returning work on floor execution paths. ### 2.11 Compile-clean shard scope @@ -81,7 +81,7 @@ ### 2.12 Regen oracle & self-host scope -**Today:** `regen_input_sources`, regen skip on PR diffs, self-host staleness inputs. **Subsumes:** `regen_stage0` + frontier carrier. **Disposition:** delete-with-v1 — bulk GENERATED cutover, not piecemeal. **Trigger:** `5-real-fixpoint` gate ([v2-self-hosting.md](v2-self-hosting.md) Wave 4). +**Today:** `regen_input_sources`, regen skip on PR diffs, self-host staleness inputs. **Subsumes:** `v2.workflow.required_regen` + frontier carrier (the `regen_stage0` binary this row named was DELETED at the root by the regen cut). **Disposition:** delete-with-v1 — bulk GENERATED cutover, not piecemeal. **Trigger:** `5-real-fixpoint` gate ([v2-self-hosting.md](v2-self-hosting.md) Wave 4). ### 2.13 Host builtin bridge diff --git a/docs/plans/host-effect-orchestration.md b/docs/plans/host-effect-orchestration.md index 8d7444c6d85..8bb4ff71645 100644 --- a/docs/plans/host-effect-orchestration.md +++ b/docs/plans/host-effect-orchestration.md @@ -18,6 +18,7 @@ apply(target: NodeControlPlane, effect: HostEffect, policy: Policy) -> Receipt NodeControlPlane = HostOs(node) # in-band — transport ∈ {SshShell, LocalShell, SystemdUnit, EmitArtifactThenThinRun} | BmcController(node) # out-of-band — transport ∈ {RedfishRest} + | RunnerLocalHost # current foreign executor; admits only typed runner-local effects HostEffect = ShellCommand{script} | RedfishAction{resource, verb, body} | … # COPRODUCT of effect-kinds Policy (§3c) = OneShotIdempotent | ConvergeToFixpoint Receipt = located/typed core + poll-until-converged task state (NOT just exit-0) @@ -27,7 +28,7 @@ apply(target: NodeControlPlane, effect: HostEffect, policy: Policy) -> Receipt Three refinements proved by driving srv3's BMC live (neat-boar-71), each load-bearing: -- **Target-duality.** A logical node has *two* control planes — in-band host OS (ssh/systemd) and out-of-band BMC (Redfish) — so `apply` targets a **control plane**, not a host address. Pre-OS lifecycle phases (`FactoryDefault → OsInstalled`) are reachable **out-of-band ONLY**: the OS doesn't exist yet, only the BMC does. Both resolve over `fleet_intent` (which already binds `HostIdentity` + `BmcEndpoint` per node). +- **Target identity.** A logical fleet node has *two* control planes — in-band host OS (ssh/systemd) and out-of-band BMC (Redfish) — while a foreign CI executor is represented separately as `RunnerLocalHost`, never as a fabricated fleet identity. Pre-OS lifecycle phases (`FactoryDefault → OsInstalled`) are reachable **out-of-band ONLY**: the OS doesn't exist yet, only the BMC does. The fleet arms resolve over `fleet_intent` (which already binds `HostIdentity` + `BmcEndpoint` per node); the runner-local arm admits only effects explicitly modeled for the current executor. - **`HostEffect` is a coproduct, not a shell string.** A Redfish op is `BootSourceOverride{target:Pxe, enabled:Once}` then `Reset{ForceRestart}` — typed actions, not bash. A stringly `command` field would be the §3 anemic leaf; ssh's shell-string is *one arm*. Dispatch on (control-plane × transport × effect-kind) makes an **incompatible combination (e.g. `RedfishAction` over `SshShell`) a typed mismatch, unwritable by construction** (§5) — not a silent failure. - **Async/polled Receipt.** Redfish `Reset` returns before the machine reboots; the real outcome is observed by **polling** (BootSourceOverrideEnabled flips `Once → Disabled` when firmware consumes it). So the Receipt carries poll-until-converged task state. This *reinforces* the policy axis: BMC ops are **intrinsically converge-shaped** even in a "one-shot" call — `ConvergeToFixpoint` is a property of the effect, not just of ssh-vs-drift.