diff --git a/CHANGELOG.md b/CHANGELOG.md index 15656a1d..450c6049 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/crates/warp-core/src/edict_effects/instruction_relation.rs b/crates/warp-core/src/edict_effects/instruction_relation.rs index c14053a8..24b7dccd 100644 --- a/crates/warp-core/src/edict_effects/instruction_relation.rs +++ b/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>, helpers: BTreeMap, + /// Input constraints, which dominate the whole body. + facts: Vec<&'a Value>, + /// Proven ceilings of earlier unsigned bindings. + caps: functions::Caps<'a>, expressions: Vec, predicates: Vec, } @@ -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 { - // 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, diff --git a/crates/warp-core/src/edict_pure/functions.rs b/crates/warp-core/src/edict_pure/functions.rs index f4e9300a..380dfb2e 100644 --- a/crates/warp-core/src/edict_pure/functions.rs +++ b/crates/warp-core/src/edict_pure/functions.rs @@ -1,7 +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::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 { + 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 { @@ -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) diff --git a/crates/warp-core/src/edict_pure/proven_order.rs b/crates/warp-core/src/edict_pure/proven_order.rs index 70033eb8..c8d47c84 100644 --- a/crates/warp-core/src/edict_pure/proven_order.rs +++ b/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, 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, + 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(bytes)`, for slice end proofs. pub(crate) fn length_of(coordinate: &Value, bytes: &Value) -> Value { Value::Map(vec![ diff --git a/crates/warp-core/tests/edict_effect_package_tests.rs b/crates/warp-core/tests/edict_effect_package_tests.rs index a7242979..dc8ead61 100644 --- a/crates/warp-core/tests/edict_effect_package_tests.rs +++ b/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; diff --git a/crates/warp-core/tests/edict_effect_package_tests/proven_ranges.rs b/crates/warp-core/tests/edict_effect_package_tests/proven_ranges.rs new file mode 100644 index 00000000..8191ca76 --- /dev/null +++ b/crates/warp-core/tests/edict_effect_package_tests/proven_ranges.rs @@ -0,0 +1,472 @@ +// SPDX-License-Identifier: Apache-2.0 +// © James Ross Ω FLYING•ROBOTS +//! Effect programs carry Edict's proven-range facts: the intent's input +//! constraints dominate its whole body, and an unsigned `let` carries its +//! proven ceiling to later nodes. A `require` guard proves nothing after it. +use super::execution::{host, limits}; +use super::*; +use warp_core::edict_effects::EffectFrameError; +use warp_core::EchoOperationBudgetV1; + +const BYTES: &str = "Bytes"; + +fn int(value: u64) -> V { + map([ + ("kind", text("const")), + ( + "value", + map([ + ("kind", text("int")), + ("width", text("U64")), + ("value", V::Integer(i128::from(value))), + ]), + ), + ]) +} +fn declared(id: &str, ty: &str) -> V { + map([ + ("id", text(id)), + ("type", text(ty)), + ("alphaName", text(&format!("${}", id.replace('.', "")))), + ]) +} +fn input_ref() -> V { + map([ + ("id", text("arg.0")), + ("type", text("app.Input")), + ("alphaName", text("$arg0")), + ]) +} +fn local(reference: &V) -> V { + map([("kind", text("local")), ("ref", reference.clone())]) +} +fn input(name: &str) -> V { + map([ + ("kind", text("field")), + ("base", local(&input_ref())), + ("field", text(name)), + ]) +} +fn call(callee: &str, types: &[&str], args: Vec) -> V { + map([ + ("kind", text("call")), + ("callee", text(callee)), + ( + "typeArgs", + V::Array(types.iter().map(|ty| text(ty)).collect()), + ), + ("args", V::Array(args)), + ]) +} +fn len(bytes: V) -> V { + call("core.bytes.length", &[BYTES], vec![bytes]) +} +fn prefix_is_utf8(bytes: &str, at: V) -> V { + call( + "core.bytes.isUtf8", + &[BYTES], + vec![call( + "core.bytes.slice", + &[BYTES], + vec![input(bytes), int(0), at], + )], + ) +} +fn add(left: V, right: V) -> V { + call("core.integer.add", &["U64"], vec![left, right]) +} +fn at_most(left: V, right: V) -> V { + map([ + ("kind", text("compare")), + ("op", text("<=")), + ("left", left), + ("right", right), + ]) +} +fn is_true(value: V) -> V { + map([ + ("kind", text("compare")), + ("op", text("==")), + ("left", value), + ( + "right", + map([ + ("kind", text("const")), + ( + "value", + map([("kind", text("bool")), ("value", V::Bool(true))]), + ), + ]), + ), + ]) +} +fn all(values: Vec) -> V { + map([("kind", text("all")), ("values", V::Array(values))]) +} + +enum Node { + Let(V, V), + Require(V), +} + +/// A pure effect program over `{ text, other: Bytes, at: U64 }`. +fn package(constraints: Vec, nodes: Vec, result: V) -> V { + let mut core = compiled_core(); + set( + &mut core, + "types", + map([ + ( + "Input", + map([ + ("kind", text("Record")), + ( + "fields", + map([ + ("at", text("U64")), + ("other", text(BYTES)), + ("text", text(BYTES)), + ]), + ), + ]), + ), + ("Result", map([("kind", text("Bool"))])), + ]), + ); + let constraints = V::Array( + constraints + .into_iter() + .enumerate() + .map(|(index, predicate)| { + map([ + ("coordinate", text(&format!("app.update@1.where.{index}"))), + ("predicate", predicate), + ]) + }) + .collect(), + ); + let intent = value_field_mut(value_field_mut(&mut core, "intents"), "update@1"); + set(intent, "input", text("app.Input")); + set(intent, "inputConstraints", constraints); + set( + value_field_mut(intent, "coreEvaluationBudget"), + "maxSteps", + V::Integer(10_000), + ); + let mut locals = vec![input_ref()]; + let mut core_nodes = Vec::new(); + let mut bindings = Vec::new(); + let mut requirements = Vec::new(); + let mut order = Vec::new(); + for (index, node) in nodes.into_iter().enumerate() { + match node { + Node::Let(binding, value) => { + locals.push(binding.clone()); + core_nodes.push(map([ + ("kind", text("let")), + ("binding", binding.clone()), + ("value", value.clone()), + ])); + let id = format!("binding.{index}"); + bindings.push(map([ + ("id", text(&id)), + ("binding", binding), + ("value", value), + ])); + order.push(text(&id)); + } + Node::Require(predicate) => { + let failure = map([ + ("kind", text("terminal")), + ( + "reason", + map([ + ("reasonKind", text("app.BadOffset")), + ("payload", map([("at", input("at"))])), + ]), + ), + ]); + core_nodes.push(map([ + ("kind", text("require")), + ("predicate", predicate.clone()), + ("onFailure", failure.clone()), + ])); + let id = format!("require.{index}"); + requirements.push(map([ + ("id", text(&id)), + ("predicate", predicate), + ("onFailure", failure), + ])); + order.push(text(&id)); + } + } + } + let body = core_body_mut(&mut core); + set(body, "locals", V::Array(locals)); + set(body, "nodes", V::Array(core_nodes)); + set(body, "result", result); + let mut target = compiled_target(&core); + let selected = selected_target_mut(&mut target); + set(selected, "pureBindings", V::Array(bindings)); + set(selected, "requirements", V::Array(requirements)); + set(selected, "executionOrder", V::Array(order)); + bound_compiler_package(&core, &target, &compiled_exports(), "update@1") +} + +fn ok_binding() -> V { + declared("local.ok", "Bool") +} +fn slice_program(constraints: Vec, bytes: &str) -> V { + package( + constraints, + vec![Node::Let(ok_binding(), prefix_is_utf8(bytes, input("at")))], + local(&ok_binding()), + ) +} + +#[test] +fn an_input_constraint_proves_a_runtime_prefix_slice() { + prepare(&slice_program( + vec![at_most(input("at"), len(input("text")))], + "text", + )) + .expect("the constraint dominates the slice"); +} + +#[test] +fn a_runtime_slice_without_its_range_proof_is_refused() { + refused(&slice_program(Vec::new(), "text")); +} + +#[test] +fn a_constraint_on_another_operand_proves_nothing() { + refused(&slice_program( + vec![at_most(input("at"), len(input("other")))], + "text", + )); +} + +#[test] +fn a_require_guard_does_not_prove_later_nodes() { + // Edict's semantics: only input constraints and earlier conjuncts of the + // same predicate dominate. A require refuses later work; it is no proof. + refused(&package( + Vec::new(), + vec![ + Node::Require(at_most(input("at"), len(input("text")))), + Node::Let(ok_binding(), prefix_is_utf8("text", input("at"))), + ], + local(&ok_binding()), + )); +} + +#[test] +fn a_let_carries_its_proven_ceiling_to_later_additions() { + let count = declared("local.count", "U64"); + let total = declared("local.total", "U64"); + let program = |addend: u64| { + package( + Vec::new(), + vec![ + Node::Let( + count.clone(), + call( + "core.bytes.count", + &[BYTES], + vec![ + input("text"), + map([ + ("kind", text("const")), + ( + "value", + map([ + ("kind", text("bytes")), + ("value", V::Bytes(vec![b'\n'])), + ]), + ), + ]), + ], + ), + ), + Node::Let(total.clone(), add(local(&count), int(addend))), + Node::Let( + ok_binding(), + is_true_value(at_most(local(&total), local(&total))), + ), + ], + local(&ok_binding()), + ) + }; + prepare(&program(u64::MAX - 64)).expect("the count is at most 64"); + refused(&program(u64::MAX - 63)); +} + +#[test] +fn an_input_constraint_bounds_a_let_and_its_later_additions() { + let at = declared("local.at", "U64"); + let total = declared("local.total", "U64"); + let program = |addend: u64| { + package( + vec![at_most(input("at"), int(10))], + vec![ + Node::Let(at.clone(), input("at")), + Node::Let(total.clone(), add(local(&at), int(addend))), + Node::Let( + ok_binding(), + is_true_value(at_most(local(&total), local(&total))), + ), + ], + local(&ok_binding()), + ) + }; + prepare(&program(u64::MAX - 10)).expect("at is at most 10"); + refused(&program(u64::MAX - 9)); +} + +/// A Bool-valued `if` of a predicate, so tests can bind a predicate result. +fn is_true_value(predicate: V) -> V { + map([ + ("kind", text("if")), + ("predicate", predicate), + ( + "then", + map([ + ("kind", text("const")), + ( + "value", + map([("kind", text("bool")), ("value", V::Bool(true))]), + ), + ]), + ), + ( + "else", + map([ + ("kind", text("const")), + ( + "value", + map([("kind", text("bool")), ("value", V::Bool(false))]), + ), + ]), + ), + ]) +} + +/// Jim's character-boundary check: one conjunction whose first conjunct +/// proves the slice in the second. +fn boundary_program() -> V { + package( + Vec::new(), + vec![Node::Require(all(vec![ + at_most(input("at"), len(input("text"))), + is_true(prefix_is_utf8("text", input("at"))), + ]))], + map([ + ("kind", text("const")), + ( + "value", + map([("kind", text("bool")), ("value", V::Bool(true))]), + ), + ]), + ) +} + +fn run(at: u64) -> Result, EffectFrameError> { + let package = prepare(&boundary_program()).expect("the conjunct prefix proves the slice"); + let program = package.program().as_effect_program().expect("effect"); + let (host, head, _) = host(); + let basis = host + .echo_operation_evaluation_basis_v1( + head, + warp_core::EchoOperationApplicationBasisV1::new([6; 32], [7; 32]), + ) + .expect("basis"); + let mut frame = host + .effect_evaluation_frame_v1( + basis, + &[], + 0, + EchoOperationBudgetV1::new(10000, 4096, 0), + limits(), + ) + .expect("frame") + .with_footprint_law(program.footprint_law().clone()) + .expect("law"); + let request = encoded(&map([ + ("at", V::Integer(i128::from(at))), + ("other", V::Bytes(Vec::new())), + ("text", V::Bytes("hé".as_bytes().to_vec())), + ])); + frame + .evaluate_effect(program, &request, &[]) + .map(<[u8]>::to_vec) +} + +#[test] +fn a_valid_program_takes_its_authored_path_for_out_of_range_requests() { + let accepted = encoded(&V::Bool(true)); + // "hé" is h, then é as two bytes: offsets 0, 1 and 3 are boundaries. + for at in [0, 1, 3] { + assert_eq!(run(at), Ok(accepted.clone()), "offset {at}"); + } + // Inside é, past the end, and at the U64 maximum: the authored obstruction. + for at in [2, 4, u64::MAX] { + assert!( + matches!( + run(at), + Err(EffectFrameError::AuthoredObstruction { ref reason_kind, .. }) + if reason_kind == "app.BadOffset" + ), + "offset {at}" + ); + } +} + +#[test] +fn the_same_check_outside_its_conjunction_is_refused_before_it_runs() { + refused(&package( + Vec::new(), + vec![Node::Require(is_true(prefix_is_utf8("text", input("at"))))], + map([ + ("kind", text("const")), + ( + "value", + map([("kind", text("bool")), ("value", V::Bool(true))]), + ), + ]), + )); +} + +#[test] +fn an_equality_constraint_bounds_a_term_from_either_side() { + let total = declared("local.total", "U64"); + let compare = |op: &str, left: V, right: V| { + map([ + ("kind", text("compare")), + ("op", text(op)), + ("left", left), + ("right", right), + ]) + }; + let program = |constraint: V, addend: u64| { + package( + vec![constraint], + vec![ + Node::Let(total.clone(), add(input("at"), int(addend))), + Node::Let( + ok_binding(), + is_true_value(at_most(local(&total), local(&total))), + ), + ], + local(&ok_binding()), + ) + }; + // Echo's predicates compare with `==` and `<=` only; as in Edict, an + // equality with a constant bounds the term on either side. + for constraint in [ + compare("==", input("at"), int(10)), + compare("==", int(10), input("at")), + ] { + prepare(&program(constraint.clone(), u64::MAX - 10)).expect("at is at most 10"); + refused(&program(constraint, u64::MAX - 9)); + } +} diff --git a/docs/topics/GeneratedRules.md b/docs/topics/GeneratedRules.md index 971b0935..25a27490 100644 --- a/docs/topics/GeneratedRules.md +++ b/docs/topics/GeneratedRules.md @@ -218,9 +218,20 @@ 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 -constraints do not cross into a helper frame. +literal, count and nested-sum bounds, carried `let` ceilings, and a dominating +fact that compares the term with a constant (`term <= c` or `term == c`). Other +terms retain their full unsigned width, so zero identity is total and an +unbounded parameter plus one refuses. Caller constraints do not cross into a +helper frame. + +Authored effect programs are judged the same way at preparation. The intent's +input constraints dominate its whole body, so `at <= len(text)` as an input +constraint proves `slice(text, 0, at)` in any later node. An unsigned `let` +proven below its width carries that ceiling to later nodes, from counts, +literals, sums or a constraint such as `at <= 10`. Earlier conjuncts of one +`all` prove the later ones. A `require` proves nothing after it, as in Edict: +its guard ends evaluation on failure but is not a dominating fact. A guard on +another operand or offset proves nothing. The retained public compiler fixtures cover a legacy-producer execution control and a strict SourceFunctions publication containing an authored arithmetic helper.