new directory structure (#396)

informalsystems · Jun 30, 2020 · 45ee6b6 · 45ee6b6
1 parent 42ea5f5
commit 45ee6b6
Show file tree

Hide file tree

Showing 18 changed files with 5 additions and 5 deletions.
diff --git 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 → docs/spec/lightclient/detection/detection.md b/docs/spec/lightclient/detection.md → docs/spec/lightclient/detection/detection.md
diff --git a/docs/spec/lightclient/001bmc-apalache.csv → ...htclient/verification/001bmc-apalache.csv b/docs/spec/lightclient/001bmc-apalache.csv → ...htclient/verification/001bmc-apalache.csv
diff --git a/docs/spec/lightclient/Blockchain_A_1.tla → ...ghtclient/verification/Blockchain_A_1.tla b/docs/spec/lightclient/Blockchain_A_1.tla → ...ghtclient/verification/Blockchain_A_1.tla
diff --git a/docs/spec/lightclient/Lightclient_A_1.tla → ...htclient/verification/Lightclient_A_1.tla b/docs/spec/lightclient/Lightclient_A_1.tla → ...htclient/verification/Lightclient_A_1.tla
diff --git a/docs/spec/lightclient/MC4_3_correct.tla → ...ightclient/verification/MC4_3_correct.tla b/docs/spec/lightclient/MC4_3_correct.tla → ...ightclient/verification/MC4_3_correct.tla
diff --git a/docs/spec/lightclient/MC4_3_faulty.tla → ...lightclient/verification/MC4_3_faulty.tla b/docs/spec/lightclient/MC4_3_faulty.tla → ...lightclient/verification/MC4_3_faulty.tla
diff --git a/docs/spec/lightclient/MC4_4_faulty.tla → ...lightclient/verification/MC4_4_faulty.tla b/docs/spec/lightclient/MC4_4_faulty.tla → ...lightclient/verification/MC4_4_faulty.tla
diff --git a/docs/spec/lightclient/MC4_5_correct.tla → ...ightclient/verification/MC4_5_correct.tla b/docs/spec/lightclient/MC4_5_correct.tla → ...ightclient/verification/MC4_5_correct.tla
diff --git a/docs/spec/lightclient/MC4_5_faulty.tla → ...lightclient/verification/MC4_5_faulty.tla b/docs/spec/lightclient/MC4_5_faulty.tla → ...lightclient/verification/MC4_5_faulty.tla
diff --git a/docs/spec/lightclient/MC4_6_faulty.tla → ...lightclient/verification/MC4_6_faulty.tla b/docs/spec/lightclient/MC4_6_faulty.tla → ...lightclient/verification/MC4_6_faulty.tla
diff --git a/docs/spec/lightclient/MC4_7_faulty.tla → ...lightclient/verification/MC4_7_faulty.tla b/docs/spec/lightclient/MC4_7_faulty.tla → ...lightclient/verification/MC4_7_faulty.tla
diff --git a/docs/spec/lightclient/MC5_5_correct.tla → ...ightclient/verification/MC5_5_correct.tla b/docs/spec/lightclient/MC5_5_correct.tla → ...ightclient/verification/MC5_5_correct.tla
diff --git a/docs/spec/lightclient/MC5_5_faulty.tla → ...lightclient/verification/MC5_5_faulty.tla b/docs/spec/lightclient/MC5_5_faulty.tla → ...lightclient/verification/MC5_5_faulty.tla
diff --git a/docs/spec/lightclient/MC5_7_faulty.tla → ...lightclient/verification/MC5_7_faulty.tla b/docs/spec/lightclient/MC5_7_faulty.tla → ...lightclient/verification/MC5_7_faulty.tla
diff --git a/docs/spec/lightclient/MC7_5_faulty.tla → ...lightclient/verification/MC7_5_faulty.tla b/docs/spec/lightclient/MC7_5_faulty.tla → ...lightclient/verification/MC7_5_faulty.tla
diff --git a/docs/spec/lightclient/MC7_7_faulty.tla → ...lightclient/verification/MC7_7_faulty.tla b/docs/spec/lightclient/MC7_7_faulty.tla → ...lightclient/verification/MC7_7_faulty.tla
diff --git a/docs/spec/lightclient/verification.md → .../lightclient/verification/verification.md b/docs/spec/lightclient/verification.md → .../lightclient/verification/verification.md