From be1a0010d53cd6b9676ae1a5a41cdb1612c9ea84 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 00:55:45 +0000 Subject: [PATCH 1/8] WIP: compiler correctness --- ...ompiler-guarantee-recovery-gap-analysis.md | 228 ++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 docs/plans/compiler-guarantee-recovery-gap-analysis.md diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md new file mode 100644 index 00000000000..bc9bd82516e --- /dev/null +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -0,0 +1,228 @@ +# Compiler guarantee recovery — gap analysis + +**Status:** WORKING DRAFT, audit in progress. No code lands from this note. +**Question it answers:** what did this compiler intend to guarantee, and what does it guarantee today? + +## 0. Provenance + +The specification half of the project's authority was lost in the 2026-06-16 doc +bankruptcy (`3127161e878` "cleanup day" #5027, re-deleted in `80ea2664925` #5029). The +epistemology survived into DESIGN.md; the specification did not. Recovered sources, all +readable at `3127161e878^`: + +- `THESIS.md` — the guarantee statement, the tier structure, the complete claims list +- `INVARIANTS.md` — five principles (they map cleanly onto today's DESIGN.md §3–§6) +- `MODELING.md`, `docs/thesis/*` (~10 files), `docs/error-examples.md` + +DESIGN.md today is a strong reconstruction of **how to reason** (§1–§2 axioms and +redundancy), **where facts live** (§3), **what makes them decidable** (§4), **how to fail** +(§5), and **how to work** (§6–§7). What it does not contain is a statement of **what must be +established before a program is `Accepted`**. That absence is the subject of this note. + +## 1. The recovered guarantee statement + +From `THESIS.md`, verbatim: + +> **If it compiles, the declared intent is sound inside the modeled system; what remains +> unverifiable is only external reality not carried in the program graph.** + +And the framing immediately above it: + +> gunbc is a causal engine: it validates that a program's declared causes, dependencies, and +> drains are structurally coherent **before emission becomes a mechanical translation**. + +Emission is specified as the downstream, mechanical half of a two-stage contract. The +upstream half — validation — is the one that was not built. + +## 2. The drop mechanism (the load-bearing finding) + +The claims did not get argued away. They got **priced out**, one at a time, by a live +authority that kept the cost discipline and lost the specification. + +Receipt, `v2.std.orchestration` `pipeline_steps_empty_arm_note`: + +> A `NonEmpty` carrier was considered and **declined**: zero occurrences in tree +> today, and it would touch this type plus every Pipeline constructor for a currently- +> unexercised case (**the purity trap, DESIGN.md sec 6**). + +That reasoning is correct *given today's DESIGN.md* and wrong against the recovered thesis, +where cardinality is Tier 1 — "impossible to write the bug," not an optional refinement. +§6's purity trap exists to bound *unbounded elegance work*; with no claims list to check +against, it also bounds **mandatory structural walls**, and the two are indistinguishable at +the point of decision. + +**Consequence for the fix:** restoring the claims list is not documentation. It is the thing +that makes the next such decision come out differently. Any wall built without it will be +re-declined by the same argument. + +## 3. Status vocabulary + +Enforcement status: + +- **ENFORCED** — the tree refuses the bad program. +- **UNENFORCED** — the carrier exists; nothing checks it. +- **UNEXPRESSIBLE** — there is no carrier. Strictly worse than UNENFORCED: the fix is a + substrate addition, not a check. + +Classified against DESIGN.md §5's three-way test (*wall now* — decidable and grounded / +*wall after grounding* — decidable, waiting on a single authority / *ratchet forever* — +undecidable). + +## 4. Tier 1 — structural correctness ("impossible to write the bug") + +| Claim (THESIS.md) | Today | Receipt | §5 class | +|---|---|---|---| +| Type mismatches caught at compile time | **UNENFORCED** (return position, `data` annotation, generic instantiation) | `fn f() -> Int { "not an int" }` typechecks — probed by execution, PR #7481; argument position *is* checked | wall after grounding | +| …in compiler source | **UNENFORCED by exemption** | `v1.compiler.infer` `module_skips_direct_call_arg_check` — skips `v2.*` and `v1.compiler.*` | wall now | +| Field typos | **PARTIAL** — concrete types checked; through a type variable, not | `v1.compiler.infer` mints `TypeVariable { id: "field_of_type_var" }` instead of refusing | wall after grounding | +| Non-exhaustive matches | **UNVERIFIED** — reported at runtime in the #6848 histogram | needs re-measurement | — | +| Cardinality / multiplicity (empty list into a callee that requires one) | **UNEXPRESSIBLE** | `Cardinality` is one of six connectives in `v2.std.node`, but every construction site is a lens/test fixture — zero `std` or production inhabitants; no `NonEmpty`; v1 forked the *name* onto optionality (`v1.compiler.core` `Cardinality = Required \| CardOptional`) | wall after grounding | +| Method existence | **UNENFORCED — fabricates** | `v1.compiler.infer` `method_pipe_map_keys_values_fallback` else-arm returns the *receiver type* with `kernel_diags: []`; unresolved method stamped `PlainMethodSemantics` | wall now | +| Grounding completeness — "**not** a name-keyed table lookup" | **VIOLATED literally** | `v1.compiler.infer_method` `builtin_function_registry() -> Map` is a name-keyed table (~120 entries), one of ≥5 independent primitive-existence authorities | wall after grounding | +| Circular deps / stale imports / cross-target drift | **UNVERIFIED** | not yet audited | — | +| CX gate: every recursive fn terminates with a proven bound | **UNVERIFIED** | `DescentEvidence` exists (`dag/std/termination.dag`, fail-closed to `DescentUnknown`); enforcement scope unaudited | — | +| Ownership: no aliased mutation in emitted code | **UNVERIFIED — known latent fail-open** | DESIGN.md open thread: emitter silently wraps every `shared_types` member in `Rc` | — | + +## 5. Tier 2 — runtime safety ("proven safe or total") + +The claim is one sentence: **"No partial functions in the runtime."** + +Every `InterpError` variant that can fire on an *accepted* program is a counterexample to it. +The enum is not the specification — it is the **evidence register**. Seventeen variants +today; the ones already known to fire on accepted programs: + +| Variant | Fires on accepted program? | Receipt | +|---|---|---| +| `Unimplemented` | **YES** | PR #7479 — `filter_map` type-checked, reached dispatch as `not yet implemented`, returned HTTP 500 on the lab. Whole-tree compile: 0 blocking errors | +| `CallContractMismatch` | **YES** — runtime wall only | #6896 landed the wall in the interpreter; the compile-time twin does not exist | +| `NoSuchFunction`, `NoSuchVariable`, `NoSuchField` | **reported at runtime** in #6848's floor histogram | UNVERIFIED sub-counts | +| `DivisionByZero` | **reported at runtime** | Tier 2 names it explicitly as "proven safe or made total" | +| `CrossRepresentationEquality` | fail-closed backstop, dead-in-corpus for numerics | DESIGN.md — waits on the `Value::Null` split | +| `PatternMatchFailure` | **UNVERIFIED** | — | + +Genuinely out of scope (environment/resource, not program soundness — these belong in a +*declared not guaranteed* column, with a reason): `EvalBudgetExceeded`, +`WitnessWallBudgetExceeded`, `HostToolUnresolved`, `HostToolRelativePathAmbiguous`, +`ArgvExceedsHostArgMax`. `EarlyReturn` is a control-flow mechanism, not an error (unverified). + +**The discipline to restore:** every variant lands in exactly one column with a reason. +Unclassified is the gap census. This is decidable because the vocabulary is closed — but the +vocabulary must be the *substrate's*, not the v1 Rust seed's. `InterpError` is one +realization's taxonomy; using it as the denominator is the §3 inversion. It is admitted here +as **evidence**, not as spec. + +## 6. Tier 3 — verification from structure + +L4 (emitted matches `.dag` eval) · L5 (same behavior across targets) · L6 (every form +compiles to every target) · L7 (operations obey declared algebraic laws). + +**Entirely unaudited.** Flagged because L6 has a known counterexample shape: `v1.compiler.emit` +`emit_error_expr` renders an "unsupported cast" error expression through the target's +`error_expr_template` rather than refusing at compile time — a form that compiles and emits a +failing artifact. + +## 7. The v2 compiler is separately exposed + +Two problems that compound, with a direction: + +1. **v1 admits v2 source unchecked** — `module_skips_direct_call_arg_check` exempts `v2.*`. +2. **v2 certifies its own nodes** — `v2.std.constraints` `solve_constraints` passes + `graph.root` as source, algebra, *and* the sole candidate; + `v2.std.constraint_satisfaction_predicate` `constraint_satisfaction_preservation_holds` + reduces to `well_formed(root)` checked three times, then relabels it `CanonicalGrounding`. + Specialized inference exists for exactly `Branch`, `Match`, `Loop` + (`v2.compiler.04_infer` `infer_gather_fold_init`); everything else takes the `_` arm. + +So neither compiler ever establishes the facts for v2's source. **v1 deletion does not close +this**, and the §7 self-host frontier reads greener than it is: `emit` can be green-by- +execution on a module whose types were never checked, because emission consumes a `Node` plus +a name string, not a proof. + +## 8. What the thesis predicted, in its own words + +Three recovered lines that name today's defects directly: + +- **The keystone.** *"It only works if the types are actually distinct… That distinctness is + the keystone: no enforcement, no derivable coercion — meaning-in-the-types is cosmetic + without it."* Return position, `data` annotation, and generic instantiation are unchecked, + and `v2.*` is exempt. Since **coercion = emission** is a declared concept unification, the + chain closes: no enforced distinctness → no derivable coercion → **emission runs on + cosmetic types.** +- **Grounding completeness.** *"…algebra inhabitance declared structurally — not string-typed + shortcuts in a lookup table… not a name-keyed table lookup."* `builtin_function_registry` + is literally that. +- **Epistemic stacking**, flagged *"load-bearing for codegen — must not be dropped"*: *"Every + emitter special case is evidence of an ungrounded concept upstream."* + +## 9. Where the ambition sat, for calibration + +`docs/thesis/what-dag-catches-that-normal-compilers-dont.md` — its examples are +non-terminating recursion (CX descent proof), accidentally quadratic, `reverse |> reverse` +(involution ⇒ "equivalent to doing nothing"), `map(f) |> map(g)` fusion, non-idempotent +workflow marked retry-safe, `create_resource()` in a retry loop, `fib` at O(2ⁿ). Closing +line: *"No special-case analysis. No lint rules. No opt-in annotations. The algebra does the +work."* + +The live defects are "does this method exist" and "does the body match the declared return." +**The documented ambition is two tiers above mainstream compilers; the current position is one +tier below them.** That gap is the honest statement of the problem. + +## 10. Evidence status + +**Verified by reading `main` (`26f747fd9ec`) during this pass:** the method fallback; +`resolve_builtin_call_type`; `module_skips_direct_call_arg_check`; the `Unimplemented` +dispatch default; `filter_map_contract` present with zero seed implementation (`flat_map` +registered, for contrast); v2 self-grounding end-to-end; v2's three specialized arms; +`field_of_type_var`; 63 `PrimitiveContract` rows; `Cardinality` declared with zero production +inhabitants; v1's `Cardinality` name fork; absence of `NonEmpty`; the +`pipeline_steps_empty_arm_note` decline; the `emit_error_expr` cast site. + +**Carried forward UNVERIFIED — do not cite until measured:** #6848's floor histogram +(1,454 pass / 149 fail; 66 `contains`, 40 no-such-function, 6 undefined-variable); #6896's +32 malformed sites / 180 intermediate failures; the "104 `TypeMismatch` false positives" from +the exemption experiment (**no receipt found at all** — this is the entire difficulty estimate +for removing the exemption); the fallback-arm census figures (2,586 / 408 / 24 / 198). + +**Known citation defect in the source audit:** PR #5585 was cited for the emitted-`panic!` +claim; #5585 is base64/RFC 4648 in `std.encoding`. The claim is true, the receipt was +fabricated. (§3 citation class.) + +## 11. Audit queue + +1. Recover the rest of `docs/thesis/` — `correctness-dimensions`, `what-falls-out`, + `two-groundings`, `the-derived-homomorphism`; and `docs/error-examples.md`, described as + *"TDD targets for the compiler… the error message is the acceptance criterion"* — a + ready-made acceptance corpus. +2. Re-measure the floor histogram, bucketed **statically-decidable vs genuinely-runtime**. + This is an execution, not a design, and it is what denominates the work in displaced cost + (§6) instead of elegance. +3. Audit Tier 3 (L4–L7) and the unverified Tier 1 rows. +4. Locate or refute the 104-false-positive claim. +5. Reconcile the recovered claims list against the DESIGN.md open thread *"enforcement intent + — ask once, compile forever."* That thread proposes minting `StandingIntent` to enforce + claim⇄coverage. The claims list already carried that rule in prose — *"If a claim IS here + but the ROADMAP has no track for it, that's a gap"* — so the thread should be **grounded + on the recovered list, not re-coined** (§3). + +## 12. Proposed sequencing (for discussion, not yet agreed) + +**Step 1 — restore the specification.** Re-home the guarantee statement, the tier claims, and +the claims-list completeness rule into DESIGN.md. Mostly transcription of text already in git +history, annotated with §4/§5 status. This is first because §2 explains why nothing else +holds without it. + +**Step 2 — the gap census against that**, replacing this draft's UNVERIFIED rows with +measurements. + +**Step 3 — walls, in dependency order.** Note two orderings that differ from the obvious one: + +- **Primitive single-authority precedes the method-existence wall.** Method existence is + currently spread across ≥5 name sets (registry, `PrimitiveContract` rows, algebra + templates, interpreter arms, per-target templates). A wall built against any one of them + reproduces #7479 inverted — correctly refusing `filter_map`, wrongly refusing what + legitimately resolves elsewhere. +- **The `v2.*` exemption comes off only after the 104 are re-adjudicated.** Otherwise the + likely outcome is that it goes back on. + +DESIGN.md is untouched by this note; it is the load-bearing authority and the §1/§4 addition +needs agreement on shape first. From 40d615c3680f104404653c06243c9447c1689d7d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 01:31:51 +0000 Subject: [PATCH 2/8] Bind the guarantee-recovery analysis into the doc graph MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/doc_graph_roots.dag | 12 +++ ...ompiler-guarantee-recovery-gap-analysis.md | 98 ++++++++++++++++++- 2 files changed, 106 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index 437b91d0078..edb921e0e5a 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -263,6 +263,18 @@ data hand_authored_doc_binds: List = [ work: DeclarationRef { module_path: "gunbc.ci_spec", decl_name: "gunbc_ci_deploy_srv1_stage", field: WholeDeclaration }, dissolution: HasTrigger { text: "all FOUR findings this diagnosis names are facts on their carriers: (1) srv1 deployment holds a typed HOST-SIDE lease spanning mutation, readiness and identity readback — a runner label or concurrency group is mitigation only, since neither excludes the operator apply path — plus a counted refusal when the candidate is not the authoritative revision under whichever revision authority is ruled, (2) the healthz fingerprint identifies what is DEPLOYED (source closure and binary artifact identity, not build provenance alone) rather than five rendered bodies, (3) the refusal path preserves the decl's located diagnosis instead of substituting a render complaint, with control-byte admission decided per CursorAction and DynamicLineState rather than one global roster, and (4) job_yaml emits Job.concurrency with a discriminating RED. Then the doc deletes with this row. Twice corrected in review: review 44735 caught that the trigger omitted the misattributed-refusal defect entirely, and review 44766 caught that it would have accepted scheduler-only exclusion, source-only identity and a global byte-roster fix" }, }, + HandAuthoredDocBind { + home: PlanDoc, + slug: "compiler-guarantee-recovery-gap-analysis", + work: DeclarationRef { module_path: "v1.compiler.infer", decl_name: "module_skips_direct_call_arg_check", field: WholeDeclaration }, + dissolution: HasTrigger { text: "the recovered guarantee statement and tier claims are re-homed into DESIGN.md as its specification half, AND every Tier 1/Tier 2 row in the analysis is either closed on its carrier or migrated to a registered gunbc.plan.Plan row. This bind names the escape hatch specifically because docs/thesis/correctness-dimensions.md states the dimension contract as 'enforced universally — all code is subject to all dimensions, no escape hatch, no wrapper functions', and module_skips_direct_call_arg_check is that clause's one named violation in tree: it exempts v2.* and v1.compiler.* from direct-call argument checking, so the compiler being bootstrapped is authored under weaker checks than ordinary source. Deleting it is the analysis's terminal Tier 1 acceptance and its removal ends this row" }, + }, + HandAuthoredDocBind { + home: PlanDoc, + slug: "compiler-guarantee-recovery-gap-analysis", + work: DeclarationRef { module_path: "v2.std.constraints", decl_name: "solve_constraints", field: WholeDeclaration }, + dissolution: HasTrigger { text: "v2 inference stops certifying source identity as semantic grounding. Today solve_constraints passes graph.root as source_facts, algebra AND the sole candidate, and v2.std.constraint_satisfaction_predicate.constraint_satisfaction_preservation_holds requires algebra == source_facts && candidate == source_facts — so the proof reduces to well_formed(root) checked three times and is then relabelled CanonicalGrounding. The row dissolves when a candidate is derived rather than supplied, or the generic arm returns a typed compile refusal instead of an accepted self-grounded InferredTree" }, + }, ] fn hand_authored_doc_graph_roots() -> List { diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index bc9bd82516e..1c7afff207a 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -154,6 +154,93 @@ Three recovered lines that name today's defects directly: - **Epistemic stacking**, flagged *"load-bearing for codegen — must not be dropped"*: *"Every emitter special case is evidence of an ungrounded concept upstream."* +## 8b. The acceptance corpus was recovered — and it has a hole in the same place + +`docs/error-examples.md` survived intact (487 lines, readable at `3127161e878^`). It is +structured as a RED-control corpus: `.dag` input, the exact expected compiler error, the +algebra that catches it, and why a traditional compiler cannot. Its own framing: + +> These serve as TDD targets: each example is a test case. The `.dag` code is the test input; +> the error message is the acceptance criterion. When the feature lands, the test should pass. + +Seven cases: (1) non-terminating recursion through type resolution · (2) cross-service data +corruption through non-idempotent retry · (3) redundant computation across service boundaries +· (4) accidentally quadratic with a non-obvious cause · (5) infrastructure drift through +partial failure · (6) semantic cancellation across function boundaries · (7) exponential +blowup from unguarded recursive branching. + +**The finding: every one is a Tier 2-or-above case. Not one is Tier 1.** There is no +method-existence example, no declared-return-conformance example, and — searched explicitly — +**no cardinality or empty-list example anywhere in the corpus** (zero occurrences of +`empty` / `cardinal` / `NonEmpty` / `arity` outside an unrelated `fold` body). + +This revises §2's account of the drop. The specification did not merely get priced out later; +it was **under-specified at the source**. Tier 1 was treated as solved-by-assumption and +given no acceptance criteria, while the exotic wins got seven fully-worked ones. So the +foundation had no test, therefore no consumer, therefore nothing to notice it was never +built — the specification-without-execution trap (§5) operating on the *specification itself*. + +**Consequence for salvage, and it is the load-bearing one:** the recovered corpus is directly +usable for Tier 2/3 walls, but **the Tier 1 RED controls do not exist and must be authored.** +They are the cheapest and most urgent artifacts in this whole effort — each is a +three-line `.dag` program — and they were never written because no one imagined needing them. +The user-supplied case is the archetype and belongs in the corpus as example 0: + +```dag +// callee requires at least one; caller can supply zero. +// Today: unexpressible — no NonEmpty carrier, Cardinality connective uninhabited. +``` + +## 8c. The dimension architecture — recovered contract, and it is still standing + +`docs/thesis/correctness-dimensions.md` defines the mechanism that was supposed to make all of +this uniform, and it is the strongest salvage news in this note. + +> Correctness is not one property — it is many orthogonal dimensions… In gunbc they are +> **inescapable properties of the system, like conservation laws in physics. You don't opt +> into gravity.** + +Four-part contract for every dimension: (1) declared in `std/` as a structural type with +lattice operations; (2) **computed at binding sites during inference — no separate analysis +pass**; (3) carried through the IR on bindings; (4) **enforced universally — all code is +subject to all dimensions, no escape hatch, no wrapper functions.** + +**Clause 4 is violated by name.** `v1.compiler.infer` `module_skips_direct_call_arg_check` is +exactly an escape hatch, and it exempts the two module trees that most need the dimension. + +**But the carriers are real and present**, verified on `main`: + +- `v1.compiler.infer_env` `TypeBinding { name, resolved, provenance: SubValueRelation }` — + the thesis names `TypeBinding.provenance`, and it is there. +- `v1.compiler.core` `ExprCall { call_semantics, descent_evidence: List? }` + — the thesis names `ExprCall.descent_evidence`, and it is there. + +So the mechanism the thesis describes was **built, not just designed**. What did not happen is +the rest of the dimensions moving onto it. Restated in the thesis's own table format +(*Carried on bindings* / *Enforced* are the load-bearing columns): + +| Dimension | Declared today | Carried on bindings | Enforced | +|---|---|---|---| +| Type safety | `dag/std/types.dag` | `TypeBinding.resolved` | **Partial** — argument position only; return, `data` annotation, generic instantiation unchecked; `v2.*`/`v1.compiler.*` exempt | +| Termination | `dag/std/termination.dag` (BoundedLattice, bottom = fail-closed) | `TypeBinding.provenance`, `ExprCall.descent_evidence` | **UNVERIFIED** — thesis-era status was "Partial, 421 violations, non-blocking"; needs re-measurement | +| Cardinality / multiplicity | **nowhere** — connective uninhabited | No | **UNEXPRESSIBLE** (§4) | +| Ownership | `src/v1/ownership.dag`, `src/v2/lens/ownership.dag` | No — still a separate pass | **Partial**, plus a known latent fail-open (Rc wrap) | +| Side effects | `dag/std/behavioral.dag`, `dag/std/effects.dag` | No | Consumers now exist (`std.effect_grant`, `std.realization`, `gunbc.host_effect`) — an improvement on the thesis-era "declared, not consumed" — but **not at binding sites** | +| Idempotence | `dag/std/effects.dag` (lattice from `EffectShape`) | No | No | +| Purity | not declared | — | No | +| Space bounds | not declared | — | No | + +**Why this matters for sequencing:** two of eight dimensions reached the binding carrier and +the carrier still works. The salvage is therefore *not* an architecture rebuild — it is +finishing a migration that stalled, plus deleting one escape hatch. That is a materially +cheaper and more defensible proposition than the wall-by-wall roadmap implies, and it should +be the frame for step 3. + +The thesis also names its own falsification test: *"If user-defined dimensions work the same +as built-in ones, the mechanism is general. If they require special compiler support, the +mechanism is incomplete."* Unaudited. `src/v1/dimensions-design.md` (396 lines, recoverable) +is the abstracted mechanism and has not been read yet. + ## 9. Where the ambition sat, for calibration `docs/thesis/what-dag-catches-that-normal-compilers-dont.md` — its examples are @@ -189,10 +276,13 @@ fabricated. (§3 citation class.) ## 11. Audit queue -1. Recover the rest of `docs/thesis/` — `correctness-dimensions`, `what-falls-out`, - `two-groundings`, `the-derived-homomorphism`; and `docs/error-examples.md`, described as - *"TDD targets for the compiler… the error message is the acceptance criterion"* — a - ready-made acceptance corpus. +1. ~~Recover `docs/error-examples.md`~~ **DONE — see §8b.** Recovered intact; 7 cases, all + Tier 2+, zero Tier 1. Still to pull: the rest of `docs/thesis/` — + `correctness-dimensions`, `what-falls-out`, `two-groundings`, `the-derived-homomorphism`. +1b. **Author the missing Tier 1 RED controls** (new, and the cheapest item here). They never + existed. Start with the cardinality archetype, method existence, and declared-return + conformance — each a three-line `.dag` program with an expected-error acceptance criterion, + in the recovered corpus's own format. 2. Re-measure the floor histogram, bucketed **statically-decidable vs genuinely-runtime**. This is an execution, not a design, and it is what denominates the work in displaced cost (§6) instead of elegance. From f71fee95b36de1b75ccb88e6bb4db0d9aafe5df6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 01:49:51 +0000 Subject: [PATCH 3/8] WIP: compiler correctness --- ...ompiler-guarantee-recovery-gap-analysis.md | 101 ++++++++++++------ 1 file changed, 66 insertions(+), 35 deletions(-) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 1c7afff207a..2722e6841e2 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -34,39 +34,69 @@ And the framing immediately above it: Emission is specified as the downstream, mechanical half of a two-stage contract. The upstream half — validation — is the one that was not built. -## 2. The drop mechanism (the load-bearing finding) - -The claims did not get argued away. They got **priced out**, one at a time, by a live -authority that kept the cost discipline and lost the specification. - -Receipt, `v2.std.orchestration` `pipeline_steps_empty_arm_note`: - -> A `NonEmpty` carrier was considered and **declined**: zero occurrences in tree -> today, and it would touch this type plus every Pipeline constructor for a currently- -> unexercised case (**the purity trap, DESIGN.md sec 6**). - -That reasoning is correct *given today's DESIGN.md* and wrong against the recovered thesis, -where cardinality is Tier 1 — "impossible to write the bug," not an optional refinement. -§6's purity trap exists to bound *unbounded elegance work*; with no claims list to check -against, it also bounds **mandatory structural walls**, and the two are indistinguishable at -the point of decision. - -**Consequence for the fix:** restoring the claims list is not documentation. It is the thing -that makes the next such decision come out differently. Any wall built without it will be -re-declined by the same argument. - -## 3. Status vocabulary - -Enforcement status: - -- **ENFORCED** — the tree refuses the bad program. -- **UNENFORCED** — the carrier exists; nothing checks it. -- **UNEXPRESSIBLE** — there is no carrier. Strictly worse than UNENFORCED: the fix is a - substrate addition, not a check. - -Classified against DESIGN.md §5's three-way test (*wall now* — decidable and grounded / -*wall after grounding* — decidable, waiting on a single authority / *ratchet forever* — -undecidable). +## 2. The failure history (revised after independent review, 2026-07-31) + +An earlier draft of this section told a two-part story: the spec was lost, then the claims +were priced out one at a time. Independent review corrected it, and the corrected history has +**three distinct failure modes**, each with its own receipt: + +1. **The implementation never matched the specification, even while the specification was + live.** `module_skips_direct_call_arg_check` (the `v2.*`/`v1.compiler.*` exemption) dates + to **2026-06-08** (`a13fb57b149`, first `-S` occurrence) — eight days *before* the + 2026-06-16 bankruptcy. The gaps predate the loss of the document that named them. +2. **The status ledger overstated completeness.** The recovered + `docs/thesis/correctness-dimensions.md` table marks Type safety as *"Yes (blocking)"* + while return-position, `data`-annotation, and generic-instantiation checking did not + exist and the compiler-module exemption was live. So "we had it and lost it" is wrong; + the honest statement is *"it was declared DONE, was not, and then the declaration that + could have been audited was deleted."* +3. **The bankruptcy removed the contract against which (2) could have been noticed.** + DESIGN.md kept the epistemology and the cost discipline; nothing survived that says what + must be established before `Accepted`. + +**A withdrawn receipt, kept for the record:** an earlier draft cited `v2.std.orchestration` +`pipeline_steps_empty_arm_note` (the declined `NonEmpty` carrier) as proof that +a required invariant was priced out by §6's purity trap. Independent review rejected that +reading and the rejection is correct: the note *deliberately* gives the empty pipeline total +no-op semantics (empty conditional arms emit the bash no-op `:`; a both-empty `If` is "run +the condition, discard the outcome"). Emptiness there is a **legitimate total semantics**, so +the decline was a correct engineering decision, not a dropped wall. The note remains a fair +illustration of the *decision procedure* — a carrier addition priced by §6 with no +specification to consult, "revisit if construction sites appear" as the only trigger — but +it is not evidence the procedure ever produced a wrong answer. No receipt currently in hand +shows a *required* invariant being declined. + +**Consequence for the fix, sharpened by mode (2):** restoring the claims list is still the +move that makes the next decline-decision answerable — but historical claims must enter as +**provenance and candidate obligations, never as implementation truth**. A recovered claim +lands as `Required` + `CurrentStatus: Gap` until a discriminating RED/green pair proves +otherwise. Copying the historical "DONE" column would repeat mode (2) verbatim. + +## 3. Status vocabulary (widened after independent review) + +The original three-state vocabulary (ENFORCED / UNENFORCED / UNEXPRESSIBLE) lost exactly the +information this tree carries: a guarantee can have a carrier that proves nothing, a wall +that holds only for literals, or a check that fires at the runtime boundary rather than at +compile time — and each of those has a different fix. Working states, adopted from the +independent review: + +`Absent` · `Declared` · `RepresentableButForgeable` · `LiteralOnlyWall` · `LocallyChecked` · +`RuntimeBoundaryOnly` · `StaticallyPropagated` · `ConstructionWall` · +`TargetRealizationGated` · `ExternalNotGuaranteed` · `UnknownUnmeasured` + +Calibration examples, each verified on `main`: `NonEmptyList` is +RepresentableButForgeable; string `non_empty` where-refinement is LiteralOnlyWall; a +nonliteral refined argument is RuntimeBoundaryOnly (five `WhereRefinementUnenforced` deferral +reasons are enrolled as *advisory* — `v1.compiler.core` +`where_refinement_deferral_reason_scaffold_note`); v2 loop termination is a ConstructionWall +(`v2.std.cardinality` requires a declared loop measure, fail-closed to `DescentUnknown`); +unknown method is a fail-open Absent; host state is ExternalNotGuaranteed by the guarantee +statement itself. + +This vocabulary is prose-interim: it becomes a typed enum on the claim carrier when the +guarantee authority lands (§11), the same way `DescentEvidence` and `DecodeFidelity` model +their own verdicts. The DESIGN.md §5 wall-classification (*wall now* / *wall after +grounding* / *ratchet forever*) stays as the orthogonal decidability axis. ## 4. Tier 1 — structural correctness ("impossible to write the bug") @@ -75,8 +105,9 @@ undecidable). | Type mismatches caught at compile time | **UNENFORCED** (return position, `data` annotation, generic instantiation) | `fn f() -> Int { "not an int" }` typechecks — probed by execution, PR #7481; argument position *is* checked | wall after grounding | | …in compiler source | **UNENFORCED by exemption** | `v1.compiler.infer` `module_skips_direct_call_arg_check` — skips `v2.*` and `v1.compiler.*` | wall now | | Field typos | **PARTIAL** — concrete types checked; through a type variable, not | `v1.compiler.infer` mints `TypeVariable { id: "field_of_type_var" }` instead of refusing | wall after grounding | -| Non-exhaustive matches | **UNVERIFIED** — reported at runtime in the #6848 histogram | needs re-measurement | — | -| Cardinality / multiplicity (empty list into a callee that requires one) | **UNEXPRESSIBLE** | `Cardinality` is one of six connectives in `v2.std.node`, but every construction site is a lens/test fixture — zero `std` or production inhabitants; no `NonEmpty`; v1 forked the *name* onto optionality (`v1.compiler.core` `Cardinality = Required \| CardOptional`) | wall after grounding | +| Application arity / call shape (missing, extra, misspelled-label args) | **fail-open by construction of the walk** | `v1.compiler.infer` `direct_call_arg_mismatch_diags` is *formal-driven*: per formal it seeks a same-named arg, else falls back to the **positional** arg at the same index (a misspelled label silently binds by position if the type fits), and `Absent => []` (missing arg → no diagnostic); extra args are never visited. The `ArityMismatch` diagnostic is **type-constructor** arity ("expects N *type* arguments"), not invocation arity — invocation arity has no compile diagnostic; #6896's wall is runtime-only | wall now | +| Non-exhaustive matches | **PARTIAL — one confirmed silent arm** | resolved coproducts have exhaustiveness machinery; but `v1.compiler.infer_patterns` `lookup_variant_in_type` / `lookup_field_in_variant` both have `PatternLookupBlocked => node_lookup_failed(diagnostics: [])` — a blocked scrutinee lookup fails with **zero diagnostics** and the pattern types as `error_type` (`PatternDynamic`, by contrast, does diagnose at these sites). "Exhaustiveness not established" is treated as success-adjacent, not refused | wall after grounding | +| Cardinality / multiplicity (empty list into a callee that requires one) | **RepresentableButForgeable, not statically propagated** — reclassified from UNEXPRESSIBLE after independent review | Representation exists: `v2.std.refinement` `Validation`/`Refined`/`refine`, a `NonEmptyList` manual fixture (`v2.test.claim.manual.refinement_nonempty_list` + testgen anchor), and **green fold-propagation witnesses** (`cardinality_fold_propagation_test`: `cardinality_is_a_fold_homomorphism`, `fold_overflow_rejects`). Forgeable: `Refined` is a public record — `refined_vacuous_stub_pack`'s `Rejected` arm literally returns `Refined { base }`, so the carrier proves nothing about validation. Not propagated: no cardinality lattice in signatures (`v2.std.cardinality` is loop-termination), `InterfaceSummary` (`dag/std/interface_summary.dag`) carries no cardinality slot, no transfer functions across `map`/`filter`/`concat`. The substrate `Cardinality` connective remains production-uninhabited and v1 forks the name onto optionality (`Required \| CardOptional`) | wall after grounding | | Method existence | **UNENFORCED — fabricates** | `v1.compiler.infer` `method_pipe_map_keys_values_fallback` else-arm returns the *receiver type* with `kernel_diags: []`; unresolved method stamped `PlainMethodSemantics` | wall now | | Grounding completeness — "**not** a name-keyed table lookup" | **VIOLATED literally** | `v1.compiler.infer_method` `builtin_function_registry() -> Map` is a name-keyed table (~120 entries), one of ≥5 independent primitive-existence authorities | wall after grounding | | Circular deps / stale imports / cross-target drift | **UNVERIFIED** | not yet audited | — | From 9ca8d009970055e8030bcfce09b333d7809055c9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 01:51:35 +0000 Subject: [PATCH 4/8] =?UTF-8?q?Reconcile=20the=20gap=20analysis=20against?= =?UTF-8?q?=20the=20independent=20review=20=E2=80=94=20three=20corrections?= =?UTF-8?q?=20adopted,=20receipts=20verified?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (a13fb57b149), 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) --- ...ompiler-guarantee-recovery-gap-analysis.md | 162 +++++++++++++++--- 1 file changed, 138 insertions(+), 24 deletions(-) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 2722e6841e2..be827dcea5e 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -114,6 +114,32 @@ grounding* / *ratchet forever*) stays as the orthogonal decidability axis. | CX gate: every recursive fn terminates with a proven bound | **UNVERIFIED** | `DescentEvidence` exists (`dag/std/termination.dag`, fail-closed to `DescentUnknown`); enforcement scope unaudited | — | | Ownership: no aliased mutation in emitted code | **UNVERIFIED — known latent fail-open** | DESIGN.md open thread: emitter silently wraps every `shared_types` member in `Rc` | — | +### 4b. The cardinality case was independently re-derived in-tree — the intent is not lost, the design pass is + +The sharpest discovery of the reconciliation pass: +`docs/plans/interface-summary-declared-use-arity.md` **§3.1 "Value-cardinality arity at +seams (operator direction 2026-07-04)"** records the operator's exact scenario — *"the +canonical divergence being one side honoring the empty list while the other assumes +non-empty. Today that disagreement is a runtime surprise or a silently-degenerate arm; **the +operator wants it a hard error in the language.**"* — with the seam design sketched (the +invariant is an interface fact in `InterfaceSummary`'s contract slot; a `0..n` producer +feeding a `1..n` consumer is *"a located type mismatch at the boundary — unwritable, not +reviewed"*). Its FLAG E names what is missing: the cardinality lattice itself, deliberately +not designed there. `docs/plans/cardinality-refinement.md` (status: scoping; registered as +`gunbc.plans.cardinality_refinement`) carries the lattice proposal — a **closed decidable +predicate vocabulary** (`Length`, `NonEmpty`, `Bounded`, `Width`, all linear +arithmetic over counts, chosen precisely to stay inside §4's bounded substrate where general +refinement would not) plus fold-propagation, whose std seed already has green witnesses. + +So the thesis-era guarantee was dropped, and then **the operator re-derived it from scratch +on 2026-07-04** — which is simultaneously the strongest evidence that the guarantee is real +(it keeps being wanted independently) and of what the missing specification costs (it had to +be re-invented rather than consulted, and 27 days later the design pass has not started +because nothing ranks it). The salvage for this axis is therefore **not new design**: it is +connecting three artifacts that already exist — the operator direction, the scoped lattice +plan, and the green fold-propagation seed — and closing the two named gaps (unforgeable +construction; signature-level propagation through `InterfaceSummary`). + ## 5. Tier 2 — runtime safety ("proven safe or total") The claim is one sentence: **"No partial functions in the runtime."** @@ -169,6 +195,51 @@ this**, and the §7 self-host frontier reads greener than it is: `emit` can be g execution on a module whose types were never checked, because emission consumes a `Node` plus a name string, not a proof. +**Calibration added after independent review — the terminal is better than the phase +carriers.** Three nuances that bound the claim: + +- `validate_then_compile` (`v2.compiler.00_compile`) is a real single gate authority + ("no second gate surface exists"): the root roster (`accumulator_copy`, `determinism`, + `machine_shape`, `mandatory_tag`) plus the per-node roster (`fact_density`, + `unit_modeling`) fire on every compile before an output exists. The staging *shape* is + worth keeping. +- The evaluator refuses unrealized semantics (`v2_eval_semantics_deferred`) rather than + fabricating results, and `canonical_grounding_for_node` does impose a coherence gate + (`node == facts.grounding.node`) — though a self-certified fact passes that gate *by + construction*, so it screens malformed trees, not fabricated groundings. +- v2 **loop termination is a genuine construction wall** (`v2.std.cardinality`: a loop + without a declared bound measure gets `cardinality_loop_bound_undeclared`; descent + fail-closed to `DescentUnknown`). + +So the correct diagnosis is not "v2 inference is fake"; it is: Branch/Match/Loop carry real +semantic work, loop termination is walled, the *generic* arm self-certifies, the terminal +may still refuse later for other reasons — and therefore **`InferredTree` is not a +trustworthy proof boundary**: its lens consumers read facts whose generic entries were never +derived. The fix is the phase-carrier separation (§12 stage 4), not a rebuild of the +terminal. + +## 7b. Where the recovered specification must land — and proof the prose already drifted + +Two facts that redirect step 1 of the sequencing: + +**DESIGN.md is a projection, not the authority.** `dag/gunbc/design_document.dag` carries the +document's content as data rows; DESIGN.md is generated from it. So "re-home the guarantee +statement into DESIGN.md" is mis-aimed as stated — the guarantee lands as **`.dag` rows** +(the claims authority of §11), and the DESIGN.md text is derived. Hand-editing the markdown +would mint a parallel representation of exactly the kind §3 forbids. + +**The prose has already drifted from the substrate, on the substrate's most load-bearing +sentence.** DESIGN.md §4 says the closed vocabulary is *"6 connectives + 5 behaviors"*. +`v2.std.node` declares **six** behaviors: `Value | Transform | Branch | Loop | Bind | +Match`. The recovered thesis is sharper about what that means: it listed five behaviors and +declared *"Substrate extension is a C1-class stop signal (seventh connective or **sixth +behavior**) — all four dissolution patterns … must fail with structural arguments before +extension is allowed."* Whether `Match`'s promotion to a behavior was adjudicated under that +rule is not established here (it may well have been — v2's `Match` inference is real work); +what is established is that the live authority's count is wrong against the live substrate, +which is a clean specimen of why the guarantee must be modeled where a lens can read it, +not written where only a reader can. + ## 8. What the thesis predicted, in its own words Three recovered lines that name today's defects directly: @@ -253,8 +324,8 @@ the rest of the dimensions moving onto it. Restated in the thesis's own table fo | Dimension | Declared today | Carried on bindings | Enforced | |---|---|---|---| | Type safety | `dag/std/types.dag` | `TypeBinding.resolved` | **Partial** — argument position only; return, `data` annotation, generic instantiation unchecked; `v2.*`/`v1.compiler.*` exempt | -| Termination | `dag/std/termination.dag` (BoundedLattice, bottom = fail-closed) | `TypeBinding.provenance`, `ExprCall.descent_evidence` | **UNVERIFIED** — thesis-era status was "Partial, 421 violations, non-blocking"; needs re-measurement | -| Cardinality / multiplicity | **nowhere** — connective uninhabited | No | **UNEXPRESSIBLE** (§4) | +| Termination | `dag/std/termination.dag` (BoundedLattice, bottom = fail-closed) | `TypeBinding.provenance`, `ExprCall.descent_evidence` | **UNVERIFIED in v1** — thesis-era status was "Partial, 421 violations, non-blocking"; **walled in v2 for loops** (`v2.std.cardinality` bound measure) | +| Cardinality / multiplicity | `v2.std.refinement` (+ scoped lattice plan `gunbc.plans.cardinality_refinement`) | No | **RepresentableButForgeable** — see §4/§4b; operator re-directed 2026-07-04 | | Ownership | `src/v1/ownership.dag`, `src/v2/lens/ownership.dag` | No — still a separate pass | **Partial**, plus a known latent fail-open (Rc wrap) | | Side effects | `dag/std/behavioral.dag`, `dag/std/effects.dag` | No | Consumers now exist (`std.effect_grant`, `std.realization`, `gunbc.host_effect`) — an improvement on the thesis-era "declared, not consumed" — but **not at binding sites** | | Idempotence | `dag/std/effects.dag` (lattice from `EffectShape`) | No | No | @@ -305,6 +376,25 @@ for removing the exemption); the fallback-arm census figures (2,586 / 408 / 24 / claim; #5585 is base64/RFC 4648 in `std.encoding`. The claim is true, the receipt was fabricated. (§3 citation class.) +**Independent-review verification ledger (2026-07-31 pass, all checked on `main`):** +CONFIRMED — `Refined` forgeable incl. the `stub_pack` `Rejected => Refined { base }` arm; +five advisory `WhereRefinementUnenforced` deferral reasons; `NonEmptyList` manual fixture + +testgen anchor; green `cardinality_fold_propagation_test`; `direct_call_arg_mismatch_diags` +formal-driven walk incl. positional fallback for misspelled labels; `ArityMismatch` = +type-constructor arity; `validate_then_compile` single-door roster exactly as stated; +`v2.std.cardinality` loop-bound wall; exemption introduction 2026-06-08 (pre-bankruptcy); +six behaviors in `v2.std.node` vs DESIGN.md's "5"; DESIGN.md projected from +`gunbc.design_document`; operator direction 2026-07-04 in +`interface-summary-declared-use-arity.md` §3.1. CORRECTED against the review — +`PatternDynamic` *does* diagnose at the variant/field lookup sites (`VariantNotFound` / +`FieldNotFound` with `type_name: "unresolved"`); the silent `diagnostics: []` arm is +`PatternLookupBlocked` specifically. PRECISION — the `0..n`/`1..n` seam is an operator +*direction* recorded inside a signed lane, with its lattice design pass (FLAG E) explicitly +not started; "operator-signed design" slightly overstates it. STILL UNLOCATED — the "104 +TypeMismatch false positives" (no receipt in tree or history found by either pass), and the +specific historical wording "branch, argument, and return type checking DONE" (the +`correctness-dimensions.md` *"Yes (blocking)"* row is the receipt actually in hand). + ## 11. Audit queue 1. ~~Recover `docs/error-examples.md`~~ **DONE — see §8b.** Recovered intact; 7 cases, all @@ -325,25 +415,49 @@ fabricated. (§3 citation class.) but the ROADMAP has no track for it, that's a gap"* — so the thread should be **grounded on the recovered list, not re-coined** (§3). -## 12. Proposed sequencing (for discussion, not yet agreed) - -**Step 1 — restore the specification.** Re-home the guarantee statement, the tier claims, and -the claims-list completeness rule into DESIGN.md. Mostly transcription of text already in git -history, annotated with §4/§5 status. This is first because §2 explains why nothing else -holds without it. - -**Step 2 — the gap census against that**, replacing this draft's UNVERIFIED rows with -measurements. - -**Step 3 — walls, in dependency order.** Note two orderings that differ from the obvious one: - -- **Primitive single-authority precedes the method-existence wall.** Method existence is - currently spread across ≥5 name sets (registry, `PrimitiveContract` rows, algebra - templates, interpreter arms, per-target templates). A wall built against any one of them - reproduces #7479 inverted — correctly refusing `filter_map`, wrongly refusing what - legitimately resolves elsewhere. -- **The `v2.*` exemption comes off only after the 104 are re-adjudicated.** Otherwise the - likely outcome is that it goes back on. - -DESIGN.md is untouched by this note; it is the load-bearing authority and the §1/§4 addition -needs agreement on shape first. +## 12. Proposed sequencing (reconciled with the independent review; for operator sign-off) + +**Stage 1 — the claims authority and the probe corpus land together, both as `.dag`.** +Model the guarantee population (the review's G0–G9 families are a good candidate cut: +binding · formation · inhabitance · invocation · domain/totality · control soundness · +semantic dimensions · realization · fidelity · external boundary) as rows with: identity, +proof mode, authoritative carrier, negative RED, positive control, per-compiler enforcement +status, and **a named consumer in `Accepted`**. Two §3 grounding rules so this doesn't fork +existing machinery: the families ground on the recovered *dimension* architecture (§8c) and +the DESIGN open thread `StandingIntent` — this IS that thread's missing claims list, not a +second taxonomy beside it; and per §7b the authority is `.dag` rows projected into DESIGN.md, +never hand-edited prose. Historical claims enter `Required` + `Gap` (mode-2 rule, §2). +The probe corpus lands simultaneously as **enrolled expecting-red rows** (the known-red +quarantine mechanism already exists: rows execute *expecting* red, so a wall landing flips +them loudly to controls). That makes the corpus a continuous measurement of the gap from day +one, before any wall exists — each probe that compiles-when-it-should-refuse is a counted +deficit, not an anecdote. + +**Stage 2 — close the ordinary premises (wall-now set):** method/callable existence; exact +call labels and counts (the §4 application-arity row); return/`data`/field/generic +inhabitance; `PatternLookupBlocked` refusing instead of `[]`; delete the success-shaped +fallbacks. One staging correction to the review's interim method wall: the +**zero-resolution half lands now** (strictly narrowing — refuse when *no* path resolves a +method; matches runtime reality, cannot red legitimate code), but the **ambiguity half +(>1 resolution) starts as a census**, walled only after the primitive-identity join defines +which dual-path resolutions are the *same* primitive — otherwise `map` resolving via both +registry and algebra template reds the whole corpus on day one and the wall gets reverted +exactly the way the 104 preserved the exemption. + +**Stage 3 — one cardinality vertical slice** (§4b: connect the 2026-07-04 operator +direction + the scoped lattice plan + the green fold seed; acceptance = the operator's +scenario refusing at the seam, with the nonempty-proof positive control compiling). + +**Stage 4 — v2 phase carriers** (source ≠ inferred ≠ realized, so self-grounding becomes +type-invalid; keep the `validate_then_compile` door). + +**Stage 5 — primitive identity consolidation** (definition / realization / cost as three +facts on one identity; dispatch derived, not hand-listed). + +**Stage 6 — remove the compiler-source exemption on fresh evidence** (rerun the probes over +`v2.*`/`v1.compiler.*`, classify every failure, fix, delete; the unsourced 104 is neither a +blocker nor a promise). + +**Stage 7 — prevalence, measured last**, with failures bucketed into: statically-decidable / +runtime-value-dependent / external-boundary / resource-budget / capability-not-grounded / +interpreter-defect. From 6a80656eb859df8b605c544cda6a4eb904873859 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 01:52:58 +0000 Subject: [PATCH 5/8] Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) --- docs/plans/compiler-guarantee-recovery-gap-analysis.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index be827dcea5e..56c685f8063 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -1,6 +1,9 @@ # Compiler guarantee recovery — gap analysis -**Status:** WORKING DRAFT, audit in progress. No code lands from this note. +**Status:** reconciled analysis — two audit passes complete (initial archaeology 2026-07-30; +independent review + receipt verification 2026-07-31, ledger in §10). No code lands from this +note. Open by design: §12 sequencing awaits operator sign-off; prevalence numbers are +deliberately unmeasured until Stage 7. **Question it answers:** what did this compiler intend to guarantee, and what does it guarantee today? ## 0. Provenance From dd7e585d758c587bed19c9ae717a541656969b5c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 02:00:12 +0000 Subject: [PATCH 6/8] Align the bind's dissolution trigger with the doc's own authority model (review 45299) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/doc_graph_roots.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index edb921e0e5a..78a528b4b21 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -267,7 +267,7 @@ data hand_authored_doc_binds: List = [ home: PlanDoc, slug: "compiler-guarantee-recovery-gap-analysis", work: DeclarationRef { module_path: "v1.compiler.infer", decl_name: "module_skips_direct_call_arg_check", field: WholeDeclaration }, - dissolution: HasTrigger { text: "the recovered guarantee statement and tier claims are re-homed into DESIGN.md as its specification half, AND every Tier 1/Tier 2 row in the analysis is either closed on its carrier or migrated to a registered gunbc.plan.Plan row. This bind names the escape hatch specifically because docs/thesis/correctness-dimensions.md states the dimension contract as 'enforced universally — all code is subject to all dimensions, no escape hatch, no wrapper functions', and module_skips_direct_call_arg_check is that clause's one named violation in tree: it exempts v2.* and v1.compiler.* from direct-call argument checking, so the compiler being bootstrapped is authored under weaker checks than ordinary source. Deleting it is the analysis's terminal Tier 1 acceptance and its removal ends this row" }, + dissolution: HasTrigger { text: "the recovered guarantee statement and tier claims are modeled as .dag claim rows (the guarantee authority of the analysis Sec 11/12, grounding the StandingIntent thread) and PROJECTED into DESIGN.md via gunbc.design_document — never hand-edited into the markdown, which is a projection, so a direct DESIGN.md edit does NOT satisfy this trigger (analysis Sec 7b; wording corrected from 're-homed into DESIGN.md' per review 45299, which caught the trigger contradicting the document it binds) — AND every Tier 1/Tier 2 row in the analysis is either closed on its carrier or migrated to a registered gunbc.plan.Plan row. This bind names the escape hatch specifically because docs/thesis/correctness-dimensions.md states the dimension contract as 'enforced universally — all code is subject to all dimensions, no escape hatch, no wrapper functions', and module_skips_direct_call_arg_check is that clause's one named violation in tree: it exempts v2.* and v1.compiler.* from direct-call argument checking, so the compiler being bootstrapped is authored under weaker checks than ordinary source. Deleting it is the analysis's terminal Tier 1 acceptance and its removal ends this row" }, }, HandAuthoredDocBind { home: PlanDoc, From a78e4bf6dc23a8f03a1637d68062d66e6504484d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 02:18:57 +0000 Subject: [PATCH 7/8] Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/doc_graph_roots.dag | 8 +- ...ompiler-guarantee-recovery-gap-analysis.md | 102 +++++++++++++++++- 2 files changed, 101 insertions(+), 9 deletions(-) diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index 78a528b4b21..37599f31d4b 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -267,13 +267,7 @@ data hand_authored_doc_binds: List = [ home: PlanDoc, slug: "compiler-guarantee-recovery-gap-analysis", work: DeclarationRef { module_path: "v1.compiler.infer", decl_name: "module_skips_direct_call_arg_check", field: WholeDeclaration }, - dissolution: HasTrigger { text: "the recovered guarantee statement and tier claims are modeled as .dag claim rows (the guarantee authority of the analysis Sec 11/12, grounding the StandingIntent thread) and PROJECTED into DESIGN.md via gunbc.design_document — never hand-edited into the markdown, which is a projection, so a direct DESIGN.md edit does NOT satisfy this trigger (analysis Sec 7b; wording corrected from 're-homed into DESIGN.md' per review 45299, which caught the trigger contradicting the document it binds) — AND every Tier 1/Tier 2 row in the analysis is either closed on its carrier or migrated to a registered gunbc.plan.Plan row. This bind names the escape hatch specifically because docs/thesis/correctness-dimensions.md states the dimension contract as 'enforced universally — all code is subject to all dimensions, no escape hatch, no wrapper functions', and module_skips_direct_call_arg_check is that clause's one named violation in tree: it exempts v2.* and v1.compiler.* from direct-call argument checking, so the compiler being bootstrapped is authored under weaker checks than ordinary source. Deleting it is the analysis's terminal Tier 1 acceptance and its removal ends this row" }, - }, - HandAuthoredDocBind { - home: PlanDoc, - slug: "compiler-guarantee-recovery-gap-analysis", - work: DeclarationRef { module_path: "v2.std.constraints", decl_name: "solve_constraints", field: WholeDeclaration }, - dissolution: HasTrigger { text: "v2 inference stops certifying source identity as semantic grounding. Today solve_constraints passes graph.root as source_facts, algebra AND the sole candidate, and v2.std.constraint_satisfaction_predicate.constraint_satisfaction_preservation_holds requires algebra == source_facts && candidate == source_facts — so the proof reduces to well_formed(root) checked three times and is then relabelled CanonicalGrounding. The row dissolves when a candidate is derived rather than supplied, or the generic arm returns a typed compile refusal instead of an accepted self-grounded InferredTree" }, + dissolution: HasTrigger { text: "ONE row, TWO anchored carriers, BOTH conditions gate dissolution (merged from a two-row form per review 45305: home+slug is this list's symbolic identity, so two rows gave one doc two independently removable authority rows). Condition zero, the authority: the recovered guarantee statement and tier claims are modeled as .dag claim rows (the guarantee authority of the analysis Sec 11/12, grounding the StandingIntent thread) and PROJECTED into DESIGN.md via gunbc.design_document — never hand-edited into the markdown, which is a projection, so a direct DESIGN.md edit does NOT satisfy this trigger (analysis Sec 7b; wording corrected from 're-homed into DESIGN.md' per review 45299) — and every Tier 1/Tier 2 row in the analysis is either closed on its carrier or migrated to a registered gunbc.plan.Plan row. Carrier (1), the work field's ref: v1.compiler.infer module_skips_direct_call_arg_check — the one named in-tree violation of the dimension contract's 'no escape hatch' clause (docs/thesis/correctness-dimensions.md): it exempts v2.* and v1.compiler.* from direct-call argument checking, so the compiler being bootstrapped is authored under weaker checks than ordinary source; its deletion is the analysis's terminal Tier 1 acceptance. Carrier (2): v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, and v2.std.constraint_satisfaction_predicate.constraint_satisfaction_preservation_holds requires algebra == source_facts && candidate == source_facts, so the grounding proof reduces to well_formed(root) relabelled CanonicalGrounding; that half dissolves when a candidate is derived rather than supplied, or the generic arm returns a typed compile refusal instead of an accepted self-grounded InferredTree. The row deletes only when BOTH carriers are closed" }, }, ] diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 56c685f8063..8757d963a7c 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -37,6 +37,91 @@ And the framing immediately above it: Emission is specified as the downstream, mechanical half of a two-stage contract. The upstream half — validation — is the one that was not built. +## 1b. The safety ladder (operator framing, 2026-07-31 — the organizing frame for every class in this note) + +The guarantee statement's operational form is a ladder that every discovered error class +climbs. It is DESIGN §1's safety axis made kinetic: safety is time-to-recover from a silent +wrong answer, paid later at interest — so each rung moves detection of the *same* defect +earlier and cheaper, and the top rung means the defect is never paid for by anyone. + +| Rung | Name | Who pays, and when | +|---|---|---| +| **R3** | Structurally impossible | No one, ever — the bad state has no writable form (construction / derivation / sealed carrier) | +| **R2** | Structural guarantee | The author, at compile time — typed, located refusal | +| **R1** | Testable / validatable / preventable | CI, before ship — witness, lens, RED control | +| **R0** | Mitigatable | The operator, at runtime — typed refusal, budget, rollback | +| — | **below the floor: silent** | The end user, at interest, unknowingly — **forbidden outright (§5)** | + +Three rules make it a discipline rather than a diagram: + +1. **The floor is absolute.** No class may sit below R0. A silently-wrong behavior — the + misspelled label that binds positionally and computes the wrong answer with no signal — + is not a low rung; it is outside the ladder, and §5 already outlaws it. The first move + for any discovered class is *to the floor*: loud, typed, counted. Climbing starts after. +2. **Every class climbs to its ceiling, and states its ceiling.** Ceilings come in exactly + three kinds: **mathematical** (undecidability, the external-reality boundary, + root-authority self-governance — permanent and honest), **capability** (R3 for + carrier-borne invariants requires unforgeable construction, i.e. reference-level + visibility the language does not yet have — no `private`/`sealed`/`opaque` in the keyword + set; one unlock raises every such class at once), and **price** (deferral compounds in + sites — `Value::Null` at 131 — so lateness raises the bill but never closes the door). + "Climb the ladder" always means *to the stated ceiling*, not unconditionally to R3. +3. **Reported rung == measured rung.** A rung is established by an executing probe, never + asserted. Rung *inflation* — v2's `CanonicalGrounding` reporting R3 while occupying R0; + the historical ledger's "Yes (blocking)" — is worse than sitting low, because an inflated + class never ranks for climbing. A lens reds inflation and reds stalls (below ceiling + with no named next-rung trigger). + +**How this compiler makes programming safer than a traditional one — the two ends of the +ladder.** A traditional compiler holds a fixed, non-negotiable set of classes at R2 (types, +syntax, constructor arity), leaves everything else at R1 (hand-written tests) or below the +floor (silent), and barely uses R3 at all. The bet here is at both ends: the **floor is +enforced** (§5 — nothing silent survives), and the **top is open** — the R2 set is +user-extensible by rows rather than compiler forks (§7's language-design-opens-up), and R3 +is a *working* rung (derive-don't-store, closed algebras, sealed construction once +visibility lands). The recovered `error-examples.md` cases — `reverse |> reverse`, +non-idempotent retry, O(n²) — are ordinary classes *lifted to R2* that no mainstream +compiler holds there. The scandal this note documents is the inversion: the ambition +examples sit above mainstream while method-existence and return-conformance sit below it. + +### The conversation's own specimens, placed on the ladder + +| Class | Floor status | Today | Ceiling | The climb | +|---|---|---|---|---| +| Misspelled label binds positionally (§4) | **BELOW FLOOR — silent wrong binding** | — | R2 | floor first (any diagnostic), then the exact call-shape judgment | +| Unknown method (`filter_map`, #7479) | at floor | R0 — typed `Unimplemented`, found as a 500 on the lab | **R2** — a nonexistent name can always be *typed*; refusal is the top rung for reference classes | zero-resolution wall now; ambiguity wall after the identity join | +| Return / `data` / generic inhabitance (#7481 probes) | at floor | R0 — first consumer breaks, typed | R2 | return-position checking (wall-after-grounding) | +| Empty list into requires-one (the operator's case, §4b) | at floor | R0 — runtime surprise or degenerate arm | **R3** — the bad *seam* becomes unwritable | seal `Refined` (capability ceiling) + propagate through `InterfaceSummary`; expecting-red probes land first | +| Cross-representation `==` | **was below floor** (silent `false`) | **R3** — numeric tower grounded by construction (#5428), guard dead-in-corpus | R3 | **done — the exemplar full climb, floor to top** | +| v2 loop termination | — | **R2** (undeclared measure refused) with R3 character (unbounded iteration has no substrate spelling; recursion is sugar over `Loop`) | R3 | done in v2; the v1 seed's classes climb by deletion, not hardening | +| Idempotency-unsafe retry | at floor | R1-capable — algebra declared, consumers exist, not at binding sites | R2 | the dimension migrates onto `TypeBinding` (§8c) | +| Non-exhaustive match via blocked lookup | below-floor risk (`diagnostics: []`) | mixed R0/R1 | R2 | `ExhaustivenessUnknown` refuses instead of passing as success | +| Doc orphan (this PR's own incident) | was below floor — silent rot, twice historically | **R1** — `ReadsLiveTree` witness; it caught this very PR | R2-ish (registration-derived roots) | live proof that climbing pays: the wall that failed open twice, repaired, did its job | + +### Non-goals — ceilings that are low BY DESIGN, stated so they are never mistaken for gaps + +- **External reality** (host state, network, tool presence): outside the program graph *by + the guarantee statement*; the ceiling is a typed refusal at the boundary — R0-at-boundary + is correct there, not a deficit. +- **Arbitrary refinement predicates** (`admits: fn(B) -> Bool`): undecidable; ceiling is the + runtime constructor boundary. The decidable cardinality *fragment* climbs instead — that + split is the whole design of `cardinality-refinement.md`. +- **Resource / budget exhaustion** (`EvalBudgetExceeded`, ARG_MAX, witness-wall budgets): + R0 by design — the bound *is* the product. +- **Optimality**: ratchet forever (Rice); §5 already names "never" as the trap. +- **Root-authority self-governance**: the substrate cannot wall edits to its own axioms; + operator review is the permanent mechanism, not a temporary one. +- **Byte-identical self-emission**: retired non-goal — behavioral equivalence replaced it + (DESIGN §7) precisely to avoid cementing the seed's accidents. + +**Landing target:** this section is drafted here for operator sign-off and lands as +`gunbc.design_document` rows projected into DESIGN.md beside §5's construction/validation +doctrine (§7b discipline — never a hand edit of the markdown). The §3 status lattice below +refines the rungs (e.g. `RepresentableButForgeable` = R1 wanting R3 behind the capability +ceiling; `LiteralOnlyWall` = R2 on a fragment); the claim carrier of §11/§12 gives every +class `current_rung` (probe-measured), `ceiling` (with its justification kind), and +`next_rung_trigger`. + ## 2. The failure history (revised after independent review, 2026-07-31) An earlier draft of this section told a two-part story: the spec was lost, then the claims @@ -293,7 +378,13 @@ The user-supplied case is the archetype and belongs in the corpus as example 0: ```dag // callee requires at least one; caller can supply zero. -// Today: unexpressible — no NonEmpty carrier, Cardinality connective uninhabited. +// Expected on landing: located refusal at the seam — a 0..n producer bound to a +// 1..n consumer position (interface-summary-declared-use-arity.md Sec 3.1). +// Today it compiles. The RED exercises unforgeable construction + seam +// propagation — NOT absence of representation: Refined> exists and is +// forgeable (Sec 4/4b). (Corrected per review 45305 — an earlier draft said +// "unexpressible" here, which would have aimed the fix at inventing a carrier +// instead of sealing and propagating the one that exists.) ``` ## 8c. The dimension architecture — recovered contract, and it is still standing @@ -425,7 +516,14 @@ Model the guarantee population (the review's G0–G9 families are a good candida binding · formation · inhabitance · invocation · domain/totality · control soundness · semantic dimensions · realization · fidelity · external boundary) as rows with: identity, proof mode, authoritative carrier, negative RED, positive control, per-compiler enforcement -status, and **a named consumer in `Accepted`**. Two §3 grounding rules so this doesn't fork +status, **a named consumer in `Accepted`**, and the three ladder fields of §1b — +`current_rung` (probe-measured, never asserted), `ceiling` (with its +mathematical/capability/price justification), `next_rung_trigger` — plus the two lens +obligations: red on rung inflation (reported > measured; v2's generic arm reds on day one) +and red on stalls (below ceiling with no named trigger). The ladder also consolidates five +existing fragment-vocabularies onto one axis (§3's lattice, `wall now`/`after`/`ratchet`, +`LifecycleByConstruction|Convention`, `DecodeFidelity`, the thesis tiers) — a §2/§3 merge, +not a new taxonomy. Two §3 grounding rules so this doesn't fork existing machinery: the families ground on the recovered *dimension* architecture (§8c) and the DESIGN open thread `StandingIntent` — this IS that thread's missing claims list, not a second taxonomy beside it; and per §7b the authority is `.dag` rows projected into DESIGN.md, From 5130f7a443a7fc1a8851e3c7cf2db9621c593741 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 02:36:21 +0000 Subject: [PATCH 8/8] WIP: compiler correctness --- DESIGN.md | 10 ++++ dag/gunbc/design_document.dag | 11 ++++ ...ompiler-guarantee-recovery-gap-analysis.md | 59 +++++++++++++++++-- 3 files changed, 75 insertions(+), 5 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index 5b86420f761..9a051ba4c34 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -25,6 +25,8 @@ Three things follow, in order: - **From A2 and A3 — grounding is intersubjective.** Because time is the *only* assumed-shared value, a fact is grounded only by pointing at a shared, time-stable framework (§4), never an internal taxonomy. - **At the limit — reduce intersubjectivity to physics.** The deepest such framework — the efficient, time-bound description of interactions that satisfies a goal — is **physics** (A1–A2 turned on grounding itself). So the aim, at its limit, is to *reduce intersubjectivity to physics*: replace convention with necessity until nothing arbitrary survives. This is the deep reason §3 models the universal frameworks and real upstream rather than re-coining them — a nickname is convention standing where physics was available. +The safety axis carries its own measure, used throughout: **safety is measured by how far each error class has climbed from runtime harm toward structural impossibility** — the guarantee ladder; §4b defines the ladder, its ceilings, and its evidence rules. + ## 2. Minimize redundancy (the master move for cost and complexity) Redundant work — **duplicated, unnecessary, or irrelevant** — loses on all three of §1's quantities at once: it costs more to run, it widens the surface where harm hides, and it adds complexity to maintain. So a perfectly DRY process is, *by the meaning of redundant*, the minimal/efficient one; minimizing redundancy is therefore the master move for §1's cost and complexity axes (the safety axis is §5). Through §1's time lens this is *why* DRY matters at all: redundant work **defers** cost into the future — it shoves a problem onto a later fixer, or builds a process destined to be thrown out — so DRY is the refusal to spend someone's future time to buy the author's present convenience; it values time **holistically**, across every party and all of it, not just the here-and-now. Redundancy is removed along exactly two directions — not separate "DRY rules," but one move seen two ways: @@ -53,6 +55,14 @@ Because the substrate is closed and grounded, the wins of §2 fall out for free: - *e.g.* `dag/std/algebra.dag` derives `Int.add` from `Int` inhabiting a ring (ops aren't listed per type); idempotency dissolved from an `idempotent: Bool` flag into the `EffectShape` variant; termination is *checked, not discovered* — `DescentEvidence = Strict | NonIncreasing | DescentUnknown` inhabits a `BoundedLattice` with bottom = fail-closed. - *e.g.* **one grammar, read in both directions** (§2 horizontal, not an adapter pair): ingest selects a production *forward* to fold surface syntax into a core `Node`; emit (`serialize_target ∘ translate`) selects from the *same* `target_model_edge_translation_rules` rows *backward* — the structural inverse, not a second emitter — so a new target language is rows authored in `extdeps/languages/`, never an edit to the fold (N rows, not N×M parser/emitter pairs). Coercion is that same move turned sideways: whether one model inhabits another is a homomorphism check (`coercion_fold` via `find_witness`), the same epistemic chain the emitter walks. One procedure asked in three directions, not three procedures. +## 4b. Safety: the guarantee ladder (every error class climbs from runtime harm toward unwritability) + +**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). 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. + +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 language capability names the capability as its trigger (the live one: **unforgeable construction** — the top rung for every carrier-borne invariant — waits on reference-level constructor visibility, there being no private/sealed/opaque in the language today, so every proof-carrier is presently forgeable); 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** — 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; a type name, diagnostic variant, inert lens, or plan establishes nothing, and **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** — a climb deletes the redundant lower-rung 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. 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. + +**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-class current rung, measured evidence, ceiling with reason, next trigger, consumer-in-`Accepted`), grounding the enforcement-intent thread below rather than minting a second registry beside it. + ## 5. Fail-closed (§1's safety axis — harm reduction) Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded "forever" ≠ an "unknown" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches "never"). The word **"never" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — "done" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.) diff --git a/dag/gunbc/design_document.dag b/dag/gunbc/design_document.dag index 8ec65c8266c..ab81e6333c4 100644 --- a/dag/gunbc/design_document.dag +++ b/dag/gunbc/design_document.dag @@ -42,6 +42,7 @@ fn section_1_blocks() -> List { li(text: "**From A2 and A3 — grounding is intersubjective.** Because time is the *only* assumed-shared value, a fact is grounded only by pointing at a shared, time-stable framework (§4), never an internal taxonomy."), li(text: "**At the limit — reduce intersubjectivity to physics.** The deepest such framework — the efficient, time-bound description of interactions that satisfies a goal — is **physics** (A1–A2 turned on grounding itself). So the aim, at its limit, is to *reduce intersubjectivity to physics*: replace convention with necessity until nothing arbitrary survives. This is the deep reason §3 models the universal frameworks and real upstream rather than re-coining them — a nickname is convention standing where physics was available."), ]), + p(text: "The safety axis carries its own measure, used throughout: **safety is measured by how far each error class has climbed from runtime harm toward structural impossibility** — the guarantee ladder; §4b defines the ladder, its ceilings, and its evidence rules."), ] } @@ -91,6 +92,15 @@ fn section_4_blocks() -> List { ] } +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). 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 language capability names the capability as its trigger (the live one: **unforgeable construction** — the top rung for every carrier-borne invariant — waits on reference-level constructor visibility, there being no private/sealed/opaque in the language today, so every proof-carrier is presently forgeable); 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** — 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; a type name, diagnostic variant, inert lens, or plan establishes nothing, and **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** — a climb deletes the redundant lower-rung 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. 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-class current rung, measured evidence, ceiling with reason, next trigger, consumer-in-`Accepted`), grounding the enforcement-intent thread below rather than minting a second registry beside it."), + ] +} + fn section_5_blocks() -> List { [ h2(text: "5. Fail-closed (§1's safety axis — harm reduction)"), @@ -188,6 +198,7 @@ fn design_blocks() -> List { section_2_blocks(), section_3_blocks(), section_4_blocks(), + section_4b_blocks(), section_5_blocks(), section_6_blocks(), section_7_blocks(), diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 8757d963a7c..4a8382c1b08 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -89,10 +89,11 @@ examples sit above mainstream while method-existence and return-conformance sit | Class | Floor status | Today | Ceiling | The climb | |---|---|---|---|---| | Misspelled label binds positionally (§4) | **BELOW FLOOR — silent wrong binding** | — | R2 | floor first (any diagnostic), then the exact call-shape judgment | -| Unknown method (`filter_map`, #7479) | at floor | R0 — typed `Unimplemented`, found as a 500 on the lab | **R2** — a nonexistent name can always be *typed*; refusal is the top rung for reference classes | zero-resolution wall now; ambiguity wall after the identity join | +| Unknown method (`filter_map`, #7479) | at floor | R0 — typed `Unimplemented`, found as a 500 on the lab | **R3 in the accepted model** — a resolved call carries a unique declaration identity, so an unresolved name has no accepted form; the author experiences it as R2-style refusal at the source boundary | zero-resolution wall now; ambiguity wall after the identity join; `FunctionRef`-carrying IR | | Return / `data` / generic inhabitance (#7481 probes) | at floor | R0 — first consumer breaks, typed | R2 | return-position checking (wall-after-grounding) | | Empty list into requires-one (the operator's case, §4b) | at floor | R0 — runtime surprise or degenerate arm | **R3** — the bad *seam* becomes unwritable | seal `Refined` (capability ceiling) + propagate through `InterfaceSummary`; expecting-red probes land first | -| Cross-representation `==` | **was below floor** (silent `false`) | **R3** — numeric tower grounded by construction (#5428), guard dead-in-corpus | R3 | **done — the exemplar full climb, floor to top** | +| **Numeric-tower** cross-representation `==` | **was below floor** (silent `false`) | **R3** — grounded by construction (#5428), guard dead-in-corpus for numerics | R3 | **done — the exemplar full climb, floor to top** | +| Cross-representation `==`, full class (`Bool` straddle; `Optional`/`Witness` over `Value::Null`) | at floor | R0 — typed `CrossRepresentationEquality` backstop; the `Value::Null` overload is live at ~131 sites | R3 — each primitive grounded in its realization | the `Value::Null` split (its own runway, `value-null-split` plan). *Row split from a single "R3 done" claim per review 45310 — the table's own inflation rule, caught by review* | | v2 loop termination | — | **R2** (undeclared measure refused) with R3 character (unbounded iteration has no substrate spelling; recursion is sugar over `Loop`) | R3 | done in v2; the v1 seed's classes climb by deletion, not hardening | | Idempotency-unsafe retry | at floor | R1-capable — algebra declared, consumers exist, not at binding sites | R2 | the dimension migrates onto `TypeBinding` (§8c) | | Non-exhaustive match via blocked lookup | below-floor risk (`diagnostics: []`) | mixed R0/R1 | R2 | `ExhaustivenessUnknown` refuses instead of passing as success | @@ -122,6 +123,54 @@ ceiling; `LiteralOnlyWall` = R2 on a fragment); the claim carrier of §11/§12 g class `current_rung` (probe-measured), `ceiling` (with its justification kind), and `next_rung_trigger`. +## 1c. Current rung census (seed population for the Stage-1 carrier — status `Unknown` where this audit has not measured) + +The operator's reorganization directive (2026-07-31): the ladder is the mechanism, the +historical tiers are *example domains*. These rows are the draft population for the Stage-1 +`ErrorClassGuarantee` carrier; every `Unknown` is honest unmeasured state, not a gap claim. +Floor-domain failures are **below-baseline safety regressions** — never compensated by +higher-order capability. + +**Domain: ordinary compiler safety floor** + +| Class | Current rung | Ceiling | Why not higher | Evidence | Next trigger | +|---|---|---|---|---|---| +| Unknown fn/method | R0 (typed at dispatch) | R3 (resolved call carries declaration identity) | fabricating fallback live | #7479 | zero-resolution wall; `FunctionRef` IR | +| Call shape (labels/count) | **partly below floor** (misspelled label binds positionally, silent) | R3 (exact bijection in normalized IR) | formal-driven walk; `ArityMismatch` is constructor-grain | `direct_call_arg_mismatch_diags` | floor diagnostic first, then exact-shape judgment | +| Return conformance | R0 | R3 (body edge inhabits Arrow codomain) | no general judgment | #7481 | return-position checking | +| `data` annotation | R0 | R3 | same lane | #7481 | same lane | +| Generic instantiation | R0 | R2 | substitution unproven | #7481 | inhabitance at instantiation | +| Field through generics | R0 | R2 (pending-constraint discharge) | `field_of_type_var` minted | §4 | constraint carried + unique discharge | +| Closed-match exhaustiveness | mixed R1/R0, one silent arm | R3 (full arm population at elimination) | `PatternLookupBlocked => []` | §4 | `ExhaustivenessUnknown` refuses | +| Record completeness | **Unknown — unmeasured** | R3 | not audited this pass | — | audit probe | +| Producer/consumer cardinality | R0 | R3 (seam unwritable) | forgeable carrier; no signature propagation (capability ceiling) | §4b | Stage-3 vertical slice | + +**Domain: structural safety extensions (the differentiator)** + +| Class | Current rung | Ceiling | Why not higher | Evidence | Next trigger | +|---|---|---|---|---|---| +| Termination | v2 loops R2 (R3 character: unbounded iteration has no substrate spelling); v1 recursion **Unknown** (thesis-era "421 non-blocking") | R3 | v1 coverage unmeasured | `v2.std.cardinality` | universal recursive-call lowering | +| Retry × idempotency | R1/R2 partial (algebra declared; `Retry` emit refuses shapes, #7303/#7318) | R2 (`Retry` admits only retry-safe evidence or compensation) | not at binding sites | `std.effects` | dimension onto `TypeBinding` (§8c) | +| Complexity budget | R2 for enrolled classes (accumulator-copy in the compile door; bare-minimum-cost rule) | R2 | coverage partial | door roster | contract propagation | +| Exponential branching | **Unknown** | R2 (against declared budget — exponential can be intentional) | unmeasured | error-examples #7 | measure, then gate | +| Algebraic cancellation | **Unknown, likely absent** | R2 (derive where algebra declared) | unmeasured | error-examples #6 | algebraic-rewrite lane | +| Redundant cross-service computation | R1 (duplicate-work design; flagship proven) | R2 | `ComputationIdentity` staged | DESIGN open thread | Half A/B landing | +| Partial-failure convergence | R2/R3 partial in-model (`MemberTeardownRefused` has no effect arm — teardown-of-unowned unwritable) | R3 in-model; external residue stays boundary | grain expansion pending | membership-reconcile | remaining grains | +| Numeric-tower cross-representation `==` | **R3 — done** (exemplar climb) | R3 | — | #5428 | backstop guard dissolves with the Null split | +| Cross-representation `==`, full class (`Bool`; `Optional`/`Witness` over `Value::Null`) | R0 (typed backstop; Null overload live, ~131 sites) | R3 | Null split is its own runway | value-null-split plan | `Value::Null` split *(split from one inflated "R3 done" row per review 45310)* | +| L4: emitted vs modeled behavior | R1 (behavioral equivalence by execution) | R2 for supported forms | derivation not proof | witness-realization plan | realization proof | +| L5: cross-target equivalence | **Unknown** | R1→R2 | unmeasured | — | witness matrix | + +**Domain: external boundary (low ceilings BY DESIGN — correct, not gaps)** + +| Class | Rung | Note | +|---|---|---| +| Host/tool availability | R0 typed at the boundary | no higher rung claimed | +| Resource/budget exhaustion | R0 by design | the bound *is* the product | +| Optimality | outside the ladder | Rice; permanent ratchet | +| Unstated business intent | outside | never fabricated | +| Unmodeled upstream behavior | outside | observe → typed evidence → admit or refuse | + ## 2. The failure history (revised after independent review, 2026-07-31) An earlier draft of this section told a two-part story: the spec was lost, then the claims @@ -186,7 +235,7 @@ guarantee authority lands (§11), the same way `DescentEvidence` and `DecodeFide their own verdicts. The DESIGN.md §5 wall-classification (*wall now* / *wall after grounding* / *ratchet forever*) stays as the orthogonal decidability axis. -## 4. Tier 1 — structural correctness ("impossible to write the bug") +## 4. Domain: the ordinary compiler safety floor (historical Tier 1 — "impossible to write the bug") | Claim (THESIS.md) | Today | Receipt | §5 class | |---|---|---|---| @@ -228,7 +277,7 @@ connecting three artifacts that already exist — the operator direction, the sc plan, and the green fold-propagation seed — and closing the two named gaps (unforgeable construction; signature-level propagation through `InterfaceSummary`). -## 5. Tier 2 — runtime safety ("proven safe or total") +## 5. Domain: runtime-safety floor obligations (historical Tier 2 — "proven safe or total") The claim is one sentence: **"No partial functions in the runtime."** @@ -256,7 +305,7 @@ vocabulary must be the *substrate's*, not the v1 Rust seed's. `InterpError` is o realization's taxonomy; using it as the denominator is the §3 inversion. It is admitted here as **evidence**, not as spec. -## 6. Tier 3 — verification from structure +## 6. Domain: realization and fidelity (historical Tier 3 — verification from structure) L4 (emitted matches `.dag` eval) · L5 (same behavior across targets) · L6 (every form compiles to every target) · L7 (operations obey declared algebraic laws).