Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
ca3d6b3
WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias →…
briansrls May 18, 2026
6ae63cc
WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias →…
briansrls May 18, 2026
255b776
WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias →…
briansrls May 18, 2026
b1be1b3
WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias →…
briansrls May 18, 2026
ac27cef
WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias →…
briansrls May 18, 2026
85ed607
fix(ci): SG-0 net-shrink append for PR #3280 (+3 hand paths)
briansrls May 18, 2026
35fea3a
fix(lean): ground signed fixed-width Int8–Int64 and ISize for Lean 4.20
briansrls May 18, 2026
9853b70
chore(lean): single-line Symbol twin note (Practice 9)
briansrls May 18, 2026
d29b378
docs(INVARIANTS): P2 receipt for extdeps GroundingMap/Symbol twins
briansrls May 18, 2026
57f87a7
docs(DECISIONS): align #3208 C5 bullet with removed disposition fns
briansrls May 18, 2026
6519a10
fix(extdeps): align lean/machine_code numerics with D2-REV
briansrls May 18, 2026
bdf7e60
chore(extdeps): Practice-9 terse .dag headers; move cpp deferral to D…
briansrls May 18, 2026
8f246e5
fix(machine_code): pin disp32/disp64 width classes per api-review
briansrls May 18, 2026
3987e72
fix(machine_code): v2-bootstrap parse for singleton width-class sums
briansrls May 18, 2026
af1a865
fix: signed-only displacement width, SG-0 path order, Lean ledger map
briansrls May 18, 2026
7b4d502
fix(cpp): C++ lex.key anchor for CppBool + P4-3208 authority receipt
briansrls May 18, 2026
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: 7 additions & 0 deletions INVARIANTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -165,6 +165,10 @@ A canonical accessor exists (e.g., a reflected substrate function), but a second

**Receipt:** Id → declaration lookup once had both a canonical Rust accessor and a parallel `.dag` list-walker that each consumer picked between. Dissolution: add the missing reflected accessor, delete the walker, migrate consumers to the typed accessor — the parallel authority disappeared.

### Interim receipt: `v4.extdeps/languages/*` `compile_to_dag` smokes and `GroundingMap` / `Symbol`

The pinned `compile_to_dag(include_str!(…), path)` integration smokes in §P5(b) (`v4_extdeps_*_dag_smoke_test.rs`) compile **one `.dag` source string in isolation**. On that path the compiler does **not** merge sibling-module bodies for `import v4.extdeps.languages.resolver { … }`, and under **M1(2.7)** `import v4.std.node { Symbol }` is not populated into the declaration table either. Until the smoke harness loads a multi-module **bundle** that includes the shared home or import-lowering closes those gaps, `lean.dag` and `cpp.dag` carry **structural twins** of the ratified `extdeps/languages/resolver.dag` surface (`GroundingMap`, and where needed bodiless `Symbol`), each tagged with a one-line pointer to **DECISIONS.md D4**. `machine_code.dag` keeps the local `Symbol` twin on the same M1(2.7) path but **omits** a `GroundingMap` twin after **D2-REV** (no spelling-only resolver rows on that slice). Treat as **P2-staging**: one named mechanical shape, one dissolution trigger (`resolver.dag` + smoke bundle, or M1(2.7) std-node import), not silent divergent semantics. `rust.dag` continues to import `Symbol` from `v4.std.node` where the full bootstrap path applies.

### Problem shape: Consumer reverse-engineers storage shape

