docs(todo): two clauses written as unobservable have been observed

Both lines were held `[>]` by a sentence about what this machine cannot
see, and both close by reading a run rather than by changing anything in
the tree.

E0-R01 wanted two runners at one commit to produce one content address.
On run 34370629685 both printed b197ec06… at /__w/f/f and the third job
printed `agreed`. The sentence that used to close the line — a workflow
that has not run is a wrapper that has not run, and E0-B16 is this file's
scar for treating those as the same thing — was right, and is discharged
rather than withdrawn.

E1-P11 wanted the AArch64 job green. It is, on `ubuntu-24.04-arm`, and
the counts came out equal: 48 test binaries and 862 tests on each side.
`lint-arch-tests` remains what asserts the property. The equal count is
corroboration, and it rules out the one failure that task's own paragraph
predicts — green on both runners while one quietly collects fewer tests.

The title keeps *under emulation*. RFC 0045 already resolved that phrase
to the arm runner rather than to a local command, and ci.yml records at
the job why native silicon is the stronger check rather than the equal
one: TCG serialises rather than reordering, so an emulated run would be
green whatever the ordering said.

In both entries the superseded sentences are kept and marked rather than
deleted, because a verdict somebody unmade is the useful part.
ARCH_RUN_GAP is untouched: it is a statement about this machine, which
has not changed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: dimmus

TODO.md

@@ -634,12 +634,17 @@ load-bearing.*
   That is a weaker criterion than the one this task was written with, and it is the one the evidence supports. The stronger criterion did not go unmet through lack of effort; it was asked of CI twice and answered twice, and both answers are above. What is owed now is a model check, and `E0-P16` owns it with the two fixtures already built and waiting — which is a better position than this task started in, where the exit named a defect that did not exist.
   *needs:* E0-B12
 
-- [>] **E0-R01** `M` `cargo xtask release` produces the full package: source tag, claims snapshot, content-addressed QEMU image, seed corpus, baseline configurations, and a dependency manifest.
+- [x] **E0-R01** `M` `cargo xtask release` produces the full package: source tag, claims snapshot, content-addressed QEMU image, seed corpus, baseline configurations, and a dependency manifest.
   It builds: one `.tar`, a `MANIFEST` naming every file and its SHA-256, and one content address over the archive. Twenty-four files and one address, from `cargo xtask release`.
   **The crux was the two contents no E0 task produces**, and getting it wrong in either direction was easy. Shipping the package with them missing makes the contract advisory, and shortening the list to fit the work is the silent scope cut `A-07` stands against and `E0-D08` already caught once. So the requirement is a **predicate over the registry**: a content is owed when the claim that needs it publishes a number. The baseline and the seed corpus both serve `ring-submit-latency`, which is `pending`; the day it is not, the packager refuses and names `E1-D06`. A scope cut becomes a gate with a known trigger, and the trigger is a status change in `claims/` rather than an edit to the tool. RFC 0021, which also states the consequence rather than leaving it to be found: `E0-R04` needs `E0-P05`, `E0-P05` makes 0001 gating, and a gating 0001 publishes `ratio_vs_baseline` against `linux-6.x-tuned` — so release 0.1 pulls `E1-D06` forward or does not publish that ratio.
   **SHA-256 and the archive writer are in the tree, and that is the contract's own rule rather than taste.** `release --dry-run` computed hashes by shelling out to `sha256sum`, so the content address of a release depended on which coreutils the machine had — and on a machine without it the manifest simply printed no hash column. An address that is sometimes absent is not an address. `xtask/src/pack.rs` is both, checked against FIPS 180-4's published vectors, in a file whose whole subject is that it has no variable fields: no mtime, no uid, no user name, no directory order, and no compression, because a deflate stream carries its encoder's version into the bytes.
   The source is `git archive` of the commit rather than a walk of the working tree — it takes its file list from the tree object and its mtimes from the commit, so it cannot pick up an untracked file and cannot vary with when the checkout happened.
