feat(warp-core): carry proven-range facts through authored effect programs

CHANGELOG.md

@@ -95,6 +95,13 @@
 
 ### Changed
 
+- Authored effect programs now carry Edict's proven-range facts at
+  preparation. The intent's input constraints dominate the body, an unsigned
+  `let` proven below its width carries that ceiling to later nodes, and an
+  addition bound also uses a dominating fact comparing its term with a
+  constant. A runtime `slice` or `subtract` in an effect program verifies when
+  those facts prove its range, so Jim's `isUtf8(slice(text, 0, at))` can run
+  inside the edit. A `require` still proves nothing after it, matching Edict.
 - `ContentAddressV1` now lives in one module, `warp_core::content_address_v1`,
   with content node ids, content and slot edge ids, and attachment digests.
   Effect admission and read evidence use it, replacing the inline hashing in

crates/warp-core/src/edict_effects/instruction_relation.rs

@@ -11,9 +11,9 @@ use crate::edict_pure::{
 use echo_edict_canonical::{encode_canonical_cbor_v1 as encode, CanonicalValueV1 as Value};
 use std::collections::{BTreeMap, BTreeSet};
 
-pub(super) fn validate(
-    module: &Value,
-    intent: &Value,
+pub(super) fn validate<'a>(
+    module: &'a Value,
+    intent: &'a Value,
     target: &Value,
     exports: &Value,
     signatures: &BTreeMap<&str, &Value>,
@@ -48,9 +48,15 @@ pub(super) fn validate(
         scope.expression(basis, None)?;
         scope.data_type(basis)?;
     }
-    for constraint in array(field(intent, "inputConstraints")?)? {
+    // As in Edict, each input constraint is checked without facts, and all of
+    // them then dominate the whole body.
+    let constraints = array(field(intent, "inputConstraints")?)?;
+    for constraint in constraints {
         scope.predicate(field(constraint, "predicate")?)?;
     }
+    for constraint in constraints {
+        scope.facts.push(field(constraint, "predicate")?);
+    }
     let mut lowered = BTreeMap::new();
     for (collection, kind) in [
         ("steps", "effect"),
@@ -86,6 +92,7 @@ pub(super) fn validate(
                     field(node, "value")?,
                     text_field(field(node, "binding")?, "type")?,
                 )?;
+                scope.carry_ceiling(field(node, "binding")?, field(node, "value")?)?;
                 scope.introduce(field(node, "binding")?)?;
             }
             "require" => {
@@ -202,6 +209,10 @@ struct Scope<'a> {
     remaining_references: usize,
     definitions: BTreeMap<String, functions::Definition<'a>>,
     helpers: BTreeMap<String, Helper>,
+    /// Input constraints, which dominate the whole body.
+    facts: Vec<&'a Value>,
+    /// Proven ceilings of earlier unsigned bindings.
+    caps: functions::Caps<'a>,
     expressions: Vec<Expr>,
     predicates: Vec<Predicate>,
 }
@@ -241,6 +252,8 @@ impl<'a> Scope<'a> {
             helpers,
             expressions: Vec::new(),
             predicates: Vec::new(),
+            facts: Vec::new(),
+            caps: functions::Caps::new(),
         })
     }
     fn claim(&mut self, reference: &Value) -> Result<&'a Value, Error> {
@@ -262,13 +275,10 @@ impl<'a> Scope<'a> {
         self.references(value, binder, 0)
     }
     fn data_type(&mut self, value: &Value) -> Result<RuntimeType, Error> {
-        // Effect programs carry no proof yet, so runtime slices and
-        // subtractions need literal operands.
-        let caps = functions::Caps::new();
         let actual = functions::infer(
             value,
             &self.available,
-            functions::Proof::new(&caps, &[]),
+            functions::Proof::new(&self.caps, &self.facts),
             &self.definitions,
             true,
             &mut self.parser,
@@ -277,6 +287,20 @@ impl<'a> Scope<'a> {
         self.expressions.push(self.parser.expr(value, 0)?);
         Ok(actual)
     }
+    /// An unsigned binding whose value is proven below its width carries that
+    /// ceiling to later nodes. Local identities are unique and immutable, so
+    /// the cap names exactly the bound value.
+    fn carry_ceiling(&mut self, binding: &'a Value, value: &Value) -> Result<(), Error> {
+        let RuntimeType::Unsigned(max) = self.parser.ty(text_field(binding, "type")?, 0)? else {
+            return Ok(());
+        };
+        let cap =
+            functions::unsigned_ceiling(value, max, &self.caps, &self.facts, &mut self.parser, 0)?;
+        if cap < max {
+            self.caps.insert(text_field(binding, "id")?, cap);
+        }
+        Ok(())
+    }
     fn typed_expression(&mut self, value: &Value, expected: &str) -> Result<(), Error> {
         self.expression(value, None)?;
         let actual = self.data_type(value)?;
@@ -287,11 +311,10 @@ impl<'a> Scope<'a> {
         Ok(())
     }
     fn predicate(&mut self, value: &Value) -> Result<(), Error> {
-        let caps = functions::Caps::new();
         functions::check_predicate(
             value,
             &self.available,
-            functions::Proof::new(&caps, &[]),
+            functions::Proof::new(&self.caps, &self.facts),
             &self.definitions,
             true,
             &mut self.parser,

crates/warp-core/src/edict_pure/functions.rs

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: Apache-2.0
 // © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
 //! Closed source/imported helper authority, lexical scopes, and runtime apertures.
-use super::proven_order::{length_of, proven};
+use super::proven_order::{length_of, proven, upper_limit};
 use super::{
     model::{
         Binding, Expr, Helper, Parameter, Predicate, RuntimeType, MAX_DEPTH, MAX_PROGRAM_NODES,
@@ -167,7 +167,7 @@ pub(crate) fn decode(
                 return Err(Error::InvalidArtifact);
             }
             if let RuntimeType::Unsigned(max) = ty {
-                let cap = unsigned_ceiling(value, max, &caps, parser, 0)?;
+                let cap = unsigned_ceiling(value, max, &caps, &[], parser, 0)?;
                 if cap < max {
                     caps.insert(id, cap);
                 }
@@ -514,10 +514,22 @@ pub(crate) fn infer<'v>(
                 ("core.integer.add", [left, right], [expected @ RuntimeType::Unsigned(max)])
                     if left == expected && right == expected =>
                 {
-                    let left =
-                        unsigned_ceiling(&arguments[0], *max, proof.caps, parser, depth + 1)?;
-                    let right =
-                        unsigned_ceiling(&arguments[1], *max, proof.caps, parser, depth + 1)?;
+                    let left = unsigned_ceiling(
+                        &arguments[0],
+                        *max,
+                        proof.caps,
+                        proof.facts,
+                        parser,
+                        depth + 1,
+                    )?;
+                    let right = unsigned_ceiling(
+                        &arguments[1],
+                        *max,
+                        proof.caps,
+                        proof.facts,
+                        parser,
+                        depth + 1,
+                    )?;
                     if left.checked_add(right).is_none_or(|sum| sum > *max) {
                         return Err(Error::UnsupportedProgram);
                     }
@@ -561,13 +573,29 @@ pub(crate) fn infer<'v>(
     }
 }
 
-// Fresh helper frames receive no caller constraints. Constants and already
-// checked nested additions can narrow a bound; every other term has its full
-// declared width. The parser's combined work/depth ceiling covers this walk.
-fn unsigned_ceiling(
+// Constants, counts, carried binding caps and already checked nested additions
+// can narrow a bound, and so can a dominating fact comparing the term with a
+// constant; every other term has its full declared width. Fresh helper frames
+// receive no caller facts. The parser's combined work/depth ceiling covers
+// this walk.
+pub(crate) fn unsigned_ceiling(
+    value: &Value,
+    max: u64,
+    caps: &Caps<'_>,
+    facts: &[&Value],
+    parser: &mut Parser<'_>,
+    depth: usize,
+) -> Result<u64, Error> {
+    let structural = structural_ceiling(value, max, caps, facts, parser, depth)?;
+    Ok(upper_limit(value, facts, parser, depth + 1)?
+        .map_or(structural, |limit| structural.min(limit)))
+}
+
+fn structural_ceiling(
     value: &Value,
     max: u64,
     caps: &Caps<'_>,
+    facts: &[&Value],
     parser: &mut Parser<'_>,
     depth: usize,
 ) -> Result<u64, Error> {
@@ -593,8 +621,15 @@ fn unsigned_ceiling(
         let [left, right] = array(field(value, "args")?)? else {
             return Err(Error::InvalidArtifact);
         };
-        return unsigned_ceiling(left, max, caps, parser, depth + 1)?
-            .checked_add(unsigned_ceiling(right, max, caps, parser, depth + 1)?)
+        return unsigned_ceiling(left, max, caps, facts, parser, depth + 1)?
+            .checked_add(unsigned_ceiling(
+                right,
+                max,
+                caps,
+                facts,
+                parser,
+                depth + 1,
+            )?)
             .ok_or(Error::UnsupportedProgram);
     }
     Ok(max)

crates/warp-core/src/edict_pure/proven_order.rs

@@ -38,6 +38,74 @@ pub(crate) fn proven(
     Ok(false)
 }
 
+/// The smallest constant upper bound a dominating fact gives `term`, as in
+/// Edict: `term <= c`, `term == c` or `c >= term` give `c`, and the strict forms
+/// give `c - 1` (saturating). Conjunctions contribute every conjunct.
+pub(crate) fn upper_limit(
+    term: &Value,
+    facts: &[&Value],
+    parser: &mut Parser<'_>,
+    depth: usize,
+) -> Result<Option<u64>, Error> {
+    if facts.is_empty() {
+        return Ok(None);
+    }
+    parser.enter(depth)?;
+    let term = key(term, parser)?;
+    let mut limit = None;
+    for fact in facts {
+        limit_from(fact, &term, &mut limit, parser, depth + 1)?;
+    }
+    Ok(limit)
+}
+
+fn limit_from(
+    fact: &Value,
+    term: &[u8],
+    limit: &mut Option<u64>,
+    parser: &mut Parser<'_>,
+    depth: usize,
+) -> Result<(), Error> {
+    parser.enter(depth)?;
+    match text_field(fact, "kind")? {
+        "all" => {
+            for item in array(field(fact, "values")?)? {
+                limit_from(item, term, limit, parser, depth + 1)?;
+            }
+        }
+        "compare" => {
+            let op = text_field(fact, "op")?;
+            let left = field(fact, "left")?;
+            let right = field(fact, "right")?;
+            let strict = matches!(op, "<" | ">");
+            let mut bound = |value: u64| {
+                let value = if strict {
+                    value.saturating_sub(1)
+                } else {
+                    value
+                };
+                *limit = Some(limit.map_or(value, |current| current.min(value)));
+            };
+            if matches!(op, "<=" | "<" | "==") {
+                if let Some(value) = constant(right) {
+                    if key(left, parser)? == term {
+                        bound(value);
+                    }
+                }
+            }
+            if matches!(op, ">=" | ">" | "==") {
+                if let Some(value) = constant(left) {
+                    if key(right, parser)? == term {
+                        bound(value);
+                    }
+                }
+            }
+        }
+        _ => {}
+    }
+    Ok(())
+}
+
 /// The Core term `core.bytes.length<coordinate>(bytes)`, for slice end proofs.
 pub(crate) fn length_of(coordinate: &Value, bytes: &Value) -> Value {
     Value::Map(vec![

crates/warp-core/tests/edict_effect_package_tests.rs

@@ -1708,3 +1708,7 @@ mod completion;
 #[cfg(feature = "native_rule_bootstrap")]
 #[path = "edict_effect_package_tests/derivation.rs"]
 mod derivation;
+
+#[cfg(feature = "native_rule_bootstrap")]
+#[path = "edict_effect_package_tests/proven_ranges.rs"]
+mod proven_ranges;