Draft PR for lean riscv emulator

[jn80842]

Current state of the lean emulator, using the version of sail-riscv that's built here.

Executing an ELF file from the test/lean-riscv directory like so:

LEAN_BACKTRACE=1 lake exec run-riscv-lean -- /PATH/TO/sail-riscv/test/riscv-tests/rv32mi-p-breakpoint.elf

produces this error message:

error: /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/LeanRiscv.lean:77:4: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'LeanRV64D.Functions.sail_main', and it does not have executable code
error: /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/LeanRiscv.lean:88:4: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'my_main', and it does not have executable code
error: Lean exited with code 1

[github-actions]

Test Results

   13 files     28 suites   0s ⏱️
  880 tests   879 ✅ 0 💤 0 ❌ 1 🔥
4 076 runs  4 075 ✅ 0 💤 0 ❌ 1 🔥

For more details on these errors, see this check.

Results for commit 7a02b9d.

♻️ This comment has been updated with latest results.

[ineol]

@Alasdair @tperami this would not be needed with the new concurrency interface right? Do you know if it's going to be used in the RISC-V model soon?

[ineol]

Thank you for the PR! I think the RISC-V specific code belongs in the RISC-V sail repository, unless there are other opinions?

[ineol]

I PRd the executable model to the risc-v repo here. This makes the OfNat trick of this PR unnecessary.

I think you should be able to use the model generated by the PR above by running cmake --build build/ --target generated_lean_rv64d_executable as a dependency for your executable, and then make a PR to the RISC-V model repo with the executable

[jn80842]

With the new executable lean model, running an ELF file gives me the following errors:

✖ [164/207] Building LeanRV64DExecutable.RiscvCallbacks:c.o
trace: .> /Users/newcomb/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577/bin/clang -c -o /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/Lean_RV64D_executable/Lean_RV64D_executable/.lake/build/ir/LeanRV64DExecutable/RiscvCallbacks.c.o.export /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/Lean_RV64D_executable/Lean_RV64D_executable/.lake/build/ir/LeanRV64DExecutable/RiscvCallbacks.c -I /Users/newcomb/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/newcomb/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577 -nostdinc -isystem /Users/newcomb/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
/Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/Lean_RV64D_executable/Lean_RV64D_executable/.lake/build/ir/LeanRV64DExecutable/RiscvCallbacks.c:7218:1: fatal error: bracket nesting level exceeded maximum of 256
 7218 | {
      | ^
/Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/Lean_RV64D_executable/Lean_RV64D_executable/.lake/build/ir/LeanRV64DExecutable/RiscvCallbacks.c:7218:1: note: use -fbracket-depth=N to increase maximum nesting level
1 error generated.
error: external command '/Users/newcomb/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577/bin/clang' exited with code 1
⚠ [183/207] Built LeanRV64DExecutable.RiscvVmem
warning: LeanRV64DExecutable/RiscvVmem.lean:191:4: declaration uses 'sorry'
✖ [205/207] Building Main
trace: .> LEAN_PATH=/Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/Cli/.lake/build/lib/lean:/Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/ELFSage/.lake/build/lib/lean:/Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/packages/Lean_RV64D_executable/Lean_RV64D_executable/.lake/build/lib/lean:/Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/build/lib/lean /Users/newcomb/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-8577/bin/lean /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/Main.lean -R /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv -o /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/build/lib/lean/Main.olean -i /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/build/lib/lean/Main.ilean -c /Users/newcomb/galois/SAILRISCV/glssail/sail/test/lean-riscv/.lake/build/ir/Main.c --json
error: Main.lean:3:4: 'main' has already been declared
error: Lean exited with code 1
Some required builds logged failures:
- LeanRV64DExecutable.RiscvTypes:c.o
- LeanRV64DExecutable.RiscvCallbacks:c.o
- Main
error: build failed

[Alasdair]

Looks like an issue with the Lean code generator? If you can control the options it uses you could try using the -fbracket-depth option like it says.

In Sail->C we avoid this by flattening the intermediate representation for deeply nested functions. I don't know if Lean's code generator has the same ability.

[ineol]

@jn80842 try to add moreLeancArgs = ["--tstack=400000"] in the file lakefile.toml? I think there is a typo in the file Sail is generating (missing c character)

[javra]

The other error you're getting is because the Sail output already includes a main function, so better call this differently or put it in a namespace.

[ineol]

The issue is that the risc-v model has its own main function that we don't want to use here. I changed my executable model branch to not compile the riscv_main.sail file, so this problem should be fixed if you pull on that branch @jn80842

[jn80842]

Thanks everyone for your help! I was able to resolve the C errors by adding

moreLeancArgs = ["-fbracket-depth=512"]

to lakefile.toml (changing moreLeanArgs = ["--tstack=400000"] to moreLeancArgs = ["--tstack=400000"] caused failures as apparently tstack isn't a clang option?)

[GZGavinZhao]

Hi there, sorry for the noise, I'm curious whether you've solved the noncomputable errors. I'm trying to prove some properties on the execute function and the noncomputable makes Lean timeout at isDefEq. I traced out the code and it seems like noncomputable propagates up to execute through execute_STORE and execute_LOAD.

[javra]

@GZGavinZhao Have you seen this repo? Contains an executable build of the model.

Otherwise, the timeouts at isDefEq might be avoidable by unfolding definitions in goals manually using the unfold tactic before using any simplicifer on them.