diff --git a/.trinity/seals/src_port::trios::crates::trios_chat::rings::CR_CHAT_01::src::identity_key_usage_count_guard.json b/.trinity/seals/src_port::trios::crates::trios_chat::rings::CR_CHAT_01::src::identity_key_usage_count_guard.json new file mode 100644 index 0000000000..4635db2601 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios_chat::rings::CR_CHAT_01::src::identity_key_usage_count_guard.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+82de5086e", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:b9b86d1f9e32e855d5bbbf5fca81628179ef08784f85265eef3ba734c7264daf", + "gen_hash_rust": "sha256:8ddc835042c8843a304a23eb50ae4bd35d99ee6ff5af903ab38fb095588da1ce", + "gen_hash_verilog": "sha256:26f87391c7247b606d68126d94310a335bc71a7785651aa33f05b5c394a6539b", + "gen_hash_zig": "sha256:503d01702e1f7491d34e824db50bf5f51a60cdc043751664819ed1e1cf906893", + "module": "port::trios::crates::trios_chat::rings::CR_CHAT_01::src::identity_key_usage_count_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-30T19:37:50Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:984e6a910b01246515a548dab1f3c0cd38701dafb84398f60c9feb8b57d189b6", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-01/src/identity_key_usage_count_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 10, + "total": 10, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1a50286d6170ef41c779d26385a1be59823925d7131497c93d84194144ba93b3", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-01/src/identity_key_usage_count_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-01/src/identity_key_usage_count_guard.t27 new file mode 100644 index 0000000000..851b365792 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-01/src/identity_key_usage_count_guard.t27 @@ -0,0 +1,91 @@ +module port::trios::crates::trios_chat::rings::CR_CHAT_01::src::identity_key_usage_count_guard; + +// Port of gHashTag/trios +// crates/trios-chat/rings/CR-CHAT-01/src/identity_key_usage_count_guard.rs (138 lines). +// +// The Rust original returns Result<(), KeyUsageError>. The .t27 language has no +// Result/Option, so the same decision is carried by a closed enum with one honest +// "accepted" variant. `NegativeCount` and `MustRotate` are declared in Rust +// (lines 40-47) but `validate_key_usage` never constructs them: u64 cannot be +// negative, and rotation is reported by `key_needs_rotation` instead. They are +// therefore documented here rather than invented as reachable outcomes. + +// Lines 31 and 34: the two pre-registered thresholds. +const IKUC_MAX_SIGNATURES: u64 = 100_000; +const IKUC_WARN_SIGNATURES: u64 = 80_000; + +// Lines 39-48: `Result<(), KeyUsageError>` collapsed to a single code. +enum KeyUsageError { + Accepted, + SignatureCountExceeded, + ZeroKeyId, +} + +// Lines 51-62: zero key id is checked first, so a zero key with an over-limit +// count reports ZeroKeyId, not SignatureCountExceeded. The count bound is +// inclusive: exactly IKUC_MAX_SIGNATURES is still accepted. +pub fn validate_key_usage(key_id: u64, signature_count: u64) -> KeyUsageError { + if (key_id == 0) { + return .ZeroKeyId; + } + if (signature_count > IKUC_MAX_SIGNATURES) { + return .SignatureCountExceeded; + } + return .Accepted; +} + +// Lines 65-67: the warning threshold is inclusive (>=), and it is independent of +// the hard maximum: 80_000 already asks for rotation, 99_999 does not exceed max. +pub fn key_needs_rotation(signature_count: u64) -> bool { + return signature_count >= IKUC_WARN_SIGNATURES; +} + +// IKUC-01 (lines 74-80): one past the max is rejected. +test ikuc_01_exceeded_rejected { + assert(validate_key_usage(1, IKUC_MAX_SIGNATURES + 1) == .SignatureCountExceeded); +} + +// IKUC-02 (lines 83-88): zero key id is rejected. +test ikuc_02_zero_key_rejected { + assert(validate_key_usage(0, 10) == .ZeroKeyId); +} + +// IKUC-03 (lines 91-95): the maximum itself is accepted. +test ikuc_03_at_max_accepted { + assert(validate_key_usage(1, IKUC_MAX_SIGNATURES) == .Accepted); +} + +// IKUC-04 (lines 98-101): a fresh key with no signatures is accepted. +test ikuc_04_zero_sigs_accepted { + assert(validate_key_usage(1, 0) == .Accepted); +} + +// IKUC-05 (lines 104-107): the warning threshold triggers rotation. +test ikuc_05_warning_triggers { + assert(key_needs_rotation(IKUC_WARN_SIGNATURES)); +} + +// IKUC-06 (lines 110-113): one below the warning threshold does not. +test ikuc_06_below_warning { + assert(!key_needs_rotation(IKUC_WARN_SIGNATURES - 1)); +} + +// IKUC-07 (lines 116-119): a valid mid-range count is accepted. +test ikuc_07_mid_range_accepted { + assert(validate_key_usage(42, 50_000) == .Accepted); +} + +// IKUC-08 (lines 122-125): a single signature is accepted. +test ikuc_08_single_accepted { + assert(validate_key_usage(1, 1) == .Accepted); +} + +// IKUC-09 (lines 128-131): the hard maximum also needs rotation. +test ikuc_09_max_needs_rotation { + assert(key_needs_rotation(IKUC_MAX_SIGNATURES)); +} + +// IKUC-10 (lines 134-137): a huge key id is still a valid key id. +test ikuc_10_large_key_accepted { + assert(validate_key_usage(18_446_744_073_709_551_615, 1000) == .Accepted); +}