A downstream stage reads a lower layer not through its declared accessors but by traversing its internal storage — walking a list, checking a field convention, matching on a tag. The consumer must evolve in lockstep with the lower layer because storage shape has become part of the contract by accident.
Expand Down Expand Up @@ -351,7 +355,10 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
| `src/v3/compiler/tests/integration/ctrl_pr_digests_dag_smoke_test.rs` | **Project plan:** `docs/r4-ctrl-dag-migration-project-plan.md` §3 — catalog **#8** `dsl/ctrl/pr_digests.dag` (Wave-1 ctrl → `.dag` subsystem modeling). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + the matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke test. **Dissolution:** remove when `compile_to_dag` (or a single generated harness) validates `module … service …` ctrl carrier files end-to-end without a parallel Rust string/lexer ratchet, or when the contract migrates to `.dag` `TestClaim` coverage. **Interim ratchet:** `ctrl_pr_digests_dag_tokenizes_and_matches_expected_surface` requires clean tokenization plus presence of `module ctrl.pr_digests`, `import extdeps.github.pulls { PullRequest, PullReview, ReviewComment }`, `std.errors` / `std.types` imports, the four Practice-4 sum/record carriers (with `🟡 STAGED` / `🟢 TERMINAL` markers per `dsl/ctrl/README.md`), `ReviewCommentBody` + `review_line_comments` wiring, and `service ctrl.PrDigests` / the four `operation` blocks / `readonly`. |
| `src/v3/compiler/tests/integration/extdeps_sql_transport_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row `T-PB-B` / `pb_rust_tests_outside_residual_zero`; this Rust integration receipt keeps HTTP/SQL/audit extdeps compiled by the existing v3 parser before downstream emission-target consumers rely on them. **Dissolution:** remove when extdeps transport and Phase 3 emission-target files are covered by a `.dag`-native parse/authority suite or generated test harness rather than per-file Rust `compile_to_dag` probes. **Interim ratchet:** `rest_transport_dag_compiles_cleanly` and `sql_transport_dag_compiles_cleanly` pin `dsl/extdeps/transports/rest.dag` and `dsl/extdeps/transports/sql.dag`; `http_server_extdep_dag_compiles_cleanly`, `sql_migration_extdep_dag_compiles_cleanly`, and `audit_event_extdep_dag_compiles_cleanly` pin `dsl/extdeps/http/server.dag`, `dsl/extdeps/sql/migration.dag`, and `dsl/extdeps/audit/event.dag` as parseable staged emission-target substrate. The field-sensitive companions (`http_server_target_fields_are_authoritative_substrate_edges`, `sql_migration_target_fields_bound_raw_sql_scaffold`, `audit_event_target_fields_preserve_cloudevents_core_names`) consume the new target-contract fields directly so they fail on raw `String`/`Int` regressions, missing SQL scaffold bounds, or CloudEvents alias drift while the first real projection consumer is still staged; the audit ratchet also locks CloudEvents core fields to branded carriers and `std.types.Timestamp` rather than raw strings. |
| `src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-29 C++ ABI / target data-model feeder (`src/v4/extdeps/cpp_abi.dag`, consumed by T-4 `cpp.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/cpp_abi.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_cpp_abi_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4 C++ language-model lane (`src/v4/extdeps/languages/cpp.dag`, DECISIONS.md D2 / P4-3208 `CppBool` surface). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/languages/cpp.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_cpp_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/v4_extdeps_typescript_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4 typescript language-model lane (`src/v4/extdeps/languages/typescript.dag`, DECISIONS.md D2 resolver slice). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/languages/typescript.dag` (or the v4 extdeps fixture set it belongs to) is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_typescript_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4.13 (`src/v4/extdeps/languages/machine_code.dag`, DECISIONS.md L-3 / P4-3208). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `machine_code.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_machine_code_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** B-2 / DECISIONS.md L-4 (`src/v4/extdeps/languages/lean.dag`, PROOF-1 prover surface / P4-3208). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `lean.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_lean_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs` | **TASKS.md** **T-30** (`src/v4/TASKS.md` — structural hollow-alias / fact-density gate); **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **Spec:** `docs/modeling-discipline.md` **Practice 8** — *Interim floor: the hollow-alias discriminator* (Practice 8 *Interim floor* on `main` post-#3226 `77b9e7d72` + Practice 9 #3234 `125fc88c8`; diff `main` if §8/§9 drift). **P2 / Practice 5:** this smoke is a **parse + inference cleanliness** probe for `src/v4/std/fact_density.dag` only — it does **not** claim a **generated** substrate consumer for `SourceSpecReadFact` (INVARIANTS §P2: declaration without generated consumer = staging; see `STRUCTURE.md`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/std/fact_density.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_std_fact_density_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/file_attachment_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#62** `substrate_gap_file_ingestion_closed` (T-Workflow-As-Data substrate-gap class; worker brief `docs/briefs/r3-substrate-gate-62-file-attachment-carrier-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `FileAttachment` field names + cross-module nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as `timing_lens_substrate_carrier_test.rs` for gate #55). **Interim ratchet:** `file_attachment_shape_locked` + `file_attachment_field_types_locked` + `file_attachment_field_count_is_five` pin the ratified Refined-B-1 five-field subset of `WorkflowObservationAnchor` (`NodeId`, `ContentHash`, `WorkflowProducerId`, `WorkflowRunId`, `Nanoseconds`) exactly as declared in `src/v3/std/timing_lens.dag`; existence proof carrier construction stays in-module as `gate_62_file_attachment_demo_record`. |
| `src/v3/compiler/tests/integration/lens_application_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#89** `section_ref_substrate_landed` (T-Lens-Application-Surface — `SectionRef` disjoint sum over `DeclarationScope` and `NodeScope` in `src/v3/std/lens_application.dag`; design authority `docs/design-lens-application-surface.md` §1.2–§2). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the harness. **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `SectionRef` variant labels, field names, and `DeclarationId` / `NodeId` nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as gate **#62** `file_attachment_substrate_carrier_test.rs`). **Interim ratchet:** `gate_89_section_ref_is_disjoint_sum_from_lens_application_authority` pins variant order (`DeclarationScope` then `NodeScope`) and payload fields to `lens_application.dag`. |
Expand Down
3 changes: 3 additions & 0 deletions scripts/ci-merge/sg0-pr-body-append.3280.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
SG-0 hand-path delta: +3

SG-0 pairing: (c) Net add is three `EXPECTED_HAND_AUTHORED_TEST` rows for v4 extdeps `compile_to_dag` smokes (`v4_extdeps_cpp_dag_smoke_test.rs`, `v4_extdeps_machine_code_dag_smoke_test.rs`, `v4_extdeps_lean_dag_smoke_test.rs`) plus matching INVARIANTS §P5(b) receipt rows per T-PB-B. Dispatch: retire each path when the corresponding `.dag` is exercised only by `.dag` `TestClaim` / generated harness; follow-close tracked in gunbc#3280 (this PR).
6 changes: 6 additions & 0 deletions src/v3/compiler/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -275,6 +275,12 @@ mod timing_lens_substrate_carrier_test;
mod v2_oracle_no_remaining_test_consumers_test;
#[path = "integration/v4_extdeps_cpp_abi_dag_smoke_test.rs"]
mod v4_extdeps_cpp_abi_dag_smoke_test;
#[path = "integration/v4_extdeps_cpp_dag_smoke_test.rs"]
mod v4_extdeps_cpp_dag_smoke_test;
#[path = "integration/v4_extdeps_lean_dag_smoke_test.rs"]
mod v4_extdeps_lean_dag_smoke_test;
#[path = "integration/v4_extdeps_machine_code_dag_smoke_test.rs"]
mod v4_extdeps_machine_code_dag_smoke_test;
#[path = "integration/v4_extdeps_typescript_dag_smoke_test.rs"]
mod v4_extdeps_typescript_dag_smoke_test;
#[path = "integration/v4_lens_cost_dag_smoke_test.rs"]
Expand Down
4 changes: 4 additions & 0 deletions src/v3/compiler/tests/integration/sg0_census_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -829,6 +829,10 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
// source ratchet — no `v2-compiler` crate references outside `src/v2/`.
"src/v3/compiler/tests/integration/v2_oracle_no_remaining_test_consumers_test.rs",
"src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs",
"src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs",
// T-4.13 / B-2: `compile_to_dag` smoke on `machine_code.dag` / `lean.dag` (zero module diagnostics).
"src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs",
"src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs",
// T-4 TypeScript primitive scaffold: `compile_to_dag` smoke on
// `src/v4/extdeps/languages/typescript.dag` (zero module diagnostics).
// SG-0 ratchet per INVARIANTS §P5(b) + `extdeps_sql_transport_test` precedent.
Expand Down
26 changes: 26 additions & 0 deletions src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//! **Layer:** integration
//!
//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/cpp.dag` — T-4 C++
//! LanguageModel D2-resolver slice must lower+infer with **zero** module diagnostics.

use v3_compiler::compile_to_dag;
use v3_compiler::CompileError;

const CPP_DAG: &str = include_str!("../../../../v4/extdeps/languages/cpp.dag");
const CPP_PATH: &str = "src/v4/extdeps/languages/cpp.dag";

#[test]
fn v4_extdeps_cpp_dag_compiles() {
match compile_to_dag(CPP_DAG, CPP_PATH) {
Ok(dag) => assert!(
dag.diagnostics().is_empty(),
"{CPP_PATH}: expected empty diagnostics, got {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(CompileError::Semantic(dag)) => panic!(
"{CPP_PATH}: semantic errors: {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(other) => panic!("{CPP_PATH}: {other:?}"),
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//! **Layer:** integration
//!
//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/lean.dag` — B-2 / L-4
//! Lean LanguageModel must lower+infer with **zero** module diagnostics.

use v3_compiler::compile_to_dag;
use v3_compiler::CompileError;

const LEAN_DAG: &str = include_str!("../../../../v4/extdeps/languages/lean.dag");
const LEAN_PATH: &str = "src/v4/extdeps/languages/lean.dag";

#[test]
fn v4_extdeps_lean_dag_compiles() {
match compile_to_dag(LEAN_DAG, LEAN_PATH) {
Ok(dag) => assert!(
dag.diagnostics().is_empty(),
"{LEAN_PATH}: expected empty diagnostics, got {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(CompileError::Semantic(dag)) => panic!(
"{LEAN_PATH}: semantic errors: {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(other) => panic!("{LEAN_PATH}: {other:?}"),
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//! **Layer:** integration
//!
//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/machine_code.dag` —
//! T-4.13 machine-code model must lower+infer with **zero** module diagnostics.

use v3_compiler::compile_to_dag;
use v3_compiler::CompileError;

const MACHINE_CODE_DAG: &str = include_str!("../../../../v4/extdeps/languages/machine_code.dag");
const MACHINE_CODE_PATH: &str = "src/v4/extdeps/languages/machine_code.dag";

#[test]
fn v4_extdeps_machine_code_dag_compiles() {
match compile_to_dag(MACHINE_CODE_DAG, MACHINE_CODE_PATH) {
Ok(dag) => assert!(
dag.diagnostics().is_empty(),
"{MACHINE_CODE_PATH}: expected empty diagnostics, got {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(CompileError::Semantic(dag)) => panic!(
"{MACHINE_CODE_PATH}: semantic errors: {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(other) => panic!("{MACHINE_CODE_PATH}: {other:?}"),
}
}
Loading
Loading