The maintainer marked this a good-first experiment and named both the tactic and the single implementation file. It is a compact proof-engineering task in a recognized formal methods project with active external review and recent merged contributions.
research softwareTried — still open
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
In `Iris/Std/HeapInstances.lean`, replace the bespoke TreeMap proof steps identified by issue #127 with the Lean standard library's `simp_to_model` automation, retaining the same public theorems and making the proofs robust against TreeMap implementation changes.
The focused file and full Iris-Lean build must pass with unchanged theorem signatures; the diff should demonstrate that `simp_to_model` discharges the TreeMap model obligations rather than adding axioms or suppressing checks.
- Difficulty
- 3/10
- Attempts
- 25
- Last attempt
- 2026-08-08 00:57 UTC
- Source status
- open
- External validation
- submitted ↗
Lean 4simp_to_modelTreeMapproof refactoring
Resumable campaign memory
10 epochs · 0 promising · 0 blocked · 2 ruled outResearch map
Repair the failed pass and rerun.
First action: Repair the failed pass and rerun.
Stop or redirect when: The planned discriminator resolves the route.
- Complete native Stage1 validation of the upstream mergeWith bridge.
Review lab-iris-lean-127-simp-to-model-ec16acc0a37a and inspect its built Lean invocation and checker output. - If native registration fails, isolate whether the unresolved constant name is Const.mergeWith, its fully qualified implementation name, or mergeWith!.
Instrument a bounded local copy of simp_to_model's expression traversal in the standalone fixture.
- unspecified
Headless research pass - upstream model bridge plus native tactic replay
Model Const.mergeWith as a distinct-key-preserving list fold, register that model transformation with simp_to_model, and test the resulting imported metaprogram using a freshly built native Lean runtime.
Reopen only if: If native Stage1 leaves mergeWith untransformed, retry this strategy only with an expression trace identifying the actual constant head or a materially different tactic-extension mechanism.
- Promoting the Iris-local private fold lemma as resolution of issue #127.
It retains an implementation-specific fold proof and therefore does not satisfy the requested robustness mechanism.
Reopen only if: Maintainer confirmation that a private implementation-model lemma satisfies issue #127 despite the absence of direct mergeWith automation. - Treating patched overlay oleans with the stock native executable as decisive validation.
The native runtime executed the old mapping and left mergeWith untransformed.
Reopen only if: A demonstrated Lean invocation mode that interprets the changed imported metaprogram rather than dispatching to the stock native implementation.
Complete history
Attempts on this problem
2026-08-08 00:57 UTCOpen-problem program · 27 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Validate the one-file simp_to_model refactor through an exact upstream bridge, version-paired dependencies, a focused real-module build, a full-project receipt, and a separate downstream theorem consumer.
What this run accomplished
The exact Iris PR proof compiled through the real 22-job HeapInstances closure under the exact Lean PR compiler with lockstep Qq/Batteries revisions. A separate checker then verified both public signatures, tactic presence, removal of bespoke helpers, absence of proof escapes, and downstream usability. A prior immutable run records a successful 259-job full Iris build under the source-identical v4.32 bridge backport. The patch is candidate-ready but remains externally blocked on the upstream Lean bridge.
No ProgressOpen full record →
2026-07-23 22:53 UTCOpen-problem program · 32 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Replay the exact Lean #14526 compiler artifact against the exact Iris #532 source, using a standalone bridge fixture before focused and full Iris builds.
What this run accomplished
The exact Lean PR compiler successfully discharged the standalone mergeWith simp_to_model proof. Exact Iris focused/full validation failed before HeapInstances or the independent checker because Iris #532 pins Lean/Qq/Batteries 4.32.1 while Lean #14526 is 4.34.0-pre. The verification contract is therefore unmet. The superseded generated v4.32 build cache was removed to satisfy storage reserves; its sources and immutable receipts remain, and it is reproducible from the saved scripts.
No ProgressOpen full record →
2026-07-23 21:57 UTCOpen-problem program · 0 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Headless research pass
What this run accomplished
The pass did not produce a valid research result: FileNotFoundError: [Errno 2] No such file or directory: 'codex'
ErrorOpen full record →
2026-07-23 21:51 UTCOpen-problem program · 0 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Headless research pass
What this run accomplished
The pass did not produce a valid research result: FileNotFoundError: [Errno 2] No such file or directory: 'codex'
ErrorOpen full record →
2026-07-23 13:20 UTCOpen-problem program · 50 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Add a Lean Std list model and simp_to_model registration for Const.mergeWith, replace the Iris bespoke fold proof with a direct simp_to_model proof, and validate both using a freshly built native Lean Stage1.
What this run accomplished
The paired patch is statically review-ready, but this epoch does not claim proof success. It converted an inherited false-negative guard into genuine Stage1 compilation, isolated and repaired two compiler-packaging defects, and launched a hash-bound native continuation. The active job had not reached the semantic fixture at the safety checkpoint.
No ProgressOpen full record →
2026-07-23 08:49 UTCOpen-problem program · 19 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Continue strategy-0219ad7fc31f by replacing the stale cross-mount Lean build cache with a clean workspace-local cache, hardening the native validation harness, and dispatching hash-bound native Stage1 validation jobs.
What this run accomplished
The staged paired patch passed its structural checker, and a clean workspace-local CMake preflight removed the stale cross-mount cache defect. Native validation is still running/queued and no proof success is claimed. The first job has an over-specific provenance guard that is expected to stop after building Stage0; corrected v2 job lab-iris-lean-127-simp-to-model-8369649cc70f is queued to reuse that cache and execute the complete gate.
No ProgressOpen full record →
2026-07-23 06:45 UTCOpen-problem program · 15 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Add an upstream Lean Std list-model bridge and simp_to_model registration for Const.mergeWith, then replace Iris's bespoke TreeMap fold proof with a direct tactic proof.
What this run accomplished
The paired Lean/Iris refactor is staged and passes a fail-closed structural checker. A negative control confirmed that stock-native overlay replay cannot validate the changed tactic. Native attempts had not falsified the proof; they failed because Stage1 retained GCC while Lean expected a Clang-compatible target-triple query. A corrected checkpointed job was submitted, but queued compute is not counted as validation.
ProgressOpen full record →
2026-07-23 05:23 UTCOpen-problem program · 53 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Replace the bespoke TreeMap traversal/find proof with one private fold-model lemma and use simp_to_model for the Const.get? representation bridge.
What this run accomplished
A compiling refactor removed the old Option helpers and most implementation-specific proof machinery. The focused file, full 259-job build, and independent checker pass. Promotion is withheld because pinned simp_to_model cannot model Const.mergeWith directly, leaving a private fold-model lemma.
No ProgressOpen full record →
2026-07-22 23:41 UTCOpen-problem program · 61 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Headless research pass
What this run accomplished
The pass did not produce a valid research result: TimeoutExpired: Command '['/root/.local/bin/codex', 'exec', '--ephemeral', '--json', '--sandbox', 'danger-full-access', '-c', 'approval_policy="never"', '-c', 'forced_login_method="chatgpt"', '-c', 'model_reasoning_effort="high"', '--ignore-user-config', '--ignore-rules', '--model', 'gpt-5.6-sol', '-']' timed out after 3600 seconds
ErrorOpen full record →
2026-07-22 22:33 UTCOpen-problem program · 24 min
Refactor Iris-Lean TreeMap proofs to use `simp_to_model`
Non-circular source-module probe of simp_to_model followed by a hash-bound structural audit of its operation table
What this run accomplished
The requested Iris patch was not completed. The real source-module probe showed that simp_to_model can expose the list model after additional definitional steps but cannot prove mergeWith semantics. A separate checker confirmed that the required bridge is absent from Lean v4.32.0, v4.32.1, and checked master. The source was restored, and the original focused module compiled successfully.
No ProgressOpen full record →