Execute proven unsigned addition in compiler-produced programs

.github/workflows/ci.yml

@@ -199,7 +199,7 @@ jobs:
               run: cargo clippy -p warp-core --features native_rule_bootstrap,trusted_runtime,host_test,application_root_shadow --lib --tests -- -D warnings
 
             - name: cargo clippy (compiler-produced pure evaluation)
-              run: cargo clippy -p warp-core --features trusted_runtime --lib --test edict_pure_evaluation_tests --test edict_pure_predicates_tests --test edict_pure_unsigned_subtraction_tests --test edict_pure_byte_length_tests --test edict_byte_equality_tests --test edict_byte_slice_tests --test edict_node_read_tests --test edict_byte_concat_tests --test edict_byte_literal_tests --test edict_source_functions_tests -- -D warnings -D missing_docs
+              run: cargo clippy -p warp-core --features trusted_runtime --lib --test edict_pure_evaluation_tests --test edict_pure_predicates_tests --test edict_pure_unsigned_subtraction_tests --test edict_unsigned_addition_tests --test edict_pure_byte_length_tests --test edict_byte_equality_tests --test edict_byte_slice_tests --test edict_node_read_tests --test edict_byte_concat_tests --test edict_byte_literal_tests --test edict_source_functions_tests -- -D warnings -D missing_docs
 
     clippy-det-fixed:
         name: Clippy (det_fixed)
@@ -395,7 +395,7 @@ jobs:
                   cargo test -p warp-core --features native_rule_bootstrap,trusted_runtime,application_root_shadow,delta_validate --test application_root_shadow_tests
             - name: cargo test (compiler-produced pure evaluation)
               run: |
-                  cargo test -p warp-core --features trusted_runtime --test edict_pure_evaluation_tests --test edict_pure_predicates_tests --test edict_pure_unsigned_subtraction_tests --test edict_pure_byte_length_tests --test edict_byte_equality_tests --test edict_byte_slice_tests --test edict_node_read_tests --test edict_byte_concat_tests --test edict_byte_literal_tests --test edict_source_functions_tests
+                  cargo test -p warp-core --features trusted_runtime --test edict_pure_evaluation_tests --test edict_pure_predicates_tests --test edict_pure_unsigned_subtraction_tests --test edict_unsigned_addition_tests --test edict_pure_byte_length_tests --test edict_byte_equality_tests --test edict_byte_slice_tests --test edict_node_read_tests --test edict_byte_concat_tests --test edict_byte_literal_tests --test edict_source_functions_tests
                   cargo test -p warp-core --features trusted_runtime --lib edict_pure::
             - name: cargo test (delta validation and the canonical delta merge)
               run: |

CHANGELOG.md

@@ -7,6 +7,11 @@
 
 ### Added
 
+- Bounded pure evaluation executes compiler-produced U32/U64 addition with
+  checked width bounds and ordinary work/value-storage charging. Independent
+  native provider judgments require same-width operands and a dominating
+  no-overflow proof, including legacy Core without a function table.
+
 - Experimental feature `application_root_shadow` (M1, off by default): an
   incremental application root over every node, edge and attachment record of
   a worldline state, kept beside the legacy state root, which it neither

crates/echo-edict-provider-lowerer/src/executable_operation/bounded_read/relation/types.rs

