ssprove

ssprove copied to clipboard

Jasmin, Mathcomp2 and Coq.8.18.0

2

cmester0

In the paper it is now called `dom` for domain.

TheoWinterhalter

The name is not great, instead we should have relations between code / packages and their interfaces and state.

TheoWinterhalter

Maybe rules and tactics should not be called synchronous and asynchronous but perhaps be one-sided or two-sided or left- and right-biased. `ssprove_sync` could also become `ssprove_cong`.

TheoWinterhalter

factor out the OTP proof to work with an abstract xor

1

haselwarter

Refactor semantics

3

We can discuss about it in this draft PR.

TheoWinterhalter

Generate .opam and CI from coq-community/templates

8

The idea is to use https://github.com/coq-community/templates so that we probably use something more principled for our CI jobs. The template can do more but I'd say we're good with these...

TheoWinterhalter

Nix flake suppport and CI

3

Dear SSProvers, this PR adds the following: - support loading `SSProve` via Nix flakes - additional CI jobs: - to test the added Nix flake - to test the CI...

sertel