Add light client detector spec in TLA+

* add Ivy proofs

* fix docker-compose command

Add detector English spec

Co-authored-by: Callum Waters <cmwaters19@gmail.com>

Co-authored-by: Robert Zaremba <robert@zaremba.ch>

* move from tendermint-rs but needs discussion

* markdown lint

* TODO links replaced

* links

* links

* links lint

* Update rust-spec/lightclient/supervisor/supervisor.md

* Update rust-spec/lightclient/supervisor/supervisor.md

* Update rust-spec/lightclient/supervisor/supervisor.md

* Update rust-spec/lightclient/supervisor/supervisor.md

* moved peer handling definitions to supervisor

* polishing

* rename

* Update rust-spec/lightclient/supervisor/supervisor_001_draft.md

* Update rust-spec/lightclient/supervisor/supervisor_001_draft.md

* changes to maintain StateVerified again

* ready for changes in verification

* start of supervisor

* module name

* fixed

* more details

* supevisor completed. Now I have to add function to verification

* ready for review

* tla comment

* removed issues

* Update rust-spec/lightclient/supervisor/supervisor_001_draft.md

* intro text fixed

* indentation

* Update rust-spec/lightclient/supervisor/supervisor_001_draft.md

* comment to entry points

Co-authored-by: Marko Baricevic <marbar3778@yahoo.com>

* VDD renaming of verification spec + links fixed

* latest()

* backwards

* added TODOs

* link in old file to new name

* better text

* revision done. needs one more round of reading

* renamed constants in 001 according to TLA+ and impl

* ready for PR

* forgot linting

* Update rust-spec/lightclient/verification/verification_002_draft.md

* Update rust-spec/lightclient/verification/verification_002_draft.md

* added lightstore function needed for supervisor

* added lightstore functions for supervisor

* ident

* Update rust-spec/lightclient/verification/verification_002_draft.md

Bumps [gaurav-nelson/github-action-markdown-link-check](https://github.com/gaurav-nelson/github-action-markdown-link-check) from 1.0.7 to 1.0.8.
- [Release notes](https://github.com/gaurav-nelson/github-action-markdown-link-check/releases)
- [Commits](https://github.com/gaurav-nelson/github-action-markdown-link-check/compare/1.0.7...e3c371c731b2f494f856dc5de7f61cea4d519907)

Signed-off-by: dependabot[bot] <support@github.com>

Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

* cleaning unused definitions

* introduced the ratio of faulty processes

Co-authored-by: Anton Kaliaev <anton.kalyaev@gmail.com>

* start with new detection and evidence spec

* more definitions at top

* sketch of functions

* pre post draft

* evidence proof

* typo

* evidence theory polished

* some TODOs resolved

* more TODOs

* links

* second to last revision before PR

* links

* I will read once more and then make a PR

* removed peer handling definitions

* secondary

* ready to review

* detector ready for review

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update rust-spec/lightclient/detection/detection.md

* skip-trace

* PossibleCommit explained

* Update rust-spec/lightclient/detection/detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* comments by Zarko

* renamed and changed link in README

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* spec/reactors/mempool: batch txs per peer

Refs https://github.com/tendermint/tendermint/issues/625

* update

* fastsync spec from tendermint-rs

* fixed broken link

* fixed linting

* more fixes

* markdown lint

* move fast_sync to rust-spec

Co-authored-by: Marko Baricevic <marbar3778@yahoo.com>

* current versions of light client specs from tendermint-rs

* markdown lint

* linting

* links

* links

* links

Co-authored-by: Marko Baricevic <marbar3778@yahoo.com>

Co-authored-by: Callum Waters <cmwaters19@gmail.com>

Bumps [gaurav-nelson/github-action-markdown-link-check](https://github.com/gaurav-nelson/github-action-markdown-link-check) from 0.6.0 to 1.0.7.

Signed-off-by: dependabot[bot] <support@github.com>

Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

This change removes unused directories (`papers` and `research`) 
and updates the README to reflect our strategy for merging the 
informalsystems/tendermint-rs specs into this repository.

Partially addresses #121.

spec: bringing blockchain back