Conversation
daira
force-pushed
the
lean
branch
3 times, most recently
from
531bec1 to
cb41963
Compare
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
|
I hereby volunteer to be a reviewer for this PR with the two big caveats:
If that schedule doesn't work for this PR, then I'd like to capture my review notes elsewhere in this repo (after this PR and subsequent changes are merged). |
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
Signed-off-by: Daira-Emma Hopwood <[email protected]>
oxarbitrage
left a comment
oxarbitrage
left a comment
There was a problem hiding this comment.
Great start, thanks for pushing this forward. I’ve left a few optional suggestions and questions inline.
I’d love to contribute more to this Lean formalization, including taking a pass at some of the current sorrys, and to help across the repo more broadly. I’m not sure what the most convenient way to coordinate is (issues, pr's, a short sync, or something else) so I’m happy to follow your lead, @daira, if you think that would add value.
| /-- | ||
| An execution of Π_bc has Agreement on the view `V : Node → Time → BcChain` iff | ||
| for all times `t`, `u` and all Π-nodes `i`, `j` (potentially the same) such that | ||
| `i` is honest at time `t` and `j` is honest at time `u`, we have `V i t ≤≥ V j u`. |
There was a problem hiding this comment.
| `i` is honest at time `t` and `j` is honest at time `u`, we have `V i t ≤≥ V j u`. | |
| `i` is honest at time `t` and `j` is honest at time `u`, we have `V i t ≼≽ V j u`. |
|
|
||
| Since chains are represented tip-first, this is implemented by dropping the first | ||
| `k` elements. | ||
| -/ |
There was a problem hiding this comment.
| -/ | |
| TODO: this definition works for any chain type; generalize it. | |
| -/ |
There are several definitions that can be generalized (bft_prefix, bc_tip, etc). Do we want to have a Definitions.lean in the future for some of those?
| local infix:50 "≼/≽" => bc_conflicts | ||
|
|
||
| /-- If a ≼ c ∧ b ≼ c then a ≼≽ b. -/ | ||
| public lemma linear_prefix (a b c : BcChain) (hac : a ≼ c) (hbc : b ≼ c) : a ≼≽ b := by |
There was a problem hiding this comment.
This is true for any chain type. Will be good to add it to the Bftchain file too, as we have no lemmas there atm.
|
|
||
| TODO: this definition works for any chain type; generalize it. | ||
| -/ | ||
| public def ComposedBftAgreement {U : Type} (V : Node → Time → U) (f : U → BftChain) := |
There was a problem hiding this comment.
I think this definition is not in the book. Should we add it there?
There was a problem hiding this comment.
Will be good to auto generate docs from the lean code and publish somewhere.
|
|
||
| import Mathlib.Tactic | ||
|
|
||
| import TFL.LCA |
There was a problem hiding this comment.
| import TFL.LCA | |
| import TFL.BcChain |
No need to import LCA here but just BcChain will do it.
3 participants
No description provided.