perf(compiler): qualify Prism model lowering and Atlas proofs

.github/workflows/ci.yml

@@ -94,7 +94,7 @@ jobs:
         run: |
           set -euo pipefail
           grep -F "verify-examples: uor-atlas verified (attestation " ci-evidence/vv.txt
-          grep -F "verify-examples: uor-atlas: 267 normalized verification records equal expected/verify (§29.5)" ci-evidence/vv.txt
+          grep -F "verify-examples: uor-atlas: 695 normalized verification records equal expected/verify (§29.5)" ci-evidence/vv.txt
       - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         if: ${{ !cancelled() }}
         with:

SPEC.md

@@ -2462,6 +2462,15 @@ source/IR limits, kernel replay, and exact axiom policies remain unchanged.
 Exhausting a finite Lean budget still fails verification; the budgets do not
 assert that every resource-bounded source can be verified on every host.
 
+Semantic byte literals lower each octet through `_root_.UInt8.ofNat (nat_lit n)`.
+Within a closed literal, values appearing at least four times share ascending
+typed local bindings. The literal's local scope cannot capture source binders;
+root-qualified constructors preserve names under shadowing. Literal byte values,
+order and canonical LaTeX decimal spelling remain unchanged. Compiler-bound
+source, snapshot, build and verification identities regenerate with the backend
+revision. These rules apply to both language 1.1 and 1.2, including model and
+well-founded definition lowering.
+
 ### 17.12 Language 1.2 and the compatibility/migration contract
 
 Language 1.2 is selected by `language = "1.2"` in `lexlean.toml`. It is a

VERIFICATION.md

@@ -4,6 +4,48 @@ How this repository's claims are checked, which recipe enforces which rule, and
 
 ## The acceptance gate
 
+### Reviewed Prism compiler checkpoint — 6 October 2026
+
+The combined tree through `efd4ca7c` passed the original complete `just vv`
+and subsequent `cargo xtask check-package` in pinned `670b191a` tooling.
+Execution used the frozen dirty tree at `b0a349ed`; independent review matched
+all 5,924 input paths and hashes to the committed combined tree. Intermediate
+commits are not individually qualified by this run.
+
+- Original conformance: 291 passed, none filtered or skipped; all other
+  original VV recipes, example verification, golden readback and two-root
+  reproducibility passed.
+- Atlas: 173 source modules, 866 build files, 695 normalized verification
+  records; all 107 added census leaves are directly imported. Original
+  statements and axiom policies remain unchanged. Twenty-two original proofs
+  additionally observe the already-allowed `Quot.sound`.
+- MD-02 executes generated artifact values through pinned Lean and rejects a
+  successfully compiled byte-corruption counterexample.
+- Input inventory SHA-256:
+  `3f22b75833eac06c49d27ce9368afd22b56a56d7257df3634ccbf80c3950eee3`.
+- Complete gate log SHA-256:
+  `582375a144a94a234b4962ce0f982598e7083dbd262942d1aaec38743cdadd99`.
+
+Earlier failed/interrupted attempts remain failures. This is actual local
+full-gate/package evidence, not hosted CI, a release, or installed Prism SDK
+qualification. This documentation was added after execution.
+
+### Legacy configuration/CLI coverage replacement — 6 October 2026
+
+Independent review maps all 29 valid executable obligations from the removed
+six-file `tests/e2e` suite to existing conformance owners. CF-07/10/16/17 and
+CL-02/12 now additionally execute malformed/unsupported lock refusals, digest
+drift and non-repair, real 1.0-to-1.1 migration, the explicit 1.1 lifecycle and
+complete version/diagnostic/color combinations. Positive projects are valid
+for their declared language; no unsupported-language success is fabricated.
+
+All six complete owners passed in pinned `670b191a` tooling: six passed,
+285 explicitly filtered, 11.77 seconds; their inputs remained unchanged.
+Log SHA-256:
+`5f1c74ff75a331fc878713ea303950525fc842ce145b587ccb7419a94f4f27d1`.
+This selected-owner run qualifies the coverage replacement only. It is not
+a new 291-case/full-VV, downstream compiler or installed SDK qualification.
+
 `just vv` runs, in the normative order (SPEC.md §9.2):
 
 | Recipe | Command | Rules it enforces |
@@ -15,7 +57,6 @@ How this repository's claims are checked, which recipe enforces which rule, and
 | `test` | `cargo test --workspace --all-features --exclude repo-conformance` | §28.1 classes 1–2 and 4–5 (unit, property, integration, CLI) and the model crate's own tests. `repo-conformance` is excluded here and owned solely by `bdd`, so each conformance test and each Lean process behind it runs once per `vv` rather than twice |
 | `bdd` | `cargo test -p repo-conformance` | R3, §27.7, §27.8: the complete conformance suite — all 291 conformance tests, including the §28.2 fixture suite (`conformance_ex_07`) and the crate-packaging round trip (`conformance_rp_12`) — plus the register ↔ scenario ↔ test bijection, the meta-gate, and its own falsifiability test. Sole owner of that suite: `test` above excludes it |
 | `features` | `cargo check --workspace --all-features --all-targets` | every target compiles |
