[humuhumu33]

Implements UOR-Foundation/PrismPM#605 upstream: a proof form that proves a decision model's properties through local box obligations instead of one linear_arithmetic case split per property.

Why

Verdant Resonance (7 fields, 35 first-match rules, 15 properties) checks but does not verify: each property's linear_arithmetic script splits the 35-rule judge, and omega fails on a branch. The properties are true (brute force over all 3,131,000 in-bounds requests). The proof has to stop growing with the case split.

What

• LexLeanRuntime.Regions, a sixth native runtime module (namespace LexLeanRegions, imports only Init). It holds the checker data (Cond, Rule, Property), its semantics, the box obligations, and holds, the soundness theorem: if obligation B R d P = true, then breaks R d P x = false for every request of the box's width. Every row pins its axioms; holds uses only propext and Quot.sound. It was exported once from authored Lean through the fold-law oracle. The regenerated environment equals it in all 379 rows (tests/runtime-library/REGIONS.md).
• region_check, a language-1.2 proof form for a theorem breaks request = false. The backend reads the judge's rules, the property, and its bounding box from the module and emits:
  exact LexLeanRegions.holds R d P B (by decide +kernel) [(request).f, …] rfl
  The runtime's semantics use the backend's own shapes (Nat.blt/ble/beq, !, && folded from the left, if b then). So the module's breaks is definitionally the runtime's breaks of the lowered data, and the kernel checks that equality. The lowering is not trusted: a misread module produces a proof Lean refuses (VERIFICATION.md, planted defect (a)).
• Linking refuses anything outside the fragment and names the reason: != in a rule, a field the property leaves unbounded, a comparison that is not field against constant, the form used as a branch, or language 1.1.

Evidence

• Verdant's canonical module, with every linear_arithmetic{…} replaced by region_check{}, runs lexlean verify in about 73 s. A planted defect (rule2's proximity limit 20 → 60) is refused with LLV7002 at exactly inv004Holds and inv008Holds.
• PF-24 (register: 494 IDs), its scenario, and conformance_pf_24 over the new examples/decision-regions:
  • pins the emitted proof;
  • checks the four linking refusals and the language-1.1 refusal;
  • verifies the example;
  • has Lean refuse a planted defect at exactly the two properties it breaks.
• SPEC.md §17.12 gains Decision regions. The v2 module and snapshot schemas admit the kind.

Identity

The language-1.2 compiler-semantics ID changes. The locks, goldens, fixture expectations, calculus and production packages, and verification records are regenerated by the repository's writers in the chore commits (Linux x86-64, pinned Lean 4.32.1). On the regenerated tree, check-golden, check-fixtures, and validate pass.

examples/uor-atlas is a language-1.0 project. Nothing under it changes, and its records reference neither the language-1.2 identity nor its runtime, so they are not regenerated; the gate's Atlas shards verify them as committed. (An earlier version of this description called them stale. That was wrong.)

Not in this PR

