🌊 Wave-20 sub-tracker — handshake fingerprint + concurrent Add/Remove

[gHashTag]

🌊 Wave-20 sub-tracker — handshake fingerprint + concurrent Add/Remove

Anchor: φ² + φ⁻² = 3 · TRINITY · CHAT · … · KEM-DECAP-ORACLE · TAG-STRIPPING · HANDSHAKE-FINGERPRINT · CONCURRENT-ADD-REMOVE

Parent EPIC: trinity-fpga#28
Branch: feat/trios-chat-wave20 (base = main, branched from W19 merge d601a58)
Cadence: 2 lanes · +20 tests · +100 falsifier · +10 Coq Qed · 0 new axioms · 0 unsafe · 0 monoliths · 0 .sh.

Lanes

Lane A — L-CHAT-1-handshake (R-CHAT-1 / CR-CHAT-01)

Handshake-transcript fingerprinting with role / suite / length-prefixed domain separation, constant-time equality, and explicit empty-field rejection.

• crates/trios-chat/rings/CR-CHAT-01/src/handshake_fingerprint.rs (343 lines)
• API: HandshakeFingerprint::compute(initiator_lt, responder_lt, initiator_pre, responder_pre, kem_ciphertext, suite_and_version) -> Result<Self, HandshakeError>
• Consts: HSF_LEN = 32, HSF_DOMAIN = b"trios-chat-handshake-fingerprint-v1\0"
• CT equality via subtle::ConstantTimeEq (HandshakeFingerprint::eq_ct)
• Tests HSF-01..10: responder-swap, role-flip, suite-downgrade, truncation, length-shift, empty-field rejection, determinism, CT single-bit flip, length const, green.

Lane B — L-CHAT-3-add (R-CHAT-11 / CR-CHAT-03)

Deterministic concurrent Add/Remove/Update ordering with no ghost-member resurrection.

• crates/trios-chat/rings/CR-CHAT-03/src/concurrent_add_remove.rs (419 lines)
• API: apply_concurrent(base_members: &BTreeSet<Leaf>, proposals: &[Proposal]) -> Result<MembershipDelta, ConcurrencyError>
• Priorities: PRI_UPDATE = 0 < PRI_REMOVE = 1 < PRI_ADD = 2; ties broken by (priority, hash_id, sort_key).
• Errors: RemoveNonMember, AddExisting, UpdateNonMember, DuplicateSortKey.
• Tests CAR-01..10: add-after-remove ghost, remove-after-add resurrection, dup-add, dup-remove, self-remove-with-update, empty-set, order-independence, tie-break, duplicate sort-key, green.

Coq Wave-20

Section TrinityChatWave20 adds INV-CHAT-110..116 plus 2 helper lemmas (all_nonzero_valid_20, update_before_add_20):

• INV-CHAT-110 inv_chat_110_hsf_determinism — hsf_of_20 a..f = hsf_of_20 a..f
• INV-CHAT-111 inv_chat_111_hsf_swap_detected — different output ⟹ inputs differ
• INV-CHAT-112 inv_chat_112_empty_field_invalid — empty init_lt_len_20 ⟹ transcript_valid_20 = false
• INV-CHAT-113 inv_chat_113_update_before_remove — priority_20 PUpdate20 < priority_20 PRemove20
• INV-CHAT-114 inv_chat_114_remove_before_add — priority_20 PRemove20 < priority_20 PAdd20
• INV-CHAT-115 inv_chat_115_empty_set_no_change — final_size_20 (MkDelta20 n 0 0) = n
• INV-CHAT-116 inv_chat_116_add_after_remove_size_neutral — final_size_20 (MkDelta20 (S n) 1 1) = S n

158 Qed. total · 0 Admitted. · 0 new axioms (cumulative 5 axioms unchanged).

Verification gates (will be re-run in PR CI)

Gate	Expected
cargo test (12 chat crates + harness)	310 / 0
cargo run -q -p trios-chat --bin e2e_chat_25	25 / 25 pass
cargo run -q -p trios-chat --bin falsifier_runner	1900 / 1900, 38 cats @ 100%
cargo clippy --all-targets -- -D warnings	clean
coqc Trinity_Chat.v	silent, exit 0 · grep -cE "Qed\." → 158 · grep -cE "^\s*Admitted\." → 0

R5 honesty tags

• All counts above are [VERIFIED] locally as of this branch's tip (pre-push).
• Anchor extension is [DERIVED] from the two lanes shipped.
• W21..W25 are [ASPIRATIONAL] in the ROADMAP.