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

rust-spec/lightclient/README.md

@@ -18,10 +18,10 @@ The light client is decomposed into three components:
 
 ## Commit Verification
 
-The [English specification](verification/verification.md) describes the light client
+The [English specification](verification/verification_001_published.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/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).
+[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification_001_published.md#lcv-dist-safe1) and
+[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification_001_published.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.
 

rust-spec/lightclient/verification/Lightclient_A_1.tla

@@ -2,7 +2,7 @@
 (**
  * A state-machine specification of the lite client, following the English spec:
  *
- * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md
+ * ./verification_001_published.md
  *) 
 
 EXTENDS Integers, FiniteSets