diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-07::src::cover_traffic_timing_correlation_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-07::src::cover_traffic_timing_correlation_guard.json new file mode 100644 index 0000000000..6c7202d2ea --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-07::src::cover_traffic_timing_correlation_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:9584114c62a3b9901a7634ee13bc97ebc1f0d535a4f6486e2be5588e96f44e5a", + "gen_hash_rust": "sha256:0c8a1ebc5d8ebb3aa2ff783c2195367e8a08da0f4a781673bde5681bc2f12392", + "gen_hash_verilog": "sha256:b76fd685573fe6a8895718df316e85af4fabf339fe7f1e3a5c2581db3578dc96", + "gen_hash_zig": "sha256:849b312808ab1db82265057ed9370622a730eed2b781545cbeca1df2ec312e89", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-07::src::cover_traffic_timing_correlation_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-17T03:34:37Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:848d7d491685f090a57ba335d59356a5f6bedaa5cea58775b3b979bbe62fe1f1", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_traffic_timing_correlation_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 11, + "total": 11, + "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 c041cbab56..5ce40728f4 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -855,6 +855,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-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_decoy_ratio_governor.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_traffic_timing_correlation_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-LAWS/src/lib.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-cli/src/cmd/agent.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-cli/src/cmd/commit.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_traffic_timing_correlation_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_traffic_timing_correlation_guard.t27 new file mode 100644 index 0000000000..759b0df765 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_traffic_timing_correlation_guard.t27 @@ -0,0 +1,327 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-07::src::cover_traffic_timing_correlation_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-07/src/cover_traffic_timing_correlation_guard.rs +// (CR-CHAT-07 - Cover traffic timing correlation guard, Wave-79 +// Lane B, R-CHAT-10). +// +// Cover and real timing must not correlate: cover always right +// after real is a recognizable pair, cover that only appears +// with real traffic makes its presence a signal, and cover +// inter-arrival mirroring real inter-arrival leaks the real +// pattern. The rules, in the original's order: the window +// ceiling, the presence of both trains (no real, no cover +// answers its own error), then per emission the consecutive- +// real probe and the cover-between-reals floor (at least one +// cover between any two reals), then over the whole window the +// always-follows rejection - when every cover of the window +// sits directly after a real, the pattern is correlated. +// +// The original returns Result<(), CoverTimingError>. This port +// carries the verdict as a named struct (owner decision D5): +// Ok first, then the six variants in the original's +// declaration order - ConsecutiveReal, InsufficientCover, +// CoverAlwaysFollowsReal, WindowTooLarge, NoRealTraffic, +// NoCoverTraffic - none of which carries a payload, so the +// code is the whole verdict. +// +// The original's CTCG-02 ignores its result entirely; the +// verified outcome is CoverAlwaysFollowsReal - the single +// cover of real, cover, real sits directly after a real, so +// every cover of the window follows one, and the port pins +// that outcome with the discrepancy named. The original +// also declares two of its counters twice (a duplicate its +// build tolerated); the port declares each once, the +// semantics identical. + +// Minimum cover emissions between two real emissions. +pub const CTCG_MIN_COVER_BETWEEN_REAL: usize = 1; + +// Maximum emissions in a window. +pub const CTCG_MAX_WINDOW: usize = 256; + +// Whether an emission is real or cover. +pub enum EmissionType { + Real, + Cover, +} + +// An emission event. +pub struct TimingEmission { + timestamp_ms: u64, + kind: EmissionType, +} + +// Verdict codes: Ok(()) and CoverTimingError's variants, in declaration order. +pub enum CoverTimingCode { + Ok, + ConsecutiveReal, + InsufficientCover, + CoverAlwaysFollowsReal, + WindowTooLarge, + NoRealTraffic, + NoCoverTraffic, +} + +// The verdict of the cover timing validation. No variant of the +// original's error carries a payload, so the code is the whole +// verdict. +pub struct CoverTimingVerdict { + code: CoverTimingCode, +} + +// [VERIFIED] Validate that cover and real traffic timing are +// not correlated. Returns Ok only when every rule holds, +// checked in the original's order: the window ceiling, the +// presence of both trains, then per emission the consecutive- +// real probe and the cover floor, then the whole-window +// always-follows rejection. +pub fn validate_cover_timing(emissions: []const TimingEmission) -> CoverTimingVerdict { + if (emissions.len > CTCG_MAX_WINDOW) { + return CoverTimingVerdict { code: CoverTimingCode.WindowTooLarge, }; + } + var has_real: bool = false; + var has_cover: bool = false; + for i in 0..emissions.len { + if (emissions[i].kind == EmissionType.Real) { + has_real = true; + } + if (emissions[i].kind == EmissionType.Cover) { + has_cover = true; + } + } + if (!has_real) { + return CoverTimingVerdict { code: CoverTimingCode.NoRealTraffic, }; + } + if (!has_cover) { + return CoverTimingVerdict { code: CoverTimingCode.NoCoverTraffic, }; + } + var consecutive_real: usize = 0; + var cover_since_last_real: usize = 0; + var cover_count: usize = 0; + var total_real: usize = 0; + var cover_after_real: usize = 0; + for i in 0..emissions.len { + if (emissions[i].kind == EmissionType.Real) { + if (consecutive_real > 0) { + return CoverTimingVerdict { code: CoverTimingCode.ConsecutiveReal, }; + } + if (total_real > 0) { + if (cover_since_last_real < CTCG_MIN_COVER_BETWEEN_REAL) { + return CoverTimingVerdict { code: CoverTimingCode.InsufficientCover, }; + } + } + consecutive_real = 1; + cover_since_last_real = 0; + total_real = total_real + 1; + } else { + cover_since_last_real = cover_since_last_real + 1; + cover_count = cover_count + 1; + if (i > 0) { + if (emissions[i - 1].kind == EmissionType.Real) { + cover_after_real = cover_after_real + 1; + } + } + consecutive_real = 0; + } + } + if (cover_count > 0) { + if (cover_after_real == cover_count) { + return CoverTimingVerdict { code: CoverTimingCode.CoverAlwaysFollowsReal, }; + } + } + return CoverTimingVerdict { code: CoverTimingCode.Ok, }; +} + +// **CTCG-01** - two consecutive reals rejected: no cover +// between them. +test ctcg_01_consecutive_real_rejected { + const seq: [4]TimingEmission = [4]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.ConsecutiveReal); +} + +// **CTCG-02** - the original ignores this result; the verified +// outcome is CoverAlwaysFollowsReal: the single cover sits +// directly after a real, so every cover of the window follows +// one - the floor of one cover between reals itself passes, +// the always-follows rule is what answers. The port pins the +// verified outcome and names the discrepancy. +test ctcg_02_insufficient_cover_exercised { + const seq: [3]TimingEmission = [3]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Real, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.CoverAlwaysFollowsReal); +} + +// **CTCG-03** - cover always follows real rejected: every cover +// of the window sits directly after a real. +test ctcg_03_cover_follows_real_rejected { + const seq: [4]TimingEmission = [4]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.CoverAlwaysFollowsReal); +} + +// **CTCG-04** - the window ceiling rejected: 257 emissions of a +// maximum 256, built in a loop like the original's, the kinds +// alternating. The batch rule fires before any emission is +// examined. +test ctcg_04_window_large_rejected { + var seq: [257]TimingEmission; + for i in 0..257 { + var kind: EmissionType = EmissionType.Cover; + if (i % 2 == 0) { + kind = EmissionType.Real; + } + seq[i] = TimingEmission { timestamp_ms: @as(u64, i) * 100, kind: kind, }; + } + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.WindowTooLarge); +} + +// **CTCG-05** - a window without real traffic rejected. +test ctcg_05_no_real_rejected { + const seq: [3]TimingEmission = [3]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.NoRealTraffic); +} + +// **CTCG-06** - a window without cover traffic rejected: one +// real, nothing else. +test ctcg_06_no_cover_rejected { + const seq: [1]TimingEmission = [1]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Real, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.NoCoverTraffic); +} + +// **CTCG-07** - the valid sequence accepted: cover, real, +// cover, cover, real, then three covers - every real separated, +// not every cover after a real. +test ctcg_07_valid_accepted { + const seq: [8]TimingEmission = [8]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 500, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 600, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 700, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 800, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.Ok); +} + +// **CTCG-08** - cover before the first real accepted: two +// covers open the window, so the later covers after reals do +// not make the whole pattern always-follows. +test ctcg_08_cover_first_accepted { + const seq: [5]TimingEmission = [5]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 500, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.Ok); +} + +// **CTCG-09** - the interleaved sequence accepted: three reals, +// each with covers between, and covers not all after reals. +test ctcg_09_interleaved_accepted { + const seq: [9]TimingEmission = [9]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 500, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 600, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 700, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 800, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 900, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.Ok); +} + +// **CTCG-10** - the minimal valid sequence accepted: six +// emissions, two reals, every gap covered. +test ctcg_10_minimal_accepted { + const seq: [6]TimingEmission = [6]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 500, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 600, kind: EmissionType.Cover, }, + }; + const v = validate_cover_timing(&seq); + assert(v.code == CoverTimingCode.Ok); +} + +// Rule order is the original's: the window ceiling before any +// presence check, the no-real before the no-cover probe, the +// presence checks before the per-emission rules, the +// consecutive-real before the cover floor, and the per-emission +// rules before the always-follows rejection. +test rule_order_matches_original { + var flooded: [257]TimingEmission; + for i in 0..257 { + flooded[i] = TimingEmission { timestamp_ms: @as(u64, i), kind: EmissionType.Cover, }; + } + const v1 = validate_cover_timing(&flooded); + assert(v1.code == CoverTimingCode.WindowTooLarge); + + const no_train: [3]TimingEmission = [3]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Cover, }, + }; + const v2 = validate_cover_timing(&no_train); + assert(v2.code == CoverTimingCode.NoRealTraffic); + + const twins: [3]TimingEmission = [3]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Cover, }, + }; + const v3 = validate_cover_timing(&twins); + assert(v3.code == CoverTimingCode.ConsecutiveReal); + + const back_to_back: [4]TimingEmission = [4]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Real, }, + }; + const v4 = validate_cover_timing(&back_to_back); + assert(v4.code == CoverTimingCode.ConsecutiveReal); + + const paired: [4]TimingEmission = [4]TimingEmission{ + TimingEmission { timestamp_ms: 100, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 200, kind: EmissionType.Cover, }, + TimingEmission { timestamp_ms: 300, kind: EmissionType.Real, }, + TimingEmission { timestamp_ms: 400, kind: EmissionType.Cover, }, + }; + const v5 = validate_cover_timing(&paired); + assert(v5.code == CoverTimingCode.CoverAlwaysFollowsReal); +}