🌊 Wave-24 sub-tracker — Key Schedule transcript binding + Forward-secrecy ratchet pruning

[gHashTag]

🌊 Wave-24 — Key Schedule transcript binding + Forward-secrecy ratchet pruning

Sub-tracker for Wave-24 of crates/trios-chat. Base SHA: 1d6f910 (post-W23 admin-merge of #734).

Lanes

• L-CHAT-2-ks (R-CHAT-2 / CR-CHAT-02) — Key Schedule transcript binding: validate_extension(&KeyScheduleTranscript, &[KeyScheduleBlock], TranscriptHash) -> Result<KeyScheduleTranscript, KsTranscriptError> enforcing five rules: (1) empty extension, (2) missing-Init when transcript empty, (3) Init-after-start (Init only as first block ever), (4) adjacent duplicate inside extension + at boundary, (5) hash mismatch with domain-separated rolling hash b"trios-chat/v1/ks-transcript". Block kinds Init,DhStep,Welcome,Commit,Reinit,AppAck with byte-tags 1..6, length-prefixed payloads. 10 unit tests KS-01..10.

• L-CHAT-2-fs (R-CHAT-2 / CR-CHAT-02) — Forward-secrecy ratchet pruning: RatchetPruningLedger with BTreeMap<Generation, ChainKey> + monotone prune_watermark. MAX_RETAINED_GENERATIONS = 5. API: get(gen) -> Result<Option<ChainKey>, RatchetPruningError> (distinguishes pruned from never-seen), insert(gen, key), prune_through(gen). Errors Pruned{gen,watermark}, ReintroducePruned{gen,watermark}, ConflictingInsert{gen}. Auto-prune triggered when ledger exceeds cap. 10 unit tests FS-01..10.

Coq Wave-24

Section TrinityChatWave24 adds INV-CHAT-138..144 with helpers:

• INV-CHAT-138 inv_chat_138_ks_empty_extension_rejected
• INV-CHAT-139 inv_chat_139_ks_missing_init_rejected
• INV-CHAT-140 inv_chat_140_ks_hash_mismatch_detected
• INV-CHAT-141 inv_chat_141_fs_reintroduce_pruned_rejected
• INV-CHAT-142 inv_chat_142_fs_watermark_monotone
• INV-CHAT-143 inv_chat_143_fs_pruned_below_watermark
• INV-CHAT-144 inv_chat_144_fs_over_cap_triggers_prune
• helpers: ks_hash_equal_no_mismatch_24, fs_fresh_gen_not_reintroduce_24, fs_at_cap_not_over_24

Result: 203 Qed / 0 Admitted / 5 axioms (unchanged) / 0 new axioms.

Falsifier 2200 → 2300

• New categories key_schedule_transcript and ratchet_pruning, 50 entries each (PI-KS-001..050, PI-FS-001..050)
• Two new threshold lanes in falsifier_runner at 0.95
• DENY_PATTERNS extension in CR-CHAT-06/src/injection.rs covering both lanes' jargon (KS + FS keywords, ~120 patterns)
• Result: 46 categories at 100% block rate, 2300 / 2300 blocked

Anchor extension (W24)

φ² + φ⁻² = 3 · … · REINIT-FRESHNESS · APPACK-REPLAY · KS-TRANSCRIPT · RATCHET-PRUNING

Verification gates (G-C1..G-C12)

• G-C1 cargo test full suite: 375 / 0
• G-C2 e2e_chat_25: 25 / 25
• G-C3 cargo clippy -- -D warnings: clean
• G-C4 Coq Trinity_Chat.v: silent exit 0
• G-C5 Coq Qed count: 203
• G-C6 Coq Admitted count: 0
• G-C7 Falsifier corpus: 2300
• G-C8 Falsifier categories at 100%: 46 / 46
• G-C9 New axioms in W24: 0 (5 cumulative unchanged)
• G-C10 thresholds met: all 46 lanes ≥ 95%, indirect ≥ 90%
• G-C11 unsafe: 0
• G-C12 monoliths: 0 (rings-only architecture preserved)

Laws compliance

• L1: NO .sh files
• L2: PR body starts with bare Closes #N
• L-ARCH-001: rings-only (no monoliths)
• R5 honesty tagging applied throughout

Status

[VERIFIED] All gates met. PR open against main.