feat: execute and verify core.bytes.count

CHANGELOG.md

@@ -342,6 +342,18 @@
 
 ### Added
 
+- 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
+  independently, including on the bounded-read route, and their addition
+  proofs bound it by the operand's byte maximum, resolving named byte types
+  through the module's type table. A count triggers that judgment even in a
+  Core without source functions or additions, so its scan is always charged
+  against the step ceiling. A binding whose value is an addition reuses the cap
+  its no-overflow proof established instead of recomputing it. Proven unsigned bounds now
+  travel through let bindings in intent and helper bodies, so Jim's
+  `lineCount = lineBreaks + 1` is proven.
+
 - 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

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

@@ -317,6 +317,9 @@ impl<'a> Scope<'a> {
         let args = super::array(value, "args")?;
         let types = super::array(value, "typeArgs")?;
         let name = text(value, "callee")?;
+        // A count's needle is a one-byte constant, checked structurally.
+        let args = crate::executable_operation::source_functions::checked_arguments(name, args)
+            .map_err(|()| invalid())?;
         let actual = args
             .iter()
             .map(|value| self.expression(value, depth + 1))
@@ -372,6 +375,11 @@ impl<'a> Scope<'a> {
             {
                 Ok(ReadType::Bool)
             }
+            ("core.bytes.count", [actual], [expected @ ReadType::Bytes(_, _)])
+                if expected == actual =>
+            {
+                Ok(ReadType::Unsigned(u64::MAX))
+            }
             ("core.bytes.length", [actual], [expected @ ReadType::Bytes(_, _)])
                 if expected.accepts(actual) =>
             {

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

@@ -66,6 +66,11 @@ struct Judgment<'a> {
     active: BTreeSet<String>,
     work: usize,
     proven: Vec<&'a Value>,
+    /// Proven caps of earlier unsigned let bindings in the current body.
+    bound: Vec<(&'a Value, u64)>,
+    /// The refined cap of the addition `expression` last proved, keyed by the
+    /// node's address, so the binding that holds it reuses the proof.
+    proven_sum: Option<(usize, u64)>,
 }
 
 pub(super) fn validate(core: &Value, exports: &Value, read: bool) -> Result<(), ProviderRefusalV1> {
@@ -160,6 +165,8 @@ fn run(core: &Value, exports: &Value, read: bool) -> Check<()> {
         active: BTreeSet::new(),
         work: WORK,
         proven: Vec::new(),
+        bound: Vec::new(),
+        proven_sum: None,
     };
     for name in proof.functions.keys().cloned().collect::<Vec<_>>() {
         proof.function(&name, 1)?;
@@ -173,6 +180,51 @@ fn run(core: &Value, exports: &Value, read: bool) -> Check<()> {
     Ok(())
 }
 impl<'a> Judgment<'a> {
+    /// An unsigned binding carries its proven cap to later evaluation in the
+    /// same body. Local identities are unique and immutable.
+    fn record_bound(&mut self, local: &'a Value, value: &Value, ty: &Ty) -> Check<()> {
+        let Ty::Word(max) = ty else { return Ok(()) };
+        if !matches!(*max, 4_294_967_295 | 18_446_744_073_709_551_615) {
+            return Ok(());
+        }
+        // `expression` already proved this addition and computed its cap.
+        let proven = self.proven_sum.take();
+        if let Some((node, cap)) = proven {
+            if node == std::ptr::from_ref(value).addr() {
+                if cap < *max {
+                    self.bound.push((local, cap));
+                }
+                return Ok(());
+            }
+        }
+        let counts = self.count_maxima(std::slice::from_ref(value))?;
+        let facts = unsigned_addition::Facts {
+            predicates: &self.proven,
+            locals: &self.bound,
+            counts: &counts,
+        };
+        let cap = unsigned_addition::ceiling(value, *max, &facts, &mut self.work)?;
+        if cap < *max {
+            self.bound.push((local, cap));
+        }
+        Ok(())
+    }
+    /// The byte maximum of every counted operand an addition proof can reach,
+    /// resolved through this module's type table so named byte types count.
+    fn count_maxima(&mut self, exprs: &[Value]) -> Check<Vec<(String, u64)>> {
+        let mut found = Vec::new();
+        for expr in exprs {
+            unsigned_addition::counted_coordinates(expr, &mut found, 0)?;
+        }
+        let mut counts = Vec::with_capacity(found.len());
+        for coordinate in found {
+            let Ty::Bytes(_, max) = self.ty(coordinate, 0)? else {
+                return Err(());
+            };
+            counts.push((coordinate.to_owned(), max));
+        }
+        Ok(counts)
+    }
     fn charge(&mut self, depth: usize) -> Check<()> {
         self.work = self.work.checked_sub(1).ok_or(())?;
         if depth > DEPTH {
@@ -286,8 +338,10 @@ impl<'a> Judgment<'a> {
         // 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 caller_bounds = std::mem::take(&mut self.bound);
         let result = self.check_function_body(name, prefix);
         self.proven = caller_facts;
+        self.bound = caller_bounds;
         self.active.remove(name);
         result
     }
@@ -323,6 +377,7 @@ impl<'a> Judgment<'a> {
             if !includes(&expected, &fact.ty) {
                 return Err(());
             }
+            self.record_bound(local, get(binding, "value")?, &expected)?;
             let (_, validations, _, ty_depth) = shape(&expected)?;
             cost = cost.plus(fact.cost)?.plus(Cost {
                 steps: validations,
@@ -463,7 +518,7 @@ impl<'a> Judgment<'a> {
                 let arguments = list(get(value, "args")?)?;
                 let types = list(get(value, "typeArgs")?)?;
                 let mut actual = Vec::new();
-                for argument in arguments {
+                for argument in checked_arguments(name, arguments)? {
                     let fact = self.expression(argument, scope, source, prefix + 1)?;
                     cost = cost.plus(fact.cost)?;
                     depth = depth.max(fact.depth + 1);
@@ -508,6 +563,16 @@ impl<'a> Judgment<'a> {
                             })?;
                             Ty::Bool
                         }
+                        ("core.bytes.count", [actual], [expected @ Ty::Bytes(_, max)])
+                            if expected == actual =>
+                        {
+                            // One complete scan plus the materialized one-byte needle.
+                            cost = cost.plus(Cost {
+                                steps: max.checked_add(3).ok_or(())?,
+                                bytes: 128,
+                            })?;
+                            Ty::Word(u64::MAX)
+                        }
                         ("core.bytes.length", [actual], [expected @ Ty::Bytes(_, _)])
                             if includes(expected, actual) =>
                         {
@@ -535,12 +600,15 @@ impl<'a> Judgment<'a> {
                                 && 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,
-                            )?;
+                            let counts = self.count_maxima(arguments)?;
+                            let facts = unsigned_addition::Facts {
+                                predicates: &self.proven,
+                                locals: &self.bound,
+                                counts: &counts,
+                            };
+                            let cap =
+                                unsigned_addition::prove(value, *max, &facts, &mut self.work)?;
+                            self.proven_sum = Some((std::ptr::from_ref(value).addr(), cap));
                             cost = cost.plus(Cost {
                                 steps: 3,
                                 bytes: 64,
@@ -652,6 +720,7 @@ impl<'a> Judgment<'a> {
     }
     fn intent(&mut self, intent: &'a Value, read: bool) -> Check<()> {
         self.proven.clear();
+        self.bound.clear();
         let body = get(intent, "body")?;
         exact(body, &["locals", "nodes", "result"])?;
         let mut pending = BTreeMap::new();
@@ -712,6 +781,7 @@ impl<'a> Judgment<'a> {
                     if !includes(&ty, &fact.ty) {
                         return Err(());
                     }
+                    self.record_bound(get(node, "binding")?, get(node, "value")?, &ty)?;
                     cost = cost.plus(fact.cost)?.plus(Cost {
                         steps: shape(&ty)?.1,
                         bytes: 0,
@@ -883,6 +953,29 @@ fn decimal(value: &str) -> Check<u64> {
     }
     Ok(parsed)
 }
+/// A count's needle is a Core constant of exactly one byte, checked
+/// structurally and excluded from ordinary expression typing.
+pub(super) fn checked_arguments<'a>(name: &str, arguments: &'a [Value]) -> Check<&'a [Value]> {
+    if name != "core.bytes.count" {
+        return Ok(arguments);
+    }
+    let [operand, needle] = arguments else {
+        return Err(());
+    };
+    exact(needle, &["kind", "value"])?;
+    let literal = get(needle, "value")?;
+    exact(literal, &["kind", "value"])?;
+    if string(get(needle, "kind")?)? != "const" || string(get(literal, "kind")?)? != "bytes" {
+        return Err(());
+    }
+    let Value::Bytes(byte) = get(literal, "value")? else {
+        return Err(());
+    };
+    if byte.len() != 1 {
+        return Err(());
+    }
+    Ok(std::slice::from_ref(operand))
+}
 fn literal(value: &Value) -> Check<u64> {
     if string(get(value, "kind")?)? != "const" {
         return Err(());

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

@@ -3,13 +3,19 @@
 //! Lowerer-owned recursive upper bounds over checked, dominating predicates.
 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.
 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")
+                    && matches!(
+                        get(value, "callee").and_then(string),
+                        Ok("core.integer.add" | "core.bytes.count")
+                    )
                 {
                     return Ok(true);
                 }
@@ -22,14 +28,27 @@ pub(super) fn present(core: &Value) -> Check<bool> {
     Ok(false)
 }
 
-pub(super) fn prove(args: &[Value], max: u64, facts: &[&Value], work: &mut usize) -> Check<()> {
-    let [left, right] = args else { return Err(()) };
+/// Facts a proof reads: dominating predicates, carried binding caps, and the
+/// resolved byte maximum of every counted operand coordinate.
+pub(super) struct Facts<'f, 'v> {
+    pub predicates: &'f [&'v Value],
+    pub locals: &'f [(&'v Value, u64)],
+    pub counts: &'f [(String, u64)],
+}
+
+/// Proves an addition total and returns its refined cap, exactly the value
+/// [`ceiling`] gives the same expression, so a binding need not recompute it.
+pub(super) fn prove(expr: &Value, max: u64, facts: &Facts<'_, '_>, work: &mut usize) -> Check<u64> {
+    let [left, right] = list(get(expr, "args")?)? else {
+        return Err(());
+    };
     let left = bound(left, max, facts, work, 0)?;
     let right = bound(right, max, facts, work, 0)?;
-    left.checked_add(right)
+    let sum = left
+        .checked_add(right)
         .filter(|sum| *sum <= max)
         .ok_or(())?;
-    Ok(())
+    refined(expr, sum, facts, work, 0)
 }
 fn debit(work: &mut usize, amount: usize) -> Check<()> {
     *work = work.checked_sub(amount).ok_or(())?;
@@ -42,12 +61,56 @@ fn same(a: &Value, b: &Value, work: &mut usize) -> Check<bool> {
     }
     Ok(a == b)
 }
-fn bound(expr: &Value, max: u64, facts: &[&Value], work: &mut usize, depth: usize) -> Check<u64> {
+/// The proven cap of one expression, for a binding's carried bound.
+pub(super) fn ceiling(
+    expr: &Value,
+    max: u64,
+    facts: &Facts<'_, '_>,
+    work: &mut usize,
+) -> Check<u64> {
+    bound(expr, max, facts, work, 0)
+}
+/// Coordinates of every count a bound can reach through additions; the caller
+/// resolves each through its own type table.
+pub(super) fn counted_coordinates<'v>(
+    expr: &'v Value,
+    found: &mut Vec<&'v str>,
+    depth: usize,
+) -> Check<()> {
+    if depth > 64 {
+        return Err(());
+    }
+    if string(get(expr, "kind")?)? != "call" {
+        return Ok(());
+    }
+    match string(get(expr, "callee")?)? {
+        "core.integer.add" => {
+            for operand in list(get(expr, "args")?)? {
+                counted_coordinates(operand, found, depth + 1)?;
+            }
+        }
+        "core.bytes.count" => {
+            let [coordinate] = list(get(expr, "typeArgs")?)? else {
+                return Err(());
+            };
+            found.push(string(coordinate)?);
+        }
+        _ => {}
+    }
+    Ok(())
+}
+fn bound(
+    expr: &Value,
+    max: u64,
+    facts: &Facts<'_, '_>,
+    work: &mut usize,
+    depth: usize,
+) -> Check<u64> {
     debit(work, 1)?;
     if depth > 64 {
         return Err(());
     }
-    let mut upper = if string(get(expr, "kind")?)? == "call"
+    let upper = if string(get(expr, "kind")?)? == "call"
         && string(get(expr, "callee")?)? == "core.integer.add"
     {
         let [left, right] = list(get(expr, "args")?)? else {
@@ -56,10 +119,44 @@ fn bound(expr: &Value, max: u64, facts: &[&Value], work: &mut usize, depth: usiz
         bound(left, max, facts, work, depth + 1)?
             .checked_add(bound(right, max, facts, work, depth + 1)?)
             .ok_or(())?
+    } else if string(get(expr, "kind")?)? == "call"
+        && string(get(expr, "callee")?)? == "core.bytes.count"
+    {
+        // A count never exceeds its operand's structural byte maximum, named or
+        // literal, as the caller resolved it.
+        let [coordinate] = list(get(expr, "typeArgs")?)? else {
+            return Err(());
+        };
+        let coordinate = string(coordinate)?;
+        facts
+            .counts
+            .iter()
+            .find(|(name, _)| name == coordinate)
+            .map(|(_, bytes)| (*bytes).min(max))
+            .ok_or(())?
+    } else if string(get(expr, "kind")?)? == "local" {
+        let reference = get(expr, "ref")?;
+        let mut upper = max;
+        for (local, cap) in facts.locals {
+            if same(local, reference, work)? {
+                upper = upper.min(*cap);
+            }
+        }
+        upper
     } else {
         literal(expr).unwrap_or(max)
     };
-    for predicate in facts {
+    refined(expr, upper, facts, work, depth)
+}
+/// Narrows a structural cap by every dominating predicate about `expr`.
+fn refined(
+    expr: &Value,
+    mut upper: u64,
+    facts: &Facts<'_, '_>,
+    work: &mut usize,
+    depth: usize,
+) -> Check<u64> {
+    for predicate in facts.predicates {
         refine(predicate, expr, &mut upper, work, depth + 1)?;
     }
     Ok(upper)