Merge pull request #956 from flyingrobots/feat/bounded-list-worklist

feat(provider): execute bounded list worklist operations

Author: flyingrobots

CHANGELOG.md

@@ -7,6 +7,27 @@
 
 ### Added
 
+- The provider judgments and runtime paths support bounded list length,
+  checked access, capacity-preserving append and bound-summing concatenation
+  under `core.list/v1`. Synthetic tests cover strict domains, capability and
+  type refusals, deterministic copy charges and one-unit-short budgets.
+  Append and concat bind each declared operand type to its reconstructed type;
+  coherently widening concat operands cannot invent capacity or item bounds.
+  Inline record coordinates from structural alias joins resolve under bounded
+  parsing in pure, ordered-read and runtime judgments, preserving nominal fields.
+  Provider judgments and runtime preparation include operand validation depth across helper calls;
+  capability discovery preserves the canonical artifact nesting allowance.
+  List-domain proof scans keep ancestor predicate depth separate from descendant
+  expression depth while preserving work and actual nesting limits.
+  The checked Wasm component pair is promoted from two matching independent
+  builds, with refreshed package manifests and identity goldens. Public compiler
+  witnesses execute non-idempotent worklist folds at bounds 0/1/2/3/5, structural
+  alias concatenation and stored-read worklists, including nominal elements
+  and forward, reversed and negated strict bounds on equal-width words.
+  Independent result oracles check contents, order, duplicate retention and
+  guarded indexing. Exact/one-unit-short limits, invalid inputs and old-provider
+  refusals exercise the compiler, separate verifier and runtime boundaries.
+
 - The source-function lowerer, independent verifier and runtime support
   bounded list values with element/length checks and deterministic resource
   accounting. Ordered-read judgments accept lists and recursive record/branch

crates/echo-edict-provider-lowerer/README.md

@@ -139,8 +139,8 @@ proposal constructor supports mutations and refuses a `Query`; authored reads
 remain a separate bounded observer/optic path and must never be represented as
 synthetic mutations.
 
-The refreshed 478,042-byte checked lowerer component has SHA-256
-`2a3738e3947529990143e184c0c1f39858e921738e6c6efaaeb4b7da5110626d` and has
+The refreshed 543,117-byte checked lowerer component has SHA-256
+`873dfec859285f26cadff97a7aa602fd91bcbcba3a3d347918c3658c4575afaa` and has
 crossed the reproducible promotion boundary. The pinned Edict host admits its
 generated envelope under the owning `generated-artifact` CDDL root, and the
 isolated host fixture exercises the exact helper binding, typed codecs, EINT

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

@@ -5,6 +5,7 @@
 mod bounded_read;
 mod capabilities;
 mod effect_resources;
+mod record_type;
 mod source_functions;
 
 use std::collections::BTreeSet;

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

@@ -172,6 +172,24 @@ impl<'a> Scope<'a> {
                 canonical_number(max)?,
             ));
         }
+        if let Some(spec) = coordinate
+            .strip_prefix("Record<")
+            .and_then(|s| s.strip_suffix('>'))
+        {
+            self.remaining_type_work.set(
+                self.remaining_type_work
+                    .get()
+                    .checked_sub(spec.len())
+                    .ok_or_else(invalid)?,
+            );
+            let mut fields = BTreeMap::new();
+            for (name, coordinate) in
+                super::super::super::record_type::fields(spec).map_err(|()| invalid())?
+            {
+                fields.insert(name.to_owned(), self.resolve(coordinate, depth + 1)?);
+            }
+            return Ok(ReadType::Record(fields));
+        }
         let key = coordinate.strip_prefix(&prefix).unwrap_or(coordinate);
         let value = field(field(self.core, "types")?, key)?;
         match text(value, "kind")? {
@@ -437,6 +455,30 @@ impl<'a> Scope<'a> {
             })
             .collect::<Result<Vec<_>, _>>()?;
         match (name, actual.as_slice(), declared.as_slice()) {
+            // Whole-intent checking has already proved the list domains.
+            ("core.list.length", [value], [ty @ ReadType::List(Some(_), _)])
+                if ty.accepts(value) =>
+            {
+                Ok(ReadType::Unsigned(u64::MAX))
+            }
+            (
+                "core.list.at",
+                [value, ReadType::Unsigned(u64::MAX)],
+                [ty @ ReadType::List(Some(item), _)],
+            ) if ty.accepts(value) => Ok(*item.clone()),
+            ("core.list.append", [value, entry], [ty @ ReadType::List(Some(item), _)])
+                if ty == value && item.accepts(entry) =>
+            {
+                Ok(ty.clone())
+            }
+            (
+                "core.list.concat",
+                [left, right],
+                [a @ ReadType::List(Some(item), n), b @ ReadType::List(Some(other), m)],
+            ) if item == other && a.accepts(left) && b.accepts(right) => Ok(ReadType::List(
+                Some(item.clone()),
+                n.checked_add(*m).ok_or_else(invalid)?,
+            )),
             // source_functions::validate already established the independent
             // no-overflow and order proofs before this read relation is constructed.
             ("core.integer.add", [left, right], [expected @ ReadType::Unsigned(_)])
@@ -528,9 +570,11 @@ impl<'a> Scope<'a> {
         ) {
             ("==", ReadType::Bool, ReadType::Bool)
             | ("==", ReadType::Bytes(_, _), ReadType::Bytes(_, _)) => Ok(()),
-            ("==" | "<=", ReadType::Unsigned(left), ReadType::Unsigned(right)) if left == right => {
-                Ok(())
-            }
+            (
+                "==" | "<=" | "<" | ">" | ">=",
+                ReadType::Unsigned(left),
+                ReadType::Unsigned(right),
+            ) if left == right => Ok(()),
             _ => Err(invalid()),
         }
     }

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

