[avrabe]

The v0.90 review record, plus the corrections it calls for. One signed commit.

What it adds

docs/reviews/v0.90-cold-review.md holds the two-round cold review of 80f8676 with a # v0.90 — coordinator disposition section appended.

• The first 63045 bytes are byte-identical to the frozen two-round copy, sha256 428edbf4…ce94c3. The first 29642 bytes (round 1) give f41f9750…6a85a.
• diff <frozen> <record> | grep -c '^<' gives 0. A negative control, one byte changed inside the prefix, makes the prefix check fail.
• The total is 80190 bytes. The record states that figure as a fixed point, and wc -c was re-run after the last edit.

Corrected sites (before → after)

1. CHANGELOG [0.90.0], New loud refusals, #1640 bullet.

• Before: "312 no-target self-contained compiles … newly refuse (133 --all-exports, 179 --func-name)".
• After: two units, not summed. 133 module-level compiles (--all-exports, and equally the default synth compile x.wat, which takes the same path), and 978 --func-name compiles in 185 files. That is 197 distinct files. The note says PR v0.90 A32CALL (#1645): self-contained A32 images patch every internal bl and enter A32 code in ARM state #1662's 179 compiled only the first export of each file.

2. CHANGELOG, the #1645 bullet.

• Before: "48 newly refuse".
• After: 107 --func-name compiles of a calling function, in 65 files. The two refusals together affect 212 distinct files. PR v0.90 A32CALL (#1645): self-contained A32 images patch every internal bl and enter A32 code in ARM state #1662's 48 is labelled a first-export sample.

3. RQ-90-A32ENTRY verified-by, the REACH paragraph.

• Before: "312 no-target self-contained compiles (133 --all-exports, 179 single-function)".
• After: the PR's 133 and 179 stay, dated to its own base pair and labelled a one-per-file first-export sample, not summed. The every-export figures (133, 978 in 185 files, 197 files) are attributed to the v0.90 cold review's re-derivation on v0.89.2 against 0.90.0.

4. RQ-90-A32CALL verified-by.

• Before: "48 cortex-r5 single-function compiles of a calling export are newly refused".
• After: the 48 is labelled as the first-export sample, plus the every-export figure: 107 compiles, in 65 files.

5. RQ-90-GATEPLACE description.

• Before: "spec-suite execution (#1636), which v0.90 SPECEXEC (#1636): promote spec-suite execution to a required context #1670 added".
• After: the context was added to branch protection directly, not by a PR, between 2026-11-06T20:34:14Z and 2026-11-07T00:08:51Z, on ci: spec suite should execute, not only compile, and be required #1636's acceptance criterion. v0.90 SPECEXEC (#1636): promote spec-suite execution to a required context #1670 only moved the name from PENDING_REQUIRED_CONTEXTS into REQUIRED_CONTEXTS in scripts/ci_pool_tripwire.py. "nine required status checks" now reads "… of v0.89".

6. RQ-90-GATEPLACE verified-by and the CHANGELOG Compliance envelope.

• Before: "kept the required set as it is (The three new wrong-code differentials and the moved island floor sit outside the required checks #1573)" / "with no branch-protection change", next to the set going from 9 to 10.
• After: the keep-as-is decision covers The three new wrong-code differentials and the moved island floor sit outside the required checks #1573's wrong-code differentials (no ci.yml job that runs them became required). The tenth context was a separate request, ci: spec suite should execute, not only compile, and be required #1636's own acceptance criterion, and main now requires 10 checks.

7. Six records: A32BRANCH, A32GUARD, F64STORE, FALCON7, MEMKFIXTURE and NPASHAPE2.

• Before: verification-track: manual beside verified-by prose saying "execution-verified".
• After: verification-track: execution, matching the prose and the v0.89.1 and v0.89.2 precedent. No script reads the field.

Re-derivation (F1)

Fresh cargo build --release -p synth-cli --features verify binaries:

• 0.90.0 from 80f8676, sha256 prefix bad16d49136ae2e1.
• 0.89.2 from git archive v0.89.2, sha256 prefix 23dc9ea26da805f5.

The census covers the 268 files from git ls-files '*.wat' '*.wasm' × {no target, cortex-r5} × {default, --all-exports, --func-index 0, --func-name for every export}. That is 4452 jobs per binary, with 0 harness errors. The export reader agrees with wasmtime on 263 of 263 files.

cell	newly refused
no target, --all-exports	133
no target, default	133
no target, --func-name	978 (185 files)
no target, --func-index 0	169
cortex-r5, --func-name	107 (65 files)

• Default and --all-exports give the same result in 1072 of 1072 pairs.
• 197 files are affected with no target, 212 including cortex-r5.
• The first-export samples reproduce 179 and 48 exactly, which is the positive control.
• Every refusal carries the SILENT MISCOMPILE: self-contained A32 images (cortex-r5, default no-target) enter A32 function bodies in Thumb state #1640 or HANG: the self-contained --target cortex-r5 image ships every internal A32 bl unpatched (ebfffffe, a branch-and-link to itself) and reports "Internal calls: 1 resolved in place", exit 0 #1645 message, and nothing flips the other way.

Gates (at the commit, from the repo root)

gate	result
claim_check.py claims.yaml	77/77, rc 0
status_evidence_check.py	rc 0, 0 failures; issue-scope 15 authorised, 2 held open
verdict_prose_check.py	rc 0; 218 classified, 0 disagree
issue_closure_check.py --release v0.90 --since-tag v0.89.2 --allow-unclosed	rc 0: 15 authorised, 2 held open (#1604 and #1568), 4 closed, 0 failures
release_file_statistics_scan.py --release v0.90	rc 0; 2 word-number hits, _release.yaml lines 32-33 ("this one", "the planned one"). Judgement: both IDIOM.
check_py_floor.py (--self-test, then every tracked .py, under Python 3.9.6)	rc 0, 321 files, 0 findings
Claim Check job, every run: step of ci.yml claim-check run whole under bash -o pipefail -e	54 of 54 rc 0. Step 53 (the evidence ledger) first went red because the sweep harness omitted the workflow-level env ORACLE_EVIDENCE_JSONL; re-run with the workflow env, steps 52 and 53 give rc 0
live tripwire, ci_pool_tripwire.py (not --offline)	rc 0: "pinned required contexts match branch protection", 10 contexts, 0 failures
review_record_provenance_check.py	rc 0

loop_conformance_check.py v0.90.0 with HEAD at the commit: verdict DOES-NOT-CONFORM, slots 7, derived 5, attested 1, failures 1. The one failure is step 5's "mcdc ran on commit", which is NOT-DERIVED because the commit was not yet pushed. Each step:

step	check	result
0	release identity	DERIVED-PASS
1-2	spar AADL→WIT	NA-FILED (RQ-90-ARCHMODEL11, proposed)
3	artifact set; reported outcome; verdict classified; status-evidence gate; live run	DERIVED-PASS on all five
4	oracle wiring with --exact-emulation-floor 449389; live run	DERIVED-PASS
5	mcdc gate	DERIVED-PASS
5	mcdc ran on commit	NOT-DERIVED; once pushed, pending until MC/DC finishes on this head
6	signing workflow; Signing E2E (pre-tag form)	DERIVED-PASS
7	cold-review record	DERIVED-PASS: declares reviewed commit 80f8676, an ancestor of the release commit and not an ancestor of v0.89.2
8	pin sweep; changelog structure	DERIVED-PASS
8	PR-head-vs-merge	ATTESTED
8	crates and npm	NA-BY-MOMENT

Squash simulation

commit-tree builds this branch's tree on parent 80f8676, in a clone in scratch. Then status_evidence_check.py runs on each result. The two runs differ only in the subject:

• Subject v0.90 cold review: record the review and correct the statements it found (#1674), which is what a squash produces: rc 0. "12 delivery-shaped commits since v0.89.2 — 12 attributed". The subject is not lane-shaped (lower case after the version) and is not a conventional delivery type.
• Control, the lane-shaped v0.90 COLDREVIEW (#1674): … on the identical tree: rc 1, FAIL R10-lane: … names artifact RQ-90-COLDREVIEW, which no release file defines, 13 delivery-shaped.

Not in this PR

Nothing is merged, tagged or posted. U2 (274 assert_return and 177 assert_trap under software) is recorded as UNPROVEN, because round 2 says so in the record. A1, the acceptance corpus, is NOT measured: the corpus volume is not mounted on this machine. The disposition lists what is carried to v0.91.

Refs #1640
Refs #1645
Refs #1573
Refs #1636

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!