-| `bdd` | `cargo test -p repo-conformance` | R3, §27.7, §27.8: the complete conformance suite — all 291 conformance tests, including the §28.2 fixture suite (`conformance_ex_07`) and the crate-packaging round trip (`conformance_rp_12`) — plus the register ↔ scenario ↔ test bijection, the meta-gate, and its own falsifiability test. Sole owner of that suite: `test` above excludes it |
 | `examples` | `cargo xtask verify-examples` | §28.6, EX-01: every example directory and the `compiler` project (§17.14, §17.15) format, lock, check, build, and verify with real Lean 4.32.1; when an example commits `expected/verify/`, its normalized verification records must equal it (§29.5) |
 | `golden` | `cargo xtask check-golden` | R10, §28.3: the *published* build tree of a real `build` in a fresh directory equals the committed oracles byte for byte |
 | `repro` | `cargo xtask check-reproducibility` | AR-13, §28.4: two clean `build`s in distinct absolute directories publish byte-identical trees with no absolute path inside |
@@ -150,6 +191,13 @@ struct-literal source change; it does not alter the diagnostic wire schema.
 
 ### semantic elaboration budgets can fail
 
+The typed-octet integration runs this complete nested corpus under language
+1.1 and 1.2, each with repeated and varied bytes. The complete SM-19 case
+passes in 127.92 seconds after the extension; all six semantic-backend unit
+owners also pass. The retained log SHA-256 is
+`06ecd37c4974ed997c8f6e647a7a3b7632e5cb15c00a83a38f29e64e6485b657`.
+This targeted execution is not complete V&V or package/downstream acceptance.
+
 The `SM-19` regression generates one nested record/list declaration containing
 twenty byte literals, including 4,096-, 4,097-, and 8,192-byte values. It keeps
 the complete consumer corpus shape, checks every ordered literal against both

compiler/expected/build/maps/Compiler/Main.map.json

