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
2 changes: 1 addition & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ The test that an edit actually *reduced* redundancy rather than moving it: **net
Minimization holds only if each fact lives in exactly one place. The recurring violation is **nicknaming — a second name for one concept** — which duplicates work at the meaning layer and, since we generate from concepts, duplicates it again in everything derived (testgen, emit, lenses). A fork always gets consolidated later, so it is a correctness concern, not a style one. We cannot enforce this programmatically yet; until then it is diligence — faithfully model the accepted universal frameworks (classical logic, set theory, algebra), and in `extdeps/` the real upstream spec (cite the source, keep its real names, declare its version, model what the API actually returns), rather than re-coining them. Corollaries: the layer DAG is strict (`std ← extdeps ← compiler ← workflow`, imports point toward std); a fact's home is its *layer*, not its file (paths are discriminators, not gospel); below-boundary representation is opaque (the rename test). A direct consequence for `extdeps/` service operations, three separable facts that must not be fused into one row: (a) the **interface shape** — the dependency's parameterized contract (inputs → outputs, exit/error semantics) — is what extdeps owns; (b) the **transport** (shell / REST / SDK) is a §2 Realization *handler* bound to that shape, *one of N*, not a fact about the dependency — a single hardwired transport is the §4 N×M-adapter trap (`git diff` argv models the git CLI, a nickname for git's diff *semantics*; libgit2 and the compare API are the other handlers); (c) **business policy** (which base ref, which flag, an idempotency protocol the dependency doesn't provide) is a *workflow* fact and modeling it in extdeps is a layer inversion (extdeps depending upward). The tell that (c) has leaked is an argv carrying a literal it should receive as a parameter (`origin/main...HEAD`, `--all-targets`); the tell that (b) has fused is the same operation forked once per transport (GCP's OAuth2 refresh modeled three ways) instead of one shape with N bound handlers. Scaffolded by `v2.lens.extdeps_shape_transport_policy`: lens-unit +/- on synthetic fact rows; corpus RED witnesses execute against live `dag/extdeps/**` via `filesystem_read` (dissolve-on: Node-tree argv projection supersedes text scan). This holds at *any* interface↔realization seam, not only service ops: the cited data behind an agnostic std surface de-fuses exactly as a transport does, and its directional reading is the same — the *dispatch* that selects a realization is itself realization, so it sits peripheral (`extdeps/`), never in the interface (a §2 pure-spec is dispatch-free; a std projection that *matched* over its realizations would have to name them, inverting the import arrow above). What migrates outward is each realization's grounded specifics — cited rows, *or* a per-OS taxonomy reduced to the shape — together with the dispatch; only the agnostic shape stays central. A std type that privileged one realization's taxonomy (POSIX `st_mode` over the `Ntfs`/`Apfs` that `FileSystemSemantics` already enumerates) is itself that inversion.

- *e.g.* `CpuArchitecture` and `TargetArchitecture` are byte-identical enums (the latter's header denies the parallel it declares); `ModulePath` was a nickname for `QualifiedName` (renamed, `ModulePathSegment` deleted); one "vendor" concept once forked three ways by rigor — `CpuVendor`/`DramManufacturer` closed enums vs `GpuFacts.vendor` stringly — now dissolved into a single generic `Vendor<Domain>` whose cited company entities live one-file-each in `extdeps/vendor/` (referencing a company *grounds* it as a real upstream entity with its legal name, not a minted enum nickname; the domain is a type argument, so `Vendor<Hardware>` is the §2-horizontal "one concept, every breadth"). Counter-example done right: a CPU/DRAM model is a hardware *domain* model, not a universal framework, so its catalog *shape* lives downstream of std in `extdeps/{cpu,memory}` beside its cited vendor rows (`extdeps/cpu/ampere`) — std keeps only the frameworks they build on (`measure`, `types`); `compute_fabric` is a product-layer domain model. Likewise `std/os.dag` projects per-vendor rows with no `match` ("projection only"), while the cited rows and the product→vendor dispatch (`cited_operating_system_surface`) live in `extdeps/os/{ubuntu,windows,macos,os}.dag` ("dispatch lives in extdeps/, not std/", promoted from that hub header).
- **§3 convergence thread — fnv1a64 dual surface:** `v1.compiler.dag_collect_support.dag_node_surface_fingerprint_rec` calls the raw v1 intrinsics `atom_identity_hash`/`hash_combine` (fnv1a64 primitives registered in `04_method.dag` builtins); `std.content_hash` (v2 layer) is the modeled surface over the same underlying authority. These are two surfaces on one concept, not two authorities. The unifying home is a grounded std type once the v2 content-hash carrier is inhabited — tracked here so the fork does not widen into a third surface. Dissolution: ground `v1.compiler.dag_collect_support` fingerprint calls through `std.content_hash` when v2 adoption for this stage is cleared.
- **§3 convergence thread — fnv1a64 dual surface:** `v1.compiler.dag_collect_support.dag_node_surface_fingerprint_rec` calls the raw v1 intrinsics `atom_identity_hash`/`hash_combine` (fnv1a64 primitives registered in `04_method.dag` builtins); `std.content_hash` is the modeled surface over the same underlying authority. **LANDED (v2 carrier):** `v2.std.node.Hash = std.types.ContentHash`; `content_hash`/`combine_hash`/`symbol_identity_digest` route through `std.content_hash`; `v2.std.materialize` keys on `ContentHash` (same identity as `RealizationPlan.target`). Remaining: ground `v1.compiler.dag_collect_support` fingerprint calls through `std.content_hash` when v1-stage v2 adoption clears.

## 4. The closed, grounded substrate (what makes §2–§3 decidable)

Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/design_document.dag
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ fn section_3_blocks() -> List<MarkdownBlock> {
p(text: "Minimization holds only if each fact lives in exactly one place. The recurring violation is **nicknaming — a second name for one concept** — which duplicates work at the meaning layer and, since we generate from concepts, duplicates it again in everything derived (testgen, emit, lenses). A fork always gets consolidated later, so it is a correctness concern, not a style one. We cannot enforce this programmatically yet; until then it is diligence — faithfully model the accepted universal frameworks (classical logic, set theory, algebra), and in `extdeps/` the real upstream spec (cite the source, keep its real names, declare its version, model what the API actually returns), rather than re-coining them. Corollaries: the layer DAG is strict (`std ← extdeps ← compiler ← workflow`, imports point toward std); a fact's home is its *layer*, not its file (paths are discriminators, not gospel); below-boundary representation is opaque (the rename test). A direct consequence for `extdeps/` service operations, three separable facts that must not be fused into one row: (a) the **interface shape** — the dependency's parameterized contract (inputs → outputs, exit/error semantics) — is what extdeps owns; (b) the **transport** (shell / REST / SDK) is a §2 Realization *handler* bound to that shape, *one of N*, not a fact about the dependency — a single hardwired transport is the §4 N×M-adapter trap (`git diff` argv models the git CLI, a nickname for git's diff *semantics*; libgit2 and the compare API are the other handlers); (c) **business policy** (which base ref, which flag, an idempotency protocol the dependency doesn't provide) is a *workflow* fact and modeling it in extdeps is a layer inversion (extdeps depending upward). The tell that (c) has leaked is an argv carrying a literal it should receive as a parameter (`origin/main...HEAD`, `--all-targets`); the tell that (b) has fused is the same operation forked once per transport (GCP's OAuth2 refresh modeled three ways) instead of one shape with N bound handlers. Scaffolded by `v2.lens.extdeps_shape_transport_policy`: lens-unit +/- on synthetic fact rows; corpus RED witnesses execute against live `dag/extdeps/**` via `filesystem_read` (dissolve-on: Node-tree argv projection supersedes text scan). This holds at *any* interface↔realization seam, not only service ops: the cited data behind an agnostic std surface de-fuses exactly as a transport does, and its directional reading is the same — the *dispatch* that selects a realization is itself realization, so it sits peripheral (`extdeps/`), never in the interface (a §2 pure-spec is dispatch-free; a std projection that *matched* over its realizations would have to name them, inverting the import arrow above). What migrates outward is each realization's grounded specifics — cited rows, *or* a per-OS taxonomy reduced to the shape — together with the dispatch; only the agnostic shape stays central. A std type that privileged one realization's taxonomy (POSIX `st_mode` over the `Ntfs`/`Apfs` that `FileSystemSemantics` already enumerates) is itself that inversion."),
ul(items: [
li(text: "*e.g.* `CpuArchitecture` and `TargetArchitecture` are byte-identical enums (the latter's header denies the parallel it declares); `ModulePath` was a nickname for `QualifiedName` (renamed, `ModulePathSegment` deleted); one \"vendor\" concept once forked three ways by rigor — `CpuVendor`/`DramManufacturer` closed enums vs `GpuFacts.vendor` stringly — now dissolved into a single generic `Vendor<Domain>` whose cited company entities live one-file-each in `extdeps/vendor/` (referencing a company *grounds* it as a real upstream entity with its legal name, not a minted enum nickname; the domain is a type argument, so `Vendor<Hardware>` is the §2-horizontal \"one concept, every breadth\"). Counter-example done right: a CPU/DRAM model is a hardware *domain* model, not a universal framework, so its catalog *shape* lives downstream of std in `extdeps/\{cpu,memory\}` beside its cited vendor rows (`extdeps/cpu/ampere`) — std keeps only the frameworks they build on (`measure`, `types`); `compute_fabric` is a product-layer domain model. Likewise `std/os.dag` projects per-vendor rows with no `match` (\"projection only\"), while the cited rows and the product→vendor dispatch (`cited_operating_system_surface`) live in `extdeps/os/\{ubuntu,windows,macos,os\}.dag` (\"dispatch lives in extdeps/, not std/\", promoted from that hub header)."),
li(text: "**§3 convergence thread — fnv1a64 dual surface:** `v1.compiler.dag_collect_support.dag_node_surface_fingerprint_rec` calls the raw v1 intrinsics `atom_identity_hash`/`hash_combine` (fnv1a64 primitives registered in `04_method.dag` builtins); `std.content_hash` (v2 layer) is the modeled surface over the same underlying authority. These are two surfaces on one concept, not two authorities. The unifying home is a grounded std type once the v2 content-hash carrier is inhabited — tracked here so the fork does not widen into a third surface. Dissolution: ground `v1.compiler.dag_collect_support` fingerprint calls through `std.content_hash` when v2 adoption for this stage is cleared."),
li(text: "**§3 convergence thread — fnv1a64 dual surface:** `v1.compiler.dag_collect_support.dag_node_surface_fingerprint_rec` calls the raw v1 intrinsics `atom_identity_hash`/`hash_combine` (fnv1a64 primitives registered in `04_method.dag` builtins); `std.content_hash` is the modeled surface over the same underlying authority. **LANDED (v2 carrier):** `v2.std.node.Hash = std.types.ContentHash`; `content_hash`/`combine_hash`/`symbol_identity_digest` route through `std.content_hash`; `v2.std.materialize` keys on `ContentHash` (same identity as `RealizationPlan.target`). Remaining: ground `v1.compiler.dag_collect_support` fingerprint calls through `std.content_hash` when v1-stage v2 adoption clears."),
]),
]
}
Expand Down
39 changes: 36 additions & 3 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13534,8 +13534,6 @@ mod reference_edge_producer_tests {
// when exhaustiveness-by-default / compile-graph access lands (gunbc#5364).

const NON_FOLD_RESIDUE_ROSTER: &[&str] = &[
"dag/extdeps/bmc/webui/nbd_proxy_serve.dag::shell_command_leading_lit_text",
"dag/extdeps/bmc/webui/nbd_proxy_serve.dag::shell_rawline_starts_with_tool",
// 2026-07-13 backfill: #6533 (Wave 2 frontier probe) landed this site unrostered — the nfr
// witnesses are corpus-read host-fed rows the affected-set selection did not run for that
// diff, so the red surfaced on the next whole-corpus cold sweep, not on the landing PR
Expand Down Expand Up @@ -13564,6 +13562,12 @@ const NON_FOLD_RESIDUE_ROSTER: &[&str] = &[
// the std eq rows; dissolve with derived equality from inhabitance (dag/std/algebra).
"src/v2/lens/live_read_classification.dag::live_read_carrier_eq",
"src/v2/lens/live_read_classification.dag::path_pattern_eq",
// 2026-07-15 backfill: #6680 merge landed bash_composition_recognizer.dag::apply_role
// with a two-special-variant dispatch (IfFraming / UnmodeledKeyword mutate ScanState;
// every other TokenRole through close_run unchanged). The nfr witness is corpus-read;
// the landing PR predict-skipped it and the red surfaced on the next cold sweep. Burns
// down with the bash composition recognizer fold migration.
"src/v2/lens/bash_composition_recognizer.dag::apply_role",
// 2026-07-12 backfill: sites that landed unrostered while the gate was red during the
// land-red-with-local-proof era (revoked 2026-07-12). Declared here so the ratchet
// re-arms; each burns down with its owning file's fold migration.
Expand Down Expand Up @@ -13636,7 +13640,6 @@ const NON_FOLD_RESIDUE_ROSTER: &[&str] = &[
"src/v2/compiler/05_eval.dag::run_test_claim_assert_decided",
"src/v2/compiler/05_eval.dag::run_test_claim_runtime_assert",
"src/v2/compiler/06_translate.dag::translate_algebra_finalize",
"src/v2/compiler/emit_host.dag::run_test_claim_emit_vs_eval_verdict",
"src/v2/compiler/emit_host.dag::runtime_value_signed_i32_le_as_int",
"src/v2/compiler/self_host/frontier_probe_types.dag::frontier_blocker_class_matches",
"src/v2/test/claim/manual/eval_runtime.dag::eval_arg_is_two_literal",
Expand Down Expand Up @@ -14078,6 +14081,36 @@ mod nfr_tests {
);
}

#[test]
fn nfr_roster_receipt() {
let live: std::collections::BTreeSet<&str> = nfr_build_report()
.sites
.iter()
.map(|s| s.as_str())
.collect();
eprintln!(
"nfr_roster_receipt: unrostered={} stale={} live={}",
non_fold_residue_unrostered_count(),
non_fold_residue_stale_roster_count(),
live.len()
);
for site in nfr_build_report().sites.iter() {
if !non_fold_residue_site_is_rostered(site) {
eprintln!("unrostered live site: {site}");
}
assert!(
non_fold_residue_site_is_rostered(site),
"unrostered: {site}"
);
}
for entry in NON_FOLD_RESIDUE_ROSTER {
if !live.contains(entry) {
eprintln!("stale roster entry: {entry}");
}
assert!(live.contains(entry), "stale roster: {entry}");
}
}

#[test]
fn green_control_wildcard_over_open_domain_is_not_residue() {
let f = files(&[(
Expand Down
1 change: 1 addition & 0 deletions src/v2/lens/inert_carrier.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ data inert_carrier_roster: List<String> = [
"FloorWitnessRow",
"FreeOutput",
"GitCliReportedVersion",
"LocalAlias",
"ProcMeminfo",
"ReactHookSite",
"SystemdUnitStatus"
Expand Down
15 changes: 8 additions & 7 deletions src/v2/std/materialize.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module v2.std.materialize

import v2.std.node { Node, Hash, content_hash, node_subtree_nodes }
import std.types { ContentHash }
import v2.std.node { Node, content_hash, node_subtree_nodes }
import std.realization { Materialization, Recompute, Memoize, Share }
import v2.std.algebra { any, fold_list, length, list_snoc_item }
import v2.std.collection { List }
Expand All @@ -10,14 +11,14 @@ import v2.std.integer { Int }
data materialize_module_note: String = "materialize is the spine's Recompute|Memoize|Share qualification step (execution-spine-design.md §2; run ≜ realize ∘ materialize ∘ dependency_view). It is the content-hash GENERALIZATION of dag/std/realization.reconcile: reconcile keys collapse on the effect-pairwise create_double_init_collapsible predicate over RealizedStep effects; materialize keys on content_hash over EVERY subtree Node, so content-identical subgraphs that a tree-fold would recompute once-per-parent are marked Share (computed once). This is Half B of the duplicate-work design (duplicate-work-graph-lens-design.md): duplication = N materializations of one computation-identity with no Share. Occurrence-independent content_hash IS the identity (src/v2/std/node.dag); node_subtree_nodes enumerates the whole DAG. MVP scope: structural identity only (ComputationIdentity.StructurallyIdentical, the decidable wall); the effect-idempotency safety gate (D3) and cost floor (D4) layer on next. Actual runtime Share (compute-once execution) is realized by emit-on-demand native artifacts (Share by content-hash), NOT by parallelizing the interpreter — the Rc→Arc gate is removed (ROADMAP §④; execution-spine-design.md reconciliation 2026-07-10, operator-signed); this analysis-side materialize lands now."

type MaterializedNode {
hash: Hash
hash: ContentHash
materialization: Materialization
}

data empty_materialized: List<MaterializedNode> = []
data empty_hashes: List<Hash> = []
data empty_hashes: List<ContentHash> = []

fn materialized_mark_peers_share(acc: List<MaterializedNode>, h: Hash) -> List<MaterializedNode> {
fn materialized_mark_peers_share(acc: List<MaterializedNode>, h: ContentHash) -> List<MaterializedNode> {
fold_list(
xs: acc,
empty: empty_materialized,
Expand All @@ -31,7 +32,7 @@ fn materialized_mark_peers_share(acc: List<MaterializedNode>, h: Hash) -> List<M
)
}

fn materialized_has_peer(acc: List<MaterializedNode>, h: Hash) -> Bool {
fn materialized_has_peer(acc: List<MaterializedNode>, h: ContentHash) -> Bool {
any(xs: acc, predicate: fn(e) { e.hash == h })
}

Expand Down Expand Up @@ -63,11 +64,11 @@ fn materialization_is_share(m: Materialization) -> Bool {
}
}

fn hashes_contain(hs: List<Hash>, h: Hash) -> Bool {
fn hashes_contain(hs: List<ContentHash>, h: ContentHash) -> Bool {
any(xs: hs, predicate: fn(x) { x == h })
}

fn distinct_hashes(root: Node) -> List<Hash> {
fn distinct_hashes(root: Node) -> List<ContentHash> {
fold_list(
xs: node_subtree_nodes(root: root),
empty: empty_hashes,
Expand Down
Loading
Loading