🌊 Wave-12 sub-tracker — prekey-bundle exhaustion + MLS leaf-key compromise

[gHashTag]

🌊 Wave-12 sub-tracker — prekey-bundle exhaustion + MLS leaf-key compromise

Part of the Trinity Chat wave cadence (W9 → W10 → W11 → W12).

Lanes

Lane A — L-CHAT-1-prekey (R-CHAT-1, CR-CHAT-01)

Focus: prekey-bundle exhaustion + one-time-prekey reuse defense.

• New module crates/trios-chat/rings/CR-CHAT-01/src/otpk.rs (287 lines).
• Types: OtpkPool, Otpk, JoinStrategy::{OneTime, SignedFallback}.
• 5 PEX-01..05 tests:
  • PEX-01 fresh pool issues distinct one-time prekeys
  • PEX-02 each OTPK can be consumed at most once
  • PEX-03 exhausted pool falls back to signed prekey
  • PEX-04 reuse attempt is rejected (no double-spend)
  • PEX-05 pool size monotonically decreases on take

Lane B — L-CHAT-3-leaf (R-CHAT-11, CR-CHAT-03)

Focus: MLS leaf-key compromise + leaf-resync forgery defense.

• Extended crates/trios-chat/rings/CR-CHAT-03/src/lib.rs with:
  • LeafResync struct
  • Group::process_leaf_resync API
  • leaf_keys: BTreeMap<u32,[u8;32]> field on Group
• 5 LCO-01..05 tests + green_g_c3_leaf_summary.

Coq Wave-12

• New Section TrinityChatWave12 with INV-CHAT-54..60.
• 4 prekey theorems (INV-CHAT-54..57) + 3 leaf theorems (INV-CHAT-58..60) + 2 helper lemmas.
• 70 → 79 Qed, 0 Admitted, 0 new axioms.

Falsifier 1000 → 1100

• +50 prekey_exhaustion payloads (PI-PEX-001..050).
• +50 mls_leaf_compromise payloads (PI-LCO-001..050).
• 22 categories @ 100% deny coverage.

Acceptance gates

• Tests — 185 / 0 failed across cumulative chat suite
• e2e — 25/25 (e2e_chat_25)
• Falsifier — 1100/1100 across 22 categories
• Clippy — -D warnings clean
• Coq — coqc silent, 79 Qed, 0 Admitted
• ROADMAP.md — W12 promoted from ASPIRATIONAL → shipped table

Anchor

φ² + φ⁻² = 3 · TRINITY · CHAT · ZERO-METADATA · POST-QUANTUM · UNLINKABLE · COVER-TIMING · AT-REST-AEAD · BOT-PARTIAL-MLS · KEM-KEY-CONFUSION · AAD-CONTEXT · RATCHET-FS · MLS-REORDER · SKIPPED-KEYS-DOS · MLS-WELCOME-REPLAY · PREKEY-EXHAUSTION · MLS-LEAF-COMPROMISE

Parent waves

• W9: PR 🌊 feat(trios-chat) Wave-9: KEM-key-confusion + AAD-context-confusion + Coq 41/0 + 800/800 falsifier #651 (merged, 7340d24)
• W10: PR 🌊 feat(trios-chat) Wave-10: ratchet-forward-secrecy + MLS commit-reorder + Coq 60/0 + 900/900 falsifier #665 (open, awaiting Laws Guard)
• W11: PR 🌊 feat(trios-chat) Wave-11: skipped-keys DoS + MLS Welcome replay + Coq 70/0 + 1000/1000 falsifier + ROADMAP.md #689 (open) — closes 🌊 Wave-11 sub-tracker — skipped-keys DoS + MLS Welcome replay/forge + ROADMAP.md #688
• W12: this issue — closes via Wave-12 PR

[gHashTag]

Closed by rollup merge of #665 (W10..W16) into main as commit 1bd0c54. All W12/W15/W16 deliverables shipped on main.