diff --git a/CHANGELOG.md b/CHANGELOG.md index 2ae4039c..721939ac 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -95,6 +95,14 @@ ### Changed +- A Core without a function table that contains `core.bytes.slice` or + `core.integer.subtract` is now judged in full by the lowerer and verifier, + including its declared budget, as addition already was. Previously such a + Core skipped that judgment, so an unproven runtime slice was not refused + before installation. Jim's retained leaf-slice package declares a 1 MiB step + budget, 93 steps below Echo's worst-case charge for slicing its whole 1 MiB + operand, and is now refused until it declares an adequate budget. + - Provider semantic declarations now support explicitly bounded Core byte aliases, including exact 32-byte identifiers. Byte aliases participate in bounded record graphs and generate canonical lawpack type definitions. @@ -342,6 +350,17 @@ ### Added +- Runtime operands for `core.bytes.slice` and `core.integer.subtract` under + Edict's proven-range rules. The lowerer, the verifier and the native helper + checker each require a dominating fact (an input constraint or an earlier + conjunct of the same `all`) for `start <= end <= len(bytes)` or + `right <= left`; conditional predicates, negations and later conjuncts prove + nothing. The bounded-read relations type both calls, so a read guard such as + `at <= len(text) && isUtf8(slice(text, 0, at))` verifies, and short-circuit + evaluation sends an out-of-range `at` down the authored path. Slices are now + typed `Bytes`, as Edict types them, rather than narrowed for literal + offsets, so `isUtf8` of a literal slice type-checks. + - Bounded pure evaluation executes Edict's `core.bytes.count` (edict#269): raw single-byte counting with a structurally checked one-byte constant needle and one complete scan charged. The lowerer and verifier type it 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 00b71226..79b359ac 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 @@ -364,12 +364,25 @@ impl<'a> Scope<'a> { .collect::, _>>()?; match (name, actual.as_slice(), declared.as_slice()) { // source_functions::validate already established the independent - // no-overflow proof before this read relation is constructed. + // no-overflow and order proofs before this read relation is constructed. ("core.integer.add", [left, right], [expected @ ReadType::Unsigned(_)]) if left == expected && right == expected => { Ok(expected.clone()) } + ("core.integer.subtract", [left, right], [expected @ ReadType::Unsigned(_)]) + if expected.accepts(left) && expected.accepts(right) => + { + Ok(expected.clone()) + } + // The same validation established start <= end <= len(bytes). + ( + "core.bytes.slice", + [actual, ReadType::Unsigned(a), ReadType::Unsigned(b)], + [expected @ ReadType::Bytes(_, max)], + ) if *a == u64::MAX && *b == u64::MAX && expected.accepts(actual) => { + Ok(ReadType::Bytes(0, *max)) + } ("core.bytes.isUtf8", [actual], [expected @ ReadType::Bytes(_, _)]) if expected == actual => { 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 ae014233..6252b189 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 @@ -2,6 +2,7 @@ // © James Ross Ω FLYING•ROBOTS //! Lowerer-owned forward type, totality, depth and deterministic cost judgment. //! Applies to the complete source-function module, including unused definitions. +mod order; mod unsigned_addition; use super::ProviderRefusalV1; use echo_edict_canonical::CanonicalValueV1 as Value; @@ -618,9 +619,14 @@ impl<'a> Judgment<'a> { ("core.integer.subtract", [left, right], [expected @ Ty::Word(_)]) if includes(expected, left) && includes(expected, right) => { - literal(&arguments[0])? - .checked_sub(literal(&arguments[1])?) - .ok_or(())?; + if !order::proven( + &arguments[0], + &arguments[1], + &self.proven, + &mut self.work, + )? { + return Err(()); + } cost = cost.plus(Cost { steps: 3, bytes: 64, @@ -630,19 +636,36 @@ impl<'a> Judgment<'a> { ( "core.bytes.slice", [actual, Ty::Word(a), Ty::Word(b)], - [expected @ Ty::Bytes(min, _)], + [expected @ Ty::Bytes(min, max)], ) if *a == u64::MAX && *b == u64::MAX && includes(expected, actual) => { - let start = literal(&arguments[1])?; - let end = literal(&arguments[2])?; - if start > end || end > *min { - return Err(()); - } - let count = end - start; + // Literal offsets within the guaranteed minimum length need + // no fact; any other offsets need start <= end <= len(bytes). + let copied = match (literal(&arguments[1]), literal(&arguments[2])) { + (Ok(start), Ok(end)) if start <= end && end <= *min => end - start, + _ => { + let length = order::length_of(&types[0], &arguments[0]); + if !order::proven( + &arguments[2], + &arguments[1], + &self.proven, + &mut self.work, + )? || !order::proven( + &length, + &arguments[2], + &self.proven, + &mut self.work, + )? { + return Err(()); + } + *max + } + }; cost = cost.plus(Cost { - steps: count.checked_add(4).ok_or(())?, - bytes: count.checked_add(64).ok_or(())?, + steps: copied.checked_add(4).ok_or(())?, + bytes: copied.checked_add(64).ok_or(())?, })?; - Ty::Bytes(0, count) + // As in Edict, a slice keeps its operand's maximum and no minimum. + Ty::Bytes(0, *max) } _ => return Err(()), } diff --git a/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/order.rs b/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/order.rs new file mode 100644 index 00000000..68642c01 --- /dev/null +++ b/crates/echo-edict-provider-lowerer/src/executable_operation/source_functions/order.rs @@ -0,0 +1,96 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Lowerer-owned order proofs for partial byte slicing and unsigned subtraction. +//! +//! `left >= right` holds for equal terms, a zero right side, ordered +//! constants, or a dominating fact: an input constraint or an earlier +//! conjunct of an enclosing `all`. Conditional predicates, negations and +//! later conjuncts prove nothing. +use super::{get, list, literal, string, Check, Value}; + +pub(super) fn proven( + left: &Value, + right: &Value, + facts: &[&Value], + work: &mut usize, +) -> Check { + let left_key = key(left, work)?; + let right_key = key(right, work)?; + if left_key == right_key || literal(right) == Ok(0) { + return Ok(true); + } + if let (Ok(a), Ok(b)) = (literal(left), literal(right)) { + return Ok(a >= b); + } + for fact in facts { + if supports(fact, &left_key, &right_key, work, 0)? { + return Ok(true); + } + } + Ok(false) +} + +/// The Core term `core.bytes.length(bytes)`, for slice end proofs. +pub(super) fn length_of(coordinate: &Value, bytes: &Value) -> Value { + Value::Map(vec![ + (Value::Text("kind".into()), Value::Text("call".into())), + ( + Value::Text("callee".into()), + Value::Text("core.bytes.length".into()), + ), + ( + Value::Text("typeArgs".into()), + Value::Array(vec![coordinate.clone()]), + ), + ( + Value::Text("args".into()), + Value::Array(vec![bytes.clone()]), + ), + ]) +} + +fn supports( + fact: &Value, + left: &[u8], + right: &[u8], + work: &mut usize, + depth: usize, +) -> Check { + debit(work, 1)?; + if depth > 64 { + return Err(()); + } + match string(get(fact, "kind")?)? { + "all" => { + for item in list(get(fact, "values")?)? { + if supports(item, left, right, work, depth + 1)? { + return Ok(true); + } + } + Ok(false) + } + "compare" => { + let a = key(get(fact, "left")?, work)?; + let b = key(get(fact, "right")?, work)?; + Ok(match string(get(fact, "op")?)? { + ">=" | ">" => a == left && b == right, + "<=" | "<" => a == right && b == left, + "==" => (a == left && b == right) || (a == right && b == left), + _ => false, + }) + } + _ => Ok(false), + } +} + +/// Terms compare by canonical encoding, independent of in-memory map order. +fn key(value: &Value, work: &mut usize) -> Check> { + let bytes = echo_edict_canonical::encode_canonical_cbor_v1(value).map_err(|_| ())?; + debit(work, bytes.len())?; + Ok(bytes) +} + +fn debit(work: &mut usize, amount: usize) -> Check<()> { + *work = work.checked_sub(amount).ok_or(())?; + Ok(()) +} 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 527670b1..ea818566 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 @@ -4,17 +4,23 @@ use super::{get, list, literal, string, Check, Value}; /// Whether an intent body calls an operation only this judgment checks: an -/// addition's no-overflow proof or a count's full-byte scan charge. A Core -/// without a function table still needs the judgment for either. +/// addition's no-overflow proof, a subtraction's or slice's range proof, or a +/// count's full-byte scan charge. A Core without a function table still needs +/// the judgment for any of them. pub(super) fn present(core: &Value) -> Check { let mut pending = vec![get(core, "intents")?]; while let Some(value) = pending.pop() { match value { Value::Map(fields) => { + // Each of these needs an intent-level proof, even without a + // source-function table. if get(value, "kind").and_then(string) == Ok("call") && matches!( get(value, "callee").and_then(string), - Ok("core.integer.add" | "core.bytes.count") + Ok("core.integer.add" + | "core.integer.subtract" + | "core.bytes.slice" + | "core.bytes.count") ) { return Ok(true); 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 2fb5d8cc..4c0b71e5 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 @@ -344,12 +344,28 @@ impl<'a> Symbols<'a> { declared.push(self.schema(string(coordinate)?, 0)?); } match (name, actual.as_slice(), declared.as_slice()) { - // The source-function audit has independently proved totality. + // The source-function audit has independently proved totality and order. ("core.integer.add", [left, right], [expected @ Schema::Word(_)]) if left == expected && right == expected => { Ok(expected.clone()) } + ("core.integer.subtract", [left, right], [expected @ Schema::Word(_)]) + if expected.includes(left) && expected.includes(right) => + { + Ok(expected.clone()) + } + // The same audit independently proved start <= end <= len(bytes). + ( + "core.bytes.slice", + [actual, Schema::Word(a), Schema::Word(b)], + [expected @ Schema::Bytes { upper, .. }], + ) if *a == u64::MAX && *b == u64::MAX && expected.includes(actual) => { + Ok(Schema::Bytes { + lower: 0, + upper: *upper, + }) + } ("core.bytes.isUtf8", [actual], [expected @ Schema::Bytes { .. }]) if expected == actual => { 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 aa4166eb..b27a6604 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 @@ -2,6 +2,7 @@ // © James Ross Ω FLYING•ROBOTS //! Independent verifier judgment: inventory authority, eliminate dependency leaves, //! then audit ordered lexical frames and conservative whole-operation charges. +mod order; mod types; mod unsigned_addition; use super::ProviderRefusalV1; @@ -520,12 +521,28 @@ impl<'a> Checker<'a, '_> { } else { false }; + let order_proven = match name { + "core.integer.subtract" => { + let [left, right] = arguments else { + return Err(()); + }; + order::proven(left, right, &self.proven, self.types)? + } + "core.bytes.slice" => { + let [coordinate] = types else { + return Err(()); + }; + order::slice_in_range(coordinate, arguments, &self.proven, self.types)? + } + _ => false, + }; let (schema, intrinsic) = intrinsic( name, arguments, &argument_schemas, &declared, addition_proven, + order_proven, )?; charge.append(intrinsic)?; schema @@ -745,6 +762,7 @@ fn intrinsic( actual: &[Schema], declared: &[Schema], addition_proven: bool, + order_proven: bool, ) -> Check<(Schema, Charge)> { let literal = |value: &Value| -> Check { if string(get(value, "kind")?)? != "const" { @@ -822,9 +840,9 @@ fn intrinsic( ("core.integer.subtract", [left, right], [expected @ Schema::Word(_)]) if expected.encloses(left) && expected.encloses(right) => { - literal(&arguments[0])? - .checked_sub(literal(&arguments[1])?) - .ok_or(())?; + if !order_proven { + return Err(()); + } Ok(( expected.clone(), Charge { @@ -836,19 +854,24 @@ fn intrinsic( ( "core.bytes.slice", [actual, Schema::Word(a), Schema::Word(b)], - [expected @ Schema::Blob { low, .. }], + [expected @ Schema::Blob { low, high }], ) if *a == u64::MAX && *b == u64::MAX && expected.encloses(actual) => { - let start = literal(&arguments[1])?; - let end = literal(&arguments[2])?; - if start > end || end > *low { - return Err(()); - } - let high = end - start; + // Literal offsets within the guaranteed minimum length need no + // fact; any other offsets need start <= end <= len(bytes). + let copied = match (literal(&arguments[1]), literal(&arguments[2])) { + (Ok(start), Ok(end)) if start <= end && end <= *low => end - start, + _ if order_proven => *high, + _ => return Err(()), + }; + // As in Edict, a slice keeps its operand's maximum and no minimum. Ok(( - Schema::Blob { low: 0, high }, + Schema::Blob { + low: 0, + high: *high, + }, Charge { - ticks: u128::from(high) + 4, - storage: u128::from(high) + 64, + ticks: u128::from(copied) + 4, + storage: u128::from(copied) + 64, }, )) } diff --git a/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/order.rs b/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/order.rs new file mode 100644 index 00000000..144c53fe --- /dev/null +++ b/crates/echo-edict-provider-verifier/src/executable_operation/source_functions/order.rs @@ -0,0 +1,108 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Verifier-owned order proofs for partial byte slicing and unsigned subtraction. +//! +//! `left >= right` holds for equal terms, a zero right side, ordered +//! constants, or a dominating fact: an input constraint or an earlier +//! conjunct of an enclosing `all`. Conditional predicates, negations and +//! later conjuncts prove nothing. +use super::{get, sequence, string, unsigned, Check, Types, Value}; + +pub(super) fn proven( + left: &Value, + right: &Value, + facts: &[&Value], + types: &mut Types<'_>, +) -> Check { + let left_key = key(left, types)?; + let right_key = key(right, types)?; + if left_key == right_key || constant(right) == Some(0) { + return Ok(true); + } + if let (Some(a), Some(b)) = (constant(left), constant(right)) { + return Ok(a >= b); + } + for fact in facts { + if supports(fact, &left_key, &right_key, types, 0)? { + return Ok(true); + } + } + Ok(false) +} + +/// Whether a slice's offsets are `start <= end <= len(bytes)` here. +pub(super) fn slice_in_range( + coordinate: &Value, + arguments: &[Value], + facts: &[&Value], + types: &mut Types<'_>, +) -> Check { + let [bytes, start, end] = arguments else { + return Err(()); + }; + let length = Value::Map(vec![ + (Value::Text("kind".into()), Value::Text("call".into())), + ( + Value::Text("callee".into()), + Value::Text("core.bytes.length".into()), + ), + ( + Value::Text("typeArgs".into()), + Value::Array(vec![coordinate.clone()]), + ), + ( + Value::Text("args".into()), + Value::Array(vec![bytes.clone()]), + ), + ]); + Ok(proven(end, start, facts, types)? && proven(&length, end, facts, types)?) +} + +fn supports( + fact: &Value, + left: &[u8], + right: &[u8], + types: &mut Types<'_>, + depth: usize, +) -> Check { + types.step(depth)?; + match string(get(fact, "kind")?)? { + "all" => { + for item in sequence(get(fact, "values")?)? { + if supports(item, left, right, types, depth + 1)? { + return Ok(true); + } + } + Ok(false) + } + "compare" => { + let a = key(get(fact, "left")?, types)?; + let b = key(get(fact, "right")?, types)?; + Ok(match string(get(fact, "op")?)? { + ">=" | ">" => a == left && b == right, + "<=" | "<" => a == right && b == left, + "==" => (a == left && b == right) || (a == right && b == left), + _ => false, + }) + } + _ => Ok(false), + } +} + +/// Terms compare by canonical encoding, independent of in-memory map order. +fn key(value: &Value, types: &mut Types<'_>) -> Check> { + let bytes = echo_edict_canonical::encode_canonical_cbor_v1(value).map_err(|_| ())?; + types.proof_work(bytes.len())?; + Ok(bytes) +} + +fn constant(value: &Value) -> Option { + if string(get(value, "kind").ok()?).ok()? != "const" { + return None; + } + let literal = get(value, "value").ok()?; + if string(get(literal, "kind").ok()?).ok()? != "int" { + return None; + } + unsigned(get(literal, "value").ok()?).ok() +} 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 1f16a302..4a5b0a66 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 @@ -4,18 +4,24 @@ 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. +/// addition's no-overflow proof, a subtraction's or slice's range proof, or a +/// count's full-byte scan charge. A Core without a function table still needs +/// the judgment for any of them. pub(super) fn present(core: &Value) -> Check { let mut layers = vec![get(core, "intents")?]; while !layers.is_empty() { let mut next = Vec::new(); for value in layers { if let Value::Map(entries) = value { + // Each of these needs an intent-level proof, even without a + // source-function table. if string(get(value, "kind").unwrap_or(&Value::Null)) == Ok("call") && matches!( string(get(value, "callee").unwrap_or(&Value::Null)), - Ok("core.integer.add" | "core.bytes.count") + Ok("core.integer.add" + | "core.integer.subtract" + | "core.bytes.slice" + | "core.bytes.count") ) { return Ok(true); 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 ca0a77b5..639a53a8 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,11 +48,18 @@ 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) + read_with_limits(max_steps, None, true) +} +/// Also raises the allocation ceiling when `max_allocated` is given. +fn read_helper_with_limits(max_steps: u64, max_allocated: Option) -> LoweringRequestV1 { + read_with_limits(max_steps, max_allocated, 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 { + read_with_limits(max_steps, None, helper) +} +fn read_with_limits(max_steps: u64, max_allocated: Option, 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"); @@ -158,8 +165,20 @@ fn read_with_budget(max_steps: u64, helper: bool) -> LoweringRequestV1 { field_mut(intent(artifact), "coreEvaluationBudget"), "maxSteps", ) = Value::Integer(i128::from(max_steps)); + if let Some(max_allocated) = max_allocated { + *field_mut( + field_mut(intent(artifact), "coreEvaluationBudget"), + "maxAllocatedBytes", + ) = Value::Integer(i128::from(max_allocated)); + } } - fork_adapter_budget(&mut source, &mut core, &mut target, max_steps); + fork_adapter_budget( + &mut source, + &mut core, + &mut target, + max_steps, + max_allocated, + ); source.core = bound( &coordinate, "edict.core.module/v1", @@ -229,6 +248,7 @@ fn fork_adapter_budget( core: &mut Value, target: &mut Value, max_steps: u64, + max_allocated: Option, ) { let mut adapter = decode(&source.semantic_inputs[0].artifact.artifact.bytes).expect("adapter"); let Value::Map(profiles) = field(&adapter, "operationProfiles") else { @@ -242,6 +262,12 @@ fn fork_adapter_budget( field_mut(field_mut(&mut adapter, "budgets"), &obligation), "maxSteps", ) = Value::Integer(i128::from(max_steps)); + if let Some(max_allocated) = max_allocated { + *field_mut( + field_mut(field_mut(&mut adapter, "budgets"), &obligation), + "maxAllocatedBytes", + ) = Value::Integer(i128::from(max_allocated)); + } let adapter_id = source.semantic_inputs[0] .artifact .reference @@ -594,6 +620,8 @@ mod imported_calls; #[path = "source_functions/count.rs"] mod count; +#[path = "source_functions/slice.rs"] +mod slice; #[path = "source_functions/utf8.rs"] mod utf8; diff --git a/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions/slice.rs b/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions/slice.rs new file mode 100644 index 00000000..8cc37a19 --- /dev/null +++ b/crates/echo-edict-provider-verifier/tests/bounded_read/source_functions/slice.rs @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Independently rebound read guards that slice the read fact at a runtime +//! offset, as Jim's character-boundary check does, not compiler artifacts. +use super::*; +const FACT: &str = "jedit.text@1.FactBytes"; +/// One slice and one UTF-8 scan of the 1 MiB fact, above the read baseline. +const BUDGET: u64 = 8_388_608; +/// Each reference to a 1 MiB value is charged as a full copy, so the guarded +/// boundary check needs slightly more than the fixture's 16 MiB. +const ALLOCATION: u64 = 33_554_432; +fn call(callee: &str, args: Vec) -> Value { + map([ + ("kind", text("call")), + ("callee", text(callee)), + ("typeArgs", Value::Array(vec![text(FACT)])), + ("args", Value::Array(args)), + ]) +} +fn integer(value: u64) -> Value { + map([ + ("kind", text("const")), + ( + "value", + map([ + ("kind", text("int")), + ("width", text("U64")), + ("value", Value::Integer(i128::from(value))), + ]), + ), + ]) +} +fn compare(op: &str, left: Value, right: Value) -> Value { + map([ + ("kind", text("compare")), + ("op", text(op)), + ("left", left), + ("right", right), + ]) +} +/// `at <= len(actual) && isUtf8(slice(actual, 0, at))`, with the runtime +/// offset `at = len(input.expected)`. +fn guarded(old: Value, case: &str) -> Value { + let actual = field(&old, "left").clone(); + let at = call("core.bytes.length", vec![field(&old, "right").clone()]); + let guard = compare( + "<=", + at.clone(), + call("core.bytes.length", vec![actual.clone()]), + ); + let boundary = compare( + "==", + call( + "core.bytes.isUtf8", + vec![call("core.bytes.slice", vec![actual, integer(0), at])], + ), + map([ + ("kind", text("const")), + ( + "value", + map([("kind", text("bool")), ("value", Value::Bool(true))]), + ), + ]), + ); + let children = match case { + "unguarded" => vec![old, boundary], + "guard after use" => vec![old, boundary, guard], + _ => vec![old, guard, boundary], + }; + map([("kind", text("all")), ("values", Value::Array(children))]) +} +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) -> LoweringRequestV1 { + let mut source = read_helper_with_limits(BUDGET, Some(ALLOCATION)); + 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) -> verifier::VerificationRequestV1 { + // The new guard is never submitted to the lowerer to obtain this carrier. + let mut request = request(read_helper_with_limits(BUDGET, Some(ALLOCATION))); + changed_core(&mut request, |core| edit_core(core, case)); + changed_target(&mut request, |intent| edit_target(intent, case)); + request +} +#[test] +fn bounded_read_runtime_slices_lower_behind_a_conjunct_guard() { + lower(source("valid")).expect("guarded runtime slice lowers"); +} +#[test] +fn bounded_read_runtime_slices_verify_independently() { + let response = verifier::verify(verification("valid")).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_runtime_slices_without_a_dominating_guard_refuse() { + for case in ["unguarded", "guard after use"] { + assert!(lower(source(case)).is_err(), "{case}"); + assert_rejected(verification(case)); + } +} diff --git a/crates/echo-edict-provider-verifier/tests/pure_relation/mod.rs b/crates/echo-edict-provider-verifier/tests/pure_relation/mod.rs index b7d8709d..3adae39f 100644 --- a/crates/echo-edict-provider-verifier/tests/pure_relation/mod.rs +++ b/crates/echo-edict-provider-verifier/tests/pure_relation/mod.rs @@ -255,3 +255,149 @@ fn assert_projection_mutation_refused(mutate: impl FnOnce(&mut CanonicalValueV1) } } } + +/// Jim's compiler-produced leaf slice: a runtime slice proven only by its two +/// input constraints, `startByte <= endByte` and `endByte <= len(blobBytes)`. +fn slice_leaf_fixture() -> (FixtureNames<'static>, RawFixture, Vec) { + let (pure, base, _) = compiler_fixture(); + let names = FixtureNames { + intent: "sliceLeaf", + ..pure + }; + let hex = include_str!( + "../../../warp-core/tests/fixtures/edict-byte-slice/executable-operation-package.cbor.hex" + ) + .trim(); + let package: Vec = (0..hex.len()) + .step_by(2) + .map(|index| u8::from_str_radix(&hex[index..index + 2], 16).expect("retained hex")) + .collect(); + let decoded = decode_canonical_cbor_v1(&package).expect("retained package"); + let program = + decode_canonical_cbor_v1(&bytes_field(&decoded, "program")).expect("retained program"); + let fixture = RawFixture { + core: bytes_field(&program, "core_artifact"), + target_ir: bytes_field(&program, "target_ir_artifact"), + exports: bytes_field(&program, "lawpack_exports_artifact"), + result_projection: bytes_field(&program, "result_projection_artifact"), + source: canonical_bytes(&CanonicalValueV1::Bytes( + include_bytes!("../../../warp-core/tests/fixtures/edict-byte-slice/LeafSlice.edict") + .to_vec(), + )), + ..base + }; + (names, fixture, package) +} + +/// Edits both intents, then rebinds Target's source Core reference. +fn edited_slice_leaf(edit: impl Fn(&mut CanonicalValueV1)) -> (FixtureNames<'static>, RawFixture) { + let (names, mut fixture, _) = slice_leaf_fixture(); + let mut core = decode_canonical_cbor_v1(&fixture.core).expect("Core"); + let mut target = decode_canonical_cbor_v1(&fixture.target_ir).expect("Target"); + edit(map_field_mut( + map_field_mut(&mut core, "intents"), + "sliceLeaf", + )); + edit(map_field_mut( + map_field_mut(&mut target, "intents"), + "sliceLeaf", + )); + fixture.core = canonical_bytes(&core); + let core_reference = raw_ref(names.application, "edict.core.module/v1", &fixture.core); + *map_field_mut(map_field_mut(&mut target, "semanticClosure"), "sourceCore") = map([ + ("id", text(names.application)), + ( + "digest", + CanonicalValueV1::Array(vec![ + text("sha256"), + CanonicalValueV1::Bytes(core_reference.digest), + ]), + ), + ]); + fixture.target_ir = canonical_bytes(&target); + (names, fixture) +} + +/// Echo's worst-case charge for this program is a slice of the whole 1 MiB +/// operand plus input validation, slightly above the 1 MiB step budget the +/// retained package declares. These tests grant 2 MiB. +fn with_step_budget(intent: &mut CanonicalValueV1) { + *map_field_mut(map_field_mut(intent, "coreEvaluationBudget"), "maxSteps") = + CanonicalValueV1::Integer(2_097_152); +} + +#[test] +fn compiler_produced_runtime_slice_is_proven_by_its_input_constraints() { + let (names, fixture) = edited_slice_leaf(with_step_budget); + let package = lower_package(names, &fixture); + let accepted = verifier::verify(verification_request(names, &fixture, package)) + .expect("valid compiler relation"); + let report = decode_canonical_cbor_v1(&accepted.outputs[0].artifact.bytes).expect("report"); + assert_eq!(text_field(&report, "outcome"), Some("accepted")); +} + +#[test] +fn compiler_produced_runtime_slice_without_its_length_constraint_is_refused() { + let (names, fixture) = edited_slice_leaf(|intent| { + with_step_budget(intent); + let CanonicalValueV1::Array(constraints) = map_field_mut(intent, "inputConstraints") else { + panic!("input constraints") + }; + assert_eq!(constraints.len(), 2); + constraints.truncate(1); + }); + assert!( + lowerer::lower(lowering_request(names, &fixture)).is_err(), + "the lowerer must refuse an unproven runtime slice" + ); + // Rebind the accepted package's carriers to the unconstrained Core and + // Target without asking the lowerer to endorse them. + let (_, proven) = edited_slice_leaf(with_step_budget); + let package = decode_canonical_cbor_v1(&lower_package(names, &proven)).expect("package"); + // Control: the same rebinding of the constrained program is accepted. + let control = rebound_package(package.clone(), names, &proven); + let accepted = verifier::verify(verification_request(names, &proven, control)) + .expect("rebound control relation"); + let report = decode_canonical_cbor_v1(&accepted.outputs[0].artifact.bytes).expect("report"); + assert_eq!(text_field(&report, "outcome"), Some("accepted")); + let package = rebound_package(package, names, &fixture); + let refused = verifier::verify(verification_request(names, &fixture, package)); + assert!( + !refused.is_ok_and(|success| { + let report = + decode_canonical_cbor_v1(&success.outputs[0].artifact.bytes).expect("report"); + text_field(&report, "outcome") == Some("accepted") + }), + "the verifier must independently refuse an unproven runtime slice" + ); +} + +fn rebound_package( + mut package: CanonicalValueV1, + names: FixtureNames<'_>, + fixture: &RawFixture, +) -> Vec { + let CanonicalValueV1::Bytes(bytes) = map_field(&package, "program") else { + panic!("program") + }; + let mut program = decode_canonical_cbor_v1(bytes).expect("program"); + for (name, bytes) in [ + ("core_artifact", &fixture.core), + ("target_ir_artifact", &fixture.target_ir), + ] { + *map_field_mut(&mut program, name) = CanonicalValueV1::Bytes(bytes.clone()); + } + *map_field_mut(&mut package, "program") = CanonicalValueV1::Bytes(canonical_bytes(&program)); + let core = raw_ref(names.application, "edict.core.module/v1", &fixture.core).digest; + let target = raw_ref( + "echo.span-ir/v1", + "edict.target-ir.artifact/v1", + &fixture.target_ir, + ) + .digest; + let closure = map_field_mut(&mut package, "semantic_closure"); + *map_field_mut(closure, "canonical_meaning_identity") = CanonicalValueV1::Bytes(core.clone()); + *map_field_mut(closure, "core_identity") = CanonicalValueV1::Bytes(core); + *map_field_mut(closure, "target_ir_identity") = CanonicalValueV1::Bytes(target); + canonical_bytes(&package) +} 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 d093baa9..f51e0ed4 100644 --- a/crates/echo-edict-provider-verifier/tests/source_functions/mod.rs +++ b/crates/echo-edict-provider-verifier/tests/source_functions/mod.rs @@ -2,6 +2,7 @@ // © James Ross Ω FLYING•ROBOTS //! Deliberately rebound native-provider tests, not compiler acceptance evidence. use super::*; +mod proven_ranges; mod unsigned_addition; fn fixture_with_functions( diff --git a/crates/echo-edict-provider-verifier/tests/source_functions/proven_ranges.rs b/crates/echo-edict-provider-verifier/tests/source_functions/proven_ranges.rs new file mode 100644 index 00000000..77e5c33b --- /dev/null +++ b/crates/echo-edict-provider-verifier/tests/source_functions/proven_ranges.rs @@ -0,0 +1,248 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Rebound native judgments of runtime slice and subtraction operands under +//! Edict's proven-range rules, not compiler acceptance evidence. +//! +//! A slice needs `start <= end <= len(bytes)` and a subtraction needs +//! `right <= left`, each from a dominating fact: equal terms, a zero right +//! side, ordered constants, an input constraint, or an earlier conjunct of +//! the same `all`. Conditional predicates, negations and later conjuncts +//! prove nothing. +use super::*; + +const BYTES: &str = "Bytes"; + +fn typed(name: &str, types: &[&str], args: Vec) -> CanonicalValueV1 { + let mut value = call(name, args); + *map_field_mut(&mut value, "typeArgs") = list(types.iter().map(|ty| text(*ty)).collect()); + value +} +fn length(bytes: CanonicalValueV1) -> CanonicalValueV1 { + typed("core.bytes.length", &[BYTES], vec![bytes]) +} +fn slice( + bytes: CanonicalValueV1, + start: CanonicalValueV1, + end: CanonicalValueV1, +) -> CanonicalValueV1 { + typed("core.bytes.slice", &[BYTES], vec![bytes, start, end]) +} +fn utf8(bytes: CanonicalValueV1) -> CanonicalValueV1 { + typed("core.bytes.isUtf8", &[BYTES], vec![bytes]) +} +fn subtract(left: CanonicalValueV1, right: CanonicalValueV1) -> CanonicalValueV1 { + typed("core.integer.subtract", &["U64"], vec![left, right]) +} +fn truth() -> CanonicalValueV1 { + map([ + ("kind", text("const")), + ( + "value", + map([ + ("kind", text("bool")), + ("value", CanonicalValueV1::Bool(true)), + ]), + ), + ]) +} +fn compare(op: &str, left: CanonicalValueV1, right: CanonicalValueV1) -> CanonicalValueV1 { + map([ + ("kind", text("compare")), + ("op", text(op)), + ("left", left), + ("right", right), + ]) +} +fn all(values: Vec) -> CanonicalValueV1 { + map([("kind", text("all")), ("values", list(values))]) +} +fn not(value: CanonicalValueV1) -> CanonicalValueV1 { + map([("kind", text("not")), ("value", value)]) +} +fn choose( + predicate: CanonicalValueV1, + then: CanonicalValueV1, + otherwise: CanonicalValueV1, +) -> CanonicalValueV1 { + map([ + ("kind", text("if")), + ("predicate", predicate), + ("then", then), + ("else", otherwise), + ]) +} +fn flag(predicate: CanonicalValueV1) -> CanonicalValueV1 { + choose(predicate, literal("U32", 1), literal("U32", 0)) +} + +fn probe(case: &str) -> CanonicalValueV1 { + let bytes_local = local("arg.0", BYTES); + let other_local = local("arg.1", BYTES); + let at_local = local("arg.2", "U64"); + let elsewhere_local = local("arg.3", "U64"); + let bytes = reference(&bytes_local); + let other = reference(&other_local); + let at = reference(&at_local); + let elsewhere = reference(&elsewhere_local); + let prefix = |bytes: CanonicalValueV1| compare("<=", at.clone(), length(bytes)); + let use_prefix = || { + compare( + "==", + utf8(slice(bytes.clone(), literal("U64", 0), at.clone())), + truth(), + ) + }; + let result = match case { + "guarded prefix" => flag(all(vec![prefix(bytes.clone()), use_prefix()])), + "zero offsets" => flag(compare( + "==", + utf8(slice(bytes.clone(), literal("U64", 0), literal("U64", 0))), + truth(), + )), + "end offset" => flag(compare( + "==", + utf8(slice( + bytes.clone(), + literal("U64", 0), + length(bytes.clone()), + )), + truth(), + )), + "guarded suffix" => flag(all(vec![ + prefix(bytes.clone()), + compare( + "==", + utf8(slice(bytes.clone(), at.clone(), length(bytes.clone()))), + truth(), + ), + ])), + "unguarded" => flag(use_prefix()), + "guard after use" => flag(all(vec![use_prefix(), prefix(bytes.clone())])), + "guard on another operand" => flag(all(vec![prefix(other), use_prefix()])), + "guard on another offset" => flag(all(vec![ + compare("<=", elsewhere, length(bytes.clone())), + use_prefix(), + ])), + "guard by declared capacity" => flag(all(vec![ + compare("<=", at.clone(), literal("U64", 32)), + use_prefix(), + ])), + "disjunctive guard" => flag(all(vec![ + not(all(vec![ + not(prefix(bytes.clone())), + not(prefix(bytes.clone())), + ])), + use_prefix(), + ])), + "guard in a conditional" => { + choose(prefix(bytes.clone()), flag(use_prefix()), literal("U32", 0)) + } + "guard in a sibling branch" => { + choose(prefix(bytes.clone()), literal("U32", 0), flag(use_prefix())) + } + "guarded subtraction" => flag(all(vec![ + compare("<=", elsewhere.clone(), at.clone()), + compare("<=", subtract(at.clone(), elsewhere), literal("U64", 10)), + ])), + "unguarded subtraction" => flag(compare( + "<=", + subtract(at.clone(), elsewhere), + literal("U64", 10), + )), + "reversed subtraction guard" => flag(all(vec![ + compare("<=", at.clone(), elsewhere.clone()), + compare("<=", subtract(at.clone(), elsewhere), literal("U64", 10)), + ])), + _ => panic!("case {case}"), + }; + function( + vec![bytes_local, other_local, at_local, elsewhere_local], + "U32", + vec![], + vec![], + result, + ) +} +fn probe_fixture(case: &str) -> (FixtureNames<'static>, RawFixture, Vec) { + called_fixture(|core, _| add_field(map_field_mut(core, "functions"), "probe", probe(case))) +} + +#[test] +fn dominating_range_facts_admit_runtime_slices_and_subtractions_in_both_judgments() { + for case in [ + "guarded prefix", + "zero offsets", + "end offset", + "guarded suffix", + "guarded subtraction", + ] { + let (names, fixture, package) = probe_fixture(case); + let lowered = lowerer::lower(lowering_request(names, &fixture)) + .unwrap_or_else(|_| panic!("{case} lowers")); + assert_eq!(lowered.outputs[0].artifact.bytes, package, "{case}"); + assert!( + verifier_accepts(names, &fixture, package), + "{case}: verifier refused an independently proven range" + ); + } +} + +#[test] +fn missing_or_non_dominating_range_facts_refuse_in_both_judgments() { + for case in [ + "unguarded", + "guard after use", + "guard on another operand", + "guard on another offset", + "guard by declared capacity", + "disjunctive guard", + "guard in a conditional", + "guard in a sibling branch", + "unguarded subtraction", + "reversed subtraction guard", + ] { + let (names, fixture, package) = probe_fixture(case); + both_refuse(names, &fixture, package, case); + } +} + +/// `endByte - startByte` in the intent body, proven by the fixture's own +/// input constraint `startByte <= endByte` when it is kept. +fn width_fixture(constrained: bool) -> (FixtureNames<'static>, RawFixture, Vec) { + called_fixture(|core, target| { + let CanonicalValueV1::Array(constraints) = map_field(intent(core), "inputConstraints") + else { + panic!("constraints") + }; + let predicate = map_field(&constraints[0], "predicate").clone(); + let start = map_field(&predicate, "left").clone(); + let end = map_field(&predicate, "right").clone(); + let kept = if constrained { + constraints.clone() + } else { + vec![] + }; + for (artifact, key) in [(&mut *core, "nodes"), (&mut *target, "pureBindings")] { + *map_field_mut(intent(artifact), "inputConstraints") = list(kept.clone()); + let body = if key == "nodes" { + map_field_mut(intent(artifact), "body") + } else { + intent(artifact) + }; + let CanonicalValueV1::Array(bindings) = map_field_mut(body, key) else { + panic!("bindings") + }; + *map_field_mut(&mut bindings[0], "value") = subtract(end.clone(), start.clone()); + } + }) +} + +#[test] +fn input_constraints_prove_intent_subtraction_in_both_judgments() { + let (names, fixture, package) = width_fixture(true); + let lowered = lowerer::lower(lowering_request(names, &fixture)).expect("proven width lowers"); + assert_eq!(lowered.outputs[0].artifact.bytes, package); + assert!(verifier_accepts(names, &fixture, package)); + let (names, fixture, package) = width_fixture(false); + both_refuse(names, &fixture, package, "unconstrained width"); +} 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 fb26b41a..f40a4305 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 d8a88bd2..5715c5c7 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 c6e6dd4a..8aae8e29 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:8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8" + "digest": "sha256:e82a973ba7b0031a75958e3fa01480e2aeeaad1989a914214232896f3d7a246f" }, "artifacts": [ { @@ -87,13 +87,13 @@ "artifactKind": "lowerer", "resource": { "coordinate": "echo.dpo.lowerer/component@1", - "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587" + "digest": "sha256:b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b" }, "source": { "kind": "component", "component": { "coordinate": "echo.dpo.lowerer/component@1", - "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587" + "digest": "sha256:b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b" } } }, @@ -178,13 +178,13 @@ "artifactKind": "verifier", "resource": { "coordinate": "echo.dpo.verifier/component@1", - "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e" + "digest": "sha256:e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced" }, "source": { "kind": "component", "component": { "coordinate": "echo.dpo.verifier/component@1", - "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e" + "digest": "sha256:e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced" } } } diff --git a/crates/echo-wesley-gen/tests/provider_package.rs b/crates/echo-wesley-gen/tests/provider_package.rs index 07fdfc7e..c982a9fa 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 = - "8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8"; + "e82a973ba7b0031a75958e3fa01480e2aeeaad1989a914214232896f3d7a246f"; 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 8a2e8fa1..2bc7ec99 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:8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8"; + "sha256:e82a973ba7b0031a75958e3fa01480e2aeeaad1989a914214232896f3d7a246f"; const EXPECTED_MANIFEST_RAW_SHA256: &str = - "704b673fbf0186a7ffd3313d89930fa4a72b47a05bade0e93c3419297098cbe7"; + "15b370fd6c56adc59d1e189dee0c7e213db05a58279d630eed013a54de112b6d"; const PACKAGE_PATHS: [&str; 25] = [ "components/lowerer.echo-dpo.component.wasm", diff --git a/crates/warp-core/src/edict_pure.rs b/crates/warp-core/src/edict_pure.rs index 8b592752..dc35cee1 100644 --- a/crates/warp-core/src/edict_pure.rs +++ b/crates/warp-core/src/edict_pure.rs @@ -14,6 +14,7 @@ mod decode; pub(crate) mod evaluate; pub(crate) mod functions; pub(crate) mod model; +pub(crate) mod proven_order; pub(crate) mod syntax; pub(crate) mod values; @@ -101,3 +102,5 @@ mod predicate_tests; mod byte_count_tests; #[cfg(test)] mod byte_utf8_tests; +#[cfg(test)] +mod proven_range_tests; diff --git a/crates/warp-core/src/edict_pure/functions.rs b/crates/warp-core/src/edict_pure/functions.rs index bdc6f8ef..b4328709 100644 --- a/crates/warp-core/src/edict_pure/functions.rs +++ b/crates/warp-core/src/edict_pure/functions.rs @@ -1,6 +1,7 @@ // SPDX-License-Identifier: Apache-2.0 // © James Ross Ω FLYING•ROBOTS //! Closed source/imported helper authority, lexical scopes, and runtime apertures. +use super::proven_order::{length_of, proven}; use super::{ model::{ Binding, Expr, Helper, Parameter, Predicate, RuntimeType, MAX_DEPTH, MAX_PROGRAM_NODES, @@ -142,7 +143,10 @@ pub(crate) fn decode( let actual = infer( value, &scope, - &caps, + Proof { + caps: &caps, + facts: &[], + }, &definitions, definition.source_owned, parser, @@ -172,7 +176,10 @@ pub(crate) fn decode( let actual = infer( result, &scope, - &caps, + Proof { + caps: &caps, + facts: &[], + }, &definitions, definition.source_owned, parser, @@ -211,7 +218,18 @@ pub(crate) fn decode( 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, &caps, &definitions, true, parser, 0)?; + infer( + basis, + &scope, + Proof { + caps: &caps, + facts: &[], + }, + &definitions, + true, + parser, + 0, + )?; basis_roots.push(parser.expr(basis, 0)?); } } @@ -262,14 +280,21 @@ fn join(left: RuntimeType, right: RuntimeType) -> Result { } type Scope<'a> = BTreeMap<&'a str, &'a Value>; +/// What is proven at one evaluation point: carried binding caps and the +/// dominating order facts (earlier conjuncts of enclosing `all`s). +#[derive(Clone, Copy)] +struct Proof<'c, 'v> { + caps: &'c Caps<'c>, + facts: &'c [&'v 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, +fn infer<'v>( + value: &'v Value, scope: &Scope<'_>, - caps: &Caps<'_>, + proof: Proof<'_, 'v>, definitions: &BTreeMap>, source: bool, parser: &mut Parser<'_>, @@ -309,7 +334,7 @@ fn infer( let RuntimeType::Record(fields) = infer( field(value, "base")?, scope, - caps, + proof, definitions, source, parser, @@ -335,7 +360,7 @@ fn infer( infer( expression, scope, - caps, + proof, definitions, source, parser, @@ -351,7 +376,7 @@ fn infer( check_predicate( field(value, "predicate")?, scope, - caps, + proof, definitions, source, parser, @@ -360,7 +385,7 @@ fn infer( let left = infer( field(value, "then")?, scope, - caps, + proof, definitions, source, parser, @@ -369,7 +394,7 @@ fn infer( let right = infer( field(value, "else")?, scope, - caps, + proof, definitions, source, parser, @@ -393,7 +418,7 @@ fn infer( let actual = infer( argument, scope, - caps, + proof, definitions, source, parser, @@ -411,7 +436,15 @@ fn infer( return Err(Error::UnsupportedProgram); }; super::syntax::count_needle(needle)?; - let actual = infer(operand, scope, caps, definitions, source, parser, depth + 1)?; + let actual = infer( + operand, + scope, + proof, + definitions, + source, + parser, + depth + 1, + )?; let expected = parser.ty(text(coordinate)?, depth + 1)?; if !matches!(expected, RuntimeType::Bytes { .. }) || expected != actual { return Err(Error::UnsupportedProgram); @@ -424,7 +457,7 @@ fn infer( infer( argument, scope, - caps, + proof, definitions, source, parser, @@ -464,38 +497,45 @@ fn infer( ("core.integer.add", [left, right], [expected @ RuntimeType::Unsigned(max)]) if left == expected && right == expected => { - let left = unsigned_ceiling(&arguments[0], *max, caps, parser, depth + 1)?; - let right = unsigned_ceiling(&arguments[1], *max, caps, parser, depth + 1)?; + let left = + unsigned_ceiling(&arguments[0], *max, proof.caps, parser, depth + 1)?; + let right = + unsigned_ceiling(&arguments[1], *max, proof.caps, parser, depth + 1)?; if left.checked_add(right).is_none_or(|sum| sum > *max) { return Err(Error::UnsupportedProgram); } Ok(expected.clone()) } - // No caller where proof crosses a fresh frame. This target's - // first source-function subset proves partial intrinsics only - // from literal offsets/operands, refusing all other cases. + // Partial intrinsics need a dominating order proof. A helper frame + // starts with no caller facts; only its own conjunct prefixes count. ("core.integer.subtract", [left, right], [expected @ RuntimeType::Unsigned(_)]) if accepts(expected, left) && accepts(expected, right) => { - let left = unsigned_literal(&arguments[0])?; - let right = unsigned_literal(&arguments[1])?; - left.checked_sub(right).ok_or(Error::UnsupportedProgram)?; + if !proven(&arguments[0], &arguments[1], proof.facts, parser, depth + 1)? { + return Err(Error::UnsupportedProgram); + } Ok(expected.clone()) } ( "core.bytes.slice", [actual, RuntimeType::Unsigned(a), RuntimeType::Unsigned(b)], - [expected @ RuntimeType::Bytes { min, .. }], + [expected @ RuntimeType::Bytes { min, max }], ) if *a == u64::MAX && *b == u64::MAX && accepts(expected, actual) => { - let start = unsigned_literal(&arguments[1])?; - let end = unsigned_literal(&arguments[2])?; - if start > end || end > *min { + // Literal offsets within the guaranteed minimum length need no + // fact; any other offsets need start <= end <= len(bytes). + let literal = matches!( + (unsigned_literal(&arguments[1]), unsigned_literal(&arguments[2])), + (Ok(start), Ok(end)) if start <= end && end <= *min + ); + let length = length_of(&types[0], &arguments[0]); + if !literal + && (!proven(&arguments[2], &arguments[1], proof.facts, parser, depth + 1)? + || !proven(&length, &arguments[2], proof.facts, parser, depth + 1)?) + { return Err(Error::UnsupportedProgram); } - Ok(RuntimeType::Bytes { - min: 0, - max: end - start, - }) + // As in Edict, a slice keeps its operand's maximum and no minimum. + Ok(RuntimeType::Bytes { min: 0, max: *max }) } _ => Err(Error::UnsupportedProgram), } @@ -549,10 +589,10 @@ fn unsigned_literal(value: &Value) -> Result { } number(field(field(value, "value")?, "value")?) } -fn check_predicate( - value: &Value, +fn check_predicate<'v>( + value: &'v Value, scope: &Scope<'_>, - caps: &Caps<'_>, + proof: Proof<'_, 'v>, definitions: &BTreeMap>, source: bool, parser: &mut Parser<'_>, @@ -566,8 +606,22 @@ fn check_predicate( if values.is_empty() { return Err(Error::InvalidArtifact); } + // Each conjunct is proven only by the conjuncts before it. + let mut prefix = proof.facts.to_vec(); for value in values { - check_predicate(value, scope, caps, definitions, source, parser, depth + 1)?; + check_predicate( + value, + scope, + Proof { + caps: proof.caps, + facts: &prefix, + }, + definitions, + source, + parser, + depth + 1, + )?; + prefix.push(value); } return Ok(()); } @@ -576,7 +630,7 @@ fn check_predicate( return check_predicate( field(value, "value")?, scope, - caps, + proof, definitions, source, parser, @@ -590,7 +644,7 @@ fn check_predicate( let left = infer( field(value, "left")?, scope, - caps, + proof, definitions, source, parser, @@ -599,7 +653,7 @@ fn check_predicate( let right = infer( field(value, "right")?, scope, - caps, + proof, definitions, source, parser, @@ -836,7 +890,10 @@ mod predicate_validation_tests { check_predicate( wire, &BTreeMap::new(), - &BTreeMap::new(), + Proof { + caps: &BTreeMap::new(), + facts: &[], + }, &BTreeMap::new(), true, &mut parser, @@ -905,7 +962,10 @@ mod predicate_validation_tests { let result = infer( &call, &scope, - &BTreeMap::new(), + Proof { + caps: &BTreeMap::new(), + facts: &[], + }, &BTreeMap::new(), true, &mut parser, @@ -961,7 +1021,10 @@ mod predicate_validation_tests { let result = infer( &call, &BTreeMap::from([("arg.0", &local)]), - &BTreeMap::new(), + Proof { + caps: &BTreeMap::new(), + facts: &[], + }, &BTreeMap::new(), true, &mut parser, diff --git a/crates/warp-core/src/edict_pure/proven_order.rs b/crates/warp-core/src/edict_pure/proven_order.rs new file mode 100644 index 00000000..70033eb8 --- /dev/null +++ b/crates/warp-core/src/edict_pure/proven_order.rs @@ -0,0 +1,110 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Echo-owned order proofs for partial byte slicing and unsigned subtraction. +//! +//! `left >= right` holds for equal terms, a zero right side, ordered +//! constants, or a dominating fact: an earlier conjunct of an enclosing +//! `all`, or a pure intent's input constraint. Conditional predicates, +//! negations and later conjuncts prove nothing. This follows Edict's +//! proven-range semantics without trusting any annotation in the artifact. +use echo_edict_canonical::{encode_canonical_cbor_v1, CanonicalValueV1 as Value}; + +use super::syntax::Parser; +use super::values::{array, field, number, text_field}; +use super::EvaluationError as Error; + +/// Whether `left >= right` is established at this evaluation point. +pub(crate) fn proven( + left: &Value, + right: &Value, + facts: &[&Value], + parser: &mut Parser<'_>, + depth: usize, +) -> Result { + parser.enter(depth)?; + let left_key = key(left, parser)?; + let right_key = key(right, parser)?; + if left_key == right_key || constant(right) == Some(0) { + return Ok(true); + } + if let (Some(a), Some(b)) = (constant(left), constant(right)) { + return Ok(a >= b); + } + for fact in facts { + if supports(fact, &left_key, &right_key, parser, depth + 1)? { + return Ok(true); + } + } + Ok(false) +} + +/// The Core term `core.bytes.length(bytes)`, for slice end proofs. +pub(crate) fn length_of(coordinate: &Value, bytes: &Value) -> Value { + Value::Map(vec![ + (Value::Text("kind".into()), Value::Text("call".into())), + ( + Value::Text("callee".into()), + Value::Text("core.bytes.length".into()), + ), + ( + Value::Text("typeArgs".into()), + Value::Array(vec![coordinate.clone()]), + ), + ( + Value::Text("args".into()), + Value::Array(vec![bytes.clone()]), + ), + ]) +} + +fn supports( + fact: &Value, + left: &[u8], + right: &[u8], + parser: &mut Parser<'_>, + depth: usize, +) -> Result { + parser.enter(depth)?; + match text_field(fact, "kind")? { + "all" => { + for item in array(field(fact, "values")?)? { + if supports(item, left, right, parser, depth + 1)? { + return Ok(true); + } + } + Ok(false) + } + "compare" => { + let a = key(field(fact, "left")?, parser)?; + let b = key(field(fact, "right")?, parser)?; + Ok(match text_field(fact, "op")? { + ">=" | ">" => a == left && b == right, + "<=" | "<" => a == right && b == left, + "==" => (a == left && b == right) || (a == right && b == left), + _ => false, + }) + } + _ => Ok(false), + } +} + +/// Terms compare by canonical encoding, independent of in-memory map order. +fn key(value: &Value, parser: &mut Parser<'_>) -> Result, Error> { + let bytes = encode_canonical_cbor_v1(value).map_err(|_| Error::InvalidArtifact)?; + parser.remaining = parser + .remaining + .checked_sub(bytes.len()) + .ok_or(Error::UnsupportedProgram)?; + Ok(bytes) +} + +fn constant(value: &Value) -> Option { + if text_field(value, "kind").ok()? != "const" { + return None; + } + let literal = field(value, "value").ok()?; + if text_field(literal, "kind").ok()? != "int" { + return None; + } + number(field(literal, "value").ok()?).ok() +} diff --git a/crates/warp-core/src/edict_pure/proven_range_tests.rs b/crates/warp-core/src/edict_pure/proven_range_tests.rs new file mode 100644 index 00000000..bf5c76e2 --- /dev/null +++ b/crates/warp-core/src/edict_pure/proven_range_tests.rs @@ -0,0 +1,316 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Runtime slice and subtraction operands under Edict's proven-range rules. +//! +//! A slice needs `start <= end <= len(bytes)` and a subtraction needs +//! `right <= left`, each from a dominating fact: equal terms, a zero right +//! side, ordered constants, or an earlier conjunct of the same `all`. +//! Conditional predicates, negations and later conjuncts prove nothing. +use super::{ + evaluate::{expression, Meter}, + functions::decode, + model::{Helper, MAX_PROGRAM_NODES}, + syntax::Parser, + EvaluationError as Error, EvaluationLimits, +}; +use echo_edict_canonical::CanonicalValueV1 as Value; +use std::collections::BTreeMap; + +const BYTES: &str = "Bytes"; +const MODULE: &str = "range.example@1"; + +fn map(fields: impl IntoIterator) -> 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 constant(kind: &str, width: Option<&str>, value: Value) -> Value { + let mut literal = vec![("kind", text(kind)), ("value", value)]; + if let Some(width) = width { + literal.push(("width", text(width))); + } + map([("kind", text("const")), ("value", map(literal))]) +} +fn word(value: u64) -> Value { + constant("int", Some("U64"), Value::Integer(i128::from(value))) +} +fn small(value: u32) -> Value { + constant("int", Some("U32"), Value::Integer(i128::from(value))) +} +fn truth() -> Value { + constant("bool", None, Value::Bool(true)) +} +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 { + map([ + ("kind", text("call")), + ("callee", text(callee)), + ( + "typeArgs", + Value::Array(types.iter().map(|ty| text(ty)).collect()), + ), + ("args", Value::Array(args)), + ]) +} +fn length(bytes: Value) -> Value { + call("core.bytes.length", &[BYTES], vec![bytes]) +} +fn slice(bytes: Value, start: Value, end: Value) -> Value { + call("core.bytes.slice", &[BYTES], vec![bytes, start, end]) +} +fn utf8(bytes: Value) -> Value { + call("core.bytes.isUtf8", &[BYTES], vec![bytes]) +} +fn subtract(left: Value, right: Value) -> Value { + call("core.integer.subtract", &["U64"], vec![left, right]) +} +fn compare(op: &str, left: Value, right: Value) -> Value { + map([ + ("kind", text("compare")), + ("op", text(op)), + ("left", left), + ("right", right), + ]) +} +fn all(values: Vec) -> Value { + map([("kind", text("all")), ("values", Value::Array(values))]) +} +fn not(value: Value) -> Value { + map([("kind", text("not")), ("value", value)]) +} +fn choose(predicate: Value, then: Value, otherwise: Value) -> Value { + map([ + ("kind", text("if")), + ("predicate", predicate), + ("then", then), + ("else", otherwise), + ]) +} +/// `1u32` when the predicate holds, else `0u32`. +fn flag(predicate: Value) -> Value { + choose(predicate, small(1), small(0)) +} +fn function(params: &[Value], result: Value) -> Value { + map([ + ("params", Value::Array(params.to_vec())), + ("returnType", text("U32")), + ( + "body", + map([ + ("locals", Value::Array(vec![])), + ("bindings", Value::Array(vec![])), + ("result", result), + ]), + ), + ]) +} +fn helpers(definition: Value) -> Result, Error> { + let core = map([ + ("functions", map([("probe", definition)])), + ("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: MODULE, + remaining: MAX_PROGRAM_NODES, + }; + decode(&core, &exports, &mut parser) +} + +struct Locals { + bytes: Value, + other: Value, + at: Value, + elsewhere: Value, +} +fn locals() -> Locals { + Locals { + bytes: local("arg.0", BYTES), + other: local("arg.1", BYTES), + at: local("arg.2", "U64"), + elsewhere: local("arg.3", "U64"), + } +} +fn params(locals: &Locals) -> Vec { + vec![ + locals.bytes.clone(), + locals.other.clone(), + locals.at.clone(), + locals.elsewhere.clone(), + ] +} +/// Jim's character-boundary test, `at <= len(bytes) && isUtf8(slice(bytes, 0, at))`. +fn boundary(l: &Locals) -> Value { + let bytes = reference(&l.bytes); + let at = reference(&l.at); + flag(all(vec![ + compare("<=", at.clone(), length(bytes.clone())), + compare("==", utf8(slice(bytes, word(0), at)), truth()), + ])) +} + +fn case(name: &str) -> Result { + let l = locals(); + let bytes = reference(&l.bytes); + let other = reference(&l.other); + let at = reference(&l.at); + let elsewhere = reference(&l.elsewhere); + let prefix = |bytes: Value| compare("<=", at.clone(), length(bytes)); + let use_prefix = || { + compare( + "==", + utf8(slice(bytes.clone(), word(0), at.clone())), + truth(), + ) + }; + let result = match name { + "guarded prefix" => boundary(&l), + "zero offsets" => flag(compare( + "==", + utf8(slice(bytes.clone(), word(0), word(0))), + truth(), + )), + "end offset" => flag(compare( + "==", + utf8(slice(bytes.clone(), word(0), length(bytes.clone()))), + truth(), + )), + "guarded suffix" => flag(all(vec![ + prefix(bytes.clone()), + compare( + "==", + utf8(slice(bytes.clone(), at.clone(), length(bytes.clone()))), + truth(), + ), + ])), + "unguarded" => flag(use_prefix()), + "guard after use" => flag(all(vec![use_prefix(), prefix(bytes.clone())])), + "guard on another operand" => flag(all(vec![prefix(other), use_prefix()])), + "guard on another offset" => flag(all(vec![ + compare("<=", elsewhere, length(bytes.clone())), + use_prefix(), + ])), + "guard by declared capacity" => { + flag(all(vec![compare("<=", at.clone(), word(32)), use_prefix()])) + } + "disjunctive guard" => flag(all(vec![ + not(all(vec![ + not(prefix(bytes.clone())), + not(prefix(bytes.clone())), + ])), + use_prefix(), + ])), + "guard in a conditional" => choose(prefix(bytes.clone()), flag(use_prefix()), small(0)), + "guard in a sibling branch" => choose(prefix(bytes.clone()), small(0), flag(use_prefix())), + "guarded subtraction" => flag(all(vec![ + compare("<=", elsewhere.clone(), at.clone()), + compare("<=", subtract(at, elsewhere), word(10)), + ])), + "unguarded subtraction" => flag(compare("<=", subtract(at, elsewhere), word(10))), + "reversed subtraction guard" => flag(all(vec![ + compare("<=", at.clone(), elsewhere.clone()), + compare("<=", subtract(at, elsewhere), word(10)), + ])), + "literal subtraction" => flag(compare("<=", subtract(word(7), word(3)), word(10))), + "underflowing literal subtraction" => { + flag(compare("<=", subtract(word(3), word(7)), word(10))) + } + _ => return Err(Error::InvalidArtifact), + }; + Ok(function(¶ms(&l), result)) +} + +#[test] +fn dominating_range_facts_admit_runtime_slices_and_subtractions() -> Result<(), Error> { + for name in [ + "guarded prefix", + "zero offsets", + "end offset", + "guarded suffix", + "guarded subtraction", + "literal subtraction", + ] { + assert!(helpers(case(name)?).is_ok(), "{name} must be admitted"); + } + Ok(()) +} + +#[test] +fn missing_or_non_dominating_range_facts_refuse() -> Result<(), Error> { + for name in [ + "unguarded", + "guard after use", + "guard on another operand", + "guard on another offset", + "guard by declared capacity", + "disjunctive guard", + "guard in a conditional", + "guard in a sibling branch", + "unguarded subtraction", + "reversed subtraction guard", + "underflowing literal subtraction", + ] { + assert_eq!( + helpers(case(name)?).map(|_| ()), + Err(Error::UnsupportedProgram), + "{name} must be refused before execution" + ); + } + Ok(()) +} + +fn run(helpers: &BTreeMap, bytes: &[u8], at: u64) -> Result { + let call = super::model::Expr::Call( + format!("{MODULE}.probe"), + vec![ + super::model::Expr::Constant(Value::Bytes(bytes.to_vec())), + super::model::Expr::Constant(Value::Bytes(vec![])), + super::model::Expr::Constant(Value::Integer(i128::from(at))), + super::model::Expr::Constant(Value::Integer(0)), + ], + ); + let mut meter = Meter::new(EvaluationLimits { + max_package_bytes: 1024, + max_input_bytes: 1024, + max_output_bytes: 1024, + max_steps: 4096, + max_allocated_bytes: 16_384, + }); + expression(&call, &BTreeMap::new(), helpers, &mut meter, 0) +} + +#[test] +fn an_out_of_range_offset_takes_the_authored_path_instead_of_failing() -> Result<(), Error> { + let checked = helpers(case("guarded prefix")?)?; + // "a" then U+00E9 as 0xC3 0xA9: offset 2 is inside the character. + let text = b"a\xc3\xa9"; + for (at, boundary) in [(0, 1), (1, 1), (2, 0), (3, 1), (4, 0), (u64::MAX, 0)] { + assert_eq!( + run(&checked, text, at)?, + Value::Integer(boundary), + "offset {at}" + ); + } + Ok(()) +} diff --git a/docs/topics/GeneratedRules.md b/docs/topics/GeneratedRules.md index 547c3244..fefee406 100644 --- a/docs/topics/GeneratedRules.md +++ b/docs/topics/GeneratedRules.md @@ -149,6 +149,24 @@ 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. +Partial `core.bytes.slice` and `core.integer.subtract` calls accept runtime +operands under Edict's proven-range rules. A slice needs `start <= end` and +`end <= len(bytes)` over that same operand: its actual length, not its declared +maximum. A subtraction needs `right <= left`. Each order holds for equal terms, a +zero right side, ordered constants, an input constraint, or an earlier conjunct +of the same `all`. Conditional predicates, negations, later conjuncts and +helper callers prove nothing. Literal slice offsets within the operand's +guaranteed minimum length still need no fact. The lowerer, the verifier and the +native helper checker each implement this independently, comparing terms by +canonical encoding within their work ceilings. Every slice is typed +`Bytes` with the operand's maximum and no minimum, as Edict types it. A +Core without a function table that contains either call is judged in full, +including its declared budget, as addition already was. Runtime evaluation of +`all` stops at the first false conjunct, so a guarded slice never runs out of +range: `at <= len(text) && isUtf8(slice(text, 0, at))` is false for an +out-of-range `at` and takes the authored path, while a program without the guard +is refused before installation. + 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 ff123753..379f3d7f 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 -490,344 bytes with SHA-256 -`34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587`; the -promoted verifier is 507,253 bytes with SHA-256 -`c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e`. +493,449 bytes with SHA-256 +`b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b`; the +promoted verifier is 510,251 bytes with SHA-256 +`e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced`. 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 1d0a4d27..fa2af64b 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 490,344 bytes with SHA-256 -`34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587`. +The checked component is 493,449 bytes with SHA-256 +`b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b`. 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 507,253 bytes +`wit-component` version recorded above. Its checked component is 510,251 bytes with SHA-256 -`c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e`. +`e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced`. 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 fb26b41a..f40a4305 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 d8a88bd2..5715c5c7 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 fb26b41a..f40a4305 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 d8a88bd2..5715c5c7 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 c6e6dd4a..8aae8e29 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:8653552abe36da80a0a64bb9471c529824e2298df5f2acdcc6e7fd90cf9fe5a8" + "digest": "sha256:e82a973ba7b0031a75958e3fa01480e2aeeaad1989a914214232896f3d7a246f" }, "artifacts": [ { @@ -87,13 +87,13 @@ "artifactKind": "lowerer", "resource": { "coordinate": "echo.dpo.lowerer/component@1", - "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587" + "digest": "sha256:b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b" }, "source": { "kind": "component", "component": { "coordinate": "echo.dpo.lowerer/component@1", - "digest": "sha256:34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587" + "digest": "sha256:b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b" } } }, @@ -178,13 +178,13 @@ "artifactKind": "verifier", "resource": { "coordinate": "echo.dpo.verifier/component@1", - "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e" + "digest": "sha256:e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced" }, "source": { "kind": "component", "component": { "coordinate": "echo.dpo.verifier/component@1", - "digest": "sha256:c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e" + "digest": "sha256:e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced" } } } diff --git a/xtask/src/provider_lowerer_component.rs b/xtask/src/provider_lowerer_component.rs index 89a62bdb..d8577620 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 = - "34fcf7200bb7e0c54166bd22fcb10fe166d7ca8faf444698cb59b98cda947587"; + "b52ec57c2e06a6da8ec38202885241b47483138c970376e6e11baf36bfe8014b"; 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 = - "c551e02e3ab0c144772e5d0b11b8abbfa05bc5ce34febe5359ff5026f034b53e"; + "e1426a80879d618cde4a8fe0f39a6d1986063efd8c6853a71b4f5ae1235ccced"; #[derive(Clone, Copy, Debug, Eq, PartialEq)] struct ProviderComponentSpec {