Prove basis-bound validated patch application

CHANGELOG.md

@@ -27,9 +27,65 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
   runtime-request admission errors at every phase boundary, checkout-independent
   artifact paths, path and budget refusals, fixed-seed cases, and bounded
   stress.
+- Compiler-authored basis-bound patch witness covering request-before-write,
+  exact writable apertures, postcondition settlement, effect-free retry and
+  replay, crash reconciliation, ambiguous outcomes, path and basis refusals,
+  request-budget boundaries, compiler-artifact substitution, fixed-seed binary
+  replacements, and bounded stress.
+- Writer-epoch chain evidence in the observation and patch reports, with
+  witness cases requiring a fresh epoch per write phase, exact predecessor and
+  final-commit-digest linkage, a strictly advancing start LSN, no epoch on
+  read-only phases, and no epoch reused across the ordered golden path. The
+  predecessor linkage is compared against the commit digest the predecessor
+  reported, not merely checked for shape.
+- A retained-ledger plateau case in both witnesses, driving sixteen fresh
+  writer epochs on one WAL and requiring the persisted ledger to stop changing
+  size, which a fixed-size ceiling could not establish.
+- A two-route basis binding for the reconciled success settlement, since the
+  reconciler is a distinct implementation from the adapter and the existing
+  probe exercised only the apply path.
+- Writer-epoch coverage on the reconciliation and uncertainty write
+  entrypoints, and retained-ledger snapshots across both retries, since a null
+  epoch in a retry report is supplied by the phase itself and cannot show that
+  no epoch was taken.
+- Negative coverage for the retained postcondition evidence: the one settlement
+  family where the declared replacement and the observed post-state differ now
+  pins that the evidence varies with what was observed and not with what was
+  requested, and records that `beforeContentDigest` reports the observed bytes
+  in that case.
+- `wal.lastCommitDigest` in both reports, so a successor epoch's declared
+  predecessor commit can be compared with the commit that actually closed it.
+- Build refusal for cross-wired, unresolved, or sentinel external-action schema
+  identities in the vendored compiler source, enforced by a single shared guard
+  that binds each schema slot to the vendored artifact it names.
+- Hermetic `tests/resource-identity-guard.sh` and
+  `tests/writer-epoch-assertions.sh` covering the build guard and the shared
+  writer-epoch assertions against crafted closures and mutated reports. Both
+  require no producer checkout and no `cargo`.
+
+- `replacementExceedsRequestBudget` and `observationExceedsFileBudget` as
+  distinct request obstructions, with witness cases covering a replacement
+  above the encodable ceiling and a declared pre-state above the file budget.
 
 ### Changed
 
+- Advanced the vendored `workspace.patch@1` closure to Edict
+  `df80f92ad6242c6da31a64224666fd37aa43b0d0`, which replaces the sentinel
+  `workspace.patch.input@1`, `workspace.patch.settlement@1`, and
+  `workspace.patch.reconcile@1` digests with the exact identities of vendored
+  `edict.external-action-resource/v1` artifacts, now supplied to the build
+  through `externalActionResources`.
+- Acquire the patch host's writer epoch through Echo's
+  `FilesystemWalStore::acquire_fresh_writer_epoch` against Echo
+  `c354d531679861fb7bbd52ab7b7703807909ab86`, replacing the static epoch
+  identity, fixed fencing, process, host, and lease digests, and absent
+  predecessor linkage that could not fence overlapping or restarted hosts.
+- Advanced the vendored `workspace.snapshot@1` closure to the same Edict
+  commit, which likewise replaces its sentinel `workspace.snapshot.input@1`,
+  `workspace.snapshot.settlement@1`, and `workspace.snapshot.reconcile@1`
+  digests with vendored external-action resource identities, and acquire the
+  observation host's writer epoch through the same producer-owned fresh-epoch
+  contract.
 - Require the runtime witness to retain the exact Edict-authored
   `GreetingCreated { key, message }` result identity and canonical bytes through
   generic Echo evaluation and to compare the applied, fresh-host, and

README.md

@@ -139,10 +139,18 @@ bounded workspace adapter. It proves:
   post-claim aperture substitution cannot recover the claim;
 - unauthorized, parent-escaped, symlink, and stale-basis paths settle as typed
   refusals;
-- the exact settlement-size boundary succeeds and one byte less refuses; and
+- the exact settlement-size boundary succeeds and one byte less refuses;
 - substituted compiler artifacts are rejected with the same typed obstruction
   at request and recovery boundaries without appending to the WAL, while
