tchajed/perennial-example-proof
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
No description
78 commits 1 branch 0 tags 84 KiB
  • Makefile 58.7%
  • Rocq Prover 32.4%
  • Go 8.9%
Find a file
Exact
Tej Chajed 9867da2f30
 Revert "Add -j to opam install" 
This reverts commit ae37b3d7d8.
2025-12-12 07:13:08 -06:00
.github/workflows Revert "Add -j to opam install" 2025-12-12 07:13:08 -06:00
src Add rocq dep args 2025-12-03 13:16:04 -06:00
.gitignore Update gitignore 2025-12-05 16:26:15 -06:00
_RocqProject Start fixing things 2025-11-25 20:56:35 -06:00
example-proof.opam Avoid redundant GOCACHE spec 2025-12-05 10:04:39 -06:00
example.go Add another proof 2025-11-25 21:57:04 -06:00
example_test.go Add some example Go code to be verified 2025-11-25 20:52:34 -06:00
go.mod Bump go dependencies 2025-12-05 09:40:59 -06:00
go.sum Bump go dependencies 2025-12-05 09:40:59 -06:00
goose.toml Add goose.toml 2025-12-01 08:37:51 -06:00
LICENSE Add license file 2025-11-25 20:53:26 -06:00
Makefile Fix make clean 2025-12-03 13:36:43 -06:00
README.md Tweak installation instructions 2025-12-06 21:17:15 -06:00

README.md

Perennial example program proof

CI

This repo demonstrates how to depend on perennial via opam and carry out a program proof. It includes some Go code, translates it with Goose, and then includes a proof using Perennial.

This setup demonstrates configuring Perennial using opam and CI using tchajed/setup-rocq, a new action that will cache opam dependencies.

Build

You will need Go 1.24+ and opam installed.

To install the Rocq dependencies, run opam pin --no-action . and opam install --deps-only .

To build, run make.