@@ -3,6 +3,161 @@
 //! Read type-judgment witnesses; these do not claim public compiler provenance.
 use super::*;
 
+#[test]
+fn ordered_list_guards_accept_strict_word_comparisons() {
+    let core = core();
+    let operation = |name: &str, args| {
+        m([
+            ("kind", t("call")),
+            ("callee", t(name)),
+            ("typeArgs", Value::Array(vec![t("Numbers")])),
+            ("args", Value::Array(args)),
+        ])
+    };
+    let length = operation("core.list.length", vec![call("numbers", vec![])]);
+    let access = operation("core.list.at", vec![call("numbers", vec![]), integer(0)]);
+    let conditional = |op: &str, index: Value, reversed: bool, negated: bool| {
+        let (left, right) = if reversed {
+            (length.clone(), index)
+        } else {
+            (index, length.clone())
+        };
+        m([
+            ("kind", t("if")),
+            (
+                "predicate",
+                m([
+                    ("kind", t("compare")),
+                    ("op", t(op)),
+                    ("left", left),
+                    ("right", right),
+                ]),
+            ),
+            ("then", if negated { integer(0) } else { access.clone() }),
+            ("else", if negated { access.clone() } else { integer(0) }),
+        ])
+    };
+    let wrong_width = m([
+        ("kind", t("const")),
+        (
+            "value",
+            m([
+                ("kind", t("int")),
+                ("width", t("U8")),
+                ("value", Value::Integer(0)),
+            ]),
+        ),
+    ]);
+    let mut admitted = Vec::new();
+    for (op, reversed, negated) in [
+        ("<", false, false),
+        ("<=", true, true),
+        (">", true, false),
+        (">=", false, true),
+    ] {
+        admitted.push(
+            check(
+                &core,
+                &conditional(op, integer(0), reversed, negated),
+                "U64",
+            )
+            .is_ok(),
+        );
+        assert_refusal(check(
+            &core,
+            &conditional(op, wrong_width.clone(), reversed, negated),
+            "U64",
+        ));
+    }
+    assert_eq!(
+        admitted,
+        vec![true, true, true, true],
+        "all compiler-supported strict guard orientations"
+    );
+}
+
+#[test]
+fn ordered_list_operations_preserve_types_after_domain_validation() {
+    let core = core();
+    let operation = |name: &str, types: &[&str], args| {
+        m([
+            ("kind", t("call")),
+            ("callee", t(name)),
+            (
+                "typeArgs",
+                Value::Array(types.iter().map(|s| t(s)).collect()),
+            ),
+            ("args", Value::Array(args)),
+        ])
+    };
+    let numbers = || call("numbers", vec![]);
+    // This type relation runs after the separate whole-intent domain audit.
+    for (value, expected) in [
+        (
+            operation("core.list.length", &["Numbers"], vec![numbers()]),
+            "U64",
+        ),
+        (
+            operation("core.list.at", &["Numbers"], vec![numbers(), integer(0)]),
+            "U64",
+        ),
+        (
+            operation(
+                "core.list.append",
+                &["Numbers"],
+                vec![numbers(), integer(7)],
+            ),
+            "Numbers",
+        ),
+        (
+            operation(
+                "core.list.concat",
+                &["Numbers", "Numbers"],
+                vec![numbers(), numbers()],
+            ),
+            "List<U64,max=4>",
+        ),
+    ] {
+        assert!(check(&core, &value, expected).is_ok(), "{expected}");
+    }
+    for (value, expected) in [
+        (
+            operation(
+                "core.list.append",
+                &["List<U64,max=3>"],
+                vec![numbers(), integer(7)],
+            ),
+            "List<U64,max=3>",
+        ),
+        (
+            operation(
+                "core.list.concat",
+                &["Numbers", "Numbers"],
+                vec![numbers(), numbers()],
+            ),
+            "List<U64,max=3>",
+        ),
+        (
+            operation(
+                "core.list.at",
+                &["List<U8,max=2>"],
+                vec![numbers(), integer(0)],
+            ),
+            "U8",
+        ),
+        (
+            operation(
+                "core.list.concat",
+                &["List<U64,max=18446744073709551615>", "Numbers"],
+                vec![numbers(), numbers()],
+            ),
+            "Numbers",
+        ),
+    ] {
+        assert_refusal(check(&core, &value, expected));
+    }
+}
+
 fn t(value: &str) -> Value {
     Value::Text(value.into())
 }
