Testgen external commands

testgen/jsonatr-lib/apalache-tendermint.json

@@ -0,0 +1,150 @@
+{
+  "description": "Transformers for Apalache counterexamples (CEs) with Tendermint blockchains",
+  "use": [
+    "tendermint.json"
+  ],
+  "input": [
+    {
+      "name": "first_state",
+      "description": "extract the first state from Apalache CE",
+      "kind": "INLINE",
+      "source": "$.declarations[1].body.and | unwrap"
+    },
+    {
+      "name": "last_state",
+      "description": "extract the last state from Apalache CE",
+      "kind": "INLINE",
+      "source": "$.declarations[-2].body.and | unwrap"
+    },
+    {
+      "name": "history",
+      "description": "extract the history from the last state of Apalache CE",
+      "kind": "INLINE",
+      "source": "$last_state..[?(@.eq == 'history')].arg.atat..arg.record"
+    },
+    {
+      "name": "states",
+      "description": "extract all state from Apalache CE",
+      "kind": "INLINE",
+      "source": "$.declarations[1:-1].body.and"
+    },
+    {
+      "name": "lightblock_commits",
+      "description": "extract commits from a LightClient block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'Commits')].value..str"
+    },
+    {
+      "name": "block_validators",
+      "description": "extract validators from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'VS')].value..str"
+    },
+    {
+      "name": "block_next_validators",
+      "description": "extract next validators from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'NextVS')].value..str"
+    },
+    {
+      "name": "block_height",
+      "description": "extract height from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'height')].value | unwrap"
+    },
+    {
+      "name": "block_time",
+      "description": "extract time from a block of Apalache CE",
+      "kind": "INLINE",
+      "source": "$..[?(@.key.str == 'time')].value | unwrap"
+    },
+    {
+      "name": "id_to_validator",
+      "description": "transform an identifier into a validator expected by `tendermint-testgen validator`",
+      "kind": "INLINE",
+      "source": {
+        "id": "$",
+        "voting_power": 50
+      }
+    },
+    {
+      "name": "id_to_vote",
+      "description": "transform an identifier into a vote expected by `tendermint-testgen vote`",
+      "kind": "INLINE",
+      "source": {
+        "validator": "$ | id_to_validator",
+        "header": "$header"
+      }
+    },
+    {
+      "name": "block_to_header",
+      "description": "transform a block from Apalache CE into a header expected by `tendermint-testgen header`",
+      "kind": "INLINE",
+      "source": {
+        "validators": "$ | block_validators | map(id_to_validator)",
+        "next_validators": "$ | block_next_validators | map(id_to_validator)",
+        "height": "$ | block_height",
+        "time": "$ | block_time"
+      }
+    },
+    {
+      "name": "block_to_commit",
+      "description": "transform a block from Apalache CE into a commit expected by `tendermint-testgen commit`",
+      "kind": "INLINE",
+      "let": {
+        "header": "$ | block_to_header"
+      },
+      "source": {
+        "header": "$header",
+        "votes": "$ | lightblock_commits | map(id_to_vote)"
+      }
+    },
+    {
+      "name": "ids_to_validators",
+      "description": "transform a non-empty array of identifiers into Tendermint validators",
+      "kind": "INLINE",
+      "source": "$ | map(id_to_validator) | map(tendermint_validator)"
+    },
+    {
+      "name": "empty_array",
+      "description": "just an empty array",
+      "kind": "INLINE",
+      "source": []
+    },
+    {
+      "name": "first_validator",
+      "description": "extract first validator from a non-empty array of identifiers",
+      "kind": "INLINE",
+      "source": "$[0] | unwrap | id_to_validator | tendermint_validator"
+    },
+    {
+      "name": "const_id",
+      "description": "constant identifier",
+      "kind": "INLINE",
+      "source": "a"
+    },    {
+      "name": "fixed_validator",
+      "description": "extract first validator from a non-empty array of identifiers",
+      "kind": "INLINE",
+      "source": "$const_id | id_to_validator | tendermint_validator"
+    },
+    {
+      "name": "ids_to_validator_set",
+      "description": "transform an array of identifiers into a JSON-encoded Tendermint validator set",
+      "kind": "INLINE",
+      "source": {
+        "validators": "$ | ifelse(ids_to_validators,empty_array)",
+        "proposer": "$ | ifelse(first_validator,fixed_validator)"
+      }
+    },
+    {
+      "name": "block_to_signed_header",
+      "description": "transform a block from Apalache CE into a JSON-encoded Tendermint signed header",
+      "kind": "INLINE",
+      "source": {
+        "header": "$ | block_to_header | tendermint_header",
+        "commit": "$ | block_to_commit | tendermint_commit"
+      }
+    }
+  ]
+}

