E0308 sub-wall 2: trait-derive completeness predicate (Clone/arith/serde) for repr grounding

dag/extdeps/languages/rust/emit.dag

@@ -290,3 +290,37 @@ fn rust_qualified_module_mod_basename(qualified_module: String) -> String {
 fn rust_qualified_module_mod_filename(qualified_module: String) -> String {
   concat(rust_qualified_module_mod_basename(qualified_module: qualified_module), ".rs")
 }
+
+data rust_repr_grounding_arm_b_dissolve_on: String = "Interim CommutativeSemiring<Magnitude> carrier arithmetic stubs dissolve when GroupCompletion/Nat body lands (#7197); replace fail-closed unimplemented! stubs with grounded i64 newtype operations. Do not retain PartialEq<i64> cross-representation bridge — numeric-tower grounding replaces the straddle."
+
+fn rust_supplemental_impls_commutative_semiring_magnitude() -> String {
+  concat(
+    "\n// repr-grounding arm (b): Nat carrier arithmetic (v1 seed emit; ",
+    rust_repr_grounding_arm_b_dissolve_on,
+    ")\n",
+    "impl std::ops::Add for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
+    "    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n",
+    "    fn add(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
+    "}\n",
+    "impl std::ops::Mul for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
+    "    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n",
+    "    fn mul(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
+    "}\n",
+    "impl std::ops::Div for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
+    "    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n",
+    "    fn div(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
+    "}\n",
+    "impl std::cmp::PartialEq<i64> for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
+    "    fn eq(&self, _other: &i64) -> bool { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
+    "}\n"
+  )
+}
+
+fn rust_supplemental_impls_bool_coproduct() -> String {
+  concat(
+    "\n// repr-grounding arm (b): Bool coproduct ↔ host bool bridge (v1 seed emit)\n",
+    "impl From<Bool> for bool {\n",
+    "    fn from(b: Bool) -> bool { match b { Bool::True => true, Bool::False => false } }\n",
+    "}\n"
+  )
+}

dag/std/trait_derive_shape.dag

@@ -2,9 +2,9 @@ module std.trait_derive_shape
 
 import std.algebra { Cons, Empty }
 
-data trait_derive_shape_note: String = "Target-agnostic authority for ReprGroundingDeriveTrait × ReprGroundingDeriveElemShape capability table and derive-trait list builders. Rust spellings: extdeps.languages.rust.emit. Consumed by v2.compiler.trait_derive_completeness and v1.compiler.trait_derive_emit. #7174 scope (operator 2026-07-25): v1 emit wires clone bounds + serde/Debug/Ord derives on named structs/enums only; ReprDeriveAdd/Sub/… rows on KernelInt are predicate authority for the grounding lane (GroupCompletion<Nat>, Vector), not v1 custom-impl emission."
+data trait_derive_shape_note: String = "Target-agnostic authority for ReprGroundingDeriveTrait × ReprGroundingDeriveElemShape capability table and derive-trait list builders. Rust spellings: extdeps.languages.rust.emit. Consumed by v2.compiler.trait_derive_completeness and v1.compiler.trait_derive_emit. #7174 (operator 2026-07-25): v1 emit wires (a) clone bounds and (c) serde/Debug/Ord #[derive] on named structs/enums. Root-4 arm (b): predicate-gated supplemental impl { … } blocks for coproduct-native arithmetic carriers — see trait_derive_shape_grounding_lane_handoff; ReprDeriveAdd/Sub/… rows on KernelInt are capability-table authority for repr_grounding_derive_completeness_predicate, not spellings."
 
-data trait_derive_shape_grounding_lane_handoff: String = "Arm (b) deferred to GroupCompletion grounding lane: coproduct-native arithmetic + PartialOrd/PartialEq impl blocks for algebra carriers (GroupCompletion<Nat>, Vector, CommutativeSemiring<Magnitude>). This module's capability table + repr_grounding_derive_completeness_predicate remain the shared authority; the grounding lane emits impl { … } from shape rows, not #[derive]. v1.compiler.trait_derive_emit does not wire arm (b)."
+data trait_derive_shape_grounding_lane_handoff: String = "Root-4 arm (b): coproduct-native arithmetic + PartialOrd/PartialEq impl blocks for algebra carriers (GroupCompletion<Nat>, Vector, CommutativeSemiring<Magnitude>). Capability table + repr_grounding_derive_completeness_predicate remain the shared authority; v1.compiler.trait_derive_emit emits impl { … } from shape rows (not #[derive]) through the seed emitter. dissolve-on: GroupCompletion/FieldOfFractions body landing (#7197) replaces interim Magnitude-carrier stubs."
 
 data trait_derive_shape_dissolve_on: String = "ReprGroundingDeriveTrait members that name Rust-specific authorities (ReprDeriveSerialize, ReprDeriveAdd, …) migrate beside each target's spelling table when a second consumer exists; until then capability roles stay in std/ with spellings in extdeps.languages.rust.emit."
 
@@ -248,3 +248,36 @@ fn payload_coproduct_derive_traits() -> List<ReprGroundingDeriveTrait> {
     }
   }
 }
