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

[afflom]

Scope

Qualify the generic compiler needed by PrismPM: typed-octet lowering in both language versions, source-bound regeneration, compositional Atlas census proofs and actual Lean observation of generated model artifacts. Preserve every original proposition, axiom policy, conformance owner and verification limit.

Restore all 29 valid legacy CLI/lock obligations in their existing conformance owners before replacing the old six-file e2e suite. Independent adversarial review found no remaining coverage loss.

Evidence

• Combined tree through efd4ca7c: original full just vv and check-package passed in pinned tooling; 291 conformance cases, no filters or skips. Independent inventory review matched all 5,924 captured paths. Intermediate commits are not independently qualified by that execution.
• Current restored CF/CL owners: six complete owners pass; 285 other cases explicitly filtered. Exact input and log hashes are in VERIFICATION.md.
• A fresh original full VV and package gate is running on clean c21dd7e09afe6c4253af3cf56d8c67bc99b3f771. This draft must not be treated as current full-gate acceptance before that result and applicable hosted checks are reviewed.

Required before merging

Current complete original VV/package success, applicable hosted checks and independent review of any further findings. Twenty-two original proofs additionally observe already-allowed Quot.sound; observed axiom sets are not claimed identical. No generated Lean was handwritten. This is not an immutable release, installed Prism SDK qualification or downstream application acceptance.

[afflom]

Hosted original workflow 37455111615 at c21dd7e09afe6c4253af3cf56d8c67bc99b3f771 completed successfully. Raw job 112240720394 log was independently retrieved through the job-log API: 181,042 bytes, SHA-256 ec225f2dbb764817d1a9b6c95d1341784057eed1f9e39a68539b021da4937dc4.

The actual full Ubuntu gate ran 291 conformance tests with zero failed, ignored or filtered tests; verified the rooted UOR Atlas and compared all 695 normalized verification records; checked all 866 Atlas published artifacts against their goldens and reproduced all 866 across two distinct absolute roots. The rooted Atlas audit retained all 173 native modules and 5,733 declarations. The full original gate ended with vv: the acceptance gate passed. The four other platform jobs passed their declared build/non-Lean test scopes; those are not native Lean proof qualification.

The earlier local v7 attempt remains a recorded failure: its 8-GiB cgroup killed the unchanged Atlas Lean process. Local v8 restored the previously qualified 12-GiB envelope and is still running with original proof inputs and deadlines. No result is inferred from a running process.

This evidence does not resolve the conflict with newer main, qualify a refreshed PrismPM SDK, authorize a handwritten Lean exception in PrismPM, or close any PrismPM issue. Those remain separate required boundaries.

[afflom]

Independent adversarial review cleared exact c21dd7e09afe6c4253af3cf56d8c67bc99b3f771 compiler-component qualification. Hosted original run 37455111615 passed, with independently re-downloaded raw job log SHA-256 ec225f2dbb764817d1a9b6c95d1341784057eed1f9e39a68539b021da4937dc4: all 291 conformance tests, rooted 173 native Atlas modules/5,733 declarations, 695 verification records, 866 goldens and two-root reproducibility.

Local v8 also finished at 15:58:03 UTC. Independently re-read Docker daemon evidence confirms exact image 670/container b2502085… exited 0. All 5,916 regular files and eight symlinks remain exactly clean c21; input inventory SHA-256 63dead615d2f38d2e5e2b0a104efc807ce7ee1ace604bfddae6a21b6e2362ccf. The fixed owner emits result SHA-256 ac19e8364454ed745e107f02d1416464caf093ec991393c3168c4b668b01cc40 only after original full VV and package checks both return 0 and both whole-source comparisons pass.

The local console recorder was interrupted: its log is incomplete. No terminal process record, full console trace or local attestation was reconstructed. Hosted full logs are a separate execution's evidence. The earlier v7 OOM failure is retained.

Latest-main conflict resolution, PrismPM's Lean tool-source ownership rule, current immutable SDK qualification and release/downstream acceptance remain unresolved. This is not approval to merge over those boundaries or close PrismPM issues.

[afflom]

Closing as superseded by #68, at the maintainer's direction. Its base (0e7e84f8) is 150 commits behind main and predates the revert of the unauthorized pushes, mergeable_state was never established against current main, and its typed-octet lowering is the same change #68 carries on a current base.

Not everything in this branch is obviously in #68, and the branch integration/prismpm-reviewed-model-compiler is kept so that it can be recovered. Before #68 is taken out of draft, these parts of this branch need an explicit yes or no, because they are not byte-literal lowering:

• the compositional Atlas census proofs and the rooted native Atlas source changes (about 1,300 files under examples/uor-atlas);
• the restoration of the 29 valid legacy CLI/lock obligations in their existing conformance owners (cases/cli_api.rs, cases/configuration_lock.rs) before the old six-file e2e suite was replaced;
• the PrismPM adoption finding in the comment thread of [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27 (the handwritten language/lcnf-1.2/extract.lean), which this branch does not address and which [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27 now carries.

---

Generated by Claude Code