[trust-quorum] tla: download jar, add check.sh, and add a no-crash cfg exposing a model bug

dev-tools/downloader/src/lib.rs

@@ -34,6 +34,8 @@ const BUILDOMAT_URL: &'static str =
 const CARGO_HACK_URL: &'static str =
     "https://github.com/taiki-e/cargo-hack/releases/download";
 const MACOS_AARCH64_SERIES: &'static str = "macos-aarch64";
+const TLA2TOOLS_URL: &'static str =
+    "https://github.com/tlaplus/tlaplus/releases/download";
 
 const RETRY_ATTEMPTS: usize = 3;
 
@@ -78,6 +80,9 @@ enum Target {
     /// SoftNPU, an admin program (scadm) and a pre-compiled P4 program.
     Softnpu,
 
+    /// TLA+ tools jar (`tla2tools.jar`), used by `trust-quorum/tla/check.sh`.
+    Tla2tools,
+
     /// Transceiver Control binary
     TransceiverControl,
 }
@@ -145,6 +150,7 @@ pub async fn run_cmd(args: DownloadArgs) -> Result<()> {
                     Target::MaghemiteMgd => downloader.download_maghemite_mgd().await,
                     Target::MaghemiteDdmd => downloader.download_maghemite_ddmd().await,
                     Target::Softnpu => downloader.download_softnpu().await,
+                    Target::Tla2tools => downloader.download_tla2tools().await,
                     Target::TransceiverControl => {
                         downloader.download_transceiver_control().await
                     }
@@ -1046,6 +1052,32 @@ impl Downloader<'_> {
         Ok(())
     }
 
