Lean backend: LeanRV32D.Functions.execute is noncomputable, has no executable code

[GZGavinZhao]

Hi! I'm trying to use the Lean model generated by the spec, and unfortunately LeanRV32D.Functions.execute seems to be noncomputable which causes me to add uncomputable to every function that uses it.

For example, the following snippet

import LeanRV32D

open Sail
open LeanRV32D.Functions

def spec_add (rd rs1 rs2 : regidx) : SailM Unit := do
  writeReg Register.nextPC (BitVec.addInt (← readReg Register.PC) 4)
  let _ ← execute (.RTYPE ⟨rs2, rs1, rd, rop.ADD⟩)
  pure ()

produces the following error:

failed to compile definition, compiler IR check failed at 'spec_add'. Error: depends on declaration 'LeanRV32D.Functions.execute', which has no executable code; consider marking definition as 'noncomputable'

However, the following works perfectly fine:

def spec_add (rd rs1 rs2 : regidx) : SailM Unit := do
  writeReg Register.nextPC (BitVec.addInt (← readReg Register.PC) 4)
  /- let _ ← execute (.RTYPE ⟨rs2, rs1, rd, rop.ADD⟩) -/
  let _ ← execute_RTYPE rs2 rs1 rd rop.ADD
  pure ()

even though this is precisely what you get if you pattern-match out .RTYPE.

Is this expected? I know there are some uncomputable functions in the generated code here, but judging from their names it seems like they're all for decoding/encoding instructions and execute shouldn't really involve them?

Thank you for your time!

The Lean model is generated at 3dc7e1c with Sail commit rems-project/sail@5794bf15

[GZGavinZhao]

I'm only interested in using RV32I, but after I trace out the code, even execute_STORE and execute_LOAD have to be noncomputable. Is noncomputable unavoidable for both load and store?

[Timmmm]

I don't know anything really about Lean but I did see that some people are working on an executable Lean version of the RISC-V Sail model, which seems to run into similar issues.

[GZGavinZhao]

Thank you so much for the info! This is really helpful. I'll ask the folks over there and see if they have any thoughts.

[GZGavinZhao]

Closing since this is not a problem from the Sail spec.