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
1 change: 1 addition & 0 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
## Open threads

- `v2.std.determinism` — **mechanically preventive for uniquely named registered roots; not repository-wide structural determinism** (honest rung correction, 2026-08-01). Determinism is emergent and boundary-relative (built on `std.perturbation`; a leak carries a `DeclarationRef` to the root reached, not a label enum), and `v2.lens.determinism.determinism_compile_gate` — enrolled in `v2.compiler.compile` `always_required_root_lenses` — refuses the two uniquely named Map projections whose traversal order is host-unspecified: `map_keys` and `map_values`. The former mechanism registered only `map_keys` and asserted it was the one readable nondeterministic atom; that premise was false because `map_values` exposes the same host iteration and was silently classified deterministic. The generic aliases `keys` and `values` remain undetectable: the lens sees only an unqualified callee `Symbol`, v2 `Node` carries neither receiver domain nor resolved declaration identity, and method/free-call lowering erases the distinction; registering either symbol would wrongly refuse unrelated same-named functions. Absence from the root list is therefore **not evidence of determinism**, absence of a diagnostic does not establish that no order-exposing operation was reached, and a newly introduced but unregistered operation is not detected. The attainable ceiling is explicit: the primitive subject universe is forked across `v1.compiler.infer_method` `builtin_function_registry`, `std.primitives` `PrimitiveContract` rows, `std.algebra` templates, native `v1_interpreter` dispatch arms, and per-target emit handlers. This is reachable rather than theoretical: `fold_list` is abundant in compiled v2 trees and has a native interpreter arm while appearing in neither the algebra Map surface nor the builtin registry; `index_by` has a writable native map-producing arm and a `PrimitiveContract` while likewise outside both. A closed denominator cannot be assembled by adding another partial roster. Dissolve-on: the `PrimitiveDefinition` identity join closes the denominator, disambiguates aliases, and gives roots resolvable identity by naming invocation forms, receiver domain, parameters, result, realization, and cost once; then every operation has exactly one traversal-order classification, unclassified refuses, and unsafe roots derive from that one authority. The x2 sampling emit gate remains deleted (#6551 · #6576 · #6594); authority is the carrier (`dag/std/determinism.dag`, `src/v2/lens/determinism.dag`), not this receipt. Prefer preserving meaningful source order in a separate list while using a map only for membership (the corrected PR #7515 pattern); there is no universal `sorted_map_values` order.
- **witness cost derives from purpose — a test is not entitled to arbitrary computation merely because it is a test** (operator ruling, 2026-08-04). A test's size must be DERIVED from what it proves: a modeled boundary it crosses (the smallest crossing specimen is the requirement plus one, never a realistic-looking input chosen for verisimilitude); a live population whose breadth is the subject (which decomposes into small discriminating mechanism fixtures per PR plus the irreducible census on an enrolled cadence — the census may be irreducible, the mechanism never is); an external effect that IS the subject (wet, under an explicit budget); or a resource contract whose threshold comes from a declared requirement. Anything else large is a benchmark, a soak test, a demonstration, or a cost-shape defect in the implementation, and none of those may gate. **The specimen that produced the ruling** is §5's absorbing fallback executed by an author, at the admission layer: a required per-PR witness went over the five-second fast-lane budget, its file was moved under `test/claim/long/`, it left per-PR discovery, no cadence row was added, nothing executed it, and admission still held — green CI, zero executed coverage, source file left behind. That is not deferral; it is deletion of the evidence with the file retained (gunbc#7762 commit `0cfd199f8`, thirteen witnesses, titled *fix CI fast-lane budget failures*). The root was a **directory deciding an admission question**: `OfflineLocalRecipe` — the verdict a broad path pattern produces — was accepted unconditionally, while the exact-admission authority already refused that same shape on an admission row. Two corrections fell out of it. **A claimed construction backstop must be checked against the transformation it is supposed to prevent, not against the state it describes**: `long/` was blessed on the ground that the eval deadline makes an over-budget witness unwritable-in-place, and the deadline is evaluated only while a witness RUNS, so relocation — the exact move — disarms it. And **`BudgetExceeded` is an interruption plus a measured lower bound on cost, never a semantic verdict on a witness, and never discharged by causing its relocation**. **Landed — stated at the scope it actually has**: path location is retired as *sufficient admission for a NEW witness*, and the legacy path-only debt is frozen and counted. `long/` remains an organizational home until that population reaches zero. Mechanically: admission splits into two independent axes because *allowed to remain* and *has an executing consumer* are different facts and one success arm cannot carry both — `WitnessExecutionStanding` (`WitnessHasExecutingConsumer{cadence}` | `LegacyFrozenPathDeferral` | `UnclassifiedPathDeferral` | `UnexecutedDeferredWitness`) and `FrozenBaselineStanding` (`Allowed` | `Shrank` | `Grew` | `Stale`). The **coverage** gate admits only the first arm, so the frozen population never reads as covered and a downstream *is this behavior exercised* receives no; the **floor** gate additionally tolerates `LegacyFrozenPathDeferral` while the baseline axis holds, so the tree stays green through the migration without anything claiming those rows execute. `gunbc.witness_deferral_freeze` enumerates the legacy identities at identity grain (701 across 152 entries at the freeze point); anything outside it and outside `gunbc.explicit_witness_admission` refuses, a frozen row the tree no longer carries refuses, and the roster may only shrink against its diff baseline. The seed realization in `cli_run.rs` is a registered `Scaffold` with a measured landing delta and an ordered dissolution — a modeled policy does not exempt its realization from the hollowing plan. **Open**: the cost half — a per-witness declared cost envelope, which is the trigger for the modified-in-place residue (identity grain cannot see a frozen witness whose body grew a corpus scan) and the condition on which the freeze, the path-policy pass-through arm and the `long/` dir row dissolve together.
- model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md)
- **enforcement intent — ask once, compile forever.** The operator's recurring standing directives (enforce complexity repo-wide; lenses must be live; lenses must self-apply; scope must not silently narrow; model must not carry dual representations; a failure arm must refuse, never widen — no absorbing fallbacks, §5) are redundant governance work (§2) re-paid each conversation — the operator performing the missing meta-lens by hand. Model each as a durable `StandingIntent` row and gate the relationship (intent ⇄ `LensContract` ⇄ coverage receipt) fail-closed: a mechanism *claiming enforcement* is complete only when it satisfies the `StandingIntent` — named live consumer, declared scope not narrowed, red control, self-application or explicit exemption — else Unknown/Refused, never silently green. One new authority (`StandingIntent`); everything else extends existing machinery — the registry (`LensRegistryEntryV0` → `LensContract`), reusing `ConstructionJustification` / `subject_roster` and consuming `intent_linearity` / `self_applying_lenses` for the fractal (§7) layer (the same property applied to the code, the lens, the subject producer, the registry, and the acceptance template). Default enforcement scope = whole corpus; under-scope is a failing receipt unless explicitly justified. → [enforcement-intent design](docs/plans/enforcement-intent-design.md)
- can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)
Expand Down
6 changes: 3 additions & 3 deletions dag/gunbc/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -502,8 +502,8 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
WitnessExclusionRow {
pattern: "test/claim/long/",
classification: OfflineLocalRecipe,
reason: "the LONG-test home at dir grain (operator 5-second rule): membership is a HOME with a construction backstop — the eval deadline makes an over-budget fast-lane witness unwritable-in-place (long_lane_exclusion_note; blessed Form-C in gunbc.roster_registry)",
dissolve_on: "per-witness declared cost envelopes (witness-cost-locality admission law) subsume the dir grain"
reason: "the LONG-test home at dir grain (operator 5-second rule). It removes these entries from per-PR discovery and NOTHING MORE: since 2026-08-04 it no longer answers the admission question, because the eval-deadline backstop it was blessed on is disarmed by the very relocation it was supposed to govern (long_lane_exclusion_note carries the retraction and the gunbc#7762 receipt). Admission is decided at identity grain by gunbc.witness_deferral_freeze plus gunbc.explicit_witness_admission",
dissolve_on: "the frozen path-deferral population reaches empty — every resident carrying an exact admission with a declared purpose, cost and executing cadence — then this row and the path-policy pass-through arm delete together"
},
WitnessExclusionRow {
pattern: "compiler_frontier_per_module_probe_test.dag",
Expand Down Expand Up @@ -762,7 +762,7 @@ fn known_red_probe_roster() -> List<ScheduleWitnessEntry> {
known_red_probe_corpus_roster()
}

data long_lane_exclusion_note: String = "test/claim/long/ is the LONG-test home (operator 5-second rule, 2026-07-12; authority + enforcement: gunbc_ci_fast_lane_rule_note / gunbc_ci_fast_lane_witness_eval_budget in v2.workflow.ci_floor_plan): a witness whose own eval reaches 5s does not run in per-PR discovery — the executor's cooperative eval deadline REDs it by name (EvalBudgetExceeded), and the fix is moving its file here (dag/test/claim/long/, src/v2/test/claim/long/), where discovery excludes it at dir grain and it runs via the local recipe (claim_batch --source-root dag --source-root src/v2 --entry <file> --functions <csv>) or the scheduled lane's future enrollment. First residents (receipted): s1_closure_receipt_test (whole-closure re-parse through the interpreted v2 frontend, 90+min eval, the run-29183446733 wedge class) and self_host_module_emit_derisk_test (~31s/witness). Named consumer with file-grain exclusion row: compiler_frontier_per_module_probe_test.dag (compiler_frontier_per_module_probe_exclusion_note). Unlike the roster exclusions above, membership here is a HOME, not a per-file ruling: the 5s deadline makes an over-budget fast-lane witness unwritable-in-place, so the roster cannot silently grow stale (§5 construction over validation). Dissolve-on: per-witness declared cost envelopes (witness-cost-locality admission law) subsume the dir grain."
data long_lane_exclusion_note: String = "test/claim/long/ is the LONG-test home (operator 5-second rule, 2026-07-12; authority + enforcement: gunbc_ci_fast_lane_rule_note / gunbc_ci_fast_lane_witness_eval_budget in v2.workflow.ci_floor_plan): a witness whose own eval reaches 5s does not run in per-PR discovery — the executor's cooperative eval deadline REDs it by name (EvalBudgetExceeded), and the fix is moving its file here (dag/test/claim/long/, src/v2/test/claim/long/), where discovery excludes it at dir grain and it runs via the local recipe (claim_batch --source-root dag --source-root src/v2 --entry <file> --functions <csv>) or the scheduled lane's future enrollment. First residents (receipted): s1_closure_receipt_test (whole-closure re-parse through the interpreted v2 frontend, 90+min eval, the run-29183446733 wedge class) and self_host_module_emit_derisk_test (~31s/witness). Named consumer with file-grain exclusion row: compiler_frontier_per_module_probe_test.dag (compiler_frontier_per_module_probe_exclusion_note). Membership here was called a HOME rather than a per-file ruling on the ground that the 5s deadline makes an over-budget fast-lane witness unwritable-in-place, so the roster could not silently grow stale. THAT SENTENCE WAS FALSE AND IS RETRACTED (2026-08-04). The deadline is evaluated only while a witness RUNS; relocating its file under this prefix is precisely what stops it running, so the claimed construction backstop is disarmed by the exact move it was supposed to govern, and the home grew by whatever anyone moved into it. BudgetExceeded is an interruption plus a measured lower bound on cost — never a semantic verdict on a witness, and never a discharge of one by causing its relocation. Receipt: gunbc#7762 commit 0cfd199f8, thirteen witnesses relocated here under the title fix CI fast-lane budget failures with a claim_batch command line as their only stated consumer and no cadence row. WHAT NOW HOLDS THE LINE: this prefix still organizes the files, but it no longer answers the admission question. gunbc.witness_deferral_freeze enumerates the exact legacy identities path policy had already admitted, and any offline-classified witness outside that frozen set and outside gunbc.explicit_witness_admission refuses as UnclassifiedPathDeferral, while a frozen row the tree no longer carries refuses as StaleFrozenPathDeferral. Dissolve-on: the freeze reaching empty — every resident carrying an exact admission with a declared purpose, cost and executing cadence — at which point the pass-through arm and this dir row delete together."

data compiler_frontier_per_module_probe_exclusion_note: String = "src/v2/test/claim/long/compiler_frontier_per_module_probe_test.dag is operator-ruled OFFLINE (Lane E closeout): fixture-free per-module frontier_probe_emit_from_ingest receipts over all 27 compiler modules exceed the 5s per-PR fast-lane eval budget; discovery excludes via test/claim/long/ dir grain and per-PR CI never executes these witnesses — green CI says nothing about survey numbers unless the local recipe below ran. LOCAL RECIPE (authority): (1) cargo build -p v1-compiler --bin frontier_probe_survey; (2) per module in compiler_frontier_sweep_order, target/debug/frontier_probe_survey --source-root src/v2 --module <path> (or docs/probes/run_frontier_probe_survey_per_module.sh scaffold until transport enrolls); (3) emit manifest to target/frontier-probe-survey/host_frontier_probe_survey_manifest.dag; (4) claim_batch --source-root src/v2 --source-root dag --source-root target/frontier-probe-survey --entry src/v2/test/claim/long/compiler_frontier_per_module_probe_test.dag --functions compiler_frontier_per_module_probe_survey_holds,compiler_frontier_gap_clustering_common_root_at_blocker_class_holds,compiler_frontier_wave2_blocker_partition_totality_holds,compiler_frontier_roster_bidirectional_totality_live_survey_holds,compiler_frontier_receipt_totality_wall_live_survey_holds,compiler_frontier_wave2_emit_surface_dominates_holds,compiler_frontier_wave2_sizing_band_a_leaf_count_holds. Dissolve-on: all 27 roster modules surveyed at current HEAD, frontier.dag rows hand-authored from receipts, totality wall witnesses pass via this recipe — then this note, the file-grain exclusion row, and the probe scaffold delete together."

Expand Down
Loading
Loading