iris-lean to prove merge-sort

[Isabelle9999]

Program + spec generated by Talos verifier. Proof uses iris-lean infrastructure (wp_wasm_prop_loop, wp_wasm_prop_call, wp_wasm_prop_block).

Status: WIP

Proven:

• func6 merge (main merge loop, drain loops, composition)
• func1 top-level sort entry
• func0 field copy
• func15 straight-line store
• merge_sort_correct wiring
• All content lemmas (merge_sorted, merge_perm)

In progress:

• func3_terminates: recursive case

Axioms (standard — unverified C library code):

• dlmalloc_alloc_spec (malloc)
• func2_vec_init (Vec::new)
• func4_dealloc (free)

Depends on #133 (shared sep-logic infrastructure in codelib).

[theebayuser]

Small note on AllocSpec: run_env_indep (unlike dlmalloc_alloc_spec) is a provable interpreter fact rather than something that needs axiomatizing — with imports = [] the host arm of run is dead and env is otherwise only threaded through, never inspected, so it drops out of the same fuel induction as fuel_mono_aux in Semantics/Lemmas.lean. I have it proved locally, axiom-clean. Happy to send it as a small standalone interpreter PR so that's one fewer axiom here; leaves dlmalloc_alloc_spec untouched.

[theebayuser]

Sent as #159 — drops in as the general-α form of the run_env_indep axiom here, so AllocSpec can delete it and close over the interpreter lemma. Leaves dlmalloc_alloc_spec untouched.

[Isabelle9999]

superseded