Computing attack types (#232)

Add light attack evidence handling
4 years ago · 42751ea4f3
--- a/rust-spec/lightclient/README.md
+++ b/rust-spec/lightclient/README.md
@ -10,12 +10,15 @@ with a trusted header and validator set. The light client
 protocol allows a client to then securely update its trusted state by requesting and
 verifying a minimal set of data from a network of full nodes (at least one of which is correct).

 The light client is decomposed into three components:
 The light client is decomposed into two main components:

 - Commit Verification - verify signed headers and associated validator
 - [Commit Verification](#Commit-Verification) - verify signed headers and associated validator
  set changes from a single full node, called primary
 - Fork Detection -  verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of forks)
 - Fork Accountability - given a fork, which validators are responsible for it.
 - [Attack Detection](#Attack-Detection) -  verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of a lightclient attack)

 In case a lightclient attack is detected, the lightclient submits evidence to a full node which is responsible for "accountability", that is, punishing attackers:

 - [Accountability](#Accountability) - given evidence for an attack, compute a set of validators that are responsible for it.

 ## Commit Verification

@ -175,10 +178,23 @@ All lines in `results.csv` should report `Error`.

 The detailed experimental results are to be added soon.

 ## Fork Accountability
 ## Accountability


 The [English specification](attacks/isolate-attackers_002_reviewed.md) 
 defines the protocol that is executed on a full node upon receiving attack [evidence](detection/detection_003_reviewed.md#tmbc-lc-evidence-data1) from a lightclient. In particular, the protocol handles three types of attacks
 - lunatic
 - equivocation
 - amnesia

 As is discussed in the [last part](attacks/isolate-attackers_002_reviewed.md#Part-III---Completeness) of the English specification, computer-aided analysis of  [Tendermint Consensus in TLA+][tendermint-accountability] shows that these three types capture all possible attacks.


 The [TLA+ specification](attacks/Isolation_001_draft.tla)
 is a formal description of the
 protocol, including the safety property, which can be model checked with Apalache.

 There is no English specification yet. TODO: Jovan's work?
 Similar to the other specifications, [MC_5_3.tla](attacks/MC_5_3.tla) contains concrete parameters to run the model checker. The specification can be checked within seconds.

 TODO: there is a WIP [TLA+
 specification](https://github.com/informalsystems/verification/pull/13) in the
 verification repo that should be moved over here.
 [tendermint-accountability]:
 https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md
--- a/rust-spec/lightclient/attacks/isolate-attackers_002_reviewed.md
+++ b/rust-spec/lightclient/attacks/isolate-attackers_002_reviewed.md
@ -0,0 +1,221 @@
 # Lightclient Attackers Isolation

 Adversarial nodes may have the incentive to lie to a lightclient about the state of a Tendermint blockchain. An attempt to do so is called attack. Light client [verification][verification] checks incoming data by checking a so-called "commit", which is a forwarded set of signed messages that is (supposedly) produced during executing Tendermint consensus. Thus, an attack boils down to creating and signing Tendermint consensus messages in deviation from the Tendermint consensus algorithm rules.

 As Tendermint consensus and light client verification is safe under the assumption of more than 2/3 of correct voting power per block [[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link], this implies that if there was an attack then [[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link] was violated, that is, there is a block such that 
 - validators deviated from the protocol, and 
 - these validators represent more than 1/3 of the voting power in that block.

 In the case of an [attack][node-based-attack-characterization], the lightclient [attack detection mechanism][detection] computes data, so called evidence [[LC-DATA-EVIDENCE.1]][LC-DATA-EVIDENCE-link], that can be used 
 - to proof that there has been attack [[TMBC-LC-EVIDENCE-DATA.1]][TMBC-LC-EVIDENCE-DATA-link] and 
 -  as basis to find the actual nodes that deviated from the Tendermint protocol. 




 This specification considers how a full node in a Tendermint blockchain can isolate a set of attackers that launched the attack. The set should satisfy
 - the set does not contain a correct validator
 - the set contains validators that represent more than 1/3 of the voting power of a block that is still within the unbonding period


 # Outline

 After providing the [problem statement](#Part-I---Basics-and-Definition-of-the-Problem), we specify the [isolator function](#Part-II---Protocol) and close with the discussion about its [correctness](#Part-III---Completeness) which is based on computer-aided analysis of Tendermint Consensus.

 # Part I - Basics and Definition of the Problem

 For definitions of data structures used here, in particular LightBlocks [[LCV-DATA-LIGHTBLOCK.1]](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-data-lightblock1), we refer to the specification of [Light Client Verification][verification].


 The specification of the [detection mechanism][detection] describes 
 - what is a light client attack,
 - conditions under which the detector will detect a light client attack,
 - and the format of the output data, called evidence, in the case an attack is detected. The format is defined in
 [[LC-DATA-EVIDENCE.1]][LC-DATA-EVIDENCE-link] and looks as follows

 ```go
 type LightClientAttackEvidence struct {
    ConflictingBlock   LightBlock
    CommonHeight       int64
 }
 ```

 The isolator is a function that gets as input evidence `ev`
 and a prefix of the blockchain `bc` at least up to height `ev.ConflictingBlock.Header.Height + 1`. The output is a set of *peerIDs* of validators.

 We assume that the full node is synchronized with the blockchain and has reached the height `ev.ConflictingBlock.Header.Height + 1`.


 #### **[LCAI-INV-Output.1]**
 When an output is generated it satisfies the following properties: 
 - If
    - `bc[CommonHeight].bfttime` is within the unbonding period w.r.t. the time at the full node, 
    - `ev.ConflictingBlock.Header != bc[ev.ConflictingBlock.Header.Height]`
    - Validators in `ev.ConflictingBlock.Commit` represent more than 1/3 of the voting power in `bc[ev.CommonHeight].NextValidators`
 - Then: The output is a set of validators in `bc[CommonHeight].NextValidators` that
    - represent more than 1/3 of the voting power in `bc[ev.commonHeight].NextValidators`
    - signed Tendermint consensus messages for height `ev.ConflictingBlock.Header.Height` by violating the Tendermint consensus protocol.
 - Else: the empty set.


 # Part II - Protocol

 Here we discuss how to solve the problem of isolating misbehaving processes. We describe the function `isolateMisbehavingProcesses` as well as all the helping functions below. In [Part III](#part-III---Completeness), we discuss why the solution is complete based on result from analysis with automated tools.

 ## Isolation

 ### Outline

 We first check whether the conflicting block can indeed be verified from the common height. We then first check whether it was a lunatic attack (violating validity). If this is not the case, we check for equivocation. If this also is not the case, we start the on-chain [accountability protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).

 #### **[LCAI-FUNC-MAIN.1]**
 ```go
 func isolateMisbehavingProcesses(ev LightClientAttackEvidence, bc Blockchain) []ValidatorAddress {
    
    reference := bc[ev.conflictingBlock.Header.Height].Header
    ev_header := ev.conflictingBlock.Header

    ref_commit := bc[ev.conflictingBlock.Header.Height + 1].Header.LastCommit // + 1 !!
    ev_commit := ev.conflictingBlock.Commit

    if violatesTMValidity(reference, ev_header) {
        // lunatic light client attack
        signatories := Signers(ev.ConflictingBlock.Commit)
        bonded_vals := Addresses(bc[ev.CommonHeight].NextValidators)
        return intersection(signatories,bonded_vals)

    } 
    // If this point is reached the validator sets in reference and ev_header are identical
    else if RoundOf(ref_commit) == RoundOf(ev_commit) {
        // equivocation light client attack
        return intersection(Signers(ref_commit), Signers(ev_commit))
    } 
    else {
        // amnesia light client attack 
        return IsolateAmnesiaAttacker(ev, bc)
    } 
 }
 ```
 - Implementation comment
    - If the full node has only reached height `ev.conflictingBlock.Header.Height` then `bc[ev.conflictingBlock.Header.Height + 1].Header.LastCommit` refers to the locally stored commit for this height. (This commit must be present by the precondition on `length(bc)`.)
    - We check in the precondition that the unbonding period is not expired. However, since time moves on, before handing the validators over Cosmos SDK, the time needs to be checked again to satisfy the contract which requires that only bonded validators are reported. This passing of validators to the SDK is out of scope of this specification.
 - Expected precondition
    - `length(bc) >= ev.conflictingBlock.Header.Height`
    - `ValidAndVerifiedUnbonding(bc[ev.CommonHeight], ev.ConflictingBlock) == SUCCESS`
    - `ev.ConflictingBlock.Header != bc[ev.ConflictingBlock.Header.Height]`
    - `ev.conflictingBlock` satisfies basic validation (in particular all signed messages in the Commit are from the same round)
 - Expected postcondition
    - [[FN-INV-Output.1]](#FN-INV-Output1) holds
 - Error condition 
    - returns an error if precondition is violated.


 ### Details of the Functions

 #### **[LCAI-FUNC-VVU.1]**
 ```go
 func ValidAndVerifiedUnbonding(trusted LightBlock, untrusted LightBlock) Result
 ```
 - Conditions are identical to [[LCV-FUNC-VALID.2]][LCV-FUNC-VALID.link] except the precondition "*trusted.Header.Time > now - trustingPeriod*" is substituted with
    - `trusted.Header.Time > now - UnbondingPeriod`

 #### **[LCAI-FUNC-NONVALID.1]**
 ```go
 func violatesTMValidity(ref Header, ev Header) boolean
 ```
 - Implementation remarks
    - checks whether the evidence header `ev` violates the validity property of Tendermint Consensus, by checking against a reference header
 - Expected precondition
    - `ref.Height == ev.Height`    
 - Expected postcondition
    - returns evaluation of the following disjunction  
    **[LCAI-NONVALID-OUTPUT.1]** ==  
    `ref.ValidatorsHash != ev.ValidatorsHash` or  
    `ref.NextValidatorsHash != ev.NextValidatorsHash` or  
    `ref.ConsensusHash != ev.ConsensusHash` or  
    `ref.AppHash != ev.AppHash` or  
    `ref.LastResultsHash != ev.LastResultsHash`


 ```go
 func IsolateAmnesiaAttacker(ev LightClientAttackEvidence, bc Blockchain) []ValidatorAddress 
 ```
 - Implementation remarks
    - This triggers the [query/response protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).
 - Expected postcondition
    - returns attackers according to [LCAI-INV-Output.1].

 ```go
 func RoundOf(commit Commit) []ValidatorAddress 
 ```
 - Expected precondition
    - `commit` is well-formed. In particular all votes are from the same round `r`.
 - Expected postcondition
    - returns round `r` that is encoded in all the votes of the commit
 - Error condition
    - reports error if precondition is violated

 ```go
 func Signers(commit Commit) []ValidatorAddress 
 ```
 - Expected postcondition
    - returns all validator addresses in `commit`

 ```go
 func Addresses(vals Validator[]) ValidatorAddress[]
 ```
 - Expected postcondition
    - returns all validator addresses in `vals`



 # Part III - Completeness

 As discussed in the beginning of this document, an attack boils down to creating and signing Tendermint consensus messages in deviation from the Tendermint consensus algorithm rules.
 The main function `isolateMisbehavingProcesses` distinguishes three kinds of wrongly signed messages, namely,
 - lunatic: signing invalid blocks
 - equivocation: double-signing valid blocks in the same consensus round 
 - amnesia: signing conflicting blocks in different consensus rounds, without having seen a quorum of messages that would have allowed to do so.

 The question is whether this captures all attacks. 
 First observe that the first check in `isolateMisbehavingProcesses` is `violatesTMValidity`. It takes care of lunatic attacks. If this check passes, that is, if `violatesTMValidity` returns `FALSE` this means that [[LCAI-NONVALID-OUTPUT.1]](#LCAI-FUNC-NONVALID1]) evaluates to false, which implies that `ref.ValidatorsHash = ev.ValidatorsHash`. Hence, after `violatesTMValidity`, all the involved validators are the ones from the blockchain. It is thus sufficient to analyze one instance of Tendermint consensus with a fixed group membership (set of validators). Also, as we have two different blocks for the same height, it is sufficient to consider two different valid consensus values, that is, binary consensus.

 For this fixed group membership, we have analyzed the attacks using the TLA+ specification of [Tendermint Consensus in TLA+][tendermint-accountability]. We checked that indeed the only possible scenarios that can lead to violation of agreement are **equivocation** and **amnesia**. An independent study by Galois of the protocol based on [Ivy proofs](https://github.com/tendermint/spec/tree/master/ivy-proofs) led to the same conclusion.




 # References

 [[supervisor]] The specification of the light client supervisor.

 [[verification]] The specification of the light client verification protocol.

 [[detection]] The specification of the light client attack detection mechanism.

 [[tendermint-accountability]]: TLA+ specification to check the types of attacks

 [tendermint-accountability]:
 https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md

 [supervisor]: 
 https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor_001_draft.md

 [verification]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md

 [detection]: 
 https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md


 [LC-DATA-EVIDENCE-link]: 
 https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#lc-data-evidence1

 [TMBC-LC-EVIDENCE-DATA-link]:
 https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#tmbc-lc-evidence-data1

 [node-based-attack-characterization]:
 https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#node-based-characterization-of-attacks

 [TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#tmbc-fm-2thirds1

 [LCV-FUNC-VALID.link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-func-valid2
--- a/rust-spec/lightclient/attacks/notes-on-evidence-handling.md
+++ b/rust-spec/lightclient/attacks/notes-on-evidence-handling.md
--- a/rust-spec/tendermint-accountability/001indinv-apalache.csv
+++ b/rust-spec/tendermint-accountability/001indinv-apalache.csv
@ -0,0 +1,13 @@
 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_n5_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
 4,MC_n5_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
 5,MC_n4_f1.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
 6,MC_n4_f2.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
 7,MC_n5_f1.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
 8,MC_n5_f2.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
 9,MC_n4_f1.tla,apalache,20h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
 10,MC_n4_f2.tla,apalache,20h,TypedInv,Accountability,,--length=0 --cinit=ConstInit
 11,MC_n5_f1.tla,apalache,20h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
 12,MC_n5_f2.tla,apalache,20h,TypedInv,Accountability,,--length=0 --cinit=ConstInit
--- a/rust-spec/tendermint-accountability/MC_n4_f1.tla
+++ b/rust-spec/tendermint-accountability/MC_n4_f1.tla
@ -0,0 +1,22 @@
 ----------------------------- 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, action 

 INSTANCE TendermintAccDebug_004_draft WITH
  Corr <- {"c1", "c2", "c3"},
  Faulty <- {"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]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/MC_n4_f2.tla
+++ b/rust-spec/tendermint-accountability/MC_n4_f2.tla
@ -0,0 +1,22 @@
 ----------------------------- 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, action

 INSTANCE TendermintAccDebug_004_draft WITH
  Corr <- {"c1", "c2"},
  Faulty <- {"f3", "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]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/MC_n4_f2_amnesia.tla
+++ b/rust-spec/tendermint-accountability/MC_n4_f2_amnesia.tla
@ -0,0 +1,40 @@
 ---------------------- MODULE MC_n4_f2_amnesia -------------------------------
 EXTENDS Sequences

 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, action

 \* the variable declared in TendermintAccTrace3
 VARIABLE
  toReplay

 \* old apalache annotations, fix with the new release
 a <: b == a  

 INSTANCE TendermintAccTrace_004_draft WITH
  Corr <- {"c1", "c2"},
  Faulty <- {"f3", "f4"},
  N <- 4,
  T <- 1,
  ValidValues <- { "v0", "v1" },
  InvalidValues <- {"v2"},
  MaxRound <- 2,
  Trace <- <<
    "UponProposalInPropose",
    "UponProposalInPrevoteOrCommitAndPrevote",
    "UponProposalInPrecommitNoDecision",
    "OnRoundCatchup", 
    "UponProposalInPropose",
    "UponProposalInPrevoteOrCommitAndPrevote",
    "UponProposalInPrecommitNoDecision"
  >> <: Seq(STRING)

 \* run Apalache with --cinit=ConstInit
 ConstInit == \* the proposer is arbitrary -- works for safety
  Proposer \in [Rounds -> AllProcs]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/MC_n4_f3.tla
+++ b/rust-spec/tendermint-accountability/MC_n4_f3.tla
@ -0,0 +1,22 @@
 ----------------------------- 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, action

 INSTANCE TendermintAccDebug_004_draft WITH
  Corr <- {"c1"},
  Faulty <- {"f2", "f3", "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]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/MC_n5_f1.tla
+++ b/rust-spec/tendermint-accountability/MC_n5_f1.tla
@ -0,0 +1,22 @@
 ----------------------------- 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, action

 INSTANCE TendermintAccDebug_004_draft WITH
  Corr <- {"c1", "c2", "c3", "c4"},
  Faulty <- {"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]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/MC_n5_f2.tla
+++ b/rust-spec/tendermint-accountability/MC_n5_f2.tla
@ -0,0 +1,22 @@
 ----------------------------- 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, action

 INSTANCE TendermintAccDebug_004_draft WITH
  Corr <- {"c1", "c2", "c3"},
  Faulty <- {"f4", "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]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/MC_n6_f1.tla
+++ b/rust-spec/tendermint-accountability/MC_n6_f1.tla
@ -0,0 +1,22 @@
 ----------------------------- MODULE MC_n6_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, action 

 INSTANCE TendermintAccDebug_004_draft WITH
  Corr <- {"c1", "c2", "c3", "c4", "c5"},
  Faulty <- {"f6"},
  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]

 =============================================================================    
--- a/rust-spec/tendermint-accountability/README.md
+++ b/rust-spec/tendermint-accountability/README.md
@ -0,0 +1,106 @@
 # Synopsis
 
 A TLA+ specification of a simplified Tendermint consensus, tuned for
 fork accountability. The simplifications are as follows:

 - the procotol runs for one height, that is, one-shot consensus

 - this specification focuses on safety, so timeouts are modelled with
   with non-determinism

 - the proposer function is non-determinstic, no fairness is assumed

 - the messages by the faulty processes are injected right in the initial states

 - every process has the voting power of 1

 - hashes are modelled as identity

 Having the above assumptions in mind, the specification follows the pseudo-code
 of the Tendermint paper: https://arxiv.org/abs/1807.04938

 Byzantine processes can demonstrate arbitrary behavior, including
 no communication. However, we have to show that under the collective evidence
 collected by the correct processes, at least `f+1` Byzantine processes demonstrate
 one of the following behaviors:

   - Equivocation: a Byzantine process sends two different values
     in the same round.

   - Amnesia: a Byzantine process locks a value, although it has locked
     another value in the past.

 # TLA+ modules
 
 - [TendermintAcc_004_draft](TendermintAcc_004_draft.tla) is the protocol
   specification,

 - [TendermintAccInv_004_draft](TendermintAccInv_004_draft.tla) contains an
   inductive invariant for establishing the protocol safety as well as the
   forking cases,

 - `MC_n<n>_f<f>`, e.g., [MC_n4_f1](MC_n4_f1.tla), contains fixed constants for
   model checking with the [Apalache model
   checker](https://github.com/informalsystems/apalache),

 - [TendermintAccTrace_004_draft](TendermintAccTrace_004_draft.tla) shows how
   to restrict the execution space to a fixed sequence of actions (e.g., to
   instantiate a counterexample),

 - [TendermintAccDebug_004_draft](TendermintAccDebug_004_draft.tla) contains
   the useful definitions for debugging the protocol specification with TLC and
   Apalache.

 # Reasoning about fork scenarios

 The theorem statements can be found in
 [TendermintAccInv_004_draft.tla](TendermintAccInv_004_draft.tla).

 First, we would like to show that `TypedInv` is an inductive invariant.
 Formally, the statement looks as follows:

 ```tla
 THEOREM TypedInvIsInductive ==
    \/ FaultyQuorum
    \//\ Init => TypedInv
      /\ TypedInv /\ [Next]_vars => TypedInv'
 ```

 When over two-thirds of processes are faulty, `TypedInv` is not inductive.
 However, there is no hope to repair the protocol in this case. We run
 [Apalache](https://github.com/informalsystems/apalache) to prove this theorem
 only for fixed instances of 4 to 5 validators.  Apalache does not parse theorem
 statements at the moment, so we ran Apalache using a shell script. To find a
 parameterized argument, one has to use a theorem prover, e.g., TLAPS.

 Second, we would like to show that the invariant implies `Agreement`, that is,
 no fork, provided that less than one third of processes is faulty. By combining
 this theorem with the previous theorem, we conclude that the protocol indeed
 satisfies Agreement under the condition `LessThanThirdFaulty`.

 ```tla
 THEOREM AgreementWhenLessThanThirdFaulty ==
    LessThanThirdFaulty /\ TypedInv => Agreement
 ```

 Third, in the general case, we either have no fork, or two fork scenarios:

 ```tla
 THEOREM AgreementOrFork ==
    ~FaultyQuorum /\ TypedInv => Accountability
 ```

 # Model checking results   

 Check the report on [model checking with Apalache](./results/001indinv-apalache-report.md).

 To run the model checking experiments, use the script:

 ```console
 ./run.sh
 ```

 This script assumes that the apalache build is available in
 `~/devl/apalache-unstable`.


--- a/rust-spec/tendermint-accountability/TendermintAccDebug_004_draft.tla
+++ b/rust-spec/tendermint-accountability/TendermintAccDebug_004_draft.tla
@ -0,0 +1,100 @@
 ------------------ MODULE TendermintAccDebug_004_draft -------------------------
 (*
 A few definitions that we use for debugging TendermintAcc3, which do not belong
 to the specification itself.
 
 * Version 3. Modular and parameterized definitions.

 Igor Konnov, 2020.
 *)

 EXTENDS TendermintAccInv_004_draft

 \* make them parameters?
 NFaultyProposals == 0   \* the number of injected faulty PROPOSE messages
 NFaultyPrevotes == 6    \* the number of injected faulty PREVOTE messages
 NFaultyPrecommits == 6  \* the number of injected faulty PRECOMMIT messages

 \* Given a set of allowed messages Msgs, this operator produces a function from
 \* rounds to sets of messages.
 \* Importantly, there will be exactly k messages in the image of msgFun.
 \* We use this action to produce k faults in an initial state.
 ProduceFaults(msgFun, From, k) ==
    \E f \in [1..k -> From]:
        msgFun = [r \in Rounds |-> {m \in {f[i]: i \in 1..k}: m.round = r}]

 \* As TLC explodes with faults, we may have initial states without faults    
 InitNoFaults ==
    /\ round = [p \in Corr |-> 0]
    /\ step = [p \in Corr |-> "PROPOSE"]
    /\ decision = [p \in Corr |-> NilValue]
    /\ lockedValue = [p \in Corr |-> NilValue]
    /\ lockedRound = [p \in Corr |-> NilRound]
    /\ validValue = [p \in Corr |-> NilValue]
    /\ validRound = [p \in Corr |-> NilRound]
    /\ msgsPropose = [r \in Rounds |-> EmptyMsgSet]
    /\ msgsPrevote = [r \in Rounds |-> EmptyMsgSet]
    /\ msgsPrecommit = [r \in Rounds |-> EmptyMsgSet]
    /\ evidence = EmptyMsgSet

 (*
 A specialized version of Init that injects NFaultyProposals proposals,
 NFaultyPrevotes prevotes, NFaultyPrecommits precommits by the faulty processes
 *)
 InitFewFaults ==
    /\ round = [p \in Corr |-> 0]
    /\ step = [p \in Corr |-> "PROPOSE"]
    /\ decision = [p \in Corr |-> NilValue]
    /\ lockedValue = [p \in Corr |-> NilValue]
    /\ lockedRound = [p \in Corr |-> NilRound]
    /\ validValue = [p \in Corr |-> NilValue]
    /\ validRound = [p \in Corr |-> NilRound]
    /\ ProduceFaults(msgsPrevote',
                     SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: Rounds, id: Values]),
                     NFaultyPrevotes)
    /\ ProduceFaults(msgsPrecommit',
                     SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: Rounds, id: Values]),
                     NFaultyPrecommits)
    /\ ProduceFaults(msgsPropose',
                     SetOfMsgs([type: {"PROPOSAL"}, src: Faulty, round: Rounds,
                                proposal: Values, validRound: Rounds \cup {NilRound}]),
                     NFaultyProposals)
    /\ evidence = EmptyMsgSet

 \* Add faults incrementally
 NextWithFaults ==
    \* either the protocol makes a step
    \/ Next
    \* or a faulty process sends a message
    \//\ UNCHANGED <<round, step, decision, lockedValue,
                     lockedRound, validValue, validRound, evidence>>
      /\ \E p \in Faulty:
         \E r \in Rounds:
           \//\ UNCHANGED <<msgsPrevote, msgsPrecommit>>
             /\ \E proposal \in ValidValues \union {NilValue}:
                \E vr \in RoundsOrNil:
                  BroadcastProposal(p, r, proposal, vr)
           \//\ UNCHANGED <<msgsPropose, msgsPrecommit>>
             /\ \E id \in ValidValues \union {NilValue}:
                  BroadcastPrevote(p, r, id)
           \//\ UNCHANGED <<msgsPropose, msgsPrevote>>
             /\ \E id \in ValidValues \union {NilValue}:
                  BroadcastPrecommit(p, r, id)

 (******************************** PROPERTIES  ***************************************)
 \* simple reachability properties to see that the spec is progressing
 NoPrevote == \A p \in Corr: step[p] /= "PREVOTE" 

 NoPrecommit == \A p \in Corr: step[p] /= "PRECOMMIT"   

 NoValidPrecommit ==
    \A r \in Rounds:
      \A m \in msgsPrecommit[r]:
        m.id = NilValue \/ m.src \in Faulty

 NoHigherRounds == \A p \in Corr: round[p] < 1

 NoDecision == \A p \in Corr: decision[p] = NilValue                    

 =============================================================================    
 
--- a/rust-spec/tendermint-accountability/TendermintAccInv_004_draft.tla
+++ b/rust-spec/tendermint-accountability/TendermintAccInv_004_draft.tla
@ -0,0 +1,370 @@
 ------------------- MODULE TendermintAccInv_004_draft --------------------------
 (*
 An inductive invariant for TendermintAcc3, which capture the forked
 and non-forked cases.

 * Version 3. Modular and parameterized definitions.
 * Version 2. Bugfixes in the spec and an inductive invariant.

 Igor Konnov, 2020.
 *)

 EXTENDS TendermintAcc_004_draft
  
 (************************** TYPE INVARIANT ***********************************)
 (* first, we define the sets of all potential messages *)
 AllProposals == 
  SetOfMsgs([type: {"PROPOSAL"},
             src: AllProcs,
             round: Rounds,
             proposal: ValuesOrNil,
             validRound: RoundsOrNil])
  
 AllPrevotes ==
  SetOfMsgs([type: {"PREVOTE"},
             src: AllProcs,
             round: Rounds,
             id: ValuesOrNil])

 AllPrecommits ==
  SetOfMsgs([type: {"PRECOMMIT"},
             src: AllProcs,
             round: Rounds,
             id: ValuesOrNil])

 (* the standard type invariant -- importantly, it is inductive *)
 TypeOK ==
    /\ round \in [Corr -> Rounds]
    /\ step \in [Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }]
    /\ decision \in [Corr -> ValidValues \union {NilValue}]
    /\ lockedValue \in [Corr -> ValidValues \union {NilValue}]
    /\ lockedRound \in [Corr -> RoundsOrNil]
    /\ validValue \in [Corr -> ValidValues \union {NilValue}]
    /\ validRound \in [Corr -> RoundsOrNil]
    /\ msgsPropose \in [Rounds -> SUBSET AllProposals]
    /\ BenignRoundsInMessages(msgsPropose)
    /\ msgsPrevote \in [Rounds -> SUBSET AllPrevotes]
    /\ BenignRoundsInMessages(msgsPrevote)
    /\ msgsPrecommit \in [Rounds -> SUBSET AllPrecommits]
    /\ BenignRoundsInMessages(msgsPrecommit)
    /\ evidence \in SUBSET (AllProposals \union AllPrevotes \union AllPrecommits)
    /\ action \in {
        "Init",
        "InsertProposal",
        "UponProposalInPropose",
        "UponProposalInProposeAndPrevote",
        "UponQuorumOfPrevotesAny",
        "UponProposalInPrevoteOrCommitAndPrevote",
        "UponQuorumOfPrecommitsAny",
        "UponProposalInPrecommitNoDecision",
        "OnTimeoutPropose",
        "OnQuorumOfNilPrevotes",
        "OnRoundCatchup"
     }

 (************************** INDUCTIVE INVARIANT *******************************)
 EvidenceContainsMessages ==
    \* evidence contains only the messages from:
    \* msgsPropose, msgsPrevote, and msgsPrecommit
  \A m \in evidence:
    LET r == m.round
        t == m.type
    IN
    CASE t = "PROPOSAL" -> m \in msgsPropose[r]
      [] t = "PREVOTE" -> m \in msgsPrevote[r]
      [] OTHER -> m \in msgsPrecommit[r]

 NoFutureMessagesForLargerRounds(p) ==
  \* a correct process does not send messages for the future rounds
  \A r \in { rr \in Rounds: rr > round[p] }:
    /\ \A m \in msgsPropose[r]: m.src /= p
    /\ \A m \in msgsPrevote[r]: m.src /= p
    /\ \A m \in msgsPrecommit[r]: m.src /= p

 NoFutureMessagesForCurrentRound(p) ==
  \* a correct process does not send messages in the future
  LET r == round[p] IN
    /\ Proposer[r] = p \/ \A m \in msgsPropose[r]: m.src /= p
    /\ \/ step[p] \in {"PREVOTE", "PRECOMMIT", "DECIDED"}
      \/ \A m \in msgsPrevote[r]: m.src /= p
    /\ \/ step[p] \in {"PRECOMMIT", "DECIDED"}
      \/ \A m \in msgsPrecommit[r]: m.src /= p
          
 \* the correct processes never send future messages
 AllNoFutureMessagesSent ==
  \A p \in Corr:
    /\ NoFutureMessagesForCurrentRound(p)                 
    /\ NoFutureMessagesForLargerRounds(p)

 \* a correct process in the PREVOTE state has sent a PREVOTE message
 IfInPrevoteThenSentPrevote(p) ==
  step[p] = "PREVOTE" =>
    \E m \in msgsPrevote[round[p]]:
      /\ m.id \in ValidValues \cup { NilValue }
      /\ m.src = p
      
 AllIfInPrevoteThenSentPrevote ==
  \A p \in Corr: IfInPrevoteThenSentPrevote(p)      

 \* a correct process in the PRECOMMIT state has sent a PRECOMMIT message
 IfInPrecommitThenSentPrecommit(p) ==
  step[p] = "PRECOMMIT" =>
    \E m \in msgsPrecommit[round[p]]:
      /\ m.id \in ValidValues \cup { NilValue }
      /\ m.src = p
      
 AllIfInPrecommitThenSentPrecommit ==
  \A p \in Corr: IfInPrecommitThenSentPrecommit(p)      

 \* a process in the PRECOMMIT state has sent a PRECOMMIT message
 IfInDecidedThenValidDecision(p) ==
  step[p] = "DECIDED" <=> decision[p] \in ValidValues
  
 AllIfInDecidedThenValidDecision ==
  \A p \in Corr: IfInDecidedThenValidDecision(p)  

 \* a decided process should have received a proposal on its decision
 IfInDecidedThenReceivedProposal(p) ==
  step[p] = "DECIDED" =>
    \E r \in Rounds: \* r is not necessarily round[p]
      /\ \E m \in msgsPropose[r] \intersect evidence:
          /\ m.src = Proposer[r]
          /\ m.proposal = decision[p]
          \* not inductive: /\ m.src \in Corr => (m.validRound <= r)
          
 AllIfInDecidedThenReceivedProposal ==
  \A p \in Corr:
    IfInDecidedThenReceivedProposal(p)          

 \* a decided process has received two-thirds of precommit messages
 IfInDecidedThenReceivedTwoThirds(p) ==
  step[p] = "DECIDED" =>
    \E r \in Rounds:
      LET PV ==
        { m \in msgsPrecommit[r] \intersect evidence: m.id = decision[p] }
      IN
      Cardinality(PV) >= THRESHOLD2
        
 AllIfInDecidedThenReceivedTwoThirds ==
  \A p \in Corr:
    IfInDecidedThenReceivedTwoThirds(p)        

 \* for a round r, there is proposal by the round proposer for a valid round vr
 ProposalInRound(r, proposedVal, vr) ==
  \E m \in msgsPropose[r]:
    /\ m.src = Proposer[r]
    /\ m.proposal = proposedVal
    /\ m.validRound = vr

 TwoThirdsPrevotes(vr, v) ==
  LET PV == { mm \in msgsPrevote[vr] \intersect evidence: mm.id = v } IN
  Cardinality(PV) >= THRESHOLD2

 \* if a process sends a PREVOTE, then there are three possibilities:
 \* 1) the process is faulty, 2) the PREVOTE cotains Nil,
 \* 3) there is a proposal in an earlier (valid) round and two thirds of PREVOTES
 IfSentPrevoteThenReceivedProposalOrTwoThirds(r) ==
  \A mpv \in msgsPrevote[r]:
    \/ mpv.src \in Faulty
      \* lockedRound and lockedValue is beyond my comprehension
    \/ mpv.id = NilValue
    \//\ mpv.src \in Corr
      /\ mpv.id /= NilValue
      /\ \/ ProposalInRound(r, mpv.id, NilRound)
         \/ \E vr \in { rr \in Rounds: rr < r }:
            /\ ProposalInRound(r, mpv.id, vr)
            /\ TwoThirdsPrevotes(vr, mpv.id)

 AllIfSentPrevoteThenReceivedProposalOrTwoThirds ==
  \A r \in Rounds:
    IfSentPrevoteThenReceivedProposalOrTwoThirds(r)

 \* if a correct process has sent a PRECOMMIT, then there are two thirds,
 \* either on a valid value, or a nil value
 IfSentPrecommitThenReceivedTwoThirds ==
  \A r \in Rounds:
    \A mpc \in msgsPrecommit[r]:
      mpc.src \in Corr =>
         \/ /\ mpc.id \in ValidValues
            /\ LET PV ==
                   { m \in msgsPrevote[r] \intersect evidence: m.id = mpc.id }
               IN
               Cardinality(PV) >= THRESHOLD2
         \/ /\ mpc.id = NilValue
            /\ Cardinality(msgsPrevote[r]) >= THRESHOLD2

 \* if a correct process has sent a precommit message in a round, it should
 \* have sent a prevote
 IfSentPrecommitThenSentPrevote ==
  \A r \in Rounds:
    \A mpc \in msgsPrecommit[r]:
      mpc.src \in Corr =>
        \E m \in msgsPrevote[r]:
          m.src = mpc.src

 \* there is a locked round if a only if there is a locked value
 LockedRoundIffLockedValue(p) ==
  (lockedRound[p] = NilRound) <=> (lockedValue[p] = NilValue)
  
 AllLockedRoundIffLockedValue ==
  \A p \in Corr:
    LockedRoundIffLockedValue(p)
            
 \* when a process locked a round, it must have sent a precommit on the locked value.
 IfLockedRoundThenSentCommit(p) ==
  lockedRound[p] /= NilRound
    => \E r \in { rr \in Rounds: rr <= round[p] }:
       \E m \in msgsPrecommit[r]:
         m.src = p /\ m.id = lockedValue[p]
         
 AllIfLockedRoundThenSentCommit ==
  \A p \in Corr:
    IfLockedRoundThenSentCommit(p)
         
 \* a process always locks the latest round, for which it has sent a PRECOMMIT
 LatestPrecommitHasLockedRound(p) ==
  LET pPrecommits ==
    {mm \in UNION { msgsPrecommit[r]: r \in Rounds }: mm.src = p /\ mm.id /= NilValue }
  IN
  pPrecommits /= {} <: {MT}
    => LET latest ==
         CHOOSE m \in pPrecommits:
           \A m2 \in pPrecommits:
             m2.round <= m.round
       IN
       /\ lockedRound[p] = latest.round
       /\ lockedValue[p] = latest.id
       
 AllLatestPrecommitHasLockedRound ==
  \A p \in Corr:
    LatestPrecommitHasLockedRound(p)

 \* Every correct process sends only one value or NilValue.
 \* This test has quantifier alternation -- a threat to all decision procedures.
 \* Luckily, the sets Corr and ValidValues are small.
 NoEquivocationByCorrect(r, msgs) ==
  \A p \in Corr:
    \E v \in ValidValues \union {NilValue}:
      \A m \in msgs[r]:
        \/ m.src /= p
        \/ m.id = v

 \* a proposer nevers sends two values
 ProposalsByProposer(r, msgs) ==
  \* if the proposer is not faulty, it sends only one value
  \E v \in ValidValues:
    \A m \in msgs[r]:
      \/ m.src \in Faulty
      \/ m.src = Proposer[r] /\ m.proposal = v
    
 AllNoEquivocationByCorrect ==
  \A r \in Rounds:
    /\ ProposalsByProposer(r, msgsPropose)    
    /\ NoEquivocationByCorrect(r, msgsPrevote)    
    /\ NoEquivocationByCorrect(r, msgsPrecommit)    

 \* construct the set of the message senders
 Senders(M) == { m.src: m \in M }

 \* The final piece by Josef Widder:
 \* if T + 1 processes precommit on the same value in a round,
 \* then in the future rounds there are less than 2T + 1 prevotes for another value
 PrecommitsLockValue ==
  \A r \in Rounds:
    \A v \in ValidValues \union {NilValue}:
      \/ LET Precommits ==  {m \in msgsPrecommit[r]: m.id = v}
        IN
        Cardinality(Senders(Precommits)) < THRESHOLD1
      \/ \A fr \in { rr \in Rounds: rr > r }:  \* future rounds
          \A w \in (ValuesOrNil) \ {v}:
            LET Prevotes == {m \in msgsPrevote[fr]: m.id = w}
            IN
            Cardinality(Senders(Prevotes)) < THRESHOLD2
    
 \* a combination of all lemmas
 Inv ==
    /\ EvidenceContainsMessages
    /\ AllNoFutureMessagesSent
    /\ AllIfInPrevoteThenSentPrevote
    /\ AllIfInPrecommitThenSentPrecommit
    /\ AllIfInDecidedThenReceivedProposal 
    /\ AllIfInDecidedThenReceivedTwoThirds 
    /\ AllIfInDecidedThenValidDecision
    /\ AllLockedRoundIffLockedValue
    /\ AllIfLockedRoundThenSentCommit
    /\ AllLatestPrecommitHasLockedRound
    /\ AllIfSentPrevoteThenReceivedProposalOrTwoThirds
    /\ IfSentPrecommitThenSentPrevote
    /\ IfSentPrecommitThenReceivedTwoThirds
    /\ AllNoEquivocationByCorrect
    /\ PrecommitsLockValue

 \* this is the inductive invariant we like to check
 TypedInv == TypeOK /\ Inv    
       
 \* UNUSED FOR SAFETY
 ValidRoundNotSmallerThanLockedRound(p) ==
  validRound[p] >= lockedRound[p]

 \* UNUSED FOR SAFETY
 ValidRoundIffValidValue(p) ==
  (validRound[p] = NilRound) <=> (validValue[p] = NilValue)

 \* UNUSED FOR SAFETY
 AllValidRoundIffValidValue ==
  \A p \in Corr: ValidRoundIffValidValue(p)

 \* if validRound is defined, then there are two-thirds of PREVOTEs
 IfValidRoundThenTwoThirds(p) ==
  \/ validRound[p] = NilRound
  \/ LET PV == { m \in msgsPrevote[validRound[p]]: m.id = validValue[p] } IN
     Cardinality(PV) >= THRESHOLD2
     
 \* UNUSED FOR SAFETY
 AllIfValidRoundThenTwoThirds ==
  \A p \in Corr: IfValidRoundThenTwoThirds(p)     

 \* a valid round can be only set to a valid value that was proposed earlier
 IfValidRoundThenProposal(p) ==
  \/ validRound[p] = NilRound
  \/ \E m \in msgsPropose[validRound[p]]:
       m.proposal = validValue[p]

 \* UNUSED FOR SAFETY
 AllIfValidRoundThenProposal ==
  \A p \in Corr: IfValidRoundThenProposal(p)

 (******************************** THEOREMS ***************************************)
 (* Under this condition, the faulty processes can decide alone *)
 FaultyQuorum == Cardinality(Faulty) >= THRESHOLD2

 (* The standard condition of the Tendermint security model *)
 LessThanThirdFaulty == N > 3 * T /\ Cardinality(Faulty) <= T

 (*
 TypedInv is an inductive invariant, provided that there is no faulty quorum.
 We run Apalache to prove this theorem only for fixed instances of 4 to 10 processes.
 (We run Apalache manually, as it does not parse theorem statements at the moment.)
 To get a parameterized argument, one has to use a theorem prover, e.g., TLAPS.
 *)
 THEOREM TypedInvIsInductive ==
    \/ FaultyQuorum \* if there are 2 * T + 1 faulty processes, we give up
    \//\ Init => TypedInv
      /\ TypedInv /\ [Next]_vars => TypedInv'

 (*
 There should be no fork, when there are less than 1/3 faulty processes.
 *)
 THEOREM AgreementWhenLessThanThirdFaulty ==
    LessThanThirdFaulty /\ TypedInv => Agreement

 (*
 In a more general case, when there are less than 2/3 faulty processes,
 there is either Agreement (no fork), or two scenarios exist:
 equivocation by Faulty, or amnesia by Faulty.
 *)
 THEOREM AgreementOrFork ==
    ~FaultyQuorum /\ TypedInv => Accountability

 =============================================================================    
 
--- a/rust-spec/tendermint-accountability/TendermintAccTrace_004_draft.tla
+++ b/rust-spec/tendermint-accountability/TendermintAccTrace_004_draft.tla
@ -0,0 +1,33 @@
 ------------------ MODULE TendermintAccTrace_004_draft -------------------------
 (*
  When Apalache is running too slow and we have an idea of a counterexample,
  we use this module to restrict the behaviors only to certain actions.
  Once the whole trace is replayed, the system deadlocks.
 
  Version 1.

  Igor Konnov, 2020.
 *)

 EXTENDS Sequences, Apalache, TendermintAcc_004_draft

 \* a sequence of action names that should appear in the given order,
 \* excluding "Init"
 CONSTANT Trace

 VARIABLE toReplay

 TraceInit ==
    /\ toReplay = Trace
    /\ action' := "Init"
    /\ Init

 TraceNext ==
    /\ Len(toReplay) > 0
    /\ toReplay' = Tail(toReplay)
    \* Here is the trick. We restrict the action to the expected one,
    \* so the other actions will be pruned
    /\ action' := Head(toReplay)
    /\ Next

 ================================================================================
--- a/rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla
+++ b/rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla
@ -0,0 +1,474 @@
 -------------------- MODULE TendermintAcc_004_draft ---------------------------
 (*
 A TLA+ specification of a simplified Tendermint consensus, tuned for
 fork accountability. The simplifications are as follows:

 - the protocol runs for one height, that is, it is one-shot consensus

 - this specification focuses on safety, so timeouts are modelled
   with non-determinism

 - the proposer function is non-determinstic, no fairness is assumed

 - the messages by the faulty processes are injected right in the initial states

 - every process has the voting power of 1

 - hashes are modelled as identity

 Having the above assumptions in mind, the specification follows the pseudo-code
 of the Tendermint paper: https://arxiv.org/abs/1807.04938

 Byzantine processes can demonstrate arbitrary behavior, including
 no communication. We show that if agreement is violated, then the Byzantine
 processes demonstrate one of the two behaviours:

   - Equivocation: a Byzantine process may send two different values
     in the same round.

   - Amnesia: a Byzantine process may lock a value without unlocking
     the previous value that it has locked in the past.

 * Version 4. Remove defective processes, fix bugs, collect global evidence.
 * Version 3. Modular and parameterized definitions.
 * Version 2. Bugfixes in the spec and an inductive invariant.
 * Version 1. A preliminary specification.

 Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
 *)

 EXTENDS Integers, FiniteSets

 (********************* PROTOCOL PARAMETERS **********************************)
 CONSTANTS
    Corr,          \* the set of correct processes 
    Faulty,        \* the set of Byzantine processes, may be empty
    N,             \* the total number of processes: correct, defective, and Byzantine
    T,             \* an upper bound on the number of Byzantine processes
    ValidValues,   \* the set of valid values, proposed both by correct and faulty
    InvalidValues, \* the set of invalid values, never proposed by the correct ones
    MaxRound,      \* the maximal round number
    Proposer       \* the proposer function from 0..NRounds to 1..N

 ASSUME(N = Cardinality(Corr \union Faulty))

 (*************************** DEFINITIONS ************************************)
 AllProcs == Corr \union Faulty      \* the set of all processes
 Rounds == 0..MaxRound               \* the set of potential rounds
 NilRound == -1   \* a special value to denote a nil round, outside of Rounds
 RoundsOrNil == Rounds \union {NilRound}
 Values == ValidValues \union InvalidValues \* the set of all values
 NilValue == "None"  \* a special value for a nil round, outside of Values
 ValuesOrNil == Values \union {NilValue}

 \* a value hash is modeled as identity
 Id(v) == v

 \* The validity predicate
 IsValid(v) == v \in ValidValues

 \* the two thresholds that are used in the algorithm
 THRESHOLD1 == T + 1     \* at least one process is not faulty
 THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T

 (********************* TYPE ANNOTATIONS FOR APALACHE **************************)
 \* the operator for type annotations
 a <: b == a

 \* the type of message records
 MT == [type |-> STRING, src |-> STRING, round |-> Int,
       proposal |-> STRING, validRound |-> Int, id |-> STRING]
       
 \* a type annotation for a message
 AsMsg(m) == m <: MT
 \* a type annotation for a set of messages
 SetOfMsgs(S) == S <: {MT}       
 \* a type annotation for an empty set of messages
 EmptyMsgSet == SetOfMsgs({})

 (********************* PROTOCOL STATE VARIABLES ******************************)
 VARIABLES
  round,    \* a process round number: Corr -> Rounds
  step,     \* a process step: Corr -> { "PROPOSE", "PREVOTE", "PRECOMMIT", "DECIDED" }
  decision, \* process decision: Corr -> ValuesOrNil
  lockedValue,  \* a locked value: Corr -> ValuesOrNil
  lockedRound,  \* a locked round: Corr -> RoundsOrNil
  validValue,   \* a valid value: Corr -> ValuesOrNil
  validRound    \* a valid round: Corr -> RoundsOrNil

 \* book-keeping variables
 VARIABLES
  msgsPropose,   \* PROPOSE messages broadcast in the system, Rounds -> Messages
  msgsPrevote,   \* PREVOTE messages broadcast in the system, Rounds -> Messages
  msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
  evidence, \* the messages that were used by the correct processes to make transitions
  action        \* we use this variable to see which action was taken

 (* to see a type invariant, check TendermintAccInv3 *)  
 
 \* a handy definition used in UNCHANGED
 vars == <<round, step, decision, lockedValue, lockedRound,
          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit>>

 (********************* PROTOCOL INITIALIZATION ******************************)
 FaultyProposals(r) ==
    SetOfMsgs([type: {"PROPOSAL"}, src: Faulty,
               round: {r}, proposal: Values, validRound: RoundsOrNil])

 AllFaultyProposals ==
    SetOfMsgs([type: {"PROPOSAL"}, src: Faulty,
               round: Rounds, proposal: Values, validRound: RoundsOrNil])

 FaultyPrevotes(r) ==
    SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: {r}, id: Values])

 AllFaultyPrevotes ==    
    SetOfMsgs([type: {"PREVOTE"}, src: Faulty, round: Rounds, id: Values])

 FaultyPrecommits(r) ==
    SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: {r}, id: Values])

 AllFaultyPrecommits ==
    SetOfMsgs([type: {"PRECOMMIT"}, src: Faulty, round: Rounds, id: Values])
   
 BenignRoundsInMessages(msgfun) ==
  \* the message function never contains a message for a wrong round
  \A r \in Rounds:
    \A m \in msgfun[r]:
      r = m.round

 \* The initial states of the protocol. Some faults can be in the system already.
 Init ==
    /\ round = [p \in Corr |-> 0]
    /\ step = [p \in Corr |-> "PROPOSE"]
    /\ decision = [p \in Corr |-> NilValue]
    /\ lockedValue = [p \in Corr |-> NilValue]
    /\ lockedRound = [p \in Corr |-> NilRound]
    /\ validValue = [p \in Corr |-> NilValue]
    /\ validRound = [p \in Corr |-> NilRound]
    /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
    /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
    /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
    /\ BenignRoundsInMessages(msgsPropose)
    /\ BenignRoundsInMessages(msgsPrevote)
    /\ BenignRoundsInMessages(msgsPrecommit)
    /\ evidence = EmptyMsgSet
    /\ action' = "Init"

 (************************ MESSAGE PASSING ********************************)
 BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
  LET newMsg ==
    AsMsg([type |-> "PROPOSAL", src |-> pSrc, round |-> pRound,
           proposal |-> pProposal, validRound |-> pValidRound])
  IN
  msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]

 BroadcastPrevote(pSrc, pRound, pId) ==
  LET newMsg == AsMsg([type |-> "PREVOTE",
                       src |-> pSrc, round |-> pRound, id |-> pId])
  IN
  msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]

 BroadcastPrecommit(pSrc, pRound, pId) ==
  LET newMsg == AsMsg([type |-> "PRECOMMIT",
                       src |-> pSrc, round |-> pRound, id |-> pId])
  IN
  msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]


 (********************* PROTOCOL TRANSITIONS ******************************)
 \* lines 12-13
 StartRound(p, r) ==
   /\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
   /\ round' = [round EXCEPT ![p] = r]
   /\ step' = [step EXCEPT ![p] = "PROPOSE"] 

 \* lines 14-19, a proposal may be sent later
 InsertProposal(p) == 
  LET r == round[p] IN
  /\ p = Proposer[r]
  /\ step[p] = "PROPOSE"
    \* if the proposer is sending a proposal, then there are no other proposals
    \* by the correct processes for the same round
  /\ \A m \in msgsPropose[r]: m.src /= p
  /\ \E v \in ValidValues: 
      LET proposal == IF validValue[p] /= NilValue THEN validValue[p] ELSE v IN
      BroadcastProposal(p, round[p], proposal, validRound[p])
  /\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
                validValue, step, validRound, msgsPrevote, msgsPrecommit>>
  /\ action' = "InsertProposal"

 \* lines 22-27
 UponProposalInPropose(p) ==
  \E v \in Values:
    /\ step[p] = "PROPOSE" (* line 22 *)
    /\ LET msg ==
        AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
               round |-> round[p], proposal |-> v, validRound |-> NilRound]) IN
      /\ msg \in msgsPropose[round[p]] \* line 22
      /\ evidence' = {msg} \union evidence
    /\ LET mid == (* line 23 *)
         IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
         THEN Id(v)
         ELSE NilValue
       IN
       BroadcastPrevote(p, round[p], mid) \* lines 24-26
    /\ step' = [step EXCEPT ![p] = "PREVOTE"]
    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
                   validValue, validRound, msgsPropose, msgsPrecommit>>
    /\ action' = "UponProposalInPropose"

 \* lines 28-33        
 UponProposalInProposeAndPrevote(p) ==
  \E v \in Values, vr \in Rounds:
    /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
    /\ LET msg ==
         AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
                round |-> round[p], proposal |-> v, validRound |-> vr])
       IN
       /\ msg \in msgsPropose[round[p]] \* line 28
       /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(v) } IN
          /\ Cardinality(PV) >= THRESHOLD2 \* line 28
          /\ evidence' = PV \union {msg} \union evidence
    /\ LET mid == (* line 29 *)
         IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
         THEN Id(v)
         ELSE NilValue
       IN
       BroadcastPrevote(p, round[p], mid) \* lines 24-26
    /\ step' = [step EXCEPT ![p] = "PREVOTE"]
    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
                   validValue, validRound, msgsPropose, msgsPrecommit>>
    /\ action' = "UponProposalInProposeAndPrevote"
                     
 \* lines 34-35 + lines 61-64 (onTimeoutPrevote)
 UponQuorumOfPrevotesAny(p) ==
  /\ step[p] = "PREVOTE" \* line 34 and 61
  /\ \E MyEvidence \in SUBSET msgsPrevote[round[p]]:
      \* find the unique voters in the evidence
      LET Voters == { m.src: m \in MyEvidence } IN
      \* compare the number of the unique voters against the threshold
      /\ Cardinality(Voters) >= THRESHOLD2 \* line 34
      /\ evidence' = MyEvidence \union evidence
      /\ BroadcastPrecommit(p, round[p], NilValue)
      /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
      /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
                    validValue, validRound, msgsPropose, msgsPrevote>>
      /\ action' = "UponQuorumOfPrevotesAny"
                     
 \* lines 36-46
 UponProposalInPrevoteOrCommitAndPrevote(p) ==
  \E v \in ValidValues, vr \in RoundsOrNil:
    /\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
    /\ LET msg ==
         AsMsg([type |-> "PROPOSAL", src |-> Proposer[round[p]],
                round |-> round[p], proposal |-> v, validRound |-> vr]) IN
        /\ msg \in msgsPropose[round[p]] \* line 36
        /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(v) } IN
          /\ Cardinality(PV) >= THRESHOLD2 \* line 36
          /\ evidence' = PV \union {msg} \union evidence
    /\  IF step[p] = "PREVOTE"
        THEN \* lines 38-41:
          /\ lockedValue' = [lockedValue EXCEPT ![p] = v]
          /\ lockedRound' = [lockedRound EXCEPT ![p] = round[p]]
          /\ BroadcastPrecommit(p, round[p], Id(v))
          /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
        ELSE
          UNCHANGED <<lockedValue, lockedRound, msgsPrecommit, step>>
      \* lines 42-43
    /\ validValue' = [validValue EXCEPT ![p] = v]
    /\ validRound' = [validRound EXCEPT ![p] = round[p]]
    /\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote>>
    /\ action' = "UponProposalInPrevoteOrCommitAndPrevote"

 \* lines 47-48 + 65-67 (onTimeoutPrecommit)
 UponQuorumOfPrecommitsAny(p) ==
  /\ \E MyEvidence \in SUBSET msgsPrecommit[round[p]]:
      \* find the unique committers in the evidence
      LET Committers == { m.src: m \in MyEvidence } IN
      \* compare the number of the unique committers against the threshold
      /\ Cardinality(Committers) >= THRESHOLD2 \* line 47
      /\ evidence' = MyEvidence \union evidence
      /\ round[p] + 1 \in Rounds
      /\ StartRound(p, round[p] + 1)   
      /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
                    validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
      /\ action' = "UponQuorumOfPrecommitsAny"
                     
 \* lines 49-54        
 UponProposalInPrecommitNoDecision(p) ==
  /\ decision[p] = NilValue \* line 49
  /\ \E v \in ValidValues (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
    /\ LET msg == AsMsg([type |-> "PROPOSAL", src |-> Proposer[r],
                           round |-> r, proposal |-> v, validRound |-> vr]) IN
     /\ msg \in msgsPropose[r] \* line 49
     /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(v) } IN
       /\ Cardinality(PV) >= THRESHOLD2 \* line 49
       /\ evidence' = PV \union {msg} \union evidence
       /\ decision' = [decision EXCEPT ![p] = v] \* update the decision, line 51
    \* The original algorithm does not have 'DECIDED', but it increments the height.
    \* We introduced 'DECIDED' here to prevent the process from changing its decision.
       /\ step' = [step EXCEPT ![p] = "DECIDED"]
       /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
                     validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
       /\ action' = "UponProposalInPrecommitNoDecision"
                                                          
 \* the actions below are not essential for safety, but added for completeness

 \* lines 20-21 + 57-60
 OnTimeoutPropose(p) ==
  /\ step[p] = "PROPOSE"
  /\ p /= Proposer[round[p]]
  /\ BroadcastPrevote(p, round[p], NilValue)
  /\ step' = [step EXCEPT ![p] = "PREVOTE"]
  /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
                validRound, decision, evidence, msgsPropose, msgsPrecommit>>
  /\ action' = "OnTimeoutPropose"

 \* lines 44-46
 OnQuorumOfNilPrevotes(p) ==
  /\ step[p] = "PREVOTE"
  /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilValue) } IN
    /\ Cardinality(PV) >= THRESHOLD2 \* line 36
    /\ evidence' = PV \union evidence
    /\ BroadcastPrecommit(p, round[p], Id(NilValue))
    /\ step' = [step EXCEPT ![p] = "PREVOTE"]
    /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
                  validRound, decision, msgsPropose, msgsPrevote>>
    /\ action' = "OnQuorumOfNilPrevotes"

 \* lines 55-56
 OnRoundCatchup(p) ==
  \E r \in {rr \in Rounds: rr > round[p]}:
    LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
    \E MyEvidence \in SUBSET RoundMsgs:
        LET Faster == { m.src: m \in MyEvidence } IN
        /\ Cardinality(Faster) >= THRESHOLD1
        /\ evidence' = MyEvidence \union evidence
        /\ StartRound(p, r)
        /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
                      validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
        /\ action' = "OnRoundCatchup"

 (*
 * A system transition. In this specificatiom, the system may eventually deadlock,
 * e.g., when all processes decide. This is expected behavior, as we focus on safety.
 *)
 Next ==
  \E p \in Corr:
    \/ InsertProposal(p)
    \/ UponProposalInPropose(p)
    \/ UponProposalInProposeAndPrevote(p)
    \/ UponQuorumOfPrevotesAny(p)
    \/ UponProposalInPrevoteOrCommitAndPrevote(p)
    \/ UponQuorumOfPrecommitsAny(p)
    \/ UponProposalInPrecommitNoDecision(p)
    \* the actions below are not essential for safety, but added for completeness
    \/ OnTimeoutPropose(p)
    \/ OnQuorumOfNilPrevotes(p)
    \/ OnRoundCatchup(p)

  
 (**************************** FORK SCENARIOS  ***************************)

 \* equivocation by a process p
 EquivocationBy(p) ==
   \E m1, m2 \in evidence:
    /\ m1 /= m2
    /\ m1.src = p
    /\ m2.src = p
    /\ m1.round = m2.round
    /\ m1.type = m2.type

 \* amnesic behavior by a process p
 AmnesiaBy(p) ==
    \E r1, r2 \in Rounds:
      /\ r1 < r2
      /\ \E v1, v2 \in ValidValues:
        /\ v1 /= v2
        /\ AsMsg([type |-> "PRECOMMIT", src |-> p,
                 round |-> r1, id |-> Id(v1)]) \in evidence
        /\ AsMsg([type |-> "PREVOTE", src |-> p,
                 round |-> r2, id |-> Id(v2)]) \in evidence
        /\ \A r \in { rnd \in Rounds: r1 <= rnd /\ rnd < r2 }:
            LET prevotes ==
                { m \in evidence:
                    m.type = "PREVOTE" /\ m.round = r /\ m.id = Id(v2) }
            IN
            Cardinality(prevotes) < THRESHOLD2

 (******************************** PROPERTIES  ***************************************)

 \* the safety property -- agreement
 Agreement ==
  \A p, q \in Corr:
    \/ decision[p] = NilValue
    \/ decision[q] = NilValue
    \/ decision[p] = decision[q]

 \* the protocol validity
 Validity ==
    \A p \in Corr: decision[p] \in ValidValues \union {NilValue}

 (*
  The protocol safety. Two cases are possible:
     1. There is no fork, that is, Agreement holds true.
     2. A subset of faulty processes demonstrates equivocation or amnesia.
 *)
 Accountability ==
    \/ Agreement
    \/ \E Detectable \in SUBSET Faulty:
        /\ Cardinality(Detectable) >= THRESHOLD1
        /\ \A p \in Detectable:
            EquivocationBy(p) \/ AmnesiaBy(p)

 (****************** FALSE INVARIANTS TO PRODUCE EXAMPLES ***********************)
 
 \* This property is violated. You can check it to see how amnesic behavior
 \* appears in the evidence variable.
 NoAmnesia ==
    \A p \in Faulty: ~AmnesiaBy(p)

 \* This property is violated. You can check it to see an example of equivocation.
 NoEquivocation ==
    \A p \in Faulty: ~EquivocationBy(p)

 \* This property is violated. You can check it to see an example of agreement.
 \* It is not exactly ~Agreement, as we do not want to see the states where
 \* decision[p] = NilValue
 NoAgreement ==
  \A p, q \in Corr:
    (p /= q /\ decision[p] /= NilValue /\ decision[q] /= NilValue)
        => decision[p] /= decision[q]
 
 \* Either agreement holds, or the faulty processes indeed demonstrate amnesia.
 \* This property is violated. A counterexample should demonstrate equivocation.
 AgreementOrAmnesia ==
    Agreement \/ (\A p \in Faulty: AmnesiaBy(p))
 
 \* We expect this property to be violated. It shows us a protocol run,
 \* where one faulty process demonstrates amnesia without equivocation.
 \* However, the absence of amnesia
 \* is a tough constraint for Apalache. It has not reported a counterexample
 \* for n=4,f=2, length <= 5.
 ShowMeAmnesiaWithoutEquivocation ==
    (~Agreement /\ \E p \in Faulty: ~EquivocationBy(p))
        => \A p \in Faulty: ~AmnesiaBy(p)

 \* This property is violated on n=4,f=2, length=4 in less than 10 min.
 \* Two faulty processes may demonstrate amnesia without equivocation.
 AmnesiaImpliesEquivocation ==
    (\E p \in Faulty: AmnesiaBy(p)) => (\E q \in Faulty: EquivocationBy(q))

 (*
  This property is violated. You can check it to see that all correct processes
  may reach MaxRound without making a decision. 
 *)
 NeverUndecidedInMaxRound ==
    LET AllInMax == \A p \in Corr: round[p] = MaxRound
        AllDecided == \A p \in Corr: decision[p] /= NilValue
    IN
    AllInMax => AllDecided

 =============================================================================    
 
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-mem-log.svg
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-mem-log.svg
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-mem.svg
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-mem.svg
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-ncells.svg
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-ncells.svg
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-nclauses.svg
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-nclauses.svg
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-report.md
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-report.md
@ -0,0 +1,62 @@
 # Results of 001indinv-apalache


 ## 1. Awesome plots

 ### 1.1. Time (logarithmic scale)

 ![time-log](001indinv-apalache-time-log.svg "Time Log")

 ### 1.2. Time (linear)

 ![time-log](001indinv-apalache-time.svg "Time Log")

 ### 1.3. Memory (logarithmic scale)

 ![mem-log](001indinv-apalache-mem-log.svg "Memory Log")

 ### 1.4. Memory (linear)

 ![mem](001indinv-apalache-mem.svg "Memory Log")

 ### 1.5. Number of arena cells (linear)

 ![ncells](001indinv-apalache-ncells.svg "Number of arena cells")

 ### 1.6. Number of SMT clauses (linear)

 ![nclauses](001indinv-apalache-nclauses.svg "Number of SMT clauses")

 ## 2. Input parameters

 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_n5_f1.tla  |  apalache  |  10h      |  TypedInv  |  TypedInv        |        |  --length=1 --cinit=ConstInit
 4   |  MC_n5_f2.tla  |  apalache  |  10h      |  TypedInv  |  TypedInv        |        |  --length=1 --cinit=ConstInit
 5   |  MC_n4_f1.tla  |  apalache  |  20h      |  Init      |  TypedInv        |        |  --length=0 --cinit=ConstInit
 6   |  MC_n4_f2.tla  |  apalache  |  20h      |  Init      |  TypedInv        |        |  --length=0 --cinit=ConstInit
 7   |  MC_n5_f1.tla  |  apalache  |  20h      |  Init      |  TypedInv        |        |  --length=0 --cinit=ConstInit
 8   |  MC_n5_f2.tla  |  apalache  |  20h      |  Init      |  TypedInv        |        |  --length=0 --cinit=ConstInit
 9   |  MC_n4_f1.tla  |  apalache  |  20h      |  TypedInv  |  Agreement       |        |  --length=0 --cinit=ConstInit
 10  |  MC_n4_f2.tla  |  apalache  |  20h      |  TypedInv  |  Accountability  |        |  --length=0 --cinit=ConstInit
 11  |  MC_n5_f1.tla  |  apalache  |  20h      |  TypedInv  |  Agreement       |        |  --length=0 --cinit=ConstInit
 12  |  MC_n5_f2.tla  |  apalache  |  20h      |  TypedInv  |  Accountability  |        |  --length=0 --cinit=ConstInit

 ## 3. Detailed results: 001indinv-apalache-unstable.csv

 01:no  |  02:tool   |  03:status  |  04:time_sec  |  05:depth  |  05:mem_kb  |  10:ninit_trans  |  11:ninit_trans  |  12:ncells  |  13:nclauses  |  14:navg_clause_len
 -------|------------|-------------|---------------|------------|-------------|------------------|------------------|-------------|---------------|--------------------
 1      |  apalache  |  NoError    |  11m          |  1         |  3.0GB      |  0               |  0               |  217K       |  1.0M         |  89
 2      |  apalache  |  NoError    |  11m          |  1         |  3.0GB      |  0               |  0               |  207K       |  1.0M         |  88
 3      |  apalache  |  NoError    |  16m          |  1         |  4.0GB      |  0               |  0               |  311K       |  2.0M         |  101
 4      |  apalache  |  NoError    |  14m          |  1         |  3.0GB      |  0               |  0               |  290K       |  1.0M         |  103
 5      |  apalache  |  NoError    |  9s           |  0         |  563MB      |  0               |  0               |  2.0K       |  14K          |  42
 6      |  apalache  |  NoError    |  10s          |  0         |  657MB      |  0               |  0               |  2.0K       |  28K          |  43
 7      |  apalache  |  NoError    |  8s           |  0         |  635MB      |  0               |  0               |  2.0K       |  17K          |  44
 8      |  apalache  |  NoError    |  10s          |  0         |  667MB      |  0               |  0               |  3.0K       |  32K          |  45
 9      |  apalache  |  NoError    |  5m05s        |  0         |  2.0GB      |  0               |  0               |  196K       |  889K         |  108
 10     |  apalache  |  NoError    |  8m08s        |  0         |  6.0GB      |  0               |  0               |  2.0M       |  3.0M         |  34
 11     |  apalache  |  NoError    |  9m09s        |  0         |  3.0GB      |  0               |  0               |  284K       |  1.0M         |  128
 12     |  apalache  |  NoError    |  14m          |  0         |  7.0GB      |  0               |  0               |  4.0M       |  5.0M         |  38
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-time-log.svg
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-time-log.svg
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-time.svg
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-time.svg
@ -0,0 +1,957 @@
 <?xml version="1.0" encoding="utf-8" standalone="no"?>
 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
  "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
 <!-- Created with matplotlib (https://matplotlib.org/) -->
 <svg height="345.6pt" version="1.1" viewBox="0 0 460.8 345.6" width="460.8pt" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
 <metadata>
  <rdf:RDF xmlns:cc="http://creativecommons.org/ns#" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
   <cc:Work>
    <dc:type rdf:resource="http://purl.org/dc/dcmitype/StillImage"/>
    <dc:date>2020-12-11T20:07:39.136767</dc:date>
    <dc:format>image/svg+xml</dc:format>
    <dc:creator>
     <cc:Agent>
      <dc:title>Matplotlib v3.3.3, https://matplotlib.org/</dc:title>
     </cc:Agent>
    </dc:creator>
   </cc:Work>
  </rdf:RDF>
 </metadata>
 <defs>
  <style type="text/css">*{stroke-linecap:butt;stroke-linejoin:round;}</style>
 </defs>
 <g id="figure_1">
  <g id="patch_1">
   <path d="M 0 345.6 
 L 460.8 345.6 
 L 460.8 0 
 L 0 0 
 z
 " style="fill:#ffffff;"/>
  </g>
  <g id="axes_1">
   <g id="patch_2">
    <path d="M 57.6 307.584 
 L 414.72 307.584 
 L 414.72 41.472 
 L 57.6 41.472 
 z
 " style="fill:#ffffff;"/>
   </g>
   <g id="matplotlib.axis_1">
    <g id="xtick_1">
     <g id="line2d_1">
      <path clip-path="url(#p902cfd873e)" d="M 103.346777 307.584 
 L 103.346777 41.472 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_2">
      <defs>
       <path d="M 0 0 
 L 0 3.5 
 " id="m6c16508061" style="stroke:#000000;stroke-width:0.8;"/>
      </defs>
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="103.346777" xlink:href="#m6c16508061" y="307.584"/>
      </g>
     </g>
     <g id="text_1">
      <!-- 2 -->
      <g transform="translate(100.165527 322.182437)scale(0.1 -0.1)">
       <defs>
        <path d="M 19.1875 8.296875 
 L 53.609375 8.296875 
 L 53.609375 0 
 L 7.328125 0 
 L 7.328125 8.296875 
 Q 12.9375 14.109375 22.625 23.890625 
 Q 32.328125 33.6875 34.8125 36.53125 
 Q 39.546875 41.84375 41.421875 45.53125 
 Q 43.3125 49.21875 43.3125 52.78125 
 Q 43.3125 58.59375 39.234375 62.25 
 Q 35.15625 65.921875 28.609375 65.921875 
 Q 23.96875 65.921875 18.8125 64.3125 
 Q 13.671875 62.703125 7.8125 59.421875 
 L 7.8125 69.390625 
 Q 13.765625 71.78125 18.9375 73 
 Q 24.125 74.21875 28.421875 74.21875 
 Q 39.75 74.21875 46.484375 68.546875 
 Q 53.21875 62.890625 53.21875 53.421875 
 Q 53.21875 48.921875 51.53125 44.890625 
 Q 49.859375 40.875 45.40625 35.40625 
 Q 44.1875 33.984375 37.640625 27.21875 
 Q 31.109375 20.453125 19.1875 8.296875 
 z
 " id="DejaVuSans-50"/>
       </defs>
       <use xlink:href="#DejaVuSans-50"/>
      </g>
     </g>
    </g>
    <g id="xtick_2">
     <g id="line2d_3">
      <path clip-path="url(#p902cfd873e)" d="M 162.374876 307.584 
 L 162.374876 41.472 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_4">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="162.374876" xlink:href="#m6c16508061" y="307.584"/>
      </g>
     </g>
     <g id="text_2">
      <!-- 4 -->
      <g transform="translate(159.193626 322.182437)scale(0.1 -0.1)">
       <defs>
        <path d="M 37.796875 64.3125 
 L 12.890625 25.390625 
 L 37.796875 25.390625 
 z
 M 35.203125 72.90625 
 L 47.609375 72.90625 
 L 47.609375 25.390625 
 L 58.015625 25.390625 
 L 58.015625 17.1875 
 L 47.609375 17.1875 
 L 47.609375 0 
 L 37.796875 0 
 L 37.796875 17.1875 
 L 4.890625 17.1875 
 L 4.890625 26.703125 
 z
 " id="DejaVuSans-52"/>
       </defs>
       <use xlink:href="#DejaVuSans-52"/>
      </g>
     </g>
    </g>
    <g id="xtick_3">
     <g id="line2d_5">
      <path clip-path="url(#p902cfd873e)" d="M 221.402975 307.584 
 L 221.402975 41.472 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_6">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="221.402975" xlink:href="#m6c16508061" y="307.584"/>
      </g>
     </g>
     <g id="text_3">
      <!-- 6 -->
      <g transform="translate(218.221725 322.182437)scale(0.1 -0.1)">
       <defs>
        <path d="M 33.015625 40.375 
 Q 26.375 40.375 22.484375 35.828125 
 Q 18.609375 31.296875 18.609375 23.390625 
 Q 18.609375 15.53125 22.484375 10.953125 
 Q 26.375 6.390625 33.015625 6.390625 
 Q 39.65625 6.390625 43.53125 10.953125 
 Q 47.40625 15.53125 47.40625 23.390625 
 Q 47.40625 31.296875 43.53125 35.828125 
 Q 39.65625 40.375 33.015625 40.375 
 z
 M 52.59375 71.296875 
 L 52.59375 62.3125 
 Q 48.875 64.0625 45.09375 64.984375 
 Q 41.3125 65.921875 37.59375 65.921875 
 Q 27.828125 65.921875 22.671875 59.328125 
 Q 17.53125 52.734375 16.796875 39.40625 
 Q 19.671875 43.65625 24.015625 45.921875 
 Q 28.375 48.1875 33.59375 48.1875 
 Q 44.578125 48.1875 50.953125 41.515625 
 Q 57.328125 34.859375 57.328125 23.390625 
 Q 57.328125 12.15625 50.6875 5.359375 
 Q 44.046875 -1.421875 33.015625 -1.421875 
 Q 20.359375 -1.421875 13.671875 8.265625 
 Q 6.984375 17.96875 6.984375 36.375 
 Q 6.984375 53.65625 15.1875 63.9375 
 Q 23.390625 74.21875 37.203125 74.21875 
 Q 40.921875 74.21875 44.703125 73.484375 
 Q 48.484375 72.75 52.59375 71.296875 
 z
 " id="DejaVuSans-54"/>
       </defs>
       <use xlink:href="#DejaVuSans-54"/>
      </g>
     </g>
    </g>
    <g id="xtick_4">
     <g id="line2d_7">
      <path clip-path="url(#p902cfd873e)" d="M 280.431074 307.584 
 L 280.431074 41.472 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_8">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="280.431074" xlink:href="#m6c16508061" y="307.584"/>
      </g>
     </g>
     <g id="text_4">
      <!-- 8 -->
      <g transform="translate(277.249824 322.182437)scale(0.1 -0.1)">
       <defs>
        <path d="M 31.78125 34.625 
 Q 24.75 34.625 20.71875 30.859375 
 Q 16.703125 27.09375 16.703125 20.515625 
 Q 16.703125 13.921875 20.71875 10.15625 
 Q 24.75 6.390625 31.78125 6.390625 
 Q 38.8125 6.390625 42.859375 10.171875 
 Q 46.921875 13.96875 46.921875 20.515625 
 Q 46.921875 27.09375 42.890625 30.859375 
 Q 38.875 34.625 31.78125 34.625 
 z
 M 21.921875 38.8125 
 Q 15.578125 40.375 12.03125 44.71875 
 Q 8.5 49.078125 8.5 55.328125 
 Q 8.5 64.0625 14.71875 69.140625 
 Q 20.953125 74.21875 31.78125 74.21875 
 Q 42.671875 74.21875 48.875 69.140625 
 Q 55.078125 64.0625 55.078125 55.328125 
 Q 55.078125 49.078125 51.53125 44.71875 
 Q 48 40.375 41.703125 38.8125 
 Q 48.828125 37.15625 52.796875 32.3125 
 Q 56.78125 27.484375 56.78125 20.515625 
 Q 56.78125 9.90625 50.3125 4.234375 
 Q 43.84375 -1.421875 31.78125 -1.421875 
 Q 19.734375 -1.421875 13.25 4.234375 
 Q 6.78125 9.90625 6.78125 20.515625 
 Q 6.78125 27.484375 10.78125 32.3125 
 Q 14.796875 37.15625 21.921875 38.8125 
 z
 M 18.3125 54.390625 
 Q 18.3125 48.734375 21.84375 45.5625 
 Q 25.390625 42.390625 31.78125 42.390625 
 Q 38.140625 42.390625 41.71875 45.5625 
 Q 45.3125 48.734375 45.3125 54.390625 
 Q 45.3125 60.0625 41.71875 63.234375 
 Q 38.140625 66.40625 31.78125 66.40625 
 Q 25.390625 66.40625 21.84375 63.234375 
 Q 18.3125 60.0625 18.3125 54.390625 
 z
 " id="DejaVuSans-56"/>
       </defs>
       <use xlink:href="#DejaVuSans-56"/>
      </g>
     </g>
    </g>
    <g id="xtick_5">
     <g id="line2d_9">
      <path clip-path="url(#p902cfd873e)" d="M 339.459174 307.584 
 L 339.459174 41.472 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_10">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="339.459174" xlink:href="#m6c16508061" y="307.584"/>
      </g>
     </g>
     <g id="text_5">
      <!-- 10 -->
      <g transform="translate(333.096674 322.182437)scale(0.1 -0.1)">
       <defs>
        <path d="M 12.40625 8.296875 
 L 28.515625 8.296875 
 L 28.515625 63.921875 
 L 10.984375 60.40625 
 L 10.984375 69.390625 
 L 28.421875 72.90625 
 L 38.28125 72.90625 
 L 38.28125 8.296875 
 L 54.390625 8.296875 
 L 54.390625 0 
 L 12.40625 0 
 z
 " id="DejaVuSans-49"/>
        <path d="M 31.78125 66.40625 
 Q 24.171875 66.40625 20.328125 58.90625 
 Q 16.5 51.421875 16.5 36.375 
 Q 16.5 21.390625 20.328125 13.890625 
 Q 24.171875 6.390625 31.78125 6.390625 
 Q 39.453125 6.390625 43.28125 13.890625 
 Q 47.125 21.390625 47.125 36.375 
 Q 47.125 51.421875 43.28125 58.90625 
 Q 39.453125 66.40625 31.78125 66.40625 
 z
 M 31.78125 74.21875 
 Q 44.046875 74.21875 50.515625 64.515625 
 Q 56.984375 54.828125 56.984375 36.375 
 Q 56.984375 17.96875 50.515625 8.265625 
 Q 44.046875 -1.421875 31.78125 -1.421875 
 Q 19.53125 -1.421875 13.0625 8.265625 
 Q 6.59375 17.96875 6.59375 36.375 
 Q 6.59375 54.828125 13.0625 64.515625 
 Q 19.53125 74.21875 31.78125 74.21875 
 z
 " id="DejaVuSans-48"/>
       </defs>
       <use xlink:href="#DejaVuSans-49"/>
       <use x="63.623047" xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="xtick_6">
     <g id="line2d_11">
      <path clip-path="url(#p902cfd873e)" d="M 398.487273 307.584 
 L 398.487273 41.472 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_12">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="398.487273" xlink:href="#m6c16508061" y="307.584"/>
      </g>
     </g>
     <g id="text_6">
      <!-- 12 -->
      <g transform="translate(392.124773 322.182437)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-49"/>
       <use x="63.623047" xlink:href="#DejaVuSans-50"/>
      </g>
     </g>
    </g>
    <g id="text_7">
     <!-- benchmark -->
     <g transform="translate(207.937344 335.860562)scale(0.1 -0.1)">
      <defs>
       <path d="M 48.6875 27.296875 
 Q 48.6875 37.203125 44.609375 42.84375 
 Q 40.53125 48.484375 33.40625 48.484375 
 Q 26.265625 48.484375 22.1875 42.84375 
 Q 18.109375 37.203125 18.109375 27.296875 
 Q 18.109375 17.390625 22.1875 11.75 
 Q 26.265625 6.109375 33.40625 6.109375 
 Q 40.53125 6.109375 44.609375 11.75 
 Q 48.6875 17.390625 48.6875 27.296875 
 z
 M 18.109375 46.390625 
 Q 20.953125 51.265625 25.265625 53.625 
 Q 29.59375 56 35.59375 56 
 Q 45.5625 56 51.78125 48.09375 
 Q 58.015625 40.1875 58.015625 27.296875 
 Q 58.015625 14.40625 51.78125 6.484375 
 Q 45.5625 -1.421875 35.59375 -1.421875 
 Q 29.59375 -1.421875 25.265625 0.953125 
 Q 20.953125 3.328125 18.109375 8.203125 
 L 18.109375 0 
 L 9.078125 0 
 L 9.078125 75.984375 
 L 18.109375 75.984375 
 z
 " id="DejaVuSans-98"/>
       <path d="M 56.203125 29.59375 
 L 56.203125 25.203125 
 L 14.890625 25.203125 
 Q 15.484375 15.921875 20.484375 11.0625 
 Q 25.484375 6.203125 34.421875 6.203125 
 Q 39.59375 6.203125 44.453125 7.46875 
 Q 49.3125 8.734375 54.109375 11.28125 
 L 54.109375 2.78125 
 Q 49.265625 0.734375 44.1875 -0.34375 
 Q 39.109375 -1.421875 33.890625 -1.421875 
 Q 20.796875 -1.421875 13.15625 6.1875 
 Q 5.515625 13.8125 5.515625 26.8125 
 Q 5.515625 40.234375 12.765625 48.109375 
 Q 20.015625 56 32.328125 56 
 Q 43.359375 56 49.78125 48.890625 
 Q 56.203125 41.796875 56.203125 29.59375 
 z
 M 47.21875 32.234375 
 Q 47.125 39.59375 43.09375 43.984375 
 Q 39.0625 48.390625 32.421875 48.390625 
 Q 24.90625 48.390625 20.390625 44.140625 
 Q 15.875 39.890625 15.1875 32.171875 
 z
 " id="DejaVuSans-101"/>
       <path d="M 54.890625 33.015625 
 L 54.890625 0 
 L 45.90625 0 
 L 45.90625 32.71875 
 Q 45.90625 40.484375 42.875 44.328125 
 Q 39.84375 48.1875 33.796875 48.1875 
 Q 26.515625 48.1875 22.3125 43.546875 
 Q 18.109375 38.921875 18.109375 30.90625 
 L 18.109375 0 
 L 9.078125 0 
 L 9.078125 54.6875 
 L 18.109375 54.6875 
 L 18.109375 46.1875 
 Q 21.34375 51.125 25.703125 53.5625 
 Q 30.078125 56 35.796875 56 
 Q 45.21875 56 50.046875 50.171875 
 Q 54.890625 44.34375 54.890625 33.015625 
 z
 " id="DejaVuSans-110"/>
       <path d="M 48.78125 52.59375 
 L 48.78125 44.1875 
 Q 44.96875 46.296875 41.140625 47.34375 
 Q 37.3125 48.390625 33.40625 48.390625 
 Q 24.65625 48.390625 19.8125 42.84375 
 Q 14.984375 37.3125 14.984375 27.296875 
 Q 14.984375 17.28125 19.8125 11.734375 
 Q 24.65625 6.203125 33.40625 6.203125 
 Q 37.3125 6.203125 41.140625 7.25 
 Q 44.96875 8.296875 48.78125 10.40625 
 L 48.78125 2.09375 
 Q 45.015625 0.34375 40.984375 -0.53125 
 Q 36.96875 -1.421875 32.421875 -1.421875 
 Q 20.0625 -1.421875 12.78125 6.34375 
 Q 5.515625 14.109375 5.515625 27.296875 
 Q 5.515625 40.671875 12.859375 48.328125 
 Q 20.21875 56 33.015625 56 
 Q 37.15625 56 41.109375 55.140625 
 Q 45.0625 54.296875 48.78125 52.59375 
 z
 " id="DejaVuSans-99"/>
       <path d="M 54.890625 33.015625 
 L 54.890625 0 
 L 45.90625 0 
 L 45.90625 32.71875 
 Q 45.90625 40.484375 42.875 44.328125 
 Q 39.84375 48.1875 33.796875 48.1875 
 Q 26.515625 48.1875 22.3125 43.546875 
 Q 18.109375 38.921875 18.109375 30.90625 
 L 18.109375 0 
 L 9.078125 0 
 L 9.078125 75.984375 
 L 18.109375 75.984375 
 L 18.109375 46.1875 
 Q 21.34375 51.125 25.703125 53.5625 
 Q 30.078125 56 35.796875 56 
 Q 45.21875 56 50.046875 50.171875 
 Q 54.890625 44.34375 54.890625 33.015625 
 z
 " id="DejaVuSans-104"/>
       <path d="M 52 44.1875 
 Q 55.375 50.25 60.0625 53.125 
 Q 64.75 56 71.09375 56 
 Q 79.640625 56 84.28125 50.015625 
 Q 88.921875 44.046875 88.921875 33.015625 
 L 88.921875 0 
 L 79.890625 0 
 L 79.890625 32.71875 
 Q 79.890625 40.578125 77.09375 44.375 
 Q 74.3125 48.1875 68.609375 48.1875 
 Q 61.625 48.1875 57.5625 43.546875 
 Q 53.515625 38.921875 53.515625 30.90625 
 L 53.515625 0 
 L 44.484375 0 
 L 44.484375 32.71875 
 Q 44.484375 40.625 41.703125 44.40625 
 Q 38.921875 48.1875 33.109375 48.1875 
 Q 26.21875 48.1875 22.15625 43.53125 
 Q 18.109375 38.875 18.109375 30.90625 
 L 18.109375 0 
 L 9.078125 0 
 L 9.078125 54.6875 
 L 18.109375 54.6875 
 L 18.109375 46.1875 
 Q 21.1875 51.21875 25.484375 53.609375 
 Q 29.78125 56 35.6875 56 
 Q 41.65625 56 45.828125 52.96875 
 Q 50 49.953125 52 44.1875 
 z
 " id="DejaVuSans-109"/>
       <path d="M 34.28125 27.484375 
 Q 23.390625 27.484375 19.1875 25 
 Q 14.984375 22.515625 14.984375 16.5 
 Q 14.984375 11.71875 18.140625 8.90625 
 Q 21.296875 6.109375 26.703125 6.109375 
 Q 34.1875 6.109375 38.703125 11.40625 
 Q 43.21875 16.703125 43.21875 25.484375 
 L 43.21875 27.484375 
 z
 M 52.203125 31.203125 
 L 52.203125 0 
 L 43.21875 0 
 L 43.21875 8.296875 
 Q 40.140625 3.328125 35.546875 0.953125 
 Q 30.953125 -1.421875 24.3125 -1.421875 
 Q 15.921875 -1.421875 10.953125 3.296875 
 Q 6 8.015625 6 15.921875 
 Q 6 25.140625 12.171875 29.828125 
 Q 18.359375 34.515625 30.609375 34.515625 
 L 43.21875 34.515625 
 L 43.21875 35.40625 
 Q 43.21875 41.609375 39.140625 45 
 Q 35.0625 48.390625 27.6875 48.390625 
 Q 23 48.390625 18.546875 47.265625 
 Q 14.109375 46.140625 10.015625 43.890625 
 L 10.015625 52.203125 
 Q 14.9375 54.109375 19.578125 55.046875 
 Q 24.21875 56 28.609375 56 
 Q 40.484375 56 46.34375 49.84375 
 Q 52.203125 43.703125 52.203125 31.203125 
 z
 " id="DejaVuSans-97"/>
       <path d="M 41.109375 46.296875 
 Q 39.59375 47.171875 37.8125 47.578125 
 Q 36.03125 48 33.890625 48 
 Q 26.265625 48 22.1875 43.046875 
 Q 18.109375 38.09375 18.109375 28.8125 
 L 18.109375 0 
 L 9.078125 0 
 L 9.078125 54.6875 
 L 18.109375 54.6875 
 L 18.109375 46.1875 
 Q 20.953125 51.171875 25.484375 53.578125 
 Q 30.03125 56 36.53125 56 
 Q 37.453125 56 38.578125 55.875 
 Q 39.703125 55.765625 41.0625 55.515625 
 z
 " id="DejaVuSans-114"/>
       <path d="M 9.078125 75.984375 
 L 18.109375 75.984375 
 L 18.109375 31.109375 
 L 44.921875 54.6875 
 L 56.390625 54.6875 
 L 27.390625 29.109375 
 L 57.625 0 
 L 45.90625 0 
 L 18.109375 26.703125 
 L 18.109375 0 
 L 9.078125 0 
 z
 " id="DejaVuSans-107"/>
      </defs>
      <use xlink:href="#DejaVuSans-98"/>
      <use x="63.476562" xlink:href="#DejaVuSans-101"/>
      <use x="125" xlink:href="#DejaVuSans-110"/>
      <use x="188.378906" xlink:href="#DejaVuSans-99"/>
      <use x="243.359375" xlink:href="#DejaVuSans-104"/>
      <use x="306.738281" xlink:href="#DejaVuSans-109"/>
      <use x="404.150391" xlink:href="#DejaVuSans-97"/>
      <use x="465.429688" xlink:href="#DejaVuSans-114"/>
      <use x="506.542969" xlink:href="#DejaVuSans-107"/>
     </g>
    </g>
   </g>
   <g id="matplotlib.axis_2">
    <g id="ytick_1">
     <g id="line2d_13">
      <path clip-path="url(#p902cfd873e)" d="M 57.6 297.404198 
 L 414.72 297.404198 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_14">
      <defs>
       <path d="M 0 0 
 L -3.5 0 
 " id="m92e578bc9b" style="stroke:#000000;stroke-width:0.8;"/>
      </defs>
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="57.6" xlink:href="#m92e578bc9b" y="297.404198"/>
      </g>
     </g>
     <g id="text_8">
      <!-- 0 -->
      <g transform="translate(44.2375 301.203417)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="ytick_2">
     <g id="line2d_15">
      <path clip-path="url(#p902cfd873e)" d="M 57.6 249.499248 
 L 414.72 249.499248 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_16">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="57.6" xlink:href="#m92e578bc9b" y="249.499248"/>
      </g>
     </g>
     <g id="text_9">
      <!-- 200 -->
      <g transform="translate(31.5125 253.298466)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-50"/>
       <use x="63.623047" xlink:href="#DejaVuSans-48"/>
       <use x="127.246094" xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="ytick_3">
     <g id="line2d_17">
      <path clip-path="url(#p902cfd873e)" d="M 57.6 201.594297 
 L 414.72 201.594297 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_18">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="57.6" xlink:href="#m92e578bc9b" y="201.594297"/>
      </g>
     </g>
     <g id="text_10">
      <!-- 400 -->
      <g transform="translate(31.5125 205.393516)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-52"/>
       <use x="63.623047" xlink:href="#DejaVuSans-48"/>
       <use x="127.246094" xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="ytick_4">
     <g id="line2d_19">
      <path clip-path="url(#p902cfd873e)" d="M 57.6 153.689347 
 L 414.72 153.689347 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_20">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="57.6" xlink:href="#m92e578bc9b" y="153.689347"/>
      </g>
     </g>
     <g id="text_11">
      <!-- 600 -->
      <g transform="translate(31.5125 157.488565)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-54"/>
       <use x="63.623047" xlink:href="#DejaVuSans-48"/>
       <use x="127.246094" xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="ytick_5">
     <g id="line2d_21">
      <path clip-path="url(#p902cfd873e)" d="M 57.6 105.784396 
 L 414.72 105.784396 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_22">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="57.6" xlink:href="#m92e578bc9b" y="105.784396"/>
      </g>
     </g>
     <g id="text_12">
      <!-- 800 -->
      <g transform="translate(31.5125 109.583615)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-56"/>
       <use x="63.623047" xlink:href="#DejaVuSans-48"/>
       <use x="127.246094" xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="ytick_6">
     <g id="line2d_23">
      <path clip-path="url(#p902cfd873e)" d="M 57.6 57.879446 
 L 414.72 57.879446 
 " style="fill:none;stroke:#b0b0b0;stroke-linecap:square;stroke-opacity:0.2;stroke-width:0.8;"/>
     </g>
     <g id="line2d_24">
      <g>
       <use style="stroke:#000000;stroke-width:0.8;" x="57.6" xlink:href="#m92e578bc9b" y="57.879446"/>
      </g>
     </g>
     <g id="text_13">
      <!-- 1000 -->
      <g transform="translate(25.15 61.678664)scale(0.1 -0.1)">
       <use xlink:href="#DejaVuSans-49"/>
       <use x="63.623047" xlink:href="#DejaVuSans-48"/>
       <use x="127.246094" xlink:href="#DejaVuSans-48"/>
       <use x="190.869141" xlink:href="#DejaVuSans-48"/>
      </g>
     </g>
    </g>
    <g id="text_14">
     <!-- time, sec -->
     <g transform="translate(19.070312 197.432687)rotate(-90)scale(0.1 -0.1)">
      <defs>
       <path d="M 18.3125 70.21875 
 L 18.3125 54.6875 
 L 36.8125 54.6875 
 L 36.8125 47.703125 
 L 18.3125 47.703125 
 L 18.3125 18.015625 
 Q 18.3125 11.328125 20.140625 9.421875 
 Q 21.96875 7.515625 27.59375 7.515625 
 L 36.8125 7.515625 
 L 36.8125 0 
 L 27.59375 0 
 Q 17.1875 0 13.234375 3.875 
 Q 9.28125 7.765625 9.28125 18.015625 
 L 9.28125 47.703125 
 L 2.6875 47.703125 
 L 2.6875 54.6875 
 L 9.28125 54.6875 
 L 9.28125 70.21875 
 z
 " id="DejaVuSans-116"/>
       <path d="M 9.421875 54.6875 
 L 18.40625 54.6875 
 L 18.40625 0 
 L 9.421875 0 
 z
 M 9.421875 75.984375 
 L 18.40625 75.984375 
 L 18.40625 64.59375 
 L 9.421875 64.59375 
 z
 " id="DejaVuSans-105"/>
       <path d="M 11.71875 12.40625 
 L 22.015625 12.40625 
 L 22.015625 4 
 L 14.015625 -11.625 
 L 7.71875 -11.625 
 L 11.71875 4 
 z
 " id="DejaVuSans-44"/>
       <path id="DejaVuSans-32"/>
       <path d="M 44.28125 53.078125 
 L 44.28125 44.578125 
 Q 40.484375 46.53125 36.375 47.5 
 Q 32.28125 48.484375 27.875 48.484375 
 Q 21.1875 48.484375 17.84375 46.4375 
 Q 14.5 44.390625 14.5 40.28125 
 Q 14.5 37.15625 16.890625 35.375 
 Q 19.28125 33.59375 26.515625 31.984375 
 L 29.59375 31.296875 
 Q 39.15625 29.25 43.1875 25.515625 
 Q 47.21875 21.78125 47.21875 15.09375 
 Q 47.21875 7.46875 41.1875 3.015625 
 Q 35.15625 -1.421875 24.609375 -1.421875 
 Q 20.21875 -1.421875 15.453125 -0.5625 
 Q 10.6875 0.296875 5.421875 2 
 L 5.421875 11.28125 
 Q 10.40625 8.6875 15.234375 7.390625 
 Q 20.0625 6.109375 24.8125 6.109375 
 Q 31.15625 6.109375 34.5625 8.28125 
 Q 37.984375 10.453125 37.984375 14.40625 
 Q 37.984375 18.0625 35.515625 20.015625 
 Q 33.0625 21.96875 24.703125 23.78125 
 L 21.578125 24.515625 
 Q 13.234375 26.265625 9.515625 29.90625 
 Q 5.8125 33.546875 5.8125 39.890625 
 Q 5.8125 47.609375 11.28125 51.796875 
 Q 16.75 56 26.8125 56 
 Q 31.78125 56 36.171875 55.265625 
 Q 40.578125 54.546875 44.28125 53.078125 
 z
 " id="DejaVuSans-115"/>
      </defs>
      <use xlink:href="#DejaVuSans-116"/>
      <use x="39.208984" xlink:href="#DejaVuSans-105"/>
      <use x="66.992188" xlink:href="#DejaVuSans-109"/>
      <use x="164.404297" xlink:href="#DejaVuSans-101"/>
      <use x="225.927734" xlink:href="#DejaVuSans-44"/>
      <use x="257.714844" xlink:href="#DejaVuSans-32"/>
      <use x="289.501953" xlink:href="#DejaVuSans-115"/>
      <use x="341.601562" xlink:href="#DejaVuSans-101"/>
      <use x="403.125" xlink:href="#DejaVuSans-99"/>
     </g>
    </g>
   </g>
   <g id="line2d_25">
    <path clip-path="url(#p902cfd873e)" d="M 73.832727 128.778772 
 L 103.346777 129.976396 
 L 132.860826 53.568 
 L 162.374876 84.466693 
 L 191.888926 295.248475 
 L 221.402975 295.00895 
 L 250.917025 295.488 
 L 280.431074 295.00895 
 L 309.945124 215.965782 
 L 339.459174 173.569901 
 L 368.973223 156.803168 
 L 398.487273 86.622416 
 " style="fill:none;stroke:#ff0000;stroke-linecap:square;stroke-opacity:0.7;stroke-width:1.5;"/>
    <defs>
     <path d="M -3 3 
 L 3 3 
 L 3 -3 
 L -3 -3 
 z
 " id="m40d9e306aa" style="stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;"/>
    </defs>
    <g clip-path="url(#p902cfd873e)">
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="73.832727" xlink:href="#m40d9e306aa" y="128.778772"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="103.346777" xlink:href="#m40d9e306aa" y="129.976396"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="132.860826" xlink:href="#m40d9e306aa" y="53.568"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="162.374876" xlink:href="#m40d9e306aa" y="84.466693"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="191.888926" xlink:href="#m40d9e306aa" y="295.248475"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="221.402975" xlink:href="#m40d9e306aa" y="295.00895"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="250.917025" xlink:href="#m40d9e306aa" y="295.488"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="280.431074" xlink:href="#m40d9e306aa" y="295.00895"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="309.945124" xlink:href="#m40d9e306aa" y="215.965782"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="339.459174" xlink:href="#m40d9e306aa" y="173.569901"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="368.973223" xlink:href="#m40d9e306aa" y="156.803168"/>
     <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="398.487273" xlink:href="#m40d9e306aa" y="86.622416"/>
    </g>
   </g>
   <g id="patch_3">
    <path d="M 57.6 307.584 
 L 57.6 41.472 
 " style="fill:none;stroke:#000000;stroke-linecap:square;stroke-linejoin:miter;stroke-width:0.8;"/>
   </g>
   <g id="patch_4">
    <path d="M 414.72 307.584 
 L 414.72 41.472 
 " style="fill:none;stroke:#000000;stroke-linecap:square;stroke-linejoin:miter;stroke-width:0.8;"/>
   </g>
   <g id="patch_5">
    <path d="M 57.6 307.584 
 L 414.72 307.584 
 " style="fill:none;stroke:#000000;stroke-linecap:square;stroke-linejoin:miter;stroke-width:0.8;"/>
   </g>
   <g id="patch_6">
    <path d="M 57.6 41.472 
 L 414.72 41.472 
 " style="fill:none;stroke:#000000;stroke-linecap:square;stroke-linejoin:miter;stroke-width:0.8;"/>
   </g>
   <g id="legend_1">
    <g id="patch_7">
     <path d="M 230.468437 64.150125 
 L 407.72 64.150125 
 Q 409.72 64.150125 409.72 62.150125 
 L 409.72 48.472 
 Q 409.72 46.472 407.72 46.472 
 L 230.468437 46.472 
 Q 228.468437 46.472 228.468437 48.472 
 L 228.468437 62.150125 
 Q 228.468437 64.150125 230.468437 64.150125 
 z
 " style="fill:#ffffff;opacity:0.8;stroke:#cccccc;stroke-linejoin:miter;"/>
    </g>
    <g id="line2d_26">
     <path d="M 232.468437 54.570438 
 L 252.468437 54.570438 
 " style="fill:none;stroke:#ff0000;stroke-linecap:square;stroke-opacity:0.7;stroke-width:1.5;"/>
    </g>
    <g id="line2d_27">
     <g>
      <use style="fill:#ff0000;fill-opacity:0.7;stroke:#ff0000;stroke-linejoin:miter;stroke-opacity:0.7;" x="242.468437" xlink:href="#m40d9e306aa" y="54.570438"/>
     </g>
    </g>
    <g id="text_15">
     <!-- 001indinv-apalache-unstable -->
     <g transform="translate(260.468437 58.070438)scale(0.1 -0.1)">
      <defs>
       <path d="M 45.40625 46.390625 
 L 45.40625 75.984375 
 L 54.390625 75.984375 
 L 54.390625 0 
 L 45.40625 0 
 L 45.40625 8.203125 
 Q 42.578125 3.328125 38.25 0.953125 
 Q 33.9375 -1.421875 27.875 -1.421875 
 Q 17.96875 -1.421875 11.734375 6.484375 
 Q 5.515625 14.40625 5.515625 27.296875 
 Q 5.515625 40.1875 11.734375 48.09375 
 Q 17.96875 56 27.875 56 
 Q 33.9375 56 38.25 53.625 
 Q 42.578125 51.265625 45.40625 46.390625 
 z
 M 14.796875 27.296875 
 Q 14.796875 17.390625 18.875 11.75 
 Q 22.953125 6.109375 30.078125 6.109375 
 Q 37.203125 6.109375 41.296875 11.75 
 Q 45.40625 17.390625 45.40625 27.296875 
 Q 45.40625 37.203125 41.296875 42.84375 
 Q 37.203125 48.484375 30.078125 48.484375 
 Q 22.953125 48.484375 18.875 42.84375 
 Q 14.796875 37.203125 14.796875 27.296875 
 z
 " id="DejaVuSans-100"/>
       <path d="M 2.984375 54.6875 
 L 12.5 54.6875 
 L 29.59375 8.796875 
 L 46.6875 54.6875 
 L 56.203125 54.6875 
 L 35.6875 0 
 L 23.484375 0 
 z
 " id="DejaVuSans-118"/>
       <path d="M 4.890625 31.390625 
 L 31.203125 31.390625 
 L 31.203125 23.390625 
 L 4.890625 23.390625 
 z
 " id="DejaVuSans-45"/>
       <path d="M 18.109375 8.203125 
 L 18.109375 -20.796875 
 L 9.078125 -20.796875 
 L 9.078125 54.6875 
 L 18.109375 54.6875 
 L 18.109375 46.390625 
 Q 20.953125 51.265625 25.265625 53.625 
 Q 29.59375 56 35.59375 56 
 Q 45.5625 56 51.78125 48.09375 
 Q 58.015625 40.1875 58.015625 27.296875 
 Q 58.015625 14.40625 51.78125 6.484375 
 Q 45.5625 -1.421875 35.59375 -1.421875 
 Q 29.59375 -1.421875 25.265625 0.953125 
 Q 20.953125 3.328125 18.109375 8.203125 
 z
 M 48.6875 27.296875 
 Q 48.6875 37.203125 44.609375 42.84375 
 Q 40.53125 48.484375 33.40625 48.484375 
 Q 26.265625 48.484375 22.1875 42.84375 
 Q 18.109375 37.203125 18.109375 27.296875 
 Q 18.109375 17.390625 22.1875 11.75 
 Q 26.265625 6.109375 33.40625 6.109375 
 Q 40.53125 6.109375 44.609375 11.75 
 Q 48.6875 17.390625 48.6875 27.296875 
 z
 " id="DejaVuSans-112"/>
       <path d="M 9.421875 75.984375 
 L 18.40625 75.984375 
 L 18.40625 0 
 L 9.421875 0 
 z
 " id="DejaVuSans-108"/>
       <path d="M 8.5 21.578125 
 L 8.5 54.6875 
 L 17.484375 54.6875 
 L 17.484375 21.921875 
 Q 17.484375 14.15625 20.5 10.265625 
 Q 23.53125 6.390625 29.59375 6.390625 
 Q 36.859375 6.390625 41.078125 11.03125 
 Q 45.3125 15.671875 45.3125 23.6875 
 L 45.3125 54.6875 
 L 54.296875 54.6875 
 L 54.296875 0 
 L 45.3125 0 
 L 45.3125 8.40625 
 Q 42.046875 3.421875 37.71875 1 
 Q 33.40625 -1.421875 27.6875 -1.421875 
 Q 18.265625 -1.421875 13.375 4.4375 
 Q 8.5 10.296875 8.5 21.578125 
 z
 M 31.109375 56 
 z
 " id="DejaVuSans-117"/>
      </defs>
      <use xlink:href="#DejaVuSans-48"/>
      <use x="63.623047" xlink:href="#DejaVuSans-48"/>
      <use x="127.246094" xlink:href="#DejaVuSans-49"/>
      <use x="190.869141" xlink:href="#DejaVuSans-105"/>
      <use x="218.652344" xlink:href="#DejaVuSans-110"/>
      <use x="282.03125" xlink:href="#DejaVuSans-100"/>
      <use x="345.507812" xlink:href="#DejaVuSans-105"/>
      <use x="373.291016" xlink:href="#DejaVuSans-110"/>
      <use x="436.669922" xlink:href="#DejaVuSans-118"/>
      <use x="493.224609" xlink:href="#DejaVuSans-45"/>
      <use x="529.308594" xlink:href="#DejaVuSans-97"/>
      <use x="590.587891" xlink:href="#DejaVuSans-112"/>
      <use x="654.064453" xlink:href="#DejaVuSans-97"/>
      <use x="715.34375" xlink:href="#DejaVuSans-108"/>
      <use x="743.126953" xlink:href="#DejaVuSans-97"/>
      <use x="804.40625" xlink:href="#DejaVuSans-99"/>
      <use x="859.386719" xlink:href="#DejaVuSans-104"/>
      <use x="922.765625" xlink:href="#DejaVuSans-101"/>
      <use x="984.289062" xlink:href="#DejaVuSans-45"/>
      <use x="1020.373047" xlink:href="#DejaVuSans-117"/>
      <use x="1083.751953" xlink:href="#DejaVuSans-110"/>
      <use x="1147.130859" xlink:href="#DejaVuSans-115"/>
      <use x="1199.230469" xlink:href="#DejaVuSans-116"/>
      <use x="1238.439453" xlink:href="#DejaVuSans-97"/>
      <use x="1299.71875" xlink:href="#DejaVuSans-98"/>
      <use x="1363.195312" xlink:href="#DejaVuSans-108"/>
      <use x="1390.978516" xlink:href="#DejaVuSans-101"/>
     </g>
    </g>
   </g>
  </g>
 </g>
 <defs>
  <clipPath id="p902cfd873e">
   <rect height="266.112" width="357.12" x="57.6" y="41.472"/>
  </clipPath>
 </defs>
 </svg>
--- a/rust-spec/tendermint-accountability/results/001indinv-apalache-unstable.csv
+++ b/rust-spec/tendermint-accountability/results/001indinv-apalache-unstable.csv
@ -0,0 +1,13 @@
 01:no,02:tool,03:status,04:time_sec,05:depth,05:mem_kb,10:ninit_trans,11:ninit_trans,12:ncells,13:nclauses,14:navg_clause_len
 1,apalache,NoError,704,1,3215424,0,0,217385,1305718,89
 2,apalache,NoError,699,1,3195020,0,0,207969,1341979,88
 3,apalache,NoError,1018,1,4277060,0,0,311798,2028544,101
 4,apalache,NoError,889,1,4080012,0,0,290989,1951616,103
 5,apalache,NoError,9,0,577100,0,0,2045,14655,42
 6,apalache,NoError,10,0,673772,0,0,2913,28213,43
 7,apalache,NoError,8,0,651008,0,0,2214,17077,44
 8,apalache,NoError,10,0,683188,0,0,3082,32651,45
 9,apalache,NoError,340,0,3053848,0,0,196943,889859,108
 10,apalache,NoError,517,0,6424536,0,0,2856378,3802779,34
 11,apalache,NoError,587,0,4028516,0,0,284369,1343296,128
 12,apalache,NoError,880,0,7881148,0,0,4382556,5778072,38
--- a/rust-spec/tendermint-accountability/run.sh
+++ b/rust-spec/tendermint-accountability/run.sh
@ -0,0 +1,9 @@
 #!/bin/sh
 #
 # The script to run all experiments at once

 export SCRIPTS_DIR=~/devl/apalache-tests/scripts
 export BUILDS="unstable"
 export BENCHMARK=001indinv-apalache
 export RUN_SCRIPT=./run-all.sh # alternatively, use ./run-parallel.sh
 make -e -f ~/devl/apalache-tests/Makefile.common