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
7 changes: 4 additions & 3 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l

- [x] **inert-lens hygiene backstop** — every `lens/*.dag` wired or deleted; runs over the corpus (#5433)
- [ ] **reachability-completeness lens** — every declared node (code carrier · doc · lens) reachable from a run-root, rostered, or deleted; generalizes #5433 to carriers + docs ([plan](docs/plans/inert-layer-lens.md))
- [ ] **gate-hygiene: a floor-enrolled gate must be green-on-main at merge** — roster-completeness assertion promoted to should-land ([plan](docs/plans/emission-ingestion-inverse.md) §2) *(quick-ant-298)*
- [x] **construction-justification rule** (authoring-time) — justify why a class can't be construction before adding a lens (#5476) ([DESIGN §6](DESIGN.md)) *(silent-wren-739)*
- [ ] **gate-hygiene: a floor-enrolled gate must be green-on-main at merge** — roster-completeness assertion promoted to should-land ([plan](docs/plans/emission-ingestion-inverse.md) §2; [merge-freshness decision record](docs/plans/ci-merge-freshness.md)) *(quick-ant-298)*
- [x] **construction-justification rule** (authoring-time) — justify why a class can't be construction before adding a lens (#5476; [plan](docs/plans/construction-justification-rule.md), [DESIGN §6](DESIGN.md)) *(silent-wren-739)*
- [ ] **expressibility frontier** — partition each modeling discipline into wall / lens-residue / undecidable-review *before* gating ([plan](docs/plans/expressibility-frontier.md))
- [ ] **confront the skipped modeling decisions** — the `🟡` comment backlog ([Disposition plan](docs/plans/disposition-carrier.md))
- [ ] **axiom + syllogism lens** (DESIGN open thread #1) — every claim chains back to an axiom, no orphan/cycle; stays `[ ]` until it runs executably over this doc
Expand All @@ -69,7 +69,7 @@ A flaky or green-but-broken floor means no gate protects anything — so CI is u
- [ ] per-PR = #5427 run-all sound baseline, shrunk to the affected set (#5427)
- [ ] nightly = full-corpus selector-backstop + non-hermetic residue (#5447 stood down; ⚠ CI-gen load-bearing) *(quick-ant-298)*
- [ ] **floor runs reliably & affordably** — memory-aware scheduling (spawn_width is memory-blind → OOM as the corpus grows) + kill sccache false-greens
- [ ] **tree-scoped builtin registry** (fail-closed) — global seed registry leaks intrinsics into the substrate compile; instance fix #5452, class fix (partition) open *(quick-ant-298)*
- [ ] **tree-scoped builtin registry** (fail-closed) — global seed registry leaks intrinsics into the substrate compile; instance fix #5452, class fix (partition) open ([force-check plan](docs/plans/compile-clean-forcecheck.md)) *(quick-ant-298)*
- [ ] repo model (internal repo) on compute fabric
- [ ] **CI on compute fabric** — derive every host knob from one measured `ResourceEnvelope`; ends the crash-or-idle swing ([plan](docs/plans/compute-envelope-model.md))
- [ ] *(downstream)* compute fabric as a sellable infra piece
Expand All @@ -85,6 +85,7 @@ Gate: uncached non-redundant work is an ERROR, not "slow". The cache-key-from-in
- [x] F2/F3 `resolved_graph` key derived from declared `inputs_considered` — construction, not a lens (#5425)
- [ ] P1 honest keys by construction — warm==cold purity oracle (#5429)
- [ ] P2 one door: `realize(subject)` sole API — kernel inhabits `cache_interface.dag` (#5446); ParseTable dissolution is downstream of the dsl→v2 de-fork (§5)
- hermetic fixtures feed P2: [x] M4.1 universal hermetic corpus governance (#5236, [plan](docs/plans/m4-universal-hermetic-corpus.md)); [ ] M5 fixture-store onto one Realization kernel ([plan](docs/plans/m5-fixture-store-consolidation.md))
- [ ] P3 **resolve-cache enable** — cuts ~18% of floor wall; purity proven (616/616); gated on #5429 ← **core ask**
- [ ] P4 economic tier (measured cost → `Materialization`) — instrument done (#5431); remaining = the consumer feedback + width-fold
- [ ] P5 native `content(T) = content_hash(subgraph)` — gated on B2
Expand Down
27 changes: 25 additions & 2 deletions docs/plans/inert-layer-lens.md
Original file line number Diff line number Diff line change
Expand Up @@ -177,8 +177,8 @@ but are unwired" — surfaced as the ranked head of the inert list.
Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every
breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or
deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph —
and the doc instance is the **cheapest wall of all** (pure link reachability, no reflective edges, no
host bridges):
and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges
*needed for the dangling half*, and far simpler than the code substrate):

| substrate | nodes | edges | roots | inert = | dangling = |
| --- | --- | --- | --- | --- | --- |
Expand Down Expand Up @@ -207,10 +207,33 @@ it). **Repointed in this PR** to the doc that holds the content. The wall would
(Methodology note: the *first* census run reported this ref as 2× — it had read a stale local `ROADMAP`
behind main's terse pass; the lens must run against the live tree, the same discipline it enforces.)

**LANDED — the doc-graph wall is live (gunbc#5484), with one premise correction.** The "no host
bridges" claim above holds **only for the dangling half**. The *orphan* half is `universe ∖ reachable`,
and the universe is `docs/**/*.md` — which requires filesystem **enumeration**, and there is no
list-dir host effect in `.dag` today (`std/filesystem` exposes only `Read`/`Write`). So the orphan
half is host-fed: `src/v1/stage0/src/doc_reachability_project.rs` walks the tree and exposes two scalar
verdicts (`doc_graph_orphan_count` / `doc_graph_dangling_link_count`) through the same additive
corpus-gate builtin seam as `extdeps_external_authority_live_clean_tree_holds` / `fact_cardinality_*`
(it does **not** touch `cli_run.rs`'s #5433 closure). The reachability primitive is the **same BFS
shape** as `inert_lens_modules` re-expressed over doc nodes — the §3-single-authority doc *instance* of
the one rule, not a forked concept. The dangling half alone *is* expressible in pure `.dag`
(`filesystem_read` BFS from roots). **DISSOLUTION TRIGGER:** when `.dag` gains list-dir / compile-graph
access (gunbc#5364, the Tier-2 note), the dir-walk + BFS fold into a pure `.dag` reader and the Rust
census deletes. Re-derived against the **live** tree at landing: **22 docs, 22 reachable, 0 orphans, 0
dangling** — clean, because this PR added the five missing inbound links + a `docs/runbooks/README.md`
index root (the runbook-kind root) and linked the runbook from it. Witness:
`dsl/test/claim/doc_reachability_witness_test.dag` (floor-discovered `test fn`s, fail-closed, RED on
revert); RED/GREEN controls over a synthetic graph in the project module's unit tests.

## 9. Open

- Confirm the run-root set (is `scheduler.dag` the sole runtime, or also the v1 `claim_executor` path?
the digest census touched both).
- Decide Tier-1-now vs wait for Tier-2's host bridge so the first landing is symbol-granular (the census
shows the interesting cases are symbol-level — `execution_receipt_digest`, `CacheLayerPlan` — so a
module-only first cut may under-deliver; weigh against Tier 1's zero-new-machinery cost).
- **Doc-graph next steps (post gunbc#5484):** (a) fold the dangling half into a pure `.dag`
`filesystem_read` BFS now (no new host effect needed), leaving only the orphan-half enumeration
host-fed until gunbc#5364; (b) the **code** Tier-1/Tier-2 instances (the original target class —
`CacheLayerPlan`, `WorkDemand`, `execution_receipt_digest`) remain unbuilt; the doc instance is the
cheapest, not the substantive one.
14 changes: 14 additions & 0 deletions docs/runbooks/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
# Runbooks — operational index

Operational runbooks for the project's infrastructure (the CI compute fabric, hosts, access). These
are *operational* docs, not roadmap items — so they root here, at their own index, rather than from
`ROADMAP.md`/`DESIGN.md` (the doc-graph reachability wall, `docs/plans/inert-layer-lens.md` §8,
roots each doc *kind* at its own root so a runbook does not false-positive as a plan orphan).

A new runbook must be linked from this index in the same PR that adds it — the doc-graph analog of
"an inert lens is a lie".

## Index

- [BMC Redfish operator access (srv1 / srv2)](bmc-redfish-operator-access.md) — enable and verify
out-of-band Redfish telemetry on the self-hosted CI fleet hosts.
41 changes: 41 additions & 0 deletions dsl/test/claim/doc_reachability_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
// dsl/test/claim/doc_reachability_witness_test.dag
//
// Floor witness for the DOC-GRAPH reachability-completeness WALL
// (docs/plans/inert-layer-lens.md §8). The doc substrate of the one reachability
// rule the #5433 inert-lens backstop runs over the lens substrate (DESIGN §3
// single authority: same rule, different graph — NOT a forked concept).
//
// THE RULE: every declared `docs/**/*.md` must be reachable from a root
// (ROADMAP/DESIGN for plan docs; docs/runbooks/README.md for runbooks), reached
// via a reflective `.dag`-comment `bind:` ref, or deleted. A dangling `](x.md)`
// link is forbidden. Both verdicts FAIL-CLOSED: any orphan / any dangling → RED.
//
// Host-fed (the orphan half needs filesystem enumeration; no list-dir `.dag` host
// effect exists yet — folds into pure `.dag` on gunbc#5364, the plan Tier-2 note).
// The verdicts come from the doc_reachability_project census builtins, the same
// additive corpus-gate seam as extdeps_external_authority_live_clean_tree_holds /
// fact_cardinality_*.
//
// RED-on-revert: revert any of this PR's inbound links → an orphan reappears →
// doc_graph_orphan_count() > 0 → doc_graph_has_no_orphan_docs() goes RED. Break a
// `](x.md)` link → doc_graph_dangling_link_count() > 0 → the dangling witness RED.
// The discriminating RED/GREEN controls over a synthetic graph live in the project
// module's unit tests (reachable_set_flags_orphan_node, dangling_detection_*).

module test.claim.doc_reachability_witness

// Every `docs/**/*.md` is reachable from a root (no orphan plan docs / runbooks).
test fn doc_graph_has_no_orphan_docs() -> Bool {
return doc_graph_orphan_count() == 0
}

// No broken `](x.md)` markdown link anywhere in the doc graph.
test fn doc_graph_has_no_dangling_links() -> Bool {
return doc_graph_dangling_link_count() == 0
}

// §5 non-emptiness floor: a zero universe means the `docs/` walk fail-opened (read_dir error),
// which would make orphan_count==0 a false green — so zero discovered docs is itself RED.
test fn doc_graph_universe_is_nonempty() -> Bool {
return doc_graph_doc_count() > 0
}
Loading