Replay the exact Lean #14526 compiler artifact against the exact Iris #532 source, using a standalone bridge fixture before focused and full Iris builds.

upstream model bridge plus native tactic replay

Use the GitHub Actions compiler whose embedded commit is Lean PR #14526, verify its source-tree provenance, compile the isolated simp_to_model fixture, then attempt exact Iris focused/full builds and a separate consumer checker.

Hypothesis: Exact Lean PR #14526 and exact Iris PR #532 jointly satisfy the issue #127 focused-file, full-build, and independent-checker contract.

Test: Compile the standalone mergeWith simp_to_model fixture with the exact PR compiler, then fail-fast through the exact Iris focused target, full build, and consumer checker.

A candidate requires the focused file, full Iris build, and independent checker all to pass. Only the exact-head standalone fixture passed, so promotion would overstate the evidence.

• Lean d3718f8f8f71799c4d39d1c7253a3d668cfc2e42 compiles the exact standalone mergeWith simp_to_model fixture with exit code 0.
• The exact Iris #532 HeapInstances file has SHA-256 0054ee1324b55f2f2a4c8c8d1b2737872b3896057c8aff7bf880ad998404f39c and preserves the two public theorem headers against base 8f501a717b7a219acf35ad36b44daa72692435b5.
• The exact combined full build fails at Qq.Typ, Iris.Algebra.COFESolver, and Batteries.Tactic.Alias under Lean 4.34.0-pre.
• The exact focused HeapInstances target is blocked first by Batteries.Tactic.Alias and therefore does not directly falsify the TreeMap proof.

• Exact fixture command: env LEAN_NUM_THREADS=1 LEAN_MAIN_USE_THREAD=0 LEAN_STACK_SIZE_KB=65536 <exact-lean>/bin/lean -j1 experiments/SimpToModelMergeWith.lean; exit 0.
• Exact full-build lab job ca8b44586489; exit 1 after 104.785 seconds.
• Focused target experiment 20260723-224801-85dba4; exit 1 at Batteries.Tactic.Alias.
• Lean compiler reports commit d3718f8f8f71799c4d39d1c7253a3d668cfc2e42; Iris worktree reports commit 8db3e7794c1c59b7e5ebf1dcba6dffd351c9ff2d.

• .proof-experiments/20260723-223348-6e8663: exact Lean #14526 standalone fixture passed.
• lab-runs/lab-iris-lean-127-simp-to-model-ca8b44586489/segment-000001/20260723-224419-a62a69: exact combined full build failed at three version-drift targets.
• .proof-experiments/20260723-224801-85dba4: focused HeapInstances target stopped at Batteries.Tactic.Alias.

A materially separate base-aware checker and consumer Lean file are preserved, but the compile phase was not reached because the exact combined full-build gate failed first.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

no_progress

Public classification

no_progress

• Reproducible-build artifact reuse -> predict elimination of the native bootstrap -> observed exact fixture result in 3.974 seconds without rebuilding 4,887 Lean jobs.
• Compatibility-matrix testing -> predict that source-exact heads may still be ecosystem-incoherent -> observed Lean 4.34-pre failures in Iris/Qq/Batteries pinned for 4.32.1.

• The exact Lean #14526 compiler transforms and proves the standalone Const.mergeWith model obligation.
  .proof-experiments/20260723-223348-6e8663/experiment.json, returncode 0. · Fixture SHA-256 49c9ad241a4014b2bdc05525f0bf549f10761fd4441788de57f4b415930fe26f under Lean d3718f8f8f71799c4d39d1c7253a3d668cfc2e42. · computed
• The exact Iris PR file is byte-identical to the locally tested downstream patch.
  Both files have SHA-256 0054ee1324b55f2f2a4c8c8d1b2737872b3896057c8aff7bf880ad998404f39c. · Iris/Iris/Std/HeapInstances.lean at PR #532 head. · computed
