Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
17 changes: 16 additions & 1 deletion dag/std/realization_schedule.dag
Original file line number Diff line number Diff line change
Expand Up @@ -211,10 +211,25 @@ WHAT THE EXECUTOR PROVIDES, stated because a carrier that promises more than its

WHAT MAKES THAT CHECKABLE RATHER THAN ASSERTED. The concurrency contract was unreachable by a test while spawn-and-join sat inlined in the batch loop, which is exactly how the first attempt promised concurrency while executing serially. `spawn_units`/`join_units` are split out so a LATCH can reach them: each member increments a shared counter and waits until it observes the other, which a serial executor cannot satisfy because the first member waits for a peer that was never started. The bound on that wait is a deadlock detector, never the assertion. Proven discriminating by mutation — making `spawn_units` run each unit inline turns the overlap control RED with the exact serial signature [false, true] and leaves the join and panic controls green. The stage BARRIER is the join half plus a structural fact: `run_walk`'s stage loop takes `&mut stage_memo` per iteration, so two iterations cannot overlap, and the claim that stage N+1 waits for every stage-N member reduces to the claim that the join returns only after every member completed, which the second control pins.

WHAT STILL REFUSES, and why it is not the old wall. The arm-time validator no longer refuses a heavy-whole-tree-resolve claim: that refusal existed BECAUSE stages bypassed governor admission, and a wall whose reason has become false is a stale claim. What refuses now is the class stages are genuinely not sized for — `spawns_host_compiler` or substantial residency — because stages declare no clamp params (`gunbc_ci_floor_batch_clamp_params` indexes the ORDINARY batches) and such a claim would run admitted but unclamped. That refusal is DERIVED from the whole `RunnableResourceProfile`, which the parse now retains; it previously kept only `heavy_whole_tree_resolve` and `execution_mode` and dropped the other two, so the validator could wall one axis and no more. A discovery runnable still refuses outright: it has no defined green-only meaning.
WHAT STILL REFUSES — the TOTAL account, replacing a paragraph that had gone self-contradictory (review 2026-07-31). The prior text asserted that the arm-time validator no longer refuses a heavy-whole-tree-resolve claim, which was true of one revision and false of the one before AND after it; the restored refusal was described elsewhere in this same note, so the canonical carrier stated both. A partial list is how that happened, so this is written as a closed enumeration rather than as commentary on what changed.

An on-success stage refuses, at arm time:
- an UNDECLARED resource profile — the values would be the parse's fail-closed fillers rather than the plan's statements, and a wall read off invented facts is worse than no wall;
- `heavy_whole_tree_resolve` — such a unit takes the memo lane, which is UNADMITTED, and its resolved context stays resident in the stage memo across every later stage;
- `spawns_host_compiler`;
- SUBSTANTIAL residency — the last two because stages supply no clamp parameters (`gunbc_ci_floor_batch_clamp_params` indexes the ORDINARY batches), so such a claim would run unclamped;
- a DISCOVERY runnable — it has no defined green-only meaning.

All four profile restrictions are conditional on mechanisms stages do not yet have, and each names a DIFFERENT trigger; they do not dissolve together. `spawns_host_compiler` and substantial residency dissolve on stages carrying declared clamp parameters. `heavy_whole_tree_resolve` dissolves on a context-lifetime resident reservation — and that reservation is NOT expressible today, which is the part an earlier draft of this sentence got wrong by naming the lease alone as its trigger. An `AdmittedSlot` is a CONCURRENCY slot: holding one for a memoized context's lifetime pins the active count, so the zero-active progress floor never fires, every later admission holds on a full window, and the width that would relieve it grows only on a completion that can no longer happen. The real trigger is therefore TWO steps in order: split execution-slot accounting from resident-reservation accounting, THEN take a context-lifetime reservation against the second. The undeclared-profile refusal has no dissolution — it is the fail-closed floor.

Every plan function returns WalkPlan<F> — a plan with no postconditions returns on_success_stages: [] — and the executor has ONE strict parser: a malformed or missing field is a hard error, never a fallback to a bare-list reading."

data walk_plan_run_stage_claim_executor_seed_deferral: String = "§7 SEED-RETAINED, declared here because this is where the obligation is INCURRED (review 2026-07-31). `run_stage`, `spawn_units`, `join_units`, `batch_unit_lane`, the stage receipt writers, and the walk-attempt observation are HAND-RUST in `claim_executor.rs`: the executor is the seed that runs before any `.dag` walk exists, so the code that decides how a walk executes cannot itself be a walk. That is a real deferral, not an exemption — the seed grew here, and a growth in the seed is a §7 debt whether or not anyone writes it down.

WHY THIS ROW LIVES WITH THE CARRIER RATHER THAN WITH A CONSUMER. A first draft of this row was authored in the FIXTURE branch that later exercised this code, on the reasoning that the fixture is where the seed expansion became visible. That reverses ownership: the debt belongs to the change that added the Rust, and a downstream consumer documenting its parent's deferral means the parent could land without one. A consumer may cite this row; it may not be the row's home.

