W<n> machine-word type + surface add_into prim (ADR-0047)

README.md

@@ -67,11 +67,12 @@ stays flat.
 
 **On real programs.** Compiled programs inherit the win. Priced at a fixed ramp,
 a reversible program's total energy sits far below the CMOS-equivalent gate
-count charged at `1/2 CV^2` -- e.g. the Fibonacci ROM costs roughly an order
-of magnitude less.
+count charged at `1/2 CV^2` -- e.g. a byte-wide (U8) Fibonacci ROM, ten
+reversible `(a, b) |-> (b, a + b mod 256)` steps each compiling to the
+two-word datapath `EXCH ; ADD`, costs well over an order of magnitude less.
 
 <p align="center">
-  <img src="docs/img/benchmark-energy.svg" width="720" alt="Per-benchmark energy: reversible total vs CMOS-equivalent baseline for fib and adder."><br>
+  <img src="docs/img/benchmark-energy.svg" width="720" alt="Per-benchmark energy: reversible total vs CMOS-equivalent baseline for a U8 Fibonacci and a half-adder."><br>
   <em>Whole-program energy, reversible vs CMOS-equivalent, at a fixed power-clock ramp.</em>
 </p>
 

conformance/programs/0027-fib8.expect

@@ -0,0 +1,5 @@
+# iso: fib8
+(0, 1) |-> (2, 3)
+(13, 21) |-> (55, 89)
+(200, 100) |-> (144, 188)
+(1, 0) |-> (1, 2)

conformance/programs/0027-fib8.thse

@@ -0,0 +1,20 @@
+-- Conformance P0027 (dialect: synthesizable, ADR-0047 W<n> + add_into prim)
+-- Byte-wide Fibonacci: three steps of the U8 fib iteration over the machine
+-- word W8, composed explicitly (constant count, like 0023-fib3 but full-byte).
+--
+-- The step is the reversible bijection (a, b) |-> (b, a + b mod 256), built as
+-- `swap2 ; add_into`, where `add_into` is the builtin reversible word-add prim
+-- (a Flat(8) leaf per operand -> a single TISC `Add` instruction).
+--
+--   (0, 1)     -> (1, 1) -> (1, 2) -> (2, 3)
+--   (13, 21)   -> (21, 34) -> (34, 55) -> (55, 89)
+--   (200, 100) -> (100, 44) -> (44, 144) -> (144, 188)   (carry wraps mod 256)
+
+prim add_into : W8 * W8 <-> W8 * W8 = "theseus.arith.add_into"
+
+iso swap2 : W8 * W8 <-> W8 * W8
+| (a, b) <-> (b, a)
+
+iso fibStep : W8 * W8 <-> W8 * W8 = swap2 ; add_into
+
+iso fib8 : W8 * W8 <-> W8 * W8 = fibStep ; fibStep ; fibStep

crates/theseus-check/src/elaborate.rs

