From 290d6b684f9cb446904708bc4881a024785e53d4 Mon Sep 17 00:00:00 2001
From: Josef Widder <josef@informal.systems>
Date: Mon, 4 Dec 2023 12:58:53 +0100
Subject: [PATCH] added English explanation to runs

---
 Specs/Quint/line28run.qnt | 24 ++++++++++++++++++++++--
 Specs/Quint/line42run.qnt | 13 +++++++++++++
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/Specs/Quint/line28run.qnt b/Specs/Quint/line28run.qnt
index 1f8cf7374..637322eb3 100644
--- a/Specs/Quint/line28run.qnt
+++ b/Specs/Quint/line28run.qnt
@@ -8,9 +8,25 @@ export TendermintDSL.*
 const otherSet : Set[Address_t]
 val others = otherSet.fold(List(), (s, x) => s.append(x)) 
 
+/*
+- there need to be faulty processes
+- there are other processes that together with the faulty ones are 2f+1
+- the others include the proposer.
+- the others are successful until sending precommit value
+    - they set locked value and valid value
+- then faulty precommit nil are delivered to correct processes
+- the precommits from others are delivered to correct processes so that timeoutprecommit is started
+- correct processes go to the next round
+- there the proposer
+    - uses the valid value stored to send proposal for valid value
+    - correct processes take this to execute line 28 and prevote for this value
+*/
+
 run runToLine28 = {
     val nextProposer = Proposer (validatorSet, 0, 1)
     init
+
+    // proposer sends proposal and correct processes receive -> send prevote value
     .then(all {
         // others should be at most 2/3.
         // if this assertion fails the set need to be set differently
@@ -18,17 +34,21 @@ run runToLine28 = {
         assert(3 * size(otherSet.union(Faulty)) > 2 * size(validators)),  
         everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "blue")
     })
-    // receive all prevotes    
+    // correct processes receive prevotes from correct processes -> send precommit    
     .then(fromPrevoteToPrecommit (correctList, correctList, validatorList, validatorSet, 0, 0, "blue"))
+    // TODO assertion: valid and locked is set.
     // now the faulty nodes precommit nil
     .then(ListDeliverAllVotes("Precommit", faultyList, correctList, validatorSet, 0, 0, "nil"))
+    // correct processes receive faulty precommit nil
     .then(faultyList.length().reps(_ => ListTakeAStep(correctList)))   
-    // now the other precommits are delivered, so that timeoutPrecommit is started
+    // now the precommits from some correct processes are delivered, 
+    // "other" processes are just enough so that timeoutPrecommit is started
     .then(ListDeliverAllVotes("Precommit", others, correctList, validatorSet, 0, 0, "blue"))
     .then(others.length().reps(_ => ListTakeAStep(correctList)))
     // TimeoutPrecommit is there an can fire and bring is to the next round.
     .then(all{
         assert(system.get(nextProposer).timeout.contains(("TimeoutPrecommit", 0, 0))),
+    // proposer sends proposal and correct processes receive -> send prevote value on line 28   
         everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "red")
     })
     .then(all{
diff --git a/Specs/Quint/line42run.qnt b/Specs/Quint/line42run.qnt
index 5da4398fd..18fbc8e64 100644
--- a/Specs/Quint/line42run.qnt
+++ b/Specs/Quint/line42run.qnt
@@ -9,11 +9,24 @@ const testedVal : Address_t
 val others = validators.exclude(Set(testedVal)) 
 val othersList = others.fold(List(), (s, x) => s.append(x))
 
+/*
+- there is a special validator testedVal and all the others
+- the others include the proposer.
+- the others are successful until sending precommit value, while testedVal doesn't do anything
+- testedVal 
+    - hits TimeoutPropose 
+    - then receives prevote from others to hitTimeoutPrevote to enter step precommit
+    - the receives the proposal
+    - then it should update valid value but not locked value 
+*/
+
 run runToLine42 = {
     val value = "blue"
     init
     .then(valStep(testedVal))
+    // proposer sends proposal and correct processes receive -> send prevote value
     .then(everyoneReceivesProposal(othersList, validatorList, validatorSet, 0, 0, value))
+    // Everyone except the tested validators sends precommit
     .then(fromPrevoteToPrecommit(othersList, othersList, validatorList, validatorSet, 0, 0, value))
     // At this point we have set up the environment for "testedVal" to reach line 42 without
     // any other process taking any steps