Lean emulator by Ptival · Pull Request #1541 · riscv/sail-riscv

Ptival · 2026-02-10T01:02:42Z

Opening this pull request for discussion about what it would take to integrate these changes upstream.

This PR contains:

a frontend to start an emulator based on Lean extracted from SAIL RISC-V,
a CI job that builds said emulator, and tests it on some ELF files.

There are, however, a couple of things that ought to be discussed:

In order to parse ELF files, this adds a dependency to ELFSage. Well, almost, the project is purposefully kept compatible with an old version of Lean (see here), so we forked and modernized it. This is a new dependency. I have found it fairly easy to maintain, but I wanted to be upfront about it.
Our "main" is not the cleanest, I might do a tiny bit of refactoring, but please let us know whether it would require significant changes to merge.
I have extended the Lean workflow to test the extracted emulator. Unfortunately, we have to re-extract the Lean code with a smaller set of modules to get less prohibitive compilation times, and then also extract the ELF files. There might be nicer ways of achieving this without all the redundancy here, but I'm neither an expert at CMake or CI, so I'm open to ideas.

Putting this as a draft request for now.

.github/workflows/compile-lean.yml

github-actions · 2026-02-10T01:48:18Z

Test Results

2 314 tests ±0 2 314 ✅ ±0 31m 24s ⏱️ +4s
1 suites ±0 0 💤 ±0
1 files ±0 0 ❌ ±0

Results for commit 1a4ce49. ± Comparison against base commit c4d3140.

♻️ This comment has been updated with latest results.

pmundkur

This is really great!

test/CMakeLists.txt

Timmmm · 2026-02-10T20:24:37Z

I agree this is great! I don't see any issue with merging it except potentially that not many of us really know Lean. Would you be willing to maintain it. Also what are you using it for, just out of curiosity?

(And on the other hand, learning Lean has been on my todo list for ages so maybe this is a good excuse to finally get around to it!)

jprider63 · 2026-02-17T17:13:23Z

I agree this is great! I don't see any issue with merging it except potentially that not many of us really know Lean. Would you be willing to maintain it. Also what are you using it for, just out of curiosity?

(And on the other hand, learning Lean has been on my todo list for ages so maybe this is a good excuse to finally get around to it!)

There's a group of us at Galois and Cambridge who have been working on Sail's Lean backend so we can help if things break.

Ptival · 2026-02-23T18:31:04Z

Alright, I have made a lot of changes, and it's back to being reviewable:

I have moved the whole logic of building and running the Lean emulator in CMake. Now the CI only calls the appropriate CMake target, much nicer.
In order to support printing out the logging of the emulator run, I needed to pass -D PRINT_EFFECTS to sail. But there was no way to do so from the current CMake setup, so I added an option PRINT_EFFECTS that, when set, adds -D PRINT_EFFECTS to sail invocations.
I wanted to use the status code of the emulator run as the status code of the process, so that a failing emulator run would be a failing run for CI. Unfortunately, the original loop did not return the result. If this is okay with everyone, I'm suggesting a change where loop returns the exit code of the code being looped. I have updated one use that doesn't care about it to throw it away, and I'm demonstrating in the emulator main function its use.
As part of having loop return a status code, I reorganized its control flow to have a clearer single exit point, rather than the current state where the handling of the exit state happens mid-loop.

EDIT: The CI is currently failing because of this limitation:
rems-project/sail#1624

pmundkur

This needs a pre-commit fix for CI.

Does the Lean emulator need an unusual amount of CPU/memory resources to build? It's been building for quite a while on my desktop.

pmundkur · 2026-02-23T21:24:30Z

lean_emulator/lake-manifest.json

This file needs to pass pre-commit checks. See

sail-riscv/CONTRIBUTING.md

Line 33 in c4d3140

We recommend installing pre-commit hooks that ensure certain basic coding

I will look at the pre-commit fix.

As for the resources, I have been building it on a powerful laptop so I'm not sure.
Anecdotally, on our Github CI, the Lean emulator build seems to take ~8 minutes.

I fixed the pre-commit problem. As for the slowness of it, I'm open to suggestions, in particular:

maybe this could be run daily rather than per commit?

we could definitely trim the list of ELF files to test, it's somewhat arbitrary.

Timmmm · 2026-02-26T14:19:14Z

model/postlude/step.sail

 }

-function loop () : unit -> unit = {
+function loop () : unit -> int = {


Suggested change

function loop () : unit -> int = {

function loop () : unit -> nat = {

Presumably?

Good point, in fact I'm not sure what a Sail int is, so maybe we should be careful.

It seems we start with a htif_exit_code, with declared type bits(64), so I guess this is a sign-agnostic view of it.

I wrote int because I had in mind the typical C status codes, e.g. return -1;, where they are typically considered signed. But this is likey inconsistent with the call to unsigned at:

let exit_val = unsigned(htif_exit_code);

So the question is, either:

we want to view exit codes as signed, in which case we would leave int but replace unsigned(...) with signed(...), or,

we want to view exit codes as unsigned, in which case we would replace int with nat.

Do you have more knowledge on the reasonable thing to do here?

Timmmm · 2026-02-26T14:19:59Z

lean_emulator/test_lean_emulator.cmake

+)
+foreach(file IN LISTS LEAN_EMULATOR_TEST_ELFS)
+    message(STATUS "Testing Lean emulator on file ${file}")
+    execute_process(


Wouldn't it make more sense to add lake build ... as a normal CMake target, and then add these as CTest tests? I can sketch out the code if you don't want to learn CMake (which would be very very understandable!)

Please do! I am indeed not used to CMake and have been teaching myself in order to produce what you're currently seeing.

Hi @Timmmm , just checking on whether you have bandwidth to look into this, or if I should figure it out.

nadime15 reviewed Feb 10, 2026

View reviewed changes

.github/workflows/compile-lean.yml Outdated Show resolved Hide resolved

pmundkur reviewed Feb 10, 2026

View reviewed changes

test/CMakeLists.txt Outdated Show resolved Hide resolved

Ptival mentioned this pull request Feb 17, 2026

private functions in Stateen support broke Lean extraction #1554

Closed

Ptival force-pushed the lean_emulator_ci branch 3 times, most recently from d22911a to e9c4ec3 Compare February 23, 2026 18:21

Ptival force-pushed the lean_emulator_ci branch from e9c4ec3 to 32b1eec Compare February 23, 2026 19:36

jprider63 added 2 commits February 23, 2026 12:14

Better errors on unsupported properties in Lean emulator

d9e6b4c

introduce Lean emulator

210ddb8

Ptival force-pushed the lean_emulator_ci branch from 32b1eec to b29db0f Compare February 23, 2026 20:32

pmundkur reviewed Feb 23, 2026

View reviewed changes

CI: test Lean emulator on some ELF files

1a4ce49

Ptival force-pushed the lean_emulator_ci branch from b29db0f to 1a4ce49 Compare February 24, 2026 17:24

Ptival marked this pull request as ready for review February 25, 2026 21:10

Timmmm reviewed Feb 26, 2026

View reviewed changes

	function loop () : unit -> int = {
	function loop () : unit -> nat = {

Conversation

Ptival commented Feb 10, 2026

Uh oh!

Uh oh!

github-actions bot commented Feb 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Test Results

Uh oh!

pmundkur left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Timmmm commented Feb 10, 2026

Uh oh!

jprider63 commented Feb 17, 2026

Uh oh!

Ptival commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pmundkur left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Feb 10, 2026 •

edited

Loading

Ptival commented Feb 23, 2026 •

edited

Loading

pmundkur left a comment •

edited

Loading