spec(port): port specs/port/trios/crates/trios-rainbow-bridge/src/channel.t27 (Closes #9734)

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) == "");
+}