• Current Lean master cannot serve as a full unchanged-Iris-4.32 validation environment.
  Lab ca8b44586489 fails at Qq.Typ, Iris.Algebra.COFESolver, and Batteries.Tactic.Alias. · Exact commit pair and dependency revisions recorded in the lab artifact. · computed
• Issue #127 remained open and requested simp_to_model-based TreeMap proofs at the status check.
  Official GitHub issue inspected on 2026-07-23. · Public issue status at inspection time. · computed

• Use exact Lean master PR #14526 directly against unchanged Iris #532 4.32.1 dependency pins as the full verification receipt.
  Lean d3718f8f8f71799c4d39d1c7253a3d668cfc2e42, Iris 8db3e7794c1c59b7e5ebf1dcba6dffd351c9ff2d, manifest revisions 38d591e7 and 023ce7d6. · The build fails in Qq, Batteries, and unrelated Iris code before the required checker. · records/labs/lab-iris-lean-127-simp-to-model-ca8b44586489-stopped-with-reason-segment-01.json · Update Qq, Batteries, and Iris to a version compatible with the exact Lean head, or use a compatible Lean release/backport.
• Treat green Lean-only CI or the standalone fixture as satisfying Iris issue #127.
  Lean #14526 CI and experiment 20260723-223348-6e8663. · Neither executes the full Iris build and separate consumer checker required by the contract. · The exact combined downstream job failed and did not reach the checker. · A green version-paired full Iris build plus independent checker.

• Produce a source-reviewed Lean v4.32.1 backport receipt.
  It matches Iris #532's declared toolchain and directly closes the remaining version-pairing gap. · Checkout official v4.32.1, port the three #14526 source changes, and run the four-second fixture before a checkpointed native build. · high · open
• Replay after #14526 enters a Lean release Iris can pin.
  This avoids maintaining a backport and supplies the natural upstream acceptance path. · On the first compatible release, update an isolated Iris worktree and run focused/full/checker gates. · normal · open
• Complete the base-aware independent consumer check.
  The checker now compares against the actual PR base and resolves the earlier self-comparison weakness. · Run check_issue_127.py with --base-ref 8f501a717b7a219acf35ad36b44daa72692435b5 after a green version-paired build. · high · open

Objective: Obtain a version-coherent focused/full/checker receipt for Iris #532.

First action: Create a clean official Lean v4.32.1 checkout and mechanically port the three #14526 files while recording the source delta.

Stop condition: Stop and redirect if the v4.32.1 port requires a semantically different model theorem or if the focused fixture leaves mergeWith untransformed; promote only if focused fixture, full Iris build, and base-aware checker all exit zero.

• Construct a clean Lean v4.32.1 checkout with a source-reviewed backport of the three #14526 files.
• Build that toolchain in the checkpointed lab and compile the exact Iris #532 worktree.
• Run the full default Iris build.
• Run check_issue_127.py with --base-ref 8f501a717b7a219acf35ad36b44daa72692435b5.
• Alternatively, wait for #14526 to merge into a Lean release that Iris can pin, then run the same three gates.

• https://github.com/leanprover-community/iris-lean/issues/127 ↗
• https://github.com/leanprover/lean4/pull/14526 ↗
• https://github.com/leanprover-community/iris-lean/pull/532 ↗
• https://github.com/leanprover/lean4/actions/runs/30047952870 ↗

Sol principal: OpenAI Codex (GPT-5) performed source audit, experiment design, checker changes, execution, and synthesis. Terra delegate gpt-5.6-terra supplied advisory source reconnaissance; its memo was audited and not treated as independent evidence. Tools used: Lean 4.34.0-pre exact PR compiler, Lake 5, Python 3.12 deterministic harness/checker, Bash, Git, GitHub REST/Actions, and the checkpointed Proof Factory lab. No CAS, SAT/SMT solver, or additional proof assistant was used.

Duration

1924.6s

Review state

evidence receipt failure; not durable progress

Attempt ID

iris-lean-127-simp-to-model-20260723-225300-934337

No human review recorded.