diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_key_rotation_uniformity_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_key_rotation_uniformity_guard.json new file mode 100644 index 0000000000..9f0a565497 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_key_rotation_uniformity_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:540333d960db61399d83acce171e83405a3ca6e1db7e9f44e85fc35aede495ec", + "gen_hash_rust": "sha256:c0c9ce296474bcc4dc6f81fa3213a6ebdd9b277db1d3ab8c2ce23acb906fbb55", + "gen_hash_verilog": "sha256:5aaebf03f50fdd63dc1066f0ae8c13e6a579fb5d1f8b3bc2021e3d13df7252a4", + "gen_hash_zig": "sha256:94e3d788d059d6dcea3b78580424f1eb30875b08e92acf0bcda6cc74c9f72bfd", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_key_rotation_uniformity_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-16T15:05:47Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:027136f8d7c7e572d50b786715a7944473c4f3412a853a5ac7c6dfe3a76e153e", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_rotation_uniformity_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "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 cfbb74965e..b70d54daf7 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -897,6 +897,7 @@ {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_crypto_binding_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_fill_byte_randomness_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_derivation_domain_separation_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_rotation_uniformity_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_length_class_transition_uniformity_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_length_distribution_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_rotation_uniformity_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_rotation_uniformity_guard.t27 new file mode 100644 index 0000000000..a3f81b99c8 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_rotation_uniformity_guard.t27 @@ -0,0 +1,312 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_key_rotation_uniformity_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_key_rotation_uniformity_guard.rs +// (CR-CHAT-04 - Padding key rotation uniformity guard, Wave-101 +// Lane A, requirement R-CHAT-4). +// +// Padding keys must rotate on a uniform clock: regular rotation +// lets an observer align size-class changes with key boundaries, +// a stale key repeats the class-selection pattern across epochs, +// and irregular timing leaks load. The rules, in the original's +// order: the batch ceiling, then per rotation the zero-key +// probe, the interval floor and ceiling, the monotonic +// non-decreasing check and the repeated-key scan - equal +// intervals pass. +// +// The original returns Result<(), KeyRotationError>. This port +// carries the verdict as a named struct (owner decision D5): Ok +// first, then the six error variants in the original's +// declaration order - TooFrequent, TooSlow, NotMonotonic, +// DuplicateKey, ZeroKey, TooMany - with every payload field: idx +// and the measured/min or measured/max interval for the bounds, +// idx with prev and current for the monotonic break, idx for the +// id rules, and got and max for the ceiling. +// +// The BTreeSet dedup becomes a scan over the rotations already +// visited; the intervals stay the original's u64 arithmetic. + +// Minimum rotation interval (messages). +pub const PKRU_MIN_INTERVAL: u64 = 100; + +// Maximum rotation interval (messages). +pub const PKRU_MAX_INTERVAL: u64 = 10000; + +// Maximum rotations per batch. +pub const PKRU_MAX_ROTATIONS: usize = 1024; + +// Key ID length. +pub const PKRU_KEY_ID_LEN: usize = 16; + +// A padding key rotation record. +pub struct KeyRotation { + key_id: [16]u8, + interval: u64, +} + +// Verdict codes: Ok(()) and KeyRotationError's variants, in declaration order. +pub enum KeyRotationCode { + Ok, + TooFrequent, + TooSlow, + NotMonotonic, + DuplicateKey, + ZeroKey, + TooMany, +} + +// The verdict of the key rotation validation, with every error +// payload field. +pub struct KeyRotationVerdict { + code: KeyRotationCode, + idx: usize, + got: usize, + bound: usize, + got64: u64, + bound64: u64, +} + +// 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(id: [16]u8) -> bool { + for i in 0..16 { + if (id[i] != 0) { + return false; + } + } + return true; +} + +// Whether rotation i repeats an earlier key - the original's +// BTreeSet insert probe, answered by a scan. +pub fn key_seen_before(rotations: []const KeyRotation, i: usize) -> bool { + for j in 0..i { + if (key_ids_equal(rotations[j].key_id, rotations[i].key_id)) { + return true; + } + } + return false; +} + +// [VERIFIED] Validate padding key rotation uniformity. Returns +// Ok only when every rule holds, checked in the original's +// order: the batch ceiling, then per rotation the zero key, the +// interval floor and ceiling, the monotonic check and the +// repeated key. +pub fn validate_key_rotations(rotations: []const KeyRotation) -> KeyRotationVerdict { + if (rotations.len > PKRU_MAX_ROTATIONS) { + return KeyRotationVerdict { code: KeyRotationCode.TooMany, idx: 0, got: rotations.len, bound: PKRU_MAX_ROTATIONS, got64: 0, bound64: 0, }; + } + var prev: u64 = 0; + for i in 0..rotations.len { + if (key_id_zero(rotations[i].key_id)) { + return KeyRotationVerdict { code: KeyRotationCode.ZeroKey, idx: i, got: 0, bound: 0, got64: 0, bound64: 0, }; + } + if (rotations[i].interval < PKRU_MIN_INTERVAL) { + return KeyRotationVerdict { code: KeyRotationCode.TooFrequent, idx: i, got: 0, bound: 0, got64: rotations[i].interval, bound64: PKRU_MIN_INTERVAL, }; + } + if (rotations[i].interval > PKRU_MAX_INTERVAL) { + return KeyRotationVerdict { code: KeyRotationCode.TooSlow, idx: i, got: 0, bound: 0, got64: rotations[i].interval, bound64: PKRU_MAX_INTERVAL, }; + } + if (i > 0) { + if (rotations[i].interval < prev) { + return KeyRotationVerdict { code: KeyRotationCode.NotMonotonic, idx: i, got: 0, bound: 0, got64: rotations[i].interval, bound64: prev, }; + } + } + if (key_seen_before(rotations, i)) { + return KeyRotationVerdict { code: KeyRotationCode.DuplicateKey, idx: i, got: 0, bound: 0, got64: 0, bound64: 0, }; + } + prev = rotations[i].interval; + } + return KeyRotationVerdict { code: KeyRotationCode.Ok, idx: 0, got: 0, bound: 0, got64: 0, bound64: 0, }; +} + +// The key ids of the fixtures, one byte repeated sixteen times - +// the original's kid(byte) helper, entry by entry. +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 KID_03: [16]u8 = [16]u8{3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,}; +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 leading key bytes of the too-many fixture: the original's +// (i % 254 + 1) walk over 0..=1024. +pub const PKRU_FLOOD_1025: [1025]u8 = [1025]u8{1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 1, 2, 3, 4, 5, 6, 7, 8, 9,}; + +// **PKRU-01** - too frequent rejected: ninety-nine messages of a +// floor hundred. +test pkru_01_too_frequent_rejected { + const rs: [1]KeyRotation = [1]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 99, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.TooFrequent); + assert(v.idx == 0); + assert(v.got64 == 99); + assert(v.bound64 == 100); +} + +// **PKRU-02** - too slow rejected: 10001 messages of a ceiling +// ten thousand. +test pkru_02_too_slow_rejected { + const rs: [1]KeyRotation = [1]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 10001, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.TooSlow); + assert(v.idx == 0); + assert(v.got64 == 10001); + assert(v.bound64 == 10000); +} + +// **PKRU-03** - not monotonic rejected: four hundred after five +// hundred. +test pkru_03_not_monotonic_rejected { + const rs: [2]KeyRotation = [2]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_02, interval: 400, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.NotMonotonic); + assert(v.idx == 1); + assert(v.got64 == 400); + assert(v.bound64 == 500); +} + +// **PKRU-04** - duplicate key rejected: the second rotation +// repeats the first's id. +test pkru_04_duplicate_rejected { + const rs: [2]KeyRotation = [2]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_01, interval: 600, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.DuplicateKey); + assert(v.idx == 1); +} + +// **PKRU-05** - zero key rejected under a live interval. +test pkru_05_zero_key_rejected { + const rs: [1]KeyRotation = [1]KeyRotation{ + KeyRotation { key_id: ZERO_KID, interval: 500, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.ZeroKey); + assert(v.idx == 0); +} + +// **PKRU-06** - too many rejected: 1025 rotations of a maximum +// 1024, built in a loop like the original's, each key carrying +// its walk byte and the minimum interval. The batch rule fires +// before any rotation is examined. +test pkru_06_too_many_rejected { + var rs: [1025]KeyRotation; + for i in 0..1025 { + var id: [16]u8 = [16]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; + id[0] = PKRU_FLOOD_1025[i]; + rs[i] = KeyRotation { key_id: id, interval: 100, }; + } + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.TooMany); + assert(v.got == 1025); + assert(v.bound == 1024); +} + +// **PKRU-07** - the valid rotations accepted: five hundred, +// five hundred, six hundred - non-decreasing. +test pkru_07_valid_accepted { + const rs: [3]KeyRotation = [3]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_02, interval: 500, }, + KeyRotation { key_id: KID_03, interval: 600, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.Ok); +} + +// **PKRU-08** - an empty batch accepted. +test pkru_08_empty_accepted { + const rs: [0]KeyRotation = [0]KeyRotation{}; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.Ok); +} + +// **PKRU-09** - a single rotation at the exact floor accepted. +test pkru_09_min_interval_accepted { + const rs: [1]KeyRotation = [1]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 100, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.Ok); +} + +// **PKRU-10** - equal intervals accepted: non-decreasing means +// equal passes. +test pkru_10_equal_intervals_accepted { + const rs: [3]KeyRotation = [3]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_02, interval: 500, }, + KeyRotation { key_id: KID_03, interval: 500, }, + }; + const v = validate_key_rotations(&rs); + assert(v.code == KeyRotationCode.Ok); +} + +// The three helpers have direct tests (coverage: Untested 0). +test pkru_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)); + const three: [3]KeyRotation = [3]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_02, interval: 500, }, + KeyRotation { key_id: KID_01, interval: 500, }, + }; + assert(!key_seen_before(&three, 0)); + assert(!key_seen_before(&three, 1)); + assert(key_seen_before(&three, 2)); +} + +// Rule order is the original's: the zero key before the interval +// floor, the floor before the monotonic check, the ceiling +// before the repeated key, the monotonic check before the +// repeated key. +test rule_order_matches_original { + const zero_fast: [1]KeyRotation = [1]KeyRotation{ + KeyRotation { key_id: ZERO_KID, interval: 50, }, + }; + const v1 = validate_key_rotations(&zero_fast); + assert(v1.code == KeyRotationCode.ZeroKey); + + const fast_backstep: [2]KeyRotation = [2]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_02, interval: 50, }, + }; + const v2 = validate_key_rotations(&fast_backstep); + assert(v2.code == KeyRotationCode.TooFrequent); + assert(v2.idx == 1); + + const slow_twin: [2]KeyRotation = [2]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_01, interval: 20000, }, + }; + const v3 = validate_key_rotations(&slow_twin); + assert(v3.code == KeyRotationCode.TooSlow); + assert(v3.idx == 1); + + const backstep_twin: [2]KeyRotation = [2]KeyRotation{ + KeyRotation { key_id: KID_01, interval: 500, }, + KeyRotation { key_id: KID_01, interval: 400, }, + }; + const v4 = validate_key_rotations(&backstep_twin); + assert(v4.code == KeyRotationCode.NotMonotonic); + assert(v4.idx == 1); +}