c939e155a6
abci: clarify connection use in-process ( #337 )
...
* abci: clarify connection use in-process
* Update abci.md
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io >
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io >
* invert abci explanations
* lint++
* lint++
* lint++
* lint++
Co-authored-by: M. J. Fromberger <fromberger@interchain.io >
2021-08-24 14:27:19 -04:00
4b79bccc0b
Fixed a broken link ( #291 )
2021-05-07 14:29:12 -04:00
00446bb9f4
Update README.md ( #286 )
2021-04-23 19:52:48 +00:00
9f6a4bcf23
readme: cleanup ( #262 )
...
* modify readme
* add rfc and proto
* add rust=spec back to avoid breakage
* lint readme
2021-03-17 13:51:10 +00:00
b270ab8d15
spec: merge rust-spec ( #252 )
2021-03-01 08:54:08 +00:00
2f590a6392
non-critical bugfix in the TLA+ spec (found by new version of apalache) ( #244 )
2021-01-21 11:50:06 +01:00
72d15a4b07
spec: remove reactor section ( #242 )
...
Co-authored-by: Tess Rinearson <tess.rinearson@gmail.com >
2021-01-19 16:28:05 +01:00
1b2b24055c
Update supervisor_001_draft.md ( #243 )
2021-01-15 13:39:36 +01:00
accd7ffe18
Update README.md ( #234 )
2020-12-16 13:27:23 +01:00
42751ea4f3
Computing attack types ( #232 )
...
Add light attack evidence handling
2020-12-15 18:45:26 +01:00
31cfa53082
The TLA+ specification of the attackers detection ( #231 )
...
* the working attackers isolation spec, needs more comments
* the TLA+ spec of the attackers isolation
2020-12-11 15:03:48 +01:00
26ef2ccddb
Draft of evidence handling for discussion ( #225 )
...
* start with accountability deliverable
* problem statement
* draft function
* quite complete draft. ready to discuss with Igor
* Update isolate-attackers_001_draft.md
* Update isolate-attackers_001_draft.md
* Update isolate-attackers_001_draft.md
* Update isolate-attackers_001_draft.md
* Update isolate-attackers_001_draft.md
* ready for TLA+ to take over
* isolate
* isolateamnesiatodos
* Update isolate-attackers_001_draft.md
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
* Update rust-spec/lightclient/attacks/isolate-attackers_001_draft.md
Co-authored-by: Igor Konnov <konnov@forsyte.at >
2020-12-11 14:34:16 +01:00
c1ff62fe44
Light client detector spec in TLA+ and refactoring of light client verification TLA+ spec ( #216 )
...
Add light client detector spec in TLA+
2020-11-09 11:08:33 +01:00
d5e0294003
Detector English Spec ready ( #215 )
...
Add detector English spec
2020-11-09 11:03:20 +01:00
9ad6440bc0
Sequential Supervisor ( #186 )
...
* 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 >
2020-11-02 17:35:25 +01:00
ec8af314cc
spec: update light client verification to match supervisor ( #171 )
...
* 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
2020-10-22 14:26:56 +02:00
792767d1cb
Extending the blockchain specification (in the light client) to produce different ratios of faults ( #183 )
...
* cleaning unused definitions
* introduced the ratio of faulty processes
2020-10-08 10:42:00 +02:00
0794fc8ff2
first check latest with secondary ( #184 )
2020-10-08 09:51:00 +02:00
8391fa0b89
TLA+ specs from MBT revision ( #173 )
2020-10-01 11:31:53 +02:00
733b020899
evidence: update data structures ( #165 )
2020-09-29 14:05:44 +02:00
80747a0872
fixed an overlooked conflict ( #167 )
2020-09-24 09:59:24 +02:00
f3033c5515
spec: Light client attack detector ( #164 )
...
* 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 >
2020-09-24 09:53:50 +02:00
606abc7fc0
Fastsync spec from tendermint-rs ( #157 )
...
* 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 >
2020-09-10 13:03:50 +02:00
b74b1c2b68
Current versions of light client specs from tendermint-rs ( #158 )
...
* current versions of light client specs from tendermint-rs
* markdown lint
* linting
* links
* links
* links
Co-authored-by: Marko Baricevic <marbar3778@yahoo.com >
2020-09-10 12:56:15 +02:00
William Banfield
Jordan Sexton
Ethan Buchman
Marko
Igor Konnov
Josef Widder
Callum Waters