Validate unsigned subtraction independently in Target IR

CHANGELOG.md

@@ -10,6 +10,15 @@ versions still track specification maturity rather than a released product.
 
 ### Changed
 
+- Removed exponential repeated Target IR operand validation for nested unsigned
+  arithmetic, including conditional and record-field operands, while preserving
+  malformed literal and reference rejection.
+
+- Independently validated unsigned subtraction in raw Core before Target IR
+  construction, preserving widths and operands and rejecting invalid signatures,
+  unproven underflow, and input-proof scope leakage. This does not add Echo
+  execution support or change a consumer producer pin.
+
 - Lowered same-width unsigned subtraction into Core only when exact operands,
   ordered literals, or dominating conjunctive input constraints prove no
   underflow. Proofs are isolated to each intent body; signed, mixed-width, and

crates/edict-syntax/src/target_ir.rs

@@ -4,6 +4,8 @@
 //! effect nodes into in-memory Echo or git-warp review artifacts. It does not
 //! execute a runtime, run a verifier, assemble bundles, or perform admission.
 
+mod unsigned_subtraction;
+
 use std::collections::{BTreeMap, BTreeSet};
 
 use crate::core_ir::{
@@ -705,6 +707,13 @@ fn validate_pure_binding_graphs(
                     "Core local table or producer contains an empty or duplicate identity",
                 ));
             }
+            if !unsigned_subtraction::intent_is_total(intent) {
+                return Some(invalid_pure_binding(
+                    intent_name,
+                    None,
+                    "unsigned subtraction is not proven total in its evaluation scope",
+                ));
+            }
             if intent
                 .body
                 .nodes
@@ -1128,6 +1137,14 @@ fn expression_has_closed_authority(
         CoreExpr::Field { .. } => {
             expression_type_coordinate(core, pure_functions, expression, available).is_some()
         }
+        CoreExpr::Call {
+            callee,
+            type_args,
+            args,
+        } if callee == unsigned_subtraction::OPERATION => {
+            unsigned_subtraction::type_coordinate(core, pure_functions, type_args, args, available)
+                .is_some()
+        }
         CoreExpr::Call { callee, .. } if callee == "core.string.concat" => {
             expression_string_shape(core, pure_functions, expression, available).is_some()
         }
@@ -1193,6 +1210,14 @@ fn expression_fits_declared_type(
                 0,
             )
         }
+        CoreExpr::Call {
+            callee,
+            type_args,
+            args,
+        } if callee == unsigned_subtraction::OPERATION => {
+            unsigned_subtraction::type_coordinate(core, pure_functions, type_args, args, available)
+                .is_some_and(|actual| core_type_fits(core, &actual, expected))
+        }
         CoreExpr::Call {
             callee,
             type_args,
@@ -1382,6 +1407,8 @@ fn expression_string_shape(
     }
 }
 
