feat: an interpreter for HeapLang

[kdvkrs]

Description

I needed an interpreter for HeapLang and ended up porting the one from iris_unstable/heap_lang/interpreter.v. Putting it here in case it's useful to anyone else and since it might be worth discussing whether this should be part of Iris Lean eventually. The implementation is mostly vibe-coded with a couple of cross-provider review rounds against the Rocq implementation and repo guidelines.

exec fuel e runs a closed expression and returns either its value or a structured error. Like the Rocq one, the interpreter is sequential and deterministic, with forks being collected but never run, and allocation always takes the next fresh location.

Divergences from Rocq are documented at their definitions. Stuck reasons are structured (StuckReason) and rendered separately.

The only change outside new files is removing local from solve_subredex_values in HeapLang/Instances.lean so it can be used in the interpreter.

Checking parity turned up two divergences in the semantics that are likely worth raising as separate issues:

• UnOp.eval rejects integers for .neg; Rocq's NegOp on LitInt is Z.lnot.
• BinOp.eval has no ≤/< on two locations; Rocq's bin_op_eval_loc does.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.

Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.

We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.