@@ -1 +1 @@
-{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/Main.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/Main.tex"}],"mappings":[{"artifact":0,"gen_end":359,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":0,"gen_end":574,"gen_start":359,"node":1,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":0,"gen_end":593,"gen_start":574,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":497,"gen_start":134,"node":3,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":1,"gen_end":512,"gen_start":497,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0}],"module":"Main","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-latex-module"},{"id":3,"kind":"semantic-declaration"}],"semantic_id":"1377796023a32d16f638e997e89f5162ae0731039b574111c9eefe0cf26d0eb7","source_id":"d20b90154e589426e4541232a435199f84dd51144b7952ed09a148f87e1b3228","sources":[{"id":0,"kind":"file","path":"src/Main.lex.tex","sha256":"e77d5068d66d7c463f830c9ddf1689bfe095de52a9fc0e99bcfbc59907620f61"}],"spec":"lexlean/source-map/1"}
+{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/Main.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/Main.tex"}],"mappings":[{"artifact":0,"gen_end":359,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":0,"gen_end":574,"gen_start":359,"node":1,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":0,"gen_end":593,"gen_start":574,"node":0,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0},{"artifact":1,"gen_end":497,"gen_start":134,"node":3,"role":"declaration","source":0,"src_end":817,"src_start":309},{"artifact":1,"gen_end":512,"gen_start":497,"node":2,"role":"declaration","source":0,"src_end":891,"src_start":0}],"module":"Main","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-latex-module"},{"id":3,"kind":"semantic-declaration"}],"semantic_id":"b15b9208626b336edfd45300888b98834cc5e7f803134ef6f57df1dd94612aad","source_id":"70bda97e147544336c668b0bf20ace9df3097665775845ca8092dcbc6064b103","sources":[{"id":0,"kind":"file","path":"src/Main.lex.tex","sha256":"e77d5068d66d7c463f830c9ddf1689bfe095de52a9fc0e99bcfbc59907620f61"}],"spec":"lexlean/source-map/1"}

compiler/expected/build/maps/Compiler/TargetOracle.map.json

@@ -1 +1 @@
-{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/TargetOracle.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/TargetOracle.tex"}],"mappings":[{"artifact":0,"gen_end":190,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":0,"gen_end":431,"gen_start":190,"node":1,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":0,"gen_end":672,"gen_start":431,"node":2,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":0,"gen_end":911,"gen_start":672,"node":3,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":0,"gen_end":1156,"gen_start":911,"node":4,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":0,"gen_end":1409,"gen_start":1156,"node":5,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":0,"gen_end":1767,"gen_start":1409,"node":6,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":0,"gen_end":2138,"gen_start":1767,"node":7,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":0,"gen_end":2165,"gen_start":2138,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":572,"gen_start":134,"node":9,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":1,"gen_end":1010,"gen_start":572,"node":10,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":1,"gen_end":1446,"gen_start":1010,"node":11,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":1,"gen_end":1888,"gen_start":1446,"node":12,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":1,"gen_end":2338,"gen_start":1888,"node":13,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":1,"gen_end":2893,"gen_start":2338,"node":14,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":1,"gen_end":3461,"gen_start":2893,"node":15,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":1,"gen_end":3476,"gen_start":3461,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0}],"module":"TargetOracle","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-declaration"},{"id":3,"kind":"semantic-declaration"},{"id":4,"kind":"semantic-declaration"},{"id":5,"kind":"semantic-declaration"},{"id":6,"kind":"semantic-declaration"},{"id":7,"kind":"semantic-declaration"},{"id":8,"kind":"semantic-latex-module"},{"id":9,"kind":"semantic-declaration"},{"id":10,"kind":"semantic-declaration"},{"id":11,"kind":"semantic-declaration"},{"id":12,"kind":"semantic-declaration"},{"id":13,"kind":"semantic-declaration"},{"id":14,"kind":"semantic-declaration"},{"id":15,"kind":"semantic-declaration"}],"semantic_id":"1377796023a32d16f638e997e89f5162ae0731039b574111c9eefe0cf26d0eb7","source_id":"d20b90154e589426e4541232a435199f84dd51144b7952ed09a148f87e1b3228","sources":[{"id":0,"kind":"file","path":"src/TargetOracle.lex.tex","sha256":"08d589074d04c4ab13c161cc1245cc3475e8723d233ce2dab2cdda15bf56d9cf"}],"spec":"lexlean/source-map/1"}
+{"artifacts":[{"id":0,"kind":"lean","path":"modules/Compiler/TargetOracle.lean"},{"id":1,"kind":"tex","path":"modules/Compiler/TargetOracle.tex"}],"mappings":[{"artifact":0,"gen_end":190,"gen_start":0,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":0,"gen_end":431,"gen_start":190,"node":1,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":0,"gen_end":672,"gen_start":431,"node":2,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":0,"gen_end":911,"gen_start":672,"node":3,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":0,"gen_end":1156,"gen_start":911,"node":4,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":0,"gen_end":1409,"gen_start":1156,"node":5,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":0,"gen_end":1767,"gen_start":1409,"node":6,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":0,"gen_end":2138,"gen_start":1767,"node":7,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":0,"gen_end":2165,"gen_start":2138,"node":0,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":134,"gen_start":0,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0},{"artifact":1,"gen_end":572,"gen_start":134,"node":9,"role":"declaration","source":0,"src_end":1006,"src_start":180},{"artifact":1,"gen_end":1010,"gen_start":572,"node":10,"role":"declaration","source":0,"src_end":1833,"src_start":1007},{"artifact":1,"gen_end":1446,"gen_start":1010,"node":11,"role":"declaration","source":0,"src_end":2658,"src_start":1834},{"artifact":1,"gen_end":1888,"gen_start":1446,"node":12,"role":"declaration","source":0,"src_end":3489,"src_start":2659},{"artifact":1,"gen_end":2338,"gen_start":1888,"node":13,"role":"declaration","source":0,"src_end":4328,"src_start":3490},{"artifact":1,"gen_end":2893,"gen_start":2338,"node":14,"role":"declaration","source":0,"src_end":5495,"src_start":4329},{"artifact":1,"gen_end":3461,"gen_start":2893,"node":15,"role":"declaration","source":0,"src_end":6744,"src_start":5496},{"artifact":1,"gen_end":3476,"gen_start":3461,"node":8,"role":"declaration","source":0,"src_end":6818,"src_start":0}],"module":"TargetOracle","nodes":[{"id":0,"kind":"semantic-lean-module"},{"id":1,"kind":"semantic-declaration"},{"id":2,"kind":"semantic-declaration"},{"id":3,"kind":"semantic-declaration"},{"id":4,"kind":"semantic-declaration"},{"id":5,"kind":"semantic-declaration"},{"id":6,"kind":"semantic-declaration"},{"id":7,"kind":"semantic-declaration"},{"id":8,"kind":"semantic-latex-module"},{"id":9,"kind":"semantic-declaration"},{"id":10,"kind":"semantic-declaration"},{"id":11,"kind":"semantic-declaration"},{"id":12,"kind":"semantic-declaration"},{"id":13,"kind":"semantic-declaration"},{"id":14,"kind":"semantic-declaration"},{"id":15,"kind":"semantic-declaration"}],"semantic_id":"b15b9208626b336edfd45300888b98834cc5e7f803134ef6f57df1dd94612aad","source_id":"70bda97e147544336c668b0bf20ace9df3097665775845ca8092dcbc6064b103","sources":[{"id":0,"kind":"file","path":"src/TargetOracle.lex.tex","sha256":"08d589074d04c4ab13c161cc1245cc3475e8723d233ce2dab2cdda15bf56d9cf"}],"spec":"lexlean/source-map/1"}