This repo contains a hyperproperty library written in Coq.
As of 2023-12-12, work on this library is still ongoing, and we expect significant changes to the interface to occur.
This library consists of core hyperproperty definitions and proofs
(Hyperproperties.v), two example hyperproperties and proofs
(GuaranteedService.v and ObservationalDeterminism.v), and an example system
(CrashSystem.v).
This code was built with Coq version 8.17.1. To build this library, clone the repo and run:
make
This should verify all proofs in all files.
A small number of lemmas outside of the Hyperproperties.v file are not yet
completed. Note that all proofs inside the Hyperproperties.v file are
complete.
This library currently uses classical logic and assumes the excluded middle for some proofs. Future work aims to remove this dependency.