Skip to content

Commit

Permalink
specs: blocksync spec under synchronization/blocksync
Browse files Browse the repository at this point in the history
  • Loading branch information
cason committed Nov 25, 2024
1 parent e07c99f commit d95d1da
Show file tree
Hide file tree
Showing 9 changed files with 3 additions and 6 deletions.
5 changes: 1 addition & 4 deletions specs/synchronization/README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
# Node Synchronization Protocols

- [Blocksync][blocksync]
- TODO: move to `synchronization/README.md`

[blocksync]: ../english/synchronization/README.md
- [Blocksync protocol](./blocksync/README.md)
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ In the section on [Issues](#issues) below we will discuss future improvements. W

We have formalized Blocksync in Quint.
To do so, we abstracted away many details not relevant to the understanding of the protocol.
The [specification](../../quint/specs/blocksync/) includes:
The [specification](./quint/) includes:

- Protocol functionality: main complexity in the client, where it maintains statuses, requests data, and feeds received data into consensus
- State machine: We have encoded two alternatives
Expand Down Expand Up @@ -193,7 +193,7 @@ I a request is served, the response message is put into the `responsesBuffer` to

### Invariants and temporal formulas

For details we refer to the [state machine in Quint](https://github.com/informalsystems/malachite/blob/main/specs/quint/specs/blocksync/bsyncStatemachine.qnt), and the [analysis documentation](https://github.com/informalsystems/malachite/blob/main/specs/quint/specs/blocksync/README.md).
For details we refer to the [state machine in Quint](./quint/bsyncStatemachine.qnt), and the [analysis documentation](./quint/README.md).

## Issues

Expand Down
File renamed without changes.
File renamed without changes.

0 comments on commit d95d1da

Please sign in to comment.