feat: verify runtime slice and subtraction operands by proven range

CHANGELOG.md

@@ -95,6 +95,14 @@
 
 ### Changed
 
+- A Core without a function table that contains `core.bytes.slice` or
+  `core.integer.subtract` is now judged in full by the lowerer and verifier,
+  including its declared budget, as addition already was. Previously such a
+  Core skipped that judgment, so an unproven runtime slice was not refused
+  before installation. Jim's retained leaf-slice package declares a 1 MiB step
+  budget, 93 steps below Echo's worst-case charge for slicing its whole 1 MiB
+  operand, and is now refused until it declares an adequate budget.
+
 - Provider semantic declarations now support explicitly bounded Core byte
   aliases, including exact 32-byte identifiers. Byte aliases participate in
   bounded record graphs and generate canonical lawpack type definitions.
@@ -342,6 +350,17 @@
 
 ### Added
 
+- Runtime operands for `core.bytes.slice` and `core.integer.subtract` under
+  Edict's proven-range rules. The lowerer, the verifier and the native helper
+  checker each require a dominating fact (an input constraint or an earlier
+  conjunct of the same `all`) for `start <= end <= len(bytes)` or
+  `right <= left`; conditional predicates, negations and later conjuncts prove
+  nothing. The bounded-read relations type both calls, so a read guard such as
+  `at <= len(text) && isUtf8(slice(text, 0, at))` verifies, and short-circuit
+  evaluation sends an out-of-range `at` down the authored path. Slices are now
+  typed `Bytes<max=N>`, as Edict types them, rather than narrowed for literal
+  offsets, so `isUtf8` of a literal slice type-checks.
+
 - Bounded pure evaluation executes Edict's `core.bytes.count` (edict#269):
   raw single-byte counting with a structurally checked one-byte constant
   needle and one complete scan charged. The lowerer and verifier type it

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

@@ -364,12 +364,25 @@ 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.
+            // no-overflow and order proofs before this read relation is constructed.
             ("core.integer.add", [left, right], [expected @ ReadType::Unsigned(_)])
                 if left == expected && right == expected =>
             {
                 Ok(expected.clone())
             }