+    async fn download_tla2tools(&self) -> Result<()> {
+        let download_dir = self.output_dir.join("downloads");
+        let destination_dir = self.output_dir.join("tla2tools");
+
+        let checksums =
+            KvFile::read(self.versions_dir.join("tla2tools_checksums")).await?;
+        let checksum = checksums.get_sha256_value("CIDL_SHA256")?;
+
+        let version = self.read_version_file("tla2tools_version").await?;
+        let jar_url = format!("{TLA2TOOLS_URL}/v{version}/tla2tools.jar");
+
+        tokio::fs::create_dir_all(&download_dir).await?;
+        tokio::fs::create_dir_all(&destination_dir).await?;
+
+        let download_path = download_dir.join("tla2tools.jar");
+        download_file_and_verify(&self.log, &download_path, &jar_url, checksum)
+            .await?;
+
+        let dest = destination_dir.join("tla2tools.jar");
+        tokio::fs::copy(&download_path, &dest).await.with_context(|| {
+            format!("Failed to copy {download_path} to {dest}")
+        })?;
+
+        Ok(())
+    }
+
     async fn download_transceiver_control(&self) -> Result<()> {
         let destination_dir = self.output_dir.join("transceiver-control");
         let download_dir = self.output_dir.join("downloads");

tools/tla2tools_checksums

@@ -0,0 +1 @@
+CIDL_SHA256="936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88"

tools/tla2tools_version

@@ -0,0 +1 @@
+1.7.4

trust-quorum/tla/check.sh

@@ -0,0 +1,125 @@
+#!/usr/bin/env bash
+# This Source Code Form is subject to the terms of the Mozilla Public
+# License, v. 2.0. If a copy of the MPL was not distributed with this
+# file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+# TLA+ check script.
+#
+# This script runs all, or the defined, configurations through TLC, and compares
+# TLC's exit status with the table below.
+#
+# The exit codes are:
+#
+# * 0: the properties are satisfied.
+# * 12: safety violation.
+# * 13: temporal/action violation.
+#
+# A non-zero entry indicates a configuration that is expected to fail. This
+# could either be an expected failure (i.e., a precondition which we know does
+# not satisfy the properties), or a current issue that a subsequent commit will
+# fix.
+set -euo pipefail
+
+cd "$(dirname "$0")"
+
+REPO_ROOT="$(cd ../.. && pwd)"
+DEFAULT_JAR="$REPO_ROOT/out/tla2tools/tla2tools.jar"
+
+usage() {
+    cat <<USAGE
+usage: $0 [CFG...]
+
+Runs every cfg in the expectation table (or only the CFGs given) through TLC
+and checks the exit status.
+
+Environment:
+  TLA2TOOLS_JAR  path to tla2tools.jar
+                 (default: $DEFAULT_JAR)
+  TLC_WORKERS    passed to TLC's -workers (default: auto)
+
+To download the pinned tla2tools.jar to the default location, run
+\`cargo xtask download tla2tools\` from the repository root.
+
+Logs and TLC state directories go under the directory printed at the start.
+USAGE
+}
+
+if [[ "${1:-}" == "-h" || "${1:-}" == "--help" ]]; then
+    usage
+    exit 0
+fi
+
+if ! command -v java >/dev/null 2>&1; then
+    echo "error: java not found in PATH (TLC requires a Java runtime)" >&2
+    exit 2
+fi
+
+TLA2TOOLS_JAR="${TLA2TOOLS_JAR:-$DEFAULT_JAR}"
+if [[ ! -f "$TLA2TOOLS_JAR" ]]; then
+    echo "error: TLA+ tools jar not found at $TLA2TOOLS_JAR" >&2
+    if [[ "$TLA2TOOLS_JAR" == "$DEFAULT_JAR" ]]; then
+        echo "To download it, run \`cargo xtask download tla2tools\` from $REPO_ROOT." >&2
+    else
+        echo "Check TLA2TOOLS_JAR, or unset it to use $DEFAULT_JAR." >&2
+    fi
+    exit 2
+fi
+echo "tla2tools: $TLA2TOOLS_JAR"
+
+WORKERS="${TLC_WORKERS:-auto}"
+
+# cfg  module  expected-exit-status
+EXPECTED=(
+    "trust_quorum.cfg          trust_quorum  0"
+    "trust_quorum_nocrash.cfg  trust_quorum  13"
+)
+
+selected=("$@")
+want() {
+    [[ ${#selected[@]} -eq 0 ]] && return 0
+    local s
+    for s in "${selected[@]}"; do
+        [[ "$s" == "$1" ]] && return 0
+    done
+    return 1
+}
+
+outdir="$(mktemp -d "${TMPDIR:-/tmp}/tlc-check.XXXXXX")"
+echo "output: $outdir"
+
+failures=0
+ran=0
+for entry in "${EXPECTED[@]}"; do
+    read -r cfg module expected <<<"$entry"
+    want "$cfg" || continue
+    ran=$((ran + 1))
+    name="${cfg%.cfg}"
+    log="$outdir/$name.log"
+    start=$SECONDS
+    set +e
+    java -XX:+UseParallelGC -cp "$TLA2TOOLS_JAR" tlc2.TLC \
+        -workers "$WORKERS" \
+        -metadir "$outdir/$name.states" \
+        -config "$cfg" "$module.tla" >"$log" 2>&1
+    actual=$?
+    set -e
+    elapsed=$((SECONDS - start))
+    if [[ "$actual" == "$expected" ]]; then
+        status="ok"
+    else
+        status="FAIL"
+        failures=$((failures + 1))
+    fi
+    printf '%-4s %-28s expected %-3s got %-3s %4ds  %s\n' \
+        "$status" "$cfg" "$expected" "$actual" "$elapsed" "$log"
+done
+
+if [[ $ran -eq 0 ]]; then
+    echo "error: no cfg matched: ${selected[*]}" >&2
+    exit 2
+fi
+
+if [[ $failures -ne 0 ]]; then
+    echo "$failures of $ran cfg(s) did not produce the expected exit status" >&2
+    exit 1
+fi

trust-quorum/tla/trust_quorum.tla

@@ -23,7 +23,7 @@
       the state space.
 *)
 
-EXTENDS Integers, FiniteSets, TLC, TLCExt
+EXTENDS Integers, FiniteSets, TLC
 
 CONSTANTS
     (* The set of trust quorum nodes *)
@@ -249,7 +249,7 @@ Msgs ==
    care which message they receive first, but whether they have received enough
    messages. In any case, even if there were a few concurrency bugs that could
    possibly be exposed via use of `\E \in msgs`, it would still be too expensive
-   to use. 
+   to use.
 
    Therefore, we instead filter down the set of valid messages, and choose one
    one from the set. The `valid(_)` operator must ensure that the same message
@@ -302,7 +302,7 @@ UpAndUnlocked(id) ==
        \/ nodeOp[id] = "Idle"
        \/ nodeOp[id] = "CoordinatePrepare"
        \/ nodeOp[id] = "CoordinateCollectShares"
-       \/ nodeOp[id] = "ComputeShare" 
+       \/ nodeOp[id] = "ComputeShare"
 
 ChooseCoordinator(members) ==
     IF nexus.last_committed_config = NONE THEN
@@ -411,7 +411,14 @@ CommittedNodesHaveShares ==
 
 -----------------------------------------------------------------------------
 (* Temporal properties *)
-AllNodesUnlock == <>[](\A id \in nexus.config.members: nodeOp[id] # "Unlock") 
+AllNodesUnlock == <>[](\A id \in nexus.config.members: nodeOp[id] # "Unlock")
+
+\* This is currently expected to FAIL under trust_quorum_nocrash.cfg, because
+\* RecvCommit never fires for the coordinator (it stays in CoordinatePrepare),
+\* so NexusRecvCommitAck never reaches Idle and epoch 2 never starts.
+\* trust_quorum.cfg only gets there because n1 is in CRASHSET and commits after
+\* restarting.
+ReconfigurationStarts == <>(nexus.config.epoch = 2)
 
 -----------------------------------------------------------------------------
 (* The initial state predicate that sets the initial state of the system. *)
@@ -664,7 +671,7 @@ RecvPrepare(id) ==
                      all the other nodes transiently reboot, we'd mask the retries
                      that we get for free by keeping all the messages ever sent
                      in `msgs`.
-   
+
                     This is one of the few places where explict retries would be
                     handy, but the whole spec would have to change again to support
                     that. *)
@@ -774,7 +781,7 @@ RecvGetConfig(id) ==
                    /\ \/ nodes[m.from] = NONE
                       \/ /\ nodes[m.from] # NONE
                          /\ nodes[m.from].config.epoch # m.epoch
-   
+
       m == Recv(valid)
   IN
     /\ m # NONE
@@ -797,7 +804,7 @@ RecvGetShare(id) ==
                      \* Commit occurred, but this node hasn't learned of it yet.
                      \* It must return the share so a crashed node that did learn
                      \* can unlock.
-                     \/ /\ m.epoch = nodes[id].config.epoch 
+                     \/ /\ m.epoch = nodes[id].config.epoch
                         /\ m.from \in nodes[id].config.members
       m == Recv(valid)
   IN

trust-quorum/tla/trust_quorum_nocrash.cfg

@@ -0,0 +1,35 @@
+\* SPECIFICATION
+\* Uncomment the previous line and provide the specification name if it's declared
+\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
+
+CONSTANTS
+    NONE = NONE
+    n1 = n1
+    n2 = n2
+    n3 = n3
+    n4 = n4
+    n5 = n5
+    NODES = {n1,n2,n3,n4,n5}
+    ALL_CONFIGS = AllConfigs
+    MAX_EPOCH = 3
+    MAX_CRASHES_PER_NODE = 1
+    MAX_NEXUS_CRASHES = 1
+    CRASHSET = {}
+
+PROPERTY
+  AllNodesUnlock
+  ReconfigurationStarts
+
+SPECIFICATION FairSpec
+
+
+INVARIANTS
+TypeOK
+NexusCoordinatorIsPartOfConfig
+NodeConfigsMatchNexus
+NodesThatHaveAckedCommitsHaveActuallyCommitted
+LastCommittedConfigLessThanEqualConfig
+CommittedNodesHaveShares
+
+CONSTRAINT
+MaxEpochConstraint