Skip to content

🌊 feat(trios-chat) Wave-33: commit-secret-export-collision + external-proposal-origin-unbound - #942

Merged
gHashTag merged 2 commits into
mainfrom
feat/trios-chat-wave33
May 22, 2026
Merged

🌊 feat(trios-chat) Wave-33: commit-secret-export-collision + external-proposal-origin-unbound#942
gHashTag merged 2 commits into
mainfrom
feat/trios-chat-wave33

Conversation

@gHashTag

@gHashTag gHashTag commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

Closes #943

🌊 Wave-33 β€” commit-secret-export-collision + external-proposal-origin-unbound

Two new falsifier lanes (both CR-CHAT-03), closing 14 new RFC 9420 invariants with 20 deterministic unit tests, 100 corpus prompts, and 7 fresh Coq theorems + 4 helper lemmas.

Base commit: b37abb1 (PR #941 merge).
Branch: feat/trios-chat-wave33.

Lane A β€” L-CHAT-3-csec (commit_secret export collision)

crates/trios-chat/rings/CR-CHAT-03/src/commit_secret_export_collision.rs (298 lines) ships
validate_commit_secret_export(export, view) -> Result<(), CommitSecretError> mapping to RFC 9420 Β§8.4 / Β§9 (commit_secret KDF-output binding to a confirmed transcript).

Seven rules enforced in fixed order, single deny wins:

# Variant Threat
1 NonCanonicalCommitSecretLength commit_secret length β‰  32
2 EmptyTranscriptHash empty transcript_hash
3 UnknownTranscriptHash transcript_hash βˆ‰ known set
4 CrossGroupCommitSecret group_id mismatch
5 StaleEpochCommitSecret commit_epoch mismatch
6 CommitSecretReplay (gid, epoch, transcript) replay
7 ZeroCommitSecret all-zero secret

Tests CSEC-01..10 cover each rule + the canonical accepted path + a fresh-transcript false-positive defence.

Lane B β€” L-CHAT-3-epou (external proposal origin unbound)

crates/trios-chat/rings/CR-CHAT-03/src/external_proposal_origin_unbound.rs (344 lines) ships
validate_external_proposal_origin(proposal, view) -> Result<(), ExternalProposalError> mapping to RFC 9420 Β§6.2 (sender type external) and Β§12.1.8.2 (new_member_proposal / new_member_commit).

Seven rules enforced in fixed order:

# Variant Threat
1 NonCanonicalOriginSignatureLength origin_signature length β‰  64
2 UnknownExternalOrigin origin βˆ‰ declared set
3 UnpermittedExternalKind kind βˆ‰ permitted set for origin
4 CrossGroupExternalProposal group_id mismatch
5 StaleEpochExternalProposal proposal_epoch mismatch
6 ExternalProposalReplay (origin, proposal_id) replay
7 ZeroOriginSignature all-zero signature

Tests EPOU-01..10 cover each rule + the canonical accepted path + a fresh proposal_id false-positive defence.

Wiring

crates/trios-chat/rings/CR-CHAT-03/src/lib.rs:

  • pub mod commit_secret_export_collision;
  • pub mod external_proposal_origin_unbound;
  • pub use re-exports for all public types of both lanes
  • 13 pub mod declarations total, sorted alphabetically, no duplicates.

Falsifier corpus 3100 β†’ 3200 (64 categories)

50 PI-CSEC-001..050 + 50 PI-EPOU-001..050 in crates/trios-chat/corpus/prompt_injection.jsonl. Every entry is expected: "blocked". Offline simulation: 3200/3200 blocked, 0 misses.

falsifier_runner threshold lane list adds:

  • ("commit_secret_export_collision", 0.95)
  • ("external_proposal_origin_unbound", 0.95)

G-C10 summary line now enumerates all 64 categories. Wave-33 doc-line appended to file header.

Coq Section TrinityChatWave33 (Trinity_Chat.v lines 4542–4670)

7 new theorems + 4 helper lemmas, all constructive:

INV Theorem
INV-CHAT-201 inv_chat_201_csec_non_canonical_commit_secret_len_rejected
INV-CHAT-202 inv_chat_202_csec_empty_transcript_hash_rejected
INV-CHAT-203 inv_chat_203_csec_cross_group_rejected
INV-CHAT-204 inv_chat_204_csec_stale_epoch_rejected
INV-CHAT-205 inv_chat_205_epou_non_canonical_origin_sig_len_rejected
INV-CHAT-206 inv_chat_206_epou_oversized_proposal_id_rejected
INV-CHAT-207 inv_chat_207_epou_stale_epoch_rejected

Helpers: csec_canonical_commit_secret_accepted_33, csec_one_byte_transcript_hash_accepted_33, epou_canonical_origin_sig_accepted_33, epou_max_proposal_id_accepted_33.

Cumulative grep -cE 'Qed\.' is 311 (W32 was 299, +12).
Wave-33 introduces 0 new axioms and 0 admissions. R5 budget: 0/10 admissions used.

ROADMAP

W33 row added (~568 tests / 25 e2e / 3200 falsifier / 64 categories / 311 Coq Qed). Status anchor line, header status, and detailed Wave-33 summary section all populated.

Stats footer

~568 tests Β· 25/25 e2e Β· 3200/3200 falsifier Β· 64 categories Β· 311 Coq Qed / 0 Admitted / 5 axioms Β· 0 unsafe Β· 0 monoliths

Co-Authored-By: Trinity Grandmaster admin@t27.ai

gHashTag and others added 2 commits May 22, 2026 09:49
@gHashTag
🌊 feat(trios-chat) Wave-33: commit-secret-export-collision + external…
9df1d8b 
…-proposal-origin-unbound

Anchor: φ² + φ⁻² = 3 Β· TRINITY Β· CHAT Β· COMMIT-SECRET-EXPORT Β· EXTERNAL-PROPOSAL-ORIGIN

Two new falsifier lanes land in distinct rings (both in CR-CHAT-03 β€”
the proposal/commit-validation ring), each closing a specific RFC 9420
threat-model invariant with 10 deterministic unit tests, 50 corpus
prompts, and a fresh Coq theorem chain.

## Lane A β€” L-CHAT-3-csec (CR-CHAT-03)

`crates/trios-chat/rings/CR-CHAT-03/src/commit_secret_export_collision.rs`
(298 lines) ships
`validate_commit_secret_export(export, view) -> Result<(), CommitSecretError>`
mapping to RFC 9420 Β§8.4 / Β§9 (commit_secret KDF-output binding).

Seven rules enforced in fixed order, single deny wins:
  (1) NonCanonicalCommitSecretLength β€” commit_secret != 32 bytes
  (2) EmptyTranscriptHash β€” empty transcript_hash
  (3) UnknownTranscriptHash β€” transcript_hash βˆ‰ known set
  (4) CrossGroupCommitSecret β€” group_id mismatch
  (5) StaleEpochCommitSecret β€” commit_epoch mismatch
  (6) CommitSecretReplay β€” (gid, epoch, transcript) replay
  (7) ZeroCommitSecret β€” all-zero secret rejected

Tests CSEC-01..10 cover each rule + the canonical accepted path
and a fresh-transcript false-positive defence.

## Lane B β€” L-CHAT-3-epou (CR-CHAT-03)

`crates/trios-chat/rings/CR-CHAT-03/src/external_proposal_origin_unbound.rs`
(344 lines) ships
`validate_external_proposal_origin(proposal, view) -> Result<(), ExternalProposalError>`
mapping to RFC 9420 Β§6.2 (external sender type) and Β§12.1.8.2
(new_member_proposal / new_member_commit).

Seven rules enforced in fixed order:
  (1) NonCanonicalOriginSignatureLength β€” origin_signature != 64 bytes
  (2) UnknownExternalOrigin β€” origin βˆ‰ declared set
  (3) UnpermittedExternalKind β€” kind βˆ‰ permitted set for origin
  (4) CrossGroupExternalProposal β€” group_id mismatch
  (5) StaleEpochExternalProposal β€” proposal_epoch mismatch
  (6) ExternalProposalReplay β€” (origin, proposal_id) replay
  (7) ZeroOriginSignature β€” all-zero signature rejected

Tests EPOU-01..10 cover each rule + the canonical accepted path
and a fresh proposal_id false-positive defence.

## Wiring

`crates/trios-chat/rings/CR-CHAT-03/src/lib.rs`:
  + pub mod commit_secret_export_collision;
  + pub mod external_proposal_origin_unbound;
  + pub use re-exports for all public types of both lanes
  (13 pub mods total, sorted alphabetically, no duplicates).

## Falsifier corpus 3100 β†’ 3200 (64 categories)

50 PI-CSEC-001..050 + 50 PI-EPOU-001..050 in
`crates/trios-chat/corpus/prompt_injection.jsonl`. Every entry is
`expected: "blocked"`. Offline simulation: 3200/3200 blocked, 0 misses.

falsifier_runner threshold lane list adds:
  + ("commit_secret_export_collision", 0.95)
  + ("external_proposal_origin_unbound", 0.95)

G-C10 summary line enumerates all 64 categories. Wave-33 doc-line
appended to the file header.

## Coq Section TrinityChatWave33 (Trinity_Chat.v lines 4542–4670)

7 new theorems + 4 helper lemmas, all constructive:
  INV-CHAT-201 inv_chat_201_csec_non_canonical_commit_secret_len_rejected
  INV-CHAT-202 inv_chat_202_csec_empty_transcript_hash_rejected
  INV-CHAT-203 inv_chat_203_csec_cross_group_rejected
  INV-CHAT-204 inv_chat_204_csec_stale_epoch_rejected
  INV-CHAT-205 inv_chat_205_epou_non_canonical_origin_sig_len_rejected
  INV-CHAT-206 inv_chat_206_epou_oversized_proposal_id_rejected
  INV-CHAT-207 inv_chat_207_epou_stale_epoch_rejected

aux: csec_canonical_commit_secret_accepted_33,
     csec_one_byte_transcript_hash_accepted_33,
     epou_canonical_origin_sig_accepted_33,
     epou_max_proposal_id_accepted_33.

Cumulative `grep -cE 'Qed\.'` is 311 (W32 was 299, +12).
Wave-33 introduces 0 new axioms and 0 admissions.
R5 budget: 0/10 admissions used.

## ROADMAP

W33 row added (~568 tests / 25 e2e / 3200 falsifier / 64 categories /
311 Coq Qed). Status anchor line, header status, and detailed Wave-33
summary section all populated.

## Stats footer

~568 tests Β· 25/25 e2e Β· 3200/3200 falsifier Β· 64 categories Β·
311 Coq Qed / 0 Admitted / 5 axioms Β· 0 unsafe Β· 0 monoliths.

Co-Authored-By: Trinity Grandmaster <admin@t27.ai>
@gHashTag
ci: re-trigger Laws Guard after PR body update (Closes #943)
8db8a59 
Empty commit to refresh PR_BODY context for Constitutional Enforcement L2 check.

Co-Authored-By: Trinity Grandmaster <admin@t27.ai>
This was referenced May 22, 2026
Closed
Merged
@gHashTag
gHashTag merged commit 521abec into main May 22, 2026
8 of 12 checks passed
@gHashTag
gHashTag deleted the feat/trios-chat-wave33 branch May 22, 2026 10:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

🌊 Wave-33 β€” commit_secret_export_collision + external_proposal_origin_unbound (sub-tracker)

1 participant

@gHashTag