diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d7b81eba..46c414735 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 @@ -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/crates/echo-edict-provider-verifier/README.md b/crates/echo-edict-provider-verifier/README.md index 51c06dde3..08ad436e0 100644 --- a/crates/echo-edict-provider-verifier/README.md +++ b/crates/echo-edict-provider-verifier/README.md @@ -34,7 +34,22 @@ 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. -For `compiler-produced-bounded-pure/v1`, the verifier independently enforces +**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 +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. 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 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 c8417e1f5..2a256ce07 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 649497ddd..c5a5e83c6 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 @@ -219,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. @@ -448,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 @@ -485,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 diff --git a/schemas/edict-provider/README.md b/schemas/edict-provider/README.md index 24f20f991..22dcc891c 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