From 82ea8dc337b8201b3aeae390a5e59d274716e2bc Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 09:33:11 +0700 Subject: [PATCH 1/2] spec(igla): own_model cell 23 verified -- 17 of 17 ML specs compile (Closes #10163) nn/attention 35/35 on the Railway lab after #10095; the other ML specs still pass on the same checkout. Tally 1 published, 16 verified, 5 drafts, 5 gaps; the board event follows. Co-Authored-By: Claude Opus 5.5 --- specs/igla/own_model.t27 | 41 ++++++++++++++++++++-------------- specs/igla/own_model_board.t27 | 22 +++++++++--------- 2 files changed, 35 insertions(+), 28 deletions(-) diff --git a/specs/igla/own_model.t27 b/specs/igla/own_model.t27 index 84e4b8d192..f30ed5aa80 100644 --- a/specs/igla/own_model.t27 +++ b/specs/igla/own_model.t27 @@ -61,13 +61,18 @@ ; forwardTrain (bind, rotate, the PHI_INV gate, +0.1 * project(context) when it fires, the ; output into the next block); the stream never reads a float parameter, so the gradient ; checks hold with it on. A gate mutant (> for >=) fails 2 tests and a gain-0 mutant fails 1. +; - re-test on 2026-10-18, t27c built from SOURCE_COMMIT, lab checkout at master ba78d6d3c, after +; the PR that made nn/attention compile (#10094): nn/attention 35/35 pass, 9 invariants proved, +; 0 vacuous. The other seven re-run on the same checkout still pass (cross_entropy_loss 5/5, sgd +; 4/4, adam 4/4, adamw 12/12, lamb 4/4, nn/hslm 61/61, hslm/forward_pass 14/14), so 17 of the 17 +; ML specs compile and pass, and cell 23 has its passing test. ; - live: GET huggingface.co/api/models/playra/tern-tc-9m and .../tern-tc-9m-t27 returned 200; ; .../tern-tc-100m returned 401, the same as a made-up name, so no 100M is public. ; GET board-production-2dec.up.railway.app/state returned 200 and a made-up path 404; its ; snapshot is dated 2026-10-05, so the board is live and 12 days stale. ; - review: no PR behind any cell has a review, so no DELIVER cell is VERIFIED. ; The engine asks an engineering LEARN step for a source link, a PRACTICE step for a passing test -; and a DELIVER step for a review. So: 1 published, 15 verified, 6 drafts, 5 gaps. +; and a DELIVER step for a review. So: 1 published, 16 verified, 5 drafts, 5 gaps. ; PERCENT is a second, separate number per cell: an estimate of how much of that part exists, with ; its basis in SOURCES. It never feeds a status. The lens and overall figures are plain means, every @@ -184,7 +189,7 @@ pub const SOURCES : [27]str = [ "trinity-fpga b2bd5a30, 7682304/7682304 receipts", "board-production-2dec.up.railway.app/state", "t27 specs/port/trinity/fpga/openxc7-synth/ternary_matvec.t27", - "t27c test-report on 17 ML specs: 16 compile", + "t27c test-report on 17 ML specs: 17 compile", "", "", "", @@ -208,20 +213,20 @@ pub const MISSING : [27]str = [ /// The measurements per cell (see the header for how each was taken). pub const GROUNDED : [27]bool = [true, true, true, true, true, true, true, false, false, true, true, true, true, true, true, true, true, true, true, true, true, true, true, false, false, false, true]; -pub const TEST_PASS : [27]bool = [false, false, false, true, true, true, false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, false, false, false, false, false]; +pub const TEST_PASS : [27]bool = [false, false, false, true, true, true, false, false, false, false, false, false, true, true, true, false, false, false, false, false, false, true, true, false, false, false, false]; pub const REVIEWED : [27]bool = [false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]; pub const LIVE : [27]bool = [false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false]; /// What a host passes the viewer, per cell: the earned status code and the step number as a label. -pub const STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 3, 0, 0, 4, 4, 4, 4, 4, 4, 3, 3, 3, 4, 4, 5, 4, 3, 0, 0, 0, 3]; +pub const STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 3, 0, 0, 4, 4, 4, 4, 4, 4, 3, 3, 3, 4, 4, 5, 4, 4, 0, 0, 0, 3]; pub const LABELS : [27]str = ["1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17", "18", "19", "20", "21", "22", "23", "24", "25", "26", "27"]; /// Percent of each part that exists, estimated from its source (see the header). Never a status. -pub const PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 0, 0, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 94, 0, 0, 0, 50]; +pub const PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 0, 0, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 100, 0, 0, 0, 50]; /// The t27c test-report counts the PRACTICE cells quote. pub const ML_SPECS_MEASURED : i32 = 17; -pub const ML_SPECS_COMPILING : i32 = 16; +pub const ML_SPECS_COMPILING : i32 = 17; pub const CODER_SPECS : i32 = 9; pub const CODER_SPECS_COMPILING : i32 = 9; @@ -240,9 +245,9 @@ pub const ROWS : [20]str = [ "64 Zig files; best PPL 2.96 at ctx 27", "Those checkpoints were wiped", "In t27: loss, optimizers, HSLM pass", - "16 of 17 ML specs compile on the lab", + "17 of 17 ML specs compile on the lab", "9 of 9 IGLA CODER specs compile", - "1 published, 15 verified, 6 drafts", + "1 published, 16 verified, 5 drafts", "5 gaps, about 54 percent overall", "Batched f32 HSLM trainer", "Shadow weights for the whole model", @@ -313,15 +318,15 @@ test a_gap_is_named_not_filled { test a_status_is_earned_not_chosen { assert statuses_earned(STATUS, DOMAIN, GROUNDED, TEST_PASS, REVIEWED, LIVE); - // the evidence slide's "1 published, 15 verified, 6 drafts" and "5 gaps" + // the evidence slide's "1 published, 16 verified, 5 drafts" and "5 gaps" assert count_status(STATUS, STATUS_PUBLISHED) == 1; - assert count_status(STATUS, STATUS_VERIFIED) == 15; - assert count_status(STATUS, STATUS_DRAFT) == 6; + assert count_status(STATUS, STATUS_VERIFIED) == 16; + assert count_status(STATUS, STATUS_DRAFT) == 5; assert count_status(STATUS, STATUS_GAP) == 5; assert count_true(REVIEWED) == 0; // every passing test is a PRACTICE step: the t27 bench, MultiPL-E and coder specs (cells 4 to - // 6), loss, optimizers, forward pass, matvec - assert count_true(TEST_PASS) == 7; + // 6), loss, optimizers, forward pass, matvec, and the ML specs that compile (cell 23) + assert count_true(TEST_PASS) == 8; var c : i32 = 0; while (c < CELL_COUNT) { const i : usize = @intCast(c); @@ -347,11 +352,13 @@ test the_compile_counts_are_the_measured_ones { assert p5 == share_pct(CODER_SPECS_COMPILING, CODER_SPECS); // the compile cell's percent is the measured share, truncated const share : i32 = share_pct(ML_SPECS_COMPILING, ML_SPECS_MEASURED); - assert share == 94; + assert share == 100; const p22 : i32 = @intCast(PCT[22]); assert p22 == share; - // the compiling ML specs are the nine coder specs plus the six that compiled before them - assert ML_SPECS_COMPILING == CODER_SPECS_COMPILING + 7; + // the compiling ML specs are the nine coder specs plus the eight others + assert ML_SPECS_COMPILING == CODER_SPECS_COMPILING + 8; + assert ML_SPECS_COMPILING == ML_SPECS_MEASURED; + assert STATUS[22] == STATUS_VERIFIED; assert CODER_SPECS <= ML_SPECS_MEASURED; // the two coder cells that carry numbers (bench, MultiPL-E) are verified by their spec's test assert TEST_PASS[3]; @@ -363,7 +370,7 @@ test the_compile_counts_are_the_measured_ones { test percent_per_lens_is_a_plain_mean { assert mean_pct(0, 9) == 55; assert mean_pct(9, 9) == 70; - assert mean_pct(18, 9) == 36; + assert mean_pct(18, 9) == 37; // the evidence slide's "about 54 percent overall" assert mean_pct(0, CELL_COUNT) == 54; } diff --git a/specs/igla/own_model_board.t27 b/specs/igla/own_model_board.t27 index 368059de15..450a2acdb4 100644 --- a/specs/igla/own_model_board.t27 +++ b/specs/igla/own_model_board.t27 @@ -48,7 +48,7 @@ pub const LENS_CELLS : i32 = 9; pub const JOB : str = "own_model"; pub const STAGE : str = "own_model"; -pub const MSG : str = "1 published, 15 verified, 6 drafts, 5 gaps; 54%"; +pub const MSG : str = "1 published, 16 verified, 5 drafts, 5 gaps; 54%"; /// What MSG says once its numbers are taken out. pub const MSG_WORDS : str = " published, verified, drafts, gaps; %"; pub const OVERALL_PCT : u8 = 54; @@ -59,12 +59,12 @@ pub const KEY_CELLS : str = "cells"; pub const KEY_STATUS : str = "status"; pub const KEY_PCT : str = "pct"; -pub const LENS_PCT : [3]u8 = [55, 70, 36]; -pub const CELL_STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 3, 0, 0, 4, 4, 4, 4, 4, 4, 3, 3, 3, 4, 4, 5, 4, 3, 0, 0, 0, 3]; -pub const CELL_PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 0, 0, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 94, 0, 0, 0, 50]; +pub const LENS_PCT : [3]u8 = [55, 70, 37]; +pub const CELL_STATUS : [27]u8 = [4, 4, 4, 4, 4, 4, 3, 0, 0, 4, 4, 4, 4, 4, 4, 3, 3, 3, 4, 4, 5, 4, 4, 0, 0, 0, 3]; +pub const CELL_PCT : [27]u8 = [60, 70, 80, 80, 60, 100, 50, 0, 0, 100, 100, 20, 80, 65, 95, 75, 55, 40, 70, 15, 60, 40, 100, 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 = 625; +pub const METRICS_BYTES : i32 = 626; pub fn is_digit(ch: u8) -> bool { return ch >= '0' and ch <= '9'; @@ -261,8 +261,8 @@ test the_tally_sums_to_twenty_seven { assert count_status(CELL_STATUS, STATUS_OPEN) == 0; assert published + verified + drafts + gaps == CELL_COUNT; assert published == 1; - assert verified == 15; - assert drafts == 6; + assert verified == 16; + assert drafts == 5; assert gaps == 5; } @@ -273,11 +273,11 @@ test the_message_is_the_tally { 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, 14 verified, 6 drafts, 5 gaps; 54%", STATUS, overall) == false; - assert msg_matches("1 published, 15 verified, 6 drafts, 5 holes; 54%", STATUS, overall) == false; - assert msg_matches("1 published, 15 verified, 6 drafts, 5 gaps; 54% of 100", STATUS, overall) == false; + assert msg_matches("1 published, 15 verified, 5 drafts, 5 gaps; 54%", STATUS, overall) == false; + assert msg_matches("1 published, 16 verified, 5 drafts, 5 holes; 54%", STATUS, overall) == false; + assert msg_matches("1 published, 16 verified, 5 drafts, 5 gaps; 54% of 100", STATUS, overall) == false; assert msg_matches(MSG, STATUS, 48) == false; - assert nth_number(MSG, 1) == 15; + assert nth_number(MSG, 1) == 16; assert nth_number(MSG, 4) == 54; assert nth_number(MSG, 5) == -1; } From d1e247fd776ef2af78ef886fe58939e32ad6a247 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 09:34:45 +0700 Subject: [PATCH 2/2] spec(igla): own_model -- re-take the DELIVER cells' evidence for review (Refs #10163) nn/ternary_ste 26/26, nn/hslm_backward 15/15, nn/hslm_data 39/39, ml/arena_heap 10/10, ml/file_io_contract 12/12 on the lab; HF and board endpoints re-read. REVIEWED stays false until a later PR names the review. Co-Authored-By: Claude Opus 5.5 --- specs/igla/own_model.t27 | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/specs/igla/own_model.t27 b/specs/igla/own_model.t27 index f30ed5aa80..c01a8c3ddd 100644 --- a/specs/igla/own_model.t27 +++ b/specs/igla/own_model.t27 @@ -65,7 +65,12 @@ ; the PR that made nn/attention compile (#10094): nn/attention 35/35 pass, 9 invariants proved, ; 0 vacuous. The other seven re-run on the same checkout still pass (cross_entropy_loss 5/5, sgd ; 4/4, adam 4/4, adamw 12/12, lamb 4/4, nn/hslm 61/61, hslm/forward_pass 14/14), so 17 of the 17 -; ML specs compile and pass, and cell 23 has its passing test. +; ML specs compile and pass, and cell 23 has its passing test. The DELIVER cells' evidence was +; re-taken on the same checkout for the review of that PR: nn/ternary_ste 26/26, +; nn/hslm_backward 15/15, nn/hslm_data 39/39, ml/arena_heap 10/10, ml/file_io_contract 12/12, +; 0 vacuous (cells 16-18); playra/tern-tc-9m and tern-tc-9m-t27 200, tern-tc-100m 401 (cells 7 +; and 8); the board /state 200 (cell 21). A review of that PR is what the engine asks of cells +; 7, 16, 17, 18 and 27; REVIEWED turns true only in a later PR that names the approving review. ; - live: GET huggingface.co/api/models/playra/tern-tc-9m and .../tern-tc-9m-t27 returned 200; ; .../tern-tc-100m returned 401, the same as a made-up name, so no 100M is public. ; GET board-production-2dec.up.railway.app/state returned 200 and a made-up path 404; its