Merge `enhancement/complete-chain-sync-program-based` of pull request #93 into `master`
Complete the specification of the chain synchronization protocol
Home /
Input Output /
ouroboros-high-assurance
Nov 23, 5-6 AM (0)
Nov 23, 6-7 AM (0)
Nov 23, 7-8 AM (0)
Nov 23, 8-9 AM (0)
Nov 23, 9-10 AM (0)
Nov 23, 10-11 AM (0)
Nov 23, 11-12 PM (0)
Nov 23, 12-1 PM (0)
Nov 23, 1-2 PM (0)
Nov 23, 2-3 PM (0)
Nov 23, 3-4 PM (0)
Nov 23, 4-5 PM (0)
Nov 23, 5-6 PM (0)
Nov 23, 6-7 PM (0)
Nov 23, 7-8 PM (0)
Nov 23, 8-9 PM (0)
Nov 23, 9-10 PM (0)
Nov 23, 10-11 PM (0)
Nov 23, 11-12 AM (0)
Nov 24, 12-1 AM (0)
Nov 24, 1-2 AM (0)
Nov 24, 2-3 AM (0)
Nov 24, 3-4 AM (0)
Nov 24, 4-5 AM (0)
Nov 24, 5-6 AM (0)
Nov 24, 6-7 AM (0)
Nov 24, 7-8 AM (0)
Nov 24, 8-9 AM (0)
Nov 24, 9-10 AM (0)
Nov 24, 10-11 AM (0)
Nov 24, 11-12 PM (0)
Nov 24, 12-1 PM (0)
Nov 24, 1-2 PM (0)
Nov 24, 2-3 PM (0)
Nov 24, 3-4 PM (0)
Nov 24, 4-5 PM (0)
Nov 24, 5-6 PM (0)
Nov 24, 6-7 PM (0)
Nov 24, 7-8 PM (0)
Nov 24, 8-9 PM (0)
Nov 24, 9-10 PM (0)
Nov 24, 10-11 PM (0)
Nov 24, 11-12 AM (0)
Nov 25, 12-1 AM (0)
Nov 25, 1-2 AM (0)
Nov 25, 2-3 AM (0)
Nov 25, 3-4 AM (0)
Nov 25, 4-5 AM (0)
Nov 25, 5-6 AM (0)
Nov 25, 6-7 AM (0)
Nov 25, 7-8 AM (0)
Nov 25, 8-9 AM (0)
Nov 25, 9-10 AM (0)
Nov 25, 10-11 AM (0)
Nov 25, 11-12 PM (0)
Nov 25, 12-1 PM (0)
Nov 25, 1-2 PM (0)
Nov 25, 2-3 PM (0)
Nov 25, 3-4 PM (0)
Nov 25, 4-5 PM (0)
Nov 25, 5-6 PM (0)
Nov 25, 6-7 PM (0)
Nov 25, 7-8 PM (0)
Nov 25, 8-9 PM (0)
Nov 25, 9-10 PM (0)
Nov 25, 10-11 PM (0)
Nov 25, 11-12 AM (0)
Nov 26, 12-1 AM (0)
Nov 26, 1-2 AM (0)
Nov 26, 2-3 AM (0)
Nov 26, 3-4 AM (0)
Nov 26, 4-5 AM (0)
Nov 26, 5-6 AM (0)
Nov 26, 6-7 AM (0)
Nov 26, 7-8 AM (0)
Nov 26, 8-9 AM (0)
Nov 26, 9-10 AM (0)
Nov 26, 10-11 AM (0)
Nov 26, 11-12 PM (0)
Nov 26, 12-1 PM (0)
Nov 26, 1-2 PM (0)
Nov 26, 2-3 PM (0)
Nov 26, 3-4 PM (0)
Nov 26, 4-5 PM (0)
Nov 26, 5-6 PM (0)
Nov 26, 6-7 PM (0)
Nov 26, 7-8 PM (1)
Nov 26, 8-9 PM (7)
Nov 26, 9-10 PM (2)
Nov 26, 10-11 PM (0)
Nov 26, 11-12 AM (0)
Nov 27, 12-1 AM (0)
Nov 27, 1-2 AM (0)
Nov 27, 2-3 AM (0)
Nov 27, 3-4 AM (0)
Nov 27, 4-5 AM (0)
Nov 27, 5-6 AM (0)
Nov 27, 6-7 AM (0)
Nov 27, 7-8 AM (0)
Nov 27, 8-9 AM (0)
Nov 27, 9-10 AM (0)
Nov 27, 10-11 AM (0)
Nov 27, 11-12 PM (0)
Nov 27, 12-1 PM (0)
Nov 27, 1-2 PM (0)
Nov 27, 2-3 PM (0)
Nov 27, 3-4 PM (0)
Nov 27, 4-5 PM (0)
Nov 27, 5-6 PM (0)
Nov 27, 6-7 PM (0)
Nov 27, 7-8 PM (0)
Nov 27, 8-9 PM (0)
Nov 27, 9-10 PM (0)
Nov 27, 10-11 PM (0)
Nov 27, 11-12 AM (0)
Nov 28, 12-1 AM (0)
Nov 28, 1-2 AM (0)
Nov 28, 2-3 AM (0)
Nov 28, 3-4 AM (0)
Nov 28, 4-5 AM (0)
Nov 28, 5-6 AM (0)
Nov 28, 6-7 AM (0)
Nov 28, 7-8 AM (0)
Nov 28, 8-9 AM (0)
Nov 28, 9-10 AM (0)
Nov 28, 10-11 AM (0)
Nov 28, 11-12 PM (0)
Nov 28, 12-1 PM (0)
Nov 28, 1-2 PM (1)
Nov 28, 2-3 PM (1)
Nov 28, 3-4 PM (0)
Nov 28, 4-5 PM (1)
Nov 28, 5-6 PM (0)
Nov 28, 6-7 PM (0)
Nov 28, 7-8 PM (0)
Nov 28, 8-9 PM (2)
Nov 28, 9-10 PM (0)
Nov 28, 10-11 PM (0)
Nov 28, 11-12 AM (0)
Nov 29, 12-1 AM (0)
Nov 29, 1-2 AM (0)
Nov 29, 2-3 AM (0)
Nov 29, 3-4 AM (0)
Nov 29, 4-5 AM (0)
Nov 29, 5-6 AM (0)
Nov 29, 6-7 AM (0)
Nov 29, 7-8 AM (0)
Nov 29, 8-9 AM (0)
Nov 29, 9-10 AM (0)
Nov 29, 10-11 AM (0)
Nov 29, 11-12 PM (0)
Nov 29, 12-1 PM (0)
Nov 29, 1-2 PM (0)
Nov 29, 2-3 PM (0)
Nov 29, 3-4 PM (0)
Nov 29, 4-5 PM (0)
Nov 29, 5-6 PM (0)
Nov 29, 6-7 PM (0)
Nov 29, 7-8 PM (0)
Nov 29, 8-9 PM (1)
Nov 29, 9-10 PM (0)
Nov 29, 10-11 PM (0)
Nov 29, 11-12 AM (0)
Nov 30, 12-1 AM (0)
Nov 30, 1-2 AM (0)
Nov 30, 2-3 AM (0)
Nov 30, 3-4 AM (0)
Nov 30, 4-5 AM (0)
Nov 30, 5-6 AM (0)
16 commits this week
Nov 23, 2023
-
Nov 30, 2023
Remove a superfluous empty line
Make the specification of `server_chains` more precise
Change `u` to `đť’ž`
Change `'p` to `'q` in the definition of `server_step`
Remove underscores from server phase identifiers
Drop sending the initial chain
The initial chain is known and therefore doesn’t need to be communicated. Also, it is likely that right after the initial intersection finding the chain has to be partially revised, making it even less useful to send the initial chain.
Correct the argument order of `client_main_loop`
Rename `client_chain_updates` to `client_chains`
Move and improve the text about `server_chains`
Get rid of the use of `smt`
`smt` doesn’t work in automated builds on GitHub.
Rename `server_chain_updates` to `server_chains`
Using the term “updates” may suggest that what the server receives are merely diffs instead of whole chains. The new identifier makes it clearer that from this channel the server gets chains.
Improve identifier `state_in_server_phase`
For the `Idle` phase, there is not just one state that the server can be in; so the above name is misleading. This function is about the state that the server is in at the beginning of a cycle. We call this now the base state and have chosen the new identifier accordingly.
Improve names of server phases
Change identifiers `*_program` to `*_main_loop`
Correct and simplify server program
This commit additionally includes the following changes:
* Cause rollback after `IntersectFound` to happen also when the server
chain hasn’t changed
* Streamline the conformance proof
* Turn the names of the universally quantified variables in the
conformance proof into single-letter variants
* Make the subproof of `program Server` conformance more robust by
removing the dependency on subgoals left over by an automated prover