Skip to content

Commit

Permalink
Revert "Merge back from master (#533)"
Browse files Browse the repository at this point in the history
This reverts commit 19622ce.
  • Loading branch information
greg-szabo committed Aug 24, 2020
1 parent 7740e56 commit 3878fd8
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 14 deletions.
6 changes: 1 addition & 5 deletions docs/spec/lightclient/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,7 @@ $DIR/apalache-tests/scripts/parse-logs.py --human .
```

The following table summarizes the experimental results. The TLA+ properties can be found in the
[TLA+ specification](verification/Lightclient_A_1.tla).
The experiments were run in an AWS instance equipped with 32GB
RAM and a 4-core Intel® Xeon® CPU E5-2686 v4 @ 2.30GHz CPU.
We write “✗=k” when a bug is reported at depth k, and “✓<=k” when
no bug is reported up to depth k.
[TLA+ specification](verification/Lightclient_A_1.tla).

![Experimental results](experiments.png)

Expand Down
18 changes: 9 additions & 9 deletions docs/spec/lightclient/verification/verification.md
Original file line number Diff line number Diff line change
Expand Up @@ -1179,15 +1179,15 @@ func Main (primary PeerID, lightStore LightStore, targetHeight Height)

[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md

[TMBC-HEADER-link]: #tmbc-header1
[TMBC-SEQ-link]: #tmbc-seq1
[TMBC-CorrFull-link]: #tmbc-corr-full1
[TMBC-Auth-Byz-link]: #tmbc-auth-byz1
[TMBC-TIME_PARAMS-link]: tmbc-time-params1
[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds1
[TMBC-VAL-CONTAINS-CORR-link]: tmbc-val-contains-corr1
[TMBC-VAL-COMMIT-link]: #tmbc-val-commit1
[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1
[TMBC-HEADER-link]: #tmbc-header.1
[TMBC-SEQ-link]: #tmbc-seq.1
[TMBC-CorrFull-link]: #tmbc-corr-full.1
[TMBC-Auth-Byz-link]: #tmbc-auth-byz.1
[TMBC-TIME_PARAMS-link]: tmbc-time-params.1
[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds.1
[TMBC-VAL-CONTAINS-CORR-link]: tmbc-val-contains-corr.1
[TMBC-VAL-COMMIT-link]: #tmbc-val-commit.1
[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit.1

[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md
[fork-detector]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/detection.md
Expand Down

0 comments on commit 3878fd8

Please sign in to comment.