-
Notifications
You must be signed in to change notification settings - Fork 6
Meeting Minutes
- Coq report is still work-in-progress.
- Discussion of the deposit re-verification effort.
-
Highlights comparing and contrasting the Coq specification against the Gasper paper are now being maintained int he repo's wiki. These and more will be part of the report.
-
Preliminary discussion for Phase 3:
- Discussed briefly the potential gap between the Gasper paper/Coq model/K model on one side and the Python specs on the other regarding what v-set (or balance) is used when justifying a block at epoch e. The paper and the models assume that the v-set and balance of epoch e is used, while the implementation may use epochs e+1 or e+2. Perhaps having something similar to Theorem 8.3 to give a bound or using the same theorem for that are possible options. This will be revisited later in the context of the work that will need to be done for Phase 3.
- Discussed a general idea to make phase 3 more manageable within a reasonable timeframe, which is that the abstract K model may be detailed enough that with additional reasonable effort can be extended to support running the Eth2.0 spec tests. Extending the model and proving its properties may actually be enough to show safety and liveness holds in the implementation, without having to bring the very detailed concrete K model closer to the abstract model. This still needs to be investigated further as we prepare for Phase 3.
-
More refined specs with documentation have been merged.
-
The technical report that is being worked on will focus on the Coq model and the mechanization of the safety and liveness proofs. The K model will have expanded documentation (in
mdformat) for the time being. A longer technical report covering the K model may be prepared later.
-
Both the Coq model and the K model are now complete, pending only a few minor improvements.
-
Gave a quick walkthrough of the slashable bound theorem mechanization in the Coq model.
-
Next up is more documentation and the report.
-
Coq model: work on finalizing the theorem's proof is ongoing. Aditya (EF) joined to audit the specs and think of ways the specs may be used to suggest/evaluate improvements to the protocol.
-
K model: more properties of rewards and penalties in the model were proved.
-
Gave a quick overview of the two models to help bring Aditya up to speed.
-
Coq Model: Discussion with Yan of a few aspects of Theorem 8.3 suggested by the formalization in Coq. Yan confirmed the following points:
-
The first two sentences of the proof of the theorem can be improved by making the application of Lemma 8.2 more explicit
-
The choice of block b0 is just to give a reference point in time. The block need not be finalized, nor does it need to be an ancestor of blocks bL and bR.
-
Although the theorem's bound is proved correct, the theorem does no guarantee that the bound will always be meaningful or useful (this depends on the choice of b0 and how much change in validator sets has occurred across the considered blocks).
-
-
K model: Went through updates on modeling rewards and penalties and proofs of their properties.
-
The deposit contract now has an implementation in solidity and EF would like to engage RV in re-verifying the contract, based on our previous engagement.
-
May 8 is a potential start date for the engagement, with the goal of completing it within 4 weeks.
- Work on both the Coq and K models is ongoing. The end of the month is still our target to complete these final tasks. The report will follow.
-
There is interest in re-verification of the deposit contract's implementation in solidity, if it can be done within a 4-week timeframe.
-
Although the new implementation is not yet ready, it's not expected to be very much different from the original.
-
Work on formalizing the proof of Theorem 8.3 in the paper is ongoing. The weight function is now defined in terms of a newly introduced function that gives the stake of a validator. Properties of the new weight function need to be formalized and proved first.
-
The pending issue in the proof of theorem 8.3 (relating to how the theorem uses lemma 8.2) will be discussed further later on.
-
In the K model, properties about validator exits and activations have been specified and proved. The model is now being extended to specify rewards and penalties.
-
Discussed generally comments received about the deposit contract, its formalization in K, and potential ideas about how take this effort further.
-
Discussed design rationale for eager vs. lazy updates to the list of activations and exits.
-
Note: it’s possible that an active validator’s stake reaches zero while still being active in the pending exit queue. This possibility thus needs to be considered in the models.
-
The generalization of the Coq model to support dynamic validators is complete and the PR will be merged soon. The next major step is show the bound of Theorem 8.3.
-
The proof of Theorem 8.3 in the paper does not seem to use Lemma 8.2 properly. The Lemma's conclusion states that there exists two blocks BL and BR and quorum sets VL \subset vSet(BL) and VR \subset vSet(BR) whose intersection is slashable. The proof, however, seems to take BL and BR given by the lemma to be the conflicting finalized blocks themselves (given in the setup of the theorem), which is not true generally. This point will be investigated further.
-
Work on the K model is progressing. We are defining the properties needed to link the the two models and their proofs.
- Work on generalizing the Coq model to support dynamic validator sets is almost complete. PR will be made soon.
- Liveness in the generalized model seems to require an additional assumption: Votes for a source-target pair must come from validators belonging to the validator set of the target. This is not surprising as the implementation checks that this holds, but the model has to make this assumption explicit for the liveness proof.
- Work (by Martin) on specifying overflow checks in the K beacon chain specification is ongoing.
-
Follow-up to points raised last time:
-
The subset notation in the paper includes the possibility of the two sets being equal (It does not exclusively mean strict or proper inclusion).
-
In Theorem 8.3, the choice of a last final block is not strictly needed; the result holds even if the chosen final block is not the last. But it makes the argument easier to make this assumption.
-
-
Project on track to finishing the second major milestone (coq and k models + proofs) by the end of April. The report will follow soon after.
-
Beacon Chain Specs:
-
There is an update to Ethe2.0 specs, namely 0.11.0. Martin will take care of bumping the K specs up to this version.
-
Martin is also finalizing overflow checking changes. Running tests with handcrafted parameters seems to work fine, but running full-fledged mainnet tests causes K to fail (this will be further investigated).
-
Mostly discussions related to Section 8 in the paper:
-
The v-sets on different branches in the checkpoint tree can be different, even at the same height. In theory, this may be because the different blocks in different branches (even at the same height) may include different activation/exit requests. In practice, the implementation limits activations to finalized blocks, but even then there may be different validators existing at different branches, resulting in the v-sets being different.
-
Note that safety is not only affected by changes in v-sets, but also by when slashing happens (the delay between detecting violations of the slashing conditions and when the slashing actually occurs). The paper assumes the ideal case in which slashing happens at time of detection (zero delay).
-
Theorem 8.3 gives a bound of zero-slashable validators (so it's possible that no validator is slashed) in the case of having justification links that are too long (spanning many epochs), even if the change in v-sets is bounded (see the Weak Subjectivity article).
-
No need to worry about these extreme cases above. The focus should be on modeling and verifying the idealized case considered by the theorem.
-
In the setup of the theorem, "last finalized" means implicitly "last shared finalized", i.e. the last finalized block is an ancestor of the two recently finalized and conflicting blocks
B_LandB_R. The statement should intuitively still holds even if that block was not the last finalized, but the proof is probably simpler with that assumption.
- On extending the Coq model with dynamic validators and Theorem 8.3 from the paper: this theorem is simply defining new validator sets that now exist due to allowing entering and exiting, and then restating the slashable validator set in terms of these new definitions.
- Coq model extension may involve defining explicit validator sets as projections from states.
- Updated Danny on the completion of k-finalization and highest justified block assumption weakening.
- Martin continuing the work on bumping the k-beacon-chain specs to 0.10.1, and also looking into incorporating the dynamic checks suggested last time to check overflow.
- Coq model has two updates: Showing that the assumption highest-justified-block exists, and generalizing safety to k-finalization have almost been completed. Updated specs will be pushed soon. Next steps will be to investigate extending the model with dynamic validators.
- Working on linking the Coq model with the K model is ongoing. Specifications of assumptions and correctness properties in K are being added.
- Note: genesis block is assumed both justified and finalized in the paper.
- Went over a suggested hybrid solution (some where in between static checking and dynamic checking) to address the point raised regarding checking bounds on int in k-beacon-chain.
- Extending the type with bounds that are updated on operations, and the bounds have checks associated with them.
- The pure-static-checking approach works well if you don’t have division operation. This can still be done but it will probably require too much annotation.
- Manual for now but will be helpful as specs evolve. Also correctness of annotation Can also be formally shown correct.
- Work on both models is ongoing.
-
Discussed methods to extend the k-beacon-chain (concrete model) to check for Uint64 overflows/underflows, as this has recently turned out to be a potential issue for actual clients.
-
Current checks exist in the python specs but they are rather coarse and do not cover the intermediate computations.
-
The goal is to understand the options we have to have these checks specified in k-beacon-chain. If this turns out to be doable in reasonable time, the python specs may refer implementers to how these checks are made in k-beacon-chain, increasing awareness about them.
-
The general options are:
- Symbolic verification: non-trivial, requires effort and time, may not be fully automatic (plus we will have to address some technical issues using k-beacon-chain on the Haskell backend)
- Sub-typing an type-checking: Instead of arbitrary integers, define bounded integer types and an appropriate sub typing hierarchy, and annotate operations and rules with the required types. Use type-checking to reject invalid expressions. Definitions and annotations are manually done, but checking is automatic. Good options if the specs is not going to change much.
- Dynamic checks: add assertion checks (conditions to rules) to detect overflow when it happens. Not very much different from falling into a runtime error. Not good enough if we are trying to avoid them in the first place.
- Use big numbers in clients (but bad fo efficiency and inter-operability)
-
The sub-typing option seems the most viable. We are going to investigate this further and will try to do an example to get a better feeling of this achieves and how much effort it will require. This may result in a proposal for extending the k-beacon-chain. This is expected to add value to this model.
- Reviewed the main design decisions in the dynamic model
- Went over the model specs of Casper in Coq https://github.com/runtimeverification/beacon-chain-verification/tree/master/casper/coq
- Made good progress on the dynamic model. The current progress can be found here: https://github.com/runtimeverification/beacon-chain-verification/tree/master/dynamic We will improve it a bit more, and should be able to submit the first milestone deliverables (i.e., the initial static and dynamic models) by end of this week.
- For the static model, we have been working on developing the model and proofs in both K and Coq over the last period. While the focus was initially on developing them in K, we realized that properly developing the infrastructure needed to simulate these proofs in K is likely going to require more time than originally anticipated, resulting in extended delays. So we decided to switch our focus to Coq for the static model only, where we have been merging the two Casper models we developed previously and updating the safety and liveness proofs (work-in-progress Coq specifications are available in the repo). This of course does not change the objectives or the tasks laid out for the static model in any significant way, nor does it alter the project’s timeline. In particular, we still intend to have the first deliverable (initial versions of the static model in Coq and the dynamic model in K) ready by the end of the week (or early next week at the latest). We would be glad to discuss this further live If needed this week, or here in the channel. The plan for next week’s meeting is to go over the Coq and K specs of the models.
- A quick progress update
- Discussed briefly some additional, more recent resources on Eth2 Phase 0 that can be useful for the project
- Martin might pick up updating the specs to the now-frozen 0.10 specs. Support will be provided as needed.
- Although January 24th is still our target for completing the first milestone of the project, we may potentially need one more week to have it ready. The main challenge has been building the ITP structure in K properly.
- Discussion on dynamic validators + reviewing some assumptions in the original casper model
Paper discussion
Paper discussion
Paper discussion
- The beacon chain academic report that includes updated safety and liveness arguments is almost ready to go to arxiv.org. These arguments have been updated and should reflect the most recent changes in the protocol.
- The paper should be used as the starting point when preparing for this engagement. We may initiate discussion on the paper to clarify things and suggest improvements.
- No meeting next week and will resume the week after.
- The Phase-II proposal has been approved. Based on internal resource planning, work on the project will officially begin December 2, 2019.
- 0.9.0 update merged with updated coverage report generated. 0.9.1 update will be done by Martin.
- Feedback from EF on the proposal in a couple of days (by the end of this week). Mainly evaluating budget allocation at this stage. 0.9 update of K specs is complete. Pending final review, will be merged soon.
- Updated standard and control-sensitive coverage analysis reports will be generated
- There were discussions of verifying validator specs and/or fork choice rule, optimizing specs for performance, and adding random testing, but priority now is given to verifying safety and liveness of the beacon chain protocol/implementation.
- Danny suggested that the update to 0.9 to be done in-house (mainly Martin)
- Proposal still under review
- Briefed Carl and Martin (Danny was not present) on what we have been doing regarding preparing for the next phase of the project (in particular preparing for using the Haskell backend for verification)
- Hinted to the point that using the current concrete model for verification is not the best way to go, and the approach we described in the proposal is the best approach.
- Martin asked about how we are going to handle changes in the BC implementation since it seems there are some somewhat major changes planned. The changes will be provided to us so that we may plan ahead and assess the amount of time and effort needed to update the K specs, and this can then be accounted for in the engagement.
- The interest is now on formal verification of beacon chain properties, rather than on expanding the specs to include other parts of Eth2 such as sharding specs.