Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
bfd48a4
Census the first() interpreter/emitted divergence, and repair the hal…
Aug 31, 2026
eccd062
Census: report a disposition per site, not a shape tally
Aug 31, 2026
95079cb
Census: step 1 re-scoped — the signature carrier exists; the gap is i…
Aug 31, 2026
32606e4
Census: enumerate the 442 from the artifact, and record that this cla…
Aug 31, 2026
79ac1aa
Merge main into session/still-swift-363
Aug 31, 2026
59f24ae
Record the measured blast radius against a trunk control, and name th…
Aug 31, 2026
3b4d565
Merge main into session/still-swift-363
Aug 31, 2026
f5e05e4
Derive phase equality from one exhaustive ordinal instead of a 7x7 wi…
Aug 31, 2026
abee235
Delete floor_probe.sh: experimental residue that hard-codes the infer…
Aug 31, 2026
7d7524d
Merge remote-tracking branch 'origin/main' into session/still-swift-363
Aug 31, 2026
dd61cc0
Census: the drift gate is a second measured victim, and the compositi…
Aug 31, 2026
5f460a2
Correct the build-lane cause: it is the coercion arm plus the deliber…
Aug 31, 2026
f052c05
Merge main into session/still-swift-363
Sep 1, 2026
2201637
Merge main into session/still-swift-363
Sep 1, 2026
adad2b0
Merge remote-tracking branch 'origin/main' into session/still-swift-363
Sep 1, 2026
91b4f5e
The coercion fired on a free type variable: silently unwrapping Prese…
Sep 1, 2026
1b0f02a
Locate builtin refusals at the call node: `parse_int expects a string…
Sep 1, 2026
62f11ae
Census superseded: its population was a spelling, and the larger half…
Sep 1, 2026
55cf946
Refusal before migration: `Optional` against a bare value under `==` …
Sep 1, 2026
660b617
Merge admission: eliminate the ten `first()` comparisons, and cover t…
Sep 1, 2026
b152146
Cover the five comparisons the first cut left blind: the subject pars…
Sep 1, 2026
cf93085
Census: 23 is a lower bound, and the completion criterion is that the…
Sep 1, 2026
5a0ca7f
Census: state the rule that covers both times this document's numbers…
Sep 1, 2026
44795c1
wip carrier-grain
Sep 1, 2026
6c22030
Merge branch 'session/still-swift-363' into scratch/cell34
Sep 1, 2026
c2be673
Delete two empty files a `git add -A` swept in
Sep 1, 2026
831cc51
Merge branch 'session/still-swift-363' into scratch/cell34
Sep 1, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions dag/gunbc/merge_admission_produce.dag
Original file line number Diff line number Diff line change
Expand Up @@ -107,13 +107,13 @@ fn parse_receipt_wire_v2(text: String) -> MergeAdmissionReceiptV2? {
let lines = receipt_wire_lines(text: text)
if !((length(lines) == 6) || (length(lines) == 7)) {
none
} else if !(lines.first() == merge_admission_receipt_schema_v2) {
} else if match lines.first() { Present { value: schema_line } => !(schema_line == merge_admission_receipt_schema_v2) Absent => true } {
none
} else if lines.skip(n: 2).first() == "" {
} else if match lines.skip(n: 2).first() { Present { value: field } => field == "" Absent => true } {
none
} else if lines.skip(n: 4).first() == "" {
} else if match lines.skip(n: 4).first() { Present { value: field } => field == "" Absent => true } {
none
} else if lines.skip(n: 5).first() == "" {
} else if match lines.skip(n: 5).first() { Present { value: field } => field == "" Absent => true } {
none
} else {
match walk_attempt_id(raw: lines.skip(n: 1).first()) {
Expand Down
12 changes: 6 additions & 6 deletions dag/gunbc/merge_admission_subject.dag
Original file line number Diff line number Diff line change
Expand Up @@ -133,9 +133,9 @@ fn render_git_object_id_wire(oid: GitObjectId) -> String {
fn parse_git_object_id_wire(raw: String) -> GitObjectId? {
if !(length(split(s: raw, delimiter: ":")) == 2) {
none
} else if split(s: raw, delimiter: ":").first() == "sha1" {
} else if match split(s: raw, delimiter: ":").first() { Present { value: algorithm } => algorithm == "sha1" Absent => false } {
git_sha1_object_id(hex: split(s: raw, delimiter: ":").skip(n: 1).first())
} else if split(s: raw, delimiter: ":").first() == "sha256" {
} else if match split(s: raw, delimiter: ":").first() { Present { value: algorithm } => algorithm == "sha256" Absent => false } {
git_sha256_object_id(hex: split(s: raw, delimiter: ":").skip(n: 1).first())
} else {
none
Expand All @@ -160,13 +160,13 @@ fn parse_tested_subject_wire(text: String) -> TestedSubject? {
let lines = receipt_wire_lines(text: text)
if !(length(lines) == 5) {
none
} else if !(lines.first() == merge_admission_tested_subject_schema) {
} else if match lines.first() { Present { value: schema_line } => !(schema_line == merge_admission_tested_subject_schema) Absent => true } {
none
} else if lines.skip(n: 2).first() == "" {
} else if match lines.skip(n: 2).first() { Present { value: field } => field == "" Absent => true } {
none
} else if lines.skip(n: 3).first() == "" {
} else if match lines.skip(n: 3).first() { Present { value: field } => field == "" Absent => true } {
none
} else if lines.skip(n: 4).first() == "" {
} else if match lines.skip(n: 4).first() { Present { value: field } => field == "" Absent => true } {
none
} else {
match walk_attempt_id(raw: lines.skip(n: 1).first()) {
Expand Down
142 changes: 133 additions & 9 deletions dag/gunbc/plans/value_null_split.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,119 @@ module gunbc.plans.value_null_split
import std.dissolution { unbound_dissolution }
import gunbc.plan { Plan, PlanRetirement, PlanRetiresWhen, PlanIsAuthorityOnly }
import std.markdown { MarkdownBlock, TableBlock, AlignNone }
import gunbc.plans.md_helpers { h2, p, li, ol, cell, row, task, tasks, Unchecked }
import std.types { Bool, Int, List, NonEmptyStr, String }
import gunbc.plans.md_helpers { h2, p, li, ol, ul, cell, row }

// PHASE STANDING IS NOT A CHECKBOX, and this module used to prove why. Every phase below was
// `task(state: Unchecked)` while Phase A had DEMONSTRABLY LANDED -- its witness module exists, runs
// in the required floor, and one of its claims is enrolled and firing. The document stated the
// right invariant in its own review bar ("every phase ships with a discriminating witness that goes
// RED when the carrier regresses") and then tracked itself by hand anyway, so it went stale by a
// full phase with nothing to notice. A hand-maintained status is the execution-provenance failure
// applied to a plan: it reads identically whether the phase landed or nobody updated the line.
//
// So the status is DERIVED from the witness roster rather than typed. What that buys and what it
// does not, stated so neither is overread: the roster below is HAND-AUTHORED, so a phase whose
// witness is never declared here reads Unwitnessed exactly like a phase with no witness at all.
// This is therefore a CITATION, one step above a checkbox because there is a single authority for
// the answer instead of one per rendering, and one step below evidence.
//
// NEXT RUNG, naming the capability rather than an artifact: reading claim OUTCOMES at claim-identity
// grain from inside `.dag`. The required floor already computes exactly that join -- its
// `required-floor-disposition` output carries one row per claim identity with the outcome that
// claim reached -- but it is an out-of-band run artifact, not something a `.dag` fold can consult,
// so no declaration here can be green-by-execution about a phase. When that capability lands,
// `value_null_phase_standing` reads the outcome instead of the roster and the citation becomes
// evidence.
type ValueNullPhase
= PhaseCarrierWitnesses
| PhaseStopProducingNull
| PhaseDeleteNullBridges
| PhaseNoneLiteralMigration
| PhaseCrossRepresentationEquality
| PhaseArgumentCoercion
| PhasePrimitiveSignatureDenominator

type ValueNullPhaseWitness {
phase: ValueNullPhase
claim: NonEmptyStr
}

type ValueNullPhaseStanding
= PhaseWitnessEnrolled { claim: NonEmptyStr }
| PhaseUnwitnessed

// Equality is DERIVED from one exhaustive projection rather than written as a 7x7 comparison,
// following `std.fermi` `fermi_ordinal`. The first draft of this function matched `a` and then
// matched `b` inside each arm with a `_ => false` wildcard, which the non-fold residue detector
// correctly flagged: a wildcard over a CLOSED coproduct is un-migrated modeling, because adding an
// eighth phase would silently take the `_` arm at seven sites instead of failing to compile. Here
// a new arm makes `value_null_phase_ordinal` non-exhaustive and the compiler refuses.
fn value_null_phase_ordinal(phase: ValueNullPhase) -> Int {
match phase {
PhaseCarrierWitnesses => 0
PhaseStopProducingNull => 1
PhaseDeleteNullBridges => 2
PhaseNoneLiteralMigration => 3
PhaseCrossRepresentationEquality => 4
PhaseArgumentCoercion => 5
PhasePrimitiveSignatureDenominator => 6
}
}

fn value_null_phase_eq(a: ValueNullPhase, b: ValueNullPhase) -> Bool {
value_null_phase_ordinal(phase: a) == value_null_phase_ordinal(phase: b)
}

// One row per phase that has a discriminating witness enrolled today. Phase A's rows are the
// carrier-pinning claims in `v2.test.manual.value_null_split_witness`; Phase B's is the
// construction claim added while Phase B was built (session still-swift-363, PR gunbc#9785, held).
// A phase absent from this list has no enrolled discriminator, which is the honest reading of
// "not started" and is NOT the same statement as "not landed".
data value_null_phase_witnesses: List<ValueNullPhaseWitness> = [
ValueNullPhaseWitness {
phase: PhaseCarrierWitnesses,
claim: "v2.test.manual.value_null_split_witness.raw_get_miss_differs_from_optional_absent" as NonEmptyStr,
},
ValueNullPhaseWitness {
phase: PhaseCarrierWitnesses,
claim: "v2.test.manual.value_null_split_witness.map_get_miss_is_absent_not_present" as NonEmptyStr,
},
ValueNullPhaseWitness {
phase: PhaseStopProducingNull,
claim: "test.claim.first_optional_construction_witness.first_of_a_list_whose_head_is_an_absent_optional_is_present_of_absent" as NonEmptyStr,
},
]

fn value_null_phase_standing(phase: ValueNullPhase) -> ValueNullPhaseStanding {
fold(
value_null_phase_witnesses,
init: PhaseUnwitnessed,
f: fn(acc, w) {
match acc {
PhaseWitnessEnrolled { claim: _ } => acc
PhaseUnwitnessed =>
if value_null_phase_eq(a: w.phase, b: phase) {
PhaseWitnessEnrolled { claim: w.claim }
} else {
acc
}
}
}
)
}

fn value_null_phase_standing_label(phase: ValueNullPhase) -> String {
match value_null_phase_standing(phase: phase) {
PhaseWitnessEnrolled { claim: c } => concat("discriminator enrolled: `", concat(c as String, "`"))
PhaseUnwitnessed => "no discriminator enrolled"
}
}

fn value_null_split_body() -> List<MarkdownBlock> {
[
p(text: "**Status:** lane opened (keen-ferret-250) · **Parent:** model↔realization fork §3.2 · **DESIGN.md open thread** · Linked from [model-realization-fork.md](model-realization-fork.md) and [fail-closed-lockdown.md](fail-closed-lockdown.md) §4 tier-1."),
p(text: "**Verified against the live tree 2026-07-26.** Census counts are receipts; re-check before acting."),
p(text: "**Ownership: none.** This plan was opened by a lane whose session no longer exists -- a `--to` addressed to it is refused as `recipient session not found`, and the name appears in no work item. A lane name written inside a document is a CITATION and rots exactly like a `file:line` or a merge-event trigger; absence from the live session graph is decidable, presence in this paragraph is not. Read the plan as an unowned authority to work AGAINST, never as a lane to defer to. **Parent:** model↔realization fork §3.2 · **DESIGN.md open thread** · Linked from [model-realization-fork.md](model-realization-fork.md) and [fail-closed-lockdown.md](fail-closed-lockdown.md) §4 tier-1."),
p(text: "**Census counts are receipts; re-check before acting.** Sections 0-3 were verified against the live tree on 2026-07-26 and have not been re-verified since. Sections 4, 4b and the phase standings were verified 2026-08-31, and the two dates are kept apart deliberately: a single freshness stamp over a document whose halves were measured five weeks apart is the same overclaim as a folded outcome column."),
h2(text: "0. Problem — one native carrier, four meanings"),
p(text: "`Value::Null` overloads four distinct semantics today: (1) the `None`/`none` literal and `LitNull`, (2) `Optional::Absent` (bridged in `match_pattern` at `v1_interpreter.rs:2830`), (3) `Witness::Violates` on map miss (bridged at `:2808` with a fabricated diagnostic), (4) untyped lookup miss (`raw_map_lookup`, `list_get_at_or_null`, `get` on map/list). A blanket `CrossRepresentationEquality` guard cannot close the Optional/Witness straddle — `present == None → false` is *legitimate* at ~218 corpus sites — so the fix is **splitting**, not grounding onto one sentinel."),
h2(text: "1. Target carriers (construction authority)"),
Expand Down Expand Up @@ -45,12 +152,29 @@ fn value_null_split_body() -> List<MarkdownBlock> {
li(text: "Existing witnesses: `witness_option_bridge_test.dag` (map_get → Present/Absent at model layer); `cross_representation_equality.dag` roster includes `Optional` × `native_value_null` straddle (target: remove when grounded)."),
]),
h2(text: "4. Phased landing (construction-first)"),
tasks(items: [
task(state: Unchecked, text: "**Phase A (this lane):** plan + discriminating witnesses pinning carrier invariants (`value_null_split_witness_test.dag`); emitter row table above is authority for S2 emit."),
task(state: Unchecked, text: "**Phase B:** stop *producing* `Null` where the return type is `Optional<T>` — route `map_get`/`get`+Optional context through `map_lookup_as_optional` (keep raw `get` returning bare value + `Null` miss for `map_lookup_dual_dispatch` until typed overload lands)."),
task(state: Unchecked, text: "**Phase C:** delete `match_pattern` `Null` bridges (`:2808–2834`) once no producer emits `Null` for Optional/Witness arms."),
task(state: Unchecked, text: "**Phase D:** type-directed `None` literal → `optional_absent()` where inhabiting `Optional<_>`; migrate `== None` sites (~218) to `match Absent` or `optional_is_absent` helper."),
task(state: Unchecked, text: "**Phase E:** cross-representation equality — ground `Optional` so `Absent` variant reconciles with narrowed `Null` *only* at the lookup-miss boundary; remove `Optional`×`native_value_null` from testgen roster; bundle `CrossRepresentationEquality` guard removal with this phase (fenced in model-realization-fork §3.1)."),
p(text: "**Standing is derived, never ticked.** Each row's standing is `value_null_phase_standing`, a fold over the enrolled-witness roster in this module -- see the note above it for exactly how far that goes (a citation, not evidence) and for the capability that would close the gap. An earlier revision of this section was a hand-checked task list in which every phase, INCLUDING the landed Phase A, read unchecked."),
TableBlock {
header: row(cells: [cell(text: "phase"), cell(text: "content"), cell(text: "standing")]),
alignments: [AlignNone, AlignNone, AlignNone],
rows: [
row(cells: [cell(text: "A"), cell(text: "plan + discriminating witnesses pinning carrier invariants (`value_null_split_witness_test.dag`); the emitter row table in section 2 is authority for S2 emit"), cell(text: value_null_phase_standing_label(phase: PhaseCarrierWitnesses))]),
row(cells: [cell(text: "B"), cell(text: "stop *producing* `Null` where the return type is `Optional<T>` -- route `map_get`/`get`+Optional context through `map_lookup_as_optional`. Extends to `first`/`last`/`lookup`, whose `std.algebra` rows declare `OptionalOf` and whose interpreter arms returned the raw element"), cell(text: value_null_phase_standing_label(phase: PhaseStopProducingNull))]),
row(cells: [cell(text: "C"), cell(text: "delete the `match_pattern` `Null` bridges once no producer emits `Null` for Optional/Witness arms"), cell(text: value_null_phase_standing_label(phase: PhaseDeleteNullBridges))]),
row(cells: [cell(text: "D"), cell(text: "type-directed `None` literal to `optional_absent()` where inhabiting `Optional<_>`; migrate the `== None` sites to `match Absent` or an `optional_is_absent` helper"), cell(text: value_null_phase_standing_label(phase: PhaseNoneLiteralMigration))]),
row(cells: [cell(text: "E"), cell(text: "cross-representation equality -- ground `Optional` so `Absent` reconciles with narrowed `Null` ONLY at the lookup-miss boundary; remove the `Optional`x`native_value_null` testgen straddle; bundle the `CrossRepresentationEquality` guard removal"), cell(text: value_null_phase_standing_label(phase: PhaseCrossRepresentationEquality))]),
row(cells: [cell(text: "F"), cell(text: "**NEW, discovered by building Phase B.** The interpreter gains the optional-into-required-parameter coercion the Rust emitter already has in `rust_call_arg_fail_closed_unwrap` -- unwrap `Present`, refuse typed and located on `Absent`. Phase B without this hands a `Present \{ .. \}` variant to every value-position call site"), cell(text: value_null_phase_standing_label(phase: PhaseArgumentCoercion))]),
row(cells: [cell(text: "G"), cell(text: "**NEW, and it gates F.** Close the language-primitive denominator so `SignatureNotGrounded` means \"not a language primitive\" rather than \"not modelled yet\". A builtin call never reaches the `.dag` call path, and `builtin_function_registry` carries a RETURN TYPE only, so argument cardinality cannot be derived for one"), cell(text: value_null_phase_standing_label(phase: PhasePrimitiveSignatureDenominator))]),
],
},
h2(text: "4b. What Phase B costs, measured"),
p(text: "Phase B was built and measured on a held draft (session still-swift-363, gunbc#9785, not landed). The required-witnesses-floor result is the number this plan should carry, because it is the argument against anyone later proposing Phase B is small enough to land alone."),
ul(items: [
li(text: "`planned=3141 passed=2630 known_red_held=15 failed=442` against a baseline of ~0."),
li(text: "The summary's `failed` FOLDS two states. Read at claim-identity grain from the run's disposition output: **442 runtime-errored-before-verdict**, 6 failed assertions, 1 budget-refused, 47 route-gap, 15 known-red-held. The job log prints only the 6, which reads as a truncated log and is not."),
li(text: "**All 442 are `v2.test.*` and none is a `dag/test/claim` witness.** The cause is self-host coupling: v2 is `.dag` interpreted by the v1 seed, so changing the interpreter changes the v2 COMPILER's behaviour as it executes. Phase B's cost lands on the interpreted v2 compiler, not on corpus witnesses -- which is not what a reader of sections 0-3 would predict."),
li(text: "The 6 assertion failures are this plan's own `raw_get_miss_differs_from_optional_absent`, two `self_host_symbol_identity_binding_witness` claims comparing `== none`, `cargo_build_run_argv`, and two `emit_host_shell_exec_run_equals_eval` claims."),
li(text: "**The Phase A witness predicted its own flip in writing** -- its comment says `raw_get_miss_differs_from_optional_absent` \"flips RED in Phase B when get+Optional routes through `map_lookup_as_optional`\". It did. That is the enrolled signal that Phase B landed, so retiring its expected-red disposition is PART of Phase B and not a repair to it."),
li(text: "The `== none` reds are Phase D arriving early, and they confirm section 0's count from the other direction: `none` EVALUATES to `Value::Null` in the interpreter's variable evaluation, so a raw miss compares equal to `none` because it IS `Null`, while a constructed `Absent` variant does not compare equal at all."),
]),
h2(text: "5. Review bar"),
p(text: "No absorbing fallback: a miss must not widen to `Null` when the type is `Optional` or `Witness`. No new per-site `if matches!(v, Value::Null)` bridges without a counted dissolution trigger. Every phase ships with a discriminating witness that goes RED when the carrier regresses."),
Expand Down
Loading
Loading