Need another wf1 variant for actions that require additional parameters (e.g., Message)

[marshtompsxd]

Currently, ourwf1 talks about actions and their preconditions/postconditions

#[verifier(external_body)]
pub proof fn wf1<T>(spec: TempPred<T>, next: ActionPred<T>, forward: ActionPred<T>, p: StatePred<T>, q: StatePred<T>)
    requires
        valid(p.lift().and(next.lift()).implies(p.lift_prime().or(q.lift_prime()))),
        valid(p.lift().and(next.lift()).and(forward.lift()).implies(q.lift_prime())),
        valid(p.lift().implies(tla_enabled(forward))),
        valid(spec.implies(always(next.lift()).and(weak_fairness(forward)))),
    ensures
        valid(spec.implies(p.lift().leads_to(q.lift()))),
{}

We use wf1 to get the initial leads_to in liveness proof. In a not very precise way, this wf1 talks about the scheduling between different actions, based on the weak_fairness assumption.

But it seems that we need another wf1 variant for actions that also takes some additional parameter, like the incoming message, since we need to do some "scheduling" between the messages that need to be handled by the same action.

Consider that we have an action like

pub open spec some_action(s, s_prime) -> bool {
  exists |m :Message| // do different things for different message m
}

We need some assumptions about the scheduling between messages that some_action can take, like "if a particular message m remains ready to be handled, some_action will eventually pick and handle this particular message".

[marshtompsxd]

We have some good progress on dealing with actions that are parameterized on the message.

The problem was that it is very difficult to directly apply wf1 to the existentially quantified action (e.g., |a: Action| { exists |m: Message| handle_message(a.s, a.s', m) }), we can just instantiate the action by feeding a concrete message that appears in our liveness path and apply wf1 to it.

More concretely, when calling wf1, we need to provide next, forward, p and q:

• next basically includes every action including the existentially quantified action
• forward is a concrete action instantiated by the message we care about during the proof
• p is the precondition for that particular message
• q is the postcondition for that particular message

Besides, we also need the weak_fairness assumption for the action of that particular message as well.

[marshtompsxd]

Implemented in #32