-  invalid runtime requests remain a distinct pre-commit refusal.
+  invalid runtime requests remain a distinct pre-commit refusal; and
+- every write phase runs under a fresh Echo-derived writer epoch chained to the
+  persisted predecessor, while read-only phases acquire no epoch.
+
+The request pins `workspace.snapshot.input@1`,
+`workspace.snapshot.settlement@1`, and `workspace.snapshot.reconcile@1` to the
+exact identities of vendored `edict.external-action-resource/v1` artifacts,
+supplied to the build through `externalActionResources`. An unresolved or
+sentinel schema identity fails the build closed.
 
 The fixed suite contains one ordered golden path, one relative
 compiler-artifact path probe, one idempotent retry, one conflicting retry, one
@@ -160,3 +168,110 @@ process, network, or model authority and introduces no application callback.
 
 No artifact in this repository may be replaced by a handwritten Echo package,
 and no native Hello Echo callback may implement application semantics.
+
+## Hello Effect validated patch application
+
+The second external-effect proof accepts bounded observation evidence as basis
+input and applies one compiler-authored validated patch:
+
+```sh
+EDICT_REPO=/path/to/edict \
+ECHO_REPO=/path/to/echo \
+./tests/patch-runtime.sh
+```
+
+This witness needs `b3sum` and `xxd` in addition to `jq`. It compares the content digests
+the settlement reports against digests computed from the witnessed bytes, so it
+must hash them the same way the adapter does.
+
+The build corroborates the exact Edict source, lawpack closure, digest
+sidecars, Core artifact, and Target IR artifact for
+`workspace.patch.applyValidated@1`. Edict emits request data only. The compiler
+provider receives no filesystem authority and emits no executable-operation
+package.
+
+The request JSON separates untrusted `proposal` data from the declared
+`observation` basis. The host owns `permittedPaths` and the adapter's
+65,536-byte file cap; the model controls only the closed `proposal` schema.
+
+That 65,536-byte cap bounds the file, not the replacement. The encoded patch
+carries the target path and the expected content digest inside the same bounded
+request carrier, so the largest accepted replacement is smaller than the cap and
+shrinks as the path grows.
+
+The budget is producer-owned. Echo's `encode_validated_workspace_patch_input_v1`
+refuses with `FileBudgetExceeded` once the canonical encoding passes
+`MAX_CANONICAL_PATCH_INPUT_BYTES`, and Hello Echo surfaces that as
+`replacementExceedsRequestBudget` rather than deriving a ceiling of its own. A
+replacement that cannot be carried is therefore refused for a stated reason
+instead of being reported as a malformed request.
+
+The reachable size follows from that bound minus the canonical framing, so it is
+not a constant this repository can pin. Measured against Echo
+`c354d531679861fb7bbd52ab7b7703807909ab86`, it was 65,366 bytes for `a.txt`,
+65,360 for `notes/x.txt`, and 65,313 for a 57-character path. Those figures
+illustrate the shape of the bound; they are not a contract, and they move with
+the producer's encoding. Nothing in this repository depends on them, and
+`tests/patch-runtime.sh` probes the refusal rather than any particular
+threshold.
+The host uses Echo's generic validated-patch encoder and authority functions;
+it does not reconstruct patch policy or perform native application semantics.
+The observation is also a closed schema. Echo durably records the request and
+claim before only the bounded adapter receives a workspace root.
+
+This witness proves the basis-bound write boundary independently. It does not
+claim that the observation and patch run share one chained transaction or
+worldline.
+
+The runtime witness proves:
+
+- request and claim commit before mutation, across separate processes;
+- recovery exposes pending requested and claimed states without workspace
+  authority;
+- the adapter can mutate only an exact permitted path under the admitted
+  observation basis;
+- the canonical settlement commits before the result is reported, and the
+  report cross-compares its attempt, request basis, external evidence,
+  postcondition digest, and resulting basis;
+- exact retry is effect-free and conflicting retry obstructs without WAL
+  growth;
+- replay accepts no workspace root and does not reapply a settled patch after
+  the file changes again;
+- a crash after mutation but before settlement reconciles from the observed
+  postcondition without inventing pre-state evidence;
+- an ambiguous postcondition settles as `outcomeUnknown` without another
+  mutation;
+- stale basis, unauthorized path, parent escape, symlink, and CI-workflow
+  policy failures obstruct before mutation;
+- the exact request-only settlement floor passes and one byte less refuses
+  before a WAL commit;
+- a replacement too large for the compiler-declared request carrier refuses as
+  `replacementExceedsRequestBudget` before a WAL commit, and a declared
+  pre-state above the host file budget refuses as
+  `observationExceedsFileBudget`, both distinct from a malformed request and
+  from each other;
+- compiler-artifact substitution fails at request and claim boundaries
+  without hidden WAL growth;
+- every write phase runs under a fresh Echo-derived writer epoch chained to the
+  persisted predecessor, read-only phases acquire no epoch, and no epoch is
+  reused across the ordered path; and
+- fixed-seed text, Unicode, and binary replacements plus eight bounded stress
+  worldlines pass.
+
+The request pins `workspace.patch.input@1`, `workspace.patch.settlement@1`, and
+`workspace.patch.reconcile@1` to the exact identities of vendored
+`edict.external-action-resource/v1` artifacts, supplied to the build through
+`externalActionResources`. An unresolved or sentinel schema identity fails the
+build closed.
+
+Writer-epoch fencing is producer-owned. Each host phase is a separate process,
+and it calls Echo's `FilesystemWalStore::acquire_fresh_writer_epoch`, which
+takes the filesystem writer lease, rereads the persisted epoch ledger, closes
+an epoch left by a terminated process, and derives the successor from that
+predecessor's identity and final commit digest. Hello Echo constructs no epoch
+identity and reuses no fencing token across restarts.
+
+The model-facing surface is data only. Edict owns the request declaration,
+Echo owns admission and durable coordination, and the adapter alone owns the
+bounded write. No generic filesystem write, process, network, Git, or model
+authority is introduced.