@@ -47,6 +202,7 @@ fn row(value: Value) -> Value {
 fn core() -> Value {
     m([
         ("coordinate", t("example@1")),
+        ("pureFunctions", Value::Array(vec![])),
         (
             "types",
             m([
@@ -255,3 +411,38 @@ fn assert_refusal(result: Result<(), ProviderRefusalV1>) {
         "{result:?}"
     );
 }
+
+#[test]
+fn list_inline_record_types_preserve_structural_and_nominal_meaning() {
+    let core = core();
+    let judgment = scope(&core);
+    assert!(judgment.ty("Row").is_ok());
+    assert!(judgment.ty("Record<payload:Bytes<max=4>>").is_ok());
+    assert_eq!(
+        judgment.ty("Row"),
+        judgment.ty("Record<payload:Bytes<max=4>>")
+    );
+    assert!(judgment
+        .ty("List<Record<a:A,nested:List<Record<x:U8>,max=2>>,max=3>")
+        .is_ok());
+    assert!(judgment.ty("Record<a:A>").is_ok());
+    assert!(judgment.ty("Record<a:B>").is_ok());
+    assert_ne!(judgment.ty("Record<a:A>"), judgment.ty("Record<a:B>"));
+    assert!(judgment.ty("Record<>").is_ok());
+    for invalid in [
+        "Record<x:U8,x:U8>",
+        "Record<z:U8,a:U8>",
+        "Record<x:U8,>",
+        "Record<:U8>",
+        "Record<0x:U8>",
+        "Record<x:>",
+        "Record<x:List<U8,max=1>>>",
+        "Record<x:Unknown>",
+    ] {
+        assert!(judgment.ty(invalid).is_err(), "{invalid}");
+    }
+    judgment.remaining_type_work.set(3);
+    assert!(judgment.ty("Record<long:U8,z:U8>").is_err());
+    let deep = format!("{}U8{}", "Record<x:".repeat(65), ">".repeat(65));
+    assert!(scope(&core).ty(&deep).is_err());
+}

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

@@ -16,8 +16,10 @@ pub(super) fn validate(core: &Value) -> Result<(), ProviderRefusalV1> {
                 "required capability is not text",
             ));
         };
-        if !matches!(name.as_str(), "core.variant/v1" | "core.fold/v1")
-            || !supported.insert(name.as_str())
+        if !matches!(
+            name.as_str(),
+            "core.variant/v1" | "core.fold/v1" | "core.list/v1"
+        ) || !supported.insert(name.as_str())
         {
             return Err(super::super::unsupported_semantics(
                 SUBJECT,

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

@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+//! Lowerer-owned grammar for structural record coordinates. Callers charge bytes
+//! before scanning and recursively resolve fields under their existing work bound.
+
+pub(super) fn fields(spec: &str) -> Result<Vec<(&str, &str)>, ()> {
+    if spec.is_empty() {
+        return Ok(Vec::new());
+    }
+    let mut result = Vec::new();
+    let mut start = 0;
+    let mut nesting = 0_usize;
+    for (index, byte) in spec.bytes().chain(std::iter::once(b',')).enumerate() {
+        match byte {
+            b'<' => {
+                nesting = nesting.checked_add(1).ok_or(())?;
+                if nesting > 64 {
+                    return Err(());
+                }
+            }
+            b'>' => nesting = nesting.checked_sub(1).ok_or(())?,
+            b',' if nesting == 0 => {
+                let (key, coordinate) = spec[start..index].split_once(':').ok_or(())?;
+                let mut letters = key.bytes();
+                if !letters
+                    .next()
+                    .is_some_and(|b| b.is_ascii_alphabetic() || b == b'_')
+                    || !letters.all(|b| b.is_ascii_alphanumeric() || b == b'_')
+                    || coordinate.is_empty()
+                    || result.last().is_some_and(|(previous, _)| *previous >= key)
+                {
+                    return Err(());
+                }
+                result.push((key, coordinate));
+                start = index + 1;
+            }
+            _ => {}
+        }
+    }
+    if nesting != 0 {
+        return Err(());
+    }
+    Ok(result)
+}