diff --git a/DESIGN.md b/DESIGN.md index 2b414a4168e..9d941205b72 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -81,6 +81,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - `v2.std.determinism` — §5 determinism mechanism P1 landed (#5941; operator shape-signed, FLAG A/C locked): [determinism mechanism design](docs/plans/determinism-mechanism-design.md) - 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) 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) - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) diff --git a/ROADMAP.md b/ROADMAP.md index 7ea117df01a..0ad9ba20456 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -107,7 +107,7 @@ Receipts + adjacent levers: [fractal Gantt](docs/plans/ci-floor-fractal-gantt.md ## 3. The floor — audit what we have (does it actually do what it claims?) -Both pillars ride the CI floor: tree-wide marker-driven witness discovery · compile-clean gate · generated-artifact drift gates (this document is one) · `regen --verify` (#5873) · doc-graph reachability · emit-determinism (#5941) · the interim self-host comparison (#6009). Those stand. The floor's *expansion* lanes (testgen, wiring-liveness, complexity gates, lens meta-walls) are shelved — a new wall must displace a measured cost on a pillar path to un-shelve. +Both pillars ride the CI floor: tree-wide marker-driven witness discovery · compile-clean gate · generated-artifact drift gates (this document is one) · `regen --verify` (#5873) · doc-graph reachability · emit-determinism (#5941) · the interim self-host comparison (#6009). Those stand. The floor's *expansion* lanes (testgen, wiring-liveness, complexity gates, lens meta-walls) are shelved — a new wall must displace a measured cost on a pillar path to un-shelve (the **enforcement-intent gate** below is the first such un-shelve, 2026-07-02: displaced cost = the operator's repeated manual *what-is-enforced-by-what-lens-over-what-corpus* join, plus CI-killing quadratics and repeated dual-representation/anemia rediscovery). **Audit directive (operator, 2026-07-01): thoroughly audit what we have and what it actually does.** For each load-bearing mechanism, prove **by execution** that it does what it claims, with a **discriminating perturb** that goes RED when the behavior is wrong — a typecheck or a grep is not a consumer (DESIGN §5), and a wired gate can still be vacuous. A mechanism claim without a red-control is *unverified*, whatever its docs say. The reset's own mapping found the pattern live: the committed converge shell is spec-without-execution (§2), the fixpoint gate self-declares interim (2-of-92 files), cargo-green is an ignored test. Highest-stakes mechanisms first: @@ -118,6 +118,7 @@ Both pillars ride the CI floor: tree-wide marker-driven witness discovery · com - [ ] **cache honesty re-receipt** — re-run the warm==cold purity oracle against CURRENT main (616/616 was pre-reset), and close the sccache exit-0-no-binary class (below); a cache that lies is worse than no cache. - [ ] **artifact-freshness gate** *(operator ask: "we need a freshness gate, if we don't already have one")* — we half-do: the per-PR drift gate proves committed==emitted for the PR's OWN tree, but drift still LANDED on main (`.gitignore` stale vs its authority since #6097; found and healed by #6110/#6111) because admission never re-validates against CURRENT main — green-on-branch is not green-on-main. The closing mechanism is the §2 merge-admission freshness block (HELD); this item is its receipt pair: (a) reproduce the landed-drift path as a RED witness, (b) confirm the freshness block refuses it once un-HELD. - [ ] **one tree, one verdict** — 2026-07-01 live finding: `dsl_compile_clean_gate` was GREEN while the discovery-corpus resolve of the same tree was RED (`extdeps.shell` module collision, silent last-root-wins shadowing; de-fork + loud-collision wall shipped as the hotfix). Two resolve paths gave two verdicts on one corpus — enumerate every place a module index is built, and make their collision/ordering semantics ONE authority so a gate cannot be green on a tree the floor cannot resolve. +- [ ] **enforcement intent + model-quality walls** *(operator-directed 2026-07-02; §3 un-shelve — displaced cost: repeated manual "what is enforced, by what lens, over what corpus" joins; CI-killing quadratics; repeated dual-representation/anemia rediscovery)* — model the operator's recurring standing directives as durable `StandingIntent` rows and gate the relationship (intent ⇄ `LensContract` ⇄ `CoverageReceipt`) fail-closed, so a mechanism *claiming* enforcement is complete only when the gate proves the claim **from receipts, not self-declared contract claims**. One new authority (`StandingIntent`); everything else extends existing machinery (`LensRegistryEntryV0` → `LensContract`; reuse `ConstructionJustification` / `subject_roster`; consume `intent_linearity` / `self_applying_lenses`). Anti-overcomplication: no lens may claim *repo-wide* / *blocking* / *complete* / *self-applying* unless the gate can prove it. Rollout: rows live; gate Blocking on contract consistency; object rules AuditOnly until receipts land. Children, A→C before object rules D/E: **A** StandingIntent carrier + LensContract extension (`ConsumerKind`/`ConsumerRequirement` NOT hardwired to `FloorGate`; `EnforcementMode` order `Advisory < AuditOnly < Blocking` modeled) · **B** enforcement_intent_gate contract-consistency reds (over `CoverageReceipt`s) · **C** complexity.repo-wide first proof (3 legs red today, no `decl_facts` dep) · **D** complexity R1 accumulator-in-copied-port object rule (HOLDS behind #6155) · **E** anemia/consolidation first model-quality consumers (suggest a consolidation target, not just warn). [design](docs/plans/enforcement-intent-design.md) **Open floor holes:** diff --git a/docs/plans/enforcement-intent-design.md b/docs/plans/enforcement-intent-design.md new file mode 100644 index 00000000000..0c9ca0904d5 --- /dev/null +++ b/docs/plans/enforcement-intent-design.md @@ -0,0 +1,214 @@ +# Enforcement intent — ask once, compile forever + +*Status: draft for operator review (2026-07-02). Extends the standing threads "model §1's axioms + enforce the syllogism" and the intent-linearity draft; does not supersede either.* + +## 1. The displaced cost (why this is on-dial) + +The operator has repeatedly expressed one standing intent — *enforce complexity / avoid objective quadratics / make lenses real, repo-wide* — and the system keeps treating each utterance as a fresh local request. The recurring manual join is: + +> what is enforced · where · over which corpus · by which lens · is it live · does it reach v1 · does it apply to itself? + +That join is **redundant governance work** (§2): paid again on every new lens, gate, PR, and roadmap node. It is the meta-instance of the very bug we chase in the object code — an intent that must be re-discovered because it was never made load-bearing. The deliverable's denominated benefit (§6) is *this displaced cost*: the operator stops performing the missing meta-lens. + +## 2. DFS first — what already exists (do NOT re-mint) + +Per §2/§3, before minting vocabulary we map onto the concept DAG. The carriers the naive proposal would fork **already exist**: + +- **Decidability boundary** — `v2.lens.common.construction_justification :: ConstructionJustification` (`WallNow` / `WallAfterGrounding` / `RatchetForever`). Reuse verbatim; do not add a parallel `declared_boundary` enum. +- **Lens contract (V0)** — `v2.lens.registry :: LensRegistryEntryV0 { lens_id, module_path: Bound | Unbound }`. This is the seed of `LensContract`; **extend it**, don't fork a new type. +- **Scope / subject set** — the per-lens `subject_roster` pattern (`v2.lens.idempotency.subject_roster`, `v2.lens.ownership.subject_roster`, …). Reuse the pattern; the scope of an intent is a `subject_roster` expression. +- **Self-application / fractal** — `v2.lens.intent_linearity` + `dsl/gunbc/plans/self_applying_lenses.dag` + `axiom_syllogism_lens.dag`. The "apply the lens to the intent expression itself" layer is already being modeled here; the enforcement-intent gate **consumes** it, it does not re-invent it. +- **Inertness backstop** — `dsl/test/claim/inert_lens_hygiene_witness_test.dag` (DESIGN §6's executable "wired-or-deleted" check, already live over the corpus). The meta-gate **strengthens** this from "is the lens wired at all?" to "does the lens satisfy the *declared scope* and self-apply?" + +**Net: this is an extension, not a greenfield build.** That materially shrinks the work and keeps single-authority intact. + +## 3. The one genuinely missing thing: the join + +Two additions, both minimal: + +### 3a. `LensContract` = extend `LensRegistryEntryV0` +Add to the existing registry entry the fields that make "is it enforced?" decidable: + +``` +type LensContract { // grows LensRegistryEntryV0, one concept + lens_id: LensIdV0 + module_path: LensModulePathV0 // already present + claimed_scope: SubjectRoster // reuse the subject_roster carrier + mode: EnforcementMode // Advisory < AuditOnly < Blocking (§12) + consumer: ConsumerKind // FloorGate | MergeAdmission | … | None (§12); "referenced by synthesis" == None + red_control: Present { witness: QualifiedName } | Absent + self_application: SelfApplies | Exempt { reason: String } + boundary: ConstructionJustification // reuse — WallNow / WallAfterGrounding / RatchetForever +} +``` + +### 3b. `StandingIntent` — the operator's durable directive (the only new authority) +A row, not a doc paragraph — the mark on the carrier is the authority (§6): + +``` +type StandingIntent { + id: String // "complexity.repo-wide" + property: LensIdV0 // REUSE the existing lens-property coproduct (src/v2/lens/registry.dag:10 — Complexity | Cost | …); do NOT mint a PropertyClass nickname (§3) + desired_scope: SubjectRoster // default = WHOLE CORPUS (see §5) + required_subjects: List // the receipts that MUST be covered + default_mode: EnforcementMode // Advisory < AuditOnly < Blocking (§12) + required_consumer: ConsumerRequirement // AnyLiveConsumer | OneOf | Exact (§12) — NOT hardwired to FloorGate + self_application_required: Bool + fallback_when_unavailable: Refuse | Unknown | AuditOnlyWithReason // never silently OK (§5) +} +``` + +`StandingIntent` references the property and subject carriers rather than restating them; it is the single home for "what the operator wants," so a future PR can refine the *implementation* but cannot silently narrow the *intent*. + +**Admission rule — `StandingIntent` is durable governance, not a preference bucket.** A row is admissible only if it (a) *recurs* across PRs, (b) has a *named displaced cost* (§6), (c) has a *scope*, (d) names an *enforcement mechanism class*, and (e) *can produce a receipt*. "make this cleaner" / "prefer better names" fail (a) and (e); the five initial rows pass. This keeps the carrier from degenerating into a global lint dump. + +## 4. The meta-gate (decidable — a wall now) + +``` +enforcement_intent_gate(intent: StandingIntent, contracts: List, receipts: CoverageReceipts) -> Witness +``` + +For each `StandingIntent` it proves, all fail-closed (`fallback_when_unavailable` on any miss — never green): + +1. **claimed** — some `LensContract` names `intent.property` with `enforcement_mode_satisfies(contract.mode, intent.default_mode)` (§12 order; no overloaded `>=`). +2. **scope ⊇** — `scope_satisfaction(contract.claimed_scope, intent.desired_scope)` is `ScopeCovers`, or a typed `ScopeNarrowed { reason }` whose reason kind the intent allows (§12; set-containment on declared roots — decidable). +3. **subjects ⊇** — the *discovered* subject set (from the `CoverageReceipt`, not the contract's claim) includes every `required_subject` (membership over the live discovery — decidable; this is the leg that fails today on `src/v1/04_infer.dag::build_type_env`). +4. **live consumer** — `consumer_satisfies(contract.consumer, intent.required_consumer)` (§12) — NOT hardwired to `FloorGate`, so merge-admission / pre-push / periodic-actuator / deploy-readback consumers count; `None` = the coverage-by-illusion failure. Reuses the inert-lens backstop. +5. **red control** — the `CoverageReceipt`'s `red_control_status == RedControlPassed` — the witness actually went red under perturbation (§5 green-by-execution). A contract that self-declares `Present` but whose receipt is `RedControlFailedToFlip`/`NotRun` still reds. +6. **self-application** — the lens module is in its own property's subject set, or carries an explicit `Exempt { reason }`. + +Every leg is decidable set-containment or liveness → the meta-gate is a `WallNow`, not a ratchet. It is itself classified by `ConstructionJustification`, and (§7) it is subject to itself. + +## 5. Flip the default: whole-corpus unless explicitly narrowed + +The operator's "objective things, enforce on the entire corpus — why not" becomes a *default*, not a per-lens opt-in: + +- `StandingIntent.desired_scope` defaults to **whole corpus** (`["dsl", "src/v1", "src/v2"]`, `DagSource`). +- Scope containment is a typed `ScopeSatisfaction` (§12): `ScopeCovers` | `ScopeNarrowed { missing, reason: NarrowingReason }` | `ScopeMissing`. A `LensContract` narrower than a `StandingIntent` it answers must carry a typed `NarrowingReason` (`BootstrapBlocked` / `TypeReflectionUnavailable` / `ExternalRuntimeOnly` / `ExplicitOperatorExemption`) — a Blocking intent **Refuses** unless the reason kind is on its allow-list; an AuditOnly intent **Reports**. Not a stringly escape hatch. +- This inverts the permissive interface: silence no longer means "v2 only." Under-scope is a failing receipt, not a default. + +## 6. The fractal layer (reuse, don't re-invent) + +Your point that the lens must apply to the *intent expression*, not just the code, is §7 recursion and is already seeded in `intent_linearity` + `self_applying_lenses`. The enforcement-intent gate makes it a **required leg** (§4.6), across five occurrences of the same property: + +1. the program analyzed · 2. the lens implementation · 3. the subject producer · 4. the enforcement registry · 5. the dispatch manager's acceptance template. + +Concretely for complexity: if `complexity_lens`'s subject producer recomputes closure per lens (O(n²) over the corpus), the enforcement of the complexity intent *itself violates the complexity intent* — and the self-application leg reds. Same case, one layer up. + +## 7. Sequencing (so the corpus can still merge) + +The **meta relationship** is Blocking now — it is decidable and cheap: scope-must-not-narrow, lens-must-be-live, must-self-apply. The **object complexity rule** ships `AuditOnly` over the whole corpus first (it will surface the 10 `06_translate.dag` + 3 `glob_discovery_law.dag` quadratic-suspect sites, several harmless-by-magnitude), then flips per-rule to `Blocking` as the false-positive magnitude tiers land. Blocking the object rule whole-corpus on day one would red everything; Blocking the *coverage* on day one is exactly what we want. + +## 8. Tasks (refined; each reuses an existing carrier) + +1. **standing-intent-carrier** — `StandingIntent` type + the `complexity.repo-wide`, `lenses.must-be-live`, `lenses.self-apply-or-exempt` rows. Reuses `LensIdV0` (the existing lens-property coproduct — NOT a new `PropertyClass`), `SubjectRoster`, `ConstructionJustification`. +2. **lens-contract-extend** — grow `LensRegistryEntryV0` → `LensContract`; classify `complexity_lens` precisely (fixture-only vs live-syntactic; blocking vs advisory); record claimed scope + discovered subject counts. `build_type_env` / former `flatten` present-or-absent **by execution**. +3. **enforcement-intent-gate** — the join (§4). RED controls: absent-`src/v1` reds; whole-corpus-claim-but-scans-only-`src/v2` reds; blocking-without-consumer reds; blocking-without-red-control reds; audit-only passes only in `AuditOnly`. +4. **complexity-bad-shape-wall (R1)** — the first real wall: accumulator-in-copied-port (`map_merge` overlay / `list_append` left), with the v1 fixtures and the `merge_envs` negative test; floor-enrolled *through* the enforcement-intent gate so it cannot be inert. + +Do 1–3 before adding many object rules, else task 4 is just one more possibly-inert lens. + +## 9. Honest limits + +- **Decidable (Blocking):** scope containment, subject coverage, consumer liveness, red-control presence, self-application. These are repo policy, not undecidable. +- **Count-witnessed residue:** magnitude / boundedness of a growing side (is the suspect fold actually bounded?) — a size fact the graph does not carry. Count-witness, never a wall-clock threshold. +- **Genuinely off-substrate:** the v1 interpreter's own quadratic is Rust (`v1_interpreter.rs`), not Nodes — structurally uncoverable by a Node lens; report as a clean negative, not a gap. + +## 10. The sentence for the manager + +> The operator has repeatedly asked for complexity enforced repo-wide. Your first job is **not** to add another complexity check — it is to make that standing intent impossible to lose: extend the registry into a contract, model the intent as a row, and gate the relationship fail-closed. A PR that narrows complexity from whole-corpus to fixture-only, adds a lens without a consumer, claims "blocking" without a red control, or omits `src/v1` without an explicit bootstrap exemption must go red. + +## 11. Operator sign-off refinements (2026-07-02) + +Signed off with these deltas: + +- **Wording:** completion attaches to *a mechanism claiming enforcement*, not to every lens. Not all lenses answer a standing directive (some are local experiments / advisory diagnostics); only ones that *claim* enforcement (`repo-wide`, `blocking`, `complete`, `self-applying`) are held to a `StandingIntent`. +- **Anti-overcomplication rule (the wall that keeps the walls honest):** *no lens may claim `repo-wide`, `blocking`, `complete`, or `self-applying` unless the enforcement gate can independently prove the claim.* This is the meta-gate turned on the vocabulary of the claims themselves. +- **Two model-quality StandingIntents** — the DFS/anemia/consolidation habit is the *same governance bug on the single-authority axis* rather than the runtime-complexity axis (§2 deep-reduction, §3 single-authority). Add: + + ``` + model.anemia.repo-wide // a String leaf hiding named parts is anemic (decompress→map→reduce) + single-authority.consolidation // two names for one concept fail unless one is explicitly + // realization / transport / external-source WITH direction + ``` + + `concept-dfs-before-minting` is an *implementation rule under* `single-authority.consolidation`, not (yet) its own top-level intent. The lens must **suggest a consolidation target**, not merely warn — "what existing concept should this map to? where is the single authority? is this a realization/transport/policy variant?" Live seed corpus: the `extdeps.shell` fork (main-red incident), the JSON-emitter fork, the hostname-surface split, `cli_run` BFS vs `module_graph` closure authority. + +- **Rollout (so the corpus still merges, without a weak gate):** three tiers, not one flip. + 1. `StandingIntent` rows: **live**. + 2. `enforcement_intent_gate`: **Blocking on contract *consistency*** now — a claim that is internally impossible fails immediately, independent of any dependency: Blocking-with-no-consumer → fail; whole-corpus-claim-scanning-only-v2 → fail; self-apply-required-but-absent → fail; AuditOnly-with-a-declared-scope-gap → report, not block. + 3. Object rules (R1/R2/R3, anemia, consolidation): **AuditOnly** over the whole corpus until the receipts are understood, then per-rule flip to Blocking as false-positive magnitude tiers land. + + This is confirmed by silent-ferret's #6162 characterization: `complexity.repo-wide` already reds today on **three contract legs** — claimed_scope (4 exemplars + 3 synthetic, not repo-wide), consumer (witness-only, no FloorGate), self_application (false) — with **no `decl_facts` dependency**. The gate's first honest RED needs nothing new; the whole-corpus *subject-discovery* leg waits on the `decl_facts(roots)` reflection builtin (#5966 / gunbc#5364), and the gate's job is precisely to red on that gap rather than hide it. + +- **Task order (manager):** 1 `StandingIntent` rows · 2 `LensContract` extension · 3 `enforcement_intent_gate` · 4 `complexity.repo-wide` first proof · 5 `model.anemia.repo-wide` + `single-authority.consolidation` next proof · 6 *only then* R1/R2 object rules. Do 1–3 before adding object rules, else task 6 is one more possibly-inert lens. + +## 12. Type refinements (operator review 2026-07-02) + +Concrete carriers so the gate consumes **receipts, not prose**. These supersede the sketchy inline enums in §3–§5. + +### Consumer — not hardwired to the floor + +``` +type ConsumerKind + = FloorGate | MergeAdmission | PrePushHook | PeriodicActuator + | RoadmapDriftGate | DeployReadback | WitnessOnly | None + +type ConsumerRequirement // lives on StandingIntent + = AnyLiveConsumer + | OneOf { acceptable: List } + | Exact { kind: ConsumerKind } + +fn consumer_satisfies(actual: ConsumerKind, required: ConsumerRequirement) -> Bool +``` + +Rationale: the roadmap already has load-bearing enforcement *off* the floor — merge-admission freshness, pre-push doc/drift hooks, periodic converge, deploy read-back, generated-artifact gates. A gate that knows only `FloorGate` would reject valid enforcement or pressure everything into the floor. `complexity.repo-wide` sets `required_consumer = Exact { FloorGate }`; a merge-admission intent may set `OneOf`/`AnyLiveConsumer`. + +### Enforcement mode — model the order, no overloaded `>=` + +``` +type EnforcementMode = Advisory | AuditOnly | Blocking // Advisory < AuditOnly < Blocking +fn enforcement_mode_satisfies(actual: EnforcementMode, required: EnforcementMode) -> Bool +``` + +REDs: required `Blocking` + actual `AuditOnly` → red · required `AuditOnly` + actual `Advisory` → red · required `Advisory` + actual `AuditOnly` → green. + +### Scope satisfaction — typed narrowing, not a stringly hatch + +``` +type ScopeSatisfaction + = ScopeCovers + | ScopeNarrowed { missing: SubjectRoster, reason: NarrowingReason } + | ScopeMissing + +type NarrowingReason + = BootstrapBlocked { blocker: String } // e.g. src/v1 pending self-host + | TypeReflectionUnavailable { blocker: String } // e.g. decl_facts(roots) not yet landed + | ExternalRuntimeOnly { reason: String } // e.g. the interpreter's off-substrate Rust loop + | ExplicitOperatorExemption { signoff: String } +``` + +Rollout: `Blocking` intent + `ScopeNarrowed` → Refused unless the reason kind is on the intent's allow-list; `AuditOnly` intent + `ScopeNarrowed` → Report. `complexity.repo-wide`'s v1-reach gap carries `TypeReflectionUnavailable { blocker: "decl_facts(roots) #5966/gunbc#5364" }` today. + +### CoverageReceipt — the gate reads receipts, never self-declared claims + +``` +type CoverageReceipt { + contract_id: LensIdV0 + discovered_subjects: SubjectRoster // what the live producer ACTUALLY found + consumer_observed: ConsumerKind + consumer_receipt_ref: ReceiptRef + red_control_status: RedControlStatus + self_application_status: SelfApplicationStatus + probed_at: Timestamp // supply via args; no argless clock in-substrate +} + +type RedControlStatus + = RedControlPassed | RedControlMissing | RedControlNotRun | RedControlFailedToFlip +``` + +The gate consumes `CoverageReceipt`, never the `LensContract`'s self-declared claim: a contract claiming `red_control: Present` whose receipt says `RedControlFailedToFlip` still reds. This is §5 "green by execution, not by declaration" — applied to the gate itself (§7). + +### StandingIntent admission (restated as a check) + +A candidate row must satisfy all five: recurs across PRs · named displaced cost (§6) · has a scope · names a mechanism class · can produce a receipt. Fail any → it is a preference, not a `StandingIntent`. This is itself the anti-purity-trap guard (§6) turned on the governance carrier. diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag index d6f41109cb2..05860bb8ae8 100644 --- a/dsl/gunbc/design_document.dag +++ b/dsl/gunbc/design_document.dag @@ -141,6 +141,7 @@ fn open_threads_blocks() -> List { ul(items: [ li(text: "`v2.std.determinism` — §5 determinism mechanism P1 landed (#5941; operator shape-signed, FLAG A/C locked): [determinism mechanism design](docs/plans/determinism-mechanism-design.md)"), li(text: "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)"), + li(text: "**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) 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)"), li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"), li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"), diff --git a/dsl/gunbc/roadmap_authority.dag b/dsl/gunbc/roadmap_authority.dag index f3ff71f3fe7..be6d26f35c6 100644 --- a/dsl/gunbc/roadmap_authority.dag +++ b/dsl/gunbc/roadmap_authority.dag @@ -257,7 +257,7 @@ fn section_3() -> RoadmapSection { RoadmapSection { title: "3. The floor — audit what we have (does it actually do what it claims?)", elements: [ - section_prose(content: "Both pillars ride the CI floor: tree-wide marker-driven witness discovery · compile-clean gate · generated-artifact drift gates (this document is one) · `regen --verify` (#5873) · doc-graph reachability · emit-determinism (#5941) · the interim self-host comparison (#6009). Those stand. The floor's *expansion* lanes (testgen, wiring-liveness, complexity gates, lens meta-walls) are shelved — a new wall must displace a measured cost on a pillar path to un-shelve."), + section_prose(content: "Both pillars ride the CI floor: tree-wide marker-driven witness discovery · compile-clean gate · generated-artifact drift gates (this document is one) · `regen --verify` (#5873) · doc-graph reachability · emit-determinism (#5941) · the interim self-host comparison (#6009). Those stand. The floor's *expansion* lanes (testgen, wiring-liveness, complexity gates, lens meta-walls) are shelved — a new wall must displace a measured cost on a pillar path to un-shelve (the **enforcement-intent gate** below is the first such un-shelve, 2026-07-02: displaced cost = the operator's repeated manual *what-is-enforced-by-what-lens-over-what-corpus* join, plus CI-killing quadratics and repeated dual-representation/anemia rediscovery)."), section_prose(content: "**Audit directive (operator, 2026-07-01): thoroughly audit what we have and what it actually does.** For each load-bearing mechanism, prove **by execution** that it does what it claims, with a **discriminating perturb** that goes RED when the behavior is wrong — a typecheck or a grep is not a consumer (DESIGN §5), and a wired gate can still be vacuous. A mechanism claim without a red-control is *unverified*, whatever its docs say. The reset's own mapping found the pattern live: the committed converge shell is spec-without-execution (§2), the fixpoint gate self-declares interim (2-of-92 files), cargo-green is an ignored test. Highest-stakes mechanisms first:"), section_group( label: "Audit — green by execution, red by perturbation", @@ -267,6 +267,7 @@ fn section_3() -> RoadmapSection { authored(id: "3-audit-cache-honesty", done: false, content: "**cache honesty re-receipt** — re-run the warm==cold purity oracle against CURRENT main (616/616 was pre-reset), and close the sccache exit-0-no-binary class (below); a cache that lies is worse than no cache."), authored_wi(id: "3-audit-artifact-freshness", done: false, content: "**artifact-freshness gate** *(operator ask: \"we need a freshness gate, if we don't already have one\")* — we half-do: the per-PR drift gate proves committed==emitted for the PR's OWN tree, but drift still LANDED on main (`.gitignore` stale vs its authority since #6097; found and healed by #6110/#6111) because admission never re-validates against CURRENT main — green-on-branch is not green-on-main. The closing mechanism is the §2 merge-admission freshness block (HELD); this item is its receipt pair: (a) reproduce the landed-drift path as a RED witness, (b) confirm the freshness block refuses it once un-HELD.", intricacy: IntricacyMedium, volume: VolumeSmall, repo: "gunbc"), authored(id: "3-audit-gate-disagreement", done: false, content: "**one tree, one verdict** — 2026-07-01 live finding: `dsl_compile_clean_gate` was GREEN while the discovery-corpus resolve of the same tree was RED (`extdeps.shell` module collision, silent last-root-wins shadowing; de-fork + loud-collision wall shipped as the hotfix). Two resolve paths gave two verdicts on one corpus — enumerate every place a module index is built, and make their collision/ordering semantics ONE authority so a gate cannot be green on a tree the floor cannot resolve."), + authored(id: "3-enforcement-intent", done: false, content: "**enforcement intent + model-quality walls** *(operator-directed 2026-07-02; §3 un-shelve — displaced cost: repeated manual \"what is enforced, by what lens, over what corpus\" joins; CI-killing quadratics; repeated dual-representation/anemia rediscovery)* — model the operator's recurring standing directives as durable `StandingIntent` rows and gate the relationship (intent ⇄ `LensContract` ⇄ `CoverageReceipt`) fail-closed, so a mechanism *claiming* enforcement is complete only when the gate proves the claim **from receipts, not self-declared contract claims**. One new authority (`StandingIntent`); everything else extends existing machinery (`LensRegistryEntryV0` → `LensContract`; reuse `ConstructionJustification` / `subject_roster`; consume `intent_linearity` / `self_applying_lenses`). Anti-overcomplication: no lens may claim *repo-wide* / *blocking* / *complete* / *self-applying* unless the gate can prove it. Rollout: rows live; gate Blocking on contract consistency; object rules AuditOnly until receipts land. Children, A→C before object rules D/E: **A** StandingIntent carrier + LensContract extension (`ConsumerKind`/`ConsumerRequirement` NOT hardwired to `FloorGate`; `EnforcementMode` order `Advisory < AuditOnly < Blocking` modeled) · **B** enforcement_intent_gate contract-consistency reds (over `CoverageReceipt`s) · **C** complexity.repo-wide first proof (3 legs red today, no `decl_facts` dep) · **D** complexity R1 accumulator-in-copied-port object rule (HOLDS behind #6155) · **E** anemia/consolidation first model-quality consumers (suggest a consolidation target, not just warn). [design](docs/plans/enforcement-intent-design.md)"), ], edges: [], ),