Mac-first completion: platform crate, AArch64 tiers, emit and runtime conformance, review fixes

.gitattributes

@@ -1,2 +1,6 @@
+# Digests under corpus/ and vendor/ pin the exact bytes of text files, so a
+# checkout must not rewrite line endings, whatever core.autocrlf says.
+* text=auto eol=lf
+
 # Upstream performance fixtures are immutable byte artifacts.
 perf/fixtures/upstream/* -text

.gitignore

@@ -24,3 +24,4 @@ perf/fixtures/boundary/
 !/.outline/gates/
 !/.outline/GATES.md
 !/.outline/type-script-7.0.2-completion.md
+/tasks/

.outline/gates/A3.1.md

@@ -30,4 +30,4 @@ EVIDENCE: 2026-09-03 sweep complete: 2048/2048 shards merged to verification/evi
 - [ ] G6: Baseline generation and ledger rebuild pass their narrow repository checks
   CHECK: just leaf-gate A3.1
   EXPECT: LEAF A3.1 PASS
-EVIDENCE: 2026-09-03 structurally blocked, measured two ways: ledger rebuild --write exit 1 E_SET_MISMATCH with 248828 rejections (merged receipt StaleBinding on candidate_tree_digest plus unreceipted benchmark/formal/test262 obligations); re-running suite merge on 0b5bdde exit 1 E_DIGEST, shards stale for the current binding. Landing a receipt changes HEAD^{tree} which the receipt binds, so no committed receipt can be admitted; guards at crates/bamts-verification/src/rebuild.rs:613-624 plus the dirty-tree gate (28dc143, postdates ledger 5e83845). A2.6 G3 tests rejects_stale_receipt as a met gate, so the guard is intentional and must not be relaxed to force a green; the landing-sequence change belongs to its owners.
+EVIDENCE: 2026-11-01 no longer structurally blocked: at f640f63 a target-cells receipt was measured, committed under verification/evidence/typescript-7.0.2/ in the next commit, and `ledger rebuild --check` there rejected only the older x86_64 receipt as stale, not it; one source change then made it stale too (355473 to 355474 rejections). The gate stays open until `just leaf-gate A3.1` passes. Earlier record: 2026-09-03 structurally blocked, measured two ways: ledger rebuild --write exit 1 E_SET_MISMATCH with 248828 rejections (merged receipt StaleBinding on candidate_tree_digest plus unreceipted benchmark/formal/test262 obligations); re-running suite merge on 0b5bdde exit 1 E_DIGEST, shards stale for the current binding. Landing a receipt changes HEAD^{tree} which the receipt binds, so no committed receipt can be admitted; guards at crates/bamts-verification/src/rebuild.rs:613-624 plus the dirty-tree gate (28dc143, postdates ledger 5e83845). A2.6 G3 tests rejects_stale_receipt as a met gate, so the guard is intentional and must not be relaxed to force a green; the landing-sequence change belongs to its owners.

.outline/gates/B7.2.md

@@ -0,0 +1,33 @@
+# Gates: B7.2 historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter
+
+Scope: B7.2 owns crates/bamts-verification/src/historical.rs; it delivers historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter.
+
+- [ ] G1: historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter: the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf B7.2 --aspect contract
+  EXPECT: LEAF B7.2 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter: every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf B7.2 --aspect evidence
+  EXPECT: LEAF B7.2 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter: the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf B7.2 --aspect coverage
+  EXPECT: LEAF B7.2 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter: no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf B7.2 --aspect regression
+  EXPECT: LEAF B7.2 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter: the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf B7.2 --aspect mutation
+  EXPECT: LEAF B7.2 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: historical 6.0.2 and 5.9.3 catalog ownership and 7.0.2 applicability filter: the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate B7.2
+  EXPECT: LEAF B7.2 PASS
+  EVIDENCE: pending

.outline/gates/E2.4.md

@@ -0,0 +1,33 @@
+# Gates: E2.4 JIT execution and W^X proof on Apple Silicon
+
+Scope: E2.4 owns crates/bamts-codegen/src/jit_memory.rs; it delivers JIT execution and W^X proof on Apple Silicon.
+
+- [ ] G1: JIT execution and W^X proof on Apple Silicon: the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E2.4 --aspect contract
+  EXPECT: LEAF E2.4 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: JIT execution and W^X proof on Apple Silicon: every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E2.4 --aspect evidence
+  EXPECT: LEAF E2.4 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: JIT execution and W^X proof on Apple Silicon: the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E2.4 --aspect coverage
+  EXPECT: LEAF E2.4 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: JIT execution and W^X proof on Apple Silicon: no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E2.4 --aspect regression
+  EXPECT: LEAF E2.4 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: JIT execution and W^X proof on Apple Silicon: the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E2.4 --aspect mutation
+  EXPECT: LEAF E2.4 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: JIT execution and W^X proof on Apple Silicon: the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E2.4
+  EXPECT: LEAF E2.4 PASS
+  EVIDENCE: pending

.outline/gates/E3.4.md

@@ -0,0 +1,33 @@
+# Gates: E3.4 native executable link and run on macOS hosts
+
+Scope: E3.4 owns crates/bamts-cli/src/driver.rs; it delivers native executable link and run on macOS hosts.
+
+- [ ] G1: native executable link and run on macOS hosts: the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.4 --aspect contract
+  EXPECT: LEAF E3.4 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: native executable link and run on macOS hosts: every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.4 --aspect evidence
+  EXPECT: LEAF E3.4 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: native executable link and run on macOS hosts: the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.4 --aspect coverage
+  EXPECT: LEAF E3.4 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: native executable link and run on macOS hosts: no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.4 --aspect regression
+  EXPECT: LEAF E3.4 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: native executable link and run on macOS hosts: the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.4 --aspect mutation
+  EXPECT: LEAF E3.4 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: native executable link and run on macOS hosts: the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E3.4
+  EXPECT: LEAF E3.4 PASS
+  EVIDENCE: pending

.outline/gates/E3.5.md

@@ -0,0 +1,35 @@
+# Gates: E3.5 native executable link and run on Windows MSVC
+
+Scope: E3.5 owns crates/bamts-cli/src/windows_link.rs; it delivers native executable link and run on Windows MSVC.
+
+Status: the owned file does not exist at this commit. `crates/bamts-cli/src/driver.rs` still links with `cc ... -o`, which is not an MSVC command line, and the platform crate has no Windows implementation, so native output is unwritten. It is the deliverable of the `windows-native-output` card, which needs the Windows host. Until then this leaf stays open and ownership checks report the file as missing.
+
+- [ ] G1: native executable link and run on Windows MSVC: the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.5 --aspect contract
+  EXPECT: LEAF E3.5 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: native executable link and run on Windows MSVC: every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.5 --aspect evidence
+  EXPECT: LEAF E3.5 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: native executable link and run on Windows MSVC: the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.5 --aspect coverage
+  EXPECT: LEAF E3.5 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: native executable link and run on Windows MSVC: no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.5 --aspect regression
+  EXPECT: LEAF E3.5 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: native executable link and run on Windows MSVC: the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.5 --aspect mutation
+  EXPECT: LEAF E3.5 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: native executable link and run on Windows MSVC: the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E3.5
+  EXPECT: LEAF E3.5 PASS
+  EVIDENCE: pending

.outline/gates/E3.6.md

@@ -0,0 +1,33 @@
+# Gates: E3.6 shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host
+
+Scope: E3.6 owns crates/bamts-platform/; it delivers shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host.
+
+- [ ] G1: shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host: the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.6 --aspect contract
+  EXPECT: LEAF E3.6 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host: every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.6 --aspect evidence
+  EXPECT: LEAF E3.6 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host: the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.6 --aspect coverage
+  EXPECT: LEAF E3.6 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host: no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.6 --aspect regression
+  EXPECT: LEAF E3.6 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host: the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.6 --aspect mutation
+  EXPECT: LEAF E3.6 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: shared platform facts: host triple, machine facts, process regions, and peak memory on every execution host: the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E3.6
+  EXPECT: LEAF E3.6 PASS
+  EVIDENCE: pending

.outline/gates/E3.7.md

@@ -0,0 +1,33 @@
+# Gates: E3.7 in-process AOT linking on every execution host
+
+Scope: E3.7 owns crates/bamts-codegen/src/aot/in_process_link.rs; it delivers in-process AOT linking on every execution host.
+
+- [ ] G1: in-process AOT linking on every execution host: the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.7 --aspect contract
+  EXPECT: LEAF E3.7 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: in-process AOT linking on every execution host: every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.7 --aspect evidence
+  EXPECT: LEAF E3.7 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: in-process AOT linking on every execution host: the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.7 --aspect coverage
+  EXPECT: LEAF E3.7 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: in-process AOT linking on every execution host: no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.7 --aspect regression
+  EXPECT: LEAF E3.7 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: in-process AOT linking on every execution host: the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E3.7 --aspect mutation
+  EXPECT: LEAF E3.7 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: in-process AOT linking on every execution host: the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E3.7
+  EXPECT: LEAF E3.7 PASS
+  EVIDENCE: pending

.outline/gates/E4.2.md

@@ -2,6 +2,8 @@
 
 Scope: E4.2 owns verification/toolchains/x86_64-unknown-linux-gnu.json; it delivers x86_64-unknown-linux-gnu cell closure (native host).
 
+Status: the owned file does not exist at this commit. Commit 1352e7b removed it because its obligations were renamed, and evidence must be re-measured, not rewritten. A native `x86_64` `rustc` has to measure it again, on the `bamti-x64` VM profile. Until then this leaf stays open and ownership checks report the file as missing.
+
 - [ ] G1: x86_64-unknown-linux-gnu cell closure (native host): the declared public contract vectors pass
   CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.2 --aspect contract
   EXPECT: LEAF E4.2 CONTRACT PASS

.outline/gates/E4.6.md

@@ -0,0 +1,33 @@
+# Gates: E4.6 aarch64-apple-darwin cell (native host)
+
+Scope: E4.6 owns verification/toolchains/aarch64-apple-darwin.json; it delivers aarch64-apple-darwin cell (native host).
+
+- [ ] G1: aarch64-apple-darwin cell (native host): the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.6 --aspect contract
+  EXPECT: LEAF E4.6 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: aarch64-apple-darwin cell (native host): every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.6 --aspect evidence
+  EXPECT: LEAF E4.6 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: aarch64-apple-darwin cell (native host): the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.6 --aspect coverage
+  EXPECT: LEAF E4.6 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: aarch64-apple-darwin cell (native host): no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.6 --aspect regression
+  EXPECT: LEAF E4.6 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: aarch64-apple-darwin cell (native host): the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.6 --aspect mutation
+  EXPECT: LEAF E4.6 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: aarch64-apple-darwin cell (native host): the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E4.6
+  EXPECT: LEAF E4.6 PASS
+  EVIDENCE: pending

.outline/gates/E4.7.md

@@ -0,0 +1,35 @@
+# Gates: E4.7 x86_64-apple-darwin cell (Rosetta)
+
+Scope: E4.7 owns verification/toolchains/x86_64-apple-darwin.json; it delivers x86_64-apple-darwin cell (Rosetta).
+
+Status: the owned file does not exist at this commit. The record is measured by `toolchain measure --target x86_64-apple-darwin`, whose two run obligations need Rosetta, and Rosetta is not installed on the measuring Mac. That is the human task `install-rosetta`, then the `macos-target-cells` card. Until then this leaf stays open and ownership checks report the file as missing.
+
+- [ ] G1: x86_64-apple-darwin cell (Rosetta): the declared public contract vectors pass
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.7 --aspect contract
+  EXPECT: LEAF E4.7 CONTRACT PASS
+  EVIDENCE: pending
+
+- [ ] G2: x86_64-apple-darwin cell (Rosetta): every selected logical obligation has a current content-addressed receipt
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.7 --aspect evidence
+  EXPECT: LEAF E4.7 EVIDENCE PASS
+  EVIDENCE: pending
+
+- [ ] G3: x86_64-apple-darwin cell (Rosetta): the scoped obligation set has zero blocking, external-blocked, catalog-error, timeout, crash, skip, or missing-receipt states
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.7 --aspect coverage
+  EXPECT: LEAF E4.7 COVERAGE PASS
+  EVIDENCE: pending
+
+- [ ] G4: x86_64-apple-darwin cell (Rosetta): no previously passing obligation regressed
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.7 --aspect regression
+  EXPECT: LEAF E4.7 REGRESSION PASS
+  EVIDENCE: pending
+
+- [ ] G5: x86_64-apple-darwin cell (Rosetta): the registered mutation makes its contract gate fail
+  CHECK: cargo run -p bamts-verification -- completion verify --leaf E4.7 --aspect mutation
+  EXPECT: LEAF E4.7 MUTATION PASS
+  EVIDENCE: pending
+
+- [ ] G6: x86_64-apple-darwin cell (Rosetta): the owned code passes its narrow repository build, lint, format, and behavioral checks
+  CHECK: just leaf-gate E4.7
+  EXPECT: LEAF E4.7 PASS
+  EVIDENCE: pending