[Monitor] Support `repeat ...` loops

[ngernest]

Extend the approach described in #172 and clone the scheduler every time we proceed to a new iteration of the repeat loop (see #172 for more details).

[ngernest]

Implementation sketch (based on my meeting with Kevin 2/20):

In the monitor, an argument (parameter to a prot) can take on two forms: it begins as Unknown, then becomes Known(n) for some n (we learn this via assignments and assert_eq in the protocol). Since arguments are immutable, once an argument becomes Known, it remains Known thereafter.

enum Arg {
    Unknown,
    Known(u32)
} 

To handle loop arguments (LoopInt) for repeat ... loops, we want to generalize this scheme using the LoopArg type below:

// The constructors will be explained below
enum LoopArg {
    Unknown, 
    Speculate(u32, StmtId),
    Known(u32)
} 

This type reflects how we learn the value of the LoopArg via control flow. A LoopArg n begins as Unknown. Then, suppose we have the following:

repeat n iterations {      // Loop A
    ...
} 
repeat n iterations {     // Loop B
   ...
} 

When we encounter Loop A, the monitor clones the scheduler into two copies:

• One copy skips Loop A and proceeds to the next immediate statement, setting n := Known(0)
• One copy sets n := Speculate(1, StmtId of Loop 1) and executes the body of Loop A once. (The StmtId is there to disambiguate between different loop statements, since different loops can use the same loop argument n.)
  Afterwards, it clones the schedulers into two copies:
  + One copy exits Loop A immediately, setting n := Known(1) and executes Loop B exactly once (since it knows that n = 1)
  + One copy executes Loop A for another iteration, setting n := Speculate(2, ...)
  and so on.

We maintain the following invariants:

• Speculate(n, loopID) only becomes Known(n) after the corresponding scheduler has executed the body of the loop at loopID exactly n times (note that n can be 0).
• Once a LoopArg becomes Known, we proceed to the next statement that immediately follows the loop (we don't enter the loop body). Moreover, once a LoopArg remains Known, it remains Known thereafter.

Here are illustrations of the two "lattices" for Args and LoopArgs:

Note that the "lattice" for LoopArg forms a right-leaning binary tree with infinite height, where Unknown is the root (the tree has infinite height, since the no. of loop iterations is unbounded). The key point is to know there is no "greatest" element in the "lattice" for LoopArg.

(Aside: I put the term "lattice" in air-quotes, since it's unclear what the notion of "most / least information" is in this lattice -- is Unknown the least or most amount information? It is probably a semilattice since the comparison only goes one way)

Whiteboard sketch: