rem-verification
| Crates.io | rem-verification |
| lib.rs | rem-verification |
| version | 0.1.0 |
| created_at | 2025-03-05 14:35:33.845344+00 |
| updated_at | 2025-03-05 14:35:33.845344+00 |
| description | Verification tool for the REM toolchain. Built to be implemented into the VSCode extension for REM. Relies on AENEAS and CoQ |
| homepage | |
| repository | https://github.com/RuleBrittonica/rem-verification |
| max_upload_size | |
| id | 1579089 |
| size | 178,832 |
Matthew Britton (RuleBrittonica)
documentation
README
rem-verifyer
This is a toolchain that allows for two .llbc files (generated by CHARON) to be compared for equivalence. This is done using CoQ. The files are converted to CoQ using AENEAS, and the given method(s) are proved to be equivalent through an automatically generated and run proof.
It is important to note that this module has no way to generate the .llbc files. That must be handled externally (i.e. by a standalone install of CHARON or by the rem-cli/(command) tool). At this stage, AENEAS seems to work best on Linux, so it is recommeded to run the program on a Linux machine. It is a WIP to get it working on Windows and MacOS/other UNIX systems.
Requirements:
- CoQ (version 8.18.0)
- AENEAS (https://github.com/AeneasVerif/aeneas)