testgen/jsonatr-lib/apalache_to_lite_test.json

@@ -0,0 +1,42 @@
+{
+  "description": "Transform an Apalache counterexample into a Tendermint LightClient test",
+  "use": [
+    "unix.json",
+    "apalache-tendermint.json"
+  ],
+  "input": [
+    {
+      "name": "block_to_initial_block",
+      "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint initial light block",
+      "kind": "INLINE",
+      "source": {
+        "signed_header": "$ | block_to_signed_header",
+        "next_validator_set": "$ | block_next_validators | ids_to_validator_set",
+        "trusting_period": "1400000000000",
+        "now": "$utc_timestamp"
+      }
+    },
+    {
+      "name": "state_to_lite_block_verdict",
+      "description": "transforms a block from Apalache CE into a JSON-encoded Tendermint light block",
+      "kind": "INLINE",
+      "let": {
+        "block": "$..[?(@.key.str == 'current')].value"
+      },
+      "source": {
+        "block": {
+          "signed_header": "$block | block_to_signed_header",
+          "validator_set": "$block | block_validators | ids_to_validator_set",
+          "next_validator_set": "$block | block_next_validators | ids_to_validator_set"
+        },
+        "now": "$..[?(@.key.str == 'now')].value | unwrap | tendermint_time",
+        "verdict": "$..[?(@.key.str == 'verdict')].value.str | unwrap"
+      }
+    }
+  ],
+  "output": {
+    "description": "auto-generated from Apalache counterexample",
+    "initial": "$history[0]..[?(@.key.str == 'current')].value | block_to_initial_block",
+    "input": "$history[1:] | map(state_to_lite_block_verdict)"
+  }
+}

testgen/jsonatr-lib/tendermint.json

@@ -0,0 +1,31 @@
+{
+  "description": "Transformers for generating Tendermint datastructures",
+  "prerequisites": "add tendermint-testgen to your $PATH",
+  "input": [
+    {
+      "name": "tendermint_validator",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin validator"
+    },
+    {
+      "name": "tendermint_header",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin header"
+    },
+    {
+      "name": "tendermint_commit",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin commit"
+    },
+    {
+      "name": "tendermint_vote",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin vote"
+    },
+    {
+      "name": "tendermint_time",
+      "kind": "COMMAND",
+      "source": "tendermint-testgen --stdin time"
+    }
+  ]
+}

testgen/jsonatr-lib/unix.json

@@ -0,0 +1,29 @@
+{
+  "description": "Useful external commands",
+  "input": [
+    {
+      "name": "date",
+      "kind": "COMMAND",
+      "source": "date -I",
+      "stdin": false
+    },
+    {
+      "name": "utc_timestamp",
+      "kind": "COMMAND",
+      "source": "date --utc +%FT%H:%M:%S.%NZ",
+      "stdin": false
+    },
+    {
+      "name": "utc_timestamp_hour_ago",
+      "kind": "COMMAND",
+      "source": "date --utc +%FT%H:%M:%S.%NZ --date '-1 hour'",
+      "stdin": false
+    },
+    {
+      "name": "utc_timestamp_2hours_ago",
+      "kind": "COMMAND",
+      "source": "date --utc +%FT%H:%M:%S.%NZ --date '-2 hour'",
+      "stdin": false
+    }
+  ]
+}

testgen/src/apalache.rs

