Specify the reciprocal A.5 catch-up and define proposal_context

[germ-mark]

Resolves how a rotated party's PQ leaves catch up. The book stays the spec of intended behavior.

Spec:

• An A.5 re-keys the opener's receive-PQ group, and the session opens one when either leaf there lags: it presents an id other than its owner's current canonical id. A same-id refresh isn't a lag. The session never opens one while the side-band is wedged.
• A PQ leaf minted at A.3 is born under its owner's then-canonical id. Every other PQ leaf catches up over A.5 rounds, one per PQ group. First, the owner's own A.5 moves its leaf in the peer's send group through its Upd'. Then the peer's reciprocal A.5 moves the owner's own send-PQ leaf through the owner's responder Commit'.
• Races (a rotation while a round is in flight, or a responder whose rotation staple hasn't applied yet) cost one extra round, never a stall.
• A credential that a live PQ leaf still presents stays admissible past the history window until that leaf catches up. The A.3 founding pins become one instance of that rule (Group Rules rule 4).
• Until a leaf moves, its owner signs in that group with the key the leaf presents. A group joined from the A.3 KP′ is signed with KP′'s key, and moving one group's leaf never retires a key another group's leaf still presents.
• No new frame is added, updatePath commits never ride the staple, and each round still re-keys exactly one group.

Shipped anomaly note:

• The deployed Rust engine's trigger reads its own send-PQ leaf, which its own round can't move, so it re-opens A.5 every turn.
• It never opens the reciprocal round. A conforming peer heals it, because its responder Commit' does carry its credential.
• A deployed born-dedicated acceptor never catches up its leaf in the initiator's send-PQ group.
• Only the A.3 ids are pinned, so a leaf left behind for longer than the history window is stranded.
• Born-dedicated catch-up Upds are never committed by a host that folds only proposing != sender offers.
• Its A.3 join signs with the current key. After a rotation before the bind, that orphans the leaf once it answers any peer A.5, so a conforming peer defers a reciprocal A.5 until the peer's own A.5 has landed. That's a deployed-engine accommodation, costing at most one extra round.

A Fable review traced the design against both engines. It found the design sound, confirmed that a native peer heals a rotated Rust party, and its fixes are applied here. The PR also defines proposal_context.

Book-only, with an empty changeset. mdbook build passes. No mermaid fences changed.

🤖 Generated with Claude Code

[changeset-bot]

🦋 Changeset detected

Latest commit: 1d1b846

The changes in this PR will be included in the next version bump.

This PR includes changesets to release 0 packages

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Not sure what this means? Click here to learn what changesets are.

Click here if you're a maintainer who wants to add another changeset to this PR