From 45ee6b620abd2f4de3a45389bd94ed68847d4a14 Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Tue, 30 Jun 2020 14:56:03 +0200 Subject: [PATCH] new directory structure (#396) --- docs/spec/lightclient/README.md | 10 +++++----- docs/spec/lightclient/{ => detection}/detection.md | 0 .../lightclient/{ => verification}/001bmc-apalache.csv | 0 .../lightclient/{ => verification}/Blockchain_A_1.tla | 0 .../lightclient/{ => verification}/Lightclient_A_1.tla | 0 .../lightclient/{ => verification}/MC4_3_correct.tla | 0 .../lightclient/{ => verification}/MC4_3_faulty.tla | 0 .../lightclient/{ => verification}/MC4_4_faulty.tla | 0 .../lightclient/{ => verification}/MC4_5_correct.tla | 0 .../lightclient/{ => verification}/MC4_5_faulty.tla | 0 .../lightclient/{ => verification}/MC4_6_faulty.tla | 0 .../lightclient/{ => verification}/MC4_7_faulty.tla | 0 .../lightclient/{ => verification}/MC5_5_correct.tla | 0 .../lightclient/{ => verification}/MC5_5_faulty.tla | 0 .../lightclient/{ => verification}/MC5_7_faulty.tla | 0 .../lightclient/{ => verification}/MC7_5_faulty.tla | 0 .../lightclient/{ => verification}/MC7_7_faulty.tla | 0 .../lightclient/{ => verification}/verification.md | 0 18 files changed, 5 insertions(+), 5 deletions(-) rename docs/spec/lightclient/{ => detection}/detection.md (100%) rename docs/spec/lightclient/{ => verification}/001bmc-apalache.csv (100%) rename docs/spec/lightclient/{ => verification}/Blockchain_A_1.tla (100%) rename docs/spec/lightclient/{ => verification}/Lightclient_A_1.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_3_correct.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_3_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_4_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_5_correct.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_5_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_6_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC4_7_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC5_5_correct.tla (100%) rename docs/spec/lightclient/{ => verification}/MC5_5_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC5_7_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC7_5_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/MC7_7_faulty.tla (100%) rename docs/spec/lightclient/{ => verification}/verification.md (100%) diff --git a/docs/spec/lightclient/README.md b/docs/spec/lightclient/README.md index ecf193a2a..137e42266 100644 --- a/docs/spec/lightclient/README.md +++ b/docs/spec/lightclient/README.md @@ -18,10 +18,10 @@ The light client is decomposed into three components: ## Commit Verification -The [English specification](verification.md) describes the light client +The [English specification](verification/verification.md) describes the light client commit verification problem in terms of the temporal properties -[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md#lcv-dist-safe1) and -[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md#lcv-dist-live1). +[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md#lcv-dist-safe1) and +[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md#lcv-dist-live1). Commit verification is assumed to operate within the Tendermint Failure Model, where +2/3 of validators are correct for some time period and validator sets can change arbitrarily at each height. @@ -33,7 +33,7 @@ many intermediate headers by exploiting overlap in trusted and untrusted validat When there is not enough overlap, a bisection routine can be used to find a minimal set of headers that do provide the required overlap. -The [TLA+ specification](Lightclient_A_1.tla) is a formal description of the +The [TLA+ specification](verification/Lightclient_A_1.tla) is a formal description of the commit verification protocol executed by a client, including the safety and liveness properties, which can be model checked with Apalache. @@ -48,7 +48,7 @@ TODO: This is a work-in-progress draft. -The [English specification](detection.md) defines blockchain forks and describes +The [English specification](detection/detection.md) defines blockchain forks and describes the problem of a light client detecting them from communication with a network of full nodes, where at least one is correct. diff --git a/docs/spec/lightclient/detection.md b/docs/spec/lightclient/detection/detection.md similarity index 100% rename from docs/spec/lightclient/detection.md rename to docs/spec/lightclient/detection/detection.md diff --git a/docs/spec/lightclient/001bmc-apalache.csv b/docs/spec/lightclient/verification/001bmc-apalache.csv similarity index 100% rename from docs/spec/lightclient/001bmc-apalache.csv rename to docs/spec/lightclient/verification/001bmc-apalache.csv diff --git a/docs/spec/lightclient/Blockchain_A_1.tla b/docs/spec/lightclient/verification/Blockchain_A_1.tla similarity index 100% rename from docs/spec/lightclient/Blockchain_A_1.tla rename to docs/spec/lightclient/verification/Blockchain_A_1.tla diff --git a/docs/spec/lightclient/Lightclient_A_1.tla b/docs/spec/lightclient/verification/Lightclient_A_1.tla similarity index 100% rename from docs/spec/lightclient/Lightclient_A_1.tla rename to docs/spec/lightclient/verification/Lightclient_A_1.tla diff --git a/docs/spec/lightclient/MC4_3_correct.tla b/docs/spec/lightclient/verification/MC4_3_correct.tla similarity index 100% rename from docs/spec/lightclient/MC4_3_correct.tla rename to docs/spec/lightclient/verification/MC4_3_correct.tla diff --git a/docs/spec/lightclient/MC4_3_faulty.tla b/docs/spec/lightclient/verification/MC4_3_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC4_3_faulty.tla rename to docs/spec/lightclient/verification/MC4_3_faulty.tla diff --git a/docs/spec/lightclient/MC4_4_faulty.tla b/docs/spec/lightclient/verification/MC4_4_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC4_4_faulty.tla rename to docs/spec/lightclient/verification/MC4_4_faulty.tla diff --git a/docs/spec/lightclient/MC4_5_correct.tla b/docs/spec/lightclient/verification/MC4_5_correct.tla similarity index 100% rename from docs/spec/lightclient/MC4_5_correct.tla rename to docs/spec/lightclient/verification/MC4_5_correct.tla diff --git a/docs/spec/lightclient/MC4_5_faulty.tla b/docs/spec/lightclient/verification/MC4_5_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC4_5_faulty.tla rename to docs/spec/lightclient/verification/MC4_5_faulty.tla diff --git a/docs/spec/lightclient/MC4_6_faulty.tla b/docs/spec/lightclient/verification/MC4_6_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC4_6_faulty.tla rename to docs/spec/lightclient/verification/MC4_6_faulty.tla diff --git a/docs/spec/lightclient/MC4_7_faulty.tla b/docs/spec/lightclient/verification/MC4_7_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC4_7_faulty.tla rename to docs/spec/lightclient/verification/MC4_7_faulty.tla diff --git a/docs/spec/lightclient/MC5_5_correct.tla b/docs/spec/lightclient/verification/MC5_5_correct.tla similarity index 100% rename from docs/spec/lightclient/MC5_5_correct.tla rename to docs/spec/lightclient/verification/MC5_5_correct.tla diff --git a/docs/spec/lightclient/MC5_5_faulty.tla b/docs/spec/lightclient/verification/MC5_5_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC5_5_faulty.tla rename to docs/spec/lightclient/verification/MC5_5_faulty.tla diff --git a/docs/spec/lightclient/MC5_7_faulty.tla b/docs/spec/lightclient/verification/MC5_7_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC5_7_faulty.tla rename to docs/spec/lightclient/verification/MC5_7_faulty.tla diff --git a/docs/spec/lightclient/MC7_5_faulty.tla b/docs/spec/lightclient/verification/MC7_5_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC7_5_faulty.tla rename to docs/spec/lightclient/verification/MC7_5_faulty.tla diff --git a/docs/spec/lightclient/MC7_7_faulty.tla b/docs/spec/lightclient/verification/MC7_7_faulty.tla similarity index 100% rename from docs/spec/lightclient/MC7_7_faulty.tla rename to docs/spec/lightclient/verification/MC7_7_faulty.tla diff --git a/docs/spec/lightclient/verification.md b/docs/spec/lightclient/verification/verification.md similarity index 100% rename from docs/spec/lightclient/verification.md rename to docs/spec/lightclient/verification/verification.md