diff --git a/specs/port/trios/crates/trios-rainbow-bridge/src/channel.t27 b/specs/port/trios/crates/trios-rainbow-bridge/src/channel.t27 new file mode 100644 index 0000000000..c7103c5cd9 --- /dev/null +++ b/specs/port/trios/crates/trios-rainbow-bridge/src/channel.t27 @@ -0,0 +1,116 @@ +// trios-rainbow-bridge colour channels — the payload-to-channel total +// function. +// Port of gHashTag/trios:crates/trios-rainbow-bridge/src/channel.rs +// (at 8b229e9489ee, 137 lines) — Roadmap Stage 6, goal #4548, target t27c +// gen-rust. +// +// The original declares exactly seven colour channels in ROY G BIV order +// (an eighth variant is forbidden — R7 + ONE SHOT §8, mirrored by the Coq +// lemma seven_channels_total) and the total function mapping each of the +// seven payload variants to its one legal channel: claim → red, +// heartbeat → orange, done → yellow, honey → green, state → blue, +// violation → indigo, victory → violet — a match with no wildcard arm, +// total and injective on colour, as the original's own test asserts. +// +// The language does not compile enum values as arguments or literals, so +// both enums are modelled by their serde snake_case tags and channel +// names, the shape this series uses for command strings: the caller hands +// the payload's tag, the decision answers the channel name. An unknown +// tag answers the empty string — the original has no eighth arm to reach, +// and the empty answer marks exactly that impossible case. Every function +// is a tested pure decision; no transport exists in this port (issue +// #9734, "Port the decision, not the plumbing"). + +module port::trios_rainbow_bridge_channel; + +// Original lines 33-46: `Channel::ALL` — the canonical ROY G BIV order, +// and `super::CHANNEL_COUNT` = 7 (the original's own exactly_seven test +// reads both). +pub fn channel_count() -> usize { + return 7; +} + +pub fn channel_in_order(index: usize) -> str { + if (index == 0) { return "red"; } + if (index == 1) { return "orange"; } + if (index == 2) { return "yellow"; } + if (index == 3) { return "green"; } + if (index == 4) { return "blue"; } + if (index == 5) { return "indigo"; } + if (index == 6) { return "violet"; } + return ""; +} + +// The seven payload kinds, in the sample order of the original's own +// injectivity test (lines 125-133). +pub fn payload_kind_count() -> usize { + return 7; +} + +pub fn payload_kind_in_order(index: usize) -> str { + if (index == 0) { return "claim"; } + if (index == 1) { return "heartbeat"; } + if (index == 2) { return "done"; } + if (index == 3) { return "honey"; } + if (index == 4) { return "state"; } + if (index == 5) { return "violation"; } + if (index == 6) { return "victory"; } + return ""; +} + +// Original lines 100-110: `pub fn channel_of_payload(p: &Payload) -> +// Channel` — the total, wildcard-free mapping from each payload variant +// to its one legal channel. The empty answer is the unreachable eighth: +// the original's match has no wildcard arm. +pub fn channel_of_payload(payload_kind: str) -> str { + if (payload_kind == "claim") { return "red"; } + if (payload_kind == "heartbeat") { return "orange"; } + if (payload_kind == "done") { return "yellow"; } + if (payload_kind == "honey") { return "green"; } + if (payload_kind == "state") { return "blue"; } + if (payload_kind == "violation") { return "indigo"; } + if (payload_kind == "victory") { return "violet"; } + return ""; +} + +// --------------------------------------------------------------------------- +// Tests: the original's own tests (lines 116-136) and the per-kind mapping. +// --------------------------------------------------------------------------- + +test exactly_seven_channels { + assert(channel_count() == 7); + assert(payload_kind_count() == 7); +} + +test each_kind_maps_to_its_colour { + assert(channel_of_payload("claim") == "red"); + assert(channel_of_payload("heartbeat") == "orange"); + assert(channel_of_payload("done") == "yellow"); + assert(channel_of_payload("honey") == "green"); + assert(channel_of_payload("state") == "blue"); + assert(channel_of_payload("violation") == "indigo"); + assert(channel_of_payload("victory") == "violet"); +} + +test mapping_is_total_and_injective_on_colour { + var i: usize = 0; + while (i < 7) { + const kind = payload_kind_in_order(i); + const mapped = channel_of_payload(kind); + assert(mapped == channel_in_order(i)); + var j: usize = 0; + while (j < 7) { + if (i != j) { + assert(mapped != channel_in_order(j)); + } + j += 1; + } + i += 1; + } +} + +test the_eighth_channel_is_unreachable { + assert(channel_of_payload("eighth") == ""); + assert(channel_in_order(7) == ""); + assert(payload_kind_in_order(7) == ""); +}