+
+fn kernel_int_arithmetic_traits() -> List<ReprGroundingDeriveTrait> {
+  Cons {
+    head: ReprDeriveAdd,
+    tail: Cons {
+      head: ReprDeriveSub,
+      tail: Cons {
+        head: ReprDeriveMul,
+        tail: Cons {
+          head: ReprDeriveDiv,
+          tail: Cons {
+            head: ReprDeriveRem,
+            tail: Cons {
+              head: ReprDeriveNeg,
+              tail: Cons {
+                head: ReprDerivePartialEq,
+                tail: Cons { head: ReprDerivePartialOrd, tail: Empty }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+fn repr_grounding_supplemental_commutative_semiring_target(module_path: String, name: String) -> Bool {
+  module_path == "std.algebra" && name == "CommutativeSemiring"
+}
+
+fn repr_grounding_supplemental_bool_host_bridge_target(module_path: String, name: String) -> Bool {
+  module_path == "std.types" && name == "Bool"
+}

src/v1/05_emit_rust.dag

@@ -56,6 +56,7 @@ import v1.compiler.closure_stub_v2_std_text_rust { closure_stub_v2_std_text_sour
 import v1.compiler.coercion { coerce_primitive_type, is_copy, lookup_checkpoint }
 import v1.compiler.trait_derive_emit {
   v1_emit_struct_derives, v1_emit_enum_derives,
+  v1_emit_struct_supplemental_impls, v1_emit_enum_supplemental_impls,
   v1_generic_params_needing_clone_bound, v1_emit_type_params_with_clone_bounds,
   rust_nominal_identity_carrier_shape_eligible, rust_symbol_wrapped_ord_carrier_shape_eligible
 }
@@ -4735,7 +4736,9 @@ fn emit_struct_from_children(name: String, type_params: String, generic_param_na
       concat(field_lines, [concat("    ", rust_visibility_prefix(), rust_phantom_field_name(), ": std::marker::PhantomData<", rust_phantom_marker_inner(unused: unused_params), ">,")])
     } else { field_lines }
     let fields_str = all_field_lines |> join(separator: "\n")
-    concat(derives, "\n", rust_visibility_prefix(), rust_items().struct_keyword, " ", name, type_params, " {\n", fields_str, "\n}")
+    let struct_def = concat(derives, "\n", rust_visibility_prefix(), rust_items().struct_keyword, " ", name, type_params, " {\n", fields_str, "\n}")
+    let supplemental = v1_emit_struct_supplemental_impls(module_path: env.module_path, name: name)
+    if supplemental == "" { struct_def } else { concat(struct_def, supplemental) }
   }
 }
 
@@ -4851,8 +4854,9 @@ fn emit_enum_from_children(name: String, type_params: String, generic_param_name
   let tag_line = if serde_policy.enum_attr == "" { "" } else { concat(serde_policy.enum_attr, "\n") }
   let enum_def = concat(derives, "\n", tag_line, rust_visibility_prefix(), rust_items().enum_keyword, " ", name, type_params, " {\n", variants_str, "\n}")
   let accessor_impl = emit_enum_shared_accessors(name: name, type_params: type_params, generic_param_names: generic_param_names, children: children, recursive_types: recursive_types, shared_types: shared_types, env: env, emit_info: emit_info)
-  if accessor_impl == "" { enum_def }
-  else { concat(enum_def, "\n", accessor_impl) }
+  let supplemental = v1_emit_enum_supplemental_impls(module_path: env.module_path, name: name)
+  let with_accessors = if accessor_impl == "" { enum_def } else { concat(enum_def, "\n", accessor_impl) }
+  if supplemental == "" { with_accessors } else { concat(with_accessors, supplemental) }
 }
 
 fn find_shared_enum_fields(children: List<Node>, env: TypeEnv) -> List<String> {

src/v1/stage0/src/extdeps_languages_rust_emit.rs

@@ -628,3 +628,20 @@ pub fn rust_qualified_module_mod_filename(qualified_module: String) -> String {
         ".rs".to_string(),
     )
 }
+
+pub fn rust_repr_grounding_arm_b_dissolve_on() -> String {
+    thread_local! {
+        static CACHED: String = {
+            "Interim CommutativeSemiring<Magnitude> carrier arithmetic stubs dissolve when GroupCompletion/Nat body lands (#7197); replace fail-closed unimplemented! stubs with grounded i64 newtype operations. Do not retain PartialEq<i64> cross-representation bridge — numeric-tower grounding replaces the straddle.".to_string()
+        };
+    }
+    CACHED.with(|c: &String| c.clone())
+}
+
+pub fn rust_supplemental_impls_commutative_semiring_magnitude() -> String {
+    v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("\n// repr-grounding arm (b): Nat carrier arithmetic (v1 seed emit; ".to_string(), rust_repr_grounding_arm_b_dissolve_on()), ")\n".to_string()), "impl std::ops::Add for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n".to_string()), "    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n".to_string()), "    fn add(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n".to_string()), "}\n".to_string()), "impl std::ops::Mul for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n".to_string()), "    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n".to_string()), "    fn mul(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n".to_string()), "}\n".to_string()), "impl std::ops::Div for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n".to_string()), "    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n".to_string()), "    fn div(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n".to_string()), "}\n".to_string()), "impl std::cmp::PartialEq<i64> for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n".to_string()), "    fn eq(&self, _other: &i64) -> bool { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n".to_string()), "}\n".to_string())
+}
+
+pub fn rust_supplemental_impls_bool_coproduct() -> String {
+    v1_rt::concat(v1_rt::concat(v1_rt::concat("\n// repr-grounding arm (b): Bool coproduct ↔ host bool bridge (v1 seed emit)\n".to_string(), "impl From<Bool> for bool {\n".to_string()), "    fn from(b: Bool) -> bool { match b { Bool::True => true, Bool::False => false } }\n".to_string()), "}\n".to_string())
+}

