diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index 86bf4fede..8d424afc1 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -15,6 +15,7 @@ on:
jobs:
coverage:
+ name: Integration
runs-on: ubuntu-latest
defaults:
run:
@@ -38,7 +39,7 @@ jobs:
- name: Install cargo-llvm-cov
uses: taiki-e/install-action@cargo-llvm-cov
- name: Generate code coverage
- run: cargo llvm-cov nextest --all-features --workspace --lcov --output-path lcov.info
+ run: cargo llvm-cov nextest --workspace --exclude malachite-itf --all-features --lcov --output-path lcov.info
- name: Generate text report
run: cargo llvm-cov report
- name: Upload coverage to Codecov
@@ -46,4 +47,41 @@ jobs:
with:
token: ${{ secrets.CODECOV_TOKEN }}
files: Code/lcov.info
+ flags: integration
+ fail_ci_if_error: true
+
+ mbt-coverage:
+ name: MBT
+ runs-on: ubuntu-latest
+ defaults:
+ run:
+ working-directory: Code
+ env:
+ CARGO_TERM_COLOR: always
+ 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:
+ toolchain: nightly
+ components: llvm-tools-preview
+ - name: Install cargo-nextest
+ uses: taiki-e/install-action@cargo-nextest
+ - name: Install cargo-llvm-cov
+ uses: taiki-e/install-action@cargo-llvm-cov
+ - name: Generate code coverage
+ run: cargo llvm-cov nextest -p malachite-itf --all-features --lcov --output-path lcov.info
+ - name: Generate text report
+ run: cargo llvm-cov report
+ - name: Upload coverage to Codecov
+ uses: codecov/codecov-action@v3
+ with:
+ token: ${{ secrets.CODECOV_TOKEN }}
+ files: Code/lcov.info
+ flags: mbt
fail_ci_if_error: true
diff --git a/Code/.cargo/config.toml b/Code/.cargo/config.toml
new file mode 100644
index 000000000..9ab3fa3a0
--- /dev/null
+++ b/Code/.cargo/config.toml
@@ -0,0 +1,2 @@
+[alias]
+mbt = "nextest run -p malachite-itf --all-features"
diff --git a/Code/itf/src/consensus.rs b/Code/itf/src/consensus.rs
deleted file mode 100644
index 2bb430b6a..000000000
--- a/Code/itf/src/consensus.rs
+++ /dev/null
@@ -1,178 +0,0 @@
-use num_bigint::BigInt;
-use serde::Deserialize;
-use std::collections::HashMap;
-
-use crate::deserializers as de;
-
-pub type Address = String;
-pub type Value = String;
-pub type Step = String;
-pub type Round = BigInt;
-pub type Height = BigInt;
-
-#[derive(Clone, Debug, Deserialize)]
-pub enum Timeout {
- #[serde(rename = "timeoutPrevote")]
- Prevote,
-
- #[serde(rename = "timeoutPrecommit")]
- Precommit,
-
- #[serde(rename = "timeoutPropose")]
- Propose,
-}
-
-#[derive(Clone, Debug, Deserialize)]
-pub struct State {
- pub system: System,
-
- #[serde(rename = "_Event")]
- pub event: Event,
-
- #[serde(rename = "_Result")]
- pub result: Result,
-}
-
-#[derive(Clone, Debug, Deserialize)]
-pub struct System(HashMap
);
-
-#[derive(Clone, Debug, Deserialize)]
-#[serde(tag = "name")]
-pub enum Event {
- Initial,
- NewRound {
- height: Height,
- round: Round,
- },
- Proposal {
- height: Height,
- round: Round,
- value: Value,
- },
- ProposalAndPolkaAndValid {
- height: Height,
- round: Round,
- value: Value,
- },
- ProposalAndCommitAndValid {
- height: Height,
- round: Round,
- value: Value,
- },
- NewHeight {
- height: Height,
- round: Round,
- },
- NewRoundProposer {
- height: Height,
- round: Round,
- value: Value,
- },
- PolkaNil {
- height: Height,
- round: Round,
- value: Value,
- },
- PolkaAny {
- height: Height,
- round: Round,
- value: Value,
- },
- PrecommitAny {
- height: Height,
- round: Round,
- value: Value,
- },
- TimeoutPrevote {
- height: Height,
- round: Round,
- },
- TimeoutPrecommit {
- height: Height,
- round: Round,
- value: Value,
- },
- TimeoutPropose {
- height: Height,
- round: Round,
- value: Value,
- },
- ProposalInvalid {
- height: Height,
- round: Round,
- },
-}
-
-#[derive(Clone, Debug, Deserialize)]
-#[serde(rename_all = "camelCase")]
-pub struct Result {
- pub name: String,
- #[serde(deserialize_with = "de::proposal_or_none")]
- pub proposal: Option,
- #[serde(deserialize_with = "de::vote_message_or_none")]
- pub vote_message: Option,
- #[serde(deserialize_with = "de::empty_string_as_none")]
- pub timeout: Option,
- #[serde(deserialize_with = "de::empty_string_as_none")]
- pub decided: Option,
- #[serde(deserialize_with = "de::minus_one_as_none")]
- pub skip_round: Option,
-}
-
-#[derive(Clone, Debug, Deserialize, PartialEq, Eq)]
-#[serde(rename_all = "camelCase")]
-pub struct Proposal {
- pub src: Address,
- pub height: Height,
- pub round: Round,
- pub proposal: Value,
- pub valid_round: Round,
-}
-
-impl Proposal {
- pub fn is_empty(&self) -> bool {
- self.src.is_empty()
- && self.proposal.is_empty()
- && self.height == BigInt::from(-1)
- && self.round == BigInt::from(-1)
- && self.valid_round == BigInt::from(-1)
- }
-}
-
-#[derive(Clone, Debug, Deserialize)]
-#[serde(rename_all = "camelCase")]
-pub struct VoteMessage {
- pub src: Address,
- pub height: Height,
- pub round: Round,
- pub step: Step,
- pub id: Value,
-}
-
-impl VoteMessage {
- pub fn is_empty(&self) -> bool {
- self.src.is_empty()
- && self.id.is_empty()
- && self.height == BigInt::from(-1)
- && self.round == BigInt::from(-1)
- && self.step.is_empty()
- }
-}
-
-#[derive(Clone, Debug, Deserialize)]
-#[serde(rename_all = "camelCase")]
-pub struct ConsensusState {
- pub p: Address,
- pub height: Height,
- pub round: Round,
- pub step: Step,
-
- #[serde(deserialize_with = "de::minus_one_as_none")]
- pub locked_round: Option,
- #[serde(deserialize_with = "de::empty_string_as_none")]
- pub locked_value: Option,
- #[serde(deserialize_with = "de::minus_one_as_none")]
- pub valid_round: Option,
- #[serde(deserialize_with = "de::empty_string_as_none")]
- pub valid_value: Option,
-}
diff --git a/Code/itf/src/deserializers.rs b/Code/itf/src/deserializers.rs
deleted file mode 100644
index 53231f40d..000000000
--- a/Code/itf/src/deserializers.rs
+++ /dev/null
@@ -1,53 +0,0 @@
-use num_bigint::BigInt;
-use serde::de::IntoDeserializer;
-use serde::Deserialize;
-
-use crate::consensus::{Proposal, VoteMessage};
-
-pub(crate) fn empty_string_as_none<'de, D, T>(de: D) -> Result