Oct 17, 2026 · Oct 17, 2026 · Oct 17, 2026
@@ -0,0 +1,28 @@
+{
+  "built_by": "t27c-bootstrap@0.5.2+01d0a635f",
+  "closure": [],
+  "config": "gen=c,rust,verilog,zig;tests=zig",
+  "gen_hash_c": "sha256:9bbcd9e2167fe62cab8184bc4f58e67dbf583e2bbe0cfd8eec679ac0e6e90939",
+  "gen_hash_rust": "sha256:1151e48a6f5f273f7aa1569121a158d5f234fea25d60568d371ffe9ad49fc1dd",
+  "gen_hash_verilog": "sha256:25a4ed76d67d001c0dc8ee6018c3f02dadb17b0cc9897de05a8096da5b0b2ffb",
+  "gen_hash_zig": "sha256:15ce101cbb616096e8b90791fdf9a41ddc5401d9fdeb520a246b5c53ee5b0307",
+  "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning",
+  "ring": 12,
+  "seal_schema": 2,
+  "sealed_at": "2026-10-15T19:47:58Z",
+  "sealed_by": "t27c-bootstrap@0.5.2",
+  "spec_hash": "sha256:289a4a6a41e8fc8acf82cb5fa1b94d56ee56784678c570acdffb33d0b7952817",
+  "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27",
+  "tests": {
+    "failed": 0,
+    "failing": [],
+    "forced": false,
+    "passed": 15,
+    "total": 15,
+    "vacuous": 0
+  },
+  "toolchain": {
+    "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d",
+    "zig": "0.16.0"
+  }
+}
@@ -857,6 +857,7 @@
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/ratchet_tree_resolution_guard.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/ratchet_tree_update_integrity_guard.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/unmerged_leaves_bound_guard.t27", "t27b": "pass"},
+  {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_alignment_boundary_guard.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_block_size_alignment_guard.t27", "t27b": "pass"},
   {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"},

@@ -0,0 +1,341 @@
+module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::external_init_secret_pinning;
+
+// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/external_init_secret_pinning.rs
+// (CR-CHAT-04 - External Init secret pinning, Wave-27 Lane L-CHAT-8-eip,
+// requirement R-CHAT-11, aligned to RFC 9420 section 12.2).
+//
+// A non-member joins an existing MLS group by re-derivation: a fresh
+// init_secret from the group's exported external_init value and a local
+// KEM ephemeral, then a signed External Commit binding to that
+// init_secret. Five confusion attacks are rejected before any key
+// derivation runs: non-canonical exporter length, stale exporter epoch,
+// cross-group exporter splice, an all-zero KEM ephemeral (the known-key
+// init), and an External Commit from a removed or unknown signer leaf.
+//
+// The original returns Result<(), ExternalInitError>. This port carries
+// the verdict as a named struct (owner decision D5): Ok first, then the
+// seven error variants in the original's declaration order -
+// NonCanonicalExporterLen, CrossGroupExporterSplice, StaleExporterEpoch,
+// ZeroKemEphemeral, NonCanonicalKemEphemeralLen, RemovedMemberRejoin,
+// UnknownSignerLeaf. No variant carries a payload, so the verdict is the
+// code alone.
+//
+// The original's Vec<u8> fields are read only by length or by all-zero
+// probe here; the BTreeSet leaves are read only by membership and maximum.
+// The byte equality of the two group ids is a helper over fixed-size
+// ids (conventions section 4: helpers inline, each with its own test).
+// The crate-wide Error conversion and the validate() adapter are
+// plumbing (formatting strings and type mapping) and are not ported.
+
+// Canonical exporter-secret length, in bytes.
+pub const EIP_EXPORTER_LEN: usize = 32;
+
+// Canonical KEM-ephemeral length, in bytes.
+pub const EIP_KEM_EPHEMERAL_LEN: usize = 32;
+
+// Fixed group-id length the tests use. The original compares Vec<u8>
+// ids of any length; a fixed port covers the decision at one length and
+// the tests exercise both equal and unequal ids.
+pub const EIP_GROUP_ID_LEN: usize = 15;
+
+// Exporter binding for a joining external commit.
+pub struct ExternalInitExporter {
+    exporter_len: usize,
+    group_id: [15]u8,
+    epoch: u64,
+}
+
+// External-commit message the joiner submits.
+pub struct ExternalCommit {
+    group_id: [15]u8,
+    epoch: u64,
+    kem_ephemeral_len: usize,
+    kem_ephemeral_nonzero: bool,
+    signer_leaf: u32,
+}
+
+// Verifier-side view of the group.
+pub struct ExternalInitView {
+    current_group_id: [15]u8,
+    current_epoch: u64,
+    active_leaves: [4]u32,
+    removed_leaves: [4]u32,
+}
+
+// Verdict codes: Ok(()) and ExternalInitError's variants, in declaration order.
+pub enum ExternalInitCode {
+    Ok,
+    NonCanonicalExporterLen,
+    CrossGroupExporterSplice,
+    StaleExporterEpoch,
+    ZeroKemEphemeral,
+    NonCanonicalKemEphemeralLen,
+    RemovedMemberRejoin,
+    UnknownSignerLeaf,
+}
+
+// The verdict of the External Commit validation. No variant of the
+// original's error carries a payload, so the code is the whole verdict.
+pub struct ExternalInitVerdict {
+    code: ExternalInitCode,
+}
+
+// Whole-id equality over the fixed-size ids.
+pub fn ids_equal(a: [15]u8, b: [15]u8) -> bool {
+    for i in 0..15 {
+        if (a[i] != b[i]) {
+            return false;
+        }
+    }
+    return true;
+}
+
+// Membership of a leaf in a fixed-size leaf table. The original asks
+// BTreeSet::contains; there is no set here, so the decision is a scan
+// over the slots the caller filled.
+pub fn leaf_in(leaf: u32, leaves: [4]u32) -> bool {
+    for i in 0..4 {
+        if (leaves[i] == leaf) {
+            return true;
+        }
+    }
+    return false;
+}
+
+// The largest leaf in the table. The original asks active_leaves.max();
+// the caller fills the slots, so the scan answers the same question over
+// exactly the leaves it put there.
+pub fn leaf_max(leaves: [4]u32) -> u32 {
+    var m: u32 = leaves[0];
+    for i in 1..4 {
+        if (leaves[i] > m) {
+            m = leaves[i];
+        }
+    }
+    return m;
+}
+
+// [VERIFIED] Validate an External Commit against an exporter binding and
+// the verifier's group view. Returns Ok only when every RFC 9420
+// section 12.2 rule accepts, checked in the original's order: canonical
+// exporter length, exporter bound to the verifier's group, exporter epoch
+// not stale, canonical KEM ephemeral length, KEM ephemeral not all-zero
+// (the commit record carries that probe as a bit, computed by the caller
+// over the bytes), signer not removed, signer leaf known (active, or a
+// slot at or beyond the largest active leaf), and the commit itself bound
+// to the verifier's group.
+pub fn validate_external_commit(exporter: ExternalInitExporter, commit: ExternalCommit, view: ExternalInitView) -> ExternalInitVerdict {
+    if (exporter.exporter_len != EIP_EXPORTER_LEN) {
+        return ExternalInitVerdict { code: ExternalInitCode.NonCanonicalExporterLen, };
+    }
+    if (!ids_equal(exporter.group_id, view.current_group_id)) {
+        return ExternalInitVerdict { code: ExternalInitCode.CrossGroupExporterSplice, };
+    }
+    if (exporter.epoch < view.current_epoch) {
+        return ExternalInitVerdict { code: ExternalInitCode.StaleExporterEpoch, };
+    }
+    if (commit.kem_ephemeral_len != EIP_KEM_EPHEMERAL_LEN) {
+        return ExternalInitVerdict { code: ExternalInitCode.NonCanonicalKemEphemeralLen, };
+    }
+    if (!commit.kem_ephemeral_nonzero) {
+        return ExternalInitVerdict { code: ExternalInitCode.ZeroKemEphemeral, };
+    }
+    if (leaf_in(commit.signer_leaf, view.removed_leaves)) {
+        return ExternalInitVerdict { code: ExternalInitCode.RemovedMemberRejoin, };
+    }
+    if (!leaf_in(commit.signer_leaf, view.active_leaves)) {
+        const m: u32 = leaf_max(view.active_leaves);
+        if (commit.signer_leaf <= m) {
+            return ExternalInitVerdict { code: ExternalInitCode.UnknownSignerLeaf, };
+        }
+    }
+    if (!ids_equal(commit.group_id, view.current_group_id)) {
+        return ExternalInitVerdict { code: ExternalInitCode.CrossGroupExporterSplice, };
+    }
+    return ExternalInitVerdict { code: ExternalInitCode.Ok, };
+}
+
+// The two typed accessors of the original answer the canonical lengths.
+pub fn exporter_len() -> usize {
+    return EIP_EXPORTER_LEN;
+}
+
+pub fn kem_ephemeral_len() -> usize {
+    return EIP_KEM_EPHEMERAL_LEN;
+}
+
+// The fixtures' group id, "trinity-group-1" as fixed bytes.
+pub const EIP_TEST_GROUP_ID: [15]u8 = [15]u8{'t', 'r', 'i', 'n', 'i', 't', 'y', '-', 'g', 'r', 'o', 'u', 'p', '-', '1',};
+
+// The fixtures' other-group id, "other-group---" as fixed bytes.
+pub const EIP_OTHER_GROUP_ID: [15]u8 = [15]u8{'o', 't', 'h', 'e', 'r', '-', 'g', 'r', 'o', 'u', 'p', '-', '-', '-', '-',};
+
+// The canonical exporter fixture of the tests.
+fn ok_exporter() -> ExternalInitExporter {
+    return ExternalInitExporter { exporter_len: EIP_EXPORTER_LEN, group_id: EIP_TEST_GROUP_ID, epoch: 7, };
+}
+
+// The canonical commit fixture of the tests.
+fn ok_commit() -> ExternalCommit {
+    return ExternalCommit { group_id: EIP_TEST_GROUP_ID, epoch: 7, kem_ephemeral_len: EIP_KEM_EPHEMERAL_LEN, kem_ephemeral_nonzero: true, signer_leaf: 10, };
+}
+
+// The canonical view fixture of the tests.
+fn ok_view() -> ExternalInitView {
+    return ExternalInitView { current_group_id: EIP_TEST_GROUP_ID, current_epoch: 7, active_leaves: [4]u32{0, 1, 2, 3,}, removed_leaves: [4]u32{4294967295, 4294967295, 4294967295, 4294967295,}, };
+}
+
+// **EIP-01** - valid external commit accepted.
+test eip_01_valid_external_commit_accepted {
+    var exp = ok_exporter();
+    var cmt = ok_commit();
+    var view = ok_view();
+    const v = validate_external_commit(exp, cmt, view);
+    assert(v.code == ExternalInitCode.Ok);
+}
+
+// **EIP-02** - short exporter rejected: 16 of a canonical 32.
+test eip_02_short_exporter_rejected {
+    var exp = ok_exporter();
+    exp.exporter_len = 16;
+    var c0 = ok_commit();
+    var w0 = ok_view();
+    const v = validate_external_commit(exp, c0, w0);
+    assert(v.code == ExternalInitCode.NonCanonicalExporterLen);
+}
+
+// **EIP-03** - oversize exporter rejected: 64 of a canonical 32.
+test eip_03_oversize_exporter_rejected {
+    var exp = ok_exporter();
+    exp.exporter_len = 64;
+    var c0 = ok_commit();
+    var w0 = ok_view();
+    const v = validate_external_commit(exp, c0, w0);
+    assert(v.code == ExternalInitCode.NonCanonicalExporterLen);
+}
+
+// **EIP-04** - cross-group exporter splice rejected.
+test eip_04_cross_group_exporter_splice_rejected {
+    var exp = ok_exporter();
+    exp.group_id = EIP_OTHER_GROUP_ID;
+    var c0 = ok_commit();
+    var w0 = ok_view();
+    const v = validate_external_commit(exp, c0, w0);
+    assert(v.code == ExternalInitCode.CrossGroupExporterSplice);
+}
+
+// **EIP-05** - stale exporter epoch rejected: 5 against a current 7.
+test eip_05_stale_exporter_epoch_rejected {
+    var exp = ok_exporter();
+    exp.epoch = 5;
+    var c0 = ok_commit();
+    var w0 = ok_view();
+    const v = validate_external_commit(exp, c0, w0);
+    assert(v.code == ExternalInitCode.StaleExporterEpoch);
+}
+
+// **EIP-06** - zero KEM ephemeral rejected: the all-zero probe bit reads false.
+test eip_06_zero_kem_ephemeral_rejected {
+    var cmt = ok_commit();
+    cmt.kem_ephemeral_nonzero = false;
+    var e0 = ok_exporter();
+    var w0 = ok_view();
+    const v = validate_external_commit(e0, cmt, w0);
+    assert(v.code == ExternalInitCode.ZeroKemEphemeral);
+}
+
+// **EIP-07** - non-canonical KEM ephemeral length rejected: 16 of 32.
+test eip_07_non_canonical_kem_ephemeral_len_rejected {
+    var cmt = ok_commit();
+    cmt.kem_ephemeral_len = 16;
+    var e0 = ok_exporter();
+    var w0 = ok_view();
+    const v = validate_external_commit(e0, cmt, w0);
+    assert(v.code == ExternalInitCode.NonCanonicalKemEphemeralLen);
+}
+
+// **EIP-08** - removed-member rejoin rejected: leaf 10 sits in the
+// removed table.
+test eip_08_removed_member_rejoin_rejected {
+    var view = ok_view();
+    view.removed_leaves = [4]u32{10, 4294967295, 4294967295, 4294967295,};
+    var e0 = ok_exporter();
+    var c0 = ok_commit();
+    const v = validate_external_commit(e0, c0, view);
+    assert(v.code == ExternalInitCode.RemovedMemberRejoin);
+}
+
+// **EIP-09** - an already-active signer leaf accepts; a leaf in a gap
+// inside the active range (2 while 0, 1, 3 are active) rejects as unknown.
+// The empty removed table of the view fixture holds the u32 sentinel
+// 4294967295, which no signer leaf of the tests equals, so the sentinel
+// answers "absent" exactly as the original's empty set does.
+test eip_09_unknown_leaf_below_max_rejected {
+    var cmt = ok_commit();
+    cmt.signer_leaf = 2;
+    var e0 = ok_exporter();
+    var w0 = ok_view();
+    const va = validate_external_commit(e0, cmt, w0);
+    assert(va.code == ExternalInitCode.Ok);
+
+    var view = ok_view();
+    view.active_leaves = [4]u32{0, 1, 3, 4294967295,};
+    var exp = ok_exporter();
+    const vb = validate_external_commit(exp, cmt, view);
+    assert(vb.code == ExternalInitCode.UnknownSignerLeaf);
+}
+
+// **EIP-10** - commit group-id mismatch rejected: the commit names
+// another group than the verifier's view.
+test eip_10_commit_group_id_mismatch_rejected {
+    var cmt = ok_commit();
+    cmt.group_id = EIP_OTHER_GROUP_ID;
+    var exp = ok_exporter();
+    var view = ok_view();
+    const v = validate_external_commit(exp, cmt, view);
+    assert(v.code == ExternalInitCode.CrossGroupExporterSplice);
+}
+
+// The three helpers have direct tests (coverage: Untested 0).
+test ids_equal_answers {
+    assert(ids_equal(EIP_TEST_GROUP_ID, EIP_TEST_GROUP_ID));
+    assert(!ids_equal(EIP_TEST_GROUP_ID, EIP_OTHER_GROUP_ID));
+}
+
+test leaf_in_answers {
+    assert(leaf_in(2, [4]u32{0, 1, 2, 3,}));
+    assert(!leaf_in(5, [4]u32{0, 1, 2, 3,}));
+}
+
+test leaf_max_answers {
+    assert(leaf_max([4]u32{0, 1, 2, 3,}) == 3);
+    assert(leaf_max([4]u32{7, 1, 9, 3,}) == 9);
+}
+
+// The accessors answer the canonical lengths.
+test accessors_answer_canonical_lengths {
+    assert(exporter_len() == 32);
+    assert(kem_ephemeral_len() == 32);
+}
+
+// Rule order is the original's: exporter length before group binding,
+// group binding before epoch, the KEM length before the zero probe, the
+// removed check before the unknown check, and the group binding of the
+// commit last of all.
+test rule_order_matches_original {
+    var exp = ok_exporter();
+    exp.exporter_len = 16;
+    exp.group_id = EIP_OTHER_GROUP_ID;
+    var c0 = ok_commit();
+    var w0 = ok_view();
+    const va = validate_external_commit(exp, c0, w0);
+    assert(va.code == ExternalInitCode.NonCanonicalExporterLen);
+
+    var cmt = ok_commit();
+    cmt.kem_ephemeral_len = 16;
+    cmt.kem_ephemeral_nonzero = false;
+    var e = ok_exporter();
+    var vw = ok_view();
+    const vb = validate_external_commit(e, cmt, vw);
+    assert(vb.code == ExternalInitCode.NonCanonicalKemEphemeralLen);
+}