src/v1/stage0/src/std_algebra.rs

@@ -84,6 +84,30 @@ pub struct CommutativeSemiring<T> {
     pub one: T,
     pub _phantom: std::marker::PhantomData<T>,
 }
+// repr-grounding arm (b): Nat carrier arithmetic (v1 seed emit; Interim CommutativeSemiring<Magnitude> carrier arithmetic stubs dissolve when GroupCompletion/Nat body lands (#7197); replace fail-closed unimplemented! stubs with grounded i64 newtype operations. Do not retain PartialEq<i64> cross-representation bridge — numeric-tower grounding replaces the straddle.)
+impl std::ops::Add for CommutativeSemiring<crate::std_magnitude::Magnitude> {
+    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;
+    fn add(self, _rhs: Self) -> Self::Output {
+        unimplemented!("interim CommutativeSemiring<Magnitude> stub — see #7197")
+    }
+}
+impl std::ops::Mul for CommutativeSemiring<crate::std_magnitude::Magnitude> {
+    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;
+    fn mul(self, _rhs: Self) -> Self::Output {
+        unimplemented!("interim CommutativeSemiring<Magnitude> stub — see #7197")
+    }
+}
+impl std::ops::Div for CommutativeSemiring<crate::std_magnitude::Magnitude> {
+    type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;
+    fn div(self, _rhs: Self) -> Self::Output {
+        unimplemented!("interim CommutativeSemiring<Magnitude> stub — see #7197")
+    }
+}
+impl std::cmp::PartialEq<i64> for CommutativeSemiring<crate::std_magnitude::Magnitude> {
+    fn eq(&self, _other: &i64) -> bool {
+        unimplemented!("interim CommutativeSemiring<Magnitude> stub — see #7197")
+    }
+}
 
 #[derive(Clone)]
 pub struct Ring<T> {

src/v1/stage0/src/std_trait_derive_shape.rs

@@ -16,7 +16,7 @@ use std::rc::Rc;
 pub fn trait_derive_shape_note() -> String {
     thread_local! {
         static CACHED: String = {
-            "Target-agnostic authority for ReprGroundingDeriveTrait × ReprGroundingDeriveElemShape capability table and derive-trait list builders. Rust spellings: extdeps.languages.rust.emit. Consumed by v2.compiler.trait_derive_completeness and v1.compiler.trait_derive_emit. #7174 scope (operator 2026-07-25): v1 emit wires clone bounds + serde/Debug/Ord derives on named structs/enums only; ReprDeriveAdd/Sub/… rows on KernelInt are predicate authority for the grounding lane (GroupCompletion<Nat>, Vector), not v1 custom-impl emission.".to_string()
+            "Target-agnostic authority for ReprGroundingDeriveTrait × ReprGroundingDeriveElemShape capability table and derive-trait list builders. Rust spellings: extdeps.languages.rust.emit. Consumed by v2.compiler.trait_derive_completeness and v1.compiler.trait_derive_emit. #7174 (operator 2026-07-25): v1 emit wires (a) clone bounds and (c) serde/Debug/Ord #[derive] on named structs/enums. Root-4 arm (b): predicate-gated supplemental impl { … } blocks for coproduct-native arithmetic carriers — see trait_derive_shape_grounding_lane_handoff; ReprDeriveAdd/Sub/… rows on KernelInt are capability-table authority for repr_grounding_derive_completeness_predicate, not spellings.".to_string()
         };
     }
     CACHED.with(|c: &String| c.clone())
@@ -25,7 +25,7 @@ pub fn trait_derive_shape_note() -> String {
 pub fn trait_derive_shape_grounding_lane_handoff() -> String {
     thread_local! {
         static CACHED: String = {
-            "Arm (b) deferred to GroupCompletion grounding lane: coproduct-native arithmetic + PartialOrd/PartialEq impl blocks for algebra carriers (GroupCompletion<Nat>, Vector, CommutativeSemiring<Magnitude>). This module's capability table + repr_grounding_derive_completeness_predicate remain the shared authority; the grounding lane emits impl { … } from shape rows, not #[derive]. v1.compiler.trait_derive_emit does not wire arm (b).".to_string()
+            "Root-4 arm (b): coproduct-native arithmetic + PartialOrd/PartialEq impl blocks for algebra carriers (GroupCompletion<Nat>, Vector, CommutativeSemiring<Magnitude>). Capability table + repr_grounding_derive_completeness_predicate remain the shared authority; v1.compiler.trait_derive_emit emits impl { … } from shape rows (not #[derive]) through the seed emitter. dissolve-on: GroupCompletion/FieldOfFractions body landing (#7197) replaces interim Magnitude-carrier stubs.".to_string()
         };
     }
     CACHED.with(|c: &String| c.clone())
@@ -382,6 +382,65 @@ pub fn payload_coproduct_derive_traits() -> Rc<Vec<ReprGroundingDeriveTrait>> {
     })
 }
 
+pub fn kernel_int_arithmetic_traits() -> Rc<Vec<ReprGroundingDeriveTrait>> {
+    Rc::new({
+        let mut __cons_v = (*Rc::new({
+            let mut __cons_v = (*Rc::new({
+                let mut __cons_v = (*Rc::new({
+                    let mut __cons_v = (*Rc::new({
+                        let mut __cons_v = (*Rc::new({
+                            let mut __cons_v = (*Rc::new({
+                                let mut __cons_v = (*Rc::new({
+                                    let mut __cons_v = (*Rc::new(vec![])).clone();
+                                    __cons_v
+                                        .insert(0, ReprGroundingDeriveTrait::ReprDerivePartialOrd);
+                                    __cons_v
+                                }))
+                                .clone();
+                                __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDerivePartialEq);
+                                __cons_v
+                            }))
+                            .clone();
+                            __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDeriveNeg);
+                            __cons_v
+                        }))
+                        .clone();
+                        __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDeriveRem);
+                        __cons_v
+                    }))
+                    .clone();
+                    __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDeriveDiv);
+                    __cons_v
+                }))
+                .clone();
+                __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDeriveMul);
+                __cons_v
+            }))
+            .clone();
+            __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDeriveSub);
+            __cons_v
+        }))
+        .clone();
+        __cons_v.insert(0, ReprGroundingDeriveTrait::ReprDeriveAdd);
+        __cons_v
+    })
+}
+
+pub fn repr_grounding_supplemental_commutative_semiring_target(
+    module_path: String,
+    name: String,
+) -> bool {
+    ((module_path.clone() == "std.algebra".to_string())
+        && (name.clone() == "CommutativeSemiring".to_string()))
+}
+
+pub fn repr_grounding_supplemental_bool_host_bridge_target(
+    module_path: String,
+    name: String,
+) -> bool {
+    ((module_path.clone() == "std.types".to_string()) && (name.clone() == "Bool".to_string()))
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
 pub struct ReprDeriveDebug;
 #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]

src/v1/stage0/src/std_types.rs

@@ -203,6 +203,15 @@ pub enum Bool {
     True,
     False,
 }
+// repr-grounding arm (b): Bool coproduct ↔ host bool bridge (v1 seed emit)
+impl From<Bool> for bool {
+    fn from(b: Bool) -> bool {
+        match b {
+            Bool::True => true,
+            Bool::False => false,
+        }
+    }
+}
 
 pub type Json = serde_json::Value;