Igor Konnov c1ff62fe44 | 4 years ago | |
---|---|---|
.. | ||
004bmc-apalache-ok.csv | 4 years ago | |
005bmc-apalache-error.csv | 4 years ago | |
Blockchain_003_draft.tla | 4 years ago | |
LCD_MC3_3_faulty.tla | 4 years ago | |
LCD_MC3_4_faulty.tla | 4 years ago | |
LCD_MC4_4_faulty.tla | 4 years ago | |
LCD_MC5_5_faulty.tla | 4 years ago | |
LCDetector_003_draft.tla | 4 years ago | |
LCVerificationApi_003_draft.tla | 4 years ago | |
README.md | 4 years ago | |
detection_001_reviewed.md | 4 years ago | |
detection_003_reviewed.md | 4 years ago | |
discussions.md | 4 years ago | |
draft-functions.md | 4 years ago | |
req-ibc-detection.md | 4 years ago |
This is a work in progress. This directory captures the ongoing work and discussion on fork detection both in the context of a Tendermint light node and in the context of IBC. It contains the following files
a draft of the light node fork detection including "proof of fork" definition, that is, the data structure to submit evidence to full nodes.
A collection of ideas and intuitions from recent discussions
In order to address the collected requirements, we started to sketch some functions that we will need in the future when we specify in more detail the
on the following components.
We decided to merge the files while there are still open points to address to record the current state an move forward. In particular, the following points need to be addressed:
https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466504876
https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466493900
https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466489045
https://github.com/informalsystems/tendermint-rs/pull/479#discussion_r466491471
Most likely we will write a specification on the light client supervisor along the outcomes of
that also addresses initialization