Non-circular source-module probe of simp_to_model followed by a hash-bound structural audit of its operation table

No Progress

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.

Research-policy redirect

Attempt evidence did not validate; durable progress is withheld.

Strategy and discriminator

static capability audit plus focused formal probe

Expose mergeWith's definitional fold, invoke simp_to_model on the real Iris source theorem, and compare the hard-coded tactic tables across pinned and current Std revisions

Hypothesis: On pinned Lean 4.32.0, simp_to_model can discharge TreeMap.mergeWith get? semantics after supplying beqOfOrd and exposing the definitional fold.

Test: Compile the actual patched Iris/Std/HeapInstances.lean module and inspect whether simp_to_model closes the theorem or leaves a model obligation.

Rationale

The negative result is formal and non-circular: it elaborates the theorem in its defining module, records the exact residual goal, binds the patched source by hash, and is corroborated by a materially separate source-structure checker. Retaining the bespoke internal proof behind a local wrapper would not satisfy the robustness contract.

Claims requiring scrutiny

On the pinned Iris commit and Lean 4.32.0, the tested simp_to_model refactor does not discharge Std.TreeMap.getElem?_mergeWith'.
The residual obligation is the list-model semantics of a foldl of Const.alter! operations implementing mergeWith.
The relevant simp_to_model source is byte-identical and lacks a mergeWith bridge in Lean v4.32.0, v4.32.1, and master commit 00f9caf44935b96cbeee36082c3abea67ab06792.
The original unmodified HeapInstances module still compiles under the pinned toolchain.

Evidence and scope

env LEAN_NUM_THREADS=1 lake env lean Iris/Std/HeapInstances.lean on the patched defining module returned 1 with the expected residual model goal.
python3 scripts/check_mergewith_blocker.py returned 0 and emitted success=true.
env LEAN_NUM_THREADS=1 elan run leanprover/lean4:v4.32.0 lake -d source/iris-lean/Iris env lean source/iris-lean/Iris/Iris/Std/HeapInstances.lean returned 0 after restoration.

Computational experiments

.proof-experiments/20260722-222622-387f7c: the exposed source probe returned the expected unsolved list-model fold obligation.
.proof-experiments/20260722-222850-1accb3: the independent checker returned success=true.
.proof-experiments/20260722-222941-d7a2e6: the restored original focused module compiled successfully.

Independent checker

scripts/check_mergewith_blocker.py uses static source-table and hash checks rather than Lean proof search; experiment 20260722-222850-1accb3 returned 0.

Contribution gate

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

Cross-domain transfers tested

Compiler capability-table auditing -> predict that a missing hard-coded operation entry leaves an exposed semantic residual -> observed exactly the foldl/alter model obligation.
Differential version testing -> hash candidate implementations before repeated builds -> three advertised version points collapsed to one identical source profile.

Established facts

The patched defining module reaches an unsolved Internal.List.getValue? goal over List.foldl and Const.alter!.
.proof-experiments/20260722-222622-387f7c/stdout.txt, SHA-256 fb51f5cd1d5404ceba0b97da0945b498f6750e30a77752fa707745e395d49aa0 · Iris commit 3e2b759 with Lean 4.32.0 and patched source SHA-256 4fd6dafe9479f85446a2b6f813f770eb8eff77a15fc9a575a5544d9d43a1adf2 · computed
The checked v4.32.0, v4.32.1, and master tactic modules are byte-identical and contain no mergeWith model registration.
scripts/check_mergewith_blocker.py and experiment 20260722-222850-1accb3 · Exactly the three stored snapshots · computed
The original focused HeapInstances module compiles after restoration.
.proof-experiments/20260722-222941-d7a2e6/experiment.json · Original source SHA-256 a4ac60e58bddfc98952dda59ea6b9969b30a2ae95ab3c252a33f553eaa616884 under Lean 4.32.0 · computed

Ruled out in this epoch

Replace the TreeMap merge theorem body with a direct simp_to_model invocation under current Std.
Pinned Lean 4.32.0, plus absence of the required capability through checked master 00f9caf · No mergeWith model bridge exists in the tactic table, and the formal probe leaves the model fold unsolved. · Experiments 20260722-222622-387f7c and 20260722-222850-1accb3 · A new public mergeWith model theorem and tactic registration, or equivalent new Std automation.
Validate the proof using an example that imports Iris.Std.HeapInstances.
Any example where the existing getElem?_mergeWith' simp theorem remains imported · The target theorem can solve the example circularly. · findings/source-discriminator.md and the defining-module control · Disable or remove the existing theorem and elaborate the defining module.
Wrap the existing private fold proof in a local model lemma and claim implementation robustness.
Current Iris-only helper architecture · The same DTreeMap.Internal.Impl dependency would merely move behind another declaration. · The residual obligation coincides with the existing fold/alter helper mechanism. · A public Std semantic bridge whose proof and maintenance belong upstream.

Open leads

Add a reusable public mergeWith list-model theorem and register it with simp_to_model.
It directly addresses the sole missing capability exposed by both dynamic and static checks. · In a project-scoped Lean source checkout, prove the constant-value mergeWith model lemma and run a focused Std get? theorem before rebuilding Iris. · high · open
Replace the tactic's private hard-coded operation map with an extensible attribute registry.
Iris could register a bridge without editing the tactic macro, and future map operations would not require modifying a private table. · Prototype one attribute-driven alter entry and compare generated simp arguments with the current modifyMap. · normal · open

Continuation checkpoint

Objective: Determine whether the missing mergeWith bridge can be added narrowly and upstream.

First action: Run python3 scripts/check_mergewith_blocker.py, then create a project-scoped Lean patch adding the model lemma and modifyMap entry.

Stop condition: Redirect if the bridge necessarily exports the same implementation-specific fold proof to Iris or lacks a credible Std acceptance path.

Next moves

Prototype a public Std toListModel_mergeWith lemma for constant-value DTreeMaps.
Register mergeWith in simp_to_model's modifyMap and add a focused Std regression theorem.
Replay artifacts/patches/source-probe.patch in the actual Iris defining module.
Only if that passes, remove the obsolete Iris private helpers and run the focused and full builds.

Citations

Tool disclosure

GPT-5 Codex served as the Sol principal. A supplied GPT-5.6 Terra source-discriminator memo was treated as advisory and independently audited. Lean 4.32.0, Lake, Python 3.12, git, ripgrep, curl, SHA-256, and deterministic experiment/checker scripts were used. No model agreement was treated as validation.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1413.5s
Review state: evidence invalid or incomplete; not durable progress
Attempt ID: iris-lean-127-simp-to-model-20260722-223326-810dbc

Human review ledger

No human review recorded.