interpreter: prove env-independence of run for import-free modules

[theebayuser]

What

Proves that when a module declares no imported functions (imports = []), run — hence exec / execOne — does not depend on the host environment:

theorem run_env_indep {m : Module} (hm : m.imports.length = 0) {id : Nat}
    {initial : Store α} {args : List Value} {fuel : Nat} {env env' : HostEnv α} :
    run fuel m id initial args env = run fuel m id initial args env'

env is only ever inspected in run's host arm (env.funcs[id]?); with no imports that arm is dead, and everywhere else env is merely threaded. So env-independence falls out of the same joint fuel induction as the existing fuel_mono_aux — env_indep_aux (over execOne/exec/run), with execOne_env_indep / exec_env_indep / run_env_indep as the projections.

Why

Fuel-free specs and iris-style adequacy results naturally quantify over an arbitrary env but want to discharge at the canonical empty one. This lets them do that by proof instead of assumption — e.g. the run_env_indep axiom currently carried in the iris merge-sort work (SepLogic/AllocSpec.lean, #157) becomes a one-line consequence of this lemma (this statement is the general-α form of that Unit-specialised axiom). Flagged in #157.

How it's proved

Mirrors fuel_mono_aux in the same file: joint statement over the three functions, strong induction on fuel, per-instruction case analysis via execOne.eq_def (reusing the existing execOne_loop_succ / execOne_memOp_succ unfolding helpers). It is simpler per case than fuel-monotonicity — env-independence is unconditional, so there is no ≠ .OutOfFuel bookkeeping. The one structural difference: run's host arm is genuinely env-dependent, so it is discharged by imports = [] (m.imports[id]? = none) rather than closed by reflexivity.

Single-file, additive: no change to any existing definition or lemma statement.

Verification

• lake build green in interpreter/.
• #print axioms on all three lemmas: [propext, Classical.choice, Quot.sound] — no sorryAx.

---

Disclosure per CONTRIBUTING: AI tooling (Claude Code) was used to write and check these changes.