From ca3d6b3f4b5cc43b6da263bba2e49fd13a6bb045 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 02:06:00 -0400 Subject: [PATCH 01/16] =?UTF-8?q?WIP:=20D2=20cleanup=20ASAP=20=E2=80=94=20?= =?UTF-8?q?#3208=20lean.dag=20+=20machine=5Fcode.dag=20bare-alias=20?= =?UTF-8?q?=E2=86=92=20fact-bu?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/extdeps/languages/lean.dag | 75 +++++++++++++-- src/v4/extdeps/languages/machine_code.dag | 106 +++++++++++++++++++--- 2 files changed, 156 insertions(+), 25 deletions(-) diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index 2904b79cf99..e0bcf65a014 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -1,8 +1,8 @@ // src/v4/extdeps/languages/lean.dag // Scope: Lean 4 language model for PROOF-1 termination export. -// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, LeanBool, LeanNat, LeanInt, LeanUSize, LeanUInt8, LeanUInt16, LeanUInt32, LeanUInt64. +// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, LeanKernelInductiveBoolWitness, LeanNatMathematicalUnboundedWitness, LeanIntMathematicalUnboundedWitness, LeanPointerSizedNaturalPerTargetWitness, LeanUnsignedFixedWidthModularWitness, LeanUInt8Width8Witness, LeanUInt16Width16Witness, LeanUInt32Width32Witness, LeanUInt64Width64Witness, LeanBool, LeanNat, LeanInt, LeanUSize, LeanUInt8, LeanUInt16, LeanUInt32, LeanUInt64. // Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, Symbol. -// Status: D2-hard-held; fact-bundle rework gated. +// Status: D2-REV — Lean 4 kernel / fixed-precision primitives as fact-bundles (DECISIONS.md P4-3208 / #3208). module v4.extdeps.languages.lean @@ -198,12 +198,67 @@ type LeanProofCheckSemantics { } +// Ledger: DECISIONS.md D2-REV + P4-3208 — Lean 4 kernel / fixed-precision +// numeric carriers as fact-bundles (spec witnesses + std `canon`), not bare aliases. // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanBool = Bool -type LeanNat = Nat -type LeanInt = Int -type LeanUSize = UIntPlatform -type LeanUInt8 = UInt8 -type LeanUInt16 = UInt16 -type LeanUInt32 = UInt32 -type LeanUInt64 = UInt64 +type LeanKernelInductiveBoolWitness {} + +type LeanBool { + canon: Bool + kernel_form: LeanKernelInductiveBoolWitness +} + +type LeanNatMathematicalUnboundedWitness {} + +type LeanNat { + canon: Nat + specification: LeanNatMathematicalUnboundedWitness +} + +type LeanIntMathematicalUnboundedWitness {} + +type LeanInt { + canon: Int + specification: LeanIntMathematicalUnboundedWitness +} + +type LeanPointerSizedNaturalPerTargetWitness {} + +type LeanUSize { + canon: UIntPlatform + specification: LeanPointerSizedNaturalPerTargetWitness +} + +type LeanUnsignedFixedWidthModularWitness {} + +type LeanUInt8Width8Witness {} + +type LeanUInt8 { + modular_semantics: LeanUnsignedFixedWidthModularWitness + width: LeanUInt8Width8Witness + canon: UInt8 +} + +type LeanUInt16Width16Witness {} + +type LeanUInt16 { + modular_semantics: LeanUnsignedFixedWidthModularWitness + width: LeanUInt16Width16Witness + canon: UInt16 +} + +type LeanUInt32Width32Witness {} + +type LeanUInt32 { + modular_semantics: LeanUnsignedFixedWidthModularWitness + width: LeanUInt32Width32Witness + canon: UInt32 +} + +type LeanUInt64Width64Witness {} + +type LeanUInt64 { + modular_semantics: LeanUnsignedFixedWidthModularWitness + width: LeanUInt64Width64Witness + canon: UInt64 +} diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index 13db8bed9b7..c8a3f02bbcf 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -1,8 +1,8 @@ // src/v4/extdeps/languages/machine_code.dag // Scope: machine-code language model parameterized by Isa. -// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition, MachineI8, MachineI16, MachineI32, MachineI64, MachineI128, MachineU8, MachineU16, MachineU32, MachineU64, MachineU128. +// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, MachineIsaSignedTwoComplementFixedWidthWitness, MachineSignedWordWidth8Witness, MachineSignedWordWidth16Witness, MachineSignedWordWidth32Witness, MachineSignedWordWidth64Witness, MachineSignedWordWidth128Witness, MachineIsaUnsignedModuloTwoPowWidthWitness, MachineUnsignedWordWidth8Witness, MachineUnsignedWordWidth16Witness, MachineUnsignedWordWidth32Witness, MachineUnsignedWordWidth64Witness, MachineUnsignedWordWidth128Witness, MachineI8, MachineI16, MachineI32, MachineI64, MachineI128, MachineU8, MachineU16, MachineU32, MachineU64, MachineU128, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. // Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, Symbol. -// Status: D2-hard-held; fact-bundle rework gated. +// Status: D2-REV — ISA primitive integers as fact-bundles (DECISIONS.md P4-3208 / #3208). module v4.extdeps.languages.machine_code @@ -60,6 +60,95 @@ type OperandFieldWidthRef { } +// Ledger: DECISIONS.md D2-REV + P4-3208 — ISA-modeled fixed-width integers as +// fact-bundles (width + representation + std `canon`), not bare std aliases. +// Anchor: Intel SDM (two's-complement fixed-width general-purpose integer reads); +// Arm A-profile Architecture Reference Manual; RISC-V ISA manual (two's complement). +type MachineIsaSignedTwoComplementFixedWidthWitness {} + +type MachineSignedWordWidth8Witness {} + +type MachineSignedWordWidth16Witness {} + +type MachineSignedWordWidth32Witness {} + +type MachineSignedWordWidth64Witness {} + +type MachineSignedWordWidth128Witness {} + +type MachineIsaUnsignedModuloTwoPowWidthWitness {} + +type MachineUnsignedWordWidth8Witness {} + +type MachineUnsignedWordWidth16Witness {} + +type MachineUnsignedWordWidth32Witness {} + +type MachineUnsignedWordWidth64Witness {} + +type MachineUnsignedWordWidth128Witness {} + +type MachineI8 { + representation: MachineIsaSignedTwoComplementFixedWidthWitness + width: MachineSignedWordWidth8Witness + canon: Int8 +} + +type MachineI16 { + representation: MachineIsaSignedTwoComplementFixedWidthWitness + width: MachineSignedWordWidth16Witness + canon: Int16 +} + +type MachineI32 { + representation: MachineIsaSignedTwoComplementFixedWidthWitness + width: MachineSignedWordWidth32Witness + canon: Int32 +} + +type MachineI64 { + representation: MachineIsaSignedTwoComplementFixedWidthWitness + width: MachineSignedWordWidth64Witness + canon: Int64 +} + +type MachineI128 { + representation: MachineIsaSignedTwoComplementFixedWidthWitness + width: MachineSignedWordWidth128Witness + canon: Int128 +} + +type MachineU8 { + representation: MachineIsaUnsignedModuloTwoPowWidthWitness + width: MachineUnsignedWordWidth8Witness + canon: UInt8 +} + +type MachineU16 { + representation: MachineIsaUnsignedModuloTwoPowWidthWitness + width: MachineUnsignedWordWidth16Witness + canon: UInt16 +} + +type MachineU32 { + representation: MachineIsaUnsignedModuloTwoPowWidthWitness + width: MachineUnsignedWordWidth32Witness + canon: UInt32 +} + +type MachineU64 { + representation: MachineIsaUnsignedModuloTwoPowWidthWitness + width: MachineUnsignedWordWidth64Witness + canon: UInt64 +} + +type MachineU128 { + representation: MachineIsaUnsignedModuloTwoPowWidthWitness + width: MachineUnsignedWordWidth128Witness + canon: UInt128 +} + + // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟡 feature:fixed-cardinality-width-carrier — DECISIONS.md P4-3208 type InstructionWord @@ -275,16 +364,3 @@ type FlagWriteDisposition | WritesArchitecturalFlags | WritesPredicateRegister - -// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html -type MachineI8 = Int8 -type MachineI16 = Int16 -type MachineI32 = Int32 -type MachineI64 = Int64 -type MachineI128 = Int128 - -type MachineU8 = UInt8 -type MachineU16 = UInt16 -type MachineU32 = UInt32 -type MachineU64 = UInt64 -type MachineU128 = UInt128 From 6ae63ccc8fd01954272673bd4f2f956ca15a5fa5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 02:10:33 -0400 Subject: [PATCH 02/16] =?UTF-8?q?WIP:=20D2=20cleanup=20ASAP=20=E2=80=94=20?= =?UTF-8?q?#3208=20lean.dag=20+=20machine=5Fcode.dag=20bare-alias=20?= =?UTF-8?q?=E2=86=92=20fact-bu?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- INVARIANTS.md | 2 + src/v3/compiler/tests/integration.rs | 4 + .../tests/integration/sg0_census_test.rs | 3 + .../v4_extdeps_lean_dag_smoke_test.rs | 26 ++++ .../v4_extdeps_machine_code_dag_smoke_test.rs | 26 ++++ src/v4/DECISIONS.md | 6 + src/v4/extdeps/languages/lean.dag | 108 +++++++++------ src/v4/extdeps/languages/machine_code.dag | 129 +++++++++--------- 8 files changed, 201 insertions(+), 103 deletions(-) create mode 100644 src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs create mode 100644 src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs diff --git a/INVARIANTS.md b/INVARIANTS.md index 8b641a1cda0..8ae852141e8 100644 --- a/INVARIANTS.md +++ b/INVARIANTS.md @@ -352,6 +352,8 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX | `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_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`. | diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 1babdf7e17c..d35d690518e 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -275,6 +275,10 @@ 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_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"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index e13a811cd7b..d16e3459161 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -833,6 +833,9 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ // `src/v4/extdeps/languages/typescript.dag` (zero module diagnostics). // SG-0 ratchet per INVARIANTS §P5(b) + `extdeps_sql_transport_test` precedent. "src/v3/compiler/tests/integration/v4_extdeps_typescript_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_machine_code_dag_smoke_test.rs", + "src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs", // T-30: `compile_to_dag` smoke on `src/v4/std/fact_density.dag` (Practice 8 // structural mirror in `v4_hollow_alias_gate`). SG-0 + INVARIANTS §P5(b) receipt. "src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs", diff --git a/src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs new file mode 100644 index 00000000000..136992035c4 --- /dev/null +++ b/src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs @@ -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::>() + ), + Err(CompileError::Semantic(dag)) => panic!( + "{LEAN_PATH}: semantic errors: {:?}", + dag.diagnostics().iter().collect::>() + ), + Err(other) => panic!("{LEAN_PATH}: {other:?}"), + } +} diff --git a/src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs new file mode 100644 index 00000000000..e59df6dd3d1 --- /dev/null +++ b/src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs @@ -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::>() + ), + Err(CompileError::Semantic(dag)) => panic!( + "{MACHINE_CODE_PATH}: semantic errors: {:?}", + dag.diagnostics().iter().collect::>() + ), + Err(other) => panic!("{MACHINE_CODE_PATH}: {other:?}"), + } +} diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 6a908a07098..66fe2b60b49 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -241,6 +241,9 @@ checked against the Practice-4 five-pattern ledger: | `LeanProofArtifact` | 🟢 GREEN terminal | All five dissolution patterns fail: proof exporter/emitter share the classifier; theorem and terminating-definition artifacts carry different required fields; not algebra; one artifact is theorem proof or terminating-definition proof; payloads are heterogeneous. | | `LeanFidelityFeature` | 🟢 GREEN terminal | All five dissolution patterns fail: C5 boundary and generic walker share feature classes; `Symbol` would make the boundary open; not algebra; one boundary decision names one feature; feature classes are heterogeneous. | | `LeanFidelityDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: modeled/normalized/fail-closed is the shared C5 disposition; non-modeled variants carry feature payloads and a flat record admits impossible combinations; not algebra; one feature has one disposition; payloads are heterogeneous. | +| `LeanIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` (`rust.dag`, DECISIONS.md Part 6 / CP-3229): signed vs unsigned is a closed external alternative for fixed-precision scalars, not a hideable coordinate; not algebra; not one `F` family over identical payloads. | +| `LeanIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` (`rust.dag`): closed width ladder for fixed-precision scalars; `Pointer` names platform-sized facts separately from fixed bit widths; not algebra; not a `Symbol` tag. | +| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling. | ### `src/v4/extdeps/languages/machine_code.dag` @@ -262,6 +265,9 @@ checked against the Practice-4 five-pattern ledger: | `MachineFidelityDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: modeled/normalized/fail-closed is the shared C5 disposition; non-modeled variants carry feature payloads and a flat record admits impossible combinations; not algebra; one feature has one disposition; payloads are heterogeneous. | | `MachineIntegerOverflowBehavior` | 🟢 GREEN terminal | All five dissolution patterns fail: integer operation semantics/lowering read overflow behavior; `Bool` cannot distinguish wrap/trap/undefined; wrapping relates to fixed-width carrier behavior but trap/undefined are target operation semantics; overflow is separate from flag writes; alternatives are closed. | | `FlagWriteDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: condition-code dependency consumers read this coordinate; `Bool` cannot distinguish architectural flags vs predicate-register writes; not algebra; one instruction has one flag-write disposition; alternatives are closed. | +| `MachineIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` / `LeanIntKind`: ISA-modeled signed vs unsigned is a closed alternative for fixed-width machine integers, not a coordinate; not algebra; consumers branch uniformly. | +| `MachineIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` / `LeanIntWidth` with `Bits128` extension: closed width ladder for ISA fixed-width integers through 128-bit class; not algebra; not a `Symbol` width tag. | +| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts; per-width `MachineI*` / `MachineU*` aliases + `machine_*_grounding` rows cite std ladder coincidence separately (Practice 8). | ## OS-1 — #3209 Coproduct Dissolution And Scaffold Record diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index e0bcf65a014..a66e401cd3b 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -1,12 +1,13 @@ // src/v4/extdeps/languages/lean.dag // Scope: Lean 4 language model for PROOF-1 termination export. -// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, LeanKernelInductiveBoolWitness, LeanNatMathematicalUnboundedWitness, LeanIntMathematicalUnboundedWitness, LeanPointerSizedNaturalPerTargetWitness, LeanUnsignedFixedWidthModularWitness, LeanUInt8Width8Witness, LeanUInt16Width16Witness, LeanUInt32Width32Witness, LeanUInt64Width64Witness, LeanBool, LeanNat, LeanInt, LeanUSize, LeanUInt8, LeanUInt16, LeanUInt32, LeanUInt64. -// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, Symbol. -// Status: D2-REV — Lean 4 kernel / fixed-precision primitives as fact-bundles (DECISIONS.md P4-3208 / #3208). +// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. +// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, Symbol, String; v4.extdeps.languages.rust (GroundingMap). +// Status: D2-REV / Practice 8 — scalar ladder `LeanScalar` + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.lean +import v4.extdeps.languages.rust { GroundingMap } import v4.std.integer { Int, UInt8, @@ -19,6 +20,7 @@ import v4.std.collection { List } import v4.std.logic { Bool } import v4.std.nat { Nat } import v4.std.node { Symbol } +import v4.std.text { String } // Anchor: https://lean-lang.org/doc/reference/4.20.0/ @@ -198,67 +200,89 @@ type LeanProofCheckSemantics { } -// Ledger: DECISIONS.md D2-REV + P4-3208 — Lean 4 kernel / fixed-precision -// numeric carriers as fact-bundles (spec witnesses + std `canon`), not bare aliases. // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanKernelInductiveBoolWitness {} +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type LeanIntKind + = Signed + | Unsigned + -type LeanBool { - canon: Bool - kernel_form: LeanKernelInductiveBoolWitness +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type LeanIntWidth + = Bits8 + | Bits16 + | Bits32 + | Bits64 + | Pointer + + +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type LeanScalar + = IntScalar { kind: LeanIntKind, width: LeanIntWidth } + | BoolScalar + + +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanBool = Bool + +data lean_bool_grounding: GroundingMap = GroundingMap { + spelling: "Bool" } -type LeanNatMathematicalUnboundedWitness {} -type LeanNat { - canon: Nat - specification: LeanNatMathematicalUnboundedWitness +// Anchor: https://lean-lang.org/doc/reference/4.20.0/ +type LeanNat = Nat + +data lean_nat_grounding: GroundingMap = GroundingMap { + spelling: "Nat" } -type LeanIntMathematicalUnboundedWitness {} -type LeanInt { - canon: Int - specification: LeanIntMathematicalUnboundedWitness +// Anchor: https://lean-lang.org/doc/reference/4.20.0/ +type LeanInt = Int + +data lean_int_grounding: GroundingMap = GroundingMap { + spelling: "Int" } -type LeanPointerSizedNaturalPerTargetWitness {} -type LeanUSize { - canon: UIntPlatform - specification: LeanPointerSizedNaturalPerTargetWitness +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanUSize = UIntPlatform + +data lean_usize_grounding: GroundingMap = GroundingMap { + spelling: "USize" } -type LeanUnsignedFixedWidthModularWitness {} -type LeanUInt8Width8Witness {} +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanUInt8 = UInt8 -type LeanUInt8 { - modular_semantics: LeanUnsignedFixedWidthModularWitness - width: LeanUInt8Width8Witness - canon: UInt8 +data lean_uint8_grounding: GroundingMap = GroundingMap { + spelling: "UInt8" } -type LeanUInt16Width16Witness {} -type LeanUInt16 { - modular_semantics: LeanUnsignedFixedWidthModularWitness - width: LeanUInt16Width16Witness - canon: UInt16 +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanUInt16 = UInt16 + +data lean_uint16_grounding: GroundingMap = GroundingMap { + spelling: "UInt16" } -type LeanUInt32Width32Witness {} -type LeanUInt32 { - modular_semantics: LeanUnsignedFixedWidthModularWitness - width: LeanUInt32Width32Witness - canon: UInt32 +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanUInt32 = UInt32 + +data lean_uint32_grounding: GroundingMap = GroundingMap { + spelling: "UInt32" } -type LeanUInt64Width64Witness {} -type LeanUInt64 { - modular_semantics: LeanUnsignedFixedWidthModularWitness - width: LeanUInt64Width64Witness - canon: UInt64 +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanUInt64 = UInt64 + +data lean_uint64_grounding: GroundingMap = GroundingMap { + spelling: "UInt64" } diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index c8a3f02bbcf..7f1f98f78c2 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -1,12 +1,13 @@ // src/v4/extdeps/languages/machine_code.dag // Scope: machine-code language model parameterized by Isa. -// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, MachineIsaSignedTwoComplementFixedWidthWitness, MachineSignedWordWidth8Witness, MachineSignedWordWidth16Witness, MachineSignedWordWidth32Witness, MachineSignedWordWidth64Witness, MachineSignedWordWidth128Witness, MachineIsaUnsignedModuloTwoPowWidthWitness, MachineUnsignedWordWidth8Witness, MachineUnsignedWordWidth16Witness, MachineUnsignedWordWidth32Witness, MachineUnsignedWordWidth64Witness, MachineUnsignedWordWidth128Witness, MachineI8, MachineI16, MachineI32, MachineI64, MachineI128, MachineU8, MachineU16, MachineU32, MachineU64, MachineU128, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. -// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, Symbol. -// Status: D2-REV — ISA primitive integers as fact-bundles (DECISIONS.md P4-3208 / #3208). +// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, MachineIntKind, MachineIntWidth, MachineScalar, MachineI8, machine_i8_grounding, MachineI16, machine_i16_grounding, MachineI32, machine_i32_grounding, MachineI64, machine_i64_grounding, MachineI128, machine_i128_grounding, MachineU8, machine_u8_grounding, MachineU16, machine_u16_grounding, MachineU32, machine_u32_grounding, MachineU64, machine_u64_grounding, MachineU128, machine_u128_grounding, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. +// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, Symbol, String; v4.extdeps.languages.rust (GroundingMap). +// Status: D2-REV / Practice 8 — `MachineScalar` kind×width bundle + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.machine_code +import v4.extdeps.languages.rust { GroundingMap } import v4.std.integer { Int8, Int16, @@ -22,6 +23,7 @@ import v4.std.integer { import v4.std.collection { List } import v4.std.machine { Byte } import v4.std.node { Symbol } +import v4.std.text { String } // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html @@ -60,92 +62,97 @@ type OperandFieldWidthRef { } -// Ledger: DECISIONS.md D2-REV + P4-3208 — ISA-modeled fixed-width integers as -// fact-bundles (width + representation + std `canon`), not bare std aliases. -// Anchor: Intel SDM (two's-complement fixed-width general-purpose integer reads); -// Arm A-profile Architecture Reference Manual; RISC-V ISA manual (two's complement). -type MachineIsaSignedTwoComplementFixedWidthWitness {} +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type MachineIntKind + = Signed + | Unsigned + -type MachineSignedWordWidth8Witness {} +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type MachineIntWidth + = Bits8 + | Bits16 + | Bits32 + | Bits64 + | Bits128 -type MachineSignedWordWidth16Witness {} -type MachineSignedWordWidth32Witness {} +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type MachineScalar + = IntScalar { kind: MachineIntKind, width: MachineIntWidth } -type MachineSignedWordWidth64Witness {} -type MachineSignedWordWidth128Witness {} +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +type MachineI8 = Int8 -type MachineIsaUnsignedModuloTwoPowWidthWitness {} +data machine_i8_grounding: GroundingMap = GroundingMap { + spelling: "i8" +} -type MachineUnsignedWordWidth8Witness {} -type MachineUnsignedWordWidth16Witness {} +type MachineI16 = Int16 -type MachineUnsignedWordWidth32Witness {} +data machine_i16_grounding: GroundingMap = GroundingMap { + spelling: "i16" +} -type MachineUnsignedWordWidth64Witness {} -type MachineUnsignedWordWidth128Witness {} +type MachineI32 = Int32 -type MachineI8 { - representation: MachineIsaSignedTwoComplementFixedWidthWitness - width: MachineSignedWordWidth8Witness - canon: Int8 +data machine_i32_grounding: GroundingMap = GroundingMap { + spelling: "i32" } -type MachineI16 { - representation: MachineIsaSignedTwoComplementFixedWidthWitness - width: MachineSignedWordWidth16Witness - canon: Int16 -} -type MachineI32 { - representation: MachineIsaSignedTwoComplementFixedWidthWitness - width: MachineSignedWordWidth32Witness - canon: Int32 -} +type MachineI64 = Int64 -type MachineI64 { - representation: MachineIsaSignedTwoComplementFixedWidthWitness - width: MachineSignedWordWidth64Witness - canon: Int64 +data machine_i64_grounding: GroundingMap = GroundingMap { + spelling: "i64" } -type MachineI128 { - representation: MachineIsaSignedTwoComplementFixedWidthWitness - width: MachineSignedWordWidth128Witness - canon: Int128 + +type MachineI128 = Int128 + +data machine_i128_grounding: GroundingMap = GroundingMap { + spelling: "i128" } -type MachineU8 { - representation: MachineIsaUnsignedModuloTwoPowWidthWitness - width: MachineUnsignedWordWidth8Witness - canon: UInt8 + +type MachineU8 = UInt8 + +data machine_u8_grounding: GroundingMap = GroundingMap { + spelling: "u8" } -type MachineU16 { - representation: MachineIsaUnsignedModuloTwoPowWidthWitness - width: MachineUnsignedWordWidth16Witness - canon: UInt16 + +type MachineU16 = UInt16 + +data machine_u16_grounding: GroundingMap = GroundingMap { + spelling: "u16" } -type MachineU32 { - representation: MachineIsaUnsignedModuloTwoPowWidthWitness - width: MachineUnsignedWordWidth32Witness - canon: UInt32 + +type MachineU32 = UInt32 + +data machine_u32_grounding: GroundingMap = GroundingMap { + spelling: "u32" } -type MachineU64 { - representation: MachineIsaUnsignedModuloTwoPowWidthWitness - width: MachineUnsignedWordWidth64Witness - canon: UInt64 + +type MachineU64 = UInt64 + +data machine_u64_grounding: GroundingMap = GroundingMap { + spelling: "u64" } -type MachineU128 { - representation: MachineIsaUnsignedModuloTwoPowWidthWitness - width: MachineUnsignedWordWidth128Witness - canon: UInt128 + +type MachineU128 = UInt128 + +data machine_u128_grounding: GroundingMap = GroundingMap { + spelling: "u128" } From 255b77607a28d5bae0e95270a22c570bc588dc44 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 02:16:38 -0400 Subject: [PATCH 03/16] =?UTF-8?q?WIP:=20D2=20cleanup=20ASAP=20=E2=80=94=20?= =?UTF-8?q?#3208=20lean.dag=20+=20machine=5Fcode.dag=20bare-alias=20?= =?UTF-8?q?=E2=86=92=20fact-bu?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/extdeps/languages/lean.dag | 39 +++++++++-------------- src/v4/extdeps/languages/machine_code.dag | 4 +-- 2 files changed, 17 insertions(+), 26 deletions(-) diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index a66e401cd3b..4c1f4ffc167 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -1,13 +1,17 @@ // src/v4/extdeps/languages/lean.dag // Scope: Lean 4 language model for PROOF-1 termination export. -// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. -// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, Symbol, String; v4.extdeps.languages.rust (GroundingMap). +// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. +// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, Symbol, String. // Status: D2-REV / Practice 8 — scalar ladder `LeanScalar` + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.lean -import v4.extdeps.languages.rust { GroundingMap } +// Twin of `rust.dag` `GroundingMap` pending shared `resolver.dag` home (DECISIONS.md D4; cpp.dag P2 note). +type GroundingMap { + spelling: String +} + import v4.std.integer { Int, UInt8, @@ -179,19 +183,6 @@ type LeanFidelityDisposition | LeanFailClosed { feature: LeanFidelityFeature } -fn lean_feature_disposition(f: LeanFidelityFeature) -> LeanFidelityDisposition { - match f { - LeanKernelTerm => LeanModeled - LeanPrettyNameSpelling => LeanDeclaredNormalized { feature: LeanPrettyNameSpelling } - LeanWhitespaceAndLayout => LeanDeclaredNormalized { feature: LeanWhitespaceAndLayout } - LeanTacticScript => LeanFailClosed { feature: LeanTacticScript } - LeanElaboratorOnlySyntax => LeanFailClosed { feature: LeanElaboratorOnlySyntax } - LeanUnresolvedUniverseLevel => LeanFailClosed { feature: LeanUnresolvedUniverseLevel } - LeanUnsupportedTheoremClass => LeanFailClosed { feature: LeanUnsupportedTheoremClass } - } -} - - // Anchor: https://lean-lang.org/doc/reference/4.20.0/ type LeanProofCheckSemantics { kernel_definitional_reduction: Bool @@ -227,7 +218,7 @@ type LeanScalar // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanBool = Bool -data lean_bool_grounding: GroundingMap = GroundingMap { +data lean_bool_grounding: GroundingMap = { spelling: "Bool" } @@ -235,7 +226,7 @@ data lean_bool_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/ type LeanNat = Nat -data lean_nat_grounding: GroundingMap = GroundingMap { +data lean_nat_grounding: GroundingMap = { spelling: "Nat" } @@ -243,7 +234,7 @@ data lean_nat_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/ type LeanInt = Int -data lean_int_grounding: GroundingMap = GroundingMap { +data lean_int_grounding: GroundingMap = { spelling: "Int" } @@ -251,7 +242,7 @@ data lean_int_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanUSize = UIntPlatform -data lean_usize_grounding: GroundingMap = GroundingMap { +data lean_usize_grounding: GroundingMap = { spelling: "USize" } @@ -259,7 +250,7 @@ data lean_usize_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanUInt8 = UInt8 -data lean_uint8_grounding: GroundingMap = GroundingMap { +data lean_uint8_grounding: GroundingMap = { spelling: "UInt8" } @@ -267,7 +258,7 @@ data lean_uint8_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanUInt16 = UInt16 -data lean_uint16_grounding: GroundingMap = GroundingMap { +data lean_uint16_grounding: GroundingMap = { spelling: "UInt16" } @@ -275,7 +266,7 @@ data lean_uint16_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanUInt32 = UInt32 -data lean_uint32_grounding: GroundingMap = GroundingMap { +data lean_uint32_grounding: GroundingMap = { spelling: "UInt32" } @@ -283,6 +274,6 @@ data lean_uint32_grounding: GroundingMap = GroundingMap { // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanUInt64 = UInt64 -data lean_uint64_grounding: GroundingMap = GroundingMap { +data lean_uint64_grounding: GroundingMap = { spelling: "UInt64" } diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index 7f1f98f78c2..07462e81d70 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/languages/machine_code.dag // Scope: machine-code language model parameterized by Isa. -// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, MachineIntKind, MachineIntWidth, MachineScalar, MachineI8, machine_i8_grounding, MachineI16, machine_i16_grounding, MachineI32, machine_i32_grounding, MachineI64, machine_i64_grounding, MachineI128, machine_i128_grounding, MachineU8, machine_u8_grounding, MachineU16, machine_u16_grounding, MachineU32, machine_u32_grounding, MachineU64, machine_u64_grounding, MachineU128, machine_u128_grounding, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. -// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, Symbol, String; v4.extdeps.languages.rust (GroundingMap). +// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, GroundingMap, MachineIntKind, MachineIntWidth, MachineScalar, MachineI8, machine_i8_grounding, MachineI16, machine_i16_grounding, MachineI32, machine_i32_grounding, MachineI64, machine_i64_grounding, MachineI128, machine_i128_grounding, MachineU8, machine_u8_grounding, MachineU16, machine_u16_grounding, MachineU32, machine_u32_grounding, MachineU64, machine_u64_grounding, MachineU128, machine_u128_grounding, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. +// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, Symbol, String. // Status: D2-REV / Practice 8 — `MachineScalar` kind×width bundle + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.machine_code From b1be1b308af9b54e71954a71756c9f2f8fb292f2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 02:19:51 -0400 Subject: [PATCH 04/16] =?UTF-8?q?WIP:=20D2=20cleanup=20ASAP=20=E2=80=94=20?= =?UTF-8?q?#3208=20lean.dag=20+=20machine=5Fcode.dag=20bare-alias=20?= =?UTF-8?q?=E2=86=92=20fact-bu?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/extdeps/languages/lean.dag | 17 +++++--- src/v4/extdeps/languages/machine_code.dag | 49 ++++++++++------------- 2 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index 4c1f4ffc167..d1d2cdac7d3 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -7,11 +7,6 @@ module v4.extdeps.languages.lean -// Twin of `rust.dag` `GroundingMap` pending shared `resolver.dag` home (DECISIONS.md D4; cpp.dag P2 note). -type GroundingMap { - spelling: String -} - import v4.std.integer { Int, UInt8, @@ -23,10 +18,20 @@ import v4.std.integer { import v4.std.collection { List } import v4.std.logic { Bool } import v4.std.nat { Nat } -import v4.std.node { Symbol } import v4.std.text { String } +// Twin of `v4.std.node.Symbol` / `rust.dag` authority: M1(2.7) compile_to_dag does not lower +// `import v4.std.node { Symbol }` into declarations; local atom preserves L-2 naming until import lowering lands. +type Symbol + + +// Twin of `rust.dag` `GroundingMap` pending shared `resolver.dag` home (DECISIONS.md D4; cpp.dag P2 note). +type GroundingMap { + spelling: String +} + + // Anchor: https://lean-lang.org/doc/reference/4.20.0/ // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type LeanDeclarationKind diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index 07462e81d70..b0a7e25f096 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -1,13 +1,12 @@ // src/v4/extdeps/languages/machine_code.dag // Scope: machine-code language model parameterized by Isa. -// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, GroundingMap, MachineIntKind, MachineIntWidth, MachineScalar, MachineI8, machine_i8_grounding, MachineI16, machine_i16_grounding, MachineI32, machine_i32_grounding, MachineI64, machine_i64_grounding, MachineI128, machine_i128_grounding, MachineU8, machine_u8_grounding, MachineU16, machine_u16_grounding, MachineU32, machine_u32_grounding, MachineU64, machine_u64_grounding, MachineU128, machine_u128_grounding, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. -// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, Symbol, String. +// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, Symbol, GroundingMap, MachineIntKind, MachineIntWidth, MachineScalar, MachineI8, machine_i8_grounding, MachineI16, machine_i16_grounding, MachineI32, machine_i32_grounding, MachineI64, machine_i64_grounding, MachineI128, machine_i128_grounding, MachineU8, machine_u8_grounding, MachineU16, machine_u16_grounding, MachineU32, machine_u32_grounding, MachineU64, machine_u64_grounding, MachineU128, machine_u128_grounding, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. +// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, String. // Status: D2-REV / Practice 8 — `MachineScalar` kind×width bundle + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.machine_code -import v4.extdeps.languages.rust { GroundingMap } import v4.std.integer { Int8, Int16, @@ -22,10 +21,19 @@ import v4.std.integer { } import v4.std.collection { List } import v4.std.machine { Byte } -import v4.std.node { Symbol } import v4.std.text { String } +// Twin of `v4.std.node.Symbol` — M1(2.7) compile_to_dag import lowering; see lean.dag. +type Symbol + + +// Twin of `rust.dag` `GroundingMap` pending shared `resolver.dag` home (DECISIONS.md D4; cpp.dag P2 note). +type GroundingMap { + spelling: String +} + + // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type Isa @@ -88,70 +96,70 @@ type MachineScalar // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html type MachineI8 = Int8 -data machine_i8_grounding: GroundingMap = GroundingMap { +data machine_i8_grounding: GroundingMap = { spelling: "i8" } type MachineI16 = Int16 -data machine_i16_grounding: GroundingMap = GroundingMap { +data machine_i16_grounding: GroundingMap = { spelling: "i16" } type MachineI32 = Int32 -data machine_i32_grounding: GroundingMap = GroundingMap { +data machine_i32_grounding: GroundingMap = { spelling: "i32" } type MachineI64 = Int64 -data machine_i64_grounding: GroundingMap = GroundingMap { +data machine_i64_grounding: GroundingMap = { spelling: "i64" } type MachineI128 = Int128 -data machine_i128_grounding: GroundingMap = GroundingMap { +data machine_i128_grounding: GroundingMap = { spelling: "i128" } type MachineU8 = UInt8 -data machine_u8_grounding: GroundingMap = GroundingMap { +data machine_u8_grounding: GroundingMap = { spelling: "u8" } type MachineU16 = UInt16 -data machine_u16_grounding: GroundingMap = GroundingMap { +data machine_u16_grounding: GroundingMap = { spelling: "u16" } type MachineU32 = UInt32 -data machine_u32_grounding: GroundingMap = GroundingMap { +data machine_u32_grounding: GroundingMap = { spelling: "u32" } type MachineU64 = UInt64 -data machine_u64_grounding: GroundingMap = GroundingMap { +data machine_u64_grounding: GroundingMap = { spelling: "u64" } type MachineU128 = UInt128 -data machine_u128_grounding: GroundingMap = GroundingMap { +data machine_u128_grounding: GroundingMap = { spelling: "u128" } @@ -338,19 +346,6 @@ type MachineFidelityDisposition | MachineFailClosed { feature: MachineFidelityFeature } -fn machine_feature_disposition(f: MachineFidelityFeature) -> MachineFidelityDisposition { - match f { - ValidInstructionEncoding => MachineModeled - InstructionAliasSpelling => MachineDeclaredNormalized { feature: InstructionAliasSpelling } - PaddingByteRun => MachineDeclaredNormalized { feature: PaddingByteRun } - UndecodableByteRun => MachineFailClosed { feature: UndecodableByteRun } - PrivilegedOrUndefinedEncoding => MachineFailClosed { feature: PrivilegedOrUndefinedEncoding } - IsaRevisionMismatch => MachineFailClosed { feature: IsaRevisionMismatch } - AmbiguousDecode => MachineFailClosed { feature: AmbiguousDecode } - } -} - - // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type MachineIntegerOverflowBehavior From ac27cef95b8d1229469faf412313f5f3118a2fd9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 02:22:36 -0400 Subject: [PATCH 05/16] =?UTF-8?q?WIP:=20D2=20cleanup=20ASAP=20=E2=80=94=20?= =?UTF-8?q?#3208=20lean.dag=20+=20machine=5Fcode.dag=20bare-alias=20?= =?UTF-8?q?=E2=86=92=20fact-bu?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- INVARIANTS.md | 1 + src/v3/compiler/tests/integration.rs | 2 ++ .../tests/integration/sg0_census_test.rs | 1 + .../v4_extdeps_cpp_dag_smoke_test.rs | 26 +++++++++++++++++++ src/v4/DECISIONS.md | 11 ++++++-- src/v4/extdeps/languages/cpp.dag | 21 ++++++++++++--- src/v4/extdeps/languages/lean.dag | 4 +-- 7 files changed, 59 insertions(+), 7 deletions(-) create mode 100644 src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs diff --git a/INVARIANTS.md b/INVARIANTS.md index 8ae852141e8..ebdb9a7c5da 100644 --- a/INVARIANTS.md +++ b/INVARIANTS.md @@ -351,6 +351,7 @@ 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. | diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index d35d690518e..9ab9ce7d823 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -275,6 +275,8 @@ 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"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index d16e3459161..a077b63833d 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -829,6 +829,7 @@ 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 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. diff --git a/src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs new file mode 100644 index 00000000000..b8cf3c94641 --- /dev/null +++ b/src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs @@ -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::>() + ), + Err(CompileError::Semantic(dag)) => panic!( + "{CPP_PATH}: semantic errors: {:?}", + dag.diagnostics().iter().collect::>() + ), + Err(other) => panic!("{CPP_PATH}: {other:?}"), + } +} diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 66fe2b60b49..5ace2c14d23 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -63,7 +63,7 @@ authority location(s) and moves to Part 1. | **D4** | **[SUPERSEDED by D2-REV — see the D2-REV row below + the "D2 REVERSAL" section]** **GroundingMap-home — the shared `extdeps/languages/resolver.dag` registry** (operator-ratified 2026-05-16; co-drafted; completes **D2**). The D2 resolver's *shared* types live in ONE new file `extdeps/languages/resolver.dag` — NOT re-declared per language (parallel-declaration P2 forbids; `feedback_import_not_redeclare_carriers`) and NOT homed in `rust.dag` (which would make one language file a substrate authority for the other four, and balloon as future shared resolver types land). `type GroundingMap { spelling: String }` is its first resident. **Admission rule (STRICT):** `resolver.dag` hosts ONLY *structurally-language-INVARIANT* resolver types — a type whose structure provably cannot vary across the modeled language specs (a convergence carrier). Spec-varying types stay per-language (`OverflowDisposition` etc. — D2.5 / L-2). Test before admitting: can you prove the structure invariant across the specs? Future shared resolver types (e.g. the C5-fidelity `Modeled \| Declared-normalized \| Fail-closed` disposition classifier) land here without a fresh placement decision. Closed-tree extension: `STRUCTURE.md` `.dag` count +1. Per-language files each add a one-line `import … resolver { GroundingMap }` + their per-primitive `data __grounding` instances (the grounding-row fan-out — canonical `rust.dag` first, then the 4 others). | new `extdeps/languages/resolver.dag` + `STRUCTURE.md` count/enumeration + `extdeps/languages/*` import lines + grounding instances; this row; cross-ref **D2** | | **D5** | **Operator-driven frozen-header / frozen-contract reconcile is sanctioned in-PR** (operator-ratified 2026-05-16). "Preserve-verbatim" on a frozen scaffold header forbids *unsanctioned worker contract-drift* — it does NOT forbid *sanctioned reconciliation*. When an operator-tier action (a BLOCKING finding, an operator ruling) legitimately moves a worker's body past its frozen header or I/O contract, the header/contract is **reconciled to match in the SAME PR**, with the reconcile receipt — citing the driving operator action — recorded in the **commit message**. **Amended 2026-05-17 (operator-ratified):** the receipt is a commit-message entry, *not* an in-file `HEADER RECONCILE` block — the in-file-block form is superseded by the no-prose directive / `docs/modeling-discipline.md` Practice 9. D5's intent — a conscious, reviewer-visible reconcile receipt — is preserved: it lives in the commit message + `git blame`. **Discriminator:** an operator-tier action drove the body change ⇒ reconcile the header/contract in-PR, flagged; NO operator action drove it ⇒ the body must conform to the frozen header (preserve-verbatim holds, the worker cannot move the contract). Covers BOTH header-doc drift (stale `Owns`/`Consumes` bullets after a sanctioned refactor) AND frozen-contract changes (operator BLOCKS an I/O contract as P2/§2-insufficient). Already operating: `integer.dag` #3190 (`Consumes` reconciled), #3209 finding 2 (`WaitProcessResult`). Does NOT permit free worker header edits — operator-driven only. | this row + the reconcile receipt recorded in the **commit message** (the in-file `HEADER RECONCILE` block form — `integer.dag` #3190 precedent — is retired by Practice 9, 2026-05-17); refines the frozen-scaffold-header / preserve-verbatim discipline | | **D2-REV** | **D2 / D4 REVERSED — fact-bundle modeling supersedes alias-identity** (operator-ratified 2026-05-17, **out-of-band** — the verbatim operator-quote provenance is in the "D2 REVERSAL" section below). An `extdeps` primitive is modeled as a fact-bundle grounded from its own spec, never a bare `std/` alias; deduplicate to a `std/` carrier only on *proven* coincidence; the structural fact-density / hollow-alias gate is `T-30`, a hard prerequisite of T-4. This is a one-line index pointer — the full record (root cause, phased plan, impact map, "coincide" definition) is the **"D2 REVERSAL + FACT-BUNDLE RESEED"** section below, which is the authority. Supersedes the **D2** and **D4** rows above. | the **"D2 REVERSAL + FACT-BUNDLE RESEED"** section of this file (authority); `#3224` executes Phase 1; `docs/modeling/grounding-worked-examples.md` companion | -| **P4-3208** | **Practice-4 ledger home for #3208 Lean/machine-code model coproducts** (operator-directed strict de-prose 2026-05-17). `.dag` files keep only terse anchors/tags; detailed dissolution ledgers live here until modeling-discipline reconciles Practice-4 vs Practice-9. See the "P4-3208 coproduct ledger" section below. | this row + "P4-3208 coproduct ledger"; `extdeps/languages/{lean,machine_code}.dag` keeps terse carrier declarations only | +| **P4-3208** | **Practice-4 ledger home for #3208 Lean/machine-code/C++-bool model coproducts** (operator-directed strict de-prose 2026-05-17). `.dag` files keep only terse anchors/tags; detailed dissolution ledgers live here until modeling-discipline reconciles Practice-4 vs Practice-9. See the "P4-3208 coproduct ledger" section below. | this row + "P4-3208 coproduct ledger"; `extdeps/languages/{lean,machine_code,cpp}.dag` keeps terse carrier declarations only | | **OS-1** | **OS extdep coproduct ledgers and refinement-scaffold disposition for #3209** (operator-audit regime, 2026-05-17). Practice-4 dissolution ledgers for `file_system.dag` / `process.dag` are architectural decision records, not source comments; the `.dag` files keep only terse tags/anchors. POSIX numeric and byte-string refinement gaps remain tracked scaffolds in #3209, not expanded fact bundles; named trigger is **T-25-core refinement substrate / T-30 fact-density gate**. | this row + "OS-1 — #3209 coproduct dissolution and scaffold record" below; terse tags in `extdeps/file_system.dag` and `extdeps/process.dag` | | **T29-ABI** | **C++ ABI / target data-model slice** (T-29, operator-ratified 2026-05-17; manager brief 2026-05-18). `extdeps/cpp_abi.dag` is the single authority for C++ implementation-defined fundamental-width choices consumed by `cpp.dag`; C++ primitive fact-bundles parameterize over `CppTargetProfile` instead of guessing LP64/ILP32 constants. `CppIntegerWidth`, `CppPlainCharSignedness`, `CppDataModelFamily`, and `CppAbiModel` remain closed coproducts: each is an externally named alternative, not simultaneous coordinates. Common ILP32/LP64/LLP64/ILP64 rows are type-level data-model facts parameterized by `plain_char_signedness`; the data-model family never defaults that independent implementation-defined fact. | `extdeps/cpp_abi.dag`, `extdeps/languages/cpp.dag`, `STRUCTURE.md`; cross-ref T-29 in `TASKS.md` | @@ -215,7 +215,8 @@ consumes that derived fact. ## P4-3208 coproduct ledger -For #3208's `lean.dag` and `machine_code.dag`, each listed coproduct was +For #3208's `lean.dag`, `machine_code.dag`, and the `CppBool` surface in +`cpp.dag`, each listed coproduct was checked against the Practice-4 five-pattern ledger: 1. **Fact placement** — can this distinction move to one consumer instead @@ -269,6 +270,12 @@ checked against the Practice-4 five-pattern ledger: | `MachineIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` / `LeanIntWidth` with `Bits128` extension: closed width ladder for ISA fixed-width integers through 128-bit class; not algebra; not a `Symbol` width tag. | | `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts; per-width `MachineI*` / `MachineU*` aliases + `machine_*_grounding` rows cite std ladder coincidence separately (Practice 8). | +### `src/v4/extdeps/languages/cpp.dag` + +| Carrier | Classification | Ledger result | +|---------|----------------|---------------| +| `CppBool` | 🟢 GREEN terminal | Same dissolution posture as `RustBool` (`rust.dag`): kernel `CppBool = Bool` + `cpp_bool_grounding` cites std coincidence for the C++ `bool` spelling (Practice 8 / D2-REV). | + ## OS-1 — #3209 Coproduct Dissolution And Scaffold Record This section preserves the Practice-4 ledger content moved out of diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag index c9fc8f0f81c..37f60c36ec0 100644 --- a/src/v4/extdeps/languages/cpp.dag +++ b/src/v4/extdeps/languages/cpp.dag @@ -1,14 +1,29 @@ // src/v4/extdeps/languages/cpp.dag // Scope: C++ language primitive resolver facts. -// Owns: CppIntegerOverflowDisposition, CppBool. -// Consumes: kernel-ambient Bool; CppTargetProfile/CppTargetDataModel via T29-ABI follow-up rows. -// Status: D2-REV-compatible C++ resolver slice; grounding rows and non-Bool scalar aliases deferred to pinned shared carriers. +// Owns: CppIntegerOverflowDisposition, CppBool, GroundingMap, cpp_bool_grounding. +// Consumes: Bool, String (explicit imports); CppTargetProfile/CppTargetDataModel via T29-ABI follow-up rows. +// Status: D2-REV-compatible C++ resolver slice; `cpp_bool_grounding` cites Bool coincidence (Practice 8). Non-Bool scalar ladder — 🟡 T-4 Phase-3 cpp-slice + T-25-core, dissolve-on-arrival, gunbc#3244 (not a now-fix). module v4.extdeps.languages.cpp + +import v4.std.logic { Bool } +import v4.std.text { String } + + +// Twin of `rust.dag` `GroundingMap` pending `resolver.dag` (DECISIONS.md D4; INVARIANTS P2). +type GroundingMap { + spelling: String +} + + // 🟢 coproduct dissolution — DECISIONS.md T29-ABI + D2-REV. type CppIntegerOverflowDisposition = RepresentableResultRequired | UnsignedModuloArithmetic type CppBool = Bool + +data cpp_bool_grounding: GroundingMap = { + spelling: "bool" +} diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index d1d2cdac7d3..09e7c53c216 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/languages/lean.dag // Scope: Lean 4 language model for PROOF-1 termination export. -// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. -// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, Symbol, String. +// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. +// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, String. // Status: D2-REV / Practice 8 — scalar ladder `LeanScalar` + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.lean From 85ed607f08132f4da7df940d5297cdfd16920862 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 06:46:45 +0000 Subject: [PATCH 06/16] fix(ci): SG-0 net-shrink append for PR #3280 (+3 hand paths) CI prepends this file so the SG-0 hand-path delta matches the census edit and carries a (c) pairing with dispatch evidence for gunbc#3280. Co-authored-by: Cursor --- scripts/ci-merge/sg0-pr-body-append.3280.txt | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 scripts/ci-merge/sg0-pr-body-append.3280.txt diff --git a/scripts/ci-merge/sg0-pr-body-append.3280.txt b/scripts/ci-merge/sg0-pr-body-append.3280.txt new file mode 100644 index 00000000000..0ee09c2a0a9 --- /dev/null +++ b/scripts/ci-merge/sg0-pr-body-append.3280.txt @@ -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). From 35fea3a349f8fd440382e839f333de5611a4c8dd Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 06:52:26 +0000 Subject: [PATCH 07/16] =?UTF-8?q?fix(lean):=20ground=20signed=20fixed-widt?= =?UTF-8?q?h=20Int8=E2=80=93Int64=20and=20ISize=20for=20Lean=204.20?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Align extdeps fidelity with the fixed-precision integer surface: std coincidence + GroundingMap spellings for Int8/16/32/64 and platform ISize (IntPlatform), matching the existing UInt* ladder. P4-3208 ledger row updated to cite the signed aliases. Co-authored-by: Cursor --- src/v4/DECISIONS.md | 2 +- src/v4/extdeps/languages/lean.dag | 49 +++++++++++++++++++++++++++++-- 2 files changed, 48 insertions(+), 3 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 5ace2c14d23..bf873fc13e8 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -244,7 +244,7 @@ checked against the Practice-4 five-pattern ledger: | `LeanFidelityDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: modeled/normalized/fail-closed is the shared C5 disposition; non-modeled variants carry feature payloads and a flat record admits impossible combinations; not algebra; one feature has one disposition; payloads are heterogeneous. | | `LeanIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` (`rust.dag`, DECISIONS.md Part 6 / CP-3229): signed vs unsigned is a closed external alternative for fixed-precision scalars, not a hideable coordinate; not algebra; not one `F` family over identical payloads. | | `LeanIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` (`rust.dag`): closed width ladder for fixed-precision scalars; `Pointer` names platform-sized facts separately from fixed bit widths; not algebra; not a `Symbol` tag. | -| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling. | +| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling. Signed fixed-width `Int8`/`Int16`/`Int32`/`Int64`/`ISize` and unsigned `UInt*`/`USize` aliases + `lean_*_grounding` rows cite the std integer ladder per Lean 4.20 fixed-precision surface (same doc anchor as `lean.dag`). | ### `src/v4/extdeps/languages/machine_code.dag` diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index 09e7c53c216..ac042125f1a 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/languages/lean.dag // Scope: Lean 4 language model for PROOF-1 termination export. -// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. -// Consumes: Int, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, String. +// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanInt8, lean_int8_grounding, LeanInt16, lean_int16_grounding, LeanInt32, lean_int32_grounding, LeanInt64, lean_int64_grounding, LeanISize, lean_isize_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. +// Consumes: Int, Int8, Int16, Int32, Int64, IntPlatform, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, String. // Status: D2-REV / Practice 8 — scalar ladder `LeanScalar` + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). module v4.extdeps.languages.lean @@ -9,6 +9,11 @@ module v4.extdeps.languages.lean import v4.std.integer { Int, + Int8, + Int16, + Int32, + Int64, + IntPlatform, UInt8, UInt16, UInt32, @@ -244,6 +249,46 @@ data lean_int_grounding: GroundingMap = { } +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanInt8 = Int8 + +data lean_int8_grounding: GroundingMap = { + spelling: "Int8" +} + + +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanInt16 = Int16 + +data lean_int16_grounding: GroundingMap = { + spelling: "Int16" +} + + +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanInt32 = Int32 + +data lean_int32_grounding: GroundingMap = { + spelling: "Int32" +} + + +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanInt64 = Int64 + +data lean_int64_grounding: GroundingMap = { + spelling: "Int64" +} + + +// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ +type LeanISize = IntPlatform + +data lean_isize_grounding: GroundingMap = { + spelling: "ISize" +} + + // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ type LeanUSize = UIntPlatform From 9853b706b17efa8378d7f5725059c49fa908a2e8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 07:11:33 +0000 Subject: [PATCH 08/16] chore(lean): single-line Symbol twin note (Practice 9) Co-authored-by: Cursor --- src/v4/extdeps/languages/lean.dag | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index ac042125f1a..825e59ee68f 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -26,8 +26,7 @@ import v4.std.nat { Nat } import v4.std.text { String } -// Twin of `v4.std.node.Symbol` / `rust.dag` authority: M1(2.7) compile_to_dag does not lower -// `import v4.std.node { Symbol }` into declarations; local atom preserves L-2 naming until import lowering lands. +// Twin of `v4.std.node.Symbol` — M1(2.7) compile_to_dag import lowering; local L-2 atom until `v4.std.node` import lowering lands (DECISIONS.md / P2). type Symbol From d29b3786cb36fa5d4d9bdd7e5b437990d924c6af Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 07:29:56 +0000 Subject: [PATCH 09/16] docs(INVARIANTS): P2 receipt for extdeps GroundingMap/Symbol twins Single-file compile_to_dag smokes cannot resolve a shared resolver import today; document the interim structural twin + dissolution trigger so the pattern is P2-staging, not silent duplicate authority (addresses D4/P2 review). Co-authored-by: Cursor --- INVARIANTS.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/INVARIANTS.md b/INVARIANTS.md index ebdb9a7c5da..4b6fb94a306 100644 --- a/INVARIANTS.md +++ b/INVARIANTS.md @@ -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`, `machine_code.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**. 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. From 57f87a7825b3868815ba0e24a44a572575c17204 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 07:42:20 +0000 Subject: [PATCH 10/16] docs(DECISIONS): align #3208 C5 bullet with removed disposition fns Co-authored-by: Cursor --- src/v4/DECISIONS.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index bf873fc13e8..4d8e2e20899 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -838,8 +838,9 @@ clobber surviving language vocabulary and the `std/` numeric core. - **Shared C5 fidelity disposition carrier and disposition rows:** 🟡 bound to the same post-D2-REV shared-C5-fidelity / fact-bundle rework. This covers `LeanFidelityDisposition` / `MachineFidelityDisposition` - consolidation and the `lean_feature_disposition` / - `machine_feature_disposition` predicate/data-row dissolution. Trigger: + consolidation and replacing the removed M1(2.8)-opaque `fn lean_feature_disposition` / + `fn machine_feature_disposition` maps with **structural** per-feature disposition + authority (data rows or shared carrier) once the shared C5 substrate lands. Trigger: the T-4 fact-bundle rework executes after T-30 and the remaining T-4 feeders clear. - **Phantom `IRCarrier` parameters:** 🟢 not a dissolution-class finding; From 6519a10f3e19b6b49f13660c69b34a01a2fb8184 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 08:03:20 +0000 Subject: [PATCH 11/16] fix(extdeps): align lean/machine_code numerics with D2-REV MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove hollow std int aliases and spelling-only GroundingMap rows; keep LeanScalar/MachineScalar fact bundles and explicit displacement records. Update P4-3208 ledger, INVARIANTS §P2 interim receipt. Co-authored-by: Cursor --- INVARIANTS.md | 2 +- src/v4/DECISIONS.md | 8 +- src/v4/extdeps/languages/lean.dag | 119 ++-------------------- src/v4/extdeps/languages/machine_code.dag | 112 +++++--------------- 4 files changed, 37 insertions(+), 204 deletions(-) diff --git a/INVARIANTS.md b/INVARIANTS.md index 4b6fb94a306..f48ae8b601a 100644 --- a/INVARIANTS.md +++ b/INVARIANTS.md @@ -167,7 +167,7 @@ A canonical accessor exists (e.g., a reflected substrate function), but a second ### 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`, `machine_code.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**. 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. +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 diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 4d8e2e20899..04d775788cf 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -244,7 +244,7 @@ checked against the Practice-4 five-pattern ledger: | `LeanFidelityDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: modeled/normalized/fail-closed is the shared C5 disposition; non-modeled variants carry feature payloads and a flat record admits impossible combinations; not algebra; one feature has one disposition; payloads are heterogeneous. | | `LeanIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` (`rust.dag`, DECISIONS.md Part 6 / CP-3229): signed vs unsigned is a closed external alternative for fixed-precision scalars, not a hideable coordinate; not algebra; not one `F` family over identical payloads. | | `LeanIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` (`rust.dag`): closed width ladder for fixed-precision scalars; `Pointer` names platform-sized facts separately from fixed bit widths; not algebra; not a `Symbol` tag. | -| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling. Signed fixed-width `Int8`/`Int16`/`Int32`/`Int64`/`ISize` and unsigned `UInt*`/`USize` aliases + `lean_*_grounding` rows cite the std integer ladder per Lean 4.20 fixed-precision surface (same doc anchor as `lean.dag`). | +| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts read from the Lean 4.20 anchor; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling only (**D2-REV**). Per-width std aliases + spelling-only `GroundingMap` rows for integers are **omitted** — they were the reversed-D2 hollow shape; unbounded / platform-width Lean numerics are deferred until modeled as explicit fact-bundles. | ### `src/v4/extdeps/languages/machine_code.dag` @@ -255,7 +255,7 @@ checked against the Practice-4 five-pattern ledger: | `InstructionLength` | 🟢 GREEN terminal | All five dissolution patterns fail: tokenization/decoding consumes the instruction boundary; fixed and variable forms carry different payloads; not algebra; one decode point has one length discipline; payloads are heterogeneous. | | `InstructionWord` | 🟡 TRACKED scaffold (`feature:fixed-cardinality-width-carrier`) | Fact placement fails; variant-is-data is partial because the bounded byte-count / Nat-indexed instruction-width primitive is missing. Named arrival: TASKS.md T-3 scalar/numeric stack lands the fixed-cardinality width carrier in `std/machine.dag` or `std/cardinality.dag`. Dissolve-on-arrival follow-up: replace this enum with that carrier and update the P4-3208 tag/row to 🟢, or remove it if no coproduct remains. | | `RegisterClass` | 🟢 GREEN terminal | All five dissolution patterns fail: operand legality/cost/register consumers share register class; width alone cannot distinguish classes; integer/float aliases ground elsewhere but register class is ISA surface; one occurrence has one class; register semantics are heterogeneous. | -| `IndexScale` | 🟢 GREEN terminal | All five dissolution patterns fail: decode/emit/address calculation share scale legality; `MachineU8` admits invalid factors; not algebra; one scaled index has one factor; closed factors are not one family. | +| `IndexScale` | 🟢 GREEN terminal | All five dissolution patterns fail: decode/emit/address calculation share scale legality; an unconstrained numeric width tag admits invalid factors; not algebra; one scaled index has one factor; closed factors are not one family. | | `AddressingMode` | 🟢 GREEN terminal | All five dissolution patterns fail: operand decode and memory-effect lenses share the classifier; variants have different required fields and a flat record admits invalid mixtures; not algebra; one operand occurrence has one address form; payloads are heterogeneous. | | `Operand` | 🟢 GREEN terminal | All five dissolution patterns fail: decode/emit/operand legality branch on operand shape; payloads are heterogeneous; instruction operand syntax is ISA surface; one operand is register/immediate/memory; payloads differ by category. | | `ImmediateOperandTarget` | 🟢 GREEN terminal | All five dissolution patterns fail: decode/branch-target analysis/emit distinguish literal and target immediates; `Bool`/`Symbol` erases target role; not algebra; one immediate slot has one target class; alternatives are closed. | @@ -268,7 +268,9 @@ checked against the Practice-4 five-pattern ledger: | `FlagWriteDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: condition-code dependency consumers read this coordinate; `Bool` cannot distinguish architectural flags vs predicate-register writes; not algebra; one instruction has one flag-write disposition; alternatives are closed. | | `MachineIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` / `LeanIntKind`: ISA-modeled signed vs unsigned is a closed alternative for fixed-width machine integers, not a coordinate; not algebra; consumers branch uniformly. | | `MachineIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` / `LeanIntWidth` with `Bits128` extension: closed width ladder for ISA fixed-width integers through 128-bit class; not algebra; not a `Symbol` width tag. | -| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts; per-width `MachineI*` / `MachineU*` aliases + `machine_*_grounding` rows cite std ladder coincidence separately (Practice 8). | +| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — explicit `{ kind, width }` products citing SDM / ISA addressing facts; coincidence with std `Int32`/`Int64` is a separate proved obligation, not spelling. | +| `MachineSignedDisplacement32` | 🟢 GREEN terminal | D2-REV: two-field product (`MachineIntKind` × `MachineIntWidth`) models ISA addressing displacement facts for 32-bit-class encodings (SDM / ISA manuals); not a bare `Int32` alias; not one nullary coproduct arm. | +| `MachineSignedDisplacement64` | 🟢 GREEN terminal | D2-REV: same posture as `MachineSignedDisplacement32` for 64-bit absolute linear-address displacement forms. | ### `src/v4/extdeps/languages/cpp.dag` diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index 825e59ee68f..f573eb24dc8 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -1,28 +1,14 @@ // src/v4/extdeps/languages/lean.dag // Scope: Lean 4 language model for PROOF-1 termination export. -// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding, LeanNat, lean_nat_grounding, LeanInt, lean_int_grounding, LeanInt8, lean_int8_grounding, LeanInt16, lean_int16_grounding, LeanInt32, lean_int32_grounding, LeanInt64, lean_int64_grounding, LeanISize, lean_isize_grounding, LeanUSize, lean_usize_grounding, LeanUInt8, lean_uint8_grounding, LeanUInt16, lean_uint16_grounding, LeanUInt32, lean_uint32_grounding, LeanUInt64, lean_uint64_grounding. -// Consumes: Int, Int8, Int16, Int32, Int64, IntPlatform, UInt8, UInt16, UInt32, UInt64, UIntPlatform, List, Bool, Nat, String. -// Status: D2-REV / Practice 8 — scalar ladder `LeanScalar` + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). +// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding. +// Consumes: List, Bool, String. +// Status: D2-REV / Practice 8 — fixed-precision numeric facts live in `LeanScalar` `IntScalar { kind, width }` only (DECISIONS.md §D2 REVERSAL); kernel `LeanBool = Bool` + `lean_bool_grounding` only. No bare std integer aliases or spelling-only `GroundingMap` rows for ints (P4-3208 / #3208). module v4.extdeps.languages.lean -import v4.std.integer { - Int, - Int8, - Int16, - Int32, - Int64, - IntPlatform, - UInt8, - UInt16, - UInt32, - UInt64, - UIntPlatform -} import v4.std.collection { List } import v4.std.logic { Bool } -import v4.std.nat { Nat } import v4.std.text { String } @@ -232,97 +218,8 @@ data lean_bool_grounding: GroundingMap = { } -// Anchor: https://lean-lang.org/doc/reference/4.20.0/ -type LeanNat = Nat - -data lean_nat_grounding: GroundingMap = { - spelling: "Nat" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/ -type LeanInt = Int - -data lean_int_grounding: GroundingMap = { - spelling: "Int" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanInt8 = Int8 - -data lean_int8_grounding: GroundingMap = { - spelling: "Int8" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanInt16 = Int16 - -data lean_int16_grounding: GroundingMap = { - spelling: "Int16" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanInt32 = Int32 - -data lean_int32_grounding: GroundingMap = { - spelling: "Int32" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanInt64 = Int64 - -data lean_int64_grounding: GroundingMap = { - spelling: "Int64" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanISize = IntPlatform - -data lean_isize_grounding: GroundingMap = { - spelling: "ISize" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanUSize = UIntPlatform - -data lean_usize_grounding: GroundingMap = { - spelling: "USize" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanUInt8 = UInt8 - -data lean_uint8_grounding: GroundingMap = { - spelling: "UInt8" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanUInt16 = UInt16 - -data lean_uint16_grounding: GroundingMap = { - spelling: "UInt16" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanUInt32 = UInt32 - -data lean_uint32_grounding: GroundingMap = { - spelling: "UInt32" -} - - -// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ -type LeanUInt64 = UInt64 - -data lean_uint64_grounding: GroundingMap = { - spelling: "UInt64" -} +// Unbounded `Nat` / `Int` and per-width fixed-precision spellings (`Int8`, …) from the Lean +// reference are **not** modeled as `type LeanX = stdX` + `GroundingMap { spelling: … }` — that +// shape is the reversed D2 hollow alias (DECISIONS.md §D2 REVERSAL; INVARIANTS.md P1 / Practice 8). +// Wire names are not structural coincidence. Fixed-precision facts live only in `LeanScalar` +// above; future unbounded / platform-width carriers land as explicit fact-bundles when needed. diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index b0a7e25f096..d50a896dbc1 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -1,39 +1,20 @@ // src/v4/extdeps/languages/machine_code.dag // Scope: machine-code language model parameterized by Isa. -// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, Symbol, GroundingMap, MachineIntKind, MachineIntWidth, MachineScalar, MachineI8, machine_i8_grounding, MachineI16, machine_i16_grounding, MachineI32, machine_i32_grounding, MachineI64, machine_i64_grounding, MachineI128, machine_i128_grounding, MachineU8, machine_u8_grounding, MachineU16, machine_u16_grounding, MachineU32, machine_u32_grounding, MachineU64, machine_u64_grounding, MachineU128, machine_u128_grounding, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. -// Consumes: Int8, Int16, Int32, Int64, Int128, UInt8, UInt16, UInt32, UInt64, UInt128, List, Byte, String. -// Status: D2-REV / Practice 8 — `MachineScalar` kind×width bundle + std coincidence via `GroundingMap` (rust.dag template; P4-3208 / #3208). +// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, Symbol, MachineIntKind, MachineIntWidth, MachineScalar, MachineSignedDisplacement32, MachineSignedDisplacement64, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. +// Consumes: List, Byte. +// Status: D2-REV / Practice 8 — ISA scalar facts in `MachineScalar` only; addressing displacements use explicit `MachineSignedDisplacement{32,64}` fact records (DECISIONS.md §D2 REVERSAL). No bare std integer aliases or spelling-only `GroundingMap` rows (P4-3208 / #3208). module v4.extdeps.languages.machine_code -import v4.std.integer { - Int8, - Int16, - Int32, - Int64, - Int128, - UInt8, - UInt16, - UInt32, - UInt64, - UInt128 -} import v4.std.collection { List } import v4.std.machine { Byte } -import v4.std.text { String } // Twin of `v4.std.node.Symbol` — M1(2.7) compile_to_dag import lowering; see lean.dag. type Symbol -// Twin of `rust.dag` `GroundingMap` pending shared `resolver.dag` home (DECISIONS.md D4; cpp.dag P2 note). -type GroundingMap { - spelling: String -} - - // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type Isa @@ -93,74 +74,22 @@ type MachineScalar = IntScalar { kind: MachineIntKind, width: MachineIntWidth } -// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html -type MachineI8 = Int8 - -data machine_i8_grounding: GroundingMap = { - spelling: "i8" -} - - -type MachineI16 = Int16 - -data machine_i16_grounding: GroundingMap = { - spelling: "i16" -} +// D2-REV (DECISIONS.md §D2 REVERSAL): displacement operands carry ISA signedness + width facts as +// an explicit product — not `type MachineI32 = Int32` hollow aliases. Coincidence with std +// fixed-width carriers is a separate proved obligation (U1 / T-9), not `GroundingMap { spelling: … }`. -type MachineI32 = Int32 - -data machine_i32_grounding: GroundingMap = { - spelling: "i32" -} - - -type MachineI64 = Int64 - -data machine_i64_grounding: GroundingMap = { - spelling: "i64" -} - - -type MachineI128 = Int128 - -data machine_i128_grounding: GroundingMap = { - spelling: "i128" -} - - -type MachineU8 = UInt8 - -data machine_u8_grounding: GroundingMap = { - spelling: "u8" -} - - -type MachineU16 = UInt16 - -data machine_u16_grounding: GroundingMap = { - spelling: "u16" -} - - -type MachineU32 = UInt32 - -data machine_u32_grounding: GroundingMap = { - spelling: "u32" -} - - -type MachineU64 = UInt64 - -data machine_u64_grounding: GroundingMap = { - spelling: "u64" +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +type MachineSignedDisplacement32 { + kind: MachineIntKind + width: MachineIntWidth } -type MachineU128 = UInt128 - -data machine_u128_grounding: GroundingMap = { - spelling: "u128" +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +type MachineSignedDisplacement64 { + kind: MachineIntKind + width: MachineIntWidth } @@ -208,11 +137,16 @@ type IndexScale // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type AddressingMode - = AbsoluteAddress { displacement: MachineI64 } + = AbsoluteAddress { displacement: MachineSignedDisplacement64 } | RegisterIndirect { base: RegisterRef } - | BaseDisplacement { base: RegisterRef, displacement: MachineI32 } - | BaseIndexScale { base: RegisterRef, index: RegisterRef, scale: IndexScale, displacement: MachineI32 } - | PcRelative { displacement: MachineI32 } + | BaseDisplacement { base: RegisterRef, displacement: MachineSignedDisplacement32 } + | BaseIndexScale { + base: RegisterRef, + index: RegisterRef, + scale: IndexScale, + displacement: MachineSignedDisplacement32 + } + | PcRelative { displacement: MachineSignedDisplacement32 } // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html From bdf7e6076cab49219c99cdec77153610a200a098 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 08:16:13 +0000 Subject: [PATCH 12/16] chore(extdeps): Practice-9 terse .dag headers; move cpp deferral to DECISIONS Drop redundant multi-line D2 rationale from lean/machine_code sources; shorten Status lines; record non-Bool cpp scalar deferral under P4-3208. Co-authored-by: Cursor --- src/v4/DECISIONS.md | 2 ++ src/v4/extdeps/languages/cpp.dag | 2 +- src/v4/extdeps/languages/lean.dag | 9 +-------- src/v4/extdeps/languages/machine_code.dag | 7 +------ 4 files changed, 5 insertions(+), 15 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 04d775788cf..90eeddc5df4 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -274,6 +274,8 @@ checked against the Practice-4 five-pattern ledger: ### `src/v4/extdeps/languages/cpp.dag` +Non-Bool C++ scalar ladder in this slice: **tracked** — 🟡 `feature:t4-cpp-scalar-ladder` (T-4 Phase-3 cpp-slice + T-25-core); dissolve on **gunbc#3244** arrival. + | Carrier | Classification | Ledger result | |---------|----------------|---------------| | `CppBool` | 🟢 GREEN terminal | Same dissolution posture as `RustBool` (`rust.dag`): kernel `CppBool = Bool` + `cpp_bool_grounding` cites std coincidence for the C++ `bool` spelling (Practice 8 / D2-REV). | diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag index 37f60c36ec0..70f5540d0d0 100644 --- a/src/v4/extdeps/languages/cpp.dag +++ b/src/v4/extdeps/languages/cpp.dag @@ -2,7 +2,7 @@ // Scope: C++ language primitive resolver facts. // Owns: CppIntegerOverflowDisposition, CppBool, GroundingMap, cpp_bool_grounding. // Consumes: Bool, String (explicit imports); CppTargetProfile/CppTargetDataModel via T29-ABI follow-up rows. -// Status: D2-REV-compatible C++ resolver slice; `cpp_bool_grounding` cites Bool coincidence (Practice 8). Non-Bool scalar ladder — 🟡 T-4 Phase-3 cpp-slice + T-25-core, dissolve-on-arrival, gunbc#3244 (not a now-fix). +// Status: D2-REV resolver slice; 🟡 feature:t4-cpp-scalar-ladder — DECISIONS.md P4-3208 + T29-ABI. module v4.extdeps.languages.cpp diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag index f573eb24dc8..527a5b0e383 100644 --- a/src/v4/extdeps/languages/lean.dag +++ b/src/v4/extdeps/languages/lean.dag @@ -2,7 +2,7 @@ // Scope: Lean 4 language model for PROOF-1 termination export. // Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding. // Consumes: List, Bool, String. -// Status: D2-REV / Practice 8 — fixed-precision numeric facts live in `LeanScalar` `IntScalar { kind, width }` only (DECISIONS.md §D2 REVERSAL); kernel `LeanBool = Bool` + `lean_bool_grounding` only. No bare std integer aliases or spelling-only `GroundingMap` rows for ints (P4-3208 / #3208). +// Status: D2-REV; 🟢 P4-3208 — DECISIONS.md (lean scalar + ledger). module v4.extdeps.languages.lean @@ -216,10 +216,3 @@ type LeanBool = Bool data lean_bool_grounding: GroundingMap = { spelling: "Bool" } - - -// Unbounded `Nat` / `Int` and per-width fixed-precision spellings (`Int8`, …) from the Lean -// reference are **not** modeled as `type LeanX = stdX` + `GroundingMap { spelling: … }` — that -// shape is the reversed D2 hollow alias (DECISIONS.md §D2 REVERSAL; INVARIANTS.md P1 / Practice 8). -// Wire names are not structural coincidence. Fixed-precision facts live only in `LeanScalar` -// above; future unbounded / platform-width carriers land as explicit fact-bundles when needed. diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index d50a896dbc1..52b7fffc973 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -2,7 +2,7 @@ // Scope: machine-code language model parameterized by Isa. // Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, Symbol, MachineIntKind, MachineIntWidth, MachineScalar, MachineSignedDisplacement32, MachineSignedDisplacement64, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. // Consumes: List, Byte. -// Status: D2-REV / Practice 8 — ISA scalar facts in `MachineScalar` only; addressing displacements use explicit `MachineSignedDisplacement{32,64}` fact records (DECISIONS.md §D2 REVERSAL). No bare std integer aliases or spelling-only `GroundingMap` rows (P4-3208 / #3208). +// Status: D2-REV; 🟢 P4-3208 — DECISIONS.md (machine_code scalar + displacement + ledger). module v4.extdeps.languages.machine_code @@ -74,11 +74,6 @@ type MachineScalar = IntScalar { kind: MachineIntKind, width: MachineIntWidth } -// D2-REV (DECISIONS.md §D2 REVERSAL): displacement operands carry ISA signedness + width facts as -// an explicit product — not `type MachineI32 = Int32` hollow aliases. Coincidence with std -// fixed-width carriers is a separate proved obligation (U1 / T-9), not `GroundingMap { spelling: … }`. - - // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html type MachineSignedDisplacement32 { kind: MachineIntKind From 8f246e52c012ed47ba507178ea2ac751e1b68a8f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 08:31:44 +0000 Subject: [PATCH 13/16] fix(machine_code): pin disp32/disp64 width classes per api-review Disambiguate displacement records with collapsed width sums so a 32-bit-class slot cannot carry Bits64 at the type level; update P4-3208. Co-authored-by: Cursor --- src/v4/DECISIONS.md | 8 +++++--- src/v4/extdeps/languages/machine_code.dag | 18 +++++++++++++++--- 2 files changed, 20 insertions(+), 6 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 90eeddc5df4..57f98e97d03 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -268,9 +268,11 @@ checked against the Practice-4 five-pattern ledger: | `FlagWriteDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: condition-code dependency consumers read this coordinate; `Bool` cannot distinguish architectural flags vs predicate-register writes; not algebra; one instruction has one flag-write disposition; alternatives are closed. | | `MachineIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` / `LeanIntKind`: ISA-modeled signed vs unsigned is a closed alternative for fixed-width machine integers, not a coordinate; not algebra; consumers branch uniformly. | | `MachineIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` / `LeanIntWidth` with `Bits128` extension: closed width ladder for ISA fixed-width integers through 128-bit class; not algebra; not a `Symbol` width tag. | -| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — explicit `{ kind, width }` products citing SDM / ISA addressing facts; coincidence with std `Int32`/`Int64` is a separate proved obligation, not spelling. | -| `MachineSignedDisplacement32` | 🟢 GREEN terminal | D2-REV: two-field product (`MachineIntKind` × `MachineIntWidth`) models ISA addressing displacement facts for 32-bit-class encodings (SDM / ISA manuals); not a bare `Int32` alias; not one nullary coproduct arm. | -| `MachineSignedDisplacement64` | 🟢 GREEN terminal | D2-REV: same posture as `MachineSignedDisplacement32` for 64-bit absolute linear-address displacement forms. | +| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — explicit products over `MachineIntKind` plus **encoding-class-collapsed** width sums (`MachineDisplacement32WidthClass` / `MachineDisplacement64WidthClass`) so a 32-bit-class slot cannot carry `Bits64` at the type level (claude-opus api-review #14158 exploratory). | +| `MachineDisplacement32WidthClass` | 🟢 GREEN terminal | Collapses the displacement width axis to the 32-bit ISA encoding class only (`Bits32`); not a bare `Int32` alias; pairs with `MachineSignedDisplacement32`. | +| `MachineDisplacement64WidthClass` | 🟢 GREEN terminal | Collapses the width axis to the 64-bit absolute linear-address class (`Bits64`); pairs with `MachineSignedDisplacement64`. | +| `MachineSignedDisplacement32` | 🟢 GREEN terminal | D2-REV: `{ kind, width }` over `MachineDisplacement32WidthClass` — SDM / ISA 32-bit-class displacement facts without isomorphism to the 64-bit absolute carrier. | +| `MachineSignedDisplacement64` | 🟢 GREEN terminal | D2-REV: `{ kind, width }` over `MachineDisplacement64WidthClass` — 64-bit absolute displacement forms; not isomorphic to the 32-bit-class record. | ### `src/v4/extdeps/languages/cpp.dag` diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index 52b7fffc973..6304ed9a629 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -1,6 +1,6 @@ // src/v4/extdeps/languages/machine_code.dag // Scope: machine-code language model parameterized by Isa. -// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, Symbol, MachineIntKind, MachineIntWidth, MachineScalar, MachineSignedDisplacement32, MachineSignedDisplacement64, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. +// Owns: Isa, ByteOrder, InstructionLength, InstructionByteLimitRef, OperandFieldWidthRef, Symbol, MachineIntKind, MachineIntWidth, MachineScalar, MachineDisplacement32WidthClass, MachineDisplacement64WidthClass, MachineSignedDisplacement32, MachineSignedDisplacement64, InstructionWord, RegisterClass, RegisterDeclaration, RegisterRef, IndexScale, AddressingMode, Operand, ByteSequence, InstructionProductionRef, RegisterOperandSlotRef, ImmediateOperandSlotRef, MemoryOperandSlotRef, ImmediateOperandTarget, ImmediateOperandConstraint, MemoryOperandConstraint, InstructionOperandSlot, InstructionProduction, OperandBinding, DecodedInstruction, MachineFidelityFeature, MachineFidelityDisposition, MachineIntegerOverflowBehavior, MachineIntegerOperationSemantics, FlagWriteDisposition. // Consumes: List, Byte. // Status: D2-REV; 🟢 P4-3208 — DECISIONS.md (machine_code scalar + displacement + ledger). @@ -74,17 +74,29 @@ type MachineScalar = IntScalar { kind: MachineIntKind, width: MachineIntWidth } +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type MachineDisplacement32WidthClass + = Bits32 + + +// Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html +// 🟢 coproduct dissolution — DECISIONS.md P4-3208 +type MachineDisplacement64WidthClass + = Bits64 + + // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html type MachineSignedDisplacement32 { kind: MachineIntKind - width: MachineIntWidth + width: MachineDisplacement32WidthClass } // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html type MachineSignedDisplacement64 { kind: MachineIntKind - width: MachineIntWidth + width: MachineDisplacement64WidthClass } From 3987e72c49392ba10cb36066de2ff62b0ffef334 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 08:42:30 +0000 Subject: [PATCH 14/16] fix(machine_code): v2-bootstrap parse for singleton width-class sums v2 treats `type T = Foo` without `{` or `|` as a type alias; use empty record variants `Foo {}` so displacement width classes stay nominal sums and v4 CI (v2 compile all .dag) passes. Co-authored-by: Cursor --- src/v4/DECISIONS.md | 6 +++--- src/v4/extdeps/languages/machine_code.dag | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 57f98e97d03..9e441d709d9 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -268,9 +268,9 @@ checked against the Practice-4 five-pattern ledger: | `FlagWriteDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: condition-code dependency consumers read this coordinate; `Bool` cannot distinguish architectural flags vs predicate-register writes; not algebra; one instruction has one flag-write disposition; alternatives are closed. | | `MachineIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` / `LeanIntKind`: ISA-modeled signed vs unsigned is a closed alternative for fixed-width machine integers, not a coordinate; not algebra; consumers branch uniformly. | | `MachineIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` / `LeanIntWidth` with `Bits128` extension: closed width ladder for ISA fixed-width integers through 128-bit class; not algebra; not a `Symbol` width tag. | -| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — explicit products over `MachineIntKind` plus **encoding-class-collapsed** width sums (`MachineDisplacement32WidthClass` / `MachineDisplacement64WidthClass`) so a 32-bit-class slot cannot carry `Bits64` at the type level (claude-opus api-review #14158 exploratory). | -| `MachineDisplacement32WidthClass` | 🟢 GREEN terminal | Collapses the displacement width axis to the 32-bit ISA encoding class only (`Bits32`); not a bare `Int32` alias; pairs with `MachineSignedDisplacement32`. | -| `MachineDisplacement64WidthClass` | 🟢 GREEN terminal | Collapses the width axis to the 64-bit absolute linear-address class (`Bits64`); pairs with `MachineSignedDisplacement64`. | +| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — explicit products over `MachineIntKind` plus encoding-class-collapsed width sums (`MachineDisplacement32WidthClass` / `MachineDisplacement64WidthClass`, singleton record arms `DisplacementEncodingBits32 {}` / `DisplacementEncodingBits64 {}` — **empty record** so v2’s `type` parser keeps the sum-arm path; also keeps 32- vs 64-bit encoding witnesses disjoint). | +| `MachineDisplacement32WidthClass` | 🟢 GREEN terminal | Singleton encoding-class witness for 32-bit-class SDM displacement fields (`DisplacementEncodingBits32 {}` — empty record so v2’s `type` parser treats this as a sum arm, not a bare-alias RHS); not a bare `Int32` alias. | +| `MachineDisplacement64WidthClass` | 🟢 GREEN terminal | Singleton witness for 64-bit absolute linear-address displacement (`DisplacementEncodingBits64 {}`); same v2-parse shape as the 32-bit class. | | `MachineSignedDisplacement32` | 🟢 GREEN terminal | D2-REV: `{ kind, width }` over `MachineDisplacement32WidthClass` — SDM / ISA 32-bit-class displacement facts without isomorphism to the 64-bit absolute carrier. | | `MachineSignedDisplacement64` | 🟢 GREEN terminal | D2-REV: `{ kind, width }` over `MachineDisplacement64WidthClass` — 64-bit absolute displacement forms; not isomorphic to the 32-bit-class record. | diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index 6304ed9a629..5aa0297c822 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -77,13 +77,13 @@ type MachineScalar // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type MachineDisplacement32WidthClass - = Bits32 + = DisplacementEncodingBits32 {} // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html // 🟢 coproduct dissolution — DECISIONS.md P4-3208 type MachineDisplacement64WidthClass - = Bits64 + = DisplacementEncodingBits64 {} // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html From af1a865080f10c83c681953842fda38bd7ef30a5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 09:05:47 +0000 Subject: [PATCH 15/16] fix: signed-only displacement width, SG-0 path order, Lean ledger map Drop MachineIntKind from signed displacement records (nominal signedness). Lex-sort EXPECTED_HAND_AUTHORED_TEST extdeps smoke paths. P4-3208: map Lean fixed-precision anchor types onto IntScalar arms; align machine_code rows. Co-authored-by: Cursor --- src/v3/compiler/tests/integration/sg0_census_test.rs | 6 +++--- src/v4/DECISIONS.md | 8 ++++---- src/v4/extdeps/languages/machine_code.dag | 2 -- 3 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index a077b63833d..9a7147f6eae 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -830,13 +830,13 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ "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. "src/v3/compiler/tests/integration/v4_extdeps_typescript_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_machine_code_dag_smoke_test.rs", - "src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs", // T-30: `compile_to_dag` smoke on `src/v4/std/fact_density.dag` (Practice 8 // structural mirror in `v4_hollow_alias_gate`). SG-0 + INVARIANTS §P5(b) receipt. "src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs", diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 9e441d709d9..fb68e39dc4b 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -244,7 +244,7 @@ checked against the Practice-4 five-pattern ledger: | `LeanFidelityDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: modeled/normalized/fail-closed is the shared C5 disposition; non-modeled variants carry feature payloads and a flat record admits impossible combinations; not algebra; one feature has one disposition; payloads are heterogeneous. | | `LeanIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` (`rust.dag`, DECISIONS.md Part 6 / CP-3229): signed vs unsigned is a closed external alternative for fixed-precision scalars, not a hideable coordinate; not algebra; not one `F` family over identical payloads. | | `LeanIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` (`rust.dag`): closed width ladder for fixed-precision scalars; `Pointer` names platform-sized facts separately from fixed bit widths; not algebra; not a `Symbol` tag. | -| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts read from the Lean 4.20 anchor; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling only (**D2-REV**). Per-width std aliases + spelling-only `GroundingMap` rows for integers are **omitted** — they were the reversed-D2 hollow shape; unbounded / platform-width Lean numerics are deferred until modeled as explicit fact-bundles. | +| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts read from the Lean 4.20 anchor; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling only (**D2-REV**). **Signed** fixed-precision surface types from the anchor (`Int8`…`Int64`, `ISize`) inhabit `IntScalar { kind: Signed, width: … }` (use the `Pointer` width arm for `ISize` per anchor); **unsigned** (`UInt8`…`UInt64`, `USize`) inhabit `IntScalar { kind: Unsigned, width: … }`. Per-name std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow); unbounded `Nat`/`Int` are deferred until explicit fact-bundles. | ### `src/v4/extdeps/languages/machine_code.dag` @@ -268,11 +268,11 @@ checked against the Practice-4 five-pattern ledger: | `FlagWriteDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: condition-code dependency consumers read this coordinate; `Bool` cannot distinguish architectural flags vs predicate-register writes; not algebra; one instruction has one flag-write disposition; alternatives are closed. | | `MachineIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` / `LeanIntKind`: ISA-modeled signed vs unsigned is a closed alternative for fixed-width machine integers, not a coordinate; not algebra; consumers branch uniformly. | | `MachineIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` / `LeanIntWidth` with `Bits128` extension: closed width ladder for ISA fixed-width integers through 128-bit class; not algebra; not a `Symbol` width tag. | -| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — explicit products over `MachineIntKind` plus encoding-class-collapsed width sums (`MachineDisplacement32WidthClass` / `MachineDisplacement64WidthClass`, singleton record arms `DisplacementEncodingBits32 {}` / `DisplacementEncodingBits64 {}` — **empty record** so v2’s `type` parser keeps the sum-arm path; also keeps 32- vs 64-bit encoding witnesses disjoint). | +| `MachineScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` (`rust.dag`): kind×width bundles ISA scalar facts (**D2-REV**). Per-width `MachineI*` / `MachineU*` std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow). `AddressingMode` **signed** displacement slots use `MachineSignedDisplacement32` / `MachineSignedDisplacement64` — **width-only** records over encoding-class witnesses (`MachineDisplacement32WidthClass` / `MachineDisplacement64WidthClass` with singleton `DisplacementEncodingBits32 {}` / `DisplacementEncodingBits64 {}`); signedness is **nominal** in the carrier name (no `MachineIntKind` field — cannot spell `Unsigned` on these SDM signed-displacement paths). | | `MachineDisplacement32WidthClass` | 🟢 GREEN terminal | Singleton encoding-class witness for 32-bit-class SDM displacement fields (`DisplacementEncodingBits32 {}` — empty record so v2’s `type` parser treats this as a sum arm, not a bare-alias RHS); not a bare `Int32` alias. | | `MachineDisplacement64WidthClass` | 🟢 GREEN terminal | Singleton witness for 64-bit absolute linear-address displacement (`DisplacementEncodingBits64 {}`); same v2-parse shape as the 32-bit class. | -| `MachineSignedDisplacement32` | 🟢 GREEN terminal | D2-REV: `{ kind, width }` over `MachineDisplacement32WidthClass` — SDM / ISA 32-bit-class displacement facts without isomorphism to the 64-bit absolute carrier. | -| `MachineSignedDisplacement64` | 🟢 GREEN terminal | D2-REV: `{ kind, width }` over `MachineDisplacement64WidthClass` — 64-bit absolute displacement forms; not isomorphic to the 32-bit-class record. | +| `MachineSignedDisplacement32` | 🟢 GREEN terminal | D2-REV: SDM / ISA **signed** 32-bit-class displacement — single `width` witness; not isomorphic to the 64-bit absolute carrier; not a free `MachineIntKind` product. | +| `MachineSignedDisplacement64` | 🟢 GREEN terminal | D2-REV: **signed** 64-bit-class absolute linear-address displacement — single `width` witness; same posture as `MachineSignedDisplacement32`. | ### `src/v4/extdeps/languages/cpp.dag` diff --git a/src/v4/extdeps/languages/machine_code.dag b/src/v4/extdeps/languages/machine_code.dag index 5aa0297c822..b932eac6788 100644 --- a/src/v4/extdeps/languages/machine_code.dag +++ b/src/v4/extdeps/languages/machine_code.dag @@ -88,14 +88,12 @@ type MachineDisplacement64WidthClass // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html type MachineSignedDisplacement32 { - kind: MachineIntKind width: MachineDisplacement32WidthClass } // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html type MachineSignedDisplacement64 { - kind: MachineIntKind width: MachineDisplacement64WidthClass } From 7b4d50213b9aa901e8085f6e837ff9e3ac19885f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 10:01:20 +0000 Subject: [PATCH 16/16] fix(cpp): C++ lex.key anchor for CppBool + P4-3208 authority receipt Add WG21 draft anchor on cpp_bool surface; ledger cites C++ spec, not RustBool, as coincidence authority (api-review / INVARIANTS P1 cite). Co-authored-by: Cursor --- src/v4/DECISIONS.md | 2 +- src/v4/extdeps/languages/cpp.dag | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index fb68e39dc4b..275cc785443 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -280,7 +280,7 @@ Non-Bool C++ scalar ladder in this slice: **tracked** — 🟡 `feature:t4-cpp-s | Carrier | Classification | Ledger result | |---------|----------------|---------------| -| `CppBool` | 🟢 GREEN terminal | Same dissolution posture as `RustBool` (`rust.dag`): kernel `CppBool = Bool` + `cpp_bool_grounding` cites std coincidence for the C++ `bool` spelling (Practice 8 / D2-REV). | +| `CppBool` | 🟢 GREEN terminal | **C++ authority:** ISO C++ `bool` keyword / fundamental boolean type (`https://eel.is/c++draft/lex.key` — mirrored by `cpp.dag` `Anchor:`). `CppBool = Bool` + `cpp_bool_grounding { spelling: \"bool\" }` is the lexical spelling read for kernel-ambient `Bool` coincidence (Practice 8 / D2-REV). `rust.dag` `RustBool` is a sibling pattern only, not the C++ spec source. | ## OS-1 — #3209 Coproduct Dissolution And Scaffold Record diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag index 70f5540d0d0..9c01a46167a 100644 --- a/src/v4/extdeps/languages/cpp.dag +++ b/src/v4/extdeps/languages/cpp.dag @@ -22,6 +22,8 @@ type CppIntegerOverflowDisposition = RepresentableResultRequired | UnsignedModuloArithmetic + +// Anchor: https://eel.is/c++draft/lex.key type CppBool = Bool data cpp_bool_grounding: GroundingMap = {