docs: ABFT corrections

[cusma]

Summary

This PR consolidates the changes proposed in: #199, #200, #202, #206, and #210.

It corrects the normative ABFT section based on some changes proposed in those PRs and some new findings; all have been AI-reviewd against the reference implementation (go-algorand 88fe542f, which is assumed correct) and kept or discarded accordingly.

The changes introduce a the following new concepts:

• History H: the player state gains an ordered history of events and outputs.
• Threshold freshness: a per-round ordering (cert, then later period, next over soft, bottom over value); a bundle is observed only if fresher than every threshold observed before it. Replaces the set-membership model, which could not express that a verified but non-fresher quorum is neither relayed nor staged.
• Summary C(S, r, p): whether a bottom next threshold formed, and the latest non-bottom value; filtering, recovery, and fast recovery select their carried value from it, correcting the previous use of the pinned value v̄ (now used for payload relay only).

Garbage collection section is deliberately kept, corrected in place. AI-review suggested a full removal: it defines no externally visible behavior, and the reference implementation itself retains more than the transition mandates.

Suggested file review order:

1. abft-notation.md;
2. abft-parameters;
3. abft-participants.md;
4. abft-ledger.md;
5. abft-messages.md;
6. abft-state-machine.md;
7. abft-player-state.md;
8. abft-relay-rules.md;
9. abft-state-transitions.md;
10. abft-broadcast-rules.md.

Validation

• I ran make ci, or make check with no version-drift warnings.
• I checked the deployment preview when the change affects rendering.

[Copilot]

Pull request overview

This PR consolidates and corrects the normative ABFT specification updates from #199, #200, #202, #206, and #210, aligning the written protocol rules (state, relay, broadcast, messages, and parameters) with the stated reference implementation and introducing new normative concepts around history, threshold freshness, and summary-derived carried values.

Changes:

• Extend the player state with history (H), introduce threshold freshness ordering, and add derived functions/summary ((\rho), (C(S,r,p))) that drive carried-value selection.
• Update relay/broadcast/state-transition rules to reflect the revised notions of observation, replay/relay behavior, and timeout-driven step progression.
• Update message formats and cryptographic domain separation/encoding references, plus parameter/timeouts clarifications.

Reviewed changes

Copilot reviewed 11 out of 11 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/abft/abft-state-transitions.md	Updates round/period/step transitions, GC, and adds (H) to state transitions.
src/abft/abft-state-machine.md	Clarifies timeout event notation using a generic (T) instead of (\lambda).
src/abft/abft-relay-rules.md	Revises vote/bundle/proposal relay rules and observation semantics.
src/abft/abft-player-state.md	Extends the state tuple with history (H), adds freshness/summary concepts, and refines (\mu,\sigma,\rho,C).
src/abft/abft-participants.md	Tightens wording and notation around signing behavior/output existence.
src/abft/abft-parameters.md	Updates parameter definitions and timeout formulas/ranges.
src/abft/abft-notation.md	Refines the meaning of context tuple components, especially step semantics.
src/abft/abft-messages.md	Adds domain-separator/encoding references and updates vote/bundle/proposal/seed definitions.
src/abft/abft-ledger.md	Adds a definition for consensus parameters lookup in the ledger.
src/abft/abft-broadcast-rules.md	Updates broadcast/resync/filter/recovery/commitment rules to use the new carried-value and freshness concepts.
.rumdl.toml	Adds a per-file markdown-lint ignore for src/abft/abft-messages.md.

Suppressed comments (3)

src/abft/abft-relay-rules.md:85

• The transition for relaying/observing a vote uses (\Vote_k(r_k, p_k, s_k, v)) in the input and state update. For consistency with the vote definition (which includes the voter address), consider using (\Vote(I_k, r_k, p_k, s_k, v)) here too.

$$
N(S, L, \Vote_k(r_k, p_k, s_k, v))
= (S' \cup \\{\Vote_k(r_k, p_k, s_k, v)\\}, L', (\Vote_k^\ast(r_k, p_k, s_k, v),\ldots));
$$

src/abft/abft-relay-rules.md:91

• The transition for relaying a vote without observing it similarly uses (\Vote_k(r_k, p_k, s_k, v)) in the event term; it should match the clarified vote notation that includes the voter identity.

$$
N(S, L, \Vote_k(r_k, p_k, s_k, v)) = (S, L, (\Vote_k^\ast(r_k, p_k, s_k, v))).
$$

src/abft/abft-relay-rules.md:78

• The transition for ignoring a vote uses (\Vote_k(r_k, p_k, s_k, v)); after clarifying the vote’s identity (including the voter address), the event term here should match the (\Vote(I, r, p, s, v)) notation used in the message definition.

$$
N(S, L, \Vote_k(r_k, p_k, s_k, v)) = (S, L, \epsilon)
$$

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 11 out of 11 changed files in this pull request and generated 1 comment.

Suppressed comments (2)

src/abft/abft-broadcast-rules.md:194

• Same as above: the third component of N should be a sequence; this case should return a singleton sequence containing the vote.

N(S, L, t(\FilterTimeout(p), p)) = (S', L, \Vote(I, r, p, \Soft, \mu));

src/abft/abft-participants.md:41

• Inline math around (\Sign) includes an extra escape/space sequence ("\( \Sign\ \)") that is hard to read and may render inconsistently. Prefer the standard form used elsewhere in the document.

Not every input to \\( \Sign\ \\) produces an output \\( y \\).

[Copilot]

Pull request overview

Copilot reviewed 11 out of 11 changed files in this pull request and generated 1 comment.

Suppressed comments (5)

src/abft/abft-relay-rules.md:34

• The section defines ( \Vote_k = \Vote(I_k, r_k, p_k, s_k, v) ) as a vote, but later treats ( \Vote_k ) as possibly being an equivocation (and a “second equivocation”). This is internally inconsistent and makes the ignore conditions ambiguous.

On receiving a vote \\( \Vote_k = \Vote(I_k, r_k, p_k, s_k, v) \\) a player

src/abft/abft-broadcast-rules.md:176

• The filtering rule bullet ends with “; and” but the next bullet is an “otherwise” case. The trailing “and” is a grammatical artifact and makes the rule list harder to read.

- if \\( p_\mu < p \\), the player broadcasts* \\( \Vote(I, r, p, \Soft, \mu) \\)
  exactly when \\( c = \mu \\); and

src/abft/abft-state-transitions.md:97

• The Garbage Collection transition is described as only removing old votes/payloads, but the equation also changes (r), (p), and resets (s) to (\Soft) while mixing in primed components ((V'), (P'), (\bar v'), (L')) that aren’t defined in this section. This makes the transition ambiguous as a standalone rule.

$$
N((r_0, p_0, s, \bar{s}, V, P, \bar{v}, H), L, \ldots)
= ((r, p, \Soft, s, V' \setminus V^\ast_{r, p}, P' \setminus P^\ast_{r, p}, \bar{v}', H'), L', \ldots)
$$

src/abft/abft-state-machine.md:29

• This paragraph says an unprimed output component is unchanged “except the history (H), which every transition extends.” But many transition equations elsewhere use an unprimed state (S) on the RHS to mean “no state change” (e.g., ignores), which is inconsistent if (S) includes (H). Clarify the shorthand so equations aren’t read as keeping (H) unchanged.

In transition equations, a primed symbol denotes a component's value after the
transition; an unprimed symbol in the output asserts that the component is
unchanged, except the history \\( H \\)
([Player State](./abft-player-state.md)), which every transition extends.

src/abft/abft-player-state.md:93

• The definition of (V_{r,p,0}) (immediately above this paragraph) uses unbound variables (I) and (v) on the left-hand side of the set builder, so it’s not a well-formed definition of the subset of accepted proposal votes at ((r,p)).

Let \\( z_k \\) be the raw selection-VRF output in \\( \Vote_k \in V_{r, p, 0} \\)
and \\( w_k \\) its weight. Its priority is