diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-02::src::skipped_message_key_gap_bound_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-02::src::skipped_message_key_gap_bound_guard.json new file mode 100644 index 0000000000..c966216620 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-02::src::skipped_message_key_gap_bound_guard.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+d06eaedc9", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:01122bcbbab59814bd7f795e4e59ef245598b643f7403d6a826a2ecb1e2b73bd", + "gen_hash_rust": "sha256:298b2c47528b5a0959dff1c0a3768f0fc22947e98d2c7ad07fd770f1505a6b57", + "gen_hash_verilog": "sha256:e11d7117bf758f4cd70e7b5b51fd025615f25d74f05285582805ee1111e2647b", + "gen_hash_zig": "sha256:cbf3229435e8c08c5fa20ec1d4f78d409102e79aa9fc98535f57121a48d0feed", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-02::src::skipped_message_key_gap_bound_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-14T22:45:01Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:ac71c5cc5602553c3aa0d0a3409a8e7c75bd5f1946806e1f2c09e9aba1fc972a", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/skipped_message_key_gap_bound_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 17, + "total": 17, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-LAWS::src::lib.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-LAWS::src::lib.json new file mode 100644 index 0000000000..b046240cb5 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-LAWS::src::lib.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+d06eaedc9", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:9c91e1f56476d20d3633c1c7f5e8f8f5e5d0e686f6a9ec6c4da45a7aca38b03a", + "gen_hash_rust": "sha256:7780d5e67b94a1f8ce9c433fc52fd16ba10a1968e20885e931ee3ba269ece526", + "gen_hash_verilog": "sha256:b00ac8d994db3153067bdf3747f20fcd8da1fc745aeb05c18e892618ba7d6bc8", + "gen_hash_zig": "sha256:630100ec7499955e3b4dfe58613c75c6ff850096158b8cfb400643717d4a2a89", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-LAWS::src::lib", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-14T22:45:05Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:4f12393eeeb9aa092e68c71c1db528e1192c30ce8d1bfe5583e3d6ac56f3b4dc", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 6, + "total": 6, + "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 26ba73e792..2742434874 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -851,6 +851,7 @@ {"path": "specs/port/trios/crates/trios-bridge/src/main.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-01/src/key_package_expiry_guard.t27", "t27b": "pass"}, {"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-02/src/skipped_message_key_gap_bound_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-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/skipped_message_key_gap_bound_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/skipped_message_key_gap_bound_guard.t27 index 76602b06d7..f5024b7b4f 100644 --- a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/skipped_message_key_gap_bound_guard.t27 +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-02/src/skipped_message_key_gap_bound_guard.t27 @@ -1,165 +1,261 @@ -//! # CR-CHAT-02 — Skipped message key gap bound guard (Wave-80 Lane A) -//! -//! RATCHET — skipped message key gaps must be bounded, R-CHAT-2. -//! -//! In the double ratchet, out-of-order messages cause skipped message -//! keys to be stored for later use. If the gap between two consecutive -//! skipped keys is unbounded: -//! -//! * **Memory exhaustion** — an attacker forces the receiver to store -//! keys for every chain index from 0 to N, where N is unbounded. -//! * **DoS via gap** — a single message at chain index 1_000_000 -//! forces the receiver to skip and store 1M keys. -//! * **Timing attack** — large gaps cause processing delays that -//! reveal which messages are out-of-order. -//! -//! trios-chat enforces **6 rules**: -//! -//! 1. Gap between consecutive skipped keys <= `SMKG_MAX_GAP`. -//! 2. First skipped key index >= `SMKG_MIN_INDEX`. -//! 3. Total skipped keys <= `SMKG_MAX_SKIPPED`. -//! 4. Skipped key indices are strictly increasing. -//! 5. No duplicate indices. -//! 6. All indices < `SMKG_MAX_INDEX`. -//! -//! Tests **SMKG-01..10**. Error enum [`SkippedGapError`]. -//! -//! Anchor: `phi^2 + phi^-2 = 3 * TRINITY * CHAT * SKIPPED-KEY-GAP` - -/// Maximum gap between consecutive skipped keys. +module port::trios::crates::trios-chat::rings::CR-CHAT-02::src::skipped_message_key_gap_bound_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-02/src/ +// skipped_message_key_gap_bound_guard.rs @ 8b229e9489ee (1 function, +// 4 constants, 1 error enum, 10 tests SMKG-01..10). +// +// CR-CHAT-02 -- Skipped message key gap bound guard (Wave-80 Lane A). +// +// RATCHET -- skipped message key gaps must be bounded, R-CHAT-2. In the +// double ratchet, out-of-order messages cause skipped message keys to be +// stored for later use. If the gap between two consecutive skipped keys is +// unbounded: memory exhaustion (keys for every chain index from 0 to N), +// DoS via gap (one message at chain index 1_000_000 forces 1M skipped keys) +// and a timing signal that reveals which messages are out of order. +// +// Repair of the first port (t27 PR 8500), which did not compile in Zig +// (payload enum variants and a ?SkippedGapError return) and indexed a +// [256]bool bitmap by the key index, which goes up to SMKG_MAX_INDEX = +// 1_000_000. This version: +// - returns a verdict struct (owner decision D5 of the Trinity Secure Chat +// rewrite): a payload-free code with Ok first, then the original variants +// in declaration order, plus `value`, the u32 payload of the variant; +// - detects a duplicate by scanning the earlier inputs, which is what the +// original's BTreeSet of seen indices answers, without a value-indexed +// array; +// - keeps the original's order of checks: count, then per index: too large, +// duplicate, not increasing, gap; +// - adds no check the original does not make: the original never returns +// IndexBelowMin (SMKG_MIN_INDEX is 0 and indices are u32), so the variant +// is kept for the adapter and is unreachable here, as in the original. +// +// Anchor: phi^2 + phi^-2 = 3 * TRINITY * CHAT * SKIPPED-KEY-GAP + +// Maximum gap between consecutive skipped keys. pub const SMKG_MAX_GAP: u32 = 32; -/// Minimum key index. +// Minimum key index. pub const SMKG_MIN_INDEX: u32 = 0; -/// Maximum total skipped keys. +// Maximum total skipped keys. pub const SMKG_MAX_SKIPPED: usize = 256; -/// Maximum key index. -pub const SMKG_MAX_INDEX: u32 = 1_000_000; +// Maximum key index. +pub const SMKG_MAX_INDEX: u32 = 1000000; -/// All ways skipped gap validation can fail. -pub enum SkippedGapError { - /// Gap too large. - GapTooLarge(u32), - /// Index below minimum. - IndexBelowMin(u32), - /// Too many skipped keys. +// Ok, then the variants of the original SkippedGapError in declaration order. +pub enum SkippedGapCode { + Ok, + GapTooLarge, + IndexBelowMin, TooManySkipped, - /// Indices not strictly increasing. NotIncreasing, - /// Duplicate index. - DuplicateIndex(u32), - /// Index exceeds maximum. - IndexTooLarge(u32), + DuplicateIndex, + IndexTooLarge, +} + +// The verdict. `value` is the u32 payload of the variant: the gap for +// GapTooLarge, the index for IndexBelowMin, DuplicateIndex and +// IndexTooLarge; 0 for Ok, TooManySkipped and NotIncreasing. +pub struct SkippedGapVerdict { + code: SkippedGapCode, + value: u32, } -/// `[VERIFIED]` Validate that skipped message key gaps are bounded. -pub fn validate_skipped_key_gaps( - indices: []u32, -) -> ?SkippedGapError { +fn smkg_verdict(code: SkippedGapCode, value: u32) -> SkippedGapVerdict { + return SkippedGapVerdict { code: code, value: value, }; +} + +// True when indices[0..i] already holds the value indices[i]. +fn smkg_seen_before(indices: []const u32, i: usize) -> bool { + for (j in 0..i) { + if (indices[j] == indices[i]) { + return true; + } + } + return false; +} + +// [VERIFIED] Validate that skipped message key gaps are bounded. +pub fn validate_skipped_key_gaps(indices: []const u32) -> SkippedGapVerdict { if (indices.len > SMKG_MAX_SKIPPED) { - return .TooManySkipped; + return smkg_verdict(SkippedGapCode.TooManySkipped, 0); } - - var seen: [SMKG_MAX_SKIPPED]bool = [_]bool{false} ** SMKG_MAX_SKIPPED; - var i: usize = 0; - for (indices) |idx| { + for (i in 0..indices.len) { + const idx: u32 = indices[i]; if (idx > SMKG_MAX_INDEX) { - return .IndexTooLarge(idx); - } - if (idx < SMKG_MIN_INDEX) { - return .IndexBelowMin(idx); - } - - if (seen[idx]) { - return .DuplicateIndex(idx); + return smkg_verdict(SkippedGapCode.IndexTooLarge, idx); } - seen[idx] = true; - - if (i > 0 and idx <= indices[i - 1]) { - return .NotIncreasing; + if (smkg_seen_before(indices, i)) { + return smkg_verdict(SkippedGapCode.DuplicateIndex, idx); } - if (i > 0) { - const gap = idx - indices[i - 1]; + const prev: u32 = indices[i - 1]; + if (idx <= prev) { + return smkg_verdict(SkippedGapCode.NotIncreasing, 0); + } + const gap: u32 = idx - prev; if (gap > SMKG_MAX_GAP) { - return .GapTooLarge(gap); + return smkg_verdict(SkippedGapCode.GapTooLarge, gap); } } - i += 1; } - - return null; + return smkg_verdict(SkippedGapCode.Ok, 0); } +// --------------------------------------------------------------------- +// Tests. SMKG-01..10 transcribed from the original with exact verdicts, +// then the boundaries the first port broke and the original's order of +// checks. +// --------------------------------------------------------------------- + +// SMKG-01 -- gap too large rejected. test smkg_01_gap_large_rejected { - const indices = [u32]{0, 1, 100}; - const result = validate_skipped_key_gaps(&indices); - const expected = .GapTooLarge(99); - assert(result == expected); + var indices: [3]u32 = [3]u32{0, 1, 100}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.GapTooLarge); + assert(v.value == 99); } +// SMKG-02 -- too many skipped rejected (SMKG_MAX_SKIPPED + 1 indices). test smkg_02_too_many_rejected { - var indices: [SMKG_MAX_SKIPPED + 1]u32 = undefined; - var i: usize = 0; - for (&indices) |*idx| { - idx.* = @intCast(i); - i += 1; + var indices: [257]u32 = undefined; + var n: u32 = 0; + for (i in 0..257) { + indices[i] = n; + n += 1; } - const result = validate_skipped_key_gaps(&indices); - assert(result == .TooManySkipped); + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.TooManySkipped); + assert(v.value == 0); } +// SMKG-03 -- not increasing rejected. test smkg_03_not_increasing_rejected { - const indices = [u32]{1, 3, 2}; - const result = validate_skipped_key_gaps(&indices); - assert(result == .NotIncreasing); + var indices: [3]u32 = [3]u32{1, 3, 2}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.NotIncreasing); + assert(v.value == 0); } +// SMKG-04 -- duplicate index rejected. test smkg_04_duplicate_rejected { - const indices = [u32]{1, 2, 2}; - const result = validate_skipped_key_gaps(&indices); - assert(result == .DuplicateIndex(2)); + var indices: [3]u32 = [3]u32{1, 2, 2}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.DuplicateIndex); + assert(v.value == 2); } +// SMKG-05 -- index too large rejected. test smkg_05_index_large_rejected { - const indices = [u32]{SMKG_MAX_INDEX + 1}; - const result = validate_skipped_key_gaps(&indices); - assert(result == .IndexTooLarge(SMKG_MAX_INDEX + 1)); + var indices: [1]u32 = [1]u32{1000001}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.IndexTooLarge); + assert(v.value == SMKG_MAX_INDEX + 1); } +// SMKG-06 -- valid indices accepted. test smkg_06_valid_accepted { - const indices = [u32]{0, 1, 2, 3, 5, 6, 8, 9}; - const result = validate_skipped_key_gaps(&indices); - assert(result == null); + var indices: [8]u32 = [8]u32{0, 1, 2, 3, 5, 6, 8, 9}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.Ok); + assert(v.value == 0); } +// SMKG-07 -- empty accepted. test smkg_07_empty_accepted { - const indices = [u32]{}; - const result = validate_skipped_key_gaps(&indices); - assert(result == null); + var indices: [0]u32 = [0]u32{}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.Ok); } +// SMKG-08 -- single index accepted. test smkg_08_single_accepted { - const indices = [u32]{0}; - const result = validate_skipped_key_gaps(&indices); - assert(result == null); + var indices: [1]u32 = [1]u32{0}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.Ok); } +// SMKG-09 -- max gap accepted. test smkg_09_max_gap_accepted { - const indices = [u32]{0, SMKG_MAX_GAP}; - const result = validate_skipped_key_gaps(&indices); - assert(result == null); + var indices: [2]u32 = [2]u32{0, 32}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.Ok); + assert(SMKG_MAX_GAP == 32); } +// SMKG-10 -- max skipped accepted (exactly SMKG_MAX_SKIPPED indices). test smkg_10_max_skipped_accepted { - var indices: [SMKG_MAX_SKIPPED]u32 = undefined; - var i: usize = 0; - for (&indices) |*idx| { - idx.* = @intCast(i); - i += 1; + var indices: [256]u32 = undefined; + var n: u32 = 0; + for (i in 0..256) { + indices[i] = n; + n += 1; + } + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.Ok); + assert(SMKG_MAX_SKIPPED == 256); +} + +// The first port indexed a [256]bool by the key index. Indices up to +// SMKG_MAX_INDEX are legal; the last one is accepted, one past it is not. +test smkg_11_max_index_accepted_without_bitmap { + var indices: [2]u32 = [2]u32{999990, 1000000}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.Ok); + assert(v.value == 0); +} + +// Duplicate is checked before order: in [5, 6, 5] the last 5 is both a +// duplicate and not increasing; the original's BTreeSet insert reports the +// duplicate first. ([5, 3, 5] stops earlier, at 3, with NotIncreasing.) +test smkg_12_duplicate_checked_before_order { + var indices: [3]u32 = [3]u32{5, 6, 5}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.DuplicateIndex); + assert(v.value == 5); + var early: [3]u32 = [3]u32{5, 3, 5}; + const w = validate_skipped_key_gaps(&early); + assert(w.code == SkippedGapCode.NotIncreasing); +} + +// Too large is checked before order and gap: [4, 2000000] reports the +// index, not a gap of 1999996. +test smkg_13_too_large_checked_before_gap { + var indices: [2]u32 = [2]u32{4, 2000000}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.IndexTooLarge); + assert(v.value == 2000000); +} + +// The count is checked before any index: 257 indices, the first too large. +test smkg_14_count_checked_before_indices { + var indices: [257]u32 = undefined; + for (i in 0..257) { + indices[i] = 2000000; } - const result = validate_skipped_key_gaps(&indices); - assert(result == null); -} \ No newline at end of file + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.TooManySkipped); +} + +// Gap of 33 rejected with the gap as the value. +test smkg_15_gap_one_past_max { + var indices: [2]u32 = [2]u32{10, 43}; + const v = validate_skipped_key_gaps(&indices); + assert(v.code == SkippedGapCode.GapTooLarge); + assert(v.value == 33); +} + +test smkg_16_verdict_helper { + const v = smkg_verdict(SkippedGapCode.IndexBelowMin, 7); + assert(v.code == SkippedGapCode.IndexBelowMin); + assert(v.value == 7); +} + +test smkg_17_seen_before_helper { + var indices: [4]u32 = [4]u32{9, 8, 9, 7}; + assert(smkg_seen_before(&indices, 0) == false); + assert(smkg_seen_before(&indices, 1) == false); + assert(smkg_seen_before(&indices, 2) == true); + assert(smkg_seen_before(&indices, 3) == false); +} diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27 index 85acd0e881..83256f87d3 100644 --- a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27 +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27 @@ -1,108 +1,232 @@ -//! CR-CHAT-LAWS — Trinity Secure Chat constitutional laws (R-CHAT-1..12). -//! -//! [VERIFIED] These 12 laws are the immutable constitution of the chat stack. -//! Any change requires an approved ADR-CHAT-* commit. The hash is asserted by -//! laws_guard tests downstream. -//! -//! Sibling rings: CR-CHAT-00 (errors), CR-CHAT-01 (sealed/identity), -//! CR-CHAT-02 (ratchet), CR-CHAT-03 (group), CR-CHAT-04 (padding), -//! CR-CHAT-06 (capability + injection). -//! -//! [CITED] design §3.0 — Twelve Laws of Trinity Secure Chat. - -/// The 12 laws. Order is part of the contract. [CITED design §3.0] -pub const R_CHAT_LAWS: [12][]const u8 = [ - "R-CHAT-1 NO PLAINTEXT AT REST", - "R-CHAT-2 HYBRID PQ FROM DAY ONE", - "R-CHAT-3 SEALED SENDER MANDATORY", - "R-CHAT-4 DENIABLE AUTHENTICATION", - "R-CHAT-5 AGENT KEY != USER KEY", - "R-CHAT-6 TOOLS ARE SIGNED PROMPTS", - "R-CHAT-7 DUAL-LLM ISOLATION", - "R-CHAT-8 SESSION-SCOPED CAPABILITY", - "R-CHAT-9 FIXED-SIZE PADDING", - "R-CHAT-10 ZERO BACKGROUND CHATTER", - "R-CHAT-11 COQ-VERIFIED INVARIANTS", - "R-CHAT-12 R5+R7 (HONESTY + FALSIFIABILITY)", +module port::trios::crates::trios-chat::rings::CR-CHAT-LAWS::src::lib; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.rs +// @ 8b229e9489ee (1 constant table of 12 laws, 1 function laws_hash, +// 4 tests). +// +// CR-CHAT-LAWS -- Trinity Secure Chat constitutional laws (R-CHAT-1..12). +// The 12 laws are the constitution of the chat stack; any change requires an +// approved ADR-CHAT-* commit. Order is part of the contract. The original's +// laws_hash() is SHA-256 over the laws, each followed by one zero byte; the +// hash is pinned by downstream tests (d8c962d0...6f3a98). +// +// Repair of the first port (t27 PR 7193): +// - [12][]const u8 did not lower to Rust (Vec) or C. The table is +// now flat bytes: LAWS_PREIMAGE holds every law followed by its zero byte, +// which is exactly the byte string the original feeds to SHA-256, and +// LAWS_OFFSETS[i] is where law i starts. +// - The first port's laws_hash() returned the precomputed digest, so the +// tamper check compared a constant with itself. SHA-256 is not computed in +// .t27 (Trinity Secure Chat owner decision D8: the hash runs in the Rust +// adapter with sha2 over LAWS_PREIMAGE). This spec keeps only the decision: +// laws_hash_matches_reference() compares a digest computed by the adapter +// with the declared reference LAWS_HASH_REFERENCE. No function returns it. +// - Every test asserts at runtime; the prefix check includes the law number. +// - Full-path module line, so the seal file name is unique (without it the +// module was "lib" and its seal would overwrite the trios-store src_lib seal). +// +// Anchor: phi^2 + phi^-2 = 3 * TRINITY * CHAT * LAWS + +// Number of laws. +pub const LAWS_COUNT: usize = 12; + +// Bytes in LAWS_PREIMAGE: the 12 laws (373 bytes) plus 12 zero bytes. +pub const LAWS_PREIMAGE_LEN: usize = 404; + +// The laws in order, each followed by one zero byte (ASCII): +// 1 "R-CHAT-1 NO PLAINTEXT AT REST" +// 2 "R-CHAT-2 HYBRID PQ FROM DAY ONE" +// 3 "R-CHAT-3 SEALED SENDER MANDATORY" +// 4 "R-CHAT-4 DENIABLE AUTHENTICATION" +// 5 "R-CHAT-5 AGENT KEY != USER KEY" +// 6 "R-CHAT-6 TOOLS ARE SIGNED PROMPTS" +// 7 "R-CHAT-7 DUAL-LLM ISOLATION" +// 8 "R-CHAT-8 SESSION-SCOPED CAPABILITY" +// 9 "R-CHAT-9 FIXED-SIZE PADDING" +// 10 "R-CHAT-10 ZERO BACKGROUND CHATTER" +// 11 "R-CHAT-11 COQ-VERIFIED INVARIANTS" +// 12 "R-CHAT-12 R5+R7 (HONESTY + FALSIFIABILITY)" +pub const LAWS_PREIMAGE: [404]u8 = [ + 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x31, 0x20, 0x20, 0x4E, 0x4F, 0x20, 0x50, 0x4C, 0x41, + 0x49, 0x4E, 0x54, 0x45, 0x58, 0x54, 0x20, 0x41, 0x54, 0x20, 0x52, 0x45, 0x53, 0x54, 0x00, 0x52, + 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x32, 0x20, 0x20, 0x48, 0x59, 0x42, 0x52, 0x49, 0x44, 0x20, + 0x50, 0x51, 0x20, 0x46, 0x52, 0x4F, 0x4D, 0x20, 0x44, 0x41, 0x59, 0x20, 0x4F, 0x4E, 0x45, 0x00, + 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x33, 0x20, 0x20, 0x53, 0x45, 0x41, 0x4C, 0x45, 0x44, + 0x20, 0x53, 0x45, 0x4E, 0x44, 0x45, 0x52, 0x20, 0x4D, 0x41, 0x4E, 0x44, 0x41, 0x54, 0x4F, 0x52, + 0x59, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x34, 0x20, 0x20, 0x44, 0x45, 0x4E, 0x49, + 0x41, 0x42, 0x4C, 0x45, 0x20, 0x41, 0x55, 0x54, 0x48, 0x45, 0x4E, 0x54, 0x49, 0x43, 0x41, 0x54, + 0x49, 0x4F, 0x4E, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x35, 0x20, 0x20, 0x41, 0x47, + 0x45, 0x4E, 0x54, 0x20, 0x4B, 0x45, 0x59, 0x20, 0x21, 0x3D, 0x20, 0x55, 0x53, 0x45, 0x52, 0x20, + 0x4B, 0x45, 0x59, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x36, 0x20, 0x20, 0x54, 0x4F, + 0x4F, 0x4C, 0x53, 0x20, 0x41, 0x52, 0x45, 0x20, 0x53, 0x49, 0x47, 0x4E, 0x45, 0x44, 0x20, 0x50, + 0x52, 0x4F, 0x4D, 0x50, 0x54, 0x53, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x37, 0x20, + 0x20, 0x44, 0x55, 0x41, 0x4C, 0x2D, 0x4C, 0x4C, 0x4D, 0x20, 0x49, 0x53, 0x4F, 0x4C, 0x41, 0x54, + 0x49, 0x4F, 0x4E, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x38, 0x20, 0x20, 0x53, 0x45, + 0x53, 0x53, 0x49, 0x4F, 0x4E, 0x2D, 0x53, 0x43, 0x4F, 0x50, 0x45, 0x44, 0x20, 0x43, 0x41, 0x50, + 0x41, 0x42, 0x49, 0x4C, 0x49, 0x54, 0x59, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x39, + 0x20, 0x20, 0x46, 0x49, 0x58, 0x45, 0x44, 0x2D, 0x53, 0x49, 0x5A, 0x45, 0x20, 0x50, 0x41, 0x44, + 0x44, 0x49, 0x4E, 0x47, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x31, 0x30, 0x20, 0x5A, + 0x45, 0x52, 0x4F, 0x20, 0x42, 0x41, 0x43, 0x4B, 0x47, 0x52, 0x4F, 0x55, 0x4E, 0x44, 0x20, 0x43, + 0x48, 0x41, 0x54, 0x54, 0x45, 0x52, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, 0x31, 0x31, + 0x20, 0x43, 0x4F, 0x51, 0x2D, 0x56, 0x45, 0x52, 0x49, 0x46, 0x49, 0x45, 0x44, 0x20, 0x49, 0x4E, + 0x56, 0x41, 0x52, 0x49, 0x41, 0x4E, 0x54, 0x53, 0x00, 0x52, 0x2D, 0x43, 0x48, 0x41, 0x54, 0x2D, + 0x31, 0x32, 0x20, 0x52, 0x35, 0x2B, 0x52, 0x37, 0x20, 0x28, 0x48, 0x4F, 0x4E, 0x45, 0x53, 0x54, + 0x59, 0x20, 0x2B, 0x20, 0x46, 0x41, 0x4C, 0x53, 0x49, 0x46, 0x49, 0x41, 0x42, 0x49, 0x4C, 0x49, + 0x54, 0x59, 0x29, 0x00, ]; -/// Expected SHA-256 over the joined laws (each followed by a null byte). -/// [DERIVED] Pre-computed from R_CHAT_LAWS; reference value asserted in test. -pub const LAWS_HASH_EXPECTED: [32]u8 = [ - 0xd8, 0xc9, 0x62, 0xd0, 0xcf, 0xe1, 0x11, 0xbf, - 0x72, 0xf9, 0xd5, 0x9f, 0x22, 0x96, 0xba, 0xf0, - 0x15, 0xff, 0x5c, 0x9f, 0x03, 0x90, 0xcf, 0x80, - 0x7b, 0x7c, 0xc0, 0x8c, 0x70, 0x6f, 0x3a, 0x98, +// LAWS_OFFSETS[i] is the first byte of law i; LAWS_OFFSETS[12] is the end. +pub const LAWS_OFFSETS: [13]u32 = [ + 0, 31, 64, 98, 132, 164, 199, 228, 264, 293, 327, 361, 404, ]; -/// SHA-256 over the joined laws. Updated only via ADR-CHAT-*. -/// [DERIVED] Returns pre-computed hash; computation is deterministic. -pub fn laws_hash() -> [32]u8 { - return LAWS_HASH_EXPECTED; +// The reference SHA-256 of LAWS_PREIMAGE, as pinned downstream. It is data: +// the digest itself is computed by the adapter, never returned from here. +pub const LAWS_HASH_REFERENCE: [32]u8 = [ + 0xD8, 0xC9, 0x62, 0xD0, 0xCF, 0xE1, 0x11, 0xBF, + 0x72, 0xF9, 0xD5, 0x9F, 0x22, 0x96, 0xBA, 0xF0, + 0x15, 0xFF, 0x5C, 0x9F, 0x03, 0x90, 0xCF, 0x80, + 0x7B, 0x7C, 0xC0, 0x8C, 0x70, 0x6F, 0x3A, 0x98, +]; + +pub fn laws_count() -> usize { + return LAWS_COUNT; +} + +// First byte of law i in LAWS_PREIMAGE. +pub fn law_start(i: usize) -> u32 { + return LAWS_OFFSETS[i]; } -test twelve_laws_present { - assert(R_CHAT_LAWS.len == 12); +// Length of law i without its zero byte. +pub fn law_len(i: usize) -> u32 { + return LAWS_OFFSETS[i + 1] - LAWS_OFFSETS[i] - 1; } -test laws_hash_stable_within_run { - const a = laws_hash(); - const b = laws_hash(); - var i: usize = 0; - while (i < 32) { - assert(a[i] == b[i]); - i += 1; +// Byte j of law i. +pub fn law_byte(i: usize, j: usize) -> u8 { + return LAWS_PREIMAGE[@as(usize, LAWS_OFFSETS[i]) + j]; +} + +// True when law i starts with "R-CHAT-" followed by the decimal digits of n +// (1..99); the original checks starts_with(format!("R-CHAT-{}", i + 1)). +pub fn law_starts_with_number(i: usize, n: u32) -> bool { + const len: u32 = law_len(i); + if (len < 8) { + return false; + } + if (law_byte(i, 0) != 82 or law_byte(i, 1) != 45 or law_byte(i, 2) != 67 or law_byte(i, 3) != 72) { + return false; + } + if (law_byte(i, 4) != 65 or law_byte(i, 5) != 84 or law_byte(i, 6) != 45) { + return false; + } + if (n < 10) { + const d: u32 = 48 + n; + return @as(u32, law_byte(i, 7)) == d; } + if (len < 9) { + return false; + } + const d1: u32 = 48 + n / 10; + const d0: u32 = 48 + n % 10; + return @as(u32, law_byte(i, 7)) == d1 and @as(u32, law_byte(i, 8)) == d0; } -test laws_hash_matches_expected { - const h = laws_hash(); - var i: usize = 0; - while (i < 32) { - assert(h[i] == LAWS_HASH_EXPECTED[i]); - i += 1; +// True when laws a and b have the same bytes. +pub fn laws_equal(a: usize, b: usize) -> bool { + const la: u32 = law_len(a); + if (la != law_len(b)) { + return false; + } + for (j in 0..@as(usize, la)) { + if (law_byte(a, j) != law_byte(b, j)) { + return false; + } } + return true; } -test laws_have_canonical_prefix { - var i: usize = 0; - while (i < 12) { - const law = R_CHAT_LAWS[i]; - const expected_prefix = "R-CHAT-"; - // Check that law starts with "R-CHAT-N" where N is i+1 - assert(law[0] == 'R'); - assert(law[1] == '-'); - assert(law[2] == 'C'); - assert(law[3] == 'H'); - assert(law[4] == 'A'); - assert(law[5] == 'T'); - assert(law[6] == '-'); - // The number follows - for 1-9 it's one digit, for 10-12 it's two digits - i += 1; +// The tamper decision: does a digest computed over LAWS_PREIMAGE (by the +// adapter, with SHA-256) equal the pinned reference? +pub fn laws_hash_matches_reference(digest: [32]u8) -> bool { + var diff: u8 = 0; + for (k in 0..32) { + diff = diff | (digest[k] ^ LAWS_HASH_REFERENCE[k]); } + return diff == 0; } -test laws_are_unique { - var i: usize = 0; - while (i < 12) { - var j: usize = i + 1; - while (j < 12) { - const a = R_CHAT_LAWS[i]; - const b = R_CHAT_LAWS[j]; - var k: usize = 0; - var equal = true; - while (k < a.len and k < b.len) { - if (a[k] != b[k]) { - equal = false; - break; - } - k += 1; - } - if (equal and a.len == b.len) { - assert(false); // duplicate found - } - j += 1; +// FNV-1a (32 bit) over LAWS_PREIMAGE. A test checksum, not a security +// function: it lets a .t27 test check every byte of the table against a +// value computed independently from the original Rust strings. +pub fn laws_preimage_fnv1a32() -> u32 { + var h: u32 = 0x811C9DC5; + for (k in 0..LAWS_PREIMAGE_LEN) { + h = h ^ @as(u32, LAWS_PREIMAGE[k]); + h = h *% 0x01000193; + } + return h; +} + +// --------------------------------------------------------------------- +// Tests. Original: twelve_laws_present, laws_hash_stable_within_run, +// laws_have_canonical_prefix, laws_are_unique. laws_hash_stable_within_run +// tests the SHA-256 call, which stays in the Rust adapter (D8); its +// counterpart here pins the tamper decision. Expected values come from the +// original Rust strings (sha256 d8c962d0...6f3a98, fnv1a32 0xED08D70D). +// --------------------------------------------------------------------- + +test laws_01_twelve_laws_present { + assert(laws_count() == 12); + assert(LAWS_OFFSETS[0] == 0); + assert(@as(usize, LAWS_OFFSETS[12]) == LAWS_PREIMAGE_LEN); + for (i in 0..LAWS_COUNT) { + assert(law_len(i) > 0); + assert(LAWS_PREIMAGE[@as(usize, LAWS_OFFSETS[i + 1]) - 1] == 0); + } +} + +test laws_02_hash_decision_against_reference { + var good: [32]u8 = LAWS_HASH_REFERENCE; + assert(laws_hash_matches_reference(good) == true); + var flipped: [32]u8 = LAWS_HASH_REFERENCE; + flipped[31] = flipped[31] ^ 1; + assert(laws_hash_matches_reference(flipped) == false); + var zero: [32]u8 = [32]u8{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}; + assert(laws_hash_matches_reference(zero) == false); +} + +test laws_03_canonical_prefix_with_number { + var n: u32 = 1; + for (i in 0..LAWS_COUNT) { + assert(law_starts_with_number(i, n) == true); + n += 1; + } + assert(law_starts_with_number(0, 2) == false); + assert(law_starts_with_number(9, 11) == false); +} + +test laws_04_unique { + for (i in 0..LAWS_COUNT) { + assert(laws_equal(i, i) == true); + for (j in (i + 1)..LAWS_COUNT) { + assert(laws_equal(i, j) == false); } - i += 1; } -} \ No newline at end of file +} + +test laws_05_exact_bytes_of_the_table { + assert(laws_preimage_fnv1a32() == 0xED08D70D); + assert(law_len(0) == 30); + assert(law_len(4) == 31); + assert(law_len(11) == 42); + assert(law_byte(4, 20) == 33); + assert(law_byte(11, 41) == 41); +} + +test laws_06_law_start_helper { + assert(law_start(0) == 0); + assert(law_start(1) == 31); + assert(law_start(11) == 361); +}