Skip to content

Conversation

lgaeher
Copy link
Collaborator

@lgaeher lgaeher commented Oct 15, 2025

Description of the changes

This updates the Rust version to 1.91-nightly, adapting the code accordingly in some places.
In a future MR, we should also adapt to edition = 2024. (I could take care of that)

Accordingly, this updates RefinedRust to the current version, adapting the annotated specifications to RefinedRust's new more compact specification format.

Type of change

  • [ x ] Refactorization (non-breaking change which improves code quality)

How to test this PR?

CI should test that this does not break the build and verification.

Signed-off-by: Lennard Gäher <[email protected]>
@lgaeher lgaeher requested a review from wojciechozga October 15, 2025 08:23
@wojciechozga
Copy link
Member

wojciechozga commented Oct 15, 2025

Hi Lennard, thanks for this MR, I see you did a lot of solid work. Could you also update the README inside the verification/ directory so that we have a human readable up-to-date overview of what has been verified so far? I refer to this https://github.com/IBM/ACE-RISCV/tree/main/verification

The extra poofs I refer are for example in below files:

  • verification/rust_proofs/ace/proofs/proof_core_page_allocator_page_Page_core_page_allocator_page_UnAllocated_init.v
  • verification/theories/page_allocator/page.v
  • verification/theories/page_table/page_table.v

Signed-off-by: Lennard Gäher <[email protected]>
@lgaeher
Copy link
Collaborator Author

lgaeher commented Oct 20, 2025

Thanks for the comments! I took a look over the readme and updated it where necessary.

This PR doesn't substantially change the amount of code that has been verified so far (this will be part of the future MR upstreaming new verification results). The new verification only includes some minor things, like strengthening the specs of read and write.
The extra proof files you're referring to should be covered by the current status for the page token, page allocator, and page table.

In the next MR, I'll also adapt the table to reflect the then-current status.

@wojciechozga
Copy link
Member

Thank you! LGTM

@wojciechozga wojciechozga merged commit 1aaabb9 into IBM:main Oct 20, 2025
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants