docs: Hashgraph Invariants#25966
Conversation
Signed-off-by: Michael Heinrichs <netopyr@users.noreply.github.com>
Signed-off-by: Michael Heinrichs <netopyr@users.noreply.github.com>
Signed-off-by: Michael Heinrichs <netopyr@users.noreply.github.com>
# Conflicts: # platform-sdk/docs/consensus-layer/invariants/INV-001-roundcreated-monotonic-along-ancestry.md
Signed-off-by: Michael Heinrichs <netopyr@users.noreply.github.com>
|
Merging to
After your PR is submitted to the merge queue, this comment will be automatically updated with its status. If the PR fails, failure details will also be posted here |
✅ Snyk checks have passed. No issues have been found so far.
💻 Catch issues earlier using the plugins for VS Code, JetBrains IDEs, Visual Studio, and Eclipse. |
| --- | ||
| type: invariant | ||
| id: INV-017 | ||
| title: The active address book never moves backward — roster and stake changes apply forward-only |
There was a problem hiding this comment.
I don't think this invariant makes a lot of sense. We can have address book A, then address book B, then address book C, which is exactly the same as address book A. At that point, what is a real difference between saying that we have moved forward to address book C or reused address book A?
I would probably state something about each round having well defined address book, I don't think that saying that "sequence of address books is monotonic" makes mathematical sense.
poulok
left a comment
poulok
left a comment
There was a problem hiding this comment.
I got to all the files up through INV-004. I'll pickup with INV-005 in the next round. Looking good so far!
|
|
||
| ## Statement | ||
|
|
||
| If an honest event becomes ancient before reaching consensus, every honest node agrees it is stale: it is assigned no consensus order or timestamp on any node. No node orders an event that another node treats as stale. |
There was a problem hiding this comment.
I think the statement needs to be a bit more specific. Not all honest nodes are guaranteed to ever know about a stale event, and a node cannot agree on something it does not know about. The stale-events.md concept document says this, but it should be said here also in the statement:
Because a stale event is by definition an event that does not reach
consensus and never will, stale event reports are **not deterministic
across nodes**.
I suggest:
If an honest event becomes ancient before reaching consensus, every honest node that knows of the event agrees it is stale: it is assigned no consensus order or timestamp on any node. No node orders an event that another node treats as stale.
|
|
||
| ## Change risk | ||
|
|
||
| - **A node-local ancient boundary** — deriving the boundary from per-node state so two nodes age out different events. |
There was a problem hiding this comment.
I can see this statement being a little confusing. The non ancient boundary is calculated locally albeit from the state that every node is guaranteed to reach deterministically. This is even stated above: The birth round is immutable and gossiped, and the boundary minNonAncientRound is a function of the agreed round state;. The key is that the determination must never be based on a non-deterministic per-node state.
| - **Ordering an event past the boundary on one node** while another has already discarded it as stale. | ||
| - **Mutating an event's birth round** after creation, so the staleness test gives different answers on different nodes. | ||
|
|
||
| Any change that lets one correct node order an event another has declared stale forks the ordered stream. |
There was a problem hiding this comment.
Should we add something about causing an ISS here so that it links to any scenarios we add later?
| - [Reconnect](../topics/reconnect.md) — `StateLifecycleManager.createStateFrom` / `initWithState` | ||
| and `onStateInitialized` with `InitTrigger.RECONNECT`; resets the pre-handle contract baseline. | ||
| - Invariants / Decisions: _(TBD: catalogs not yet populated)_. | ||
| - Invariants: INV-005 (every honest event eventually reaches consensus or becomes stale), INV-004 (staleness is agreed by all nodes) — see the [pre-handle → consensus-or-stale contract](#every-pre-handled-event-reaches-consensus-or-goes-stale) above. |
There was a problem hiding this comment.
Related to my comment on INV-004, the statement "staleness is agreed by all nodes" could be a little misleading.
| - Topics: [wiring-framework.md](wiring-framework.md), [event-creator.md](event-creator.md), [gossip.md](gossip.md), [restart-and-pces.md](restart-and-pces.md), [reasons-not-to-gossip.md](reasons-not-to-gossip.md). | ||
| - Tunables: [../../tunables.md](../../tunables.md). | ||
| - Invariants: [TBD: INV-NNN once invariants.md catalog populates]. | ||
| - Invariants: INV-005 — every honest event eventually reaches consensus or becomes stale (what the throttling reactions ultimately protect). |
There was a problem hiding this comment.
What does this invariant have to do with throttling?
| [`branching.md`](branching.md), | ||
| [`strongly-seeing.md`](strongly-seeing.md), | ||
| [`coin-rounds.md`](coin-rounds.md). | ||
| - Invariants: INV-006 (every round eventually has at least one judge), INV-007 (all deciders of a round agree on its judge set), INV-014 (every round has a supermajority of judges). |
There was a problem hiding this comment.
Hmm, it seems that INV-014 supercedes INV-006 🤔
| [`../architecture/topics/event-intake.md`](../architecture/topics/event-intake.md), | ||
| [`../architecture/topics/gossip.md`](../architecture/topics/gossip.md). | ||
| - Sibling concept: [`event-lifecycle.md`](event-lifecycle.md). | ||
| - Invariants: INV-004 (staleness is agreed by all nodes — the *fate*, not the local stale-report stream this concept calls non-deterministic), INV-005 (every honest event eventually reaches consensus or becomes stale). |
There was a problem hiding this comment.
Ahhh the clarification here about the stale "fate" of an event, not the reporting of the stale event, helps a lot. I think this clarification should be added to the invariant wording and possibly the summary used when referencing the invariant.
| type: invariant | ||
| id: INV-001 | ||
| title: roundCreated is monotonic along ancestry — a parent's round never exceeds its child's | ||
| title: Voting round is monotonic along ancestry — a parent's round never exceeds its child's |
There was a problem hiding this comment.
The filename should also be updated to use the term "voting round"
| --- | ||
| type: invariant | ||
| id: INV-002 | ||
| title: Consensus order is agreed by all nodes — any two nodes that order an event report the same order |
|
|
||
| The invariant is at risk whenever consensus order is made to depend on something not shared identically across nodes. Mechanisms to defend against: | ||
|
|
||
| - **Node-local state in the ordering computation** — breaking ties in `before` with a value that differs between nodes (wall-clock arrival time, local receive sequence, peer identity). The tie-break must be a deterministic function of the events alone. |
There was a problem hiding this comment.
| - **Node-local state in the ordering computation** — breaking ties in `before` with a value that differs between nodes (wall-clock arrival time, local receive sequence, peer identity). The tie-break must be a deterministic function of the events alone. | |
| - **Node-local state in the ordering computation** — breaking ties in `before` with a value that differs between nodes (wall-clock arrival time, local receive sequence, peer identity). The tie-break must be a deterministic function of the immutable event properties alone. |
poulok
left a comment
poulok
left a comment
There was a problem hiding this comment.
I noticed these files do not wrap long lines. Spotless passed, but still there are very long single lines. I'm not sure what happened but it would be nice to not have an entire paragraph on a single line for review purposes.
There was a problem hiding this comment.
I think we agreed to use the term "consensus" instead of "decided" for consistency.
|
|
||
| ## Statement | ||
|
|
||
| Under the algorithm's standard assumptions, every event created by an honest node eventually reaches a final fate — a consensus order and timestamp, or staleness — with probability 1. No honest event remains forever undecided. |
There was a problem hiding this comment.
Isn't this also true of dishonest events? (btw, it's a little strange to think of honest and dishonest events rather than nodes). Maybe not if we define these fates as only applying to events that at in the hashgraph it works - and by "in the hashgraph" i mean has linkage via parents to the conceptual hashgraph formed by the network, not the hashgraph module.
|
|
||
| It is a theorem of the hashgraph consensus algorithm that an event created by an honest node eventually reaches consensus (with probability 1), where reaching consensus means it either has a consensus timestamp and consensus order agreed to by all nodes, or it becomes stale and all nodes agree it is stale. | ||
|
|
||
| Termination rests on two facts. First, virtual voting on each round's witnesses always terminates: a coin round periodically injects a vote drawn from a source no adversary can predict (the `coin`), which with probability 1 eventually breaks any asynchronous stalemate the network might sustain. Second, once witnesses are decided the round has judges, against which every event is either ordered or — if it fails to reach consensus before the advancing ancient boundary — declared stale. The theorem is conditional on the algorithm's standard assumptions (honest stake exceeds two-thirds; an honest event eventually reaches every honest node; and the rest). |
There was a problem hiding this comment.
Is one of the "standard assumptions" that no single node has a super majority of network stake? Is there a list of all "standard assumptions"?
| - **A voting rule that need not terminate** — one without the coin's eventual tie-break. | ||
| - **An ancient boundary that never advances**, leaving non-consensus events neither ordered nor aged out. | ||
|
|
||
| Any change under which an honest event can stay undecided forever defeats liveness: consensus stalls and no transactions finalize. |
There was a problem hiding this comment.
I'm not sure this is true. If an event can stay undecided forever, it does not follow that consensus stalls and no transactions finalize.
|
|
||
| ## Statement | ||
|
|
||
| With probability 1, every round eventually has at least one judge, and this continues for an infinite number of rounds. Round elections do not dry up: the supply of judges that anchors ordering and timestamps never runs out. |
There was a problem hiding this comment.
Assuming the network is live, i.e. that it is connected and alive. Do you think that needs to be added here?
4 participants
Description:
This PR adds several invariants from the Hashgraph algorithm and fixes some links and minor formatting issues.
Related issue(s):
Fixes #25352