From 63c239ff3a422bb9beac65a46857c6ed7aff7d5d Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Sun, 11 Oct 2026 12:03:19 -0300 Subject: [PATCH 1/3] Port trios-chat CR-CHAT-00: lib.rs data and decisions as lib.t27 (Refs #8880) Refs #8880 T-SPLIT port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-00/src/lib.rs at 8b229e9489ee: the eight error kinds in declaration order, SessionId, Counter, DestHash and EnvelopeMeta records, the counter successor with an Overflow verdict (the original panics), lowercase hex of a session id into [64]u8, and the 12-row R-CHAT law table as flat bytes plus offsets. The thiserror Error facade, Result, serde derives, tuple newtypes and the const fn chat_laws() stay Rust. test-report 16/16, vacuous 0; gen-rust compiles; coverage Untested 0; sealed with t27c built from this tree (t27c-bootstrap@0.5.2+5e5493cab), seal --verify all hashes MATCH. --- ...ios-chat::rings::CR-CHAT-00::src::lib.json | 28 + .../trios-chat/rings/CR-CHAT-00/src/lib.t27 | 551 ++++++++++++++++++ 2 files changed, 579 insertions(+) create mode 100644 .trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json create mode 100644 specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json new file mode 100644 index 0000000000..e3e6139612 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+5e5493cab", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:d06eeb331c8bac6b1d20401598d9a91927e2e544d9a2293a759d443639820ab4", + "gen_hash_rust": "sha256:75b33e546f69e193d4f27fb65e646b7627ac17b782372d006862ca0f4df65578", + "gen_hash_verilog": "sha256:e14888fd201f29a83fa2cdda469bf2b6a70ce12f637635d8083984b1fd535c66", + "gen_hash_zig": "sha256:b7b97b5826ea7351e33b0bdf98a5de9cfe37421de938a48585eca6f2f29ec6fa", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-11T15:02:51Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:ed8b435142e7bb149023b37bb75fad7e98301e3b180a96084e484445adb22afb", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 16, + "total": 16, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 new file mode 100644 index 0000000000..2da64576e4 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 @@ -0,0 +1,551 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib; + +// CR-CHAT-00: chat wire-format primitives. +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-00/src/lib.rs at +// 8b229e9489ee (T-SPLIT: the data and decision part of a mixed lib.rs). +// Tracker: gHashTag/t27 issue 8880. Epic: gHashTag/trios issue 1812. +// +// In this spec: the eight error kinds in declaration order, the id and +// counter records, the counter successor with an overflow verdict (the +// original panics), lowercase hex of a session id into [64]u8, and the +// 12-row R-CHAT law table as flat bytes plus offsets. +// +// Stays Rust (facade, not ported): the thiserror Error enum with its +// &'static str / String payloads and Display strings, the Result alias, +// serde derives and the serde_json round trip, tuple newtypes with .0, +// the panic message "counter overflow", and the const fn chat_laws() +// returning &'static [ChatLaw]. +// +// Not reconciled on purpose (changes only by ADR): the titles here differ +// from CR-CHAT-LAWS, and the original Error docs map Capability to R-CHAT-7 +// and Injection to R-CHAT-8, swapped versus the law table. + +pub const CHAT_U64_MAX: u64 = 0xFFFFFFFFFFFFFFFF; + +/// Bytes in a session id. +pub const SESSION_ID_LEN: usize = 32; + +/// Characters in the lowercase hex form of a session id. +pub const SESSION_ID_HEX_LEN: usize = 64; + +/// Bytes in a destination hash (routing hint). +pub const DEST_HASH_LEN: usize = 16; + +/// Rows in the R-CHAT law table. +pub const CHAT_LAW_COUNT: usize = 12; + +/// Fields per law row: id, title, summary. +pub const CHAT_LAW_FIELDS: usize = 3; +pub const CHAT_LAW_FIELD_ID: usize = 0; +pub const CHAT_LAW_FIELD_TITLE: usize = 1; +pub const CHAT_LAW_FIELD_SUMMARY: usize = 2; + +/// Total bytes of all law fields, concatenated without separators. +pub const CHAT_LAWS_TEXT_LEN: usize = 1088; + +/// The crate-wide error kinds, payload-free, in the declaration order of the +/// original Error enum. +pub enum ErrorKind { + Invariant, + Aead, + Crypto, + Capability, + Injection, + Persist, + Wire, + Encoding, +} + +/// Opaque 32-byte session identity (original: tuple struct SessionId). +pub struct SessionId { + bytes: [32]u8, +} + +/// Strictly monotone ratchet counter (original: tuple struct Counter). +pub struct Counter { + value: u64, +} + +/// 16-byte routing hint (original: tuple struct DestHash). +pub struct DestHash { + bytes: [16]u8, +} + +/// Non-secret header travelling alongside ciphertext. No sender identity. +pub struct EnvelopeMeta { + session: SessionId, + counter: Counter, + dest: DestHash, + padded_len: u32, +} + +/// Verdict of counter_next: Ok first, then Overflow (the original panics with +/// "counter overflow"; the adapter keeps that panic). +pub enum CounterCode { + Ok, + Overflow, +} + +/// On Ok, value is the successor. On Overflow, value is the input, unchanged. +pub struct CounterNext { + code: CounterCode, + value: u64, +} + +pub const CHAT_LAWS_TEXT: [1088]u8 = [ + // law 1 id: "R-CHAT-1" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x31, + // law 1 title: "NO PLAINTEXT AT REST" + 0x4e, 0x4f, 0x20, 0x50, 0x4c, 0x41, 0x49, 0x4e, 0x54, 0x45, 0x58, 0x54, + 0x20, 0x41, 0x54, 0x20, 0x52, 0x45, 0x53, 0x54, + // law 1 summary: "Persistence layers only ever see sealed envelopes." + 0x50, 0x65, 0x72, 0x73, 0x69, 0x73, 0x74, 0x65, 0x6e, 0x63, 0x65, 0x20, + 0x6c, 0x61, 0x79, 0x65, 0x72, 0x73, 0x20, 0x6f, 0x6e, 0x6c, 0x79, 0x20, + 0x65, 0x76, 0x65, 0x72, 0x20, 0x73, 0x65, 0x65, 0x20, 0x73, 0x65, 0x61, + 0x6c, 0x65, 0x64, 0x20, 0x65, 0x6e, 0x76, 0x65, 0x6c, 0x6f, 0x70, 0x65, + 0x73, 0x2e, + // law 2 id: "R-CHAT-2" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x32, + // law 2 title: "HYBRID PQ" + 0x48, 0x59, 0x42, 0x52, 0x49, 0x44, 0x20, 0x50, 0x51, + // law 2 summary: "Every key agreement combines X25519 with a PQ KEM (ML-KEM-768)." + 0x45, 0x76, 0x65, 0x72, 0x79, 0x20, 0x6b, 0x65, 0x79, 0x20, 0x61, 0x67, + 0x72, 0x65, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x20, 0x63, 0x6f, 0x6d, 0x62, + 0x69, 0x6e, 0x65, 0x73, 0x20, 0x58, 0x32, 0x35, 0x35, 0x31, 0x39, 0x20, + 0x77, 0x69, 0x74, 0x68, 0x20, 0x61, 0x20, 0x50, 0x51, 0x20, 0x4b, 0x45, + 0x4d, 0x20, 0x28, 0x4d, 0x4c, 0x2d, 0x4b, 0x45, 0x4d, 0x2d, 0x37, 0x36, + 0x38, 0x29, 0x2e, + // law 3 id: "R-CHAT-3" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x33, + // law 3 title: "SEALED SENDER" + 0x53, 0x45, 0x41, 0x4c, 0x45, 0x44, 0x20, 0x53, 0x45, 0x4e, 0x44, 0x45, + 0x52, + // law 3 summary: "Routing happens on dest_hash; sender identity is encrypted." + 0x52, 0x6f, 0x75, 0x74, 0x69, 0x6e, 0x67, 0x20, 0x68, 0x61, 0x70, 0x70, + 0x65, 0x6e, 0x73, 0x20, 0x6f, 0x6e, 0x20, 0x64, 0x65, 0x73, 0x74, 0x5f, + 0x68, 0x61, 0x73, 0x68, 0x3b, 0x20, 0x73, 0x65, 0x6e, 0x64, 0x65, 0x72, + 0x20, 0x69, 0x64, 0x65, 0x6e, 0x74, 0x69, 0x74, 0x79, 0x20, 0x69, 0x73, + 0x20, 0x65, 0x6e, 0x63, 0x72, 0x79, 0x70, 0x74, 0x65, 0x64, 0x2e, + // law 4 id: "R-CHAT-4" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x34, + // law 4 title: "DENIABLE AUTH" + 0x44, 0x45, 0x4e, 0x49, 0x41, 0x42, 0x4c, 0x45, 0x20, 0x41, 0x55, 0x54, + 0x48, + // law 4 summary: "Authentication uses MAC-then-encrypt, leaving no signature trail." + 0x41, 0x75, 0x74, 0x68, 0x65, 0x6e, 0x74, 0x69, 0x63, 0x61, 0x74, 0x69, + 0x6f, 0x6e, 0x20, 0x75, 0x73, 0x65, 0x73, 0x20, 0x4d, 0x41, 0x43, 0x2d, + 0x74, 0x68, 0x65, 0x6e, 0x2d, 0x65, 0x6e, 0x63, 0x72, 0x79, 0x70, 0x74, + 0x2c, 0x20, 0x6c, 0x65, 0x61, 0x76, 0x69, 0x6e, 0x67, 0x20, 0x6e, 0x6f, + 0x20, 0x73, 0x69, 0x67, 0x6e, 0x61, 0x74, 0x75, 0x72, 0x65, 0x20, 0x74, + 0x72, 0x61, 0x69, 0x6c, 0x2e, + // law 5 id: "R-CHAT-5" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x35, + // law 5 title: "AGENT KEY != USER KEY" + 0x41, 0x47, 0x45, 0x4e, 0x54, 0x20, 0x4b, 0x45, 0x59, 0x20, 0x21, 0x3d, + 0x20, 0x55, 0x53, 0x45, 0x52, 0x20, 0x4b, 0x45, 0x59, + // law 5 summary: "Bot identities live on a disjoint keyring from human users." + 0x42, 0x6f, 0x74, 0x20, 0x69, 0x64, 0x65, 0x6e, 0x74, 0x69, 0x74, 0x69, + 0x65, 0x73, 0x20, 0x6c, 0x69, 0x76, 0x65, 0x20, 0x6f, 0x6e, 0x20, 0x61, + 0x20, 0x64, 0x69, 0x73, 0x6a, 0x6f, 0x69, 0x6e, 0x74, 0x20, 0x6b, 0x65, + 0x79, 0x72, 0x69, 0x6e, 0x67, 0x20, 0x66, 0x72, 0x6f, 0x6d, 0x20, 0x68, + 0x75, 0x6d, 0x61, 0x6e, 0x20, 0x75, 0x73, 0x65, 0x72, 0x73, 0x2e, + // law 6 id: "R-CHAT-6" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x36, + // law 6 title: "TOOLS ARE SIGNED PROMPTS" + 0x54, 0x4f, 0x4f, 0x4c, 0x53, 0x20, 0x41, 0x52, 0x45, 0x20, 0x53, 0x49, + 0x47, 0x4e, 0x45, 0x44, 0x20, 0x50, 0x52, 0x4f, 0x4d, 0x50, 0x54, 0x53, + // law 6 summary: "An agent only invokes a tool whose payload was signed by the publisher." + 0x41, 0x6e, 0x20, 0x61, 0x67, 0x65, 0x6e, 0x74, 0x20, 0x6f, 0x6e, 0x6c, + 0x79, 0x20, 0x69, 0x6e, 0x76, 0x6f, 0x6b, 0x65, 0x73, 0x20, 0x61, 0x20, + 0x74, 0x6f, 0x6f, 0x6c, 0x20, 0x77, 0x68, 0x6f, 0x73, 0x65, 0x20, 0x70, + 0x61, 0x79, 0x6c, 0x6f, 0x61, 0x64, 0x20, 0x77, 0x61, 0x73, 0x20, 0x73, + 0x69, 0x67, 0x6e, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, 0x68, 0x65, + 0x20, 0x70, 0x75, 0x62, 0x6c, 0x69, 0x73, 0x68, 0x65, 0x72, 0x2e, + // law 7 id: "R-CHAT-7" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x37, + // law 7 title: "DUAL-LLM ISOLATION" + 0x44, 0x55, 0x41, 0x4c, 0x2d, 0x4c, 0x4c, 0x4d, 0x20, 0x49, 0x53, 0x4f, + 0x4c, 0x41, 0x54, 0x49, 0x4f, 0x4e, + // law 7 summary: "Untrusted text crosses a sandbox before reaching the action LLM." + 0x55, 0x6e, 0x74, 0x72, 0x75, 0x73, 0x74, 0x65, 0x64, 0x20, 0x74, 0x65, + 0x78, 0x74, 0x20, 0x63, 0x72, 0x6f, 0x73, 0x73, 0x65, 0x73, 0x20, 0x61, + 0x20, 0x73, 0x61, 0x6e, 0x64, 0x62, 0x6f, 0x78, 0x20, 0x62, 0x65, 0x66, + 0x6f, 0x72, 0x65, 0x20, 0x72, 0x65, 0x61, 0x63, 0x68, 0x69, 0x6e, 0x67, + 0x20, 0x74, 0x68, 0x65, 0x20, 0x61, 0x63, 0x74, 0x69, 0x6f, 0x6e, 0x20, + 0x4c, 0x4c, 0x4d, 0x2e, + // law 8 id: "R-CHAT-8" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x38, + // law 8 title: "SESSION-SCOPED CAPABILITY" + 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, + // law 8 summary: "Every action token is bound to one session and one verb." + 0x45, 0x76, 0x65, 0x72, 0x79, 0x20, 0x61, 0x63, 0x74, 0x69, 0x6f, 0x6e, + 0x20, 0x74, 0x6f, 0x6b, 0x65, 0x6e, 0x20, 0x69, 0x73, 0x20, 0x62, 0x6f, + 0x75, 0x6e, 0x64, 0x20, 0x74, 0x6f, 0x20, 0x6f, 0x6e, 0x65, 0x20, 0x73, + 0x65, 0x73, 0x73, 0x69, 0x6f, 0x6e, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x6f, + 0x6e, 0x65, 0x20, 0x76, 0x65, 0x72, 0x62, 0x2e, + // law 9 id: "R-CHAT-9" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x39, + // law 9 title: "FIXED-SIZE PADDING" + 0x46, 0x49, 0x58, 0x45, 0x44, 0x2d, 0x53, 0x49, 0x5a, 0x45, 0x20, 0x50, + 0x41, 0x44, 0x44, 0x49, 0x4e, 0x47, + // law 9 summary: "Every envelope is padded to one of a small set of length classes." + 0x45, 0x76, 0x65, 0x72, 0x79, 0x20, 0x65, 0x6e, 0x76, 0x65, 0x6c, 0x6f, + 0x70, 0x65, 0x20, 0x69, 0x73, 0x20, 0x70, 0x61, 0x64, 0x64, 0x65, 0x64, + 0x20, 0x74, 0x6f, 0x20, 0x6f, 0x6e, 0x65, 0x20, 0x6f, 0x66, 0x20, 0x61, + 0x20, 0x73, 0x6d, 0x61, 0x6c, 0x6c, 0x20, 0x73, 0x65, 0x74, 0x20, 0x6f, + 0x66, 0x20, 0x6c, 0x65, 0x6e, 0x67, 0x74, 0x68, 0x20, 0x63, 0x6c, 0x61, + 0x73, 0x73, 0x65, 0x73, 0x2e, + // law 10 id: "R-CHAT-10" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x31, 0x30, + // law 10 title: "ZERO BACKGROUND CHATTER" + 0x5a, 0x45, 0x52, 0x4f, 0x20, 0x42, 0x41, 0x43, 0x4b, 0x47, 0x52, 0x4f, + 0x55, 0x4e, 0x44, 0x20, 0x43, 0x48, 0x41, 0x54, 0x54, 0x45, 0x52, + // law 10 summary: "No background pings, presence, or read-receipts; the wire is silent." + 0x4e, 0x6f, 0x20, 0x62, 0x61, 0x63, 0x6b, 0x67, 0x72, 0x6f, 0x75, 0x6e, + 0x64, 0x20, 0x70, 0x69, 0x6e, 0x67, 0x73, 0x2c, 0x20, 0x70, 0x72, 0x65, + 0x73, 0x65, 0x6e, 0x63, 0x65, 0x2c, 0x20, 0x6f, 0x72, 0x20, 0x72, 0x65, + 0x61, 0x64, 0x2d, 0x72, 0x65, 0x63, 0x65, 0x69, 0x70, 0x74, 0x73, 0x3b, + 0x20, 0x74, 0x68, 0x65, 0x20, 0x77, 0x69, 0x72, 0x65, 0x20, 0x69, 0x73, + 0x20, 0x73, 0x69, 0x6c, 0x65, 0x6e, 0x74, 0x2e, + // law 11 id: "R-CHAT-11" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x31, 0x31, + // law 11 title: "COQ-VERIFIED INVARIANTS" + 0x43, 0x4f, 0x51, 0x2d, 0x56, 0x45, 0x52, 0x49, 0x46, 0x49, 0x45, 0x44, + 0x20, 0x49, 0x4e, 0x56, 0x41, 0x52, 0x49, 0x41, 0x4e, 0x54, 0x53, + // law 11 summary: "Every wire invariant has a Coq theorem (Defined or budgeted Admitted)." + 0x45, 0x76, 0x65, 0x72, 0x79, 0x20, 0x77, 0x69, 0x72, 0x65, 0x20, 0x69, + 0x6e, 0x76, 0x61, 0x72, 0x69, 0x61, 0x6e, 0x74, 0x20, 0x68, 0x61, 0x73, + 0x20, 0x61, 0x20, 0x43, 0x6f, 0x71, 0x20, 0x74, 0x68, 0x65, 0x6f, 0x72, + 0x65, 0x6d, 0x20, 0x28, 0x44, 0x65, 0x66, 0x69, 0x6e, 0x65, 0x64, 0x20, + 0x6f, 0x72, 0x20, 0x62, 0x75, 0x64, 0x67, 0x65, 0x74, 0x65, 0x64, 0x20, + 0x41, 0x64, 0x6d, 0x69, 0x74, 0x74, 0x65, 0x64, 0x29, 0x2e, + // law 12 id: "R-CHAT-12" + 0x52, 0x2d, 0x43, 0x48, 0x41, 0x54, 0x2d, 0x31, 0x32, + // law 12 title: "R5+R7 (HONESTY MODE)" + 0x52, 0x35, 0x2b, 0x52, 0x37, 0x20, 0x28, 0x48, 0x4f, 0x4e, 0x45, 0x53, + 0x54, 0x59, 0x20, 0x4d, 0x4f, 0x44, 0x45, 0x29, + // law 12 summary: "Every claim is tagged [VERIFIED] / [CITED] / [DERIVED] / [ASPIRATIONAL]." + 0x45, 0x76, 0x65, 0x72, 0x79, 0x20, 0x63, 0x6c, 0x61, 0x69, 0x6d, 0x20, + 0x69, 0x73, 0x20, 0x74, 0x61, 0x67, 0x67, 0x65, 0x64, 0x20, 0x5b, 0x56, + 0x45, 0x52, 0x49, 0x46, 0x49, 0x45, 0x44, 0x5d, 0x20, 0x2f, 0x20, 0x5b, + 0x43, 0x49, 0x54, 0x45, 0x44, 0x5d, 0x20, 0x2f, 0x20, 0x5b, 0x44, 0x45, + 0x52, 0x49, 0x56, 0x45, 0x44, 0x5d, 0x20, 0x2f, 0x20, 0x5b, 0x41, 0x53, + 0x50, 0x49, 0x52, 0x41, 0x54, 0x49, 0x4f, 0x4e, 0x41, 0x4c, 0x5d, 0x2e, +]; + +/// Start of field f of law i is CHAT_LAWS_OFFSETS[3 * i + f]; the last entry is the +/// total length. Fields: 0 id, 1 title, 2 summary. +pub const CHAT_LAWS_OFFSETS: [37]u32 = [ + 0, 8, 28, + 78, 86, 95, + 158, 166, 179, + 238, 246, 259, + 324, 332, 353, + 412, 420, 444, + 515, 523, 541, + 605, 613, 638, + 694, 702, 720, + 785, 794, 817, + 885, 894, 917, + 987, 996, 1016, + 1088, +]; + +/// Declaration index of an error kind (0 = Invariant .. 7 = Encoding). +pub fn error_kind_code(k: ErrorKind) -> u8 { + if (k == ErrorKind.Invariant) { + return 0; + } + if (k == ErrorKind.Aead) { + return 1; + } + if (k == ErrorKind.Crypto) { + return 2; + } + if (k == ErrorKind.Capability) { + return 3; + } + if (k == ErrorKind.Injection) { + return 4; + } + if (k == ErrorKind.Persist) { + return 5; + } + if (k == ErrorKind.Wire) { + return 6; + } + return 7; +} + +/// SessionId::new. +pub fn session_id_new(bytes: [32]u8) -> SessionId { + return SessionId { bytes: bytes, }; +} + +/// SessionId::as_bytes. +pub fn session_id_as_bytes(s: SessionId) -> [32]u8 { + return s.bytes; +} + +/// One lowercase hex digit for a nibble 0..15 ('0'..'9', 'a'..'f'). +pub fn hex_digit(n: u8) -> u8 { + if (n < 10) { + return 48 + n; + } + return 87 + n; +} + +/// SessionId::to_hex: lowercase, two characters per byte, 64 in total. +pub fn session_id_to_hex(s: SessionId) -> [64]u8 { + var out: [64]u8 = [64]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, + 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, + }; + for (i in 0..SESSION_ID_LEN) { + const b: u8 = s.bytes[i]; + out[2 * i] = hex_digit(b >> 4); + out[2 * i + 1] = hex_digit(b & 15); + } + return out; +} + +/// Counter::ZERO, the start-of-session value. +pub fn counter_zero() -> Counter { + return Counter { value: 0, }; +} + +/// Counter::next: the successor, or Overflow at u64::MAX. +pub fn counter_next(c: Counter) -> CounterNext { + if (c.value == CHAT_U64_MAX) { + return CounterNext { code: CounterCode.Overflow, value: c.value, }; + } + return CounterNext { code: CounterCode.Ok, value: c.value + 1, }; +} + +/// Counter::get. +pub fn counter_get(c: Counter) -> u64 { + return c.value; +} + +/// DestHash::new. +pub fn dest_hash_new(bytes: [16]u8) -> DestHash { + return DestHash { bytes: bytes, }; +} + +/// Number of law rows (chat_laws().len()). +pub fn chat_law_count() -> usize { + return CHAT_LAW_COUNT; +} + +/// Offset of field f of law i in CHAT_LAWS_TEXT (i in 0..12, f in 0..3). +pub fn chat_law_field_start(law: usize, field: usize) -> u32 { + return CHAT_LAWS_OFFSETS[law * CHAT_LAW_FIELDS + field]; +} + +/// Length in bytes of field f of law i. +pub fn chat_law_field_len(law: usize, field: usize) -> u32 { + const k: usize = law * CHAT_LAW_FIELDS + field; + return CHAT_LAWS_OFFSETS[k + 1] - CHAT_LAWS_OFFSETS[k]; +} + +/// Byte j of field f of law i. +pub fn chat_law_byte(law: usize, field: usize, j: usize) -> u8 { + return CHAT_LAWS_TEXT[@as(usize, chat_law_field_start(law, field)) + j]; +} + +/// True when the id of law i is exactly "R-CHAT-" followed by the decimal +/// form of n (1..99). The original test law_ids_are_canonical_and_unique +/// asks this with n = i + 1 for every row. +pub fn chat_law_id_matches(law: usize, n: usize) -> bool { + var want: [9]u8 = [9]u8{82, 45, 67, 72, 65, 84, 45, 0, 0}; + var want_len: usize = 8; + if (n < 10) { + const d: u8 = @truncate(n); + want[7] = 48 + d; + } else { + const t: u8 = @truncate(n / 10); + const u: u8 = @truncate(n % 10); + want[7] = 48 + t; + want[8] = 48 + u; + want_len = 9; + } + if (@as(usize, chat_law_field_len(law, CHAT_LAW_FIELD_ID)) != want_len) { + return false; + } + for (j in 0..want_len) { + if (chat_law_byte(law, CHAT_LAW_FIELD_ID, j) != want[j]) { + return false; + } + } + return true; +} + +/// True when field f of law a and field f of law b hold the same bytes. +pub fn chat_law_fields_equal(a: usize, b: usize, field: usize) -> bool { + const la: u32 = chat_law_field_len(a, field); + if (la != chat_law_field_len(b, field)) { + return false; + } + for (j in 0..@as(usize, la)) { + if (chat_law_byte(a, field, j) != chat_law_byte(b, field, j)) { + return false; + } + } + return true; +} + +// --------------------------------------------------------------------- +// Tests. Original tests transcribed: session_id_hex_roundtrip, +// counter_zero_and_next, counter_overflow_panics (decision only), +// dest_hash_size_is_16, law_table_has_exactly_twelve_rows, +// law_ids_are_canonical_and_unique. Rust oracles: envelope_meta_serde_roundtrip +// (serde), error_invariant_renders and error_aead_renders (Display). +// --------------------------------------------------------------------- + +test cr00_01_session_id_hex_roundtrip { + var b: [32]u8 = [32]u8{0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB, 0xAB}; + const s = session_id_new(b); + const h = session_id_to_hex(s); + assert(h.len == 64); + for (i in 0..SESSION_ID_HEX_LEN) { + const c: u8 = h[i]; + assert((c >= 48 and c <= 57) or (c >= 97 and c <= 102)); + } + assert(h[0] == 97); + assert(h[1] == 98); +} + +test cr00_02_counter_zero_and_next { + assert(counter_get(counter_zero()) == 0); + const n0 = counter_next(counter_zero()); + assert(n0.code == CounterCode.Ok); + assert(n0.value == 1); + const n7 = counter_next(Counter { value: 7, }); + assert(n7.code == CounterCode.Ok); + assert(n7.value == 8); +} + +test cr00_03_counter_overflow_verdict { + const n = counter_next(Counter { value: CHAT_U64_MAX, }); + assert(n.code == CounterCode.Overflow); + assert(n.value == CHAT_U64_MAX); +} + +test cr00_04_counter_next_below_max { + const n = counter_next(Counter { value: 0xFFFFFFFFFFFFFFFE, }); + assert(n.code == CounterCode.Ok); + assert(n.value == CHAT_U64_MAX); +} + +test cr00_05_dest_hash_size_is_16 { + var b: [16]u8 = [16]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; + b[15] = 9; + const d = dest_hash_new(b); + assert(d.bytes.len == DEST_HASH_LEN); + assert(d.bytes[0] == 0); + assert(d.bytes[15] == 9); +} + +test cr00_06_session_id_as_bytes { + var b: [32]u8 = [32]u8{0, 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}; + const s = session_id_new(b); + const back = session_id_as_bytes(s); + for (i in 0..SESSION_ID_LEN) { + assert(back[i] == b[i]); + } +} + +test cr00_07_session_id_hex_sequence { + var b: [32]u8 = [32]u8{0, 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}; + b[31] = 0xF0; + const h = session_id_to_hex(session_id_new(b)); + assert(h[0] == 48); + assert(h[1] == 48); + assert(h[20] == 48); + assert(h[21] == 97); + assert(h[62] == 102); + assert(h[63] == 48); +} + +test cr00_08_hex_digit { + assert(hex_digit(0) == 48); + assert(hex_digit(9) == 57); + assert(hex_digit(10) == 97); + assert(hex_digit(15) == 102); +} + +test cr00_09_envelope_meta_fields { + var sb: [32]u8 = [32]u8{1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1}; + var db: [16]u8 = [16]u8{2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2}; + const m = EnvelopeMeta { session: session_id_new(sb), counter: Counter { value: 42, }, dest: dest_hash_new(db), padded_len: 1024, }; + assert(m.session.bytes[0] == 1); + assert(m.counter.value == 42); + assert(m.dest.bytes[15] == 2); + assert(m.padded_len == 1024); +} + +test cr00_10_error_kinds_in_declaration_order { + assert(error_kind_code(ErrorKind.Invariant) == 0); + assert(error_kind_code(ErrorKind.Aead) == 1); + assert(error_kind_code(ErrorKind.Crypto) == 2); + assert(error_kind_code(ErrorKind.Capability) == 3); + assert(error_kind_code(ErrorKind.Injection) == 4); + assert(error_kind_code(ErrorKind.Persist) == 5); + assert(error_kind_code(ErrorKind.Wire) == 6); + assert(error_kind_code(ErrorKind.Encoding) == 7); +} + +test cr00_11_law_table_has_exactly_twelve_rows { + assert(chat_law_count() == 12); + assert(CHAT_LAWS_OFFSETS.len == CHAT_LAW_COUNT * CHAT_LAW_FIELDS + 1); + assert(@as(usize, CHAT_LAWS_OFFSETS[36]) == CHAT_LAWS_TEXT_LEN); + assert(CHAT_LAWS_TEXT.len == CHAT_LAWS_TEXT_LEN); +} + +test cr00_12_law_ids_are_canonical_and_unique { + for (i in 0..CHAT_LAW_COUNT) { + assert(chat_law_id_matches(i, i + 1)); + } + for (i in 0..CHAT_LAW_COUNT) { + for (j in 0..i) { + assert(!chat_law_fields_equal(i, j, CHAT_LAW_FIELD_ID)); + } + } +} + +test cr00_13_law_field_start_and_len { + assert(chat_law_field_start(0, CHAT_LAW_FIELD_ID) == 0); + assert(chat_law_field_len(0, CHAT_LAW_FIELD_ID) == 8); + assert(chat_law_field_start(0, CHAT_LAW_FIELD_TITLE) == 8); + assert(chat_law_field_len(0, CHAT_LAW_FIELD_TITLE) == 20); + assert(chat_law_field_len(9, CHAT_LAW_FIELD_ID) == 9); + assert(chat_law_field_len(11, CHAT_LAW_FIELD_SUMMARY) == 72); +} + +test cr00_14_law_byte_reads_title_and_summary { + // law 5 title "AGENT KEY != USER KEY": 'A' first, '!' at index 10 + assert(chat_law_byte(4, CHAT_LAW_FIELD_TITLE, 0) == 65); + assert(chat_law_byte(4, CHAT_LAW_FIELD_TITLE, 10) == 33); + // law 1 summary ends with '.' + const n: u32 = chat_law_field_len(0, CHAT_LAW_FIELD_SUMMARY); + assert(chat_law_byte(0, CHAT_LAW_FIELD_SUMMARY, @as(usize, n) - 1) == 46); +} + +test cr00_15_law_id_matches_only_its_own_number { + assert(chat_law_id_matches(0, 1)); + assert(chat_law_id_matches(11, 12)); + assert(!chat_law_id_matches(0, 2)); + assert(!chat_law_id_matches(0, 10)); + assert(!chat_law_id_matches(9, 1)); + assert(!chat_law_id_matches(11, 11)); +} + +test cr00_16_law_fields_equal { + assert(chat_law_fields_equal(3, 3, CHAT_LAW_FIELD_SUMMARY)); + assert(!chat_law_fields_equal(0, 1, CHAT_LAW_FIELD_TITLE)); + assert(!chat_law_fields_equal(0, 9, CHAT_LAW_FIELD_ID)); +} From 198865e783faa71a707b3c7c7a1effac4dc94af2 Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Sun, 11 Oct 2026 12:08:53 -0300 Subject: [PATCH 2/3] Port trios-chat CR-CHAT-00: name the counter record ChatCounter (Refs #8880) Refs #8880 The types ratchet (Corpus ratchet, 'A type name may not gain a second definition') reported Counter as a NEW conflict: specs/port/trinity/fpga/ openxc7-synth/d_e21_test.t27 already defines a type Counter. The record is renamed ChatCounter; the swap adapter maps it to the original tuple struct Counter. Resealed with t27c-bootstrap@0.5.2+5e5493cab: tests 16/16, vacuous 0, all hashes MATCH. --- ...ios-chat::rings::CR-CHAT-00::src::lib.json | 14 +++++------ .../trios-chat/rings/CR-CHAT-00/src/lib.t27 | 25 +++++++++++-------- 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json index e3e6139612..87be1f9879 100644 --- a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json @@ -1,17 +1,17 @@ { - "built_by": "t27c-bootstrap@0.5.2+5e5493cab", + "built_by": "t27c-bootstrap@0.5.2+4b6ee3b82", "closure": [], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:d06eeb331c8bac6b1d20401598d9a91927e2e544d9a2293a759d443639820ab4", - "gen_hash_rust": "sha256:75b33e546f69e193d4f27fb65e646b7627ac17b782372d006862ca0f4df65578", - "gen_hash_verilog": "sha256:e14888fd201f29a83fa2cdda469bf2b6a70ce12f637635d8083984b1fd535c66", - "gen_hash_zig": "sha256:b7b97b5826ea7351e33b0bdf98a5de9cfe37421de938a48585eca6f2f29ec6fa", + "gen_hash_c": "sha256:26658302f4ba1a6ec18dbd8a801eec563aa54080c706d2c586700061b2e603e8", + "gen_hash_rust": "sha256:7877fd8a6f08da50b4213188e94d5707ca4149ec2011400e67742330ae24b511", + "gen_hash_verilog": "sha256:d66125020f21cc5f9a531a82f80918f6407cf70597a6ae46725b1816d92ee0df", + "gen_hash_zig": "sha256:2e6e7a731364ee1b287f7f7bdfad00447b886ca402715dfb457876cd7af1085e", "module": "port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-11T15:02:51Z", + "sealed_at": "2026-10-11T15:08:48Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:ed8b435142e7bb149023b37bb75fad7e98301e3b180a96084e484445adb22afb", + "spec_hash": "sha256:5681b7a34672463f2db1ed54f2f92ed06dc31aa94bbc2b294d6f9d24a627cec1", "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27", "tests": { "failed": 0, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 index 2da64576e4..1154a528f6 100644 --- a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 @@ -61,8 +61,11 @@ pub struct SessionId { bytes: [32]u8, } -/// Strictly monotone ratchet counter (original: tuple struct Counter). -pub struct Counter { +/// Strictly monotone ratchet counter (original: tuple struct Counter). Named +/// ChatCounter because the type name Counter is already defined by another +/// spec (specs/port/trinity/fpga/openxc7-synth/d_e21_test.t27) and the types +/// ratchet refuses a second definition. +pub struct ChatCounter { value: u64, } @@ -74,7 +77,7 @@ pub struct DestHash { /// Non-secret header travelling alongside ciphertext. No sender identity. pub struct EnvelopeMeta { session: SessionId, - counter: Counter, + counter: ChatCounter, dest: DestHash, padded_len: u32, } @@ -314,12 +317,12 @@ pub fn session_id_to_hex(s: SessionId) -> [64]u8 { } /// Counter::ZERO, the start-of-session value. -pub fn counter_zero() -> Counter { - return Counter { value: 0, }; +pub fn counter_zero() -> ChatCounter { + return ChatCounter { value: 0, }; } /// Counter::next: the successor, or Overflow at u64::MAX. -pub fn counter_next(c: Counter) -> CounterNext { +pub fn counter_next(c: ChatCounter) -> CounterNext { if (c.value == CHAT_U64_MAX) { return CounterNext { code: CounterCode.Overflow, value: c.value, }; } @@ -327,7 +330,7 @@ pub fn counter_next(c: Counter) -> CounterNext { } /// Counter::get. -pub fn counter_get(c: Counter) -> u64 { +pub fn counter_get(c: ChatCounter) -> u64 { return c.value; } @@ -424,19 +427,19 @@ test cr00_02_counter_zero_and_next { const n0 = counter_next(counter_zero()); assert(n0.code == CounterCode.Ok); assert(n0.value == 1); - const n7 = counter_next(Counter { value: 7, }); + const n7 = counter_next(ChatCounter { value: 7, }); assert(n7.code == CounterCode.Ok); assert(n7.value == 8); } test cr00_03_counter_overflow_verdict { - const n = counter_next(Counter { value: CHAT_U64_MAX, }); + const n = counter_next(ChatCounter { value: CHAT_U64_MAX, }); assert(n.code == CounterCode.Overflow); assert(n.value == CHAT_U64_MAX); } test cr00_04_counter_next_below_max { - const n = counter_next(Counter { value: 0xFFFFFFFFFFFFFFFE, }); + const n = counter_next(ChatCounter { value: 0xFFFFFFFFFFFFFFFE, }); assert(n.code == CounterCode.Ok); assert(n.value == CHAT_U64_MAX); } @@ -481,7 +484,7 @@ test cr00_08_hex_digit { test cr00_09_envelope_meta_fields { var sb: [32]u8 = [32]u8{1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1}; var db: [16]u8 = [16]u8{2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2}; - const m = EnvelopeMeta { session: session_id_new(sb), counter: Counter { value: 42, }, dest: dest_hash_new(db), padded_len: 1024, }; + const m = EnvelopeMeta { session: session_id_new(sb), counter: ChatCounter { value: 42, }, dest: dest_hash_new(db), padded_len: 1024, }; assert(m.session.bytes[0] == 1); assert(m.counter.value == 42); assert(m.dest.bytes[15] == 2); From b48e46bd54cae92eb1a1229bd376622309003c74 Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Sun, 11 Oct 2026 12:20:35 -0300 Subject: [PATCH 3/3] Port trios-chat CR-CHAT-00: id check without @truncate, t27b ledger row (Refs #8880) Refs #8880 t27b-native-ratchet listed the spec as UNLISTED, blocked on ExprCall(@truncate) in chat_law_id_matches. The check now compares the id digits as usize (@as widening only) and rejects n outside 1..99; two more asserts cover that. Local t27b (built from this tree): 16 passed, 0 failed, so the ledger gets the row t27b=pass, in path order. Resealed: tests 16/16, vacuous 0, all hashes MATCH. --- ...ios-chat::rings::CR-CHAT-00::src::lib.json | 12 +++---- docs/reports/t27b_expectations.json | 1 + .../trios-chat/rings/CR-CHAT-00/src/lib.t27 | 34 +++++++++---------- 3 files changed, 24 insertions(+), 23 deletions(-) diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json index 87be1f9879..9e424ad6d5 100644 --- a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib.json @@ -2,16 +2,16 @@ "built_by": "t27c-bootstrap@0.5.2+4b6ee3b82", "closure": [], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:26658302f4ba1a6ec18dbd8a801eec563aa54080c706d2c586700061b2e603e8", - "gen_hash_rust": "sha256:7877fd8a6f08da50b4213188e94d5707ca4149ec2011400e67742330ae24b511", - "gen_hash_verilog": "sha256:d66125020f21cc5f9a531a82f80918f6407cf70597a6ae46725b1816d92ee0df", - "gen_hash_zig": "sha256:2e6e7a731364ee1b287f7f7bdfad00447b886ca402715dfb457876cd7af1085e", + "gen_hash_c": "sha256:a266e9edbebf0c76f15f934778eaea0e9e2ca97a0695b434674d5b3be2e757a7", + "gen_hash_rust": "sha256:a354e0c9b62120c44927f4d3670a8601ac1eec6ec4091075d25871fe1e346df7", + "gen_hash_verilog": "sha256:0cb2f57afd6f91fd4c1fa41cfe8060c8cbcb4f09b8141f68486f75fa22be08fe", + "gen_hash_zig": "sha256:d703b57a784806b3f5dad4bbb33ba0934d12107486e5ec8d8a58a1572b21f7ea", "module": "port::trios::crates::trios-chat::rings::CR-CHAT-00::src::lib", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-11T15:08:48Z", + "sealed_at": "2026-10-11T15:20:35Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:5681b7a34672463f2db1ed54f2f92ed06dc31aa94bbc2b294d6f9d24a627cec1", + "spec_hash": "sha256:0d316f003d9a47f8b46f42bf32e4412bffc8325a5644a0583ab19a03b9113761", "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27", "tests": { "failed": 0, diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 74855af865..2328be8da6 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -849,6 +849,7 @@ {"path": "specs/port/trios/crates/tri-tunnel/src/main.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trinity_loss/src/lib.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-bridge/src/main.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.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-03/src/ratchet_tree_resolution_guard.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 index 1154a528f6..9c978fef12 100644 --- a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 @@ -361,30 +361,28 @@ pub fn chat_law_byte(law: usize, field: usize, j: usize) -> u8 { } /// True when the id of law i is exactly "R-CHAT-" followed by the decimal -/// form of n (1..99). The original test law_ids_are_canonical_and_unique +/// form of n (1..99; anything else is false). The original test law_ids_are_canonical_and_unique /// asks this with n = i + 1 for every row. pub fn chat_law_id_matches(law: usize, n: usize) -> bool { - var want: [9]u8 = [9]u8{82, 45, 67, 72, 65, 84, 45, 0, 0}; - var want_len: usize = 8; - if (n < 10) { - const d: u8 = @truncate(n); - want[7] = 48 + d; - } else { - const t: u8 = @truncate(n / 10); - const u: u8 = @truncate(n % 10); - want[7] = 48 + t; - want[8] = 48 + u; - want_len = 9; - } - if (@as(usize, chat_law_field_len(law, CHAT_LAW_FIELD_ID)) != want_len) { + const len: usize = @as(usize, chat_law_field_len(law, CHAT_LAW_FIELD_ID)); + if (n == 0 or n > 99 or len < 8) { return false; } - for (j in 0..want_len) { - if (chat_law_byte(law, CHAT_LAW_FIELD_ID, j) != want[j]) { + var prefix: [7]u8 = [7]u8{82, 45, 67, 72, 65, 84, 45}; + for (j in 0..7) { + if (chat_law_byte(law, CHAT_LAW_FIELD_ID, j) != prefix[j]) { return false; } } - return true; + const d0: usize = @as(usize, chat_law_byte(law, CHAT_LAW_FIELD_ID, 7)); + if (n < 10) { + return len == 8 and d0 == 48 + n; + } + if (len != 9) { + return false; + } + const d1: usize = @as(usize, chat_law_byte(law, CHAT_LAW_FIELD_ID, 8)); + return d0 == 48 + n / 10 and d1 == 48 + n % 10; } /// True when field f of law a and field f of law b hold the same bytes. @@ -545,6 +543,8 @@ test cr00_15_law_id_matches_only_its_own_number { assert(!chat_law_id_matches(0, 10)); assert(!chat_law_id_matches(9, 1)); assert(!chat_law_id_matches(11, 11)); + assert(!chat_law_id_matches(0, 0)); + assert(!chat_law_id_matches(0, 100)); } test cr00_16_law_fields_equal {