+            ("core.integer.subtract", [left, right], [expected @ ReadType::Unsigned(_)])
+                if expected.accepts(left) && expected.accepts(right) =>
+            {
+                Ok(expected.clone())
+            }
+            // The same validation established start <= end <= len(bytes).
+            (
+                "core.bytes.slice",
+                [actual, ReadType::Unsigned(a), ReadType::Unsigned(b)],
+                [expected @ ReadType::Bytes(_, max)],
+            ) if *a == u64::MAX && *b == u64::MAX && expected.accepts(actual) => {
+                Ok(ReadType::Bytes(0, *max))
+            }
             ("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 order;
 mod unsigned_addition;
 use super::ProviderRefusalV1;
 use echo_edict_canonical::CanonicalValueV1 as Value;
@@ -618,9 +619,14 @@ impl<'a> Judgment<'a> {
                         ("core.integer.subtract", [left, right], [expected @ Ty::Word(_)])
                             if includes(expected, left) && includes(expected, right) =>
                         {
-                            literal(&arguments[0])?
-                                .checked_sub(literal(&arguments[1])?)
-                                .ok_or(())?;
+                            if !order::proven(
+                                &arguments[0],
+                                &arguments[1],
+                                &self.proven,
+                                &mut self.work,
+                            )? {
+                                return Err(());
+                            }
                             cost = cost.plus(Cost {
                                 steps: 3,
                                 bytes: 64,
@@ -630,19 +636,36 @@ impl<'a> Judgment<'a> {
                         (
                             "core.bytes.slice",
                             [actual, Ty::Word(a), Ty::Word(b)],
-                            [expected @ Ty::Bytes(min, _)],
+                            [expected @ Ty::Bytes(min, max)],
                         ) if *a == u64::MAX && *b == u64::MAX && includes(expected, actual) => {
-                            let start = literal(&arguments[1])?;
-                            let end = literal(&arguments[2])?;
-                            if start > end || end > *min {
-                                return Err(());
-                            }
-                            let count = end - start;
+                            // Literal offsets within the guaranteed minimum length need
+                            // no fact; any other offsets need start <= end <= len(bytes).
+                            let copied = match (literal(&arguments[1]), literal(&arguments[2])) {
+                                (Ok(start), Ok(end)) if start <= end && end <= *min => end - start,
+                                _ => {
+                                    let length = order::length_of(&types[0], &arguments[0]);
+                                    if !order::proven(
+                                        &arguments[2],
+                                        &arguments[1],
+                                        &self.proven,
+                                        &mut self.work,
+                                    )? || !order::proven(
+                                        &length,
+                                        &arguments[2],
+                                        &self.proven,
+                                        &mut self.work,
+                                    )? {
+                                        return Err(());
+                                    }
+                                    *max
+                                }
+                            };
                             cost = cost.plus(Cost {
-                                steps: count.checked_add(4).ok_or(())?,
-                                bytes: count.checked_add(64).ok_or(())?,
+                                steps: copied.checked_add(4).ok_or(())?,
+                                bytes: copied.checked_add(64).ok_or(())?,
                             })?;
-                            Ty::Bytes(0, count)
+                            // As in Edict, a slice keeps its operand's maximum and no minimum.
+                            Ty::Bytes(0, *max)
                         }
                         _ => return Err(()),
                     }

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

@@ -0,0 +1,96 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+//! Lowerer-owned order proofs for partial byte slicing and unsigned subtraction.
+//!
+//! `left >= right` holds for equal terms, a zero right side, ordered
+//! constants, or a dominating fact: an input constraint or an earlier
+//! conjunct of an enclosing `all`. Conditional predicates, negations and
+//! later conjuncts prove nothing.
+use super::{get, list, literal, string, Check, Value};
+
+pub(super) fn proven(
+    left: &Value,
+    right: &Value,
+    facts: &[&Value],
+    work: &mut usize,
+) -> Check<bool> {
+    let left_key = key(left, work)?;
+    let right_key = key(right, work)?;
+    if left_key == right_key || literal(right) == Ok(0) {
+        return Ok(true);
+    }
+    if let (Ok(a), Ok(b)) = (literal(left), literal(right)) {
+        return Ok(a >= b);
+    }
+    for fact in facts {
+        if supports(fact, &left_key, &right_key, work, 0)? {
+            return Ok(true);
+        }
+    }
+    Ok(false)
+}
+
+/// The Core term `core.bytes.length<coordinate>(bytes)`, for slice end proofs.
+pub(super) fn length_of(coordinate: &Value, bytes: &Value) -> Value {
+    Value::Map(vec![
+        (Value::Text("kind".into()), Value::Text("call".into())),
+        (
+            Value::Text("callee".into()),
+            Value::Text("core.bytes.length".into()),
+        ),
+        (
+            Value::Text("typeArgs".into()),
+            Value::Array(vec![coordinate.clone()]),
+        ),
+        (
+            Value::Text("args".into()),
+            Value::Array(vec![bytes.clone()]),
+        ),
+    ])
+}
+
+fn supports(
+    fact: &Value,
+    left: &[u8],
+    right: &[u8],
+    work: &mut usize,
+    depth: usize,
+) -> Check<bool> {
+    debit(work, 1)?;
+    if depth > 64 {
+        return Err(());
+    }
+    match string(get(fact, "kind")?)? {
+        "all" => {
+            for item in list(get(fact, "values")?)? {
+                if supports(item, left, right, work, depth + 1)? {
+                    return Ok(true);
+                }
+            }
+            Ok(false)
+        }
+        "compare" => {
+            let a = key(get(fact, "left")?, work)?;
+            let b = key(get(fact, "right")?, work)?;
+            Ok(match string(get(fact, "op")?)? {
+                ">=" | ">" => a == left && b == right,
+                "<=" | "<" => a == right && b == left,
+                "==" => (a == left && b == right) || (a == right && b == left),
+                _ => false,
+            })
+        }
+        _ => Ok(false),
+    }
+}
+
+/// Terms compare by canonical encoding, independent of in-memory map order.
+fn key(value: &Value, work: &mut usize) -> Check<Vec<u8>> {
+    let bytes = echo_edict_canonical::encode_canonical_cbor_v1(value).map_err(|_| ())?;
+    debit(work, bytes.len())?;
+    Ok(bytes)
+}
+
+fn debit(work: &mut usize, amount: usize) -> Check<()> {
+    *work = work.checked_sub(amount).ok_or(())?;
+    Ok(())
+}

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

@@ -4,17 +4,23 @@
 use super::{get, list, literal, string, Check, Value};
 
 /// Whether an intent body calls an operation only this judgment checks: an
-/// addition's no-overflow proof or a count's full-byte scan charge. A Core
-/// without a function table still needs the judgment for either.
+/// addition's no-overflow proof, a subtraction's or slice's range proof, or a
+/// count's full-byte scan charge. A Core without a function table still needs
+/// the judgment for any of them.
 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) => {
+                // Each of these needs an intent-level proof, even without a
+                // source-function table.
                 if get(value, "kind").and_then(string) == Ok("call")
                     && matches!(
                         get(value, "callee").and_then(string),
-                        Ok("core.integer.add" | "core.bytes.count")
+                        Ok("core.integer.add"
+                            | "core.integer.subtract"
+                            | "core.bytes.slice"
+                            | "core.bytes.count")
                     )
                 {
                     return Ok(true);

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

@@ -344,12 +344,28 @@ 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.
+            // The source-function audit has independently proved totality and order.
             ("core.integer.add", [left, right], [expected @ Schema::Word(_)])
                 if left == expected && right == expected =>
             {
                 Ok(expected.clone())
             }
+            ("core.integer.subtract", [left, right], [expected @ Schema::Word(_)])
+                if expected.includes(left) && expected.includes(right) =>
+            {
+                Ok(expected.clone())
+            }
+            // The same audit independently proved start <= end <= len(bytes).
+            (
+                "core.bytes.slice",
+                [actual, Schema::Word(a), Schema::Word(b)],
+                [expected @ Schema::Bytes { upper, .. }],
+            ) if *a == u64::MAX && *b == u64::MAX && expected.includes(actual) => {
+                Ok(Schema::Bytes {
+                    lower: 0,
+                    upper: *upper,
+                })
+            }
             ("core.bytes.isUtf8", [actual], [expected @ Schema::Bytes { .. }])
                 if expected == actual =>
             {

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

@@ -2,6 +2,7 @@
 // © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
 //! Independent verifier judgment: inventory authority, eliminate dependency leaves,
 //! then audit ordered lexical frames and conservative whole-operation charges.
+mod order;
 mod types;
 mod unsigned_addition;
 use super::ProviderRefusalV1;
@@ -520,12 +521,28 @@ impl<'a> Checker<'a, '_> {
                     } else {
                         false
                     };
+                    let order_proven = match name {
+                        "core.integer.subtract" => {
+                            let [left, right] = arguments else {
+                                return Err(());
+                            };
+                            order::proven(left, right, &self.proven, self.types)?
+                        }
+                        "core.bytes.slice" => {
+                            let [coordinate] = types else {
+                                return Err(());
+                            };
+                            order::slice_in_range(coordinate, arguments, &self.proven, self.types)?
+                        }
+                        _ => false,
+                    };
                     let (schema, intrinsic) = intrinsic(
                         name,
                         arguments,
                         &argument_schemas,
                         &declared,
                         addition_proven,
+                        order_proven,
                     )?;
                     charge.append(intrinsic)?;
                     schema
@@ -745,6 +762,7 @@ fn intrinsic(
     actual: &[Schema],
     declared: &[Schema],
     addition_proven: bool,
+    order_proven: bool,
 ) -> Check<(Schema, Charge)> {
     let literal = |value: &Value| -> Check<u64> {
         if string(get(value, "kind")?)? != "const" {
@@ -822,9 +840,9 @@ fn intrinsic(
         ("core.integer.subtract", [left, right], [expected @ Schema::Word(_)])
             if expected.encloses(left) && expected.encloses(right) =>
         {
-            literal(&arguments[0])?
-                .checked_sub(literal(&arguments[1])?)
-                .ok_or(())?;
+            if !order_proven {
+                return Err(());
+            }
             Ok((
                 expected.clone(),
                 Charge {
@@ -836,19 +854,24 @@ fn intrinsic(
         (
             "core.bytes.slice",
             [actual, Schema::Word(a), Schema::Word(b)],
-            [expected @ Schema::Blob { low, .. }],
+            [expected @ Schema::Blob { low, high }],
         ) if *a == u64::MAX && *b == u64::MAX && expected.encloses(actual) => {
-            let start = literal(&arguments[1])?;
-            let end = literal(&arguments[2])?;
-            if start > end || end > *low {
-                return Err(());
-            }
-            let high = end - start;
+            // Literal offsets within the guaranteed minimum length need no
+            // fact; any other offsets need start <= end <= len(bytes).
+            let copied = match (literal(&arguments[1]), literal(&arguments[2])) {
+                (Ok(start), Ok(end)) if start <= end && end <= *low => end - start,
+                _ if order_proven => *high,
+                _ => return Err(()),
+            };
+            // As in Edict, a slice keeps its operand's maximum and no minimum.
             Ok((
-                Schema::Blob { low: 0, high },
+                Schema::Blob {
+                    low: 0,
+                    high: *high,
+                },
                 Charge {
-                    ticks: u128::from(high) + 4,
-                    storage: u128::from(high) + 64,
+                    ticks: u128::from(copied) + 4,
+                    storage: u128::from(copied) + 64,
                 },
             ))
         }