docs/roadmap.md

@@ -132,11 +132,28 @@ Add `ApplyValidatedPatch` only after read-only observation is green:
 - settlement records the resulting basis or `outcome_unknown`; and
 - replay never reapplies the patch.
 
+The `workspace.patch.applyValidated@1` consumer proof now satisfies this phase.
+Exact Edict Core and Target IR artifacts construct the request without callable
+write effects. Proposal data is deterministically encoded against declared
+bounded-observation input and an exact host-owned writable aperture.
+Model-facing fields are a closed schema, while both the aperture and file cap
+remain host-owned and cannot be substituted after claim. This independently
+proves the basis-bound write boundary; it does not claim one chained
+observation-to-patch transaction or worldline. Echo records request and claim
+before only its generic adapter receives the workspace root. Settlement
+precedes publication; exact retry and replay are effect-free; ambiguous
+postconditions reconcile to either the observed success or `outcomeUnknown`;
+the consumer cross-compares Echo's attempt, request-basis, external-evidence,
+postcondition, and resulting-basis bindings; and path, basis, symlink,
+CI-workflow, budget, and compiler-artifact violations fail closed at their
+owning boundaries.
+
 No generic process, filesystem, or network capability is introduced.
 
-Roadmap A.1 is four of five phases complete: Echo durable external actions,
-Edict typed external requests, Echo bounded observation, and this external
-consumer proof are complete. Basis-bound validated patch application remains.
+Roadmap A.1 is five of five phases complete: Echo durable external actions,
+Edict typed external requests, Echo bounded observation, the external
+observation consumer proof, and basis-bound validated patch application are
+complete.
 
 ## Roadmap B — Graft hosted by Echo
 

edict.effect.application.json

@@ -13,6 +13,17 @@
       "targetConfiguration": "effect/vendor/workspace-snapshot/request-profile-configuration.cbor"
     }
   ],
+  "externalActionResources": [
+    {
+      "artifact": "effect/vendor/workspace-snapshot/input-schema.cbor"
+    },
+    {
+      "artifact": "effect/vendor/workspace-snapshot/settlement-schema.cbor"
+    },
+    {
+      "artifact": "effect/vendor/workspace-snapshot/reconciliation-law.cbor"
+    }
+  ],
   "target": {
     "profile": "echo.dpo@1",
     "providerPackage": ".build/effect/echo-provider"

edict.patch.application.json

@@ -0,0 +1,32 @@
+{
+  "schema": "edict.application/v1",
+  "buildKind": "externalAction",
+  "coordinate": "examples.workspace_patcher@1",
+  "sources": [
+    "patch/src/apply-validated-patch.edict"
+  ],
+  "lawpacks": [
+    {
+      "manifest": "patch/vendor/workspace-patch/manifest.cbor",
+      "exports": "patch/vendor/workspace-patch/exports.cbor",
+      "adapter": "patch/vendor/workspace-patch/adapter.cbor",
+      "targetConfiguration": "patch/vendor/workspace-patch/request-profile-configuration.cbor"
+    }
+  ],
+  "externalActionResources": [
+    {
+      "artifact": "patch/vendor/workspace-patch/input-schema.cbor"
+    },
+    {
+      "artifact": "patch/vendor/workspace-patch/settlement-schema.cbor"
+    },
+    {
+      "artifact": "patch/vendor/workspace-patch/reconciliation-law.cbor"
+    }
+  ],
+  "target": {
+    "profile": "echo.dpo@1",
+    "providerPackage": ".build/patch/echo-provider"
+  },
+  "outputDirectory": ".build/patch/application"
+}