-  *exit:* **half met, and the other half is now asked rather than deferred.** `cargo xtask release --twice` packages the same tree twice and requires one address; it passes, and the command says in its own output why that is the weaker half — directory order, uid, path and clock are all constant within one machine. The real question needs two runners at one commit, and `cargo xtask release --address` plus the `package` and `address` jobs are what ask it: one line per runner, compared by a third job. Still `[>]`, because a workflow that has not run is a wrapper that has not run, and `E0-B16` is this file's scar for treating those as the same thing.
+  *exit:* **met, and what was owed was a run rather than a change.** `cargo xtask release --twice` packages the same tree twice and requires one address; it passes, and the command says in its own output why that is the weaker half — directory order, uid, path and clock are all constant within one machine. The real question needs two runners at one commit, and `cargo xtask release --address` plus the `package` and `address` jobs are what ask it: one line per runner, compared by a third job. Still `[>]`, because a workflow that has not run is a wrapper that has not run, and `E0-B16` is this file's scar for treating those as the same thing. **The wrapper has now run, and that was the whole of what was left.** The sentence immediately above it — *still `[>]`, because a workflow that has not run is a wrapper that has not run* — was right when it was written and is discharged rather than withdrawn: nothing in this tree was edited to close this line, a runner simply did the thing the wrapper wraps. On **run 34370629685**, the merge of #31 into `main` on 2026-09-09, `package address (runner a)` and `package address (runner b)` each printed one address and the path it was built at, and `the content address check` printed `agreed`:
+  ```
+  runner a  b197ec06dbec7414feafbc21baabd5bd7d251547a62536d184680c905b2e3824  at /__w/f/f
+  runner b  b197ec06dbec7414feafbc21baabd5bd7d251547a62536d184680c905b2e3824  at /__w/f/f
+  ```
+  Two machines, one commit, one address. The workspace-path precondition held by construction on both, as the job's own comment said it would, so the comparison never had to tell a path difference from a finding. **That address is evidence of an agreement and not a constant to check against**, for exactly the reason the two numbers below are evidence of a difference: the line recording it is inside the source archive the address is taken over, so writing it down changed it. The next run's number will differ from this one and that is not a regression.
   **The same-path precondition was stated here as an argument and is now a measurement**, which matters because the whole job is built on it. The same tree, same image, same commit, packaged at two paths:
   ```
   /work        e544abc2009007758433d33c51e00650190b045d060f09677be29c4be76cbc13
@@ -909,10 +914,10 @@ everything after this cheap to debug.*
 - [ ] **E1-P10** `M` Claims for the datapath: ring submit under load, doorbells per operation, copies per operation, kernel entries per operation.
   *exit:* four claims, gating, each with a tuned-Linux baseline where one exists.
   *needs:* E1-B09
-- [>] **E1-P11** `M` Cross-architecture CI: the AArch64 job builds and runs the same suite under emulation.
+- [x] **E1-P11** `M` Cross-architecture CI: the AArch64 job builds and runs the same suite under emulation.
   **The architecture list is derived from the workspace** (RFC 0045), which removes the failure this task existed to remove: `cargo xtask test` cross-compiled a hand-written list of crates, and a hand-written list stops matching the workspace silently — `xtask` already carried a comment recording that exact thing happening once, to `f-bench` and `f-init`. Every crate is now either built for AArch64 or excluded with its reason in the source, and a new crate is included by default.
   **Then the review found the gap the crate list leaves**, and it is the difference between the two halves of this exit: a crate can be on both runners with an architecture `cfg` on a test *inside* it, so the job stays green while one machine collects fewer tests — and a test count is not an assertion. `cargo xtask lint-arch-tests` reads the gate where it is written, including on a `mod` declaration and everything that file declares in turn, because `user/init/src/component.rs` carries no trace of the gate that excludes it.
-  *exit:* **half met, and the other half is not observable from here.** No test is skipped on AArch64 without a recorded reason, and that is now checked rather than reviewed. *Green* is a statement about a job that runs only on an arm runner; no such runner and no way to execute an AArch64 hosted binary exists on this machine or in the container, so nothing local can observe it. It is the same honest gap `CLAUDE.md` already records — the AArch64 job is where the ring's ordering means anything, and nothing local substitutes for it.
+  *exit:* **met, and what changed is where somebody looked rather than anything in the tree.** No test is skipped on AArch64 without a recorded reason, and that is now checked rather than reviewed. *Green* is a statement about a job that runs only on an arm runner; no such runner and no way to execute an AArch64 hosted binary exists on this machine or in the container, so nothing local can observe it. It is the same honest gap `CLAUDE.md` already records — the AArch64 job is where the ring's ordering means anything, and nothing local substitutes for it. **Every sentence above is still true, and not one of them was a verdict on this task** — *not observable from here* is not *not observed*, and the observation was one `gh run view` away for as long as the sentence stood unread. **Run 34370629685**, the merge of #31 into `main` on 2026-09-09, carries `tests (AArch64, weak memory)` and `memory-ordering litmus (AArch64, weak memory)`, both green, on `ubuntu-24.04-arm`. **The counts came out equal too**, which this task's own paragraph says a green job does not establish: 48 test binaries and 862 tests on x86-64, 48 and 862 on AArch64, in that run. `cargo xtask lint-arch-tests` is still what asserts it and the equality is only corroboration — but the failure that paragraph predicts, green on both runners while one collects fewer tests, is the one thing an equal count rules out, and it is ruled out. **The title keeps *under emulation* rather than being edited to match the runner.** RFC 0045 already resolved that phrase to the arm runner rather than to a local command, and `ci.yml` states the reason at the job: TCG serialises rather than reordering, so an emulated run would be green whatever the ordering said. Native silicon is the stronger check and not the equal one, so the word stays and this paragraph is what a reader comparing the two should find. `ARCH_RUN_GAP` is untouched and stays true: it is a statement about *this machine*, which has not changed, and closing this line on a runner is precisely what it was written to permit.
 - [>] **E1-P12** `M` Kani on the ring's validation paths: panic-freedom proved, not sampled.
   `E1-P07` proves the capability properties; the same tooling reaches the other structure a hostile peer feeds bytes to. `pop`, `take`, `Layout::adopt` and `execute` each promise that nothing a peer writes produces a panic, and today that promise rests on fuzzing that samples and a clippy wall that guards this crate's own code. A bounded proof over arbitrary header bytes, cursors and entries is cheap for code this small, and it is the difference between "no fuzzer found one" and "there is none".
   **The fixture is a region of bytes, not a struct of fields**, and `ring/src/mapping.rs` had already named that trap: a channel assembled from fields a harness owns can only ever be laid out correctly. So the proof hands 640 symbolic bytes to the real `adopt`, and the header, both cursor pairs, the flags word, the index ring, both entry arrays and the arena are then *the same bytes*. Cursors and index-ring slot numbers are unbounded. That is what makes the unchecked index a proof obligation rather than a fuzzing target.