-
Notifications
You must be signed in to change notification settings - Fork 224
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Light Client: Follow-up #284
Changes from 19 commits
906add1
c95c919
9c22449
ff62097
dddf9e8
18ffa1c
e39a6cb
d208b04
38153cb
d9fbe4c
594ce1a
6c2b7c5
88aafd4
ed2ee36
3d4c226
d1bb164
74134a4
cd38cf3
8b7a2aa
72bc898
4590350
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,5 @@ | ||
//! Components used by the Light Client. | ||
|
||
pub mod clock; | ||
pub mod fork_detector; | ||
pub mod io; | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 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_schedule( | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Since this is actually performing bisection does it make sense to call it There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Sure, that's indeed a better name. I chose There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. So perhaps |
||
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 < next_height` and `latest_verified_height < target_height` | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. s/next_height/current_height |
||
/// then `latest_verified_height < scheduled_height < next_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 nextHeight has been verified, | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. s/nextHeight/current_height |
||
/// and we can choose a height closer to the targetHeight. 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 of `next_height` could not be verified, and we need to pick a smaller height. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. same |
||
/// - 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 { | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe in the preamble provide reference to the english spec such that the invariants can be looked up by the reader.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@ebuchman suggested getting rid of the prelude entirely for better discoverability so that's perhaps not the right place to put those references. The crate-level documentation in
lib.rs
might be a better fit.