melion

Melion formalises a verified translation from a mutable imperative source IR into a structured SSA form w/in the Lean interactive theorem prover. This implements a total big step operational semantics constrained by a fuel parameter to make sure that termination while facilitating sound reasoning over loop headers and join points. By mapping source variables to a finite index set and utilising versioned name pairs the pipeline forms SSA representation that has dense phi node insertion.

The primary objective is the mechanisation of a semantic preservation theorem that verifies bisimulation between the source state and the projected SSA environment

It has a CFG abstraction to define dominance properties and membership w/in the dominance frontier. The transformation logic in Transform.lean executes the renaming pass bc every definition point w/in the structured control flow yields a fresh versioned name. Verification w/in Proofs.lean establishes that the SSA evaluator maintains consistency w. the source store by proving lemmas on expression renaming and phi bundle projection

My idea for this project was to extend the pipeline to support global value numbering and loop invariant code motion directly on the SSA graph. By computing value equivalences through structural hashing of expressions at phi nodes the compiler can eliminate redundant computations w.o needing difficult dataflow equations. I wanted to formalise the dominance tree properties to prove that hoisting invariant expressions out of loop headers doesnt violate the strict execution semantics of the source IR. This proves that the dense phi placement actually simplifies equivalence checking across basic blocks bc the def use chains remain explicit and invariant under structural transformations

The main theorem is:

theorem compile_correct {n : Nat} (fuel : Nat) (cmd : Source.Cmd n) (σ : Source.Store n) :
    let r := compile cmd
    Option.map (project r.env) (SSA.evalCmd fuel r.code (liftStore σ)) =
      Source.evalCmd fuel cmd σ

Two important supporting lemmas are:

theorem init_expr_preservation {n : Nat} (σ : Source.Store n) (rhs : Source.AExpr n) :
    SSA.AExpr.eval (compileA initEnv rhs) (liftStore σ) = Source.AExpr.eval rhs σ

theorem fresh_bundle_left {n : Nat} (left right : Env n) (next : Nat) (σ : State n) :
    project (PhiBundle.mkFresh left right next).dest
        (applyLeft (PhiBundle.mkFresh left right next) σ) =
      project left σ

Together these show the pipeline is machine-checked end to end: renaming preserves expression meaning, phi insertion copies the correct predecessor values, and the compiled SSA program simulates the source program at every fuel bound.