The inductive sequentialization part of the Paxos proof in Civl depends on some assumptions injected into the left-mover checks for the eliminated actions. To justify these assumptions, the following must be checked for each of A_Paxos, A_StartRound, A_Propose, A_Join, A_Vote, and A_Conclude.
permissions in inputs do not flow to globals
permissions in globals do not flow to inputs of created actions
These conditions are currently not being checked.
shazqadeer
commented
6 hours ago
The inductive sequentialization part of the Paxos proof in Civl depends on some assumptions injected into the left-mover checks for the eliminated actions. To justify these assumptions, the following must be checked for each of A_Paxos, A_StartRound, A_Propose, A_Join, A_Vote, and A_Conclude.