Merge branch 'main' into josef/testcoverage

.github/dependabot.yml

@@ -0,0 +1,8 @@
+# https://docs.github.com/github/administering-a-repository/configuration-options-for-dependency-updates
+
+version: 2
+updates:
+  - package-ecosystem: "cargo"
+    directory: "/Code"
+    schedule:
+      interval: "weekly"

.github/workflows/coverage.yml

@@ -5,9 +5,13 @@ on:
     branches: main
     paths:
       - Code/**
+      - Specs/Quint/**
+      - .github/workflows/coverage.yml
   pull_request:
     paths:
       - Code/**
+      - Specs/Quint/**
+      - .github/workflows/coverage.yml
 
 jobs:
   coverage:
@@ -20,6 +24,10 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
       - name: Setup Rust toolchain
         uses: actions-rust-lang/setup-rust-toolchain@v1
         with:

.github/workflows/mbt.yml

@@ -0,0 +1,45 @@
+name: MBT
+on:
+  push:
+    branches:
+      - main
+    paths:
+      - Specs/Quint/**
+      - Code/**
+      - .github/workflows/mbt.yml
+  pull_request:
+    paths:
+      - Specs/Quint/**
+      - Code/**
+      - .github/workflows/mbt.yml
+
+jobs:
+  gen-and-exec-traces:
+    name: Generate and execute random traces
+    runs-on: ubuntu-latest
+    env:
+      CARGO_INCREMENTAL: 0
+      CARGO_PROFILE_DEV_DEBUG: 1
+      CARGO_PROFILE_RELEASE_DEBUG: 1
+      RUST_BACKTRACE: short
+      CARGO_NET_RETRY: 10
+      RUSTUP_MAX_RETRIES: 10
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - name: Setup Rust toolchain
+        uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Install cargo-nextest
+        uses: taiki-e/install-action@cargo-nextest
+      - name: Build code
+        working-directory: Code/itf
+        run: cargo nextest run --workspace --all-features --no-run
+      - name: Current time as random seed for Quint
+        run: echo "QUINT_SEED=$(date +%s)" >> $GITHUB_ENV
+      - name: Run tests from traces (with random seed)
+        working-directory: Code/itf
+        run: cargo nextest run --workspace --all-features test_itf

.github/workflows/quint.yml

@@ -33,4 +33,3 @@ jobs:
           node-version: "18"
       - run: npm install -g @informalsystems/quint
       - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt
-

.github/workflows/rust.yml

@@ -5,9 +5,13 @@ on:
     branches: main
     paths:
       - Code/**
+      - Specs/Quint/**
+      - .github/workflows/rust.yml
   pull_request:
     paths:
       - Code/**
+      - Specs/Quint/**
+      - .github/workflows/rust.yml
 
 env:
   CARGO_INCREMENTAL: 0
@@ -27,6 +31,10 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
       - name: Setup Rust toolchain
         uses: actions-rust-lang/setup-rust-toolchain@v1
       - name: Install cargo-nextest
@@ -51,7 +59,7 @@ jobs:
         with:
           token: ${{secrets.GITHUB_TOKEN}}
           args: --all-features --all-targets --manifest-path Code/Cargo.toml
- 
+
   fmt:
     name: Formatting
     runs-on: ubuntu-latest

Code/Cargo.toml

@@ -19,10 +19,13 @@ publish      = false
 
 [workspace.dependencies]
 async-trait       = "0.1"
-futures           = "0.3"
 ed25519-consensus = "2.1.0"
-itf               = "0.1.2"
+futures           = "0.3"
+glob              = "0.3.0"
+itf               = "0.2.1"
+num-bigint        = "0.4.4"
 rand              = { version = "0.8.5", features = ["std_rng"] }
 serde             = "1.0"
+serde_json        = "1.0"
 sha2              = "0.10.8"
 signature         = "2.1.0"

Code/common/src/round.rs

@@ -17,7 +17,6 @@ pub enum Round {
 impl Round {
     /// The initial, zero round.
     pub const INITIAL: Round = Round::new(0);
-    pub const NIL: Round = Round::new(-1);
 
     /// Create a new round.
     ///
@@ -42,12 +41,12 @@ impl Round {
         }
     }
 
-    /// Wether the round is defined, ie. `Round::Some(r)` where `r >= 0`.
+    /// Whether the round is defined, ie. `Round::Some(r)` where `r >= 0`.
     pub fn is_defined(&self) -> bool {
         matches!(self, Round::Some(r) if *r >= 0)
     }
 
-    /// Wether the round is `Round::Nil`.
+    /// Whether the round is `Round::Nil`.
     pub fn is_nil(&self) -> bool {
         matches!(self, Round::Nil)
     }

Code/common/src/validator_set.rs

@@ -37,6 +37,7 @@ where
 /// A validator set is a collection of validators.
 pub trait ValidatorSet<Ctx>
 where
+    Self: Clone + Debug,
     Ctx: Context,
 {
     /// The total voting power of the validator set.