Oct 17, 2026 · 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:a5685b2503fa6471b679a8a6612050aa1f2b2bf8156d2ec44213ea85d613ef99",
+  "gen_hash_rust": "sha256:abd1593938d72bbfc9d572f8adfd08bdd090e21a3d3f7385ec3d6d2acdb8cf31",
+  "gen_hash_verilog": "sha256:a969cc380ea1f50c30ed1a35e36c60e75d11b127c90ea9bc8087fa247e7e5685",
+  "gen_hash_zig": "sha256:d811fdb0334f599db5adfe3fb5ac646f01c39e487a2d71c97f7d24acd6b4f248",
+  "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos",
+  "ring": 12,
+  "seal_schema": 2,
+  "sealed_at": "2026-10-15T21:25:10Z",
+  "sealed_by": "t27c-bootstrap@0.5.2",
+  "spec_hash": "sha256:c6c5d8d439602f073ae1fa1100496f631ab6107fe6a6dd9a4af2ba4d1c95d282",
+  "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.t27",
+  "tests": {
+    "failed": 0,
+    "failing": [],
+    "forced": false,
+    "passed": 14,
+    "total": 14,
+    "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/application_message_generation_skip_dos.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,318 @@
+module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos;
+
+// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.rs
+// (CR-CHAT-04 - Application-message generation skip-window DoS defence,
+// Wave-36 Lane L-CHAT-4-amgsd, requirement R-CHAT-4, RFC 9420 sections
+// 9.3 and 15.2).
+//
+// Within one (sender, epoch) the MLS generation counter is strictly
+// monotone, but receivers tolerate a bounded amount of out-of-order
+// delivery by key-deriving skipped generations on demand. Without a cap
+// one attacker packet claiming generation u64::MAX forces a
+// tens-of-billions-of-rounds HKDF chain, so the skip distance the
+// receiver will derive is capped at APP_MSG_SKIP_WINDOW.
+//
+// The original returns Result<(), AppMessageSkipError>. 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 -
+// NonCanonicalSenderIdLength, UnknownSender, ZeroGeneration,
+// NonMonotonicGeneration, SkipDistanceExceeded, EpochMismatch,
+// CiphertextEmpty. No variant carries a payload, so the verdict is the
+// code alone.
+//
+// The original's Vec<u8> sender ids are read by length and equality;
+// its known_senders and last_generation tables by membership and
+// lookup. The port uses fixed-size ids ([16]u8) with helpers (equality,
+// membership, table lookup), each with its own test. The ciphertext is
+// read only by emptiness, so the record carries the length. The
+// (Vec<u8>, u64, u64) last_generation rows become a record of the id
+// and the two numbers.
+
+// Canonical sender_id length (16 bytes - MLS LeafNodeRef, RFC 9420 6.1).
+pub const APP_MSG_SENDER_ID_LEN: usize = 16;
+
+// Maximum number of skipped generations the receiver will key-derive
+// ahead of last_generation.
+pub const APP_MSG_SKIP_WINDOW: u64 = 1024;
+
+// A row of the receiver's last_generation table: a sender, its epoch
+// and the last generation seen for that pair.
+pub struct GenRow {
+    sender: [16]u8,
+    epoch: u64,
+    last: u64,
+}
+
+// A known sender's id, wrapped in a record so the known-sender table
+// is a one-dimensional array of records (a two-dimensional fixed array
+// is not lowered by the Rust backend - conventions section 4).
+pub struct SenderId {
+    id: [16]u8,
+}
+
+// A single MLS application-message header arriving at the receiver.
+pub struct AppMessagePacket {
+    sender_id: [16]u8,
+    sender_id_len: usize,
+    epoch: u64,
+    generation: u64,
+    ciphertext_len: usize,
+}
+
+// Receiver-side view of application-key state.
+pub struct AppMessageView {
+    current_epoch: u64,
+    known_senders: [2]SenderId,
+    last_generation: [2]GenRow,
+}
+
+// Verdict codes: Ok(()) and AppMessageSkipError's variants, in declaration order.
+pub enum AppMessageSkipCode {
+    Ok,
+    NonCanonicalSenderIdLength,
+    UnknownSender,
+    ZeroGeneration,
+    NonMonotonicGeneration,
+    SkipDistanceExceeded,
+    EpochMismatch,
+    CiphertextEmpty,
+}
+
+// The verdict of the skip-window validation. No variant of the
+// original's error carries a payload, so the code is the whole verdict.
+pub struct AppMessageSkipVerdict {
+    code: AppMessageSkipCode,
+}
+
+// Whole-id equality over the fixed-size ids.
+pub fn ids_equal(a: [16]u8, b: [16]u8) -> bool {
+    for i in 0..16 {
+        if (a[i] != b[i]) {
+            return false;
+        }
+    }
+    return true;
+}
+
+// Membership of a sender in the fixed-size known-sender table. The
+// original asks known_senders.contains(&sender); there is no Vec here,
+// so the scan covers exactly the slots the caller filled. The sentinel
+// row holds id 255 in every byte, which no fixture id equals.
+pub fn sender_known(id: [16]u8, known: [2]SenderId) -> bool {
+    for i in 0..2 {
+        if (ids_equal(id, known[i].id)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+// The last generation seen for one (sender, epoch), 0 when the table has
+// no row for the pair - the original's unwrap_or(0).
+pub fn last_seen_for(id: [16]u8, epoch: u64, table: [2]GenRow) -> u64 {
+    for i in 0..2 {
+        if (ids_equal(id, table[i].sender)) {
+            if (table[i].epoch == epoch) {
+                return table[i].last;
+            }
+        }
+    }
+    return 0;
+}
+
+// [VERIFIED] Validate a single application packet's (sender, epoch,
+// generation) triple plus body shape against the receiver's view.
+// Returns Ok only when every rule holds, checked in the original's
+// order: canonical sender-id length, known sender, active epoch,
+// non-empty ciphertext, non-zero generation, strictly monotone
+// generation, and a skip distance within the window.
+pub fn validate_app_message_skip(packet: AppMessagePacket, view: AppMessageView) -> AppMessageSkipVerdict {
+    if (packet.sender_id_len != APP_MSG_SENDER_ID_LEN) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.NonCanonicalSenderIdLength, };
+    }
+    if (!sender_known(packet.sender_id, view.known_senders)) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.UnknownSender, };
+    }
+    if (packet.epoch != view.current_epoch) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.EpochMismatch, };
+    }
+    if (packet.ciphertext_len == 0) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.CiphertextEmpty, };
+    }
+    if (packet.generation == 0) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.ZeroGeneration, };
+    }
+    const last_seen: u64 = last_seen_for(packet.sender_id, packet.epoch, view.last_generation);
+    if (packet.generation <= last_seen) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.NonMonotonicGeneration, };
+    }
+    const skip_distance: u64 = packet.generation - last_seen - 1;
+    if (skip_distance > APP_MSG_SKIP_WINDOW) {
+        return AppMessageSkipVerdict { code: AppMessageSkipCode.SkipDistanceExceeded, };
+    }
+    return AppMessageSkipVerdict { code: AppMessageSkipCode.Ok, };
+}
+
+// The fixtures' sender ids, one byte repeated 16 times.
+pub const SENDER_A: [16]u8 = [16]u8{0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1,};
+pub const SENDER_B: [16]u8 = [16]u8{0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2,};
+
+// The sentinel row of the tables: id 255 in every byte, epoch and last
+// at values no fixture pair equals.
+pub const EMPTY_ROW: GenRow = GenRow { sender: [16]u8{255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255,}, epoch: 18446744073709551615, last: 0, };
+
+// The canonical view fixture of the tests: one known sender, one
+// last_generation row (sender A, epoch 7, generation 10).
+fn ok_view() -> AppMessageView {
+    return AppMessageView {
+        current_epoch: 7,
+        known_senders: [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: SENDER_B, }, },
+        last_generation: [2]GenRow{ GenRow { sender: SENDER_A, epoch: 7, last: 10, }, EMPTY_ROW, },
+    };
+}
+
+// The canonical packet fixture of the tests: sender A, epoch 7,
+// generation 11 (last seen 10, skip distance 0), 64 bytes of ciphertext.
+fn ok_packet() -> AppMessagePacket {
+    return AppMessagePacket {
+        sender_id: SENDER_A,
+        sender_id_len: APP_MSG_SENDER_ID_LEN,
+        epoch: 7,
+        generation: 11,
+        ciphertext_len: 64,
+    };
+}
+
+// **AMGSD-01** - short sender id rejected: 8 of a canonical 16.
+test amgsd_01_short_sender_id_rejected {
+    var p = ok_packet();
+    p.sender_id_len = 8;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.NonCanonicalSenderIdLength);
+}
+
+// **AMGSD-02** - unknown sender rejected: sender B is not in the view's
+// known table.
+test amgsd_02_unknown_sender_rejected {
+    var p = ok_packet();
+    p.sender_id = SENDER_B;
+    var view = ok_view();
+    view.known_senders = [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: EMPTY_ROW.sender, }, };
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.UnknownSender);
+}
+
+// **AMGSD-03** - wrong epoch rejected: packet claims epoch 6 against a
+// current 7.
+test amgsd_03_epoch_mismatch_rejected {
+    var p = ok_packet();
+    p.epoch = 6;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.EpochMismatch);
+}
+
+// **AMGSD-04** - empty ciphertext rejected.
+test amgsd_04_empty_ciphertext_rejected {
+    var p = ok_packet();
+    p.ciphertext_len = 0;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.CiphertextEmpty);
+}
+
+// **AMGSD-05** - zero generation rejected: the counter starts at 1.
+test amgsd_05_zero_generation_rejected {
+    var p = ok_packet();
+    p.generation = 0;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.ZeroGeneration);
+}
+
+// **AMGSD-06** - non-monotonic generation (equal to last seen 10)
+// rejected.
+test amgsd_06_non_monotonic_equal_rejected {
+    var p = ok_packet();
+    p.generation = 10;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.NonMonotonicGeneration);
+}
+
+// **AMGSD-07** - non-monotonic generation (lower than last seen 10)
+// rejected - the explicit replay.
+test amgsd_07_non_monotonic_lower_rejected {
+    var p = ok_packet();
+    p.generation = 5;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.NonMonotonicGeneration);
+}
+
+// **AMGSD-08** - skip distance one past the cap rejected - the
+// DoS-resistance core: last seen 10, generation 10 + 1 + 1024 + 1.
+test amgsd_08_skip_distance_just_over_cap_rejected {
+    var p = ok_packet();
+    p.generation = 10 + 1 + (APP_MSG_SKIP_WINDOW + 1);
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.SkipDistanceExceeded);
+}
+
+// **AMGSD-09** - skip distance exactly at the cap accepted - the
+// boundary of the window: generation 10 + 1 + 1024.
+test amgsd_09_skip_distance_at_cap_accepted {
+    var p = ok_packet();
+    p.generation = 10 + 1 + APP_MSG_SKIP_WINDOW;
+    var view = ok_view();
+    const v = validate_app_message_skip(p, view);
+    assert(v.code == AppMessageSkipCode.Ok);
+}
+
+// **AMGSD-10** - the canonical packet (skip distance 0) accepted.
+test amgsd_10_canonical_packet_accepted {
+    var view = ok_view();
+    const v = validate_app_message_skip(ok_packet(), view);
+    assert(v.code == AppMessageSkipCode.Ok);
+}
+
+// The three helpers have direct tests (coverage: Untested 0).
+test ids_equal_answers {
+    assert(ids_equal(SENDER_A, SENDER_A));
+    assert(!ids_equal(SENDER_A, SENDER_B));
+}
+
+test sender_known_answers {
+    const t: [2]SenderId = [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: SENDER_B, }, };
+    const u: [2]SenderId = [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: EMPTY_ROW.sender, }, };
+    assert(sender_known(SENDER_A, t));
+    assert(!sender_known(SENDER_B, u));
+}
+
+test last_seen_for_answers {
+    const t: [2]GenRow = [2]GenRow{ GenRow { sender: SENDER_A, epoch: 7, last: 10, }, EMPTY_ROW, };
+    assert(last_seen_for(SENDER_A, 7, t) == 10);
+    assert(last_seen_for(SENDER_A, 6, t) == 0);
+    assert(last_seen_for(SENDER_B, 7, t) == 0);
+}
+
+// Rule order is the original's: sender length before known-sender,
+// epoch before ciphertext emptiness, ciphertext before zero generation,
+// monotonicity before the skip window.
+test rule_order_matches_original {
+    var p = ok_packet();
+    p.sender_id_len = 8;
+    p.epoch = 6;
+    var view = ok_view();
+    const va = validate_app_message_skip(p, view);
+    assert(va.code == AppMessageSkipCode.NonCanonicalSenderIdLength);
+
+    var q = ok_packet();
+    q.epoch = 6;
+    q.ciphertext_len = 0;
+    var w = ok_view();
+    const vb = validate_app_message_skip(q, w);
+    assert(vb.code == AppMessageSkipCode.EpochMismatch);
+}