Prove basis-bound validated patch application

.github/workflows/ci.yml

@@ -0,0 +1,127 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+    branches: [main]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ci-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  witnesses:
+    name: Witness gate
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out Hello Echo
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+
+      - name: Read the pinned producer commits
+        id: producers
+        run: |
+          set -eu
+          test "$(jq -r '.version' producers.lock.json)" = 1
+          {
+            printf 'edict_repo=%s\n' "$(jq -r '.edict.repository' producers.lock.json)"
+            printf 'edict_commit=%s\n' "$(jq -r '.edict.commit' producers.lock.json)"
+            printf 'echo_repo=%s\n' "$(jq -r '.echo.repository' producers.lock.json)"
+            printf 'echo_commit=%s\n' "$(jq -r '.echo.commit' producers.lock.json)"
+          } >>"$GITHUB_OUTPUT"
+
+      - name: Check out Edict at the pinned commit
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          repository: ${{ steps.producers.outputs.edict_repo }}
+          ref: ${{ steps.producers.outputs.edict_commit }}
+          path: .producers/edict
+
+      - name: Check out Echo at the pinned commit
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          repository: ${{ steps.producers.outputs.echo_repo }}
+          ref: ${{ steps.producers.outputs.echo_commit }}
+          path: .producers/echo
+
+      - name: Install the Rust toolchain
+        run: |
+          set -eu
+          rustup toolchain install stable --profile minimal \
+            --component rustfmt --component clippy
+          rustup default stable
+
+      - name: Install witness tools
+        run: |
+          set -eu
+          sudo apt-get update
+          sudo apt-get install --yes --no-install-recommends b3sum xxd
+
+      - name: Cache cargo
+        uses: actions/cache@1bd1e32a3bdc45362d1e726936510720a7c30a57 # v4.2.0
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            .build
+          key: cargo-${{ runner.os }}-${{ steps.producers.outputs.edict_commit }}-${{ steps.producers.outputs.echo_commit }}
+          restore-keys: cargo-${{ runner.os }}-
+
+      - name: Check shell syntax
+        run: |
+          set -eu
+          for script in tests/*.sh tests/lib/*.sh; do
+            test -e "$script" || continue
+            sh -n "$script"
+          done
+
+      - name: Verify the producer lock
+        env:
+          EDICT_REPO: .producers/edict
+          ECHO_REPO: .producers/echo
+        run: ./tests/producer-lock.sh
+
+      # Every witness builds what it needs, so the build boundaries are covered
+      # by the suites that invoke them.
+      - name: Run the pure runtime witness
+        env:
+          EDICT_REPO: .producers/edict
+          ECHO_REPO: .producers/echo
+        run: ./tests/runtime.sh
+
+      - name: Run the workspace observation witness
+        env:
+          EDICT_REPO: .producers/edict
+          ECHO_REPO: .producers/echo
+        run: ./tests/effect-runtime.sh
+
+      - name: Run the validated patch witness
+        env:
+          EDICT_REPO: .producers/edict
+          ECHO_REPO: .producers/echo
+        run: ./tests/patch-runtime.sh
+
+      - name: Run the stale-output witness
+        env:
+          EDICT_REPO: .producers/edict
+          ECHO_REPO: .producers/echo
+        run: ./tests/build-cleans-output.sh
+
+      - name: Run the hermetic assertion tests
+        run: ./tests/writer-epoch-assertions.sh
+
+      - name: Check host formatting
+        run: |
+          set -eu
+          cargo fmt --manifest-path .build/effect/host/Cargo.toml -- --check
+          cargo fmt --manifest-path .build/patch/host/Cargo.toml -- --check
+
+      - name: Lint the generated hosts
+        run: |
+          set -eu
+          cargo clippy --manifest-path .build/effect/host/Cargo.toml \
+            --target-dir .build/effect/host-target --all-targets -- -D warnings
+          cargo clippy --manifest-path .build/patch/host/Cargo.toml \
+            --target-dir .build/patch/host-target --all-targets -- -D warnings

.gitignore

@@ -1 +1,4 @@
 /.build/
+
+# Producer checkouts materialised by CI.
+.producers/

CHANGELOG.md

@@ -27,9 +27,92 @@ 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.
+- Hermetic `tests/writer-epoch-assertions.sh` covering the shared writer-epoch
+  assertions against mutated reports. It requires 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.
+
+- `producers.lock.json` pinning the exact Edict and Echo commits, enforced at
+  every build boundary by `tests/producer-lock.sh`, so a stale, mismatched, or
+  locally modified producer checkout fails rather than silently changing what
+  is proven.
+- A CI workflow that reads that lock, checks the producers out at those
+  commits, and runs the complete witness gate plus shell syntax, formatting,
+  and strict clippy on pull requests and pushes to `main`.
+
+- Large file bodies are handed to `jq` through `--rawfile` rather than `--arg`.
+  A body at the file budget is 131,072 hex characters, which is exactly Linux's
+  `MAX_ARG_STRLEN`, so the oversize cases failed with "Argument list too long"
+  anywhere but a developer machine.
+- Absolute symlink targets in the relative-producer-path probe. The probe
+  linked the producer checkout as given, so a relative producer path produced a
+  dangling link rather than a relative path, and the observation witness failed
+  before it began. It worked only because every caller had passed absolute
+  paths until CI existed.
+
+### Removed
+
+- `tests/lib/check-resource-identities.sh` and
+  `tests/resource-identity-guard.sh`. The guard had grown into a second Edict
+  parser written in shell and living in the consumer: declaration syntax,
+  comments, coordinates, same-line clauses, sidecar terminators, digest
+  grammar, and placeholder recognition. Edict owns canonical resource
+  construction, identity derivation, closure validation, and rejection of
+  malformed, missing, substituted, and sentinel resources, and the build
+  already corroborates every artifact byte-for-byte and invokes that validator.
+  Hello Echo corroborates Edict artifacts; it does not partially reparse Edict
+  source.
 
 ### 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

@@ -26,9 +26,23 @@ basis-bound patch application, Graft hosting, Git and GitHub adapters, and the
 self-hosted delivery loop. The delivery loop is Roadmap Ω, not Hello Echo's
 bootstrap workload.
 
+## Producer pin
+
+`producers.lock.json` records the exact Edict and Echo commits this repository
+is proven against. Every build boundary calls `tests/producer-lock.sh` first
+and refuses a checkout that is not those commits, or that has uncommitted
+changes, so a stale or locally modified producer fails loudly instead of
+producing a misleading result. A commit id alone would not catch the second
+case: edits to the producer leave `rev-parse` reporting the pinned commit while
+the build compiles different sources. CI reads the same file and
+checks the producers out at those commits.
+
+Advancing a producer means changing that file in the same commit as the
+re-vendored artifacts it implies.
+
 ## Local build
 
-Set `EDICT_REPO` and `ECHO_REPO` to compatible local checkouts, then run:
+Set `EDICT_REPO` and `ECHO_REPO` to checkouts at the pinned commits, then run:
 
 ```sh
 EDICT_REPO=/path/to/edict \
@@ -139,10 +153,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`. Edict validates that
+closure; Hello Echo corroborates the artifacts and invokes the validator.
 
 The fixed suite contains one ordered golden path, one relative
 compiler-artifact path probe, one idempotent retry, one conflicting retry, one
@@ -160,3 +182,112 @@ 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`. Edict recomputes and validates the complete closure
+and refuses a malformed, missing, substituted, or unresolved resource. Hello
+Echo corroborates those artifacts byte-for-byte and invokes that validator; it
+does not reparse Edict source.
+
+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.