T-Ground Pilot

dsl/extdeps/languages/rust/primitives.dag

@@ -0,0 +1,198 @@
+// 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/compiler/src/pilot/grounding_pilot.rs
+// consumes these declarations and 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."
+//
+// 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. Post-DB-11 this becomes a where-clause refinement on
+//      the algebra carrier (e.g. OrderedRing<Word64> where overflow =
+//      TwoComplementWrap). Today the language doesn't yet support
+//      first-class refinement qualifiers on type aliases, so the cleanest
+//      structural shape is a carried enum.
+//   2. `TargetAlgebra` / `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 }
+
+
+// =========================================================================
+// Target algebra tag.
+//
+// Closed enumeration identifying which std/algebra.dag structure a target
+// primitive inhabits. Each variant corresponds 1:1 to a std/algebra.dag
+// declaration:
+//   OrderedRingAlgebra   <-> std.algebra.OrderedRing<C>     (signed)
+//   SemiringAlgebra      <-> std.algebra.Semiring<C>        (unsigned)
+//   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 TargetAlgebra
+  = OrderedRingAlgebra
+  | SemiringAlgebra
+  | BooleanAlgebraAlgebra
+  | TerminalAlgebra
+
+
+// =========================================================================
+// Target carrier tag.
+//
+// Closed enumeration identifying which std/bit.dag carrier (or terminal)
+// the target primitive's underlying machine representation corresponds to:
+//   BitCarrier     <-> std.bit.Bit         (1-bit truth value)
+//   ByteCarrier    <-> std.bit.Byte        (8 bits)
+//   Word16Carrier  <-> std.bit.Word16      (16 bits)
+//   Word32Carrier  <-> std.bit.Word32      (32 bits)
+//   Word64Carrier  <-> std.bit.Word64      (64 bits)
+//   TerminalCarrier<-> single inhabitant   (Unit; DB-11 -> Cardinality 1)
+//
+// 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.
+//
+// Single record carrying the structural facts about one Rust target
+// primitive. Selection is by structural agreement on (algebra, carrier);
+// is_copy and overflow are target-specific qualifiers consumed downstream
+// (is_copy by sharing/Rc decisions; overflow by laws verification, T-Ground
+// L4-(C) witness scope).
+// =========================================================================
+
+type RustPrimitive {
+  target_name: String          // Rust syntactic token: "i64", "bool", "()"
+  algebra: TargetAlgebra
+  carrier: TargetCarrier
+  is_copy: Bool
+  overflow: IntegerOverflow?   // none for non-integer primitives
+}
+
+
+// =========================================================================
+// 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.
+
+  { target_name: "i8",  algebra: OrderedRingAlgebra, carrier: ByteCarrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+  { target_name: "i16", algebra: OrderedRingAlgebra, carrier: Word16Carrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+  { target_name: "i32", algebra: OrderedRingAlgebra, carrier: Word32Carrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+  { target_name: "i64", algebra: OrderedRingAlgebra, carrier: Word64Carrier,
+    is_copy: true, overflow: Some { value: 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.
+
+  { target_name: "u8",  algebra: SemiringAlgebra, carrier: ByteCarrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+  { target_name: "u16", algebra: SemiringAlgebra, carrier: Word16Carrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+  { target_name: "u32", algebra: SemiringAlgebra, carrier: Word32Carrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+  { target_name: "u64", algebra: SemiringAlgebra, carrier: Word64Carrier,
+    is_copy: true, overflow: Some { value: TwoComplementWrap } },
+
+
+  // -- Bool : BooleanAlgebra over Bit -----------------------------------
+  // Rust Reference §3.5. The canonical two-element Boolean algebra; carrier
+  // is a single Bit.
+
+  { target_name: "bool", algebra: BooleanAlgebraAlgebra, carrier: BitCarrier,
+    is_copy: true, overflow: none },
+
+
+  // -- 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.
+
+  { target_name: "()", algebra: TerminalAlgebra, carrier: TerminalCarrier,
+    is_copy: true, overflow: none }
+]

src/v3/compiler/src/pilot/mod.rs

@@ -0,0 +1,19 @@
+// Pilot-scope probes. Code in this module is explicitly *not* part of the
+// production v3 compiler pipeline — each submodule is a bounded experiment
+// validating a design hypothesis, scoped per its worker brief, and either
+// promotes into the main compiler (with its own dissolution lane) or
+// escalates findings back to its manager.
+//
+// Add new probes only when a worker brief explicitly authorizes
+// pilot-scoped code. Pilot modules must:
+//   - be named after the brief (e.g., grounding_pilot)
+//   - carry a header pointing to the brief and its escalation path
+//   - never modify production substrate or pipeline stages
+//   - be deletable as a unit when the probe completes
+//
+// Active probes:
+//   grounding_pilot -- T-Ground-Pilot worker brief; validates that
+//     algebra-homomorphism inhabitance search reproduces today's
+//     name-keyed table-lookup routing on a 10-element Rust pilot set.
+
+pub mod grounding_pilot;