Merge and make first pass changes for new events

.github/workflows/coverage.yml

@@ -2,7 +2,7 @@ name: Coverage
 
 on:
   push:
-    branches: master
+    branches: main
     paths:
       - Code/**
   pull_request:
@@ -12,6 +12,9 @@ on:
 jobs:
   coverage:
     runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: Code
     env:
       CARGO_TERM_COLOR: always
     steps:
@@ -26,10 +29,8 @@ jobs:
       - name: Install cargo-llvm-cov
         uses: taiki-e/install-action@cargo-llvm-cov
       - name: Generate code coverage
-        working-directory: Code
         run: cargo llvm-cov nextest --all-features --workspace --lcov --output-path lcov.info
       - name: Generate text report
-        working-directory: Code
         run: cargo llvm-cov report
       - name: Upload coverage to Codecov
         uses: codecov/codecov-action@v3

.github/workflows/quint.yml

@@ -0,0 +1,29 @@
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+    paths:
+      - Specs/Quint/**
+  pull_request:
+    paths:
+      - Specs/Quint/**
+
+name: Quint
+
+jobs:
+  quint-typecheck:
+    name: Typecheck
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: ./Specs/Quint
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - run: npx @informalsystems/quint typecheck consensus.qnt
+      - run: npx @informalsystems/quint typecheck voteBookkeeper.qnt
+

.github/workflows/rust.yml

@@ -2,16 +2,13 @@ name: Rust
 
 on:
   push:
-    branches: master
+    branches: main
     paths:
       - Code/**
   pull_request:
     paths:
       - Code/**
 
-# permissions:
-#   checks: write
-
 env:
   CARGO_INCREMENTAL: 0
   CARGO_PROFILE_DEV_DEBUG: 1
@@ -24,6 +21,9 @@ jobs:
   test:
     name: Test
     runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: Code
     steps:
       - name: Checkout
         uses: actions/checkout@v4
@@ -32,10 +32,8 @@ jobs:
       - name: Install cargo-nextest
         uses: taiki-e/install-action@cargo-nextest
       - name: Build code
-        working-directory: Code
         run: cargo nextest run --workspace --all-features --no-run
       - name: Run tests
-        working-directory: Code
         run: cargo nextest run --workspace --all-features
 
   clippy:

Code/QUESTIONS.md

@@ -1,2 +1 @@
 - How do we deal with errors?
-- How do we parametrize over values, id(v), etc.

Code/TODO.md

@@ -8,6 +8,4 @@ if complete proposal from a past round => to current one
 if we have some threshold (f+1) of votes for a future round => skip to that round
 
 context (get proposer, get value)
-signing contextt
-
-abstract over values and validator sets
+signing context

Code/common/Cargo.toml

@@ -5,3 +5,5 @@ edition = "2021"
 publish = false
 
 [dependencies]
+secrecy = "0.8.0"
+signature = "2.1.0"

Code/common/src/consensus.rs → Code/common/src/context.rs

@@ -1,28 +1,34 @@
 use crate::{
-    Address, Height, Proposal, PublicKey, Round, Validator, ValidatorSet, Value, ValueId, Vote,
+    Address, Height, PrivateKey, Proposal, PublicKey, Round, Signature, SignedVote, SigningScheme,
+    Validator, ValidatorSet, Value, ValueId, Vote,
 };
 
 /// This trait allows to abstract over the various datatypes
 /// that are used in the consensus engine.
-pub trait Consensus
+pub trait Context
 where
     Self: Sized,
 {
     type Address: Address;
     type Height: Height;
     type Proposal: Proposal<Self>;
-    type PublicKey: PublicKey;
     type Validator: Validator<Self>;
     type ValidatorSet: ValidatorSet<Self>;
     type Value: Value;
     type Vote: Vote<Self>;
-
-    // FIXME: Remove this and thread it through where necessary
-    const DUMMY_ADDRESS: Self::Address;
+    type SigningScheme: SigningScheme; // TODO: Do we need to support multiple signing schemes?
 
     // FIXME: Remove altogether
     const DUMMY_VALUE: Self::Value;
 
+    /// Sign the given vote using the given private key.
+    /// TODO: Maybe move this as concrete methods in `SignedVote`?
+    fn sign_vote(vote: &Self::Vote, private_key: &PrivateKey<Self>) -> Signature<Self>;
+
+    /// Verify the given vote's signature using the given public key.
+    /// TODO: Maybe move this as concrete methods in `SignedVote`?
+    fn verify_signed_vote(signed_vote: &SignedVote<Self>, public_key: &PublicKey<Self>) -> bool;
+
     /// Build a new proposal for the given value at the given height, round and POL round.
     fn new_proposal(
         height: Self::Height,

Code/common/src/lib.rs

@@ -1,5 +1,6 @@
 //! Common data types and abstractions for the consensus engine.
 
+#![no_std]
 #![forbid(unsafe_code)]
 #![deny(unused_crate_dependencies, trivial_casts, trivial_numeric_casts)]
 #![warn(
@@ -10,23 +11,33 @@
 )]
 #![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::panic))]
 
-mod consensus;
+mod context;
 mod height;
 mod proposal;
 mod round;
+mod signed_vote;
+mod signing;
 mod timeout;
 mod validator_set;
 mod value;
 mod vote;
 
+// Re-export `signature` crate for convenience
+pub use ::signature;
+
 /// Type alias to make it easier to refer the `ValueId` type of a given `Consensus` engine.
-pub type ValueId<C> = <<C as Consensus>::Value as Value>::Id;
+pub type ValueId<Ctx> = <<Ctx as Context>::Value as Value>::Id;
+pub type PublicKey<Ctx> = <<Ctx as Context>::SigningScheme as SigningScheme>::PublicKey;
+pub type PrivateKey<Ctx> = <<Ctx as Context>::SigningScheme as SigningScheme>::PrivateKey;
+pub type Signature<Ctx> = <<Ctx as Context>::SigningScheme as SigningScheme>::Signature;
 
-pub use consensus::Consensus;
+pub use context::Context;
 pub use height::Height;
 pub use proposal::Proposal;
 pub use round::Round;
+pub use signed_vote::SignedVote;
+pub use signing::SigningScheme;
 pub use timeout::{Timeout, TimeoutStep};
-pub use validator_set::{Address, PublicKey, Validator, ValidatorSet, VotingPower};
+pub use validator_set::{Address, Validator, ValidatorSet, VotingPower};
 pub use value::Value;
 pub use vote::{Vote, VoteType};

Code/common/src/proposal.rs

@@ -1,20 +1,21 @@
 use core::fmt::Debug;
 
-use crate::{Consensus, Round};
+use crate::{Context, Round};
 
 /// Defines the requirements for a proposal type.
-pub trait Proposal<C: Consensus>
+pub trait Proposal<Ctx>
 where
     Self: Clone + Debug + PartialEq + Eq,
+    Ctx: Context,
 {
     /// The height for which the proposal is for.
-    fn height(&self) -> C::Height;
+    fn height(&self) -> Ctx::Height;
 
     /// The round for which the proposal is for.
     fn round(&self) -> Round;
 
     /// The value that is proposed.
-    fn value(&self) -> &C::Value;
+    fn value(&self) -> &Ctx::Value;
 
     /// The POL round for which the proposal is for.
     fn pol_round(&self) -> Round;

Code/common/src/round.rs

@@ -1,3 +1,5 @@
+use core::cmp;
+
 /// A round number.
 ///
 /// Can be either:
@@ -69,13 +71,13 @@ impl Round {
 }
 
 impl PartialOrd for Round {
-    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+    fn partial_cmp(&self, other: &Self) -> Option<cmp::Ordering> {
         Some(self.cmp(other))
     }
 }
 
 impl Ord for Round {
-    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+    fn cmp(&self, other: &Self) -> cmp::Ordering {
         self.as_i64().cmp(&other.as_i64())
     }
 }

Code/common/src/signed_vote.rs

@@ -0,0 +1,25 @@
+use crate::{Context, Signature, Vote};
+
+// TODO: Do we need to abstract over `SignedVote` as well?
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SignedVote<Ctx>
+where
+    Ctx: Context,
+{
+    pub vote: Ctx::Vote,
+    pub signature: Signature<Ctx>,
+}
+
+impl<Ctx> SignedVote<Ctx>
+where
+    Ctx: Context,
+{
+    pub fn new(vote: Ctx::Vote, signature: Signature<Ctx>) -> Self {
+        Self { vote, signature }
+    }
+
+    pub fn validator_address(&self) -> &Ctx::Address {
+        self.vote.validator_address()
+    }
+}

Code/common/src/signing.rs

@@ -0,0 +1,20 @@
+use core::fmt::Debug;
+
+use secrecy::{CloneableSecret, DebugSecret, Zeroize};
+use signature::{Keypair, Signer, Verifier};
+
+pub trait SigningScheme
+where
+    Self: Clone + Debug + Eq,
+{
+    type Signature: Clone + Debug + Eq;
+
+    type PublicKey: Clone + Debug + Eq + Verifier<Self::Signature>;
+
+    type PrivateKey: Clone
+        + Signer<Self::Signature>
+        + Keypair<VerifyingKey = Self::PublicKey>
+        + Zeroize
+        + DebugSecret
+        + CloneableSecret;
+}

Code/common/src/validator_set.rs

@@ -1,19 +1,12 @@
 use core::fmt::Debug;
 
-use crate::Consensus;
+use crate::{Context, PublicKey};
 
 /// Voting power held by a validator.
 ///
 /// TODO: Do we need to abstract over this as well?
 pub type VotingPower = u64;
 
-/// Defines the requirements for a public key type.
-pub trait PublicKey
-where
-    Self: Clone + Debug + PartialEq + Eq,
-{
-}
-
 /// Defines the requirements for an address.
 ///
 /// TODO: Keep this trait or just add the bounds to Consensus::Address?
@@ -24,16 +17,16 @@ where
 }
 
 /// Defines the requirements for a validator.
-pub trait Validator<C>
+pub trait Validator<Ctx>
 where
     Self: Clone + Debug + PartialEq + Eq,
-    C: Consensus,
+    Ctx: Context,
 {
     /// The address of the validator, typically derived from its public key.
-    fn address(&self) -> &C::Address;
+    fn address(&self) -> &Ctx::Address;
 
     /// The public key of the validator, used to verify signatures.
-    fn public_key(&self) -> &C::PublicKey;
+    fn public_key(&self) -> &PublicKey<Ctx>;
 
     /// The voting power held by the validaror.
     fn voting_power(&self) -> VotingPower;
@@ -42,19 +35,19 @@ where
 /// Defines the requirements for a validator set.
 ///
 /// A validator set is a collection of validators.
-pub trait ValidatorSet<C>
+pub trait ValidatorSet<Ctx>
 where
-    C: Consensus,
+    Ctx: Context,
 {
     /// The total voting power of the validator set.
     fn total_voting_power(&self) -> VotingPower;
 
     /// The proposer in the validator set.
-    fn get_proposer(&self) -> C::Validator;
+    fn get_proposer(&self) -> Ctx::Validator;
 
     /// Get the validator with the given public key.
-    fn get_by_public_key(&self, public_key: &C::PublicKey) -> Option<&C::Validator>;
+    fn get_by_public_key(&self, public_key: &PublicKey<Ctx>) -> Option<&Ctx::Validator>;
 
     /// Get the validator with the given address.
-    fn get_by_address(&self, address: &C::Address) -> Option<&C::Validator>;
+    fn get_by_address(&self, address: &Ctx::Address) -> Option<&Ctx::Validator>;
 }