Lookback
Lookback amount.
It may seem natural for the committee bonded at a round
to be in charge of that round,
i.e. proposing and signing certificates for that round, etc.
However, validators are not always perfectly in sync;
there may be delays,
and a validator's blockchain may be
ahead of another validator's blockchain.
For this reason, AleoBFT uses a lookback approach:
the committee in charge of a round is `looked back' by a given amount.
That is, the committee in charge for a round R
is the committee bonded at round R-B,
where B is a fixed globally known positive integer.
When R <= B, the genesis committee is used.
The idea behind this lookback approach is that,
by going sufficiently back in rounds (e.g. B = 100),
all validators should have blocks for those rounds,
and should be able to calculate (and agree on)
the committee bonded at those rounds.
This is an assumption, which should be subjected to more formal study,
but it is the rationale behind the approach.
Since B is fixed and globally known,
we introduce a constrained nullary function that returns it.
There is no need to pick a specific value in this model;
this way the model is more general.
Should the need arise to prove properties that depend on
specific values of B,
or more generally, on whether B is in a certain range,
those constraints can be hypotheses of such theorems.
Definitions and Theorems
Theorem: posp-of-lookback
(defthm posp-of-lookback
(posp (lookback))
:rule-classes (:rewrite :type-prescription))