@@ -0,0 +1,122 @@
+use crate::{command::*, tester::TestEnv};
+use serde::{Deserialize, Serialize};
+use std::io;
+
+#[derive(Deserialize, Clone, Debug)]
+pub struct ApalacheTestBatch {
+    pub description: String,
+    pub model: String,
+    pub length: Option<u64>,
+    pub timeout: Option<u64>,
+    pub tests: Vec<String>,
+}
+
+#[derive(Serialize, Deserialize, Clone, Debug)]
+pub struct ApalacheTestCase {
+    pub model: String,
+    pub test: String,
+    pub length: Option<u64>,
+    pub timeout: Option<u64>,
+}
+
+pub enum ApalacheRun {
+    /// Apalache has found a counterexample
+    Counterexample(CommandRun),
+    /// Apalache has not found a counterexample up to specified length bound
+    NoCounterexample(CommandRun),
+    /// Apalache has found a deadlock
+    Deadlock(CommandRun),
+    /// Apalache model checking run failed (e.g. a parsing error)
+    ModelError(CommandRun),
+    /// Apalache returned an unknown error code
+    Unknown(CommandRun),
+    /// The tool has reached the specified timeout without producing an answer
+    Timeout(CommandRun),
+}
+
+impl ApalacheRun {
+    pub fn message(&self) -> &str {
+        match self {
+            ApalacheRun::Counterexample(_) => "Apalache has generated a counterexample",
+            ApalacheRun::NoCounterexample(_) => "Apalache failed to generate a counterexample; consider increasing the length bound, or changing your test",
+            ApalacheRun::Deadlock(_) => "Apalache has found a deadlock; please inspect your model and test",
+            ApalacheRun::ModelError(_) => "Apalache failed to process the model; please check it",
+            ApalacheRun::Unknown(_) => "Apalache has generated an unknown outcome; please contact Apalache developers",
+            ApalacheRun::Timeout(_) => "Apalache failed to generate a counterexample within given time; consider increasing the timeout, or changing your test",
+        }
+    }
+}
+
+pub fn run_apalache_test(dir: &str, test: ApalacheTestCase) -> io::Result<ApalacheRun> {
+    let inv = format!("{}Inv", test.test);
+
+    // Mutate the model: negate the test assertion to get the invariant to check
+    let mutation_failed = || {
+        io::Error::new(
+            io::ErrorKind::InvalidInput,
+            "failed to mutate the model and add invariant",
+        )
+    };
+    let env = TestEnv::new(dir).ok_or_else(mutation_failed)?;
+    let model = env.read_file(&test.model).unwrap();
+    let mut new_model = String::new();
+    for line in model.lines() {
+        if line.starts_with(&inv) {
+            // invariant already present; skip mutation
+            new_model.clear();
+            break;
+        }
+        if line.starts_with("======") {
+            new_model += &format!("{} == ~{}\n", inv, test.test);
+        }
+        new_model += line;
+        new_model += "\n";
+    }
+    if !new_model.is_empty() {
+        env.write_file(&test.model, &new_model)
+            .ok_or_else(mutation_failed)?;
+    }
+
+    // Run Apalache, and process the result
+    let mut cmd = Command::new();
+    if let Some(timeout) = test.timeout {
+        cmd.program("timeout");
+        cmd.arg(&timeout.to_string());
+        cmd.arg("apalache-mc");
+    } else {
+        cmd.program("apalache-mc");
+    }
+    cmd.arg("check");
+    cmd.arg_from_parts(vec!["--inv=", &inv]);
+    if let Some(length) = test.length {
+        cmd.arg_from_parts(vec!["--length=", &length.to_string()]);
+    }
+    cmd.arg(&test.model);
+    if !dir.is_empty() {
+        cmd.current_dir(dir);
+    }
+    match cmd.spawn() {
+        Ok(run) => {
+            if run.status.success() {
+                if run.stdout.contains("The outcome is: NoError") {
+                    Ok(ApalacheRun::NoCounterexample(run))
+                } else if run.stdout.contains("The outcome is: Error") {
+                    Ok(ApalacheRun::Counterexample(run))
+                } else if run.stdout.contains("The outcome is: Deadlock") {
+                    Ok(ApalacheRun::Deadlock(run))
+                } else {
+                    Ok(ApalacheRun::Unknown(run))
+                }
+            } else if let Some(code) = run.status.code() {
+                match code {
+                    99 => Ok(ApalacheRun::ModelError(run)),
+                    124 => Ok(ApalacheRun::Timeout(run)),
+                    _ => Ok(ApalacheRun::Unknown(run)),
+                }
+            } else {
+                Ok(ApalacheRun::Timeout(run))
+            }
+        }
+        Err(e) => Err(e),
+    }
+}