TLA+: Forking cases for tendermint (#496)

* specification in TLA+ and model checking with Apalache

Co-authored-by: istoilkovska <[email protected]>

docs/spec/tendermint-fork-cases/001indinv-apalache.csv

@@ -0,0 +1,31 @@
+no,filename,tool,timeout,init,inv,next,args
+1,MC_n4_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+2,MC_n4_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+3,MC_n4_f3.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+4,MC_n5_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+5,MC_n5_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+6,MC_n7_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+7,MC_n7_f3.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+8,MC_n7_f4.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+9,MC_n10_f3.tla,apalache,24h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+10,MC_n10_f4.tla,apalache,24h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+11,MC_n4_f1.tla,apalache,10h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
+12,MC_n4_f2.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
+13,MC_n4_f3.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
+14,MC_n5_f1.tla,apalache,10h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
+15,MC_n5_f2.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
+16,MC_n7_f2.tla,apalache,10h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
+17,MC_n7_f3.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
+18,MC_n7_f4.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
+19,MC_n10_f3.tla,apalache,24h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
+20,MC_n10_f4.tla,apalache,24h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
+21,MC_n4_f1.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+22,MC_n4_f2.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+23,MC_n4_f3.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+24,MC_n5_f1.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+25,MC_n5_f2.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+26,MC_n7_f2.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+27,MC_n7_f3.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+28,MC_n7_f4.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
+29,MC_n10_f3.tla,apalache,24h,Init,TypedInv,,--length=0 --cinit=ConstInit
+30,MC_n10_f4.tla,apalache,24h,Init,TypedInv,,--length=0 --cinit=ConstInit

docs/spec/tendermint-fork-cases/001indinv-apalache.ini

@@ -0,0 +1,8 @@
+# a configuration file for apalache-tests/scripts/mk-run.py
+
+[apalache-unstable]
+more_args=
+
+[apalache-card]
+more_args=
+

docs/spec/tendermint-fork-cases/MC_n10_f3.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n10_f3 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3", "c4", "c5", "c6", "c7"},
+  Defective <- {} <: {STRING},
+  Byzantine <- {"f8", "f9", "f10"},
+  N <- 10,
+  T <- 3,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n10_f4.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n10_f4 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3", "c4", "c5", "c6"},
+  Defective <- {"f7"},
+  Byzantine <- {"f8", "f9", "f10"},
+  N <- 10,
+  T <- 3,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n4_f1.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n4_f1 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3"},
+  Defective <- {} <: {STRING},
+  Byzantine <- {"f1"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n4_f2.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n4_f2 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2"},
+  Defective <- {"f3"},
+  Byzantine <- {"f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n4_f3.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n4_f3 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1"},
+  Defective <- {"a2", "a3"},
+  Byzantine <- {"f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n5_f1.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n5_f1 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3", "c4"},
+  Defective <- {} <: {STRING},
+  Byzantine <- {"f5"},
+  N <- 5,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n5_f2.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n5_f2 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3"},
+  Defective <- {"a4"},
+  Byzantine <- {"f5"},
+  N <- 5,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n7_f2.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n7_f2 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3", "c4", "c5"},
+  Defective <- {} <: {STRING},
+  Byzantine <- {"f6", "f7"},
+  N <- 7,
+  T <- 2,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n7_f3.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n7_f3 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3", "c4"},
+  Defective <- {"f5"},
+  Byzantine <- {"f6", "f7"},
+  N <- 7,
+  T <- 2,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

docs/spec/tendermint-fork-cases/MC_n7_f4.tla

@@ -0,0 +1,26 @@
+----------------------------- MODULE MC_n7_f4 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence
+
+\* an operator for type annotations
+a <: b == a
+
+INSTANCE TendermintAccDebug3 WITH
+  Corr <- {"c1", "c2", "c3"},
+  Defective <- {"f4", "f5"},
+  Byzantine <- {"f6", "f7"},
+  N <- 7,
+  T <- 2,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================