MIGRATION TRIGGER: the executor's own scheduling decisions become a `.dag` walk over `WalkPlan` — lane selection, admission, and receipt emission expressed as modeled effects rather than as `std::thread` plus `std::fs` — at which point this Rust becomes an emitted realization and the row deletes. Gated behind the witness-realization lane, since a `.dag`-expressed executor needs native witness execution to run at all. Until then the honest statement is that these are seed-retained by necessity with a named trigger, which is exactly what a self-host frontier row is for."

data walk_finalization_note: String = "THE PLAN CARRIES ITS FINALIZATION POLICY IN ITS TYPE, and the executor never infers it — not from a function's spelling, and not from which arm of a coproduct an authored value happened to pick. Two corrections stacked here. FIRST: the original cut selected finalization by plan-function name (if plan_function == gunbc_ci_floor_plan read the law from the closure) — the same hidden seed-roster convention the WalkPlan carrier was built to remove, reintroduced in the same PR (review 2026-07-30), and the RED fixture made the coupling visible by having to impersonate the production name to arm the contract. Moving it to a field fixed that. SECOND: a field of a coproduct type is still only an authored choice (review 2026-07-30, second pass). With `finalization: WalkFinalization`, `WalkPlan \{ batches: floor_batches, finalization: NoWalkFinalization, .. \}` typechecked — NoWalkFinalization and FloorFinalization inhabit the same sum, so nothing connected floor-shaped work to floor finalization; the production constructor merely chose correctly. So the carrier is PARAMETERIZED: WalkPlan<F>, and gunbc_ci_floor_plan returns WalkPlan<FloorFinalization> while regen, plan-artifact, and falsifier return WalkPlan<NoWalkFinalization>. One runtime parser still reads both, because the parse is over the finalization VALUE and does not care which instantiation produced it. The parameterization also stops this generic std carrier from owning a growing coproduct of gunbc-specific receipt policies: FloorFinalization moved to gunbc.ci_materialization, beside the declared count it is about, and std keeps only the parameter and the declared-empty inhabitant.

WHAT THE PARAMETERIZATION DOES AND DOES NOT BUY, measured rather than assumed — and the measurement contradicted the intent, so the intent is not what gets written down. The review that requested this asked for a construction wall: the floor's return type should REJECT the empty policy. It does not, today. Probed by execution 2026-07-30: replacing the floor's finalization with NoFinalizationDeclared \{\} while the signature still reads WalkPlan<FloorFinalization> TYPECHECKS, and fails only later, at the first field access, as a runtime error. A narrower probe isolates the general defect — the typechecker does not check a function's declared return type against its body at all (`fn f() -> Int \{ \"not an int\" \}` typechecks; so does a mismatched generic instantiation), nor a `data` declaration's annotation against its value, while ARGUMENT position is checked and refuses correctly. So this is a §5 WALL-AFTER-GROUNDING, not a wall now: the class is decidable, the single authority it waits on is return-position typechecking, and until that lands the enforcement is honestly VALIDATION — the enrolled witness floor_plan_projects_the_declared_resolve_count_authority (v2.test.claim.ci_floor_plan_witness) reds when the floor stops projecting the declared count, with a forked-count RED control beside it. Saying the signature walls it would be the same overclaim this note's own history is a record of. dissolve-on: return-position type enforcement in the typechecker, at which point the signature becomes the wall and the witness becomes redundant.
Expand Down
2 changes: 1 addition & 1 deletion docs/plans/fail-closed-lockdown.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ The test for "locked": (a) wired into the floor (discovered + run), (b) fail-clo
| Gate | Scope | Evidence |
| --- | --- | --- |
| DagCompileCleanGate | whole tree (fail-fast root) | `gunbc.ci_gate` `DagCompileCleanGate`; `v2.workflow.ci_floor_plan` `gate_runnable` |
| GeneratedArtifactDriftGate | `ci.yml` / `ROADMAP.md` / `.gitignore` byte-drift + per-artifact perturb, over the committed (= generated AND not-ignored) registry | `ci_spec.dag` `GeneratedArtifactDriftGate`; `generated_artifact_gate.dag`; registry+commit-derivation `gunbc/generated_artifact.dag` |
| GeneratedArtifactDriftGate | `ci.yml` / `ROADMAP.md` / `.gitignore` byte-drift + per-artifact perturb, over the committed (= generated AND not-ignored) registry | `gunbc.ci_gate` `GeneratedArtifactDriftGate`; `tools.generated_artifact_gate` `run_generated_artifact_drift_gate`; `gunbc.generated_artifact` `committed_generated_artifacts` |

These are the **structural** gates. The gap is everything *analytical* and the *bootstrap purity* gate.

Expand Down
Loading
Loading