Program proofs for tulip, using Perennial (the "old" version, prior to new goose).
To build run opam install --deps-only . and then dune build.
You can update the version of perennial used with go tool perennial-cli opam update.
Paths below are relative to src/program_proof/tulip/.
- Action lemmas:
invariance/andpaxos/invariance/. Some simple protocol updates are proved directly in program proofs. - Program specifications and proofs:
program/andpaxos/program/. - Permissions and interaction rules:
res*.vin the Tulip and Paxos proof roots.
The ten PSM module types (Section 5.1, Figure 13) map to the following definitions:
| Module | File | Predicate |
|---|---|---|
| Transaction system | inv_txnsys.v | txnsys_inv |
| Key | inv_key.v | key_inv |
| Replica group | inv_group.v | group_inv |
| Replica | inv_replica.v | replica_inv |
| Tulip file | inv.v | replica_file_inv |
| Tulip network | inv.v | tulip_network_inv |
| Multi-Paxos proposers | paxos/inv.v | paxos_inv (excluding the per-acceptor node_inv) |
| Multi-Paxos acceptor | paxos/inv.v | node_inv |
| Multi-Paxos file | paxos/inv.v | node_file_inv |
| Multi-Paxos network | paxos/inv.v | paxos_network_inv |
- Strict serializability (Section 5):
program/txn/txn_run.v,
wp_Txn__Run, states the client-facing atomic transaction specification. - Prepare example (Section 5.2, Figure 11):
invariance/prepare.v,
group_inv_prepare, and its use in program/txn/txn_prepare.v. - Tulip and Multi-Paxos interface (Section A.4): inv_txnlog.v connects their command pools and logs; program/txnlog/txnlog.v proves the adapter.