Skip to content

🌊 Wave-23: ReInit ceremony freshness + AppAck replay attestation#734

Merged
gHashTag merged 1 commit into
mainfrom
feat/trios-chat-wave23
May 12, 2026
Merged

🌊 Wave-23: ReInit ceremony freshness + AppAck replay attestation#734
gHashTag merged 1 commit into
mainfrom
feat/trios-chat-wave23

Conversation

@gHashTag
Copy link
Copy Markdown
Owner

Closes #733

🌊 Wave-23 β€” ReInit ceremony freshness + AppAck replay attestation

Base SHA: 119f0fe (post-W22 admin-merge of #732).

Lanes shipped

L-CHAT-3-rin (R-CHAT-3 / CR-CHAT-03) β€” reinit_freshness.rs (317 lines, RIN-01..10):
validate_reinit(&ReInitProposal, current_membership_count: usize) -> Result<(), ReInitError> enforcing five rules in fixed order:

  1. Reject zero-bytes new_group_id β†’ EmptyNewGroupId
  2. Reject new_group_id == current_group_id β†’ StaleGroupIdReuse
  3. Reject new_version < current_version β†’ ProtocolDowngrade { current, new }
  4. Reject new_version > MAX_SUPPORTED_VERSION (=1) β†’ UnsupportedVersionLeap { new, max_supported }
  5. Reject all-welcomers == committer when membership > 1 β†’ SelfTargetingReInit

L-CHAT-1-ack (R-CHAT-1 / CR-CHAT-01) β€” appack_replay.rs (413 lines, ACK-01..10):
AppAckLedger with BTreeMap<AppAckLeaf, Generation> high-watermark map. validate(&mut self, own_leaf, &AppAckProposal) -> Result<(), AppAckError> is two-pass atomic: first pass validates every entry (SelfAttestation, InvertedRange, StaleOrShrinking), second pass commits watermarks. On any failure the ledger is untouched.

Coq Wave-23

Section TrinityChatWave23 (lines β‰ˆ 3247–3353) adds INV-CHAT-131..137 + helpers:

  • INV-CHAT-131..134 cover ReInit (empty GID, stale reuse, downgrade, unsupported leap)
  • INV-CHAT-135..137 cover AppAck (inverted, singleton, stale)
  • helpers: reinit_same_version_not_downgrade_23, appack_grow_not_stale_23, appack_equal_not_stale_23

191 Qed / 0 Admitted / 5 axioms (unchanged) / 0 new axioms in W23.

Falsifier 2100 β†’ 2200

  • New categories reinit_freshness and appack_replay, 50 entries each (PI-RIN-001..050, PI-ACK-001..050)
  • Two new threshold lanes in falsifier_runner at 0.95
  • DENY_PATTERNS in CR-CHAT-06/src/injection.rs extended with W23 keyword blocks (Lane A ReInit jargon + Lane B AppAck jargon)

Result: 44 categories at 100% block rate, 2200 / 2200 blocked.

Anchor extension (W23)

φ² + φ⁻² = 3 Β· … Β· PROPOSAL-VALIDATION Β· MAC-TRUNCATION Β· REINIT-FRESHNESS Β· APPACK-REPLAY

Verification gates [VERIFIED]

Gate Result
G-C1 cargo test full suite 355 / 0
G-C2 e2e_chat_25 25 / 25
G-C3 cargo clippy -- -D warnings clean
G-C4 Coq coqc Trinity_Chat.v silent exit 0
G-C5 Coq Qed count 191
G-C6 Coq Admitted count 0
G-C7 Falsifier corpus 2200
G-C8 Falsifier categories at 100% 44 / 44
G-C9 New axioms in W23 0 (5 cumulative unchanged)
G-C10 thresholds met all 44 lanes β‰₯ 95%, indirect β‰₯ 90%
G-C11 unsafe 0
G-C12 monoliths 0 (rings-only)

Laws compliance

  • L1: NO .sh files βœ“
  • L2: PR body starts with bare Closes #733 βœ“
  • L-ARCH-001: rings-only architecture preserved βœ“
  • R5 honesty tagging applied throughout ROADMAP

Files

  • NEW crates/trios-chat/rings/CR-CHAT-03/src/reinit_freshness.rs (317 lines)
  • NEW crates/trios-chat/rings/CR-CHAT-01/src/appack_replay.rs (413 lines)
  • EDIT crates/trios-chat/rings/CR-CHAT-03/src/lib.rs (+ module + aliased re-exports)
  • EDIT crates/trios-chat/rings/CR-CHAT-01/src/lib.rs (+ module + re-exports)
  • EDIT crates/trios-chat/rings/CR-CHAT-01/Cargo.toml (+thiserror)
  • EDIT crates/trios-chat/proofs/chat/Trinity_Chat.v (+Section TrinityChatWave23)
  • EDIT crates/trios-chat/corpus/prompt_injection.jsonl (2100 β†’ 2200)
  • EDIT crates/trios-chat/src/bin/falsifier_runner.rs (+2 threshold lanes)
  • EDIT crates/trios-chat/rings/CR-CHAT-06/src/injection.rs (+W23 DENY block)
  • EDIT crates/trios-chat/ROADMAP.md (W23 detail + anchor + ASPIRATIONAL shift to W24-W28)

Status

[VERIFIED] All gates met. Ready for review and merge.

- CR-CHAT-03 reinit_freshness.rs (317 lines, RIN-01..10)
- CR-CHAT-01 appack_replay.rs (413 lines, ACK-01..10)
- Coq Section TrinityChatWave23: INV-CHAT-131..137 + helpers
  β†’ 191 Qed / 0 Admitted / 5 axioms (unchanged) / 0 new axioms
- Falsifier 2100 β†’ 2200: +50 RIN + +50 ACK, 44 cats @ 100%
- DENY_PATTERNS W23 extension in CR-CHAT-06/src/injection.rs
- ROADMAP W23: anchor +REINIT-FRESHNESS +APPACK-REPLAY, ASPIRATIONAL β†’ W24-W28

[VERIFIED] cargo test 355/0, e2e 25/25, clippy clean, coqc silent.
Closes #733
@gHashTag gHashTag merged commit 1d6f910 into main May 12, 2026
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

🌊 Wave-23 sub-tracker β€” ReInit ceremony freshness + AppAck replay attestation

1 participant