T-Ground Pilot

Cargo.toml

@@ -8,6 +8,10 @@ members = [
     "src/v2/tests",
     # v3 compiler — M0: hand-written substrate skeleton
     "src/v3/compiler",
+    # T-Ground-Pilot probe — bounded inhabitance-search routing pilot
+    # for the Rust target. Sibling crate so the probe lifecycle is
+    # isolated and the v3-compiler SG-0 ratchet is untouched.
+    "src/v3/grounding_pilot",
     # v1 compiler — ARCHIVED. No longer in the build or generation path.
     # Retained in src/v1/ for historical reference. Can be deleted.
 ]

dsl/extdeps/languages/rust/primitives.dag

@@ -0,0 +1,246 @@
+// extdeps/languages/rust/primitives.dag -- Structural target-primitive
+// declarations for the Rust target.
+//
+// PILOT SCOPE (T-Ground-Pilot): {i8, i16, i32, i64, u8, u16, u32, u64,
+// bool, ()} only. No containers, no floats, no coercion paths.
+//
+// PURPOSE: Each declaration says "Rust target type T is a target primitive
+// inhabiting algebra A over carrier C." Selection by algebra-homomorphism
+// match — the toy engine in src/v3/grounding_pilot/src/lib.rs reproduces
+// today's name-keyed table-lookup routing on the pilot set, validating
+// the target-grounding-proposal.md thesis that "the mapping should fall
+// out from the algebra, not from a hand-maintained table."
+//
+// CONSUMER BOUNDARY (HONEST STATE): the engine does NOT yet read this
+// .dag file directly. It mirrors the structural facts authored here as
+// Rust constants, with this file as the documented authority. Wiring the
+// engine to consume .dag declarations as parsed-data is T-Ground-Engine's
+// production-walker job; until then the mirror in
+// src/v3/grounding_pilot/src/lib.rs must be kept in sync by hand when
+// declarations here change. The duplication is bounded — pilot scope is
+// 10 primitives, parallel-existence, deletable as a unit when
+// T-Ground-Engine lands and removes both this file's parallel-existence
+// status and the pilot crate together.
+//
+// LANES:
+//   This file is parallel-existence. Dissolution of
+//   dsl/extdeps/languages/rust/types.dag (TypeCheckpoint name-keyed table
+//   + InhabitantDecl algebra-keyed fallback) is T-Ground-Dissolve scope,
+//   not Pilot.
+//
+// SOURCE AUTHORITY:
+//   Rust Reference §Types — https://doc.rust-lang.org/reference/types.html
+//     §3.4 Numeric types         (i8/i16/i32/i64, u8/u16/u32/u64)
+//     §3.5 Boolean type          (bool)
+//     §3.7 Tuple types           (() as the empty tuple / unit)
+//   This is language-level grounding (Rust Reference, not stdlib) — the
+//   two-authority discipline (language reference vs stdlib) starts here.
+//
+// SUBSTRATE-GAP FLAGS (DB-11 will sharpen):
+//   1. `IntegerOverflow` carries two's-complement-wrap as a closed-enum
+//      value field on the `IntegerPrimitive` variant. Post-DB-11 this
+//      becomes a where-clause refinement on the algebra carrier (e.g.
+//      OrderedRing<Word64> where overflow = TwoComplementWrap), and
+//      under T-Ground-Engine refinement is per-operator (debug vs
+//      release for +/-/*; `/` and `%` panic on int::MIN/-1 regardless;
+//      `wrapping_*`/`checked_*`/`saturating_*` are explicit operator
+//      selections per Rust Reference §"overflow"). Today the language
+//      doesn't yet support first-class refinement qualifiers on type
+//      aliases, so the cleanest structural shape is a per-variant
+//      carried enum, with the integer/non-integer split handled by
+//      sum-typing `RustPrimitive` so overflow is structurally absent
+//      where it would be nonsensical (no `bool: Some(TwoComplementWrap)`,
+//      no `i64: None`).
+//   2. `IntegerAlgebra` / `NonIntegerAlgebra` / `TargetCarrier` enums
+//      identify std/algebra.dag and std/bit.dag concepts by structural
+//      tag rather than as first-class type-references-as-data. The .dag
+//      substrate doesn't yet expose type expressions as data values
+//      (data-table fields can't be `algebra: OrderedRing` with OrderedRing
+//      referenced as a
+//      type identity). When that closes — co-temporally with the
+//      types.dag/coercion.dag dissolution under T-Ground-Dissolve — these
+//      tag enums collapse into direct algebra-and-carrier references and
+//      this file shrinks accordingly.
+//   3. Unit modeled with `TerminalAlgebra` / `TerminalCarrier` sentinels.
+//      Post-DB-11 this becomes Cardinality<T, Exactly(1)>; the terminal
+//      object is the canonical inhabitant. Pilot uses the sentinel pair
+//      because cardinality-substrate is not yet available (out-of-scope
+//      per brief: "Container types — block on cardinality-substrate.").
+
+module extdeps.languages.rust.primitives
+
+import std.algebra { OrderedRing, Semiring, BooleanAlgebra }
+import std.bit { Bit, Byte, Word16, Word32, Word64 }
+
+
+// =========================================================================
+// Algebra tags, partitioned by overflow-bearing class.
+//
+// Closed enumerations identifying which std/algebra.dag structure a target
+// primitive inhabits. Partitioned into integer-bearing and non-integer-
+// bearing subtypes so that overflow facts attach only where they have
+// meaning — making `bool: Some(TwoComplementWrap)` and `i64: None`
+// structurally unrepresentable rather than ruled out by convention
+// (state-space modeling discipline; no validation passes).
+//
+//   IntegerAlgebra
+//     OrderedRingAlgebra  <-> std.algebra.OrderedRing<C>    (signed integers)
+//     SemiringAlgebra     <-> std.algebra.Semiring<C>       (unsigned integers)
+//
+//   NonIntegerAlgebra
+//     BooleanAlgebraAlgebra<-> std.algebra.BooleanAlgebra<C> (Bool)
+//     TerminalAlgebra      <-> single-inhabitant terminal    (Unit; DB-11)
+//
+// Substrate-gap flag #2: these tags are bridges to algebra references.
+// =========================================================================
+
+type IntegerAlgebra
+  = OrderedRingAlgebra
+  | SemiringAlgebra
+
+type NonIntegerAlgebra
+  = BooleanAlgebraAlgebra
+  | TerminalAlgebra
+
+
+// =========================================================================
+// Target carrier tag.
+//
+// Closed enumeration identifying which std/bit.dag carrier (or terminal)
+// the target primitive's **algebra value-domain witness** corresponds to,
+// per the std convention declared in `dsl/std/integer.dag:4` ("Int is a
+// CARRIER (Word64) with EVIDENCE that it inhabits OrderedRing"):
+//   BitCarrier     <-> std.bit.Bit         (BooleanAlgebra value-domain: 2-element set)
+//   ByteCarrier    <-> std.bit.Byte        (Ring/Semiring value-domain over 2^8)
+//   Word16Carrier  <-> std.bit.Word16      (Ring/Semiring value-domain over 2^16)
+//   Word32Carrier  <-> std.bit.Word32      (Ring/Semiring value-domain over 2^32)
+//   Word64Carrier  <-> std.bit.Word64      (Ring/Semiring value-domain over 2^64)
+//   TerminalCarrier<-> single inhabitant   (Unit; DB-11 -> Cardinality 1)
+//
+// NOT target storage layout. Rust's `bool` storage is 1 byte with only
+// 0x00 and 0x01 valid (Rust Reference §3.5), but its algebra value-domain
+// is the 2-element {⊤, ⊥} carried by Bit. Storage layout, ABI, and
+// validity bytes are a distinct axis the pilot deliberately doesn't
+// model — they're target-codegen concerns scoped to T-Ground-Engine /
+// emit-pipeline, not to the structural target-grounding routing the
+// pilot probes.
+//
+// Substrate-gap flag #2: these tags are bridges to type references.
+// =========================================================================
+
+type TargetCarrier
+  = BitCarrier
+  | ByteCarrier
+  | Word16Carrier
+  | Word32Carrier
+  | Word64Carrier
+  | TerminalCarrier
+
+
+// =========================================================================
+// Integer overflow semantics.
+//
+// All Rust integer primitives in release mode wrap on overflow per
+// two's-complement; debug mode panics on overflow. This is uniform across
+// i8..u64 and so does not affect routing within the pilot set, but is
+// declared structurally rather than left implicit because the
+// target-grounding-proposal.md worked example calls it out as a
+// declared-fact (proposal lines 174-210).
+//
+// Substrate-gap flag #1: post-DB-11 this becomes a where-clause refinement
+// on the algebra carrier rather than a separate enum field.
+// =========================================================================
+
+type IntegerOverflow
+  = TwoComplementWrap
+  | Saturating
+  | Trap
+
+
+// =========================================================================
+// Rust target-primitive declaration.
+//
+// Sum-typed so the integer/non-integer split is structural, not
+// conventional: overflow is a field on IntegerPrimitive and structurally
+// absent on NonIntegerPrimitive. State-space discipline — no
+// `bool: Some(TwoComplementWrap)`, no `i64: None`. is_copy carries on
+// both variants (target-specific Copy-trait fact consumed downstream by
+// sharing/Rc decisions). overflow carries on IntegerPrimitive only
+// (T-Ground L4-(C) witness consumer; substrate-gap flag #1 names DB-11
+// dissolution to a where-clause refinement on the algebra carrier).
+// =========================================================================
+
+type RustPrimitive
+  = IntegerPrimitive {
+      target_name: String          // Rust syntactic token: "i8".."i64", "u8".."u64"
+      algebra: IntegerAlgebra
+      carrier: TargetCarrier
+      is_copy: Bool
+      overflow: IntegerOverflow
+    }
+  | NonIntegerPrimitive {
+      target_name: String          // Rust syntactic token: "bool", "()"
+      algebra: NonIntegerAlgebra
+      carrier: TargetCarrier
+      is_copy: Bool
+    }
+
+
+// =========================================================================
+// Pilot-set declarations.
+//
+// Ordering: signed integers (i8..i64), unsigned integers (u8..u64), bool,
+// (). No other types in pilot scope.
+// =========================================================================
+
+data rust_pilot_primitives: List<RustPrimitive> = [
+  // -- Signed integers : OrderedRing over machine-word carriers ----------
+  // Rust Reference §3.4. signed = additive inverse exists (negate in
+  // OrderedRing). Wrap is the release-mode semantics.
+
+  IntegerPrimitive { target_name: "i8",  algebra: OrderedRingAlgebra, carrier: ByteCarrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+  IntegerPrimitive { target_name: "i16", algebra: OrderedRingAlgebra, carrier: Word16Carrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+  IntegerPrimitive { target_name: "i32", algebra: OrderedRingAlgebra, carrier: Word32Carrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+  IntegerPrimitive { target_name: "i64", algebra: OrderedRingAlgebra, carrier: Word64Carrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+
+  // -- Unsigned integers : Semiring over machine-word carriers -----------
+  // Rust Reference §3.4. unsigned = no additive inverse (no negate in
+  // Semiring). Distinguished from signed by algebra tag, not by carrier.
+
+  IntegerPrimitive { target_name: "u8",  algebra: SemiringAlgebra, carrier: ByteCarrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+  IntegerPrimitive { target_name: "u16", algebra: SemiringAlgebra, carrier: Word16Carrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+  IntegerPrimitive { target_name: "u32", algebra: SemiringAlgebra, carrier: Word32Carrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+  IntegerPrimitive { target_name: "u64", algebra: SemiringAlgebra, carrier: Word64Carrier,
+    is_copy: true, overflow: TwoComplementWrap },
+
+
+  // -- Bool : BooleanAlgebra over Bit -----------------------------------
+  // Rust Reference §3.5. The canonical two-element Boolean algebra; carrier
+  // is a single Bit.
+
+  NonIntegerPrimitive { target_name: "bool", algebra: BooleanAlgebraAlgebra, carrier: BitCarrier,
+    is_copy: true },
+
+
+  // -- Unit : terminal object -------------------------------------------
+  // Rust Reference §3.7 (empty tuple). DB-11 substrate gap flag #3:
+  // TerminalAlgebra/TerminalCarrier are sentinels for the not-yet-modeled
+  // Cardinality<T, Exactly(1)> refinement.
+
+  NonIntegerPrimitive { target_name: "()", algebra: TerminalAlgebra, carrier: TerminalCarrier,
+    is_copy: true }
+]

src/v3/grounding_pilot/Cargo.toml

@@ -0,0 +1,26 @@
+[package]
+name = "v3-grounding-pilot"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+
+# T-Ground-Pilot — bounded probe validating that algebra-homomorphism
+# inhabitance search reproduces today's name-keyed table-lookup routing
+# on a 10-element Rust pilot set ({i8..i64, u8..u64, bool, ()}).
+#
+# Scope: src/v3/grounding_pilot/src/lib.rs. Authority for the structural
+# target-side facts: dsl/extdeps/languages/rust/primitives.dag.
+#
+# Lives as a sibling crate (not a module of v3-compiler) so the probe's
+# lifecycle is fully isolated:
+#   - zero compiler-internal dependencies; nothing in here couples to the
+#     production pipeline
+#   - SG-0 ratchet on src/v3/compiler is untouched; admission of new
+#     hand-Rust into the pilot probe doesn't drift that ratchet
+#   - "deletable as a unit" is literal: when T-Ground-Engine produces the
+#     production walker, this entire crate disappears alongside removal
+#     from workspace members
+#
+# No dependencies — the probe is pure structural data + free functions.
+
+[dependencies]