diff --git a/CHANGELOG.md b/CHANGELOG.md
index 928e9360..2ae4039c 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/crates/echo-edict-provider-lowerer/src/executable_operation/bounded_read/relation/types.rs b/crates/echo-edict-provider-lowerer/src/executable_operation/bounded_read/relation/types.rs
index 82d339dd..00b71226 100644
--- a/crates/echo-edict-provider-lowerer/src/executable_operation/bounded_read/relation/types.rs
+++ b/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) =>
             {
diff --git a/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions.rs b/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions.rs
index ec1d5f45..ae014233 100644
--- a/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions.rs
+++ b/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(());
diff --git a/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/unsigned_addition.rs b/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/unsigned_addition.rs
index 36cb3e49..527670b1 100644
--- a/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/unsigned_addition.rs
+++ b/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)
diff --git a/crates/echo-edict-provider-verifier/src/executable_operation/bounded_read/audit/types.rs b/crates/echo-edict-provider-verifier/src/executable_operation/bounded_read/audit/types.rs
index 14975252..2fb5d8cc 100644
--- a/crates/echo-edict-provider-verifier/src/executable_operation/bounded_read/audit/types.rs
+++ b/crates/echo-edict-provider-verifier/src/executable_operation/bounded_read/audit/types.rs
@@ -303,7 +303,9 @@ impl<'a> Symbols<'a> {
         let args = super::sequence(value, "args")?;
         let types = super::sequence(value, "typeArgs")?;
         let mut actual = Vec::new();
-        for argument in args {
+        for argument in
+            crate::executable_operation::source_functions::checked_arguments(name, args)?
+        {
             actual.push(self.expression(argument, depth + 1)?);
         }
         let core = self.core;
@@ -353,6 +355,11 @@ impl<'a> Symbols<'a> {
             {
                 Ok(Schema::Boolean)
             }
+            ("core.bytes.count", [actual], [expected @ Schema::Bytes { .. }])
+                if expected == actual =>
+            {
+                Ok(Schema::Word(u64::MAX))
+            }
             ("core.bytes.length", [actual], [expected @ Schema::Bytes { .. }])
                 if expected.includes(actual) =>
             {
diff --git a/crates/echo-edict-provider-verifier/src/executable_operation/source_functions.rs b/crates/echo-edict-provider-verifier/src/executable_operation/source_functions.rs
index cf5f311a..aa4166eb 100644
--- a/crates/echo-edict-provider-verifier/src/executable_operation/source_functions.rs
+++ b/crates/echo-edict-provider-verifier/src/executable_operation/source_functions.rs
@@ -110,6 +110,7 @@ fn audit(core: &Value, exports: &Value, read: bool) -> Check<()> {
                         }
                         edges.insert(callee);
                     } else if ![
+                        "core.bytes.count",
                         "core.bytes.isUtf8",
                         "core.bytes.length",
                         "core.bytes.concat",
@@ -148,6 +149,8 @@ fn audit(core: &Value, exports: &Value, read: bool) -> Check<()> {
             definitions: &definitions,
             summaries: &summaries,
             proven: Vec::new(),
+            bound: Vec::new(),
+            proven_sum: None,
         }
         .function(definition)?;
         if summary.height + 1 > 64 {
@@ -172,6 +175,8 @@ fn audit(core: &Value, exports: &Value, read: bool) -> Check<()> {
         definitions: &definitions,
         summaries: &summaries,
         proven: Vec::new(),
+        bound: Vec::new(),
+        proven_sum: None,
     };
     if super::map_field(core, "functions").is_none() && !unsigned_addition::present(core)? {
         return Ok(());
@@ -282,8 +287,38 @@ struct Checker<'a, 'b> {
     definitions: &'b BTreeMap<String, Definition<'a>>,
     summaries: &'b BTreeMap<String, Summary>,
     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)>,
 }
 impl<'a> Checker<'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, schema: &Schema) -> Check<()> {
+        let Schema::Word(max) = schema 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.
+        if let Some((node, cap)) = self.proven_sum.take() {
+            if node == std::ptr::from_ref(value).addr() {
+                if cap < *max {
+                    self.bound.push((local, cap));
+                }
+                return Ok(());
+            }
+        }
+        let cap =
+            unsigned_addition::ceiling_of(value, *max, &self.proven, &self.bound, self.types)?;
+        if cap < *max {
+            self.bound.push((local, cap));
+        }
+        Ok(())
+    }
     fn function(&mut self, definition: &Definition<'a>) -> Check<Summary> {
         let declarations = sequence(get(definition.body, "locals")?)?;
         let mut frame = Frame::new(definition.params.iter().chain(declarations), self.types)?;
@@ -304,6 +339,7 @@ impl<'a> Checker<'a, '_> {
             if !declared.encloses(&value.schema) {
                 return Err(());
             }
+            self.record_bound(local, get(binding, "value")?, &declared)?;
             let size = declared.measure()?;
             charge.append(value.charge)?;
             charge.append(Charge {
@@ -432,7 +468,7 @@ impl<'a> Checker<'a, '_> {
                 let arguments = sequence(get(value, "args")?)?;
                 let types = sequence(get(value, "typeArgs")?)?;
                 let mut argument_schemas = Vec::new();
-                for argument in arguments {
+                for argument in checked_arguments(name, arguments)? {
                     let argument = self.expression(argument, frame, depth + 1)?;
                     charge.append(argument.charge)?;
                     height = height.max(argument.height + 1);
@@ -472,7 +508,14 @@ impl<'a> Checker<'a, '_> {
                         if !matches!(*max, 4_294_967_295 | 18_446_744_073_709_551_615) {
                             return Err(());
                         }
-                        unsigned_addition::prove(arguments, *max, &self.proven, self.types)?;
+                        let cap = unsigned_addition::prove(
+                            value,
+                            *max,
+                            &self.proven,
+                            &self.bound,
+                            self.types,
+                        )?;
+                        self.proven_sum = Some((std::ptr::from_ref(value).addr(), cap));
                         true
                     } else {
                         false
@@ -578,6 +621,7 @@ impl<'a> Checker<'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 frame = Frame::new(sequence(get(body, "locals")?)?, self.types)?;
@@ -620,6 +664,7 @@ impl<'a> Checker<'a, '_> {
                     if !expected.encloses(&value.schema) {
                         return Err(());
                     }
+                    self.record_bound(local, get(node, "value")?, &expected)?;
                     charge.append(value.charge)?;
                     charge.append(Charge {
                         ticks: expected.measure()?.checks,
@@ -671,6 +716,29 @@ impl<'a> Checker<'a, '_> {
         Ok(())
     }
 }
+/// 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<'v>(name: &str, arguments: &'v [Value]) -> Check<&'v [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 intrinsic(
     name: &str,
     arguments: &[Value],
@@ -696,6 +764,18 @@ fn intrinsic(
                 },
             ))
         }
+        ("core.bytes.count", [actual], [expected @ Schema::Blob { high, .. }])
+            if expected == actual =>
+        {
+            // One complete scan plus the materialized one-byte needle.
+            Ok((
+                Schema::Word(u64::MAX),
+                Charge {
+                    ticks: u128::from(*high) + 3,
+                    storage: 128,
+                },
+            ))
+        }
         ("core.bytes.length", [actual], [expected @ Schema::Blob { .. }])
             if expected.encloses(actual) =>
         {
diff --git a/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/unsigned_addition.rs b/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/unsigned_addition.rs
index a1283926..1f16a302 100644
--- a/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/unsigned_addition.rs
+++ b/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/unsigned_addition.rs
@@ -1,8 +1,11 @@
 // SPDX-License-Identifier: Apache-2.0
 // © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
 //! Verifier-owned inventory of canonical-expression caps and independent composition.
-use super::{get, sequence, string, unsigned, Check, Types, Value};
+use super::{get, sequence, string, unsigned, Check, Schema, Types, 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 layers = vec![get(core, "intents")?];
     while !layers.is_empty() {
@@ -10,8 +13,10 @@ pub(super) fn present(core: &Value) -> Check<bool> {
         for value in layers {
             if let Value::Map(entries) = value {
                 if string(get(value, "kind").unwrap_or(&Value::Null)) == Ok("call")
-                    && string(get(value, "callee").unwrap_or(&Value::Null))
-                        == Ok("core.integer.add")
+                    && matches!(
+                        string(get(value, "callee").unwrap_or(&Value::Null)),
+                        Ok("core.integer.add" | "core.bytes.count")
+                    )
                 {
                     return Ok(true);
                 }
@@ -25,13 +30,39 @@ pub(super) fn present(core: &Value) -> Check<bool> {
     Ok(false)
 }
 
+/// Proves an addition total and returns its refined cap, exactly the value
+/// [`ceiling_of`] gives the same expression, so a binding need not recompute it.
 pub(super) fn prove(
-    args: &[Value],
+    expr: &Value,
+    max: u64,
+    facts: &[&Value],
+    locals: &[(&Value, u64)],
+    types: &mut Types<'_>,
+) -> Check<u64> {
+    let [left, right] = sequence(get(expr, "args")?)? else {
+        return Err(());
+    };
+    let caps = caps(facts, types)?;
+    let a = ceiling(left, max, &caps, locals, types, 0)?;
+    let b = ceiling(right, max, &caps, locals, types, 0)?;
+    let sum = u128::from(a) + u128::from(b);
+    if sum > u128::from(max) {
+        return Err(());
+    }
+    refined(expr, sum, &caps, types)
+}
+/// The proven cap of one expression, for a binding's carried bound.
+pub(super) fn ceiling_of(
+    expr: &Value,
     max: u64,
     facts: &[&Value],
+    locals: &[(&Value, u64)],
     types: &mut Types<'_>,
-) -> Check<()> {
-    let [left, right] = args else { return Err(()) };
+) -> Check<u64> {
+    let caps = caps(facts, types)?;
+    ceiling(expr, max, &caps, locals, types, 0)
+}
+fn caps(facts: &[&Value], types: &mut Types<'_>) -> Check<Vec<(Vec<u8>, u64)>> {
     let mut pending: Vec<_> = facts.iter().map(|value| (*value, 0)).collect();
     let mut caps = Vec::new();
     while let Some((predicate, depth)) = pending.pop() {
@@ -60,12 +91,7 @@ pub(super) fn prove(
             _ => {}
         }
     }
-    let a = ceiling(left, max, &caps, types, 0)?;
-    let b = ceiling(right, max, &caps, types, 0)?;
-    if u128::from(a) + u128::from(b) > u128::from(max) {
-        return Err(());
-    }
-    Ok(())
+    Ok(caps)
 }
 fn constant(expr: &Value) -> Option<u64> {
     if string(get(expr, "kind").ok()?).ok()? != "const" {
@@ -82,21 +108,57 @@ fn ceiling(
     expr: &Value,
     max: u64,
     caps: &[(Vec<u8>, u64)],
+    locals: &[(&Value, u64)],
     types: &mut Types<'_>,
     depth: usize,
 ) -> Check<u64> {
     types.step(depth)?;
-    let mut value = if string(get(expr, "kind")?)? == "call"
+    let value = if string(get(expr, "kind")?)? == "call"
         && string(get(expr, "callee")?)? == "core.integer.add"
     {
         let [a, b] = sequence(get(expr, "args")?)? else {
             return Err(());
         };
-        u128::from(ceiling(a, max, caps, types, depth + 1)?)
-            + u128::from(ceiling(b, max, caps, types, depth + 1)?)
+        u128::from(ceiling(a, max, caps, locals, types, depth + 1)?)
+            + u128::from(ceiling(b, max, caps, locals, types, depth + 1)?)
+    } else if string(get(expr, "kind")?)? == "call"
+        && string(get(expr, "callee")?)? == "core.bytes.count"
+    {
+        // A count never exceeds its operand's structural byte maximum, resolved
+        // through the module's type table so named byte types count too.
+        let [coordinate] = sequence(get(expr, "typeArgs")?)? else {
+            return Err(());
+        };
+        let Schema::Blob { high, .. } = types
+            .resolve(string(coordinate)?, depth + 1)?
+            .representation()
+            .clone()
+        else {
+            return Err(());
+        };
+        u128::from(high.min(max))
+    } else if string(get(expr, "kind")?)? == "local" {
+        let reference = get(expr, "ref")?;
+        let mut upper = max;
+        for (local, cap) in locals {
+            types.proof_work(1)?;
+            if *local == reference {
+                upper = upper.min(*cap);
+            }
+        }
+        u128::from(upper)
     } else {
         constant(expr).map_or_else(|| u128::from(max), u128::from)
     };
+    refined(expr, value, caps, types)
+}
+/// Narrows a structural cap by every proven cap on exactly `expr`.
+fn refined(
+    expr: &Value,
+    mut value: u128,
+    caps: &[(Vec<u8>, u64)],
+    types: &mut Types<'_>,
+) -> Check<u64> {
     let encoded = key(expr, types)?;
     for (term, cap) in caps {
         types.proof_work(encoded.len().min(term.len()).checked_add(1).ok_or(())?)?;
diff --git a/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions.rs b/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions.rs
index e39e6db0..ca0a77b5 100644
--- a/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions.rs
+++ b/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions.rs
@@ -48,6 +48,11 @@ fn read_helper() -> LoweringRequestV1 {
     read_helper_with_budget(4_194_304)
 }
 fn read_helper_with_budget(max_steps: u64) -> LoweringRequestV1 {
+    read_with_budget(max_steps, true)
+}
+/// The real read fixture at an explicit step ceiling, with or without the
+/// pure source helper; without it, the Core has no function table.
+fn read_with_budget(max_steps: u64, helper: bool) -> LoweringRequestV1 {
     let mut source = fixture();
     let mut core = decode(&source.core.artifact.bytes).expect("core");
     let mut target = decode(&source.semantic_inputs[5].artifact.artifact.bytes).expect("target");
@@ -61,88 +66,90 @@ fn read_helper_with_budget(max_steps: u64) -> LoweringRequestV1 {
         panic!("output type")
     };
     let output_type = output_type.clone();
-    let parameter = local("arg.0", &output_type);
-    let helper_local = local("local.0", &output_type);
-    insert(
-        &mut core,
-        "functions",
-        map([(
-            "retain",
-            map([
-                ("params", Value::Array(vec![parameter.clone()])),
-                ("returnType", text(&output_type)),
-                (
-                    "body",
-                    map([
-                        ("locals", Value::Array(vec![helper_local.clone()])),
-                        (
-                            "bindings",
-                            Value::Array(vec![map([
-                                ("kind", text("let")),
-                                ("binding", helper_local.clone()),
-                                ("value", reference(&parameter)),
-                            ])]),
-                        ),
-                        ("result", reference(&helper_local)),
-                    ]),
-                ),
-            ]),
-        )]),
-    );
-    let saved = local("source.return", &output_type);
-    let body = field_mut(intent(&mut core), "body");
-    let call = map([
-        ("kind", text("call")),
-        ("callee", text(&format!("{coordinate}.retain"))),
-        ("args", Value::Array(vec![field(body, "result").clone()])),
-        ("typeArgs", Value::Array(vec![])),
-    ]);
-    let Value::Array(locals) = field_mut(body, "locals") else {
-        panic!("locals")
-    };
-    locals.push(saved.clone());
-    let Value::Array(nodes) = field_mut(body, "nodes") else {
-        panic!("nodes")
-    };
-    nodes.push(map([
-        ("kind", text("let")),
-        ("binding", saved.clone()),
-        ("value", call.clone()),
-    ]));
-    *field_mut(body, "result") = reference(&saved);
-    let target_intent = intent(&mut target);
-    let binding = map([
-        ("id", text("replaceRange.binding.0")),
-        ("binding", saved.clone()),
-        ("value", call),
-    ]);
-    let Value::Map(entries) = target_intent else {
-        panic!("intent")
-    };
-    match entries
-        .iter_mut()
-        .find(|(key, _)| key == &text("pureBindings"))
-    {
-        Some((_, Value::Array(bindings))) => bindings.push(binding),
-        None => entries.push((text("pureBindings"), Value::Array(vec![binding]))),
-        _ => panic!("pure bindings"),
+    if helper {
+        let parameter = local("arg.0", &output_type);
+        let helper_local = local("local.0", &output_type);
+        insert(
+            &mut core,
+            "functions",
+            map([(
+                "retain",
+                map([
+                    ("params", Value::Array(vec![parameter.clone()])),
+                    ("returnType", text(&output_type)),
+                    (
+                        "body",
+                        map([
+                            ("locals", Value::Array(vec![helper_local.clone()])),
+                            (
+                                "bindings",
+                                Value::Array(vec![map([
+                                    ("kind", text("let")),
+                                    ("binding", helper_local.clone()),
+                                    ("value", reference(&parameter)),
+                                ])]),
+                            ),
+                            ("result", reference(&helper_local)),
+                        ]),
+                    ),
+                ]),
+            )]),
+        );
+        let saved = local("source.return", &output_type);
+        let body = field_mut(intent(&mut core), "body");
+        let call = map([
+            ("kind", text("call")),
+            ("callee", text(&format!("{coordinate}.retain"))),
+            ("args", Value::Array(vec![field(body, "result").clone()])),
+            ("typeArgs", Value::Array(vec![])),
+        ]);
+        let Value::Array(locals) = field_mut(body, "locals") else {
+            panic!("locals")
+        };
+        locals.push(saved.clone());
+        let Value::Array(nodes) = field_mut(body, "nodes") else {
+            panic!("nodes")
+        };
+        nodes.push(map([
+            ("kind", text("let")),
+            ("binding", saved.clone()),
+            ("value", call.clone()),
+        ]));
+        *field_mut(body, "result") = reference(&saved);
+        let target_intent = intent(&mut target);
+        let binding = map([
+            ("id", text("replaceRange.binding.0")),
+            ("binding", saved.clone()),
+            ("value", call),
+        ]);
+        let Value::Map(entries) = target_intent else {
+            panic!("intent")
+        };
+        match entries
+            .iter_mut()
+            .find(|(key, _)| key == &text("pureBindings"))
+        {
+            Some((_, Value::Array(bindings))) => bindings.push(binding),
+            None => entries.push((text("pureBindings"), Value::Array(vec![binding]))),
+            _ => panic!("pure bindings"),
+        }
+        let Value::Array(order) = field_mut(target_intent, "executionOrder") else {
+            panic!("order")
+        };
+        order.push(text("replaceRange.binding.0"));
+        *field_mut(target_intent, "result") = reference(&saved);
+        *field_mut(&mut projection, "expression") = map([
+            ("kind", text("source")),
+            (
+                "source",
+                map([
+                    ("kind", text("pureBinding")),
+                    ("bindingId", text("replaceRange.binding.0")),
+                ]),
+            ),
+            ("path", Value::Array(vec![])),
+        ]);
     }
-    let Value::Array(order) = field_mut(target_intent, "executionOrder") else {
-        panic!("order")
-    };
-    order.push(text("replaceRange.binding.0"));
-    *field_mut(target_intent, "result") = reference(&saved);
-    *field_mut(&mut projection, "expression") = map([
-        ("kind", text("source")),
-        (
-            "source",
-            map([
-                ("kind", text("pureBinding")),
-                ("bindingId", text("replaceRange.binding.0")),
-            ]),
-        ),
-        ("path", Value::Array(vec![])),
-    ]);
     // This synthetic fixture explicitly increases its declared step ceiling.
     // At FactBytes.max=1 MiB, read work plus the required byte equality already
     // exceeds the legacy 1 MiB step ceiling. Allocation stays at its old 16 MiB.
@@ -585,6 +592,8 @@ fn verifier_source_function_names_cannot_shadow_imported_read_effects() {
 #[path = "imported_calls.rs"]
 mod imported_calls;
 
+#[path = "source_functions/count.rs"]
+mod count;
 #[path = "source_functions/utf8.rs"]
 mod utf8;
 
diff --git a/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions/count.rs b/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions/count.rs
new file mode 100644
index 00000000..7b42c4f6
--- /dev/null
+++ b/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions/count.rs
@@ -0,0 +1,157 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+//! Independently rebound read guards that count bytes, not public compiler artifacts.
+use super::*;
+fn integer(value: u64) -> Value {
+    map([
+        ("kind", text("const")),
+        (
+            "value",
+            map([
+                ("kind", text("int")),
+                ("width", text("U64")),
+                ("value", Value::Integer(i128::from(value))),
+            ]),
+        ),
+    ])
+}
+fn needle(value: &[u8]) -> Value {
+    map([
+        ("kind", text("const")),
+        (
+            "value",
+            map([
+                ("kind", text("bytes")),
+                ("value", Value::Bytes(value.to_vec())),
+            ]),
+        ),
+    ])
+}
+fn guarded(old: Value, case: &str) -> Value {
+    let operand = field(&old, "left").clone();
+    let counted = match case {
+        "two-byte-needle" => needle(b"\r\n"),
+        "empty-needle" => needle(b""),
+        "integer-needle" => integer(10),
+        _ => needle(b"\n"),
+    };
+    let mut scan = map([
+        ("kind", text("call")),
+        ("callee", text("core.bytes.count")),
+        (
+            "typeArgs",
+            Value::Array(vec![text("jedit.text@1.FactBytes")]),
+        ),
+        ("args", Value::Array(vec![operand, counted])),
+    ]);
+    if case == "wide-type" {
+        *field_mut(&mut scan, "typeArgs") = Value::Array(vec![text("Bytes<max=2097152>")]);
+    }
+    let compare = map([
+        ("kind", text("compare")),
+        ("op", text("<=")),
+        ("left", scan),
+        ("right", integer(u64::MAX)),
+    ]);
+    map([
+        ("kind", text("all")),
+        ("values", Value::Array(vec![old, compare])),
+    ])
+}
+fn edit_core(core: &mut Value, case: &str) {
+    let Value::Array(nodes) = field_mut(field_mut(intent(core), "body"), "nodes") else {
+        panic!("nodes")
+    };
+    let old = field(&nodes[1], "predicate").clone();
+    *field_mut(&mut nodes[1], "predicate") = guarded(old, case);
+}
+fn edit_target(intent: &mut Value, case: &str) {
+    let Value::Array(requirements) = field_mut(intent, "requirements") else {
+        panic!("requirements")
+    };
+    let old = field(&requirements[0], "predicate").clone();
+    *field_mut(&mut requirements[0], "predicate") = guarded(old, case);
+}
+fn source(case: &str, budget: u64) -> LoweringRequestV1 {
+    source_with(case, budget, true)
+}
+fn source_with(case: &str, budget: u64, helper: bool) -> LoweringRequestV1 {
+    let mut source = read_with_budget(budget, helper);
+    let mut core = decode(&source.core.artifact.bytes).expect("canonical rebound artifact");
+    let mut target = decode(&source.semantic_inputs[5].artifact.artifact.bytes)
+        .expect("canonical rebound artifact");
+    edit_core(&mut core, case);
+    edit_target(intent(&mut target), case);
+    source.core = bound(
+        "jedit.text.replace_range@1",
+        "edict.core.module/v1",
+        encode(&core).expect("canonical rebound artifact"),
+    );
+    *field_mut(field_mut(&mut target, "semanticClosure"), "sourceCore") = map([
+        ("id", text("jedit.text.replace_range@1")),
+        (
+            "digest",
+            Value::Array(vec![
+                text("sha256"),
+                Value::Bytes(source.core.reference.digest.bytes.clone()),
+            ]),
+        ),
+    ]);
+    source.semantic_inputs[5].artifact = bound(
+        "echo.span-ir/v2",
+        "edict.target-ir.artifact/v1",
+        encode(&target).expect("canonical rebound artifact"),
+    );
+    source
+}
+fn verification(case: &str, budget: u64) -> verifier::VerificationRequestV1 {
+    verification_with(case, budget, true)
+}
+fn verification_with(case: &str, budget: u64, helper: bool) -> verifier::VerificationRequestV1 {
+    // The new guard is never submitted to the lowerer to obtain this carrier.
+    let mut request = request(read_with_budget(budget, helper));
+    changed_core(&mut request, |core| edit_core(core, case));
+    changed_target(&mut request, |intent| edit_target(intent, case));
+    request
+}
+#[test]
+fn bounded_read_count_guards_lower_after_a_real_read() {
+    lower(source("valid", 4_194_304)).expect("count read guard lowers");
+}
+#[test]
+fn bounded_read_count_guards_verify_independently() {
+    let response =
+        verifier::verify(verification("valid", 4_194_304)).expect("independent verifier response");
+    let report = decode(&response.outputs[0].artifact.bytes).expect("canonical rebound artifact");
+    assert_eq!(field(&report, "outcome"), &text("accepted"));
+}
+#[test]
+fn bounded_read_count_rejects_needle_type_and_step_budget_forgeries() {
+    for case in [
+        "wide-type",
+        "two-byte-needle",
+        "empty-needle",
+        "integer-needle",
+    ] {
+        assert!(lower(source(case, 4_194_304)).is_err(), "{case}");
+        assert_rejected(verification(case, 4_194_304));
+    }
+    lower(read_helper_with_budget(2_500_000))
+        .expect("without scan, baseline fits this exact same step ceiling");
+    assert!(lower(source("valid", 2_500_000)).is_err());
+    assert_rejected(verification("valid", 2_500_000));
+}
+#[test]
+fn a_count_guard_is_charged_even_without_a_function_table() {
+    // With no source functions and no addition, the count's full-byte scan is
+    // still the only judgment that charges it against the step ceiling.
+    lower(read_with_budget(2_500_000, false))
+        .expect("without scan, the plain read fits this step ceiling");
+    lower(source_with("valid", 4_194_304, false)).expect("a fitting count guard lowers");
+    let response = verifier::verify(verification_with("valid", 4_194_304, false))
+        .expect("independent verifier response");
+    let report = decode(&response.outputs[0].artifact.bytes).expect("canonical report");
+    assert_eq!(field(&report, "outcome"), &text("accepted"));
+    assert!(lower(source_with("valid", 2_500_000, false)).is_err());
+    assert_rejected(verification_with("valid", 2_500_000, false));
+}
diff --git a/crates/echo-edict-provider-verifier/tests/source_functions/count.rs b/crates/echo-edict-provider-verifier/tests/source_functions/count.rs
new file mode 100644
index 00000000..4b39dc9c
--- /dev/null
+++ b/crates/echo-edict-provider-verifier/tests/source_functions/count.rs
@@ -0,0 +1,173 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+//! Native provider judgments over rebound single-byte counts, not compiler proof.
+use super::*;
+fn bytes(value: &[u8]) -> CanonicalValueV1 {
+    map([
+        ("kind", text("const")),
+        (
+            "value",
+            map([
+                ("kind", text("bytes")),
+                ("value", CanonicalValueV1::Bytes(value.to_vec())),
+            ]),
+        ),
+    ])
+}
+fn typed(name: &str, types: &[&str], args: Vec<CanonicalValueV1>) -> CanonicalValueV1 {
+    let mut value = call(name, args);
+    *map_field_mut(&mut value, "typeArgs") = list(types.iter().map(|ty| text(*ty)).collect());
+    value
+}
+fn add(left: CanonicalValueV1, addend: u64) -> CanonicalValueV1 {
+    typed(
+        "core.integer.add",
+        &["U64"],
+        vec![left, literal("U64", i128::from(addend))],
+    )
+}
+fn count_fixture(case: &str, addend: u64) -> (FixtureNames<'static>, RawFixture, Vec<u8>) {
+    called_fixture(|core, _| {
+        let coordinate = text_field(core, "coordinate")
+            .expect("coordinate")
+            .to_owned();
+        // A named operand type must give the same structural maximum.
+        let named = format!("{coordinate}.Blob");
+        let operand = if case.starts_with("named") {
+            add_field(
+                map_field_mut(core, "types"),
+                "Blob",
+                map([
+                    ("kind", text("Bytes")),
+                    ("max", CanonicalValueV1::Integer(32)),
+                ]),
+            );
+            named.as_str()
+        } else {
+            "Bytes<max=32>"
+        };
+        let parameter = local("arg.0", operand);
+        let mut types = vec![operand];
+        let mut args = vec![reference(&parameter), bytes(b"\n")];
+        match case {
+            "empty-needle" => args[1] = bytes(b""),
+            "two-byte-needle" => args[1] = bytes(b"\r\n"),
+            "integer-needle" => args[1] = literal("U64", 10),
+            "local-needle" => args[1] = reference(&parameter),
+            "missing-needle" => args.truncate(1),
+            "extra-needle" => args.push(bytes(b"\n")),
+            "missing-type" => types.clear(),
+            "wrong-type" => types = vec!["U64"],
+            "wide-type" => types = vec!["Bytes<max=64>"],
+            _ => {}
+        }
+        let scan = typed("core.bytes.count", &types, args);
+        let breaks = local("local.0", "U64");
+        let mut functions = Vec::new();
+        let lines = match case {
+            "let" | "named-let" => function(
+                vec![parameter],
+                "U64",
+                vec![breaks.clone()],
+                vec![map([
+                    ("kind", text("let")),
+                    ("binding", breaks.clone()),
+                    ("value", scan),
+                ])],
+                add(reference(&breaks), addend),
+            ),
+            // The binding's own value is an addition, so its cap is the one
+            // the addition proof already established: 32 + 1.
+            "sum-let" => function(
+                vec![parameter],
+                "U64",
+                vec![breaks.clone()],
+                vec![map([
+                    ("kind", text("let")),
+                    ("binding", breaks.clone()),
+                    ("value", add(scan, 1)),
+                ])],
+                add(reference(&breaks), addend),
+            ),
+            "helper-result" => {
+                functions.push((
+                    "countBreaks",
+                    function(vec![parameter.clone()], "U64", vec![], vec![], scan),
+                ));
+                function(
+                    vec![parameter.clone()],
+                    "U64",
+                    vec![],
+                    vec![],
+                    add(
+                        call(
+                            &format!("{coordinate}.countBreaks"),
+                            vec![reference(&parameter)],
+                        ),
+                        addend,
+                    ),
+                )
+            }
+            "wrong-result" => function(vec![parameter], "Bool", vec![], vec![], scan),
+            _ => function(vec![parameter], "U64", vec![], vec![], add(scan, addend)),
+        };
+        functions.push(("lines", lines));
+        for (name, definition) in functions {
+            add_field(map_field_mut(core, "functions"), name, definition);
+        }
+    })
+}
+#[test]
+fn source_function_counts_prove_line_count_directly_and_through_let_bindings() {
+    for case in ["direct", "let", "named", "named-let"] {
+        for addend in [1, u64::MAX - 32] {
+            let (names, fixture, package) = count_fixture(case, addend);
+            let lowered = lowerer::lower(lowering_request(names, &fixture))
+                .unwrap_or_else(|_| panic!("{case} + {addend} lowers"));
+            assert_eq!(lowered.outputs[0].artifact.bytes, package);
+            assert!(
+                verifier_accepts(names, &fixture, package),
+                "{case} + {addend}: verifier refused the independently proven count"
+            );
+        }
+    }
+}
+#[test]
+fn source_function_count_sums_that_overflow_at_the_operand_maximum_refuse() {
+    for case in ["direct", "let", "named", "named-let"] {
+        let (names, fixture, package) = count_fixture(case, u64::MAX - 31);
+        both_refuse(names, &fixture, package, case);
+    }
+}
+#[test]
+fn source_function_count_bounds_do_not_cross_helper_results() {
+    let (names, fixture, package) = count_fixture("helper-result", 1);
+    both_refuse(names, &fixture, package, "helper-result");
+}
+#[test]
+fn source_function_count_rejects_needle_signature_and_result_forgeries() {
+    for case in [
+        "empty-needle",
+        "two-byte-needle",
+        "integer-needle",
+        "local-needle",
+        "missing-needle",
+        "extra-needle",
+        "missing-type",
+        "wrong-type",
+        "wide-type",
+        "wrong-result",
+    ] {
+        let (names, fixture, package) = count_fixture(case, 1);
+        both_refuse(names, &fixture, package, case);
+    }
+}
+#[test]
+fn a_bound_addition_carries_its_proven_cap_to_later_sums() {
+    let (names, fixture, package) = count_fixture("sum-let", u64::MAX - 33);
+    let lowered = lowerer::lower(lowering_request(names, &fixture)).expect("sum-let lowers");
+    assert_eq!(lowered.outputs[0].artifact.bytes, package);
+    assert!(verifier_accepts(names, &fixture, package));
+    let (names, fixture, package) = count_fixture("sum-let", u64::MAX - 32);
+    both_refuse(names, &fixture, package, "sum-let one past the carried cap");
+}
diff --git a/crates/echo-edict-provider-verifier/tests/source_functions/mod.rs b/crates/echo-edict-provider-verifier/tests/source_functions/mod.rs
index 286e7064..d093baa9 100644
--- a/crates/echo-edict-provider-verifier/tests/source_functions/mod.rs
+++ b/crates/echo-edict-provider-verifier/tests/source_functions/mod.rs
@@ -756,4 +756,5 @@ fn source_functions_pure_basis_has_complete_input_only_call_authority() {
 
 mod nominal_types;
 
+mod count;
 mod utf8;
diff --git a/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm b/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm
index 424970f6..fb26b41a 100644
Binary files a/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm and b/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm differ
diff --git a/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm b/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm
index 9a766125..d8a88bd2 100644
Binary files a/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm and b/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm differ
diff --git a/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/provider-manifest.echo.json b/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/provider-manifest.echo.json
index 72f2301b..c6e6dd4a 100644
--- a/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/provider-manifest.echo.json
+++ b/crates/echo-wesley-gen/assets/v1/edict-provider/package/v1/provider-manifest.echo.json
@@ -3,7 +3,7 @@
   "providerAbi": "edict:target-provider@1.0.0",
   "provider": {
     "coordinate": "echo.edict-provider@1",
-    "digest": "sha256:36ce20c612c8c46bbe450c93e6fb2235f38e4ec2b14f04f128eee91805cdb26a"
+    "digest": "sha256:8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8"
   },
   "artifacts": [
     {
@@ -87,13 +87,13 @@
       "artifactKind": "lowerer",
       "resource": {
         "coordinate": "echo.dpo.lowerer/component@1",
-        "digest": "sha256:cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c"
+        "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587"
       },
       "source": {
         "kind": "component",
         "component": {
           "coordinate": "echo.dpo.lowerer/component@1",
-          "digest": "sha256:cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c"
+          "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587"
         }
       }
     },
@@ -178,13 +178,13 @@
       "artifactKind": "verifier",
       "resource": {
         "coordinate": "echo.dpo.verifier/component@1",
-        "digest": "sha256:3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11"
+        "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e"
       },
       "source": {
         "kind": "component",
         "component": {
           "coordinate": "echo.dpo.verifier/component@1",
-          "digest": "sha256:3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11"
+          "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e"
         }
       }
     }
diff --git a/crates/echo-wesley-gen/tests/provider_package.rs b/crates/echo-wesley-gen/tests/provider_package.rs
index c49b25d4..07fdfc7e 100644
--- a/crates/echo-wesley-gen/tests/provider_package.rs
+++ b/crates/echo-wesley-gen/tests/provider_package.rs
@@ -65,7 +65,7 @@ const SEMANTIC_DIGEST: &str =
 const RELEASE_DIGEST: &str =
     "sha256:c39449495281b51f978468d08c21e93bcfa423176063b41675da61e4674b0066";
 const PACKAGE_ARTIFACT_SHA256: &str =
-    "36ce20c612c8c46bbe450c93e6fb2235f38e4ec2b14f04f128eee91805cdb26a";
+    "8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8";
 const OTHER_PACKAGE_ARTIFACT_SHA256: &str =
     "eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee";
 
diff --git a/crates/echo-wesley-gen/tests/provider_package_corpus.rs b/crates/echo-wesley-gen/tests/provider_package_corpus.rs
index a91abf8c..8a2e8fa1 100644
--- a/crates/echo-wesley-gen/tests/provider_package_corpus.rs
+++ b/crates/echo-wesley-gen/tests/provider_package_corpus.rs
@@ -11,9 +11,9 @@ use std::sync::atomic::{AtomicU64, Ordering};
 use sha2::{Digest as _, Sha256};
 
 const EXPECTED_PROVIDER_DIGEST: &str =
-    "sha256:36ce20c612c8c46bbe450c93e6fb2235f38e4ec2b14f04f128eee91805cdb26a";
+    "sha256:8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8";
 const EXPECTED_MANIFEST_RAW_SHA256: &str =
-    "8bb6c675598fc457513a953c2aee65316f80315583df418a5ef96788321cd649";
+    "704b673fbf0186a7ffd3313d89930fa4a72b47a05bade0e93c3419297098cbe7";
 
 const PACKAGE_PATHS: [&str; 25] = [
     "components/lowerer.echo-dpo.component.wasm",
diff --git a/crates/warp-core/src/coordinator.rs b/crates/warp-core/src/coordinator.rs
index 3a38d02b..932e3bcb 100644
--- a/crates/warp-core/src/coordinator.rs
+++ b/crates/warp-core/src/coordinator.rs
@@ -2254,7 +2254,10 @@ impl WorldlineRuntime {
     /// Results are ordered by deterministic ticketed-ingress identity. A commit
     /// can admit more than one correlated submission, so this lookup is
     /// intentionally one-to-many.
-    #[cfg(any(test, feature = "trusted_runtime"))]
+    #[cfg(any(
+        test,
+        all(feature = "native_rule_bootstrap", feature = "trusted_runtime")
+    ))]
     pub(crate) fn receipt_correlations_for_current_basis(
         &self,
         worldline_id: WorldlineId,
diff --git a/crates/warp-core/src/edict_pure.rs b/crates/warp-core/src/edict_pure.rs
index d8f0fbfc..8b592752 100644
--- a/crates/warp-core/src/edict_pure.rs
+++ b/crates/warp-core/src/edict_pure.rs
@@ -97,5 +97,7 @@ pub fn evaluate(
 #[cfg(test)]
 mod predicate_tests;
 
+#[cfg(test)]
+mod byte_count_tests;
 #[cfg(test)]
 mod byte_utf8_tests;
diff --git a/crates/warp-core/src/edict_pure/byte_count_tests.rs b/crates/warp-core/src/edict_pure/byte_count_tests.rs
new file mode 100644
index 00000000..d9b24c17
--- /dev/null
+++ b/crates/warp-core/src/edict_pure/byte_count_tests.rs
@@ -0,0 +1,268 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+//! Raw single-byte counting, its structural needle and its helper-frame bound.
+use super::{
+    evaluate::{expression, Meter},
+    functions::{check_roots, decode},
+    model::MAX_PROGRAM_NODES,
+    syntax::Parser,
+    EvaluationError as Error, EvaluationLimits,
+};
+use echo_edict_canonical::CanonicalValueV1 as Value;
+use std::collections::BTreeMap;
+
+fn map(fields: impl IntoIterator<Item = (&'static str, Value)>) -> Value {
+    Value::Map(
+        fields
+            .into_iter()
+            .map(|(k, v)| (Value::Text(k.into()), v))
+            .collect(),
+    )
+}
+fn text(value: &str) -> Value {
+    Value::Text(value.into())
+}
+fn bytes(value: &[u8]) -> Value {
+    map([
+        ("kind", text("const")),
+        (
+            "value",
+            map([
+                ("kind", text("bytes")),
+                ("value", Value::Bytes(value.to_vec())),
+            ]),
+        ),
+    ])
+}
+fn integer(value: u64) -> Value {
+    map([
+        ("kind", text("const")),
+        (
+            "value",
+            map([
+                ("kind", text("int")),
+                ("width", text("U64")),
+                ("value", Value::Integer(i128::from(value))),
+            ]),
+        ),
+    ])
+}
+fn local(id: &str, ty: &str) -> Value {
+    map([
+        ("id", text(id)),
+        ("alphaName", text(id)),
+        ("type", text(ty)),
+    ])
+}
+fn reference(local: &Value) -> Value {
+    map([("kind", text("local")), ("ref", local.clone())])
+}
+fn call(callee: &str, types: &[&str], args: Vec<Value>) -> Value {
+    map([
+        ("kind", text("call")),
+        ("callee", text(callee)),
+        (
+            "typeArgs",
+            Value::Array(types.iter().map(|ty| text(ty)).collect()),
+        ),
+        ("args", Value::Array(args)),
+    ])
+}
+fn count(operand: Value) -> Value {
+    call(
+        "core.bytes.count",
+        &["Bytes<max=32>"],
+        vec![operand, bytes(b"\n")],
+    )
+}
+fn add(left: Value, right: Value) -> Value {
+    call("core.integer.add", &["U64"], vec![left, right])
+}
+fn limits(steps: u64, allocated: u64) -> EvaluationLimits {
+    EvaluationLimits {
+        max_package_bytes: 1024,
+        max_input_bytes: 1024,
+        max_output_bytes: 1024,
+        max_steps: steps,
+        max_allocated_bytes: allocated,
+    }
+}
+fn parsed(wire: &Value) -> Result<super::model::Expr, Error> {
+    let types = Value::Map(vec![]);
+    let mut parser = Parser {
+        types: &types,
+        coordinate: "count.example@1",
+        remaining: MAX_PROGRAM_NODES,
+    };
+    parser.expr(wire, 0)
+}
+fn usage(operand: &[u8], needle: u8) -> Result<(Value, (u64, u64)), Error> {
+    let wire = call(
+        "core.bytes.count",
+        &["Bytes<max=32>"],
+        vec![bytes(operand), bytes(&[needle])],
+    );
+    let expr = parsed(&wire)?;
+    check_roots(&BTreeMap::new(), [&expr], [])?;
+    let mut meter = Meter::new(limits(1024, 4096));
+    let value = expression(&expr, &BTreeMap::new(), &BTreeMap::new(), &mut meter, 0)?;
+    Ok((value, meter.usage()))
+}
+
+#[test]
+fn count_is_raw_byte_counting_with_one_complete_scan() -> Result<(), Error> {
+    let (_, (base_steps, base_allocated)) = usage(b"", b'\n')?;
+    for (operand, needle, want) in [
+        (&b""[..], b'\n', 0),
+        (&b"abc"[..], b'\n', 0),
+        (&b"\n\n\n"[..], b'\n', 3),
+        (&b"a\nb\r\nc"[..], b'\n', 2),
+        (&b"\r"[..], b'\n', 0),
+        (&b"\0a\0"[..], 0, 2),
+        (&[0xff, 0x00, 0xff, 0xff][..], 0xff, 3),
+        (&[0x80, b'\n', 0xc0, 0x80][..], 0x80, 2),
+    ] {
+        let (value, (steps, allocated)) = usage(operand, needle)?;
+        assert_eq!(value, Value::Integer(want), "{operand:?} counting {needle}");
+        let length = operand.len() as u64;
+        assert_eq!(steps, base_steps + length, "one complete scan");
+        assert_eq!(allocated, base_allocated + length);
+        let wire = call(
+            "core.bytes.count",
+            &["Bytes<max=32>"],
+            vec![bytes(operand), bytes(&[needle])],
+        );
+        let expr = parsed(&wire)?;
+        assert_eq!(
+            expression(
+                &expr,
+                &BTreeMap::new(),
+                &BTreeMap::new(),
+                &mut Meter::new(limits(steps - 1, allocated)),
+                0
+            ),
+            Err(Error::StepBudgetExceeded)
+        );
+    }
+    Ok(())
+}
+
+#[test]
+fn count_parser_requires_one_structural_byte_needle_and_exact_signature() {
+    let operand = bytes(b"a\nb");
+    for (types, args) in [
+        (vec!["Bytes<max=32>"], vec![operand.clone(), bytes(b"")]),
+        (vec!["Bytes<max=32>"], vec![operand.clone(), bytes(b"\r\n")]),
+        (vec!["Bytes<max=32>"], vec![operand.clone(), integer(10)]),
+        (
+            vec!["Bytes<max=32>"],
+            vec![
+                operand.clone(),
+                reference(&local("arg.0", "Bytes<exact=1>")),
+            ],
+        ),
+        (vec!["Bytes<max=32>"], vec![operand.clone()]),
+        (
+            vec!["Bytes<max=32>"],
+            vec![operand.clone(), bytes(b"\n"), bytes(b"\n")],
+        ),
+        (vec![], vec![operand.clone(), bytes(b"\n")]),
+        (vec!["U64"], vec![operand.clone(), bytes(b"\n")]),
+        (
+            vec!["Bytes<max=32>", "Bytes<max=32>"],
+            vec![operand, bytes(b"\n")],
+        ),
+    ] {
+        let wire = call("core.bytes.count", &types, args.clone());
+        assert!(parsed(&wire).is_err(), "{types:?} {args:?}");
+    }
+}
+
+fn helpers(functions: Vec<(&'static str, Value)>) -> Result<(), Error> {
+    let core = map([
+        ("functions", map(functions)),
+        ("intents", Value::Map(vec![])),
+        ("types", Value::Map(vec![])),
+    ]);
+    let exports = map([
+        ("pureFunctions", Value::Array(vec![])),
+        ("effects", Value::Array(vec![])),
+    ]);
+    let types = Value::Map(vec![]);
+    let mut parser = Parser {
+        types: &types,
+        coordinate: "count.example@1",
+        remaining: MAX_PROGRAM_NODES,
+    };
+    decode(&core, &exports, &mut parser).map(|_| ())
+}
+fn function(bindings: Vec<(Value, Value)>, result: Value) -> Value {
+    let locals = bindings.iter().map(|(local, _)| local.clone()).collect();
+    map([
+        (
+            "params",
+            Value::Array(vec![local("arg.0", "Bytes<max=32>")]),
+        ),
+        ("returnType", text("U64")),
+        (
+            "body",
+            map([
+                ("locals", Value::Array(locals)),
+                (
+                    "bindings",
+                    Value::Array(
+                        bindings
+                            .into_iter()
+                            .map(|(binding, value)| {
+                                map([
+                                    ("kind", text("let")),
+                                    ("binding", binding),
+                                    ("value", value),
+                                ])
+                            })
+                            .collect(),
+                    ),
+                ),
+                ("result", result),
+            ]),
+        ),
+    ])
+}
+
+#[test]
+fn helper_addition_uses_the_count_bound_directly_and_through_let_bindings() {
+    let text_bytes = reference(&local("arg.0", "Bytes<max=32>"));
+    let breaks = local("local.0", "U64");
+    for (addend, accepted) in [(1, true), (u64::MAX - 32, true), (u64::MAX - 31, false)] {
+        let direct = function(vec![], add(count(text_bytes.clone()), integer(addend)));
+        let bound = function(
+            vec![(breaks.clone(), count(text_bytes.clone()))],
+            add(reference(&breaks), integer(addend)),
+        );
+        for (shape, helper) in [("direct", direct), ("let", bound)] {
+            assert_eq!(
+                helpers(vec![("lines", helper)]).is_ok(),
+                accepted,
+                "{shape} + {addend}"
+            );
+        }
+    }
+}
+
+#[test]
+fn helper_results_do_not_carry_the_count_bound() {
+    let text_bytes = reference(&local("arg.0", "Bytes<max=32>"));
+    let breaks = function(vec![], count(text_bytes.clone()));
+    let lines = function(
+        vec![],
+        add(
+            call("count.example@1.breaks", &[], vec![text_bytes]),
+            integer(1),
+        ),
+    );
+    assert_eq!(
+        helpers(vec![("breaks", breaks.clone()), ("lines", lines)]),
+        Err(Error::UnsupportedProgram)
+    );
+    assert_eq!(helpers(vec![("breaks", breaks)]), Ok(()));
+}
diff --git a/crates/warp-core/src/edict_pure/evaluate.rs b/crates/warp-core/src/edict_pure/evaluate.rs
index c139b44e..4f09a6a9 100644
--- a/crates/warp-core/src/edict_pure/evaluate.rs
+++ b/crates/warp-core/src/edict_pure/evaluate.rs
@@ -263,6 +263,33 @@ pub(crate) fn expression(
             meter.charge_steps(length)?;
             meter.copy(&Value::Bool(std::str::from_utf8(&bytes).is_ok()))
         }
+        Expr::ByteCount {
+            min,
+            max,
+            value,
+            needle,
+        } => {
+            let value = expression(value, locals, helpers, meter, depth + 1)?;
+            validate(
+                &value,
+                &RuntimeType::Bytes {
+                    min: *min,
+                    max: *max,
+                },
+                meter,
+                depth + 1,
+            )?;
+            let Value::Bytes(bytes) = value else {
+                return Err(Error::InvalidArtifact);
+            };
+            let length = u64::try_from(bytes.len()).map_err(|_| Error::StepBudgetExceeded)?;
+            meter.charge_steps(length)?;
+            // Never exceeds the already-charged byte length.
+            let count = bytes
+                .iter()
+                .fold(0_u64, |count, byte| count + u64::from(byte == needle));
+            meter.copy(&Value::Integer(i128::from(count)))
+        }
         Expr::ByteLength { min, max, value } => {
             let value = expression(value, locals, helpers, meter, depth + 1)?;
             validate(
diff --git a/crates/warp-core/src/edict_pure/functions.rs b/crates/warp-core/src/edict_pure/functions.rs
index 29278497..bdc6f8ef 100644
--- a/crates/warp-core/src/edict_pure/functions.rs
+++ b/crates/warp-core/src/edict_pure/functions.rs
@@ -108,6 +108,7 @@ pub(crate) fn decode(
         parser.enter(0)?;
         exact_fields(definition.body, &["locals", "bindings", "result"])?;
         let mut scope = BTreeMap::new();
+        let mut caps = Caps::new();
         let mut params = Vec::new();
         for parameter in definition.params {
             local(parameter)?;
@@ -141,6 +142,7 @@ pub(crate) fn decode(
             let actual = infer(
                 value,
                 &scope,
+                &caps,
                 &definitions,
                 definition.source_owned,
                 parser,
@@ -150,6 +152,12 @@ pub(crate) fn decode(
             if !accepts(&ty, &actual) {
                 return Err(Error::InvalidArtifact);
             }
+            if let RuntimeType::Unsigned(max) = ty {
+                let cap = unsigned_ceiling(value, max, &caps, parser, 0)?;
+                if cap < max {
+                    caps.insert(id, cap);
+                }
+            }
             bindings.push(Binding {
                 id: id.to_owned(),
                 ty,
@@ -164,6 +172,7 @@ pub(crate) fn decode(
         let actual = infer(
             result,
             &scope,
+            &caps,
             &definitions,
             definition.source_owned,
             parser,
@@ -199,9 +208,10 @@ pub(crate) fn decode(
                 .ok_or(Error::InvalidArtifact)?;
             local(input)?;
             let scope = BTreeMap::from([("arg.0", input)]);
+            let caps = Caps::new();
             // A pure basis is retained authority, not executed work. Admit its
             // input-only scope, calls and combined depth without spending Meter.
-            infer(basis, &scope, &definitions, true, parser, 0)?;
+            infer(basis, &scope, &caps, &definitions, true, parser, 0)?;
             basis_roots.push(parser.expr(basis, 0)?);
         }
     }
@@ -252,9 +262,14 @@ fn join(left: RuntimeType, right: RuntimeType) -> Result<RuntimeType, Error> {
 }
 
 type Scope<'a> = BTreeMap<&'a str, &'a Value>;
+/// Proven upper bounds of earlier unsigned bindings in the same helper body.
+/// Local identities are unique and immutable, so a cap names exactly the
+/// bound value. Bounds never cross helper results or record fields.
+type Caps<'a> = BTreeMap<&'a str, u64>;
 fn infer(
     value: &Value,
     scope: &Scope<'_>,
+    caps: &Caps<'_>,
     definitions: &BTreeMap<String, Definition<'_>>,
     source: bool,
     parser: &mut Parser<'_>,
@@ -294,6 +309,7 @@ fn infer(
             let RuntimeType::Record(fields) = infer(
                 field(value, "base")?,
                 scope,
+                caps,
                 definitions,
                 source,
                 parser,
@@ -316,7 +332,15 @@ fn infer(
                 .map(|(name, expression)| {
                     Ok((
                         text(name)?.to_owned(),
-                        infer(expression, scope, definitions, source, parser, depth + 1)?,
+                        infer(
+                            expression,
+                            scope,
+                            caps,
+                            definitions,
+                            source,
+                            parser,
+                            depth + 1,
+                        )?,
                     ))
                 })
                 .collect::<Result<Vec<_>, Error>>()?;
@@ -327,6 +351,7 @@ fn infer(
             check_predicate(
                 field(value, "predicate")?,
                 scope,
+                caps,
                 definitions,
                 source,
                 parser,
@@ -335,6 +360,7 @@ fn infer(
             let left = infer(
                 field(value, "then")?,
                 scope,
+                caps,
                 definitions,
                 source,
                 parser,
@@ -343,6 +369,7 @@ fn infer(
             let right = infer(
                 field(value, "else")?,
                 scope,
+                caps,
                 definitions,
                 source,
                 parser,
@@ -363,7 +390,15 @@ fn infer(
                     return Err(Error::InvalidArtifact);
                 }
                 for (argument, parameter) in arguments.iter().zip(callee.params) {
-                    let actual = infer(argument, scope, definitions, source, parser, depth + 1)?;
+                    let actual = infer(
+                        argument,
+                        scope,
+                        caps,
+                        definitions,
+                        source,
+                        parser,
+                        depth + 1,
+                    )?;
                     let expected = parser.ty(text_field(parameter, "type")?, 0)?;
                     if !accepts(&expected, &actual) {
                         return Err(Error::InvalidArtifact);
@@ -371,9 +406,31 @@ fn infer(
                 }
                 return parser.ty(callee.result_type, 0);
             }
+            if name == "core.bytes.count" {
+                let ([operand, needle], [coordinate]) = (arguments, types) else {
+                    return Err(Error::UnsupportedProgram);
+                };
+                super::syntax::count_needle(needle)?;
+                let actual = infer(operand, scope, caps, definitions, source, parser, depth + 1)?;
+                let expected = parser.ty(text(coordinate)?, depth + 1)?;
+                if !matches!(expected, RuntimeType::Bytes { .. }) || expected != actual {
+                    return Err(Error::UnsupportedProgram);
+                }
+                return Ok(RuntimeType::Unsigned(u64::MAX));
+            }
             let actual = arguments
                 .iter()
-                .map(|argument| infer(argument, scope, definitions, source, parser, depth + 1))
+                .map(|argument| {
+                    infer(
+                        argument,
+                        scope,
+                        caps,
+                        definitions,
+                        source,
+                        parser,
+                        depth + 1,
+                    )
+                })
                 .collect::<Result<Vec<_>, _>>()?;
             let declared = types
                 .iter()
@@ -407,8 +464,8 @@ fn infer(
                 ("core.integer.add", [left, right], [expected @ RuntimeType::Unsigned(max)])
                     if left == expected && right == expected =>
                 {
-                    let left = unsigned_ceiling(&arguments[0], *max, parser, depth + 1)?;
-                    let right = unsigned_ceiling(&arguments[1], *max, parser, depth + 1)?;
+                    let left = unsigned_ceiling(&arguments[0], *max, caps, parser, depth + 1)?;
+                    let right = unsigned_ceiling(&arguments[1], *max, caps, parser, depth + 1)?;
                     if left.checked_add(right).is_none_or(|sum| sum > *max) {
                         return Err(Error::UnsupportedProgram);
                     }
@@ -453,10 +510,25 @@ fn infer(
 fn unsigned_ceiling(
     value: &Value,
     max: u64,
+    caps: &Caps<'_>,
     parser: &mut Parser<'_>,
     depth: usize,
 ) -> Result<u64, Error> {
     parser.enter(depth)?;
+    if text_field(value, "kind")? == "local" {
+        let id = text_field(field(value, "ref")?, "id")?;
+        return Ok(caps.get(id).map_or(max, |cap| (*cap).min(max)));
+    }
+    if text_field(value, "kind")? == "call" && text_field(value, "callee")? == "core.bytes.count" {
+        // A count never exceeds its operand's byte maximum.
+        let [coordinate] = array(field(value, "typeArgs")?)? else {
+            return Err(Error::InvalidArtifact);
+        };
+        let RuntimeType::Bytes { max: bytes, .. } = parser.ty(text(coordinate)?, depth + 1)? else {
+            return Err(Error::InvalidArtifact);
+        };
+        return Ok(bytes.min(max));
+    }
     if text_field(value, "kind")? == "const" {
         return unsigned_literal(value);
     }
@@ -464,8 +536,8 @@ fn unsigned_ceiling(
         let [left, right] = array(field(value, "args")?)? else {
             return Err(Error::InvalidArtifact);
         };
-        return unsigned_ceiling(left, max, parser, depth + 1)?
-            .checked_add(unsigned_ceiling(right, max, parser, depth + 1)?)
+        return unsigned_ceiling(left, max, caps, parser, depth + 1)?
+            .checked_add(unsigned_ceiling(right, max, caps, parser, depth + 1)?)
             .ok_or(Error::UnsupportedProgram);
     }
     Ok(max)
@@ -480,6 +552,7 @@ fn unsigned_literal(value: &Value) -> Result<u64, Error> {
 fn check_predicate(
     value: &Value,
     scope: &Scope<'_>,
+    caps: &Caps<'_>,
     definitions: &BTreeMap<String, Definition<'_>>,
     source: bool,
     parser: &mut Parser<'_>,
@@ -494,7 +567,7 @@ fn check_predicate(
                 return Err(Error::InvalidArtifact);
             }
             for value in values {
-                check_predicate(value, scope, definitions, source, parser, depth + 1)?;
+                check_predicate(value, scope, caps, definitions, source, parser, depth + 1)?;
             }
             return Ok(());
         }
@@ -503,6 +576,7 @@ fn check_predicate(
             return check_predicate(
                 field(value, "value")?,
                 scope,
+                caps,
                 definitions,
                 source,
                 parser,
@@ -516,6 +590,7 @@ fn check_predicate(
     let left = infer(
         field(value, "left")?,
         scope,
+        caps,
         definitions,
         source,
         parser,
@@ -524,6 +599,7 @@ fn check_predicate(
     let right = infer(
         field(value, "right")?,
         scope,
+        caps,
         definitions,
         source,
         parser,
@@ -651,9 +727,9 @@ impl Heights<'_> {
                 }
                 maximum + 1
             }
-            Expr::ByteUtf8 { value, .. } | Expr::ByteLength { value, .. } => {
-                self.expr(value, depth + 1)? + 1
-            }
+            Expr::ByteUtf8 { value, .. }
+            | Expr::ByteLength { value, .. }
+            | Expr::ByteCount { value, .. } => self.expr(value, depth + 1)? + 1,
             Expr::ByteSlice {
                 value, start, end, ..
             } => {
@@ -761,6 +837,7 @@ mod predicate_validation_tests {
             wire,
             &BTreeMap::new(),
             &BTreeMap::new(),
+            &BTreeMap::new(),
             true,
             &mut parser,
             0,
@@ -825,7 +902,15 @@ mod predicate_validation_tests {
                 coordinate: "generic.predicates@1",
                 remaining: MAX_PROGRAM_NODES,
             };
-            let result = infer(&call, &scope, &BTreeMap::new(), true, &mut parser, 0);
+            let result = infer(
+                &call,
+                &scope,
+                &BTreeMap::new(),
+                &BTreeMap::new(),
+                true,
+                &mut parser,
+                0,
+            );
             if accepted {
                 assert_eq!(result, Ok(RuntimeType::Bool));
             } else {
@@ -877,6 +962,7 @@ mod predicate_validation_tests {
                     &call,
                     &BTreeMap::from([("arg.0", &local)]),
                     &BTreeMap::new(),
+                    &BTreeMap::new(),
                     true,
                     &mut parser,
                     0,
diff --git a/crates/warp-core/src/edict_pure/model.rs b/crates/warp-core/src/edict_pure/model.rs
index a826b5f1..dd02efbd 100644
--- a/crates/warp-core/src/edict_pure/model.rs
+++ b/crates/warp-core/src/edict_pure/model.rs
@@ -28,6 +28,12 @@ pub(crate) enum Expr {
         max: u64,
         value: Box<Expr>,
     },
+    ByteCount {
+        min: u64,
+        max: u64,
+        value: Box<Expr>,
+        needle: u8,
+    },
     ByteSlice {
         min: u64,
         max: u64,
diff --git a/crates/warp-core/src/edict_pure/syntax.rs b/crates/warp-core/src/edict_pure/syntax.rs
index cc24469c..1c7fd142 100644
--- a/crates/warp-core/src/edict_pure/syntax.rs
+++ b/crates/warp-core/src/edict_pure/syntax.rs
@@ -130,6 +130,20 @@ impl Parser<'_> {
                 value: Box::new(self.expr(value, depth + 1)?),
             });
         }
+        if callee == "core.bytes.count" {
+            let ([value, needle], [coordinate]) = (args, types) else {
+                return Err(Error::UnsupportedProgram);
+            };
+            let RuntimeType::Bytes { min, max } = self.ty(text(coordinate)?, depth + 1)? else {
+                return Err(Error::UnsupportedProgram);
+            };
+            return Ok(Expr::ByteCount {
+                min,
+                max,
+                needle: count_needle(needle)?,
+                value: Box::new(self.expr(value, depth + 1)?),
+            });
+        }
         if callee == "core.bytes.length" {
             let ([value], [coordinate]) = (args, types) else {
                 return Err(Error::UnsupportedProgram);
@@ -362,6 +376,24 @@ fn byte_bound(value: &str) -> Result<u64, Error> {
     Ok(bound)
 }
 
+/// The counted byte is a Core constant of exactly one byte. Its shape is
+/// checked structurally, never inferred from a type.
+pub(crate) fn count_needle(needle: &Value) -> Result<u8, Error> {
+    exact_fields(needle, &["kind", "value"])?;
+    if text_field(needle, "kind")? != "const" {
+        return Err(Error::UnsupportedProgram);
+    }
+    let literal = field(needle, "value")?;
+    exact_fields(literal, &["kind", "value"])?;
+    if text_field(literal, "kind")? != "bytes" {
+        return Err(Error::UnsupportedProgram);
+    }
+    let [byte] = bytes(field(literal, "value")?)? else {
+        return Err(Error::UnsupportedProgram);
+    };
+    Ok(*byte)
+}
+
 #[cfg(test)]
 mod tests {
     use super::{constant, Error, Value};
diff --git a/docs/architecture/application-contract-hosting.md b/docs/architecture/application-contract-hosting.md
index 2345aa8a..64f1a98f 100644
--- a/docs/architecture/application-contract-hosting.md
+++ b/docs/architecture/application-contract-hosting.md
@@ -290,6 +290,16 @@ Boolean substitutes. Predicates support Boolean equality, not ordering.
 The native pure interpreter's implementation does not by itself establish
 provider component support or a public compiler/provider/runtime witness.
 
+The generic `core.bytes.count<OperandType>(bytes, needle)` operation counts the
+occurrences of one byte in a bounded raw-byte value and returns U64. The needle
+must be a Core byte constant of exactly one byte; the parser, the lowerer and
+the verifier each check that shape structurally, and refuse empty, multi-byte,
+integer and non-constant needles. It counts raw bytes, including NUL, 0xFF and
+invalid UTF-8, without decoding or normalization. It charges one work unit per
+actual operand byte for the scan, plus ordinary operand evaluation, bound
+validation and result storage. The result never exceeds the operand's byte
+maximum, which the addition proofs use.
+
 Negation uses the closed `not` predicate shape with exactly one `value` child.
 The interpreter validates the entire child before execution, evaluates it once,
 and inverts its Boolean result. A negation wrapper costs one predicate step;
diff --git a/docs/topics/GeneratedRules.md b/docs/topics/GeneratedRules.md
index f2e93d90..547c3244 100644
--- a/docs/topics/GeneratedRules.md
+++ b/docs/topics/GeneratedRules.md
@@ -139,6 +139,16 @@ even when the legacy Core function table is absent. Both implementations bound p
 using their existing work ceilings. Rebound native tests exercise these checks;
 they do not establish public compiler acceptance.
 
+An unsigned let binding carries its proven upper bound to later bindings and
+the result of the same intent or helper body, in the lowerer, the verifier and
+the native helper checker alike. Local identities are unique and immutable, so
+the carried bound names exactly that value. Bounds do not cross helper results
+or record fields. `core.bytes.count<OperandType>` contributes its operand's
+structural byte maximum, which each of the three resolves through the module's
+type table, so a named byte type such as `jedit.text@1.FactBytes` gives the same
+bound as its literal `Bytes<...>` form. `count(text, b"\n") + 1` is therefore
+proven for any operand below the width maximum, directly or through a binding.
+
 Runtime helper validation also proves addition within its fresh frame using
 literal and nested-sum bounds. Other terms retain their full unsigned width,
 so zero identity is total and an unbounded parameter plus one refuses. Caller
diff --git a/schemas/edict-provider/README.md b/schemas/edict-provider/README.md
index 4bf85393..ff123753 100644
--- a/schemas/edict-provider/README.md
+++ b/schemas/edict-provider/README.md
@@ -179,10 +179,10 @@ nor manifest. Independent fresh-store replay and separate host processes
 reproduce all three completed outcomes identically. Both checked components
 remain uninstalled package material; neither they nor the generated
 authority-facts documents are runtime Echo authority. The promoted lowerer is
-485,983 bytes with SHA-256
-`cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c`; the
-promoted verifier is 504,431 bytes with SHA-256
-`3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11`.
+490,344 bytes with SHA-256
+`34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587`; the
+promoted verifier is 507,253 bytes with SHA-256
+`c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e`.
 
 The checked schema/components also support the explicit
 `compiler-produced-bounded-read/v1` configuration with required `maxReads`
diff --git a/schemas/edict-provider/components/v1/README.md b/schemas/edict-provider/components/v1/README.md
index d17349a3..1d0a4d27 100644
--- a/schemas/edict-provider/components/v1/README.md
+++ b/schemas/edict-provider/components/v1/README.md
@@ -23,8 +23,8 @@ is componentized with `wit-component` 0.251.0.
 The source WIT is the exact 7,392-byte Edict contract with SHA-256
 `2971fe44def7e51d5271dfc0f04f3088aa58754cffdc847681a587605aac749e`.
 
-The checked component is 485,983 bytes with SHA-256
-`cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c`.
+The checked component is 490,344 bytes with SHA-256
+`34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587`.
 Its sole contract attestation is the top-level custom section
 `edict:target-provider-contract` containing
 `edict:target-provider/lowerer@1.0.0`. Its only imports are the frozen WIT's
@@ -35,9 +35,9 @@ capability imports.
 `verifier.echo-dpo.component.wasm` implements
 `edict:target-provider/verifier@1.0.0`. It uses the same immutable builder,
 authenticated Rust/Cargo identities, frozen WIT bytes, path-remapping law, and
-`wit-component` version recorded above. Its checked component is 504,431 bytes
+`wit-component` version recorded above. Its checked component is 507,253 bytes
 with SHA-256
-`3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11`.
+`c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e`.
 Its sole contract attestation is the top-level custom section
 `edict:target-provider-contract` containing
 `edict:target-provider/verifier@1.0.0`. Its only imports are the frozen WIT's
diff --git a/schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm b/schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm
index 424970f6..fb26b41a 100644
Binary files a/schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm and b/schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm differ
diff --git a/schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm b/schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm
index 9a766125..d8a88bd2 100644
Binary files a/schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm and b/schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm differ
diff --git a/schemas/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm b/schemas/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm
index 424970f6..fb26b41a 100644
Binary files a/schemas/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm and b/schemas/edict-provider/package/v1/components/lowerer.echo-dpo.component.wasm differ
diff --git a/schemas/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm b/schemas/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm
index 9a766125..d8a88bd2 100644
Binary files a/schemas/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm and b/schemas/edict-provider/package/v1/components/verifier.echo-dpo.component.wasm differ
diff --git a/schemas/edict-provider/package/v1/provider-manifest.echo.json b/schemas/edict-provider/package/v1/provider-manifest.echo.json
index 72f2301b..c6e6dd4a 100644
--- a/schemas/edict-provider/package/v1/provider-manifest.echo.json
+++ b/schemas/edict-provider/package/v1/provider-manifest.echo.json
@@ -3,7 +3,7 @@
   "providerAbi": "edict:target-provider@1.0.0",
   "provider": {
     "coordinate": "echo.edict-provider@1",
-    "digest": "sha256:36ce20c612c8c46bbe450c93e6fb2235f38e4ec2b14f04f128eee91805cdb26a"
+    "digest": "sha256:8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8"
   },
   "artifacts": [
     {
@@ -87,13 +87,13 @@
       "artifactKind": "lowerer",
       "resource": {
         "coordinate": "echo.dpo.lowerer/component@1",
-        "digest": "sha256:cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c"
+        "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587"
       },
       "source": {
         "kind": "component",
         "component": {
           "coordinate": "echo.dpo.lowerer/component@1",
-          "digest": "sha256:cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c"
+          "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587"
         }
       }
     },
@@ -178,13 +178,13 @@
       "artifactKind": "verifier",
       "resource": {
         "coordinate": "echo.dpo.verifier/component@1",
-        "digest": "sha256:3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11"
+        "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e"
       },
       "source": {
         "kind": "component",
         "component": {
           "coordinate": "echo.dpo.verifier/component@1",
-          "digest": "sha256:3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11"
+          "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e"
         }
       }
     }
diff --git a/xtask/src/provider_lowerer_component.rs b/xtask/src/provider_lowerer_component.rs
index 49cc91a9..89a62bdb 100644
--- a/xtask/src/provider_lowerer_component.rs
+++ b/xtask/src/provider_lowerer_component.rs
@@ -53,7 +53,7 @@ const PINNED_CARGO_COMMIT: &str = "840b83a10fb0e039a83f4d70ad032892c287570a";
 
 /// Reviewed identity that the portable promotion command is permitted to install.
 pub(crate) const APPROVED_CHECKED_COMPONENT_SHA256: &str =
-    "cd81874f971f290f74987b39479ef89ddb5060e56df54044d2359e6e89b2430c";
+    "34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587";
 pub(crate) const CHECKED_COMPONENT_REPOSITORY_PATH: &str =
     "schemas/edict-provider/components/v1/lowerer.echo-dpo.component.wasm";
 
@@ -62,7 +62,7 @@ pub(crate) const VERIFIER_CHECKED_COMPONENT_REPOSITORY_PATH: &str =
     "schemas/edict-provider/components/v1/verifier.echo-dpo.component.wasm";
 /// Approved SHA-256 identity of the checked verifier component.
 pub(crate) const APPROVED_CHECKED_VERIFIER_COMPONENT_SHA256: &str =
-    "3451e95a7d084d4874c30833f90f5c21012e8341f35ed0f0888d4d268a768b11";
+    "c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e";
 
 #[derive(Clone, Copy, Debug, Eq, PartialEq)]
 struct ProviderComponentSpec {