[Civl] Paxos proof depends on unchecked assumption

[shazqadeer]

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]

cc: @NamrathaG , @bkragl