@@ -99,7 +99,12 @@ fn elab_expr(
         Expr::Paren(inner, _) => elab_expr(inner, env, isos, iso_lhs),
         Expr::Var(name) => match isos.get(&name.text) {
             Some(iso) => elab_iso(iso, env, isos),
-            None => unsupported(),
+            // Not an iso -- a reference to a declared `prim` resolves via the
+            // builtin registry against its declared (lowered) types (ADR-0047).
+            None => match env.prim(&name.text) {
+                Some(sig) => elab_prim_ref(sig, env),
+                None => unsupported(),
+            },
         },
         Expr::Adjoint(inner, _) => Ok(Iso::sym(elab_expr(inner, env, isos, None)?)),
         Expr::Bin(op, l, r, _) => {
@@ -155,6 +160,32 @@ fn elab_expr(
     }
 }
 
+/// Elaborate a reference to a declared `prim` (ADR-0047): lower its declared
+/// LHS/RHS types, resolve the key against the builtin registry, and admit the
+/// resulting `(forward, backward)` pair (mutual-inverse over the finite domain)
+/// before wrapping it in `Iso::Prim`. An unknown key, or a type the builtin
+/// does not support, elaborates to `unsupported()` (an empty-diagnostic sentinel
+/// -- the surrounding type/coverage checks report the user-facing error).
+fn elab_prim_ref(sig: &crate::env::PrimSig, env: &Env) -> ElabResult {
+    let in_ty = env.lower(&sig.lhs);
+    let out_ty = env.lower(&sig.rhs);
+    let Some(def) = theseus_core::prim::builtin_prim(&sig.key, &in_ty, &out_ty) else {
+        return unsupported();
+    };
+    // Guard the def before wrapping. A symbolic-only prim (builtins carry a
+    // `PrimSpec`, no table) cannot be certified by `core::admit` -- validate its
+    // spec structurally here; full mutual-inverse certification is the compiler's
+    // symbolic BVEQ. A table prim (should one appear) still runs `admit`.
+    let admissible = match &def.symbolic {
+        Some(spec) => spec.validate_against(&def.input_ty, &def.output_ty).is_ok(),
+        None => theseus_core::prim::admit(&def).is_ok(),
+    };
+    if !admissible {
+        return unsupported();
+    }
+    Ok(Iso::Prim(Box::new(def)))
+}
+
 /// Position type inference for `id` as a combinator body (ADR-0038).
 ///
 /// Given `iter T id` (or `fold`/`unfold T id`) and the iso's declared LHS type,

crates/theseus-check/src/env.rs

@@ -300,10 +300,14 @@ impl Env {
     /// Lower a named ADT into its right-nested sum-of-products, spending one
     /// unit of the name's per-path unroll budget (μ-cutoff ⇒ `Zero`).
     fn lower_named(&self, name: &str, fuel: &mut BTreeMap<String, usize>) -> CoreType {
-        // Builtin U<n> types are not user-declared; intercept before ADT lookup.
+        // Builtin U<n>/W<n> types are not user-declared; intercept before ADT
+        // lookup.
         if let Some(ct) = lower_un(name) {
             return ct;
         }
+        if let Some(ct) = lower_wn(name) {
+            return ct;
+        }
         let Some(info) = self.types.get(name) else {
             // Unknown type: total fallback. Names reports the real error.
             return CoreType::Zero;
@@ -378,11 +382,11 @@ pub(crate) fn navigate<'a>(value: &'a Value, path: &[Inj]) -> Option<&'a Value>
     Some(v)
 }
 
-/// The blessed stdlib numeric types `U<n>` (ADR-0017): `U1`, `U2`, `U4`, `U8`,
-/// `U16`, ... -- builtin, not user-declared, so name resolution treats them as
-/// known.
+/// The blessed stdlib builtin types: the numeric types `U<n>` (ADR-0017) and the
+/// machine-word types `W<n>` (ADR-0047). Both are builtin, not user-declared, so
+/// name resolution treats them as known.
 fn is_builtin_type(name: &str) -> bool {
-    parse_un_bits(name).is_some()
+    parse_un_bits(name).is_some() || parse_wn_bits(name).is_some()
 }
 
 /// Parse a `U<n>` name and return the bit-width `n` if it is a valid builtin
@@ -423,6 +427,34 @@ fn lower_un_bits(n: u32) -> CoreType {
     }
 }
 
+/// Parse a `W<n>` machine-word name and return the bit-width `n` if valid
+/// (a power of two in `1..=8`). See [`lower_wn`] for the representation.
+fn parse_wn_bits(name: &str) -> Option<u8> {
+    let digits = name.strip_prefix('W')?;
+    // Only the canonical decimal form is a builtin: no empty suffix, no leading
+    // zeros (`W08` is not `W8` -- it stays an ordinary, unknown type name).
+    if digits.is_empty() || (digits.len() > 1 && digits.starts_with('0')) {
+        return None;
+    }
+    let n: u32 = digits.parse().ok()?;
+    // A machine word is a single ISA register, so it caps at the byte width 8.
+    if n == 0 || n > 8 || !n.is_power_of_two() {
+        return None;
+    }
+    Some(n as u8)
+}
+
+/// Lower a `W<n>` machine-word type to its core encoding (ADR-0047).
+///
+/// Unlike the tree-encoded numeric `U<n>` (which is `1+1` bits nested by
+/// products), a `W<n>` lowers to a single packed [`CoreType::Flat`] leaf -- one
+/// ISA register. That single-leaf shape is what lets the compiler recognize
+/// register-native word operations (e.g. the `add_into` prim → one reversible
+/// `Add`). Capped at 8 bits: one register is byte-wide.
+fn lower_wn(name: &str) -> Option<CoreType> {
+    parse_wn_bits(name).map(CoreType::Flat)
+}
+
 /// Build the resolution environment for a program.
 ///
 /// Resolution itself does not emit diagnostics, but it records iso-name
@@ -669,6 +701,31 @@ mod tests {
         assert!(parse_un_bits("U5").is_none());
     }
 
+    #[test]
+    fn wn_word_type_parses_and_lowers_to_flat() {
+        // Valid W<n>: power of two in 1..=8, one Flat leaf.
+        for n in [1u8, 2, 4, 8] {
+            let name = format!("W{n}");
+            assert_eq!(parse_wn_bits(&name), Some(n), "parse {name}");
+            assert_eq!(lower_wn(&name), Some(CoreType::Flat(n)), "lower {name}");
+            assert!(is_builtin_type(&name), "{name} must be a builtin type");
+        }
+        // W8 has 256 inhabitants (one packed byte), unlike the U8 bit-tree.
+        assert_eq!(enumerate_values(&lower_wn("W8").unwrap()).len(), 256);
+    }
+
+    #[test]
+    fn wn_rejects_non_power_of_two_and_over_byte() {
+        assert!(parse_wn_bits("W3").is_none()); // not a power of two
+        assert!(parse_wn_bits("W0").is_none()); // zero width
+        assert!(parse_wn_bits("W16").is_none()); // exceeds the byte-wide register
+        assert!(parse_wn_bits("W").is_none()); // no digits
+        assert!(parse_wn_bits("W08").is_none()); // leading zero is not canonical
+        assert!(parse_wn_bits("W008").is_none());
+        assert!(!is_builtin_type("W16"));
+        assert!(!is_builtin_type("W08"));
+    }
+
     #[test]
     fn duplicate_iso_name_detected_as_collision() {
         // Two where-isos with the same name should be detected, not silently

crates/theseus-cli/src/value.rs

@@ -143,6 +143,18 @@ fn is_un_type(name: &str) -> bool {
         .is_some_and(|n| n > 0 && n.is_power_of_two())
 }
 
+/// Is `name` a builtin `W<n>` machine-word type (power-of-two width in 1..=8)?
+/// Like `U<n>`, its values marshal to/from decimal numeric literals.
+fn is_wn_type(name: &str) -> bool {
+    match name.strip_prefix('W') {
+        // Canonical decimal only: reject empty and leading-zero forms (`W08`).
+        Some(d) if !d.is_empty() && (d.len() == 1 || !d.starts_with('0')) => d
+            .parse::<u32>()
+            .is_ok_and(|n| n > 0 && n <= 8 && n.is_power_of_two()),
+        _ => false,
+    }
+}
+
 // ── Surface→Core conversion ──────────────────────────────────────────────
 
 /// Convert a surface value to a core [`Value`], guided by the surface [`Type`]
@@ -183,10 +195,10 @@ fn tuple_to_core(elems: &[SVal], ty: &Type, env: &Env) -> Value {
 }
 
 fn ctor_to_core(name: &str, args: &[SVal], ty: &Type, env: &Env) -> Value {
-    // Numeric literal at a U<n> type: the k-th enumerated value.
+    // Numeric literal at a U<n>/W<n> type: the k-th enumerated value.
     if is_numeric(name) && args.is_empty() {
         if let Type::Name(n) = strip_paren_ty(ty) {
-            if is_un_type(&n.text) {
+            if is_un_type(&n.text) || is_wn_type(&n.text) {
                 let k: usize = name
                     .parse()
                     .unwrap_or_else(|_| panic!("bad numeric literal: {name}"));
@@ -258,8 +270,9 @@ pub fn render(v: &Value, ty: &Type, env: &Env) -> String {
 }
 
 fn render_named(v: &Value, type_name: &str, env: &Env) -> String {
-    // U<n> builtin: render as the numeric index of the value in the enumeration.
-    if is_un_type(type_name) {
+    // U<n>/W<n> builtin: render as the numeric index of the value in the
+    // enumeration.
+    if is_un_type(type_name) || is_wn_type(type_name) {
         let ty = Type::Name(theseus_syntax::ast::UpperName {
             text: type_name.into(),
             span: theseus_syntax::ast::Span { start: 0, end: 0 },

crates/theseus-core/src/prim.rs

@@ -529,6 +529,123 @@ fn validate_expr_var_indices(
     }
 }
 
+// ── Builtin prim registry (ADR-0047) ────────────────────────────────
+//
+// A `prim name : T <-> T = "key"` declaration is opaque until its key resolves
+// to a concrete `(forward, backward)` pair. Builtin keys resolve here: given the
+// declared (lowered) input/output types, [`builtin_prim`] materializes the
+// `PrimDef` the elaborator wraps in `Iso::Prim`. Today the only builtin is the
+// reversible word add.
+
+/// The reversible word-add prim key: `(a, b) |-> (a, a + b mod 2^w)` over a pair
+/// of `W<n>` machine words (a `Flat(w)` leaf each). The addend `a` is preserved,
+/// so the map is a bijection; the inverse subtracts. At `w = 8` the TISC compiler
+/// recognizes it as a single reversible `Add` instruction.
+pub const ADD_INTO_KEY: &str = "theseus.arith.add_into";
+
+/// Resolve a builtin prim `key` against its declared (lowered) `input_ty` and
+/// `output_ty`, returning the concrete [`PrimDef`] or `None` if the key is
+/// unknown or the types do not fit the builtin's shape.
+///
+/// The returned def carries a symbolic [`PrimSpec`] (no materialized table). The
+/// caller validates it structurally via [`PrimSpec::validate_against`]; full
+/// mutual-inverse certification is the compiler's symbolic BVEQ (`admit_symbolic`
+/// in theseus-tisc), since `core::admit` cannot certify a symbolic-only prim.
+pub fn builtin_prim(key: &str, input_ty: &Type, output_ty: &Type) -> Option<PrimDef> {
+    match key {
+        ADD_INTO_KEY => {
+            // add_into is an endo-prim over a homogeneous word pair.
+            if input_ty != output_ty {
+                return None;
+            }
+            let w = flat_pair_width(input_ty)?;
+            Some(build_add_into(w))
+        }
+        _ => None,
+    }
+}
+
+/// If `ty` is `Prod(Flat(w), Flat(w))` (a pair of equal-width words), return `w`.
+fn flat_pair_width(ty: &Type) -> Option<u8> {
+    match ty {
+        Type::Prod(a, b) => match (a.as_ref(), b.as_ref()) {
+            (Type::Flat(wa), Type::Flat(wb)) if wa == wb => Some(*wa),
+            _ => None,
+        },
+        _ => None,
+    }
+}
+
+/// Build the `add_into` symbolic prim at width `w` (1..=8):
+/// `(a, b) |-> (a, (a + b) mod 2^w)`, inverse `(a, s) |-> (a, (s - a) mod 2^w)`.
+///
+/// A **symbolic** spec (bit-level ripple-carry `BvExpr`s), not a table: the
+/// `Flat(w)` value domain is `2^w` deep-thermometer values, so a materialized
+/// `2^w x 2^w` table is quadratically large and heap-heavy. The spec is `O(w)`
+/// tiny expressions -- eval decodes each input to bytes on demand, and the TISC
+/// compiler certifies + recognizes it symbolically (BDD) rather than enumerating.
+fn build_add_into(w: u8) -> PrimDef {
+    debug_assert!((1..=8).contains(&w), "add_into width must be 1..=8");
+    let f = Type::Flat(w);
+    let ty = Type::prod(f.clone(), f);
+    let spec = PrimSpec {
+        forward: add_transfer(w),
+        backward: sub_transfer(w),
+    };
+    PrimDef {
+        forward_name: "add_into".into(),
+        backward_name: "sub_into".into(),
+        input_ty: ty.clone(),
+        output_ty: ty,
+        forward: BTreeMap::new(),
+        backward: BTreeMap::new(),
+        symbolic: Some(spec),
+    }
+}
+
+/// Forward transfer `(a, b) |-> (a, a + b mod 2^w)`. Operand 0 = `a` (preserved),
+/// operand 1 = `b`; output leaf 0 = `a`, leaf 1 = the ripple-carry sum. The final
+/// carry-out is dropped, giving mod-`2^w` (wrapping) semantics.
+fn add_transfer(w: u8) -> SpecTransfer {
+    let n = w as usize;
+    let a = |i: usize| BvExpr::var(0, i);
+    let b = |i: usize| BvExpr::var(1, i);
+    let leaf_a: Vec<BvExpr> = (0..n).map(a).collect();
+    let mut sum = Vec::with_capacity(n);
+    let mut carry = BvExpr::constant(false);
+    for i in 0..n {
+        // s_i = a_i ^ b_i ^ carry_i
+        sum.push(a(i).xor(b(i)).xor(carry.clone()));
+        // carry_{i+1} = (a_i & b_i) | (carry_i & (a_i ^ b_i))
+        carry = a(i).and(b(i)).or(carry.and(a(i).xor(b(i))));
+    }
+    SpecTransfer {
+        leaves: vec![leaf_a, sum],
+        width: w,
+    }
+}
+
+/// Backward transfer `(a, s) |-> (a, s - a mod 2^w)`. Operand 0 = `a` (preserved),
+/// operand 1 = `s`; output leaf 0 = `a`, leaf 1 = the ripple-borrow difference.
+fn sub_transfer(w: u8) -> SpecTransfer {
+    let n = w as usize;
+    let a = |i: usize| BvExpr::var(0, i);
+    let s = |i: usize| BvExpr::var(1, i);
+    let leaf_a: Vec<BvExpr> = (0..n).map(a).collect();
+    let mut diff = Vec::with_capacity(n);
+    let mut borrow = BvExpr::constant(false);
+    for i in 0..n {
+        // d_i = s_i ^ a_i ^ borrow_i
+        diff.push(s(i).xor(a(i)).xor(borrow.clone()));
+        // borrow_{i+1} = (!s_i & a_i) | (borrow_i & !(s_i ^ a_i))
+        borrow = s(i).not().and(a(i)).or(borrow.and(s(i).xor(a(i)).not()));
+    }
+    SpecTransfer {
+        leaves: vec![leaf_a, diff],
+        width: w,
+    }
+}
+
 /// Count the number of leaves in a type (for Sum padding).
 pub fn count_leaves(ty: &Type) -> usize {
     match ty {