• Delta proofs (by_checker_delta, PrismPM#604).
• Content-addressed per-obligation reuse (PrismPM#603).
• A shorter refusal diagnostic. Today Lean prints the whole lowered data before the source-mapped location.

🤖 Generated with Claude Code

[afflom]

Bounded source/acceptance triage at91912e (not complete proof or generated-product approval): I found no demonstrated kernel bypass in the inspected fragment/lowering boundary. The emitted proof still applies the pinned LexLeanRegions.holds theorem with a kernel-decided obligation and checks the original target through Lean; its declared axioms are exactly Quot.sound/propext.

Two concrete delivery items remain with this implementation owner:

1. The explicitly omitted uor-atlas/CensusCert11 current-identity records still block the normative example/expected-record equality requirement. Complete and review that missing writer output on sufficient resources before final-tree acceptance; normal CI validation does not itself adopt regenerated output. Preserve valid completed evidence and avoid repeating already completed producers.
2. tests/runtime-library/REGIONS.md ends with a blanket claim that every language1.2 verified record was regenerated, contradicting the Atlas exception in this PR body. Make the evidence wording match what was actually produced.

Keep this draft until the remaining outputs, complete final-head gate, same-run honesty and repro are accepted. This review did not rerun the 379-row or Verdant measurements, inspect all2675 changed files, or perform a full proof audit. No competing patch, identity wave or qualification run has been started.

[afflom]

Bounded delta readback at9f9d928: the regeneration-wording finding is addressed by1e746; REGIONS.md now explicitly excludes Atlas. The release integration adds only the maintenance Cargo.lock/CHANGELOG delta; region proof/runtime/generated-product source is unchanged from the prior inspected scope, so no duplicate source or producer review was performed.

Atlas current-identity verification records remain the concrete unresolved output blocker. This stays draft pending that owner's output review and complete resulting-head qualification. The prior review was bounded triage, not a complete proof/product audit, and this delta review does not expand that claim. No writer, test or CI run was repeated.

[afflom]

Correction to my earlier reviews5865263518/5865729927: I withdraw the requirement to regenerate Atlas records for this language-1.2 identity change. The exact-head Atlas manifest and lock both select language1.0; their blobs and entrypoint are unchanged from the release base, and compiler_semantics_id_for excludes runtime1.2 and v2 schemas from that identity. My previous inference from the earlier OOM/staleness wording was wrong. No Atlas writer should be repeated on that premise. Ordinary committed-record verification remains part of acceptance.

The remaining concrete correction is small: tests/runtime-library/REGIONS.md still says Atlas records carry the previous identity. Update that paragraph to match the corrected PR body and unaffected language1.0 scope; historical OOM does not establish stale records.

The fc57→5800 delta contains five gate/documentation support changes for PF-24, with no additional concrete source blocker demonstrated in this bounded review. This does not establish the full proof/product audit: affected language1.2 outputs, complete resulting-head CI, same-run honesty and independent reproducibility still need acceptance under the existing owner. No runtime, writer, measurement or gate was repeated.

[afflom]

The remaining documentation finding is resolved at5e5c518: the only change from5800 is REGIONS.md, which now correctly distinguishes regenerated language1.2 projects from unaffected language1.0 Atlas records. The prior Atlas-regeneration requirement remains withdrawn; no repeat writer is needed on that premise.

No new blocking source delta was found in this documentation review. It does not expand the earlier bounded proof/product review: complete resulting-head qualification and affected1.2 output acceptance remain with the existing owner. Exact-head repro43126857745 passed; CI43126858163 is still active. No completed proof, producer, test or measurement was repeated.

[afflom]

[P2] Reconcile SM-38 declaration goldens for the resulting PF-24 compiler identity. This exact merge preserves actual release5dcc ancestry, but the imported outputs are incomplete/stale in two concrete places:

• examples/decision-regions/expected/build has no declarations directory or declarations manifest row. Its Main is a language1.2 semantic module, and the imported api.rs now emits that output for every such module.
• The LanguageTwelve/Main declarations blob906165cd is byte-identical to release5dcc (manifest output SHA92ec9b45), while its manifest compiler-semantics changes from635a25ac to28156029. declaration_id.rs explicitly frames compiler semantics into the IDs, and api.rs supplies the selected language identity. Retaining that parent-generated file does not reconcile it with this compiler identity.

These are source/committed-output correspondence findings, not claimed runtime failures or an audit of all101 imported declaration files. Please produce and review the required declaration outputs/manifest rows with the official resulting-source golden writer, including the new example. Reuse other valid completed products; no parallel writer or repeated export/verification/measurement is requested. Also update the PR body's current register count483→484; historical SM-38 records need not be rewritten.

The earlier Atlas regeneration requirement remains withdrawn, and its documentation correction remains resolved. Exact-head repro passed; the draft CI is still incomplete. Independent bounded integration receipt3b08ecf1 records the136-path delta and these samples; this is not a repeated proof audit or full product acceptance.

[afflom]

Terminal CI43130959531 now provides a narrower product-reconciliation target. The single saved rest-job log130902956430 reports284 passes and7 failures: GC-01, GN-01, RB-02–05 and RB-07. Independent static decoding of all four RB-02–05 manifest pairs shows that only sources[0] differs: committed46bcb26a… versus generateda9477044…. GC-01/GN-01 first report compiler/rust/negative/arithmetic-invented-overflow.json. No program/export/effect change was found in those four decoded comparisons.

RB-07 separately reports that compiler/rust/rust-std/adt-evaluation builda9477044 does not bind the committed TargetFixtures source d746739e…. Its source-map check combines semantic ID, source path and source hash, so the message does not identify which field is wrong. Please reconcile the intended final compiler/source-map binding and affected generated-manifest closure through the official owning writer, retaining unchanged completed products. This evidence does not justify blindly repeating the entire calculus or identity wave, and generated IDs should not be hand-edited.

The existing declaration-golden/census findings remain separate. The withdrawn Atlas-regeneration requirement stays withdrawn. Exact repro success does not resolve these observed failures. Receipt2e8a7438 preserves the focused log and decoded comparison; no test, producer, log replay, artifact download or stopped TC-03 validation was run.

[afflom]

Bounded product-delta review at d48a52b on actual release aaf8455: the sampled findings from254c are structurally reconciled. The compiler manifest, TargetFixtures map, four previously failing negative manifests and adt-evaluation package now agree on46bcb26a. The previously missing DecisionRegions declaration and manifest row are present, and LanguageTwelve's declaration no longer retains the old release blob.

This retires the old missing-file/unchanged-blob and sampled a947-versus46bcb diagnosis for this head. It does not claim the seven cases passed, verify every new declaration ID, or audit all2,739 changed paths. The withdrawn Atlas-regeneration request remains withdrawn; no producer, old log or completed check was repeated.

The known census wording still needs correction: the PR body says483 while exact-head model/ids.toml has494 rows and the new CHANGELOG already says494. Current draft run43195281073 has12 required groups skipped; even if its remaining job succeeds, it is development evidence rather than full final-head acceptance. Repro43195281146 passed at this head. Existing owner retains readiness, final qualification and landing.

[afflom]

Exact-head terminal diagnostic for d48a52b: CI43195281073, rest job131106284198, reports290 conformance passes and one failure. GC-01, GN-01 and RB-02–05 now PASS, retiring those six old failures.

Remaining RB-07 blocker: compiler/rust/rust-std/adt-evaluation: no verification of the build46bcb26a… is committed. Exact-head rust_packages.rs60–80 requires a matching LexLeanAudit.A46bcb26a78a0357ffba6c8270c0ddd424. audit filename under compiler/expected/verify/audit before the later source-map assertions. This is a missing current-build verification artifact, not the old a947/46bcb map mismatch; those sampled binding repairs remain credited.

Please reconcile the affected compiler verification evidence through its official product path, retaining completed valid outputs. The evidence does not justify an Atlas regeneration or a blind all-project writer repeat. This diagnostic does not establish that later RB-07 assertions will pass.

Repro43195281146 passed, but twelve required groups were skipped in this draft run: full final-head qualification is still owed. One new focused log was archived; no old log, runtime test, producer or gate was repeated. Existing owner retains the repair.

[afflom]

The previously missing current compiler-verification artifact is now structurally repaired at2c1e6705. An exact old/new Git-tree comparison accounts for2,315 changed paths despite the compare/PR file-list caps. Current46bcb26a audit/process artifacts are committed; sampled TargetFixtures package, map and source bindings agree, and sampled bootstrap75b76e3c exports/provenance agree. This credits adoption and supersedes the missing-file finding in5875193285; it does not establish every generated byte or later RB07 assertions.

Use the existing owner qualification on this head to establish the remaining product/gate acceptance. Draft CI43341479857 is active and exact repro43341479905 passed. No Atlas regeneration, old log refetch or completed producer repeat is requested. The earlier withdrawn Atlas prerequisite stays withdrawn. Keep PF24's decision-region contract distinct from #507's proposed PF26 conditional-chain work during integration. Existing owner retains the implementation and final qualification; no readiness transition or merge was performed.