BLOCKED: refactor: replace `rewrite` with `mkEqNDRec`

[alexkeizer]

Description:

Stacked on

• [ ] #214

We've replaced uses of rewrite in AxEffects with a more manual application of Eq.ndRec.

This is motivated by the slowdown observed in #210, where the size of hypotheses would grow and a lot of time was being spent on rewriting. With Eq.ndRec, the meta-code explicitly constructs the motive, thus, no inspection of the expression being rewritten is needed, hence, the speedup.

That said, in this PR we've not yet switched to intermediate state aggregation, and here, the change actually seems to slow us down. Also, it seems we could be triggering an infinite loop here. I'm unsure what's happening, and why we didn't trigger this behaviour in #210. More investigation is needed.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

I tried, but SHA512Loop seems to be stuck in an infinite loop, making my laptop go OOM.

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[alexkeizer]

This is currently blocked, waiting on a diagnosis of https://github.com/leanprover/lean4/issues/5610

[alexkeizer]

We had a working hypothesis that the instantiateMVars slowdown was somehow related to proof sizes. Unfortunately, this does not seem to be the case: I compared the proof generated for 7 steps of SHA512 in this PR with the main branch, and in fact this PR generates slightly smaller proofs, despite being significantly slower for the larger sizes (I tried measuring the size of the proofs in the larger cases, too, but the computation wouldn't terminate).

For context, the main branch gave a proof of size 50575532 (where each Expr constructor counts as 1), and this PR got that down around 10%, to 46906018.

Here's the code that computed those numbers:

partial def sizeOfExpr : Expr → Nat := go #[] 0 where
  go (queue : Array Expr) (acc : Nat) : Expr → Nat
  | Expr.bvar _ | Expr.mvar _ | Expr.fvar _ | Expr.lit _
  | Expr.const .. | Expr.sort _ =>
      let acc := acc + 1
      if h : queue.size = 0 then
        acc
      else
        let x := queue[queue.size - 1]
        let queue := queue.pop
        go queue acc x
  | Expr.mdata _ x | Expr.proj _ _ x =>
      go queue (acc + 1) x
  | Expr.app x y | Expr.forallE _ x y _ | Expr.lam _ x y _  =>
      go (queue.push x) (acc + 1) y
  | Expr.letE _ x y z _ =>
      go (queue.push x |>.push y) (acc + 1) z