Lean4 wip

[nomeata]

Playing around with a new Lean4 backend (not based on #2) but rather fresh, adapting the Rocq backend from @DCupello1. Opening this PR to have a place for notes and comments, not meant for merging.

Status

• File generated from NanoWasm is processed successfully.

  make && ./spectec doc/example/NanoWasm.spectec -v -l --lean4 -o Wasm.lean
  

• Files generated from wasm 2.0 are processed successfully.

  git ls-files |entr -c bash -c 'make && ./spectec _specification/wasm-2.0/* -v -l --lean4 -o Wasm.lean'
  

• Files generated from wasm 3.0 are processed successfully (sans definitions)
• Some form of CI is needed
• (Much more to do)

IR-to-IR passes that may be useful

• lifting type alias out of recursive groups

Issues with Lean that we might want to fix or work-around

• deriving DecidableEq for nested inductives (e.g. instr) Support for mutual and nested inductive types as DecidableEq instance generator leanprover/lean4#2329.
  Using BEq so far. (Or maybe we can do away with equality checks on instructions?)

• Nested inductive predicates with indices in parameters Nested inductives cannot have indices leanprover/lean4#1964

  mutual
  inductive Subtype_ok2 : context -> subtype -> oktypeidxnat -> Prop where
    | mk_Subtype_ok2 : forall (C : context) (typeuse_lst : (List typeuse)) (compttype : comptype) (x : idx) (i : Nat) (typeuse'_lst_lst : (List (List typeuse))) (comptype'_lst : (List comptype)) (v_comptype : comptype), 
      Forall (fun (comptype' : comptype) => (Comptype_sub C v_comptype comptype')) comptype'_lst ->
      Subtype_ok2 C (.SUB (some .FINAL) typeuse_lst compttype) (.TYPEIDXNAT_OK x i)
  
  inductive Comptype_sub : context -> comptype -> comptype -> Prop where
  end
  

  This is a big one, as this is a kernel issue. We have two work-arounds:

  • Use the lattice-based construction for predicates that is behind coinduction, and can also do inductives. This can handle that kind of nested recursion.

  • Write

    def Forall (R : α → Prop) : List α → Prop := fun xs => ∀ x ∈ xs, R x
    

    which makes the nested induction go through. Conveniently we already generate xs == ys sie-conditions, so this works easily for Forall₂ as well.

[raoxiaojia]

@nomeata I've recently been working on something relevant to what you mentioned above (related to leanprover/lean4#2329 -- generating decidable equality instances for nested mutual recursive types in Lean (I'm trying to build something in Lean to reason about Wasm 3.0's type lattice structure and executing them, among other stuffs). I wonder if there's been any update on Lean's support on this matter. I've also had a custom workaround which almost works and might be applicable to your intention here as well, and I'm curious if you'd be happy to give some feedback.

For the current status of Lean, I can see that the Lean's DecEq deriver currently does not support nested mutual inductives yet, and I did some searches on the Lean zulip chat and found about a comment ~4 years ago from Leonardo saying that this is very low priority as Mathlib doesn't need it. Using BEq seems unsatisfactory either, as the generated definition is basically opaque and cannot be used in any proofs, unless they are axiomatised to be LawfulBEq which allows DecidableEq to be generated, but that introduces some axioms to the codebase.

Currently I made a workaround and constructed a deriver for the DecidableEq instances from the kernel's recursor directly, because Lean can successfully generate the full recursors for nested mutual inductive types (where as Rocq's default recursor generator misses the IHs for nested containers). More specifically, I constructed a command that derives a DecidableEq instance using the recursor of an inductive type, by applying it with the motive being the pointwise DecEq for the argument (i.e. fun x => forall (x' :T), Decidable (x=x')). This works to generate the DecidableEq instance without axiomatising anything, and it seems to evaluate normally within Lean.

The downside is that I have to mark the generated definition noncomputable in the command, because Lean refuses to compile the equality function generated this way to C, stating that code generator does not support recursor .... I guess recursors in Lean work differently than that in e.g. Rocq (which can be extracted to OCaml without a problem). I'm currently trying to use the utility compile_inductive% from Mathlib to generate compiled code though, but that is not a default Lean built-in and seems a bit like a hack. I wonder if there's a better option here, and if you think the above approach of making a DecidableEq deriver might cause any other problems.

I think generating decidable equality for the mutual type lattice definition will also be an issue in the Rocq backend as well, as I don't think Rocq's Scheme Equality handles this case, so maybe some porting of the existing WasmCert tactics might be needed.

[nomeata]

This is maybe the wrong place to discuss, we should probably continue at leanprover/lean4#2329.

Do you need your theory to even use DecidableEq or are you happy with using classical logic? I.e. do you need to compile things or prove things by reduction?

A solution that implements decidable along the recursors at least helps if you want to use these definitions only in proofs or definitions you want to reduce in the kernel, but don’t need to compile. So it’s useful in that way. I don’t know of concrete plans to make recursors computable (leanprover/lean4#2049), unfortunately.

Other options you can consider

1. follow the recursors to know what to do, but still generate Syntax and hope that the structural recursion handler can handle it.
2. similar, but generate a PreDefinition directly (avoiding syntax and elaboration) and hope that the structural recursion handler can handle it.
3. use the construction you already have for the kernel, and send a unsafe recursive definition (with match statements) to the compiler, essentially doing what the equation compiler does

Of these, 2 seems the most principled and modular.

[raoxiaojia]

1. follow the recursors to know what to do, but still generate Syntax and hope that the structural recursion handler can handle it.
2. similar, but generate a PreDefinition directly (avoiding syntax and elaboration) and hope that the structural recursion handler can handle it.
3. use the construction you already have for the kernel, and send a unsafe recursive definition (with match statements) to the compiler, essentially doing what the equation compiler does

Of these, 2 seems the most principled and modular.

Thanks for the comments! Actually, using the recursors as input 'to know what to do' is a nice observation. There's no reason I need to apply the recursor which creates the dependency on it for compilation. I'll have a go in this direction.

I'll post further replies directly under the Lean issue you linked if I can get something that works!