🌊 Wave-19: KEM decapsulation oracle + tag-stripping

[gHashTag]

Closes #718

🌊 Trinity Chat Wave-19 — KEM decapsulation oracle + structured-output tag-stripping

Parent EPIC: trinity-fpga#28
Predecessor: #717 (W18 — merged 6902a82)
Anchor: φ² + φ⁻² = 3 · … · PADDING-CLASS-ORACLE · JITTER-SIDE-CHANNEL · KEM-DECAP-ORACLE · TAG-STRIPPING

Threat lanes (×2)

Lane A — L-CHAT-8-decap (R-CHAT-2 / CR-CHAT-01)

crates/trios-chat/rings/CR-CHAT-01/src/kem_decap_oracle.rs (285 lines)

• DecapObservation::{MatchedReference, DifferedFromReference, Errored}
• ss_eq() — constant-time subtle::ConstantTimeEq
• observe() — never returns the shared secret, only an opaque enum
• consts KEM_DECAP_ORACLE_CT_LEN = MLKEM768_CT_LEN, KEM_DECAP_ORACLE_SS_LEN = MLKEM768_SS_LEN

Routing note (R5 honesty): ML-KEM-768 keypair, encapsulate_to, and CT/SS types live in CR-CHAT-01 (kem.rs), not in CR-CHAT-02 as the W18 ROADMAP plan suggested. Placing the oracle observer in CR-CHAT-01 avoids cross-ring leaks of kem.rs internals (preserves L-ARCH-001).

Test	Property
DEC-01	honest decap matches reference (FO determinism)
DEC-02	single-bit CT flip → DifferedFromReference
DEC-03	distinct CTs under same KP never collapse to same SS
DEC-04	implicit-reject branch is (ek, ct)-bound
DEC-05	ss_eq is constant-time (no early-exit oracle)
DEC-06	observe() never returns SS — only opaque enum variants
+4 bonus + 1 green	Errored path, idempotence, length consts

Lane B — L-CHAT-9-tagsplit (R-CHAT-12 / CR-CHAT-06)

crates/trios-chat/rings/CR-CHAT-06/src/tag_stripping.rs (380 lines)

• SpanTag::{Trusted, Untrusted}
• TagSplit::{Unbalanced, NestedNotAllowed, UnknownTag, TagInPayload, EmptyInput, EmptyPayload, StrayBytes}
• Span{tag, payload}, parse_structured_output(), serialise_structured_output()
• Tag alphabet: <TRUSTED>…</TRUSTED> / <UNTRUSTED>…</UNTRUSTED> only

Test	Property
TAG-01	unbalanced opener → Unbalanced
TAG-02	nested span → NestedNotAllowed (flat sequence only)
TAG-03	unknown tag (<SYSTEM>, <TRUST>, <TRUSTED foo>) → UnknownTag
TAG-04	tag-like substring inside payload → TagInPayload
TAG-05	empty input → EmptyInput; empty payload → EmptyPayload
TAG-06	stray bytes outside any tagged span → StrayBytes
+4 bonus + 1 green	round-trip, mixed sequence, case-sensitivity

Coq Wave-19 — Section TrinityChatWave19

INV-CHAT-103..109 + 2 helpers (nested_check_passes19, well_formed_span_passes19) — 9 new Qed. → 148 Qed total, 0 Admitted, 0 new axioms.

Cumulative axiom set unchanged at 5: ss_kp_injective (W9), dh_step_fresh + dh_post_history_independent + hybrid_kem_non_degenerate (W10), sn_hash_sym (W14).

Falsifier 1700 → 1800

• corpus/prompt_injection.jsonl: +50 PI-DEC-001..050 + +50 PI-TAG-001..050
• falsifier_runner.rs: +2 threshold lanes (kem_decap_oracle, tag_stripping) at 0.95
• injection.rs::DENY_PATTERNS: +260 keywords covering FO-rejection distinguishability + tag-stripping language

Verification gauntlet (all green)

Gate	Result
cargo test (12 chat crates)	290 / 0
e2e_chat_25	25 / 25
falsifier_runner	1800 / 1800, 36 cats @ 100%
cargo clippy --all-targets -- -D warnings	clean
coqc Trinity_Chat.v	silent, exit 0
Coq Qed	148
Coq Admitted	0
New axioms	0
unsafe blocks	0
Monoliths	0

Wave progression

Wave	SHA	Tests	Coq Qed	Falsifier	Cats
W17	047f3cb	249	130	1600	32
W18	6902a82	270	139	1700	34
W19	(this PR)	290	148	1800	36

Honesty tags (Art. I + R5)

• All test counts, falsifier counts, and Coq totals: [VERIFIED] by cargo / grep -cE
• Routing of kem_decap_oracle to CR-CHAT-01 (not CR-CHAT-02): [DERIVED] from kem.rs location
• Anchor extension: [VERIFIED] in ROADMAP.md
• W20–W24 lane plan: [ASPIRATIONAL]

Compliance

• L1: zero .sh files
• L2: this PR body opens with bare Closes #718 (Laws Guard regex green)
• L-ARCH-001: zero monoliths, all new code under rings/CR-CHAT-NN/
• R5: every claim tagged or self-evidently [VERIFIED] from CI gates