@@ -360,6 +360,13 @@ impl<'a> Scope<'a> {
             })
             .collect::<Result<Vec<_>, _>>()?;
         match (name, actual.as_slice(), declared.as_slice()) {
+            // source_functions::validate already established the independent
+            // no-overflow proof before this read relation is constructed.
+            ("core.integer.add", [left, right], [expected @ ReadType::Unsigned(_)])
+                if left == expected && right == expected =>
+            {
+                Ok(expected.clone())
+            }
             ("core.bytes.isUtf8", [actual], [expected @ ReadType::Bytes(_, _)])
                 if expected == actual =>
             {

crates/echo-edict-provider-lowerer/src/executable_operation/source_functions.rs

@@ -2,6 +2,7 @@
 // © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
 //! Lowerer-owned forward type, totality, depth and deterministic cost judgment.
 //! Applies to the complete source-function module, including unused definitions.
+mod unsigned_addition;
 use super::ProviderRefusalV1;
 use echo_edict_canonical::CanonicalValueV1 as Value;
 use std::collections::{BTreeMap, BTreeSet};
@@ -64,6 +65,7 @@ struct Judgment<'a> {
     completed: BTreeMap<String, Fact>,
     active: BTreeSet<String>,
     work: usize,
+    proven: Vec<&'a Value>,
 }
 
 pub(super) fn validate(core: &Value, exports: &Value, read: bool) -> Result<(), ProviderRefusalV1> {
@@ -157,19 +159,20 @@ fn run(core: &Value, exports: &Value, read: bool) -> Check<()> {
         completed: BTreeMap::new(),
         active: BTreeSet::new(),
         work: WORK,
+        proven: Vec::new(),
     };
     for name in proof.functions.keys().cloned().collect::<Vec<_>>() {
         proof.function(&name, 1)?;
     }
-    if super::map_field(core, "functions").is_none() {
+    if super::map_field(core, "functions").is_none() && !unsigned_addition::present(core)? {
         return Ok(());
     }
     for (_, intent) in members(get(core, "intents")?)? {
         proof.intent(intent, read)?;
     }
     Ok(())
 }
-impl Judgment<'_> {
+impl<'a> Judgment<'a> {
     fn charge(&mut self, depth: usize) -> Check<()> {
         self.work = self.work.checked_sub(1).ok_or(())?;
         if depth > DEPTH {
@@ -255,7 +258,7 @@ impl Judgment<'_> {
             _ => Err(()),
         }
     }
-    fn declaration<'a>(&mut self, value: &'a Value, scope: &mut Scope<'a>) -> Check<Ty> {
+    fn declaration(&mut self, value: &'a Value, scope: &mut Scope<'a>) -> Check<Ty> {
         exact(value, &["id", "type", "alphaName"])?;
         let id = string(get(value, "id")?)?;
         string(get(value, "alphaName")?)?;
@@ -280,6 +283,15 @@ impl Judgment<'_> {
                 .ok_or(())?;
             return Ok(fact.clone());
         }
+        // A helper has a fresh proof scope. Restore the caller on success and
+        // failure, so recursive checks cannot change enclosing all/not scopes.
+        let caller_facts = std::mem::take(&mut self.proven);
+        let result = self.check_function_body(name, prefix);
+        self.proven = caller_facts;
+        self.active.remove(name);
+        result
+    }
+    fn check_function_body(&mut self, name: &str, prefix: usize) -> Check<Fact> {
         let function = *self.functions.get(name).ok_or(())?;
         self.active.insert(name.to_owned());
         exact(function.body, &["locals", "bindings", "result"])?;
@@ -343,14 +355,13 @@ impl Judgment<'_> {
         if prefix.checked_add(fact.depth).ok_or(())? > DEPTH {
             return Err(());
         }
-        self.active.remove(name);
         self.completed.insert(name.to_owned(), fact.clone());
         Ok(fact)
     }
     fn expression(
         &mut self,
-        value: &Value,
-        scope: &Scope<'_>,
+        value: &'a Value,
+        scope: &Scope<'a>,
         source: bool,
         prefix: usize,
     ) -> Check<Fact> {
@@ -519,6 +530,23 @@ impl Judgment<'_> {
                             })?;
                             Ty::Bytes(min, max)
                         }
+                        ("core.integer.add", [left, right], [expected @ Ty::Word(max)])
+                            if left == expected
+                                && right == expected
+                                && matches!(*max, 4_294_967_295 | 18_446_744_073_709_551_615) =>
+                        {
+                            unsigned_addition::prove(
+                                arguments,
+                                *max,
+                                &self.proven,
+                                &mut self.work,
+                            )?;
+                            cost = cost.plus(Cost {
+                                steps: 3,
+                                bytes: 64,
+                            })?;
+                            expected.clone()
+                        }
                         ("core.integer.subtract", [left, right], [expected @ Ty::Word(_)])
                             if includes(expected, left) && includes(expected, right) =>
                         {
@@ -561,8 +589,8 @@ impl Judgment<'_> {
     }
     fn predicate(
         &mut self,
-        value: &Value,
-        scope: &Scope<'_>,
+        value: &'a Value,
+        scope: &Scope<'a>,
         source: bool,
         prefix: usize,
     ) -> Check<(Cost, usize)> {
@@ -582,11 +610,14 @@ impl Judgment<'_> {
                 }
                 let mut cost = Cost { steps: 1, bytes: 0 };
                 let mut height = 0;
+                let inherited = self.proven.len();
                 for value in values {
                     let (child, depth) = self.predicate(value, scope, source, prefix + 1)?;
                     cost = cost.plus(child)?;
                     height = height.max(depth);
+                    self.proven.push(value);
                 }
+                self.proven.truncate(inherited);
                 return Ok((cost, height + 1));
             }
             _ => {}
@@ -619,7 +650,8 @@ impl Judgment<'_> {
             left.depth.max(right.depth) + 1,
         ))
     }
