Add C++ code generation and test scenario (#310)

* add parameters to byzantine send action

* make net not trusted

it's not necessary since for proofs Ivy will assume that the environment
does not break action preconditions

* use require instead of assume

it seems that assume is not checked when other isolates call!

* add comment

* add comment

* run with random seed

* make domain model extractable to C++

* substitute require for assume

assumes in an action are not checked when the action is called! I.e.
they place no requirement on the caller; we're just assuming that the
caller is going to do the right thing. This wasn't very important here
but it leade to a minor inconsistency slipping through.

* make the net isolate not trusted

there was no need for it

* add tendermint_test.ivy

contains a simple test scenario that show that the specification is no
vacuuous

* update comment

* add comments

* throw if trying to parse nset value in the repl

* add comment

* minor refactoring

ivy-proofs/abstract_tendermint.ivy

@@ -165,7 +165,9 @@ module abstract_tendermint = {
 
     action misbehave = {
 # Byzantine nodes can claim they observed whatever they want about themselves,
-# but they cannot remove observations.
+# but they cannot remove observations. Note that we use assume because we don't
+# want those to be checked; we just want them to be true (that's the model of
+# Byzantine behavior).
         observed_prevoted(N,R,V) := *;
         assume (old observed_prevoted(N,R,V)) -> observed_prevoted(N,R,V);
         assume well_behaved(N) -> old observed_prevoted(N,R,V) = observed_prevoted(N,R,V);

ivy-proofs/accountable_safety_1.ivy

@@ -117,6 +117,7 @@ isolate abstract_accountable_safety = {
             }
             proof {
                 apply complete_induction # the two subgoals (base case and inductive case) are then discharged automatically
+                # NOTE: this can take a long time depending on the SMT random seed (to try a different seed, use `ivy_check seed=$RANDOM`
             }
         }
     } with this, round, nset, accountable_bft.max_2f_byzantine, defs.observed_equivocation_def, defs.observed_unlawful_prevote_def, defs.accountability_violation_def, defs.agreement_def

ivy-proofs/check_proofs.sh

@@ -4,10 +4,11 @@
 
 success=0
 log_dir=$(cat /dev/urandom | tr -cd 'a-f0-9' | head -c 6)
+cmd="ivy_check seed=$RANDOM"
 mkdir -p output/$log_dir
 
 echo "Checking classic safety:"
-res=$(ivy_check classic_safety.ivy | tee "output/$log_dir/classic_safety.txt" | tail -n 1)
+res=$($cmd classic_safety.ivy | tee "output/$log_dir/classic_safety.txt" | tail -n 1)
 if [ "$res" = "OK" ]; then
   echo "OK"
 else
@@ -16,7 +17,7 @@ else
 fi
 
 echo "Checking accountable safety 1:"
-res=$(ivy_check accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1)
+res=$($cmd accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1)
 if [ "$res" = "OK" ]; then
   echo "OK"
 else
@@ -25,7 +26,7 @@ else
 fi
 
 echo "Checking accountable safety 2:"
-res=$(ivy_check complete=fo accountable_safety_2.ivy | tee "output/$log_dir/accountable_safety_2.txt" | tail -n 1)
+res=$($cmd complete=fo accountable_safety_2.ivy | tee "output/$log_dir/accountable_safety_2.txt" | tail -n 1)
 if [ "$res" = "OK" ]; then
   echo "OK"
 else

ivy-proofs/domain_model.ivy

@@ -1,8 +1,4 @@
 #lang ivy1.7
-# ---
-# layout: page
-# title: Proof of Classic Safety
-# ---
 
 include order # this is a file from the standard library (`ivy/ivy/include/1.7/order.ivy`)
 
@@ -32,14 +28,15 @@ isolate round = {
 }
 
 instance node : iterable # nodes are a set with an order, that can be iterated over (see order.ivy in the standard library)
-relation well_behaved(N:node) # whether a node is well-behaved or not. NOTE: Use only in the proof! Nodes do know know that.
+
+relation well_behaved(N:node) # whether a node is well-behaved or not. NOTE: Used only in the proof and the Byzantine model; Nodes do know know who is well-behaved and who is not.
 
 isolate proposers = {
     # each round has a unique proposer in Tendermint. In order to avoid a
     # function from round to node (which makes verification more difficult), we
     # abstract over this function using a relation.
     relation is_proposer(N:node, R:round)
-    action get_proposer(r:round) returns (n:node)
+    export action get_proposer(r:round) returns (n:node)
     specification {
         property is_proposer(N1,R) & is_proposer(N2,R) -> N1 = N2
         after get_proposer {
@@ -47,8 +44,8 @@ isolate proposers = {
         }
     }
     implementation {
-    # here we prove that the abstraction is sound
         function f(R:round):node
+        definition f(r:round) = <<<r % `node.size`>>>
         definition is_proposer(N,R) = N = f(R)
         implement get_proposer {
             n := f(r);
@@ -64,6 +61,8 @@ isolate value = { # the type of values
         property ~valid(nil)
     }
     implementation {
+        interpret value -> bv[2]
+        definition nil = <<< -1 >>> # let's say nil is -1
         definition valid(V) = V ~= nil
     }
 }
@@ -73,6 +72,60 @@ object nset = { # the type of node sets
     relation member(N:node, S:nset) # set-membership relation
     relation is_quorum(S:nset) # intent: sets of cardinality at least 2f+i+1
     relation is_blocking(S:nset) # intent: at least f+1 nodes
+    export action insert(s:nset, n:node) returns (t:nset)
+    export action empty returns (s:nset)
+    implementation {
+        # NOTE: this is not checked at all by Ivy; it is however useful to generate C++ code and run it for debugging purposes
+        <<< header
+            #include <set>
+            #include <exception>
+            namespace hash_space {
+                template <typename T>
+                    class hash<std::set<T> > {
+                public:
+                    size_t operator()(const std::set<T> &s) const {
+                        hash<T> h;
+                        size_t res = 0;
+                        for (const T &e : s)
+                            res += h(e);
+                        return res;
+                    }
+                };
+        }
+        >>>
+        interpret nset -> <<< std::set<`node`> >>>
+        definition member(n:node, s:nset) = <<< `s`.find(`n`) != `s`.end() >>>
+        definition is_quorum(s:nset) = <<< 3*`s`.size() > 2*`node.size` >>>
+        definition is_blocking(s:nset) = <<< 3*`s`.size() > `node.size` >>>
+        implement empty {
+            <<<
+            >>>
+        }
+        implement insert {
+            <<<
+                `t` = `s`;
+                `t`.insert(`n`);
+            >>>
+        }
+    <<< encode `nset`
+
+        std::ostream &operator <<(std::ostream &s, const `nset` &a) {
+            s << "{";
+            for (auto iter = a.begin(); iter != a.end(); iter++) {
+                if (iter != a.begin()) s << ", ";
+                s << *iter;
+            }
+            s << "}";
+            return s;
+        }
+
+        template <>
+        `nset` _arg<`nset`>(std::vector<ivy_value> &args, unsigned idx, long long bound) {
+            throw std::invalid_argument("Not implemented"); // no syntax for nset values in the REPL
+        }
+
+    >>>
+    }
 }
 
 object classic_bft = {
@@ -87,4 +140,4 @@ trusted isolate accountable_bft = {
     private {
         property [max_2f_byzantine] exists N . well_behaved(N) & nset.member(N,Q) # every quorum has a well-behaved member
     }
-}# with nset
+}

ivy-proofs/network_shim.ivy

@@ -28,9 +28,7 @@ object msg = {
 }
 
 # This is our model of the network:
-trusted isolate net = {
-# `trusted` indicates to Ivy that this is a trusted object, i.e. we assume
-# without proof that receive is only called when its requirement is true.
+isolate net = {
 
     export action recv(dst:node,v:msg)
     action send(src:node,dst:node,v:msg)
@@ -40,25 +38,21 @@ trusted isolate net = {
     # sense, the network is fully asynchronous. Moreover, there is no
     # requirement that a given message will be received at all.
 
-    specification {
-
-        # The state of the network consists of all the packets that have been
-        # sent so far, along with their destination.
-        relation sent(V:msg, N:node)
-
-        after init {
-            sent(V, N) := false
-        }
+    # The state of the network consists of all the packets that have been
+    # sent so far, along with their destination.
+    relation sent(V:msg, N:node)
 
-        before send {
-            sent(v,dst) := true
-        }
+    after init {
+        sent(V, N) := false
+    }
 
-        before recv {
-            require sent(v,dst) # only sent messages can be received.
-        }
+    before send {
+        sent(v,dst) := true
     }
 
+    before recv {
+        require sent(v,dst) # only sent messages can be received.
+    }
 }
 
 # The network shim sits on top of the network and, upon receiving a message,
@@ -100,7 +94,6 @@ isolate shim = {
         }
     }
 
-    # In contrast to the network object, the shim is not a trusted component.
     # Here we give an implementation of it that satisfies its specification:
     implementation {
 

ivy-proofs/tendermint.ivy

@@ -60,7 +60,7 @@ include network_shim
 module tendermint(abstract_protocol) = {
 
     # the initial value of a node:
-    parameter init_val(N:node): value
+    function init_val(N:node): value
 
     # the three type of steps
     object step_t = {
@@ -129,7 +129,7 @@ module tendermint(abstract_protocol) = {
         }
 
         export action start = {
-            assume ~_has_started;
+            require ~_has_started;
             _has_started := true;
             # line 10
             call startRound(0);
@@ -171,17 +171,15 @@ module tendermint(abstract_protocol) = {
             call shim.broadcast(n,m);
         }
 
-
         implement shim.proposal_handler.handle(msg:msg) {
             _recved_proposal(msg.m_src, msg.m_round, msg.m_value, msg.m_vround) := true;
         }
 
-
         # line 22-27
         export action l_22(v:value) = {
-            assume _has_started;
-            assume _recved_proposal(proposers.get_proposer(round_p), round_p, v, round.minus_one);
-            assume step = step_t.propose;
+            require _has_started;
+            require _recved_proposal(proposers.get_proposer(round_p), round_p, v, round.minus_one);
+            require step = step_t.propose;
 
             if (value.valid(v) & (lockedRound = round.minus_one | lockedValue = v)) {
                 call broadcast_prevote(round_p, v); # line 24
@@ -195,17 +193,15 @@ module tendermint(abstract_protocol) = {
             step := step_t.prevote;
         }
 
-
-
         # line 28-33
         export action l_28(r:round, v:value, vr:round, q:nset) = {
-            assume _has_started;
-            assume r = round_p;
-            assume _recved_proposal(proposers.get_proposer(r), r, v, vr);
-            assume nset.is_quorum(q);
-            assume nset.member(N,q) -> _recved_prevote(N,vr,v);
-            assume step = step_t.propose;
-            assume vr >= 0 & vr < r;
+            require _has_started;
+            require r = round_p;
+            require _recved_proposal(proposers.get_proposer(r), r, v, vr);
+            require nset.is_quorum(q);
+            require nset.member(N,q) -> _recved_prevote(N,vr,v);
+            require step = step_t.propose;
+            require vr >= 0 & vr < r;
 
             # line 29
             if (value.valid(v) & (lockedRound <= vr | lockedValue = v)) {
@@ -228,19 +224,17 @@ module tendermint(abstract_protocol) = {
         }
 
         implement shim.prevote_handler.handle(msg:msg) {
-            assume msg.m_vround = round.minus_one;
             _recved_prevote(msg.m_src, msg.m_round, msg.m_value) := true;
         }
 
-
         # line 34-35
         export action l_34(r:round, q:nset) = {
-            assume _has_started;
-            assume round_p = r;
-            assume nset.is_quorum(q);
-            assume exists V . nset.member(N,q) -> _recved_prevote(N,r,V);
-            assume step = step_t.prevote;
-            assume ~done_l34(r);
+            require _has_started;
+            require round_p = r;
+            require nset.is_quorum(q);
+            require exists V . nset.member(N,q) -> _recved_prevote(N,r,V);
+            require step = step_t.prevote;
+            require ~done_l34(r);
             done_l34(r) := true;
 
             prevote_timer_scheduled(r) := true;
@@ -249,15 +243,15 @@ module tendermint(abstract_protocol) = {
 
         # line 36-43
         export action l_36(r:round, v:value, q:nset) = {
-            assume _has_started;
-            assume r = round_p;
-            assume exists VR . _recved_proposal(proposers.get_proposer(r), r, v, VR);
-            assume nset.is_quorum(q);
-            assume nset.member(N,q) -> _recved_prevote(N,r,v);
-            assume value.valid(v);
-            assume step = step_t.prevote | step = step_t.precommit;
-
-            assume ~done_l36(r,v);
+            require _has_started;
+            require r = round_p;
+            require exists VR . round.minus_one <= VR & VR < r & _recved_proposal(proposers.get_proposer(r), r, v, VR);
+            require nset.is_quorum(q);
+            require nset.member(N,q) -> _recved_prevote(N,r,v);
+            require value.valid(v);
+            require step = step_t.prevote | step = step_t.precommit;
+
+            require ~done_l36(r,v);
             done_l36(r, v) := true;
 
             if step = step_t.prevote {
@@ -270,17 +264,15 @@ module tendermint(abstract_protocol) = {
 
             validValue := v; # line 42
             validRound := r; # line 43
-
         }
 
-
         # line 44-46
         export action l_44(r:round, q:nset) = {
-            assume _has_started;
-            assume r = round_p;
-            assume nset.is_quorum(q);
-            assume nset.member(N,q) -> _recved_prevote(N,r,value.nil);
-            assume step = step_t.prevote;
+            require _has_started;
+            require r = round_p;
+            require nset.is_quorum(q);
+            require nset.member(N,q) -> _recved_prevote(N,r,value.nil);
+            require step = step_t.prevote;
 
             call broadcast_precommit(r, value.nil); # line 45
             step := step_t.precommit; # line 46
@@ -294,23 +286,21 @@ module tendermint(abstract_protocol) = {
             m.m_src := n;
             m.m_round := r;
             m.m_value := v;
-            m.m_vround := round.minus_one;
             call shim.broadcast(n,m);
         }
 
         implement shim.precommit_handler.handle(msg:msg) {
-            assume msg.m_vround = round.minus_one;
             _recved_precommit(msg.m_src, msg.m_round, msg.m_value) := true;
         }
 
 
         # line 47-48
         export action l_47(r:round, q:nset) = {
-            assume _has_started;
-            assume round_p = r;
-            assume nset.is_quorum(q);
-            assume nset.member(N,q) -> exists V . _recved_precommit(N,r,V);
-            assume ~done_l47(r);
+            require _has_started;
+            require round_p = r;
+            require nset.is_quorum(q);
+            require nset.member(N,q) -> exists V . _recved_precommit(N,r,V);
+            require ~done_l47(r);
             done_l47(r) := true;
 
             precommit_timer_scheduled(r) := true;
@@ -319,11 +309,11 @@ module tendermint(abstract_protocol) = {
 
         # line 49-54
         export action l_49_decide(r:round, v:value, q:nset) = {
-            assume _has_started;
-            assume exists VR . _recved_proposal(proposers.get_proposer(r), r, v, VR);
-            assume nset.is_quorum(q);
-            assume nset.member(N,q) -> _recved_precommit(N,r,v);
-            assume decision = value.nil;
+            require _has_started;
+            require exists VR . round.minus_one <= VR & VR < r & _recved_proposal(proposers.get_proposer(r), r, v, VR);
+            require nset.is_quorum(q);
+            require nset.member(N,q) -> _recved_precommit(N,r,v);
+            require decision = value.nil;
 
             if value.valid(v) {
                 decision := v;
@@ -334,19 +324,19 @@ module tendermint(abstract_protocol) = {
 
         # line 55-56
         export action l_55(r:round, b:nset) = {
-            assume _has_started;
-            assume nset.is_blocking(b);
-            assume nset.member(N,b) -> exists V,VR . _recved_proposal(N,r,V,VR) | _recved_prevote(N,r,V) | _recved_precommit(N,r,V);
-            assume r > round_p;
+            require _has_started;
+            require nset.is_blocking(b);
+            require nset.member(N,b) -> exists VR . round.minus_one <= VR & VR < r & exists V . _recved_proposal(N,r,V,VR) | _recved_prevote(N,r,V) | _recved_precommit(N,r,V);
+            require r > round_p;
             call startRound(r); # line 56
         }
 
         # line 57-60
         export action onTimeoutPropose(r:round) = {
-            assume _has_started;
-            assume propose_timer_scheduled(r);
-            assume r = round_p;
-            assume step = step_t.propose;
+            require _has_started;
+            require propose_timer_scheduled(r);
+            require r = round_p;
+            require step = step_t.propose;
             call broadcast_prevote(r,value.nil);
             step := step_t.prevote;
 
@@ -357,10 +347,10 @@ module tendermint(abstract_protocol) = {
 
         # line 61-64
         export action onTimeoutPrevote(r:round) = {
-            assume _has_started;
-            assume prevote_timer_scheduled(r);
-            assume r = round_p;
-            assume step = step_t.prevote;
+            require _has_started;
+            require prevote_timer_scheduled(r);
+            require r = round_p;
+            require step = step_t.prevote;
             call broadcast_precommit(r,value.nil);
             step := step_t.precommit;
 
@@ -369,12 +359,11 @@ module tendermint(abstract_protocol) = {
             prevote_timer_scheduled(r) := false;
         }
 
-
         # line 65-67
         export action onTimeoutPrecommit(r:round) = {
-            assume _has_started;
-            assume precommit_timer_scheduled(r);
-            assume r = round_p;
+            require _has_started;
+            require precommit_timer_scheduled(r);
+            require r = round_p;
             call startRound(round.incr(r));
 
             precommit_timer_scheduled(r) := false;
@@ -385,13 +374,11 @@ module tendermint(abstract_protocol) = {
 
 # Byzantine nodes can send whatever they want, but they cannot send
 # messages on behalf of well-behaved nodes. In practice this is implemented
-# using cryprography (e.g. public-key cryptography).
+# using cryptography (e.g. public-key cryptography).
 
-        export action byzantine_send = {
-            assume ~well_behaved(n);
-            var m:msg;
-            var dst:node;
-            assume ~well_behaved(m.m_src); # cannot forge the identity of well-behaved nodes
+        export action byzantine_send(m:msg, dst:node) = {
+            require ~well_behaved(n);
+            require ~well_behaved(m.m_src); # cannot forge the identity of well-behaved nodes
             call shim.send(n,dst,m);
         }
 
@@ -407,24 +394,27 @@ module tendermint(abstract_protocol) = {
 # preconditions are met, and b) provide a refinement relation.
 
 
-        invariant 0 <= round_p
-        invariant abstract_protocol.left_round(n,R) <-> R < round_p
+        specification {
 
-        invariant lockedRound ~= round.minus_one -> forall R,V . abstract_protocol.locked(n,R,V) <-> R <= lockedRound & lockedValue = V
-        invariant lockedRound = round.minus_one -> forall R,V . ~abstract_protocol.locked(n,R,V)
+            invariant 0 <= round_p
+            invariant abstract_protocol.left_round(n,R) <-> R < round_p
 
-        invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.prevote & shim.sent(M,N) -> abstract_protocol.prevoted(M.m_src,M.m_round,M.m_value)
-        invariant well_behaved(N) & _recved_prevote(N,R,V) -> abstract_protocol.prevoted(N,R,V)
-        invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.precommit & shim.sent(M,N) -> abstract_protocol.precommitted(M.m_src,M.m_round,M.m_value)
-        invariant well_behaved(N) & _recved_precommit(N,R,V) -> abstract_protocol.precommitted(N,R,V)
+            invariant lockedRound ~= round.minus_one -> forall R,V . abstract_protocol.locked(n,R,V) <-> R <= lockedRound & lockedValue = V
+            invariant lockedRound = round.minus_one -> forall R,V . ~abstract_protocol.locked(n,R,V)
 
-        invariant (step = step_t.prevote | step = step_t.propose) -> ~abstract_protocol.precommitted(n,round_p,V)
-        invariant step = step_t.propose -> ~abstract_protocol.prevoted(n,round_p,V)
-        invariant step = step_t.prevote -> exists V . abstract_protocol.prevoted(n,round_p,V)
+            invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.prevote & shim.sent(M,N) -> abstract_protocol.prevoted(M.m_src,M.m_round,M.m_value)
+            invariant well_behaved(N) & _recved_prevote(N,R,V) -> abstract_protocol.prevoted(N,R,V)
+            invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.precommit & shim.sent(M,N) -> abstract_protocol.precommitted(M.m_src,M.m_round,M.m_value)
+            invariant well_behaved(N) & _recved_precommit(N,R,V) -> abstract_protocol.precommitted(N,R,V)
 
-        invariant round_p < R -> ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V))
-        invariant ~_has_started -> step = step_t.propose & ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V)) & round_p = 0
+            invariant (step = step_t.prevote | step = step_t.propose) -> ~abstract_protocol.precommitted(n,round_p,V)
+            invariant step = step_t.propose -> ~abstract_protocol.prevoted(n,round_p,V)
+            invariant step = step_t.prevote -> exists V . abstract_protocol.prevoted(n,round_p,V)
 
-        invariant decision ~= value.nil -> exists R . abstract_protocol.decided(n,R,decision)
+            invariant round_p < R -> ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V))
+            invariant ~_has_started -> step = step_t.propose & ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V)) & round_p = 0
+
+            invariant decision ~= value.nil -> exists R . abstract_protocol.decided(n,R,decision)
+        }
     }
 }

ivy-proofs/tendermint_test.ivy

@@ -0,0 +1,127 @@
+#lang ivy1.7
+
+include tendermint
+include abstract_tendermint
+
+isolate ghost_ = {
+    instantiate abstract_tendermint
+}
+
+isolate protocol = {
+    instantiate tendermint(ghost_) # here we instantiate the parameter of the tendermint module with `ghost_`; however note that we don't extract any code for `ghost_` (it's not in the list of object in the extract, and it's thus sliced away).
+    implementation {
+        definition init_val(n:node) = <<< `n`%2 >>>
+    }
+    # attribute test = impl
+} with ghost_, shim, value, round, proposers
+
+# Here we run a simple scenario that exhibits an execution in which nodes make
+# a decision. We do this to rule out trivial modeling errors.
+
+# One option to check that this scenario is valid is to run it in Ivy's REPL.
+# For this, first compile the scenario:
+#```ivyc target=repl isolate=code trace=true tendermint_test.ivy
+# Then, run the produced binary (e.g. for 4 nodes):
+#``` ./tendermint_test 4
+# Finally, call the action:
+#``` scenarios.scenario_1
+# Note that Ivy will check at runtime that all action preconditions are
+# satisfied. For example, runing the scenario twice will cause a violation of
+# the precondition of the `start` action, because a node cannot start twice
+# (see `require ~_has_started` in action `start`).
+
+# Another possibility would be to run `ivy_check` on the scenario, but that
+# does not seem to work at the moment.
+
+isolate scenarios = {
+    individual all:nset # will be used as parameter to actions requiring a quorum
+
+    after init {
+        var iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            all := all.insert(iter.val);
+            iter := iter.next;
+        };
+        assert nset.is_quorum(all); # we can also use asserts to make sure we are getting what we expect
+    }
+
+    export action scenario_1 = {
+        # all nodes start:
+        var iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            call protocol.server.start(iter.val);
+            iter := iter.next;
+        };
+        # all nodes receive the leader's proposal:
+        var m:msg;
+        m.m_kind := msg_kind.proposal;
+        m.m_src := 0;
+        m.m_round := 0;
+        m.m_value := 0;
+        m.m_vround := round.minus_one;
+        iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            call net.recv(iter.val,m);
+            iter := iter.next;
+        };
+        # all nodes prevote:
+        iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            call protocol.server.l_22(iter.val,0);
+            iter := iter.next;
+        };
+        # all nodes receive each other's prevote messages;
+        m.m_kind := msg_kind.prevote;
+        m.m_vround := 0;
+        iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            var iter2 := node.iter.create(0); # the sender
+            while ~iter2.is_end
+            {
+                m.m_src := iter2.val;
+                call net.recv(iter.val,m);
+                iter2 := iter2.next;
+            };
+            iter := iter.next;
+        };
+        # all nodes precommit:
+        iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            call protocol.server.l_36(iter.val,0,0,all);
+            iter := iter.next;
+        };
+        # all nodes receive each other's pre-commits
+        m.m_kind := msg_kind.precommit;
+        iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            var iter2 := node.iter.create(0); # the sender
+            while ~iter2.is_end
+            {
+                m.m_src := iter2.val;
+                call net.recv(iter.val,m);
+                iter2 := iter2.next;
+            };
+            iter := iter.next;
+        };
+        # now all nodes can decide:
+        iter := node.iter.create(0);
+        while ~iter.is_end
+        {
+            call protocol.server.l_49_decide(iter.val,0,0,all);
+            iter := iter.next;
+        };
+    }
+
+    # TODO: add more scenarios
+
+} with round, node, proposers, value, nset, protocol, shim, net
+
+# extract code = protocol, shim, round, node
+extract code = round, node, proposers, value, nset, protocol, shim, net, scenarios