A Rocq model of a Linux process that runs a RISC-V binary
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.1.tar.gz
sha512=0a65fb0f09273fa642f33a87e978b5ddb8748013f34edd45c67a9f33b8d1c2313d9d15ee019332f378c43fe79eff47a2343fec87f9a441e770bd1f7737c01c0b
Description
The Rocq theory LinuxProcessSemantics: a model of a Linux process that runs an RV64GC binary (LinuxProcessSem, Riscv), and the statements that proofs about such binaries are checked against (EquivalenceDefinition): observable equivalence of two binaries, termination, and patch classifiers. Also installs two helper tools, elf-snapshot and gen-fd-lemmas (Python 3, standard library only).
Published: 24 Oct 2026
Dependencies (7)
-
rocq-read-file
>= "0.0.2" -
coq-flocq
>= "4.2" -
rocq-stdpp-bitvector
>= "1.13.0" -
rocq-stdpp
>= "1.13.0" -
rocq-stdlib
>= "9.0" -
rocq-core
>= "9.2" -
dune
>= "3.23"
Dev Dependencies
None
Used by (3)
Conflicts
None
On This Page