Challenges during proving liveness for mini controller

[marshtompsxd]

While working on proving liveness of the mini controller #54 , I encountered some technical challenges. Some might require more support from Verus, and some need us to develop more lemmas.

Issue 1: Universal/existential quantifiers for temporal predicates

We need universal and existential quantifiers (on messages) everywhere in the proof, but it is hard to develop such proof with our current tla library. To give an example, the second assertion cannot pass:

let p = lift_state(|s: State| forall |msg: Message| #[trigger] s.message_sent(msg));
let q = tla_forall(|msg: Message| lift_state(|s: State| s.message_sent(msg)));
assert(valid(p.implies(q)));
assert(valid(q.implies(p))); // this assert fails

I am trying to develop more automation for tla_forall but I am often blocked by the issue that I cannot set FnSpec call as triggers, or set no triggers in forall.

[lalithsuresh]

Worth running this by @utaal at some point.

[marshtompsxd]

no longer challenges