Running code in reflective tactics/metaprograms

Stream: general

[l1mey]

I am implementing a reflective metaprogram that takes in a Lean expression, reifies it into an AST, then runs a user supplied function with a proof of correctness to optimise the AST, then denotes that AST back into a Lean expression. I believe this is a pretty standard way of proof, and the reification and denotation metaprograms are inverses of eachother and return proofs:

(reify) Expr -> IR, returns a proof that IR.eval = expr
(denote) IR -> Expr, returns a proof that IR.eval = expr


  ir  = reify lhs     (IR.eval ir = lhs)
  ir' = opt ir        (IR.eval ir ~> IR.eval ir')   (opt.wf)
  rhs = denote ir'    (IR.eval ir' = rhs)

  lhs = IR.eval ir ~> IR.eval ir' = rhs
  ⊢ lhs ~> rhs                               (by proof chaining)

Optimisations are declared as follows, using the Rule type like below, they're just programs:

def addNsw_refine_add' : Rule :=
  { impl := fun ir =>
    match ir with
      | IR.addNsw lhs rhs => IR.add lhs rhs
      | _ => ir

  , wf := by
      intros idx ξ σ lhs

      split <;> try rfl
      apply addNsw_refine_add
  }

However, I have an issue. After reifying, I need to actually run the impl function on the reified IR. So, right now given the rule supplied to the metaprogram as an Expr, I evaluate the the impl function using an unsafe program:

have rule : Q(Rule) := ...  /- user supplied -/

let ⟨ir, irExpr, _, irProof⟩ ← reifyIRExpr resultIdx body   /- irExpr = toExpr ir -/
let ir' ← evalImpl resultIdx irExpr rule

unsafe def evalImplUnsafe (idx : Nat) (irExpr : Q(IR $idx)) (rule : Q(Rule)) : MetaM (IR idx) := do
  let expr := q(($rule).impl $irExpr)
  evalExpr (IR idx) q(IR $idx) expr

@[implemented_by evalImplUnsafe]
opaque evalImpl (idx : Nat) (irExpr : Q(IR $idx)) (rule : Q(Rule)) : MetaM (IR idx)

The thing is, even though this actually evaluates the IR on the rule.impl, it's useless to me because there isn't any proof that this new IR ir' is equal to impl ir.

If I were to do proof chaining, I wouldn't want to work on the impl ir expression, I would like to work on the actual evaluated version of that, but after the evaluation, Lean doesn't know that they're equivalent (I need a proof that ir = impl ir, but I don't have that)

"Running the code" has got me stuck here. What is the solution? Using something like Lean.ofReduceBool? I can see that's what bv_decide sort of does. I appreciate any insight, since I'm quite new to this.

[l1mey]

I was thinking using Lean.ofReduceBool to do this:

have rule : Q(Rule) := ...  /- user supplied -/

let ⟨ir, irExpr, _, irProof⟩ ← reifyIRExpr resultIdx body   /- irExpr = toExpr ir -/
let ir' ← evalImpl resultIdx irExpr rule

/- ir' = rule.impl ir -/
let proofType := q($ir = @$(rule).impl $resultIdx $(reified.irExpr))

/- then, as they're both inductive ASTs this can be proved by just running the code
  by doing Lean.reduceBool + Lean.ofReduceBool -/

This seems like the right fit, but honestly, I wouldn't know since there isn't much documentation on writing tactics of this form and knowing when or not to use these reflection primitives.

If I were to do it this way, it does seem that I'll have to run the code twice as well. I'll have to run it once in the unsafae eval (to run impl on it and denote), and a second time using Lean.reduceBool to get the proof that the ir' is actually impl ir.

[l1mey]

Okay, so using rfl the function is "ran" inside the kernel. However I don't know to what extent this works for all Lean functions:

example :
  addNsw_refine_add'.impl ((IR.var 0).addNsw (IR.var 0) : IR 0)
    = (IR.var 0).add (IR.var 0) := rfl

Since I am only admitting optimisations that you can prove correct, these optimisation functions must be all provably terminating (so just normal Lean functions). To what extent can normal Lean functions be evaluated in the kernel? (For example, the function above is defined using pattern matching, what about functions that use other constructs?)

These optimisations might be quite heavy, since I'm planning to port and reimplement certain LLVM optimisations. The kernel might not be able to keep up eventually, so reduceBool might be an option eventually?

[Aaron Liu]

l1mey said:

To what extent can normal Lean functions be evaluated in the kernel? (For example, the function above is defined using pattern matching, what about functions that use other constructs?)

Can you elaborate? For inductive types, recursive pattern matching is essentially the only thing you can do.