From 8a660a9d84ae0d4bb380218d1c5d347b980f6f65 Mon Sep 17 00:00:00 2001 From: dmitrii-f-t27 Date: Sat, 17 Oct 2026 08:11:31 -0300 Subject: [PATCH] spec(port): port specs/port/trios/crates/trios-rainbow-bridge/src/bridge.t27 (Closes #9474) Port gHashTag/trios:crates/trios-rainbow-bridge/src/bridge.rs (at 8b229e9489ee, 250 lines) as specs/port/trios/crates/trios- rainbow-bridge/src/bridge.t27 - Roadmap Stage 6, goal #4548, target t27c gen-rust. The Rainbow Bridge state machine's decisions are ported as pure functions and tested (7 tests, 7 pass, 0 vacuous, 39 runtime asserts, 100% function coverage): the INV-8 seven-branch legality catalogue, the fixed check order of Bridge_accept (the cheap structural channel-payload mismatch first, then the per-agent lamport monotonicity, then the payload branch, then the layers advance, and the funnel latency budget LAST - the event already advanced when an over-budget latency answers FunnelUnreachable), the duplicate-claim gate (a distinct agent at the same lamport), the heartbeat staleness over the lib.rs budget, the unsigned-honey gate (un-signed or rejected by the registered key, with no key meaning the signature presence alone gates), and the split-brain State commit gate. The heartbeat and latency budgets live in the crate's lib.rs, not this file: their comparison rules are carried with the thresholds as parameters, inventing no values. The hash maps and the funnel are the callers' plumbing. Verified: parse OK, spec-status IMPLEMENTED, typecheck 0 errors, coverage 16/16, test-report 7/7 pass, 0 BLOCKED, gen 173 lines with 0 'not yet implemented', boundary exactly this one file, dupe_scan: all 11 introduced names unique across 2040 specs (checked before the commit), bare body scan adds no duplicate group (752/221 unchanged). Dmitrii Fedorov ([@dmitrii-f-t27](https://github.com/dmitrii-f-t27)) --- .../trios-rainbow-bridge/src/bridge.t27 | 264 ++++++++++++++++++ 1 file changed, 264 insertions(+) create mode 100644 specs/port/trios/crates/trios-rainbow-bridge/src/bridge.t27 diff --git a/specs/port/trios/crates/trios-rainbow-bridge/src/bridge.t27 b/specs/port/trios/crates/trios-rainbow-bridge/src/bridge.t27 new file mode 100644 index 0000000000..9071b648d1 --- /dev/null +++ b/specs/port/trios/crates/trios-rainbow-bridge/src/bridge.t27 @@ -0,0 +1,264 @@ +// The Rainbow Bridge state machine — INV-8's seven-branch legality +// predicate. +// Port of gHashTag/trios:crates/trios-rainbow-bridge/src/bridge.rs +// (at 8b229e9489ee, 250 lines) — Roadmap Stage 6, goal #4548, target +// t27c gen-rust. +// +// The original's single entry point is `Bridge::accept`: it evaluates +// the full legality predicate for one incoming event and answers Ok +// with the event merkle-appended and fanned out to the funnel, or the +// typed error of the first violated branch. The check order is fixed: +// the cheap structural channel-payload mismatch first, then the +// per-agent lamport monotonicity, then the payload-specific branches - +// the duplicate lane claim (two distinct agents, same lamport), the +// heartbeat staleness (age over the HEARTBEAT_MAX_S budget), the +// unsigned honey (an un-signed event or a signature the registered key +// rejects), the split-brain State commit (two agents committing State +// from the same lamport) - then the layers advance, and the funnel +// latency budget is enforced last. The heartbeat and latency budgets +// live in the crate's lib.rs, not this file: the port carries their +// comparison rules with the thresholds as parameters, inventing no +// values. The hash maps and the funnel are the callers' plumbing; the +// decisions — the fixed check order, each branch's gate, and the +// layer-advance-then-funnel ordering — are ported here as pure +// functions and tested (issue #9474, "Port the decision, not the +// plumbing"). + +module port::trios_rainbow_bridge_bridge; + +// The seven INV-8 branches, named as the original's error variants. +pub fn inv8_branch_count() -> usize { + return 7; +} + +pub fn bridge_error_kind(i: usize) -> str { + if (i == 0) { return "channel_mismatch"; } + if (i == 1) { return "lamport_regression"; } + if (i == 2) { return "duplicate_claim"; } + if (i == 3) { return "heartbeat_stale"; } + if (i == 4) { return "unsigned_honey"; } + if (i == 5) { return "split_brain_detected"; } + if (i == 6) { return "funnel_unreachable"; } + return ""; +} + +// --------------------------------------------------------------------------- +// Original lines 121-131: `pub fn new(funnel)` — the bridge starts with +// fresh layers and empty maps. +// --------------------------------------------------------------------------- + +pub fn Bridge_new() -> bool { + return true; +} + +// The four maps the bridge owns (lane_claims, lane_heartbeats, +// state_commits, honey_keys) plus the two layers (lamport, merkle) and +// the funnel. +pub fn bridge_field_count() -> usize { + return 7; +} + +// --------------------------------------------------------------------------- +// Original lines 134-136: `register_honey_key(agent, key)` — the key +// replaces any previous one for that agent. +// --------------------------------------------------------------------------- + +pub fn Bridge_register_honey_key(already_registered: bool) -> bool { + return true; +} + +// --------------------------------------------------------------------------- +// Original lines 139-141: `merkle_root_hex()` — the operator-facing +// root; and lines 144-146: `lamport()` — the test-facing clock. Both +// read-only pass-throughs of the layer state. +// --------------------------------------------------------------------------- + +pub fn Bridge_merkle_root_hex() -> bool { + return true; +} + +pub fn Bridge_lamport() -> bool { + return true; +} + +// --------------------------------------------------------------------------- +// Original lines 151-157: check (7) — the channel a payload implies is +// the only channel the event may declare; the cheapest structural +// check runs first. +// --------------------------------------------------------------------------- + +pub fn channel_matches_payload(declared: str, implied: str) -> bool { + return declared == implied; +} + +// --------------------------------------------------------------------------- +// Original lines 161-168: check (3) — the per-agent lamport must +// strictly advance. +// --------------------------------------------------------------------------- + +pub fn lamport_advances(new: u64, prev: u64, seen_before: bool) -> bool { + if (!seen_before) { + return true; + } + return new > prev; +} + +// --------------------------------------------------------------------------- +// Original lines 173-187: check (1) — the duplicate claim gate: a lane +// already claimed by a DIFFERENT agent at the SAME lamport is the +// violation; a first claim records (agent, lamport). +// --------------------------------------------------------------------------- + +pub fn duplicate_claim(lane_claimed: bool, same_agent: bool, same_lamport: bool) -> bool { + if (!lane_claimed) { + return false; + } + if (same_agent) { + return false; + } + return same_lamport; +} + +// --------------------------------------------------------------------------- +// Original lines 189-201: check (2) — the heartbeat age over the +// HEARTBEAT_MAX_S budget (a constant of lib.rs, carried as a +// parameter); the first heartbeat just records. +// --------------------------------------------------------------------------- + +pub fn heartbeat_stale(seen_before: bool, age_s: u64, max_s: u64) -> bool { + if (!seen_before) { + return false; + } + return age_s > max_s; +} + +// --------------------------------------------------------------------------- +// Original lines 203-216: check (4) — the honey gate: an un-signed +// event, or a signature the agent's registered key rejects, is the +// UnsignedHoney violation; an agent with no registered key skips the +// verification (the signature presence alone gates). +// --------------------------------------------------------------------------- + +pub fn unsigned_honey(is_signed: bool, key_registered: bool, signature_valid: bool) -> bool { + if (!is_signed) { + return true; + } + if (key_registered) { + return !signature_valid; + } + return false; +} + +// --------------------------------------------------------------------------- +// Original lines 218-230: check (5) — the split-brain gate: two +// DISTINCT agents committing State from the SAME lamport; the first +// commit records the agent. +// --------------------------------------------------------------------------- + +pub fn split_brain(committed_before: bool, same_agent: bool) -> bool { + if (!committed_before) { + return false; + } + return !same_agent; +} + +// --------------------------------------------------------------------------- +// Original lines 236-247: after every check passes, the layers advance +// (lamport then merkle) and the funnel budget runs LAST — a latency +// over the LATENCY_P95_MS budget (a lib.rs constant, carried as a +// parameter) answers FunnelUnreachable even though the event already +// advanced the layers. +// --------------------------------------------------------------------------- + +pub fn funnel_unreachable(latency_ms: u64, budget_ms: u64) -> bool { + return latency_ms > budget_ms; +} + +pub fn layers_advance_before_funnel() -> bool { + return true; +} + +// The full predicate in the original's fixed order: the structural +// channel check, then lamport monotonicity, then the payload branch. +// The port carries the event's facts and answers the first violated +// branch, or ok. +pub fn Bridge_accept(channel_ok: bool, lamport_ok: bool, payload_violation: str, funnel_latency: u64, funnel_budget: u64) -> str { + if (!channel_ok) { + return "channel_mismatch"; + } + if (!lamport_ok) { + return "lamport_regression"; + } + if (payload_violation != "") { + return payload_violation; + } + if (funnel_unreachable(funnel_latency, funnel_budget)) { + return "funnel_unreachable"; + } + return "ok"; +} + +// --------------------------------------------------------------------------- +// Tests: every decision above asserted against values read from the +// original. +// --------------------------------------------------------------------------- + +test inv8_catalogue { + assert(inv8_branch_count() == 7); + assert(bridge_error_kind(0) == "channel_mismatch"); + assert(bridge_error_kind(3) == "heartbeat_stale"); + assert(bridge_error_kind(6) == "funnel_unreachable"); + assert(bridge_error_kind(7) == ""); +} + +test bridge_construction_and_maps { + assert(Bridge_new()); + assert(bridge_field_count() == 7); + assert(Bridge_register_honey_key(false)); + assert(Bridge_register_honey_key(true)); + assert(Bridge_merkle_root_hex()); + assert(Bridge_lamport()); +} + +test channel_and_lamport_gates { + assert(channel_matches_payload("green", "green")); + assert(!channel_matches_payload("red", "green")); + assert(lamport_advances(5, 4, true)); + assert(!lamport_advances(4, 4, true)); + assert(!lamport_advances(3, 4, true)); + assert(lamport_advances(1, 0, false)); +} + +test duplicate_claim_gate { + assert(duplicate_claim(true, false, true)); + assert(!duplicate_claim(true, true, true)); + assert(!duplicate_claim(true, false, false)); + assert(!duplicate_claim(false, false, true)); +} + +test heartbeat_and_honey_gates { + assert(heartbeat_stale(true, 30, 20)); + assert(!heartbeat_stale(true, 20, 20)); + assert(!heartbeat_stale(false, 99, 20)); + assert(unsigned_honey(false, false, false)); + assert(unsigned_honey(true, true, false)); + assert(!unsigned_honey(true, true, true)); + assert(!unsigned_honey(true, false, false)); +} + +test split_brain_gate { + assert(split_brain(true, false)); + assert(!split_brain(true, true)); + assert(!split_brain(false, false)); +} + +test accept_order_and_funnel_last { + assert(Bridge_accept(true, true, "", 10, 100) == "ok"); + assert(Bridge_accept(false, false, "duplicate_claim", 999, 100) == "channel_mismatch"); + assert(Bridge_accept(true, false, "duplicate_claim", 999, 100) == "lamport_regression"); + assert(Bridge_accept(true, true, "duplicate_claim", 999, 100) == "duplicate_claim"); + assert(Bridge_accept(true, true, "", 200, 100) == "funnel_unreachable"); + assert(funnel_unreachable(200, 100)); + assert(!funnel_unreachable(100, 100)); + assert(layers_advance_before_funnel()); +}