diff --git a/specs/igla/own_model_board.t27 b/specs/igla/own_model_board.t27 new file mode 100644 index 0000000000..144df03edb --- /dev/null +++ b/specs/igla/own_model_board.t27 @@ -0,0 +1,311 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/igla/own_model_board.t27 -- the own-model map (specs/igla/own_model.t27, epic #10024) said +; in the IGLA board's own event shape, so the board can show it with no new code on its side. + +; THE BOARD (gHashTag/igla-coder-gpu board/server.py, read 2026-10-17) takes a live event +; {job, stage, msg, progress, metrics} +; with msg at most 500 characters, progress in 0..1 and metrics an object of at most 4 KB. It draws +; the event in its live log, and as a bar on any pipeline node whose id equals the event's stage. +; This spec is that event, as values: JOB, STAGE, MSG, PROGRESS, and the metrics object +; {"lens_pct": LENS_PCT, "cells": [{"status": CELL_STATUS[c], "pct": CELL_PCT[c]}, ...]} +; whose keys are KEY_LENS, KEY_CELLS, KEY_STATUS and KEY_PCT below. + +; WHY THE VALUES ARE WRITTEN OUT and not read through `use`: the event has to leave the compiler as +; data, and a backend that prints declarations prints a literal but announces, and leaves out, a +; value that lives in another module. So every field is a literal here, and the tests below hold +; each one to the own_model value it projects. A change to own_model.t27 that is not carried here +; fails this spec; nothing here can drift from the map in silence. + +; MSG is the map's tally: "N published, N verified, N drafts, N gaps; NN%". msg_matches reads +; the five numbers back out of the text and compares them to count_status over own_model's STATUS +; and to its overall mean percent, and checks the words between them. + +; Not claimed: this spec delivers nothing. Posting the event (a cron service in Railway project +; igla-judge, to the board's private port) is separate work, and so is the board's stale snapshot. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module own_model_board; + +use t27f::reel::CELL_COUNT; +use t27f::topic_engine::STATUS_GAP; +use t27f::topic_engine::STATUS_LOCKED; +use t27f::topic_engine::STATUS_OPEN; +use t27f::topic_engine::STATUS_DRAFT; +use t27f::topic_engine::STATUS_VERIFIED; +use t27f::topic_engine::STATUS_PUBLISHED; +use t27f::topic_reel::count_status; +use igla::own_model::STATUS; +use igla::own_model::PCT; +use igla::own_model::LENS_TITLES; +use igla::own_model::mean_pct; + +/// The board's limits on one event (board/server.py). +pub const MSG_MAX : i32 = 500; +pub const METRICS_MAX : i32 = 4096; + +/// Cells per lens: three lenses of nine. +pub const LENS_CELLS : i32 = 9; + +pub const JOB : str = "own_model"; +pub const STAGE : str = "own_model"; +pub const MSG : str = "1 published, 11 verified, 8 drafts, 7 gaps; 39%"; +/// What MSG says once its numbers are taken out. +pub const MSG_WORDS : str = " published, verified, drafts, gaps; %"; +pub const OVERALL_PCT : u8 = 39; +pub const PROGRESS : f64 = 0.39; + +pub const KEY_LENS : str = "lens_pct"; +pub const KEY_CELLS : str = "cells"; +pub const KEY_STATUS : str = "status"; +pub const KEY_PCT : str = "pct"; + +pub const LENS_PCT : [3]u8 = [45, 45, 28]; +pub const CELL_STATUS : [27]u8 = [4, 4, 4, 3, 3, 3, 3, 0, 0, 4, 4, 4, 4, 4, 3, 3, 0, 0, 4, 4, 5, 4, 3, 0, 0, 0, 3]; +pub const CELL_PCT : [27]u8 = [60, 70, 80, 80, 60, 10, 50, 0, 0, 100, 100, 20, 80, 65, 35, 5, 0, 0, 70, 15, 60, 40, 23, 0, 0, 0, 50]; + +/// The size of the compact metrics object, in bytes, computed from the keys and values above. +pub const METRICS_BYTES : i32 = 621; + +pub fn is_digit(ch: u8) -> bool { + return ch >= '0' and ch <= '9'; +} + +/// The number n (from 0) among the runs of decimal digits in s, or -1 if s has fewer. +pub fn nth_number(s: str, n: i32) -> i32 { + const len : i32 = @intCast(s.len); + var seen : i32 = 0; + var value : i32 = 0; + var inside : bool = false; + var i : i32 = 0; + while (i < len) { + const ch : u8 = s[@intCast(i)]; + if (is_digit(ch)) { + const d : i32 = @intCast(ch); + value = value * 10 + (d - 48); + inside = true; + } else { + if (inside) { + if (seen == n) { + return value; + } + seen = seen + 1; + } + value = 0; + inside = false; + } + i = i + 1; + } + if (inside and seen == n) { + return value; + } + return -1; +} + +/// s, with every digit taken out, is exactly words. +pub fn words_match(s: str, words: str) -> bool { + const len : i32 = @intCast(s.len); + const wlen : i32 = @intCast(words.len); + var j : i32 = 0; + var i : i32 = 0; + while (i < len) { + const ch : u8 = s[@intCast(i)]; + if (is_digit(ch) == false) { + if (j >= wlen) { + return false; + } + if (words[@intCast(j)] != ch) { + return false; + } + j = j + 1; + } + i = i + 1; + } + return j == wlen; +} + +/// msg is the tally of status and the overall percent, in MSG_WORDS, with nothing else in it. +pub fn msg_matches(msg: str, status: [27]u8, overall: i32) -> bool { + if (words_match(msg, MSG_WORDS) == false) { + return false; + } + if (nth_number(msg, 0) != count_status(status, STATUS_PUBLISHED)) { + return false; + } + if (nth_number(msg, 1) != count_status(status, STATUS_VERIFIED)) { + return false; + } + if (nth_number(msg, 2) != count_status(status, STATUS_DRAFT)) { + return false; + } + if (nth_number(msg, 3) != count_status(status, STATUS_GAP)) { + return false; + } + if (nth_number(msg, 4) != overall) { + return false; + } + return nth_number(msg, 5) == -1; +} + +/// progress is overall percent over a hundred, to within f64 rounding, and inside the board's 0..1. +pub fn progress_matches(progress: f64, overall: i32) -> bool { + const want : f64 = @floatFromInt(overall); + const d : f64 = progress * 100.0 - want; + if (d > 0.000000001 or d < -0.000000001) { + return false; + } + return progress >= 0.0 and progress <= 1.0; +} + +/// Every cell drawn as a gap is at 0 percent. +pub fn gaps_at_zero(status: [27]u8, pct: [27]u8) -> bool { + var c : i32 = 0; + while (c < CELL_COUNT) { + const i : usize = @intCast(c); + if (status[i] == STATUS_GAP and pct[i] > 0) { + return false; + } + c = c + 1; + } + return true; +} + +/// The first cell where a and b differ, or -1. +pub fn first_difference(a: [27]u8, b: [27]u8) -> i32 { + var c : i32 = 0; + while (c < CELL_COUNT) { + const i : usize = @intCast(c); + if (a[i] != b[i]) { + return c; + } + c = c + 1; + } + return -1; +} + +/// Decimal digits of a value 0..255. +pub fn digits(v: u8) -> i32 { + if (v >= 100) { + return 3; + } + if (v >= 10) { + return 2; + } + return 1; +} + +/// A key and its quotes. +pub fn quoted(key: str) -> i32 { + const n : i32 = @intCast(key.len); + return n + 2; +} + +/// Bytes of {"lens_pct":[a,b,c],"cells":[{"status":s,"pct":p},...]} with no spaces. +pub fn metrics_bytes(lens: [3]u8, status: [27]u8, pct: [27]u8) -> i32 { + var lens_array : i32 = 2 + 2; + var l : i32 = 0; + while (l < 3) { + lens_array = lens_array + digits(lens[@intCast(l)]); + l = l + 1; + } + var cells_array : i32 = 2 + (CELL_COUNT - 1); + var c : i32 = 0; + while (c < CELL_COUNT) { + const i : usize = @intCast(c); + cells_array = cells_array + 1 + quoted(KEY_STATUS) + 1 + digits(status[i]) + 1 + quoted(KEY_PCT) + 1 + digits(pct[i]) + 1; + c = c + 1; + } + return 1 + quoted(KEY_LENS) + 1 + lens_array + 1 + quoted(KEY_CELLS) + 1 + cells_array + 1; +} + +test the_metrics_are_own_models_arrays { + assert first_difference(CELL_STATUS, STATUS) == -1; + assert first_difference(CELL_PCT, PCT) == -1; + var l : i32 = 0; + while (l < 3) { + const lens : i32 = @intCast(LENS_PCT[@intCast(l)]); + assert lens == mean_pct(l * LENS_CELLS, LENS_CELLS); + assert LENS_TITLES[@intCast(l)].len > 0; + l = l + 1; + } + assert LENS_CELLS * 3 == CELL_COUNT; + // a copy one cell off is caught, at that cell + var wrong : [27]u8 = CELL_PCT; + wrong[12] = 81; + assert first_difference(wrong, PCT) == 12; +} + +test a_gap_cell_is_never_above_zero_percent { + assert gaps_at_zero(CELL_STATUS, CELL_PCT); + var c : i32 = 0; + while (c < CELL_COUNT) { + const i : usize = @intCast(c); + if (CELL_STATUS[i] == STATUS_GAP) { + assert CELL_PCT[i] == 0; + } + assert CELL_PCT[i] <= 100; + c = c + 1; + } + // the public 100M model, cell 7, is a gap: drawn at 10 percent it is refused + assert CELL_STATUS[7] == STATUS_GAP; + var wrong : [27]u8 = CELL_PCT; + wrong[7] = 10; + assert gaps_at_zero(CELL_STATUS, wrong) == false; +} + +test the_tally_sums_to_twenty_seven { + const published : i32 = count_status(CELL_STATUS, STATUS_PUBLISHED); + const verified : i32 = count_status(CELL_STATUS, STATUS_VERIFIED); + const drafts : i32 = count_status(CELL_STATUS, STATUS_DRAFT); + const gaps : i32 = count_status(CELL_STATUS, STATUS_GAP); + assert count_status(CELL_STATUS, STATUS_LOCKED) == 0; + assert count_status(CELL_STATUS, STATUS_OPEN) == 0; + assert published + verified + drafts + gaps == CELL_COUNT; + assert published == 1; + assert verified == 11; + assert drafts == 8; + assert gaps == 7; +} + +test the_message_is_the_tally { + const overall : i32 = @intCast(OVERALL_PCT); + assert overall == mean_pct(0, CELL_COUNT); + assert msg_matches(MSG, STATUS, overall); + const n : i32 = @intCast(MSG.len); + assert n <= MSG_MAX; + // one number wrong, a word changed, or a number added: each refused + assert msg_matches("1 published, 12 verified, 8 drafts, 7 gaps; 39%", STATUS, overall) == false; + assert msg_matches("1 published, 11 verified, 8 drafts, 7 holes; 39%", STATUS, overall) == false; + assert msg_matches("1 published, 11 verified, 8 drafts, 7 gaps; 39% of 100", STATUS, overall) == false; + assert msg_matches(MSG, STATUS, 40) == false; + assert nth_number(MSG, 1) == 11; + assert nth_number(MSG, 4) == 39; + assert nth_number(MSG, 5) == -1; +} + +test progress_is_the_overall_percent_over_a_hundred { + assert progress_matches(PROGRESS, mean_pct(0, CELL_COUNT)); + // a bar one point off, or past the end of the board's 0..1, is refused + assert progress_matches(0.40, mean_pct(0, CELL_COUNT)) == false; + assert progress_matches(1.39, 139) == false; + assert progress_matches(-0.01, -1) == false; + assert JOB.len > 0; + assert STAGE.len > 0; +} + +test the_metrics_fit_the_board { + assert metrics_bytes(LENS_PCT, CELL_STATUS, CELL_PCT) == METRICS_BYTES; + assert METRICS_BYTES <= METRICS_MAX; + // the worst case, every percent three digits, still fits + var full : [27]u8 = CELL_PCT; + var c : i32 = 0; + while (c < CELL_COUNT) { + full[@intCast(c)] = 100; + c = c + 1; + } + assert metrics_bytes(LENS_PCT, CELL_STATUS, full) <= METRICS_MAX; + assert metrics_bytes(LENS_PCT, CELL_STATUS, full) > METRICS_BYTES; +} + +invariant one_event_per_map { + assert CELL_COUNT == 27; +}