diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_byte_entropy_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_byte_entropy_guard.json new file mode 100644 index 0000000000..585d63b527 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_byte_entropy_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:447a6883b3851936a9f01e7736dc84a5ca9cbc1b341adccab87f6fdc8016c472", + "gen_hash_rust": "sha256:1e8d29faa7f66b17fd5d9857f3600b6086e4c594e724fbc0016fb92ed3be2a0d", + "gen_hash_verilog": "sha256:895282ce5203eb9f5cf1b1f4d93b02c7660ca793dae1f680a9017caf8c106a7f", + "gen_hash_zig": "sha256:abed3e29b9b8781d92d85252559824ec76082f16b0f2e2f8f05e11ba5ab625a7", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_byte_entropy_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-15T21:59:06Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:9571ce3cbdce39b7aa059c66765315503e8040a71ba0a186926b786ee2dc0be9", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_byte_entropy_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 3483595ccc..337a77dbed 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -859,6 +859,7 @@ {"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_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-04/src/padding_byte_entropy_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/blind_signature_sender_token.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_decoy_ratio_governor.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_byte_entropy_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_byte_entropy_guard.t27 new file mode 100644 index 0000000000..3ddc532b38 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_byte_entropy_guard.t27 @@ -0,0 +1,254 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_byte_entropy_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_byte_entropy_guard.rs +// (CR-CHAT-04 - Padding byte entropy guard, Wave-77 Lane A, requirement R-CHAT-4). +// +// Padding bytes must resist statistical separation from the encrypted +// payload: not empty, within its length bounds, not one repeated byte, +// at least PBEG_MIN_UNIQUE distinct values, and no single byte more +// frequent than the PBEG_MAX_FREQ_RATIO_NUM/PBEG_MAX_FREQ_RATIO_DEN +// ceiling. The original's BTreeMap frequency count becomes a fixed +// 256-slot table indexed by the byte (the conventions' own form for a +// key range that fits an array); the table is initialized from a +// literal because the Rust backend leaves an uninitialized binding +// unreadable (E0381, measured). +// +// The original returns Result<(), PaddingEntropyError>. 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 - +// TooShort, TooFewUnique, ByteTooFrequent, TooLong, AllSameByte, Empty. +// The verdict carries the unique count TooFewUnique reports (got). + +// Minimum padding length. +pub const PBEG_MIN_LEN: usize = 16; + +// Maximum padding length. +pub const PBEG_MAX_LEN: usize = 65536; + +// Minimum unique byte values. +pub const PBEG_MIN_UNIQUE: usize = 8; + +// Maximum frequency ratio numerator (max count / total). +pub const PBEG_MAX_FREQ_RATIO_NUM: usize = 4; + +// Maximum frequency ratio denominator. +pub const PBEG_MAX_FREQ_RATIO_DEN: usize = 10; + +// Verdict codes: Ok(()) and PaddingEntropyError's variants, in declaration order. +pub enum PaddingEntropyCode { + Ok, + TooShort, + TooFewUnique, + ByteTooFrequent, + TooLong, + AllSameByte, + Empty, +} + +// The verdict of the entropy validation, with the payload field the one +// reporting variant carries. +pub struct PaddingEntropyVerdict { + code: PaddingEntropyCode, + got: usize, +} + +// The zeroed frequency table, initialized at declaration: the Rust +// backend emits an uninitialized binding otherwise and the read on the +// right side of the increment fails (E0381, measured). +pub const PBEG_ZERO_TABLE: [256]u32 = [256]u32{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + +// The number of distinct byte values in the padding. +pub fn unique_count(padding: []const u8) -> usize { + var freq: [256]u32 = PBEG_ZERO_TABLE; + for i in 0..padding.len { + const b: u8 = padding[i]; + const slot: usize = @as(usize, b); + freq[slot] = freq[slot] + 1; + } + var unique: usize = 0; + for i in 0..256 { + if (freq[i] > 0) { + unique = unique + 1; + } + } + return unique; +} + +// The highest single-byte count in the padding. +pub fn max_count(padding: []const u8) -> u32 { + var freq: [256]u32 = PBEG_ZERO_TABLE; + for i in 0..padding.len { + const b: u8 = padding[i]; + const slot: usize = @as(usize, b); + freq[slot] = freq[slot] + 1; + } + var m: u32 = 0; + for i in 0..256 { + if (freq[i] > m) { + m = freq[i]; + } + } + return m; +} + +// [VERIFIED] Validate that padding bytes have sufficient entropy. +// Returns Ok only when every rule holds, checked in the original's +// order: non-empty, at least PBEG_MIN_LEN long, at most PBEG_MAX_LEN +// long, not one repeated byte, at least PBEG_MIN_UNIQUE distinct +// values, and no byte more frequent than the ratio ceiling. +pub fn validate_padding_entropy(padding: []const u8) -> PaddingEntropyVerdict { + if (padding.len == 0) { + return PaddingEntropyVerdict { code: PaddingEntropyCode.Empty, got: 0, }; + } + if (padding.len < PBEG_MIN_LEN) { + return PaddingEntropyVerdict { code: PaddingEntropyCode.TooShort, got: 0, }; + } + if (padding.len > PBEG_MAX_LEN) { + return PaddingEntropyVerdict { code: PaddingEntropyCode.TooLong, got: 0, }; + } + const first: u8 = padding[0]; + var same: bool = true; + for i in 0..padding.len { + if (padding[i] != first) { + same = false; + } + } + if (same) { + return PaddingEntropyVerdict { code: PaddingEntropyCode.AllSameByte, got: 0, }; + } + const unique: usize = unique_count(padding); + if (unique < PBEG_MIN_UNIQUE) { + return PaddingEntropyVerdict { code: PaddingEntropyCode.TooFewUnique, got: unique, }; + } + const m: u32 = max_count(padding); + if (@as(u64, m) * @as(u64, PBEG_MAX_FREQ_RATIO_DEN) > @as(u64, padding.len) * @as(u64, PBEG_MAX_FREQ_RATIO_NUM)) { + return PaddingEntropyVerdict { code: PaddingEntropyCode.ByteTooFrequent, got: 0, }; + } + return PaddingEntropyVerdict { code: PaddingEntropyCode.Ok, got: 0, }; +} + +// The fixtures of the tests, precomputed literal tables: the original +// builds each by arithmetic over its index; the literals carry the same +// bytes without a narrowing cast. +pub const PBEG_GOOD: [16]u8 = [16]u8{42, 59, 76, 93, 110, 127, 144, 161, 178, 195, 212, 229, 246, 7, 24, 41,}; +pub const PBEG_MOD3: [16]u8 = [16]u8{0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0,}; +pub const PBEG_ALT: [16]u8 = [16]u8{1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0,}; +pub const PBEG_MINL: [16]u8 = [16]u8{7, 14, 21, 28, 35, 42, 49, 56, 63, 70, 77, 84, 91, 98, 105, 112,}; +pub const PBEG_BIG: [256]u8 = [256]u8{17, 148, 23, 154, 29, 160, 35, 166, 41, 172, 47, 178, 53, 184, 59, 190, 65, 196, 71, 202, 77, 208, 83, 214, 89, 220, 95, 226, 101, 232, 107, 238, 113, 244, 119, 250, 125, 0, 131, 6, 137, 12, 143, 18, 149, 24, 155, 30, 161, 36, 167, 42, 173, 48, 179, 54, 185, 60, 191, 66, 197, 72, 203, 78, 209, 84, 215, 90, 221, 96, 227, 102, 233, 108, 239, 114, 245, 120, 251, 126, 1, 132, 7, 138, 13, 144, 19, 150, 25, 156, 31, 162, 37, 168, 43, 174, 49, 180, 55, 186, 61, 192, 67, 198, 73, 204, 79, 210, 85, 216, 91, 222, 97, 228, 103, 234, 109, 240, 115, 246, 121, 252, 127, 2, 133, 8, 139, 14, 145, 20, 151, 26, 157, 32, 163, 38, 169, 44, 175, 50, 181, 56, 187, 62, 193, 68, 199, 74, 205, 80, 211, 86, 217, 92, 223, 98, 229, 104, 235, 110, 241, 116, 247, 122, 253, 128, 3, 134, 9, 140, 15, 146, 21, 152, 27, 158, 33, 164, 39, 170, 45, 176, 51, 182, 57, 188, 63, 194, 69, 200, 75, 206, 81, 212, 87, 218, 93, 224, 99, 230, 105, 236, 111, 242, 117, 248, 123, 254, 129, 4, 135, 10, 141, 16, 147, 22, 153, 28, 159, 34, 165, 40, 171, 46, 177, 52, 183, 58, 189, 64, 195, 70, 201, 76, 207, 82, 213, 88, 219, 94, 225, 100, 231, 106, 237, 112, 243, 118, 249, 124, 255, 130, 5, 136, 11, 142,}; +pub const PBEG_EXACT: [16]u8 = [16]u8{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15,}; +pub const PBEG_FREQ: [16]u8 = [16]u8{0, 1, 0, 2, 0, 3, 0, 4, 0, 5, 0, 6, 0, 7, 0, 1,}; + +// **PBEG-01** - too short rejected: 4 of a minimum 16. +test pbeg_01_too_short_rejected { + const xs: [4]u8 = [4]u8{1, 2, 3, 4,}; + const v = validate_padding_entropy(&xs); + assert(v.code == PaddingEntropyCode.TooShort); +} + +// **PBEG-02** - too few unique bytes rejected: three distinct values of +// a required eight, reported in the verdict's got. +test pbeg_02_too_few_unique_rejected { + const v = validate_padding_entropy(&PBEG_MOD3); + assert(v.code == PaddingEntropyCode.TooFewUnique); + assert(v.got == 3); +} + +// **PBEG-03** - the alternating fixture of the original. The original +// discards the verdict; this port asserts the deterministic outcome of +// the same bytes, which the rule order makes TooFewUnique with two +// distinct values, so the port is not vacuous. +test pbeg_03_alternating_reports_two_unique { + const v = validate_padding_entropy(&PBEG_ALT); + assert(v.code == PaddingEntropyCode.TooFewUnique); + assert(v.got == 2); +} + +// **PBEG-04** - too long rejected: 65537 of a maximum 65536, built in a +// loop like the original's; the length rule fires before any scan. +test pbeg_04_too_long_rejected { + var big: [65537]u8; + for i in 0..65537 { + big[i] = 0xAB; + } + const v = validate_padding_entropy(&big); + assert(v.code == PaddingEntropyCode.TooLong); +} + +// **PBEG-05** - all same byte rejected: sixteen 0x42. +test pbeg_05_all_same_rejected { + const xs: [16]u8 = [16]u8{66, 66, 66, 66, 66, 66, 66, 66, 66, 66, 66, 66, 66, 66, 66, 66,}; + const v = validate_padding_entropy(&xs); + assert(v.code == PaddingEntropyCode.AllSameByte); +} + +// **PBEG-06** - empty rejected. +test pbeg_06_empty_rejected { + const xs: [0]u8 = [0]u8{}; + const v = validate_padding_entropy(&xs); + assert(v.code == PaddingEntropyCode.Empty); +} + +// **PBEG-07** - good padding accepted. +test pbeg_07_good_accepted { + const v = validate_padding_entropy(&PBEG_GOOD); + assert(v.code == PaddingEntropyCode.Ok); +} + +// **PBEG-08** - the minimum length with diverse bytes accepted. +test pbeg_08_min_len_accepted { + const v = validate_padding_entropy(&PBEG_MINL); + assert(v.code == PaddingEntropyCode.Ok); +} + +// **PBEG-09** - large padding accepted: all 256 byte values once. +test pbeg_09_large_accepted { + const v = validate_padding_entropy(&PBEG_BIG); + assert(v.code == PaddingEntropyCode.Ok); +} + +// **PBEG-10** - exactly the minimum eight unique bytes accepted. +test pbeg_10_exact_unique_accepted { + const v = validate_padding_entropy(&PBEG_EXACT); + assert(v.code == PaddingEntropyCode.Ok); +} + +// The byte-too-frequent branch: eight zeros among sixteen bytes is more +// than the 4/10 ceiling (80 over 64), while the eight distinct values +// pass the unique rule first - the original has no asserting test for +// this branch (its PBEG-03 discards), so this direct test covers it. +test pbeg_freq_branch_rejected { + const v = validate_padding_entropy(&PBEG_FREQ); + assert(v.code == PaddingEntropyCode.ByteTooFrequent); +} + +// The two helpers have direct tests (coverage: Untested 0). +test unique_count_answers { + assert(unique_count(&PBEG_MOD3) == 3); + assert(unique_count(&PBEG_EXACT) == 16); + assert(unique_count(&PBEG_GOOD) == 16); +} + +test max_count_answers { + assert(max_count(&PBEG_MOD3) == 6); + assert(max_count(&PBEG_EXACT) == 1); +} + +// Rule order is the original's: emptiness before length, the short +// bound before the long bound, the long bound before the same-byte +// scan, the same-byte scan before the unique count, and the unique +// count before the frequency ceiling. +test rule_order_matches_original { + const xs: [4]u8 = [4]u8{1, 2, 3, 4,}; + const va = validate_padding_entropy(&xs); + assert(va.code == PaddingEntropyCode.TooShort); + + var big: [65537]u8; + for i in 0..65537 { + big[i] = 0xAB; + } + const vb = validate_padding_entropy(&big); + assert(vb.code == PaddingEntropyCode.TooLong); + + const vc = validate_padding_entropy(&PBEG_MOD3); + assert(vc.code == PaddingEntropyCode.TooFewUnique); +}