π Wave-20: handshake fingerprint + concurrent Add/Remove#724
Merged
Conversation
β¦move Lane A β L-CHAT-1-handshake (CR-CHAT-01): handshake_fingerprint.rs (343 lines) + 10 tests HSF-01..10 (responder-swap, role-flip, suite-downgrade, truncation, length-shift, empty-field, determinism, CT flip, len const, green). Lane B β L-CHAT-3-add (CR-CHAT-03): concurrent_add_remove.rs (419 lines) + 10 tests CAR-01..10 (add-after-remove ghost, remove-after-add resurrection, dup-add, dup-remove, self-remove+update, empty-set, order-independence, tie-break, dup sort-key, green). Coq Wave-20: Section TrinityChatWave20 with INV-CHAT-110..116 + 2 helpers β 158 Qed total / 0 Admitted / 0 new axioms (5 cumulative unchanged). Falsifier 1800 β 1900: +50 handshake_fingerprint + +50 concurrent_add_remove, 38 categories all at 100%. DENY_PATTERNS in CR-CHAT-06/src/injection.rs extended with ~360 W20 keywords. ROADMAP.md updated: status β 310 tests Β· 25/25 e2e Β· 1900/1900 falsifier Β· 38 cats Β· 158 Coq Qed. W20 row promoted (bold), W19 demoted. Wave-20 detail section added before Wave-19. ASPIRATIONAL window slides to W21..W25. Verified [VERIFIED]: - cargo test β 310 / 0 - e2e_chat_25 β 25 / 25 pass - falsifier_runner β 1900 / 1900, 38 cats @ 100% - cargo clippy β clean - coqc Trinity_Chat.v β silent exit 0; grep -cE 'Qed\.' β 158; Admitted β 0 R5: 0 unsafe Β· 0 monoliths Β· 0 .sh Β· 0 new axioms Β· L-ARCH-001 preserved.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #723
π Trinity Chat β Wave-20
Two new threat-model lanes shipped per the W19 ROADMAP forward plan:
Lane A β
L-CHAT-1-handshake(CR-CHAT-01) βhandshake_fingerprint.rs(343 lines).
HandshakeFingerprint::compute(initiator_lt, responder_lt, initiator_pre, responder_pre, kem_ciphertext, suite_and_version) -> Result<Self, HandshakeError>,HSF_LEN = 32,HSF_DOMAIN = b"trios-chat-handshake-fingerprint-v1\0",constant-time
eq_ctviasubtle::ConstantTimeEq, length-prefixedabsorb_taggedper-field domain separator. 10 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(CR-CHAT-03) βconcurrent_add_remove.rs(419 lines).
apply_concurrent(base_members, proposals)withdeterministic priorities
PRI_UPDATE = 0 < PRI_REMOVE = 1 < PRI_ADD = 2,ties broken by
(priority, hash_id, sort_key). ErrorsRemoveNonMember | AddExisting | UpdateNonMember | DuplicateSortKey.10 tests CAR-01..10 (add-after-remove ghost, remove-after-add
resurrection, dup-add, dup-remove, self-remove+update, empty-set,
order-independence, tie-break, dup sort-key, green).
Coq Wave-20
Section TrinityChatWave20adds INV-CHAT-110..116 plus 2 helperlemmas (
all_nonzero_valid_20,update_before_add_20). All proofsconstructive over
PropClass20::{PUpdate20, PRemove20, PAdd20},records
TranscriptLens20andDelta20, with variablehsf_of_20 : nat -> nat -> nat -> nat -> nat -> nat -> nat.10 new
Qed.β 158Qed.total, 0Admitted., 0 new axioms(cumulative 5 axioms unchanged:
ss_kp_injective,dh_step_fresh,dh_post_history_independent,hybrid_kem_non_degenerate,sn_hash_sym).Falsifier 1800 β 1900
+50
handshake_fingerprint(PI-HSF-001..050) + +50concurrent_add_remove(PI-CAR-001..050). 38 attack categories all at 100 %, G-C10 thresholds
met for every category (β₯95 % non-direct, β₯90 % direct).
DENY_PATTERNSin
CR-CHAT-06/src/injection.rsextended with ~360 W20 keywords.Anchor extended
Verified [VERIFIED]
cargo test(12 chat crates + harness)cargo run -q -p trios-chat --bin e2e_chat_25cargo run -q -p trios-chat --bin falsifier_runnercargo clippy --all-targets -- -D warningscoqc crates/trios-chat/proofs/chat/Trinity_Chat.vgrep -cE "Qed\." Trinity_Chat.vgrep -cE "^\s*Admitted\." Trinity_Chat.vCompliance
crates/trios-chat/rings/CR-CHAT-NN/..shfiles anywhere incrates/trios-chat/.Closes #723.unsafe, clippy-D warningsclean,coqcsilent.ROADMAP.md updated: status β
310 tests Β· 25/25 e2e Β· 1900/1900 falsifier Β· 38 categories Β· 158 Coq Qed / 0 Admitted. W20 row promoted (bold),W19 demoted. Wave-20 detail section added before Wave-19.
ASPIRATIONAL window slides to W21..W25.
Branched from
d601a58(post-W19 main HEAD); commit on this branch tipis
8116c0b.