From dca2ff03de8496f3d4771498dd489c89c9aeeded Mon Sep 17 00:00:00 2001 From: James Ross Date: Wed, 14 Oct 2026 01:43:48 -0700 Subject: [PATCH 1/5] Verifier README: state what the executable-operation check is independent of The README said the verifier reconstructs the expected package without importing or calling the lowerer. That is true, but on 2026-10-14 91% of the lowerer's distinct code lines in executable_operation.rs appeared verbatim in the verifier's copy, so one mistake is usually made twice. The new paragraph states the property the byte comparison does provide: it rejects tampering and a defect in the lowerer alone, as the rebound-coordinate and tamper tests show, and it accepts a mistake present in both copies, as d121758b showed. Fixes #809. Co-Authored-By: Claude Opus 5.5 --- crates/echo-edict-provider-verifier/README.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/crates/echo-edict-provider-verifier/README.md b/crates/echo-edict-provider-verifier/README.md index 51c06dde..82bbba7e 100644 --- a/crates/echo-edict-provider-verifier/README.md +++ b/crates/echo-edict-provider-verifier/README.md @@ -34,6 +34,19 @@ runtime expression and application-input paths, binds their identity into the expected package, and names that exact projection in the accepted report. Application vocabulary is treated only as opaque authored data. +**What this independence covers.** The executable-operation route does not +import the lowerer, but most of its reconstruction in +`src/executable_operation.rs` is a copy of the lowerer's file of the same +name: on 2026-10-14, 91% of the lowerer's distinct code lines appeared +verbatim. The byte comparison therefore rejects any package that differs from +what this copy produces. That covers tampering after lowering and a defect +introduced in the lowerer alone, as the rebound-coordinate and tamper tests in +`tests/executable_operation_package.rs` show. It does not catch a mistake +present in both copies: such a package lowers and then verifies. Commit +`d121758b` is an example, where one missing refusal had to be added to both +files. On this route, acceptance shows that two copies agree; it is not an +independent semantic check (#809). + For `compiler-produced-bounded-pure/v1`, the verifier independently enforces the zero-choice configuration, effect-free Core and Target IR shapes, exact budget and closure bindings, pure-binding result projection, and embedded From 518325a05a04a934524a8f2d20fdd4ca9530aaa9 Mon Sep 17 00:00:00 2001 From: James Ross Date: Wed, 14 Oct 2026 01:49:02 -0700 Subject: [PATCH 2/5] Docs: scope the copy caveat and stop calling the CAS verifier independent The caveat now names the packages rebuilt in the copied file (mutation, compare-and-set, bounded pure) and says the bounded-read route rebuilds Core from the Target IR instead. The architecture document called the mutation/CAS verifier independent twice; it now says structurally separate. Found by review of #849. Co-Authored-By: Claude Opus 5.5 --- crates/echo-edict-provider-verifier/README.md | 12 +++++++----- docs/architecture/application-contract-hosting.md | 5 +++-- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/crates/echo-edict-provider-verifier/README.md b/crates/echo-edict-provider-verifier/README.md index 82bbba7e..af0fbfc5 100644 --- a/crates/echo-edict-provider-verifier/README.md +++ b/crates/echo-edict-provider-verifier/README.md @@ -34,9 +34,9 @@ runtime expression and application-input paths, binds their identity into the expected package, and names that exact projection in the accepted report. Application vocabulary is treated only as opaque authored data. -**What this independence covers.** The executable-operation route does not -import the lowerer, but most of its reconstruction in -`src/executable_operation.rs` is a copy of the lowerer's file of the same +**What this independence covers.** The mutation, compare-and-set and bounded +pure packages are rebuilt in `src/executable_operation.rs`. That file does not +import the lowerer, but most of it is a copy of the lowerer's file of the same name: on 2026-10-14, 91% of the lowerer's distinct code lines appeared verbatim. The byte comparison therefore rejects any package that differs from what this copy produces. That covers tampering after lowering and a defect @@ -44,8 +44,10 @@ introduced in the lowerer alone, as the rebound-coordinate and tamper tests in `tests/executable_operation_package.rs` show. It does not catch a mistake present in both copies: such a package lowers and then verifies. Commit `d121758b` is an example, where one missing refusal had to be added to both -files. On this route, acceptance shows that two copies agree; it is not an -independent semantic check (#809). +files. For these packages, acceptance shows that two copies agree; it is not +an independent semantic check (#809). The bounded-read route below is +different: `src/executable_operation/bounded_read.rs` rebuilds Core from the +Target IR instead of repeating the lowering. For `compiler-produced-bounded-pure/v1`, the verifier independently enforces the zero-choice configuration, effect-free Core and Target IR shapes, exact diff --git a/docs/architecture/application-contract-hosting.md b/docs/architecture/application-contract-hosting.md index 649497dd..2919e8be 100644 --- a/docs/architecture/application-contract-hosting.md +++ b/docs/architecture/application-contract-hosting.md @@ -177,7 +177,7 @@ supported. Invocation admission also checks the relationship and exact digest. Missing or substituted invocation bindings return `ApplicationInputMismatch`; legacy invocation encodings remain unchanged. Both mutation profiles require the effect argument to be the declared application -input directly. The lowerer and independent verifier each check the canonical +input directly. The lowerer and the structurally separate verifier each check the canonical `arg.0` reference, its declared type and alpha name, and its unique local declaration. They refuse transformed records and other local references with `UnsupportedSemantics`; these bounded profiles do not evaluate arbitrary effect @@ -187,7 +187,8 @@ accepted `message: "forced"` counterexample as historical failing evidence; the corrected components refuse that source without publishing package artifacts, while the direct-input control produces the same package and report bytes. -The native lowerer and independent verifier select the CAS program from an exact +The native lowerer and the structurally separate verifier select the CAS program +from an exact `continuum.profile.write/v1` effect with the CAS target intrinsic and `replace` write class. Its configuration requires a distinct `expectedValueDigestField` and at least four steps; the package binds the corresponding input path and From 2a046bdcf9bb4d5d92340fcf7f5bb05a6dc24b9e Mon Sep 17 00:00:00 2001 From: James Ross Date: Wed, 14 Oct 2026 01:52:45 -0700 Subject: [PATCH 3/5] Docs: stop calling the copied verifier routes independent The bounded-pure, mutation and compare-and-set verifier routes rebuild the package with code that largely repeats the lowerer's. Four more places called that reconstruction independent: the provider schema README, the verifier README's bounded-pure paragraph, the architecture document, and the Jedit fixture README. They now say structurally separate or name the shared code. Found by review of #849. Statements of the requirement, and the first native verifier, are unchanged. Co-Authored-By: Claude Opus 5.5 --- crates/echo-edict-provider-verifier/README.md | 2 +- crates/warp-core/tests/fixtures/edict-pure-jedit/README.md | 2 +- docs/architecture/application-contract-hosting.md | 6 +++--- schemas/edict-provider/README.md | 5 +++-- 4 files changed, 8 insertions(+), 7 deletions(-) diff --git a/crates/echo-edict-provider-verifier/README.md b/crates/echo-edict-provider-verifier/README.md index af0fbfc5..08ad436e 100644 --- a/crates/echo-edict-provider-verifier/README.md +++ b/crates/echo-edict-provider-verifier/README.md @@ -49,7 +49,7 @@ an independent semantic check (#809). The bounded-read route below is different: `src/executable_operation/bounded_read.rs` rebuilds Core from the Target IR instead of repeating the lowering. -For `compiler-produced-bounded-pure/v1`, the verifier independently enforces +For `compiler-produced-bounded-pure/v1`, the verifier separately enforces the zero-choice configuration, effect-free Core and Target IR shapes, exact budget and closure bindings, pure-binding result projection, and embedded compiler artifact bytes. It reconstructs the distinct generic pure package diff --git a/crates/warp-core/tests/fixtures/edict-pure-jedit/README.md b/crates/warp-core/tests/fixtures/edict-pure-jedit/README.md index c8417e1f..2a256ce0 100644 --- a/crates/warp-core/tests/fixtures/edict-pure-jedit/README.md +++ b/crates/warp-core/tests/fixtures/edict-pure-jedit/README.md @@ -42,7 +42,7 @@ not graph mutation, installed invocation, a Tick, a Receipt, or WAL evidence. The `mutated-*.hex` carriers came from a separate copy of the same application. The only authored change was `then 1u32` to `then 2u32` in `src/ReplaceRange.edict`. Edict's public JSONL application build generated the -new executable package and accepted independent verification report. No emitted +new executable package and accepted verification report. No emitted Core, Target IR, package, or report bytes were edited. The deliberate source change makes the original expected value of 1 false at diff --git a/docs/architecture/application-contract-hosting.md b/docs/architecture/application-contract-hosting.md index 2919e8be..6fe91290 100644 --- a/docs/architecture/application-contract-hosting.md +++ b/docs/architecture/application-contract-hosting.md @@ -220,7 +220,7 @@ The external-provider schema additionally admits one exact zero-choice application operation, target-specific budget override, or mutation authority. The checked lowerer emits a distinct generic package retaining the exact compiler-produced pure program closure, and the structurally separate verifier -independently reconstructs that relation. No runtime evaluator, installation, +reconstructs that relation with code that largely repeats the lowerer's. No runtime evaluator, installation, graph mutation, Tick settlement, or application-specific Echo branch follows from package acceptance. @@ -449,8 +449,8 @@ effectful execution and its settlement evidence remain tracked by The slice exposes no application matcher, executor, or footprint callback. A generic provider lowerer now emits the package from exact Edict source, Core, lawpack, exports, adapter, target-configuration, and Target IR artifacts, and a -structurally separate provider verifier independently reconstructs that -relation. Edict's public application-build command assembles those inputs end +structurally separate provider verifier reconstructs that relation with code +that largely repeats the lowerer's, so a mistake made in both is not caught. Edict's public application-build command assembles those inputs end to end and invokes the checked Echo lowerer and structurally separate verifier. The slice does not implement Jedit `ReplaceRange`, any Graft operation, or cross-head atomic filesystem-WAL persistence. Provider v1 remains diff --git a/schemas/edict-provider/README.md b/schemas/edict-provider/README.md index 24f20f99..22dcc891 100644 --- a/schemas/edict-provider/README.md +++ b/schemas/edict-provider/README.md @@ -196,8 +196,9 @@ configuration, the anchored compare-and-set configuration with its distinct value's length, which evaluation also charges), and the exact two-field `compiler-produced-bounded-pure/v1` configuration. The latter contains no application coordinate or policy choice. The checked lowerer now emits the -distinct generic pure package and the checked independent verifier reconstructs -that exact compiler relation. The package remains uninstalled and unevaluated; +distinct generic pure package and the checked, structurally separate verifier +reconstructs that exact compiler relation (its reconstruction largely repeats +the lowerer's code; see the verifier README). The package remains uninstalled and unevaluated; it confers no Echo runtime authority or consequence. External Edict contract inputs come from the checked From 253eee0deb5d12d38bfe6e4649531e1c280d1c86 Mon Sep 17 00:00:00 2001 From: James Ross Date: Wed, 14 Oct 2026 01:57:15 -0700 Subject: [PATCH 4/5] Changelog: stop calling the copied verifier routes independent Three Unreleased entries (projected CAS, transformed effect arguments, the bounded-pure package) called the same verifier independent. They now say structurally separate. Source-function checks, where the verifier shares about 29% of the lowerer's code, keep their wording. Found by review of #849. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d7b81eb..95468126 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -71,7 +71,7 @@ - `SlotWriteIndex` resolves the value of one node, edge or attachment slot at a tick cursor from tick patches and the initial boundary, without materializing a graph or replaying unrelated ticks. It indexes the operations that wrote each slot, including values cleared by node, edge and instance deletion, and truncates in proportion to the ticks removed. A reader is bound to the exact patches the index was built from by patch digest, and truncation refuses patches that are not the indexed suffix. It is a derived reading aid; the runtime does not use it yet. -- Native projected compare-and-set invocation encoding retains canonical application input and statically binds the expected attachment-value digest. The native lowerer and independent verifier reconstruct CAS-specific profiles and reject rebound digest paths or under-budget configurations. Generated schema, reproducible components and a retained public Edict compiler build establish package production. The retained compiler package now has scheduler execution, pending/committed Action recovery, stale-digest noncommit recovery and typed refusal witnesses. `EchoOperationInvocationV1::anchored_node_attachment_compare_and_set_with_application_input` and `ExecutableOperationPackageV1::with_compare_and_set_application_result_projection` construct the projected forms without byte editing. +- Native projected compare-and-set invocation encoding retains canonical application input and statically binds the expected attachment-value digest. The native lowerer and the structurally separate verifier reconstruct CAS-specific profiles and reject rebound digest paths or under-budget configurations. Generated schema, reproducible components and a retained public Edict compiler build establish package production. The retained compiler package now has scheduler execution, pending/committed Action recovery, stale-digest noncommit recovery and typed refusal witnesses. `EchoOperationInvocationV1::anchored_node_attachment_compare_and_set_with_application_input` and `ExecutableOperationPackageV1::with_compare_and_set_application_result_projection` construct the projected forms without byte editing. - The trusted executable-operation host can retain two native alternative strands, continue a losing strand under new observations, and recover its fork ancestry @@ -161,7 +161,7 @@ - Package admission rejects result projections whose expected-digest binding conflicts with the selected mutation program, before they can occupy an installed operation coordinate. Recovery applies the same rule to retained installations: a WAL that holds such a hand-built package is refused rather than reinstalled. Echo's providers never emitted that shape, and no invocation of it could be admitted. Admission likewise refuses an expected-digest path that is empty or overlaps the key or replacement path. -- Both executable mutation providers refuse transformed effect arguments instead of silently projecting the caller input into a different mutation. Direct application-input arguments remain supported; the independent verifier enforces the same boundary. +- Both executable mutation providers refuse transformed effect arguments instead of silently projecting the caller input into a different mutation. Direct application-input arguments remain supported; the structurally separate verifier enforces the same boundary. - Retained local fork retries reconcile durable topology after uncertain appends, preserving the original basis and preventing duplicate fork records. @@ -351,8 +351,8 @@ contains no operation coordinate, application vocabulary, budget override, or runtime authority. The checked lowerer now emits a distinct generic pure package containing the exact compiler Core, lawpack exports, Target IR, and - result projection; the structurally separate verifier independently - reconstructs and accepts that relation. This is executable package + result projection; the structurally separate verifier reconstructs and + accepts that relation. This is executable package construction evidence, not Echo runtime evaluation or settlement evidence. - Strict filesystem WAL stores now persist a checksummed writer-epoch ledger containing the active epoch, its exact latest closed predecessor, and final From 372a1b05ff376e0d7bd2f5fe6ad0e18ac1c7f821 Mon Sep 17 00:00:00 2001 From: James Ross Date: Wed, 14 Oct 2026 02:05:12 -0700 Subject: [PATCH 5/5] Docs: withdraw the last independence claims for the copied routes The create mutation profile's Core-relation evidence, the result-ceiling entry and the obstruction-alias entry still called the copied verification independent. Remaining uses describe the requirement, the bounded-read route, or how release digests are verified. Found by review of #849. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 4 ++-- docs/architecture/application-contract-hosting.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 95468126..46c41473 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -448,7 +448,7 @@ recovers this evidence without a native application callback or application-specific reconstruction. Runtime admission caps canonical application input at 65,536 bytes and the compiler-declared result ceiling at - 65,536 before private scheduler evaluation. Both independent provider + 65,536 before private scheduler evaluation. Both provider components reject result ceilings above that runtime maximum and ambiguous input bindings. Configuration-derived node-key and replacement field names share the projection path-segment text ceiling. Package admission preserves @@ -2026,7 +2026,7 @@ Applied, Rejected, Obstructed}` with receipt evidence and typed contract unwritten log position. A second reopen followed by append previously left an LSN gap and made subsequent recovery fail. -- Generic executable-operation lowering and independent verification now +- Generic executable-operation lowering and verification now resolve source-local obstruction constructor aliases through the exact digest-locked lawpack import before encoding or comparing the package. Runtime duplicate outcomes therefore retain the capability-owned obstruction diff --git a/docs/architecture/application-contract-hosting.md b/docs/architecture/application-contract-hosting.md index 6fe91290..c5a5e83c 100644 --- a/docs/architecture/application-contract-hosting.md +++ b/docs/architecture/application-contract-hosting.md @@ -486,7 +486,7 @@ reconstructs the entire expected package, including those limits, so changing or removing them fails the package relation. This native profile does not normalize input text or establish NFC validity. The runtime checks alone do not -prove the Core relation; the independent provider verification supplies that +prove the Core relation; the structurally separate provider verification supplies that separate evidence. The checked provider component distribution includes this profile, built reproducibly with the pinned component toolchain and corroborated by its regenerated manifest. A retained fresh public application build with