From c89ce4d8d36957d7f10aa90205705eb48ab1eaff Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Fri, 16 Oct 2026 04:47:07 -0300 Subject: [PATCH] spec(port): port the padding nonce reuse detection guard (Refs #8884) The twentieth W2 target of the CR-CHAT-04 ring tracker: the nonce-reuse rules for padding AEAD - the batch ceiling, then per record the zero-key probe, the zero-nonce probe, the nonce-value ceiling and the repeated-pair scan - as the D5 verdict with every payload field, the original's rule order, and all ten PNRD tests transcribed plus helper and rule-order tests. The original's BTreeSet of (key_id, nonce) pairs becomes a scan over the visited records. The nonce value is the big-endian u64 of the nonce's last eight bytes, folded byte by byte through the int-widening cast - no shift-and-truncate anywhere. Checks (conventions 0-14): t27b test 14 passed 0 failed; t27c test-report 14/14, 0 vacuous; gen-rust output compiles under rustc; coverage Untested 0; ASCII only; seal saved, all hashes MATCH; --- ...::padding_nonce_reuse_detection_guard.json | 28 ++ docs/reports/t27b_expectations.json | 1 + .../padding_nonce_reuse_detection_guard.t27 | 334 ++++++++++++++++++ 3 files changed, 363 insertions(+) create mode 100644 .trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_nonce_reuse_detection_guard.json create mode 100644 specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.t27 diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_nonce_reuse_detection_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_nonce_reuse_detection_guard.json new file mode 100644 index 0000000000..38d1c527af --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_nonce_reuse_detection_guard.json @@ -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:e09fb9e8609322c41c0b6a2eeef34f6b78e4658f2b15a0b2f4818095dc3c2d36", + "gen_hash_rust": "sha256:d6896ae0f3a1fc107b179595cf2e4100e829bcce92165fc0c7d26c941046df89", + "gen_hash_verilog": "sha256:25d44a0d44280b968fd2edea0fdd45b9ee206cc2be7a8163bfbb49cc5efd8606", + "gen_hash_zig": "sha256:80de8b3e760d686f40edf0a0c6fb46361965ca6e85d56ef1402192b4d9f5da98", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_nonce_reuse_detection_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-16T07:45:10Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:5fd4eef52999efffced9dd17cd07a74688ae32e35c6f00ec33dfdaf168366f02", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 14, + "total": 14, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index c041cbab56..96e194296e 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -853,6 +853,7 @@ {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/epoch_rollover_wraparound_guard.t27", "t27b": "pass"}, {"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/unmerged_leaves_bound_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_decoy_ratio_governor.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.t27 new file mode 100644 index 0000000000..0d8c252937 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.t27 @@ -0,0 +1,334 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_nonce_reuse_detection_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_nonce_reuse_detection_guard.rs +// (CR-CHAT-04 - Padding nonce reuse detection guard, Wave-105 Lane A, +// requirement R-CHAT-4). +// +// Padding nonces must never repeat under the same key: a repeated +// nonce XORs two ciphertexts into the XOR of their plaintexts, +// enables third-ciphertext forgeries, and in some AEAD modes a +// practical key recovery. The rules, in the original's order: the +// batch ceiling, then per record the zero-key probe, the zero-nonce +// probe, the nonce-value ceiling and the repeated-pair scan. +// +// The original returns Result<(), NonceReuseError>. This port +// carries the verdict as a named struct (owner decision D5): Ok +// first, then the five error variants in the original's declaration +// order - Duplicate, ZeroNonce, ZeroKey, NonceOverflow, TooMany - +// with every payload field: idx for Duplicate, ZeroNonce, ZeroKey +// and NonceOverflow, got and max for TooMany. +// +// The original's BTreeSet of (key_id, nonce) pairs becomes a scan +// over the records already visited (conventions section 4). The +// nonce value is the big-endian u64 of the nonce's last eight +// bytes, folded byte by byte with the int-widening cast both +// backends lower - no shift-and-truncate anywhere. + +// Nonce length. +pub const PNRD_NONCE_LEN: usize = 12; + +// Key ID length. +pub const PNRD_KEY_ID_LEN: usize = 16; + +// Maximum records per batch. +pub const PNRD_MAX_RECORDS: usize = 10000; + +// Maximum nonce value (big-endian u96): two to the forty-eighth +// less one, the original's (1 << 48) - 1. +pub const PNRD_MAX_NONCE: u64 = 281474976710655; + +// A nonce usage record. +pub struct NonceRecord { + key_id: [16]u8, + nonce: [12]u8, +} + +// Verdict codes: Ok(()) and NonceReuseError's variants, in declaration order. +pub enum NonceReuseCode { + Ok, + Duplicate, + ZeroNonce, + ZeroKey, + NonceOverflow, + TooMany, +} + +// The verdict of the nonce reuse validation, with every error +// payload field. +pub struct NonceReuseVerdict { + code: NonceReuseCode, + idx: usize, + got: usize, + bound: usize, +} + +// Whole-form equality over the fixed sixteen key ID bytes. +pub fn key_ids_equal(a: [16]u8, b: [16]u8) -> bool { + for i in 0..16 { + if (a[i] != b[i]) { + return false; + } + } + return true; +} + +// The all-zero key ID - the original's [0u8; 16] probe. +pub fn key_id_zero(k: [16]u8) -> bool { + for i in 0..16 { + if (k[i] != 0) { + return false; + } + } + return true; +} + +// Whole-form equality over the fixed twelve nonce bytes. +pub fn nonces_equal(a: [12]u8, b: [12]u8) -> bool { + for i in 0..12 { + if (a[i] != b[i]) { + return false; + } + } + return true; +} + +// The all-zero nonce - the original's [0u8; 12] probe. +pub fn nonce_zero(n: [12]u8) -> bool { + for i in 0..12 { + if (n[i] != 0) { + return false; + } + } + return true; +} + +// The big-endian u64 of the nonce's last eight bytes - the +// original's nonce_to_u64, folded byte by byte through the +// int-widening cast. +pub fn nonce_to_u64(n: [12]u8) -> u64 { + var v: u64 = 0; + var wide: u64 = 0; + for i in 0..8 { + wide = @as(u64, n[i + 4]); + v = v * 256 + wide; + } + return v; +} + +// Whether record i repeats an earlier (key ID, nonce) pair - the +// original's BTreeSet insert probe, answered by a scan. +pub fn pair_seen_before(records: []const NonceRecord, i: usize) -> bool { + for j in 0..i { + if (key_ids_equal(records[j].key_id, records[i].key_id)) { + if (nonces_equal(records[j].nonce, records[i].nonce)) { + return true; + } + } + } + return false; +} + +// [VERIFIED] Validate padding nonce reuse. Returns Ok only when +// every rule holds, checked in the original's order: the batch +// ceiling, then per record the zero key, the zero nonce, the nonce +// value ceiling and the repeated pair. +pub fn validate_nonce_reuse(records: []const NonceRecord) -> NonceReuseVerdict { + if (records.len > PNRD_MAX_RECORDS) { + return NonceReuseVerdict { code: NonceReuseCode.TooMany, idx: 0, got: records.len, bound: PNRD_MAX_RECORDS, }; + } + for i in 0..records.len { + if (key_id_zero(records[i].key_id)) { + return NonceReuseVerdict { code: NonceReuseCode.ZeroKey, idx: i, got: 0, bound: 0, }; + } + if (nonce_zero(records[i].nonce)) { + return NonceReuseVerdict { code: NonceReuseCode.ZeroNonce, idx: i, got: 0, bound: 0, }; + } + if (nonce_to_u64(records[i].nonce) > PNRD_MAX_NONCE) { + return NonceReuseVerdict { code: NonceReuseCode.NonceOverflow, idx: i, got: 0, bound: 0, }; + } + if (pair_seen_before(records, i)) { + return NonceReuseVerdict { code: NonceReuseCode.Duplicate, idx: i, got: 0, bound: 0, }; + } + } + return NonceReuseVerdict { code: NonceReuseCode.Ok, idx: 0, got: 0, bound: 0, }; +} + +// The key IDs of the fixtures, one byte repeated sixteen times. +pub const KID_01: [16]u8 = [16]u8{1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,}; +pub const KID_02: [16]u8 = [16]u8{2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,}; +pub const ZERO_KID: [16]u8 = [16]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + +// The nonces of the fixtures: twelve bytes, the last eight the +// big-endian form of the value - the original's nonce(val) +// helper, entry by entry. +pub const NONCE_1: [12]u8 = [12]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1,}; +pub const NONCE_2: [12]u8 = [12]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2,}; +pub const NONCE_42: [12]u8 = [12]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 42,}; +pub const NONCE_MAX: [12]u8 = [12]u8{0, 0, 0, 0, 0, 0, 255, 255, 255, 255, 255, 255,}; +pub const NONCE_OVER: [12]u8 = [12]u8{0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0,}; +pub const ZERO_NONCE: [12]u8 = [12]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + +// **PNRD-01** - duplicate rejected: the second record repeats the +// first's key and nonce. +test pnrd_01_duplicate_rejected { + const records: [2]NonceRecord = [2]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_42, }, + NonceRecord { key_id: KID_01, nonce: NONCE_42, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.Duplicate); + assert(v.idx == 1); +} + +// **PNRD-02** - zero nonce rejected under a live key. +test pnrd_02_zero_nonce_rejected { + const records: [1]NonceRecord = [1]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: ZERO_NONCE, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.ZeroNonce); + assert(v.idx == 0); +} + +// **PNRD-03** - zero key rejected under a live nonce. +test pnrd_03_zero_key_rejected { + const records: [1]NonceRecord = [1]NonceRecord{ + NonceRecord { key_id: ZERO_KID, nonce: NONCE_1, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.ZeroKey); + assert(v.idx == 0); +} + +// **PNRD-04** - nonce overflow rejected: the nonce carries two to +// the forty-eighth, one over the maximum. +test pnrd_04_nonce_overflow_rejected { + const records: [1]NonceRecord = [1]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_OVER, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.NonceOverflow); + assert(v.idx == 0); +} + +// **PNRD-05** - too many rejected: 10001 records of a maximum +// 10000, built in a loop like the original's. The batch rule fires +// before any record is examined, so every record carries the same +// minimal pair. +test pnrd_05_too_many_rejected { + var records: [10001]NonceRecord; + for i in 0..10001 { + records[i] = NonceRecord { key_id: KID_01, nonce: NONCE_1, }; + } + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.TooMany); + assert(v.got == 10001); + assert(v.bound == 10000); +} + +// **PNRD-06** - the same nonce under a different key accepted. +test pnrd_06_same_nonce_diff_key_accepted { + const records: [2]NonceRecord = [2]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_42, }, + NonceRecord { key_id: KID_02, nonce: NONCE_42, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.Ok); +} + +// **PNRD-07** - the valid batch accepted: two nonces under the +// first key, the first nonce again under the second. +test pnrd_07_valid_accepted { + const records: [3]NonceRecord = [3]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_1, }, + NonceRecord { key_id: KID_01, nonce: NONCE_2, }, + NonceRecord { key_id: KID_02, nonce: NONCE_1, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.Ok); +} + +// **PNRD-08** - an empty batch accepted. +test pnrd_08_empty_accepted { + const records: [0]NonceRecord = [0]NonceRecord{}; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.Ok); +} + +// **PNRD-09** - a single record accepted. +test pnrd_09_single_accepted { + const records: [1]NonceRecord = [1]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_1, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.Ok); +} + +// **PNRD-10** - the boundary nonce accepted: the maximum value +// itself, one byte over nothing. +test pnrd_10_boundary_nonce_accepted { + const records: [1]NonceRecord = [1]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_MAX, }, + }; + const v = validate_nonce_reuse(&records); + assert(v.code == NonceReuseCode.Ok); +} + +// The six helpers have direct tests (coverage: Untested 0). +test byte_form_helpers_answer { + assert(key_ids_equal(KID_01, KID_01)); + assert(!key_ids_equal(KID_01, KID_02)); + assert(key_id_zero(ZERO_KID)); + assert(!key_id_zero(KID_01)); + assert(nonces_equal(NONCE_1, NONCE_1)); + assert(!nonces_equal(NONCE_1, NONCE_2)); + assert(nonce_zero(ZERO_NONCE)); + assert(!nonce_zero(NONCE_1)); +} + +test nonce_to_u64_answers { + assert(nonce_to_u64(NONCE_1) == 1); + assert(nonce_to_u64(NONCE_42) == 42); + assert(nonce_to_u64(NONCE_MAX) == 281474976710655); + assert(nonce_to_u64(NONCE_OVER) == 281474976710656); + assert(nonce_to_u64(ZERO_NONCE) == 0); +} + +test pair_seen_before_answers { + const records: [3]NonceRecord = [3]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_1, }, + NonceRecord { key_id: KID_01, nonce: NONCE_2, }, + NonceRecord { key_id: KID_01, nonce: NONCE_1, }, + }; + assert(!pair_seen_before(&records, 0)); + assert(!pair_seen_before(&records, 1)); + assert(pair_seen_before(&records, 2)); +} + +// Rule order is the original's: the zero key before the zero nonce, +// the zero nonce before the repeated pair, and the nonce ceiling +// before the repeated pair. +test rule_order_matches_original { + const both_zero: [1]NonceRecord = [1]NonceRecord{ + NonceRecord { key_id: ZERO_KID, nonce: ZERO_NONCE, }, + }; + const v1 = validate_nonce_reuse(&both_zero); + assert(v1.code == NonceReuseCode.ZeroKey); + assert(v1.idx == 0); + + const zero_twice: [2]NonceRecord = [2]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: ZERO_NONCE, }, + NonceRecord { key_id: KID_01, nonce: ZERO_NONCE, }, + }; + const v2 = validate_nonce_reuse(&zero_twice); + assert(v2.code == NonceReuseCode.ZeroNonce); + assert(v2.idx == 0); + + const over_twice: [2]NonceRecord = [2]NonceRecord{ + NonceRecord { key_id: KID_01, nonce: NONCE_OVER, }, + NonceRecord { key_id: KID_01, nonce: NONCE_OVER, }, + }; + const v3 = validate_nonce_reuse(&over_twice); + assert(v3.code == NonceReuseCode.NonceOverflow); + assert(v3.idx == 0); +}