Light Client: Follow-up (#284)

* Introduce clock_drift verification parameter, as per the spec

* Re-enable contract in IO component

* Document the scheduler component

* Cleanup fork detector

* Document verifier

* Fix tests and example

* Add more documentation

* Add more spec tags for traceability

* Rename light_client crate to tendermint_light_client

* WIP: Enable precondition on verify_to_target

* Improve documentation

* Point to light_client module for main documentation

* Update #[deny] flags

* Include trust threshold in InsufficientValidatorsOverlap error

* Improve performance of LightStore::latest

* Fix verifier predicates logic

* Remove Verdict::and_then

* Formatting

* Disable test unsupported on CI

* Address review comments

* Rename scheduler::basic_schedule to scheduler::basic_bisecting_schedule

light-client/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "light-client"
+name = "tendermint-light-client"
 version = "0.1.0"
 authors = ["Romain Ruetschi <romain@informal.systems>"]
 edition = "2018"

light-client/examples/light_client.rs

@@ -1,5 +1,5 @@
 use gumdrop::Options;
-use light_client::prelude::Height;
+use tendermint_light_client::prelude::Height;
 
 use std::collections::HashMap;
 use std::path::PathBuf;
@@ -58,8 +58,8 @@ fn main() {
 }
 
 fn sync_cmd(opts: SyncOpts) {
-    use light_client::components::scheduler;
-    use light_client::prelude::*;
+    use tendermint_light_client::components::scheduler;
+    use tendermint_light_client::prelude::*;
 
     let primary_addr = opts.address;
     let primary: PeerId = "BADFADAD0BEFEEDC0C0ADEADBEEFC0FFEEFACADE".parse().unwrap();
@@ -102,24 +102,14 @@ fn sync_cmd(opts: SyncOpts) {
             denominator: 3,
         },
         trusting_period: Duration::from_secs(36000),
+        clock_drift: Duration::from_secs(1),
         now: Time::now(),
     };
 
-    let predicates = ProdPredicates;
-    let voting_power_calculator = ProdVotingPowerCalculator;
-    let commit_validator = ProdCommitValidator;
-    let header_hasher = ProdHeaderHasher;
-
-    let verifier = ProdVerifier::new(
-        predicates,
-        voting_power_calculator,
-        commit_validator,
-        header_hasher,
-    );
-
+    let verifier = ProdVerifier::default();
     let clock = SystemClock;
-    let scheduler = scheduler::schedule;
-    let fork_detector = RealForkDetector::new(header_hasher);
+    let scheduler = scheduler::basic_bisecting_schedule;
+    let fork_detector = ProdForkDetector::default();
 
     let mut light_client = LightClient::new(
         state,

light-client/src/components.rs

@@ -1,3 +1,5 @@
+//! Components used by the Light Client.
+
 pub mod clock;
 pub mod fork_detector;
 pub mod io;

light-client/src/components/fork_detector.rs

@@ -14,19 +14,25 @@ pub trait ForkDetector {
     fn detect(&self, light_blocks: Vec<LightBlock>) -> ForkDetection;
 }
 
-pub struct RealForkDetector {
+pub struct ProdForkDetector {
     header_hasher: Box<dyn HeaderHasher>,
 }
 
-impl RealForkDetector {
+impl ProdForkDetector {
     pub fn new(header_hasher: impl HeaderHasher + 'static) -> Self {
         Self {
             header_hasher: Box::new(header_hasher),
         }
     }
 }
 
-impl ForkDetector for RealForkDetector {
+impl Default for ProdForkDetector {
+    fn default() -> Self {
+        Self::new(ProdHeaderHasher)
+    }
+}
+
+impl ForkDetector for ProdForkDetector {
     fn detect(&self, mut light_blocks: Vec<LightBlock>) -> ForkDetection {
         if light_blocks.is_empty() {
             return ForkDetection::NotDetected;

light-client/src/components/io.rs

@@ -1,4 +1,6 @@
-use contracts::pre;
+use std::collections::HashMap;
+
+use contracts::{contract_trait, post, pre};
 use serde::{Deserialize, Serialize};
 use tendermint::{block, rpc};
 use thiserror::Error;
@@ -7,7 +9,6 @@ use tendermint::block::signed_header::SignedHeader as TMSignedHeader;
 use tendermint::validator::Set as TMValidatorSet;
 
 use crate::prelude::*;
-use std::collections::HashMap;
 
 pub const LATEST_HEIGHT: Height = 0;
 
@@ -19,15 +20,17 @@ pub enum IoError {
 }
 
 /// Interface for fetching light blocks from a full node, typically via the RPC client.
-// TODO: Enable contracts on the trait once the provider field is available.
-// #[contract_trait]
+#[contract_trait]
 pub trait Io {
     /// Fetch a light block at the given height from the peer with the given peer ID.
-    // #[post(ret.map(|lb| lb.provider == peer).unwrap_or(true))]
+    ///
+    /// ## Postcondition
+    /// - The provider of the returned light block matches the given peer [LCV-IO-POST-PROVIDER]
+    #[post(ret.as_ref().map(|lb| lb.provider == peer).unwrap_or(true))]
     fn fetch_light_block(&mut self, peer: PeerId, height: Height) -> Result<LightBlock, IoError>;
 }
 
-// #[contract_trait]
+#[contract_trait]
 impl<F> Io for F
 where
     F: FnMut(PeerId, Height) -> Result<LightBlock, IoError>,
@@ -44,7 +47,7 @@ pub struct ProdIo {
     peer_map: HashMap<PeerId, tendermint::net::Address>,
 }
 
-// #[contract_trait]
+#[contract_trait]
 impl Io for ProdIo {
     fn fetch_light_block(&mut self, peer: PeerId, height: Height) -> Result<LightBlock, IoError> {
         let signed_header = self.fetch_signed_header(peer, height)?;

light-client/src/components/scheduler.rs

@@ -1,14 +1,25 @@
 use crate::prelude::*;
 use contracts::*;
 
+/// The scheduler decides what block to verify next given the current and target heights.
+///
+/// The scheduler is given access to the light store, in order to optionally
+/// improve performance by picking a next block that has already been fetched.
 #[contract_trait]
 pub trait Scheduler {
+    /// Decides what block to verify next.
+    ///
+    /// ## Precondition
+    /// - The light store contains at least one verified block. [LCV-SCHEDULE-PRE.1]
+    ///
+    /// ## Postcondition
+    /// - The resulting height must be valid according to `valid_schedule`. [LCV-SCHEDULE-POST.1]
     #[pre(light_store.latest(VerifiedStatus::Verified).is_some())]
-    #[post(valid_schedule(ret, target_height, next_height, light_store))]
+    #[post(valid_schedule(ret, target_height, current_height, light_store))]
     fn schedule(
         &self,
         light_store: &dyn LightStore,
-        next_height: Height,
+        current_height: Height,
         target_height: Height,
     ) -> Height;
 }
@@ -21,51 +32,81 @@ where
     fn schedule(
         &self,
         light_store: &dyn LightStore,
-        next_height: Height,
+        current_height: Height,
         target_height: Height,
     ) -> Height {
-        self(light_store, next_height, target_height)
+        self(light_store, current_height, target_height)
     }
 }
 
+/// Basic bisecting scheduler which picks the appropriate midpoint without
+/// optimizing for performance using the blocks available in the light store.
+///
+/// ## Precondition
+/// - The light store contains at least one verified block. [LCV-SCHEDULE-PRE.1]
+///
+/// ## Postcondition
+/// - The resulting height must be valid according to `valid_schedule`. [LCV-SCHEDULE-POST.1]
 #[pre(light_store.latest(VerifiedStatus::Verified).is_some())]
-#[post(valid_schedule(ret, target_height, next_height, light_store))]
-pub fn schedule(
+#[post(valid_schedule(ret, target_height, current_height, light_store))]
+pub fn basic_bisecting_schedule(
     light_store: &dyn LightStore,
-    next_height: Height,
+    current_height: Height,
     target_height: Height,
 ) -> Height {
     let latest_trusted_height = light_store
         .latest(VerifiedStatus::Verified)
         .map(|lb| lb.height())
         .unwrap();
 
-    if latest_trusted_height == next_height && latest_trusted_height < target_height {
+    if latest_trusted_height == current_height && latest_trusted_height < target_height {
         target_height
-    } else if latest_trusted_height < next_height && latest_trusted_height < target_height {
-        midpoint(latest_trusted_height, next_height)
+    } else if latest_trusted_height < current_height && latest_trusted_height < target_height {
+        midpoint(latest_trusted_height, current_height)
     } else if latest_trusted_height == target_height {
         target_height
     } else {
-        midpoint(next_height, target_height)
+        midpoint(current_height, target_height)
     }
 }
 
-fn valid_schedule(
+/// Checks whether the given `scheduled_height` is a valid schedule according to the
+/// following specification.
+///
+/// - i) If `latest_verified_height == current_height` and `latest_verified_height < target_height`
+/// then `current_height < scheduled_height <= target_height`.
+///
+/// - ii) If `latest_verified_height < current_height` and `latest_verified_height < target_height`
+/// then `latest_verified_height < scheduled_height < current_height`.
+///
+/// - iii) If `latest_verified_height = target_height` then `scheduled_height == target_height`.
+///
+/// ## Note
+///
+/// - Case i. captures the case where the light block at height `current_height` has been verified,
+///   and we can choose a height closer to the `target_height`. As we get the `light_store` as parameter,
+///   the choice of the next height can depend on the `light_store`, e.g., we can pick a height
+///   for which we have already downloaded a light block.
+/// - In Case ii. the header at `current_height` could not be verified, and we need to pick a lesser height.
+/// - In Case iii. is a special case when we have verified the `target_height`.
+///
+/// ## Implements
+/// - [LCV-SCHEDULE-POST.1]
+pub fn valid_schedule(
     scheduled_height: Height,
     target_height: Height,
-    next_height: Height,
+    current_height: Height,
     light_store: &dyn LightStore,
 ) -> bool {
     let latest_trusted_height = light_store
         .latest(VerifiedStatus::Verified)
         .map(|lb| lb.height())
         .unwrap();
 
-    if latest_trusted_height == next_height && latest_trusted_height < target_height {
-        next_height < scheduled_height && scheduled_height <= target_height
-    } else if latest_trusted_height < next_height && latest_trusted_height < target_height {
-        latest_trusted_height < scheduled_height && scheduled_height < next_height
+    if latest_trusted_height == current_height && latest_trusted_height < target_height {
+        current_height < scheduled_height && scheduled_height <= target_height
+    } else if latest_trusted_height < current_height && latest_trusted_height < target_height {
+        latest_trusted_height < scheduled_height && scheduled_height < current_height
     } else if latest_trusted_height == target_height {
         scheduled_height == target_height
     } else {