+// A returned coordinate also establishes operand validity. Callers must not
+// recursively validate the same expression again just to recover its type.
 fn expression_type_coordinate(
     core: &CoreModule,
     pure_functions: &[TargetPureFunctionFact],
@@ -1390,12 +1417,15 @@ fn expression_type_coordinate(
 ) -> Option<String> {
     match expression {
         CoreExpr::Local { reference }
-            if available.get(reference.id.as_str()).copied() == Some(reference) =>
+            if available.get(reference.id.as_str()).copied() == Some(reference)
+                && resolved_core_type(core, &reference.ty).is_some() =>
         {
             Some(reference.ty.clone())
         }
         CoreExpr::Const(CoreValue::Bool(_)) => Some("Bool".to_owned()),
-        CoreExpr::Const(CoreValue::Int { width, .. }) => Some(width.clone()),
+        CoreExpr::Const(CoreValue::Int { width, value }) => {
+            crate::core_ir::parse_core_integer(width, value).map(|_| width.clone())
+        }
         CoreExpr::Const(CoreValue::String(value)) => Some(format!(
             "String<max={},canonical=raw-utf8>",
             u64::try_from(value.chars().count()).ok()?
@@ -1411,6 +1441,13 @@ fn expression_type_coordinate(
             };
             Some(coordinate)
         }
+        CoreExpr::Call {
+            callee,
+            type_args,
+            args,
+        } if callee == unsigned_subtraction::OPERATION => {
+            unsigned_subtraction::type_coordinate(core, pure_functions, type_args, args, available)
+        }
         CoreExpr::Call { callee, .. } if callee == "core.string.concat" => {
             expression_string_shape(core, pure_functions, expression, available)
                 .map(|(max, canonical)| format!("String<max={max},canonical={canonical}>"))
@@ -1665,12 +1702,8 @@ fn comparison_operand_shape(
             let else_shape = comparison_operand_shape(core, pure_functions, else_value, available)?;
             join_conditional_shapes(core, &then_shape, &else_shape, 0)
         }
-        _ => {
-            let coordinate =
-                expression_type_coordinate(core, pure_functions, expression, available)?;
-            expression_fits_declared_type(core, pure_functions, expression, &coordinate, available)
-                .then_some(ComparisonOperandShape::Coordinate(coordinate))
-        }
+        _ => expression_type_coordinate(core, pure_functions, expression, available)
+            .map(ComparisonOperandShape::Coordinate),
     }
 }
 

crates/edict-syntax/src/target_ir/unsigned_subtraction.rs

@@ -0,0 +1,247 @@
+//! Target-owned totality check over untrusted Core, independent of the compiler proof.
+use super::{
+    expression_type_coordinate, BTreeMap, CoreExpr, CoreIntent, CoreModule, CoreNode,
+    CorePredicate, CoreRequireFailureArm, CoreValue, InputConstraint, LocalRef,
+    TargetPureFunctionFact,
+};
+use crate::core_ir::{CompareOp, CoreBlock};
+
+pub(super) const OPERATION: &str = "core.integer.subtract";
+
+pub(super) fn type_coordinate(
+    core: &CoreModule,
+    functions: &[TargetPureFunctionFact],
+    type_args: &[String],
+    args: &[CoreExpr],
+    available: &BTreeMap<&str, &LocalRef>,
+) -> Option<String> {
+    #[cfg(test)]
+    tests::VALIDATION_VISITS.with(|count| count.set(count.get() + 1));
+    let [width] = type_args else { return None };
+    let [left, right] = args else { return None };
+    if !matches!(width.as_str(), "U32" | "U64") {
+        return None;
+    }
+    [left, right]
+        .iter()
+        .all(|operand| {
+            expression_type_coordinate(core, functions, operand, available).as_ref() == Some(width)
+        })
+        .then(|| width.clone())
+}
+
+pub(super) fn intent_is_total(intent: &CoreIntent) -> bool {
+    intent
+        .basis
+        .as_ref()
+        .is_none_or(|basis| expression_is_total(basis, &[]))
+        && intent
+            .input_constraints
+            .iter()
+            .all(|constraint| predicate_is_total(&constraint.predicate, &[]))
+        && block_is_total(&intent.body, &intent.input_constraints)
+}
+
+fn block_is_total(block: &CoreBlock, constraints: &[InputConstraint]) -> bool {
+    block.nodes.iter().all(|node| match node {
+        CoreNode::Let { value, .. } => expression_is_total(value, constraints),
+        CoreNode::Require { predicate, arm } => {
+            let (CoreRequireFailureArm::Terminal { reason }
+            | CoreRequireFailureArm::ContinueObstructed { reason }) = arm;
+            predicate_is_total(predicate, constraints)
+                && reason
+                    .payload
+                    .values()
+                    .all(|value| expression_is_total(value, constraints))
+        }
+        CoreNode::Effect {
+            input,
+            obstruction_map,
+            ..
+        } => {
+            expression_is_total(input, constraints)
+                && obstruction_map
+                    .values()
+                    .all(|arm| expression_is_total(&arm.value, constraints))
+        }
+        CoreNode::ExternalActionRequest {
+            input,
+            authority_scope,
+            basis,
+            budget,
+            ..
+        } => [
+            input,
+            authority_scope,
+            basis,
+            &budget.max_settlement_bytes,
+            &budget.max_attempts,
+        ]
+        .iter()
+        .all(|value| expression_is_total(value, constraints)),
+        CoreNode::For { iter, body, .. } => {
+            expression_is_total(iter, constraints) && block_is_total(body, constraints)
+        }
+        CoreNode::Branch {
+            predicate,
+            then_block,
+            else_block,
+            ..
+        } => {
+            predicate_is_total(predicate, constraints)
+                && block_is_total(then_block, constraints)
+                && block_is_total(else_block, constraints)
+        }
+    }) && expression_is_total(&block.result, constraints)
+}
+
+fn predicate_is_total(predicate: &CorePredicate, constraints: &[InputConstraint]) -> bool {
+    match predicate {
+        CorePredicate::True | CorePredicate::False => true,
+        CorePredicate::Not(inner) => predicate_is_total(inner, constraints),
+        CorePredicate::All(items) | CorePredicate::Any(items) => items
+            .iter()
+            .all(|item| predicate_is_total(item, constraints)),
+        CorePredicate::Compare { left, right, .. } => {
+            expression_is_total(left, constraints) && expression_is_total(right, constraints)
+        }
+    }
+}
+
+fn expression_is_total(expression: &CoreExpr, constraints: &[InputConstraint]) -> bool {
+    match expression {
+        CoreExpr::Local { .. } | CoreExpr::Const(_) => true,
+        CoreExpr::Field { base, .. } => expression_is_total(base, constraints),
+        CoreExpr::Record { fields } => fields
+            .values()
+            .all(|value| expression_is_total(value, constraints)),
+        CoreExpr::If {
+            predicate,
+            then_value,
+            else_value,
+        } => {
+            predicate_is_total(predicate, constraints)
+                && expression_is_total(then_value, constraints)
+                && expression_is_total(else_value, constraints)
+        }
+        CoreExpr::Call { callee, args, .. } => {
+            if !args.iter().all(|arg| expression_is_total(arg, constraints)) {
+                return false;
+            }
+            if callee != OPERATION {
+                return true;
+            }
+            let [left, right] = args.as_slice() else {
+                return false;
+            };
+            left == right
+                || constant(right) == Some(0)
+                || matches!((constant(left), constant(right)), (Some(a), Some(b)) if a >= b)
+                || constraints
+                    .iter()
+                    .any(|constraint| proves_order(&constraint.predicate, left, right))
+        }
+    }
+}
+
+fn constant(value: &CoreExpr) -> Option<u64> {
+    let CoreExpr::Const(CoreValue::Int { width, value }) = value else {
+        return None;
+    };
+    match width.as_str() {
+        "U32" => value.parse::<u32>().ok().map(u64::from),
+        "U64" => value.parse().ok(),
+        _ => None,
+    }
+}
+
+fn proves_order(predicate: &CorePredicate, minuend: &CoreExpr, subtrahend: &CoreExpr) -> bool {
+    match predicate {
+        CorePredicate::All(items) => items
+            .iter()
+            .any(|item| proves_order(item, minuend, subtrahend)),
+        CorePredicate::Compare { op, left, right } => match op {
+            CompareOp::Lt | CompareOp::Le => left == subtrahend && right == minuend,
+            CompareOp::Gt | CompareOp::Ge => left == minuend && right == subtrahend,
+            CompareOp::Eq => {
+                (left == minuend && right == subtrahend) || (left == subtrahend && right == minuend)
+            }
+            CompareOp::Ne => false,
+        },
+        CorePredicate::True
+        | CorePredicate::False
+        | CorePredicate::Not(_)
+        | CorePredicate::Any(_) => false,
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use std::cell::Cell;
+
+    std::thread_local! {
+        pub(super) static VALIDATION_VISITS: Cell<usize> = const { Cell::new(0) };
+    }
+
+    fn integer(value: &str) -> CoreExpr {
+        CoreExpr::Const(CoreValue::Int {
+            width: "U64".to_owned(),
+            value: value.to_owned(),
+        })
+    }
+
+    fn assert_bounded_validation(wrap: fn(CoreExpr) -> CoreExpr) {
+        let core = CoreModule {
+            api_version: crate::core_ir::CORE_API_VERSION.to_owned(),
+            coordinate: "arithmetic.work@1".to_owned(),
+            imports: Vec::new(),
+            types: BTreeMap::new(),
+            intents: BTreeMap::new(),
+            required_core_capabilities: Vec::new(),
+        };
+        let depth = 8;
+        let expression = (0..depth).fold(integer("9"), |left, _| {
+            wrap(CoreExpr::Call {
+                callee: OPERATION.to_owned(),
+                type_args: vec!["U64".to_owned()],
+                args: vec![left, integer("0")],
+            })
+        });
+        VALIDATION_VISITS.with(|count| count.set(0));
+        assert_eq!(
+            expression_type_coordinate(&core, &[], &expression, &BTreeMap::new()),
+            Some("U64".to_owned())
+        );
+        let visits = VALIDATION_VISITS.with(Cell::get);
+        println!("{depth} subtraction nodes required {visits} validation visits");
+        assert!(
+            visits <= 4 * depth,
+            "{depth} subtraction nodes required {visits} validation visits"
+        );
+    }
+
+    #[test]
+    fn nested_subtraction_validation_work_is_bounded() {
+        assert_bounded_validation(std::convert::identity);
+    }
+
+    #[test]
+    fn conditional_subtraction_validation_work_is_bounded() {
+        assert_bounded_validation(|value| CoreExpr::If {
+            predicate: Box::new(CorePredicate::True),
+            then_value: Box::new(value),
+            else_value: Box::new(integer("9")),
+        });
+    }
+
+    #[test]
+    fn record_field_subtraction_validation_work_is_bounded() {
+        assert_bounded_validation(|value| CoreExpr::Field {
+            base: Box::new(CoreExpr::Record {
+                fields: BTreeMap::from([("value".to_owned(), value)]),
+            }),
+            field: "value".to_owned(),
+        });
+    }
+}