🌊 Wave-32 — welcome_encrypted_group_info_aead + proposal_ref_collision (sub-tracker)

[gHashTag]

🌊 Wave-32 — welcome_encrypted_group_info_aead + proposal_ref_collision (sub-tracker)

Anchor: φ² + φ⁻² = 3

Sub-tracker for the Wave-32 of the trios-chat protocol — two fresh
threat-model lanes following the W7..W31 canonical cadence.

1. Background

Wave-31 (PR #771,
merged 756cf35) closed KeyPackage init_key reuse + External PSK
identifier provenance, bringing the threat coverage to 60
categories / 288 Coq Qed / ~528 tests. Two uncovered MLS surfaces
remain right under the existing W31 ones:

1. Welcome encrypted_group_info AEAD envelope (RFC 9420 §12.4.3)
   — a hostile sender can publish a Welcome whose
   encrypted_group_info AEAD envelope carries a non-12-byte
   nonce, a sub-tag ciphertext, a foreign group_id, a stale
   epoch, a previously-used (group_id, epoch, nonce) triple
   (catastrophic AEAD nonce-misuse), or the all-zero AEAD nonce.
2. ProposalRef collision (RFC 9420 §12.1.1) — a hostile member
   can inject a Proposal carrying a non-canonical proposal_ref
   length, an empty proposal_id, a proposal_ref never
   provisioned in the local commit ledger, a foreign group_id,
   a stale epoch, a replayed (group_id, epoch, proposal_ref)
   triple, or the all-zero proposal_ref.

Both are MLS hazards independently observable from existing
material; both fit the standard rule-shape of W12..W31.

2. Hypothesis (Gate G1 — Popper)

H = "the W32 validators reject every malformed (WelcomeAeadEnvelope,
view) / (ProposalReference, view) pair listed in §3" is false iff
there exists an input in the falsification witness corpus that
returns Ok(()) despite violating one of the rules per lane.

Refutation observable: a single failing #[test] fn wegi_… /
#[test] fn pref_… or a single Lemma counter_… constructive
counter-example would falsify H.

3. Method — lane decomposition

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

• File:
  crates/trios-chat/rings/CR-CHAT-01/src/welcome_encrypted_group_info_aead.rs
  (≈270 lines).
• Public API:
  validate_welcome_aead_envelope(envelope: &WelcomeAeadEnvelope, view: &WelcomeAeadView) -> Result<(), WelcomeAeadError>.
• Consts WELCOME_GROUP_INFO_AEAD_NONCE_LEN = 12,
  WELCOME_GROUP_INFO_MIN_CT_LEN = 16.
• Six rules in fixed order:
  1. NonCanonicalAeadNonceLength
  2. ShortAeadCiphertext
  3. CrossGroupAeadEnvelope
  4. StaleEpochAeadEnvelope
  5. ReusedAeadNonce
  6. ZeroAeadNonce
• WEGI-01..10 unit tests (10 new tests).

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

• File:
  crates/trios-chat/rings/CR-CHAT-03/src/proposal_ref_collision.rs
  (≈265 lines).
• Public API:
  validate_proposal_ref(proposal: &ProposalReference, view: &ProposalRefView) -> Result<(), ProposalRefError>.
• Consts PROPOSAL_REF_LEN = 32, PROPOSAL_ID_MAX_LEN = 255.
• Seven rules in fixed order:
  1. NonCanonicalProposalRefLength
  2. EmptyProposalId
  3. UnknownProposalRef
  4. CrossGroupProposalRef
  5. StaleEpochProposalRef
  6. ProposalRefReplay
  7. ZeroProposalRef
• PREF-01..10 unit tests (10 new tests).

4. Pre-registration (Gate G2)

Field	Value
statistical_test	n/a — exhaustive falsification on a finite deny-corpus + Coq Qed
alpha	n/a
effect_size	100 % falsifier deny-rate per W32 lane (3100/3100)
n_required	50 prompts per lane × 2 lanes = 100 W32 prompts
stop_rule	"first 100/100 deny-rate on W32 corpus"
multiple_testing	n/a — single hypothesis per lane

5. Falsification (Gate G5)

• #[test] fn wegi_01..wegi_10 and #[test] fn pref_01..pref_10
  in the two new modules — each error variant has a positive
  witness (Err(<Variant>)) and the lanes share a positive accept
  case.
• Lemma inv_chat_194_… through Lemma inv_chat_200_… +
  helpers wegi_canonical_envelope_accepted_32,
  wegi_min_ciphertext_accepted_32,
  pref_canonical_proposal_accepted_32,
  pref_one_byte_proposal_id_accepted_32 in
  crates/trios-chat/proofs/chat/Trinity_Chat.v Section
  TrinityChatWave32 (lines 4418–4540).

6. Deliverables

File	Status
crates/trios-chat/rings/CR-CHAT-01/src/welcome_encrypted_group_info_aead.rs (NEW, 268 lines)	✅
crates/trios-chat/rings/CR-CHAT-01/src/lib.rs (mod + pub use)	✅
crates/trios-chat/rings/CR-CHAT-03/src/proposal_ref_collision.rs (NEW, 265 lines)	✅
crates/trios-chat/rings/CR-CHAT-03/src/lib.rs (mod + pub use)	✅
crates/trios-chat/corpus/prompt_injection.jsonl (+100 entries, total 3100)	✅
crates/trios-chat/rings/CR-CHAT-06/src/injection.rs (+201 deny patterns)	✅
crates/trios-chat/proofs/chat/Trinity_Chat.v (+Section TrinityChatWave32, +11 Qed)	✅
crates/trios-chat/src/bin/falsifier_runner.rs (+2 threshold lanes)	✅
crates/trios-chat/ROADMAP.md (Wave-32 detail + future waves W33..W37)	✅

7. Quality Gates

Gate	Expected
Cargo tests	~548 / 0
End-to-end smoke	25/25 pass
Falsifier corpus	3100/3100 blocked at 62 thresholds
Clippy	clean
Coq	silent, exit 0 (299 Qed / 0 Admitted)
Laws Guard CI	PR body opens with Closes #<this issue>
L-ARCH-001	new code under crates/trios-chat/rings/CR-CHAT-{01,03}/ only
13/13 CI checks	green

8. Forbidden

• New axioms (cumulative axiom list stays at 5: ss_kp_injective,
  dh_step_fresh, dh_post_history_independent,
  hybrid_kem_non_degenerate, sn_hash_sym).
• Admitted. in Trinity_Chat.v (W32 ships 0 admissions).
• unsafe blocks (W32 introduces 0 unsafe).
• Skipping any of the rules per lane.
• Force-push to main (this PR targets the new branch
  feat/trios-chat-wave32).

9. References

• Algebraic anchor φ² + φ⁻² = 3 — Zenodo
  10.5281/zenodo.19227877.
• Trinity software release v2.0.2 — Zenodo
  10.5281/zenodo.18947017.
• Sibling sub-tracker (W31) — #770
  closed by PR #771,
  merged 756cf35.
• RFC 9420 §12.4.3 (Welcome / encrypted_group_info AEAD) — IETF MLS protocol.
• RFC 9420 §12.1.1 (ProposalRef = MAC over ProposalContent).

10. Battle Cry

Wave-32: two more MLS hazards turn from folklore into Qed. The
Welcome AEAD nonce may not be reused, the ProposalRef may not
collide. φ² + φ⁻² = 3 — and the falsifier blocks every phrasing.