-    fn intent(&mut self, intent: &Value, read: bool) -> Check<()> {
+    fn intent(&mut self, intent: &'a Value, read: bool) -> Check<()> {
+        self.proven.clear();
         let body = get(intent, "body")?;
         exact(body, &["locals", "nodes", "result"])?;
         let mut pending = BTreeMap::new();
@@ -659,6 +691,7 @@ impl Judgment<'_> {
                 self.predicate(get(constraint, "predicate")?, &scope, true, 0)?
                     .0,
             )?;
+            self.proven.push(get(constraint, "predicate")?);
         }
         for node in list(get(body, "nodes")?)? {
             if read {

crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/unsigned_addition.rs

@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+//! Lowerer-owned recursive upper bounds over checked, dominating predicates.
+use super::{get, list, literal, string, Check, Value};
+
+pub(super) fn present(core: &Value) -> Check<bool> {
+    let mut pending = vec![get(core, "intents")?];
+    while let Some(value) = pending.pop() {
+        match value {
+            Value::Map(fields) => {
+                if get(value, "kind").and_then(string) == Ok("call")
+                    && get(value, "callee").and_then(string) == Ok("core.integer.add")
+                {
+                    return Ok(true);
+                }
+                pending.extend(fields.iter().map(|(_, value)| value));
+            }
+            Value::Array(values) => pending.extend(values),
+            _ => {}
+        }
+    }
+    Ok(false)
+}
+
+pub(super) fn prove(args: &[Value], max: u64, facts: &[&Value], work: &mut usize) -> Check<()> {
+    let [left, right] = args else { return Err(()) };
+    let left = bound(left, max, facts, work, 0)?;
+    let right = bound(right, max, facts, work, 0)?;
+    left.checked_add(right)
+        .filter(|sum| *sum <= max)
+        .ok_or(())?;
+    Ok(())
+}
+fn debit(work: &mut usize, amount: usize) -> Check<()> {
+    *work = work.checked_sub(amount).ok_or(())?;
+    Ok(())
+}
+fn same(a: &Value, b: &Value, work: &mut usize) -> Check<bool> {
+    for value in [a, b] {
+        let bytes = echo_edict_canonical::encode_canonical_cbor_v1(value).map_err(|_| ())?;
+        debit(work, bytes.len())?;
+    }
+    Ok(a == b)
+}
+fn bound(expr: &Value, max: u64, facts: &[&Value], work: &mut usize, depth: usize) -> Check<u64> {
+    debit(work, 1)?;
+    if depth > 64 {
+        return Err(());
+    }
+    let mut upper = if string(get(expr, "kind")?)? == "call"
+        && string(get(expr, "callee")?)? == "core.integer.add"
+    {
+        let [left, right] = list(get(expr, "args")?)? else {
+            return Err(());
+        };
+        bound(left, max, facts, work, depth + 1)?
+            .checked_add(bound(right, max, facts, work, depth + 1)?)
+            .ok_or(())?
+    } else {
+        literal(expr).unwrap_or(max)
+    };
+    for predicate in facts {
+        refine(predicate, expr, &mut upper, work, depth + 1)?;
+    }
+    Ok(upper)
+}
+fn refine(
+    predicate: &Value,
+    expr: &Value,
+    upper: &mut u64,
+    work: &mut usize,
+    depth: usize,
+) -> Check<()> {
+    debit(work, 1)?;
+    if depth > 64 {
+        return Err(());
+    }
+    match string(get(predicate, "kind")?)? {
+        "all" => {
+            for child in list(get(predicate, "values")?)? {
+                refine(child, expr, upper, work, depth + 1)?;
+            }
+        }
+        "compare" => {
+            let op = string(get(predicate, "op")?)?;
+            let left = get(predicate, "left")?;
+            let right = get(predicate, "right")?;
+            if matches!(op, "<=" | "==") {
+                if let Ok(limit) = literal(right) {
+                    if same(left, expr, work)? {
+                        *upper = (*upper).min(limit);
+                    }
+                }
+            }
+            if op == "==" {
+                if let Ok(limit) = literal(left) {
+                    if same(right, expr, work)? {
+                        *upper = (*upper).min(limit);
+                    }
+                }
+            }
+        }
+        _ => {}
+    }
+    Ok(())
+}

crates/echo-edict-provider-verifier/src/executable_operation/bounded_read/audit/types.rs

@@ -342,6 +342,12 @@ impl<'a> Symbols<'a> {
             declared.push(self.schema(string(coordinate)?, 0)?);
         }
         match (name, actual.as_slice(), declared.as_slice()) {
+            // The source-function audit has independently proved totality.
+            ("core.integer.add", [left, right], [expected @ Schema::Word(_)])
+                if left == expected && right == expected =>
+            {
+                Ok(expected.clone())
+            }
             ("core.bytes.isUtf8", [actual], [expected @ Schema::Bytes { .. }])
                 if expected == actual =>
             {