diff --git a/.trinity/seals/coder_igla-coder-kill-rule.json b/.trinity/seals/coder_igla-coder-kill-rule.json new file mode 100644 index 0000000000..c16ffc1d72 --- /dev/null +++ b/.trinity/seals/coder_igla-coder-kill-rule.json @@ -0,0 +1,33 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+6ca19eff2", + "closure": [ + { + "spec": "specs/base/types.t27", + "spec_hash": "sha256:3c2fb2a2edf20e90bc76798fb5d12690b2f60fc0f5bbf2f6052936e22d6e62e2" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:3abc4aa902e592f6671f55c87356467326c665b4205ee12e06d6692b3678829e", + "gen_hash_rust": "sha256:5737988e3f076917142673f1e89de98c813db6c3fb1d60ff900fe3feb7b9d6fd", + "gen_hash_verilog": "sha256:8f9440ac71fca858b4f2d344184cd9a8ee956d4d274992b97bee3e4fac013598", + "gen_hash_zig": "sha256:131673eebb6cc83a1390c9800cc6d823fc2a304ad97591070384ec4b28021aa0", + "module": "igla-coder-kill-rule", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T09:29:20Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:d0421059df14fa62c1e3720a2e9d8dc732b94e063f96a8e147778c8c70205a12", + "spec_path": "specs/igla/coder/kill_rule.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-preflight.json b/.trinity/seals/coder_igla-coder-preflight.json new file mode 100644 index 0000000000..eb2bed4e1c --- /dev/null +++ b/.trinity/seals/coder_igla-coder-preflight.json @@ -0,0 +1,33 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+6ca19eff2", + "closure": [ + { + "spec": "specs/base/types.t27", + "spec_hash": "sha256:3c2fb2a2edf20e90bc76798fb5d12690b2f60fc0f5bbf2f6052936e22d6e62e2" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:0ef95fe518d5b914f05ed2a4233bccf747d7e82a0ca92a0ca0db6b0b43cd4c68", + "gen_hash_rust": "sha256:98a61660045b1445d0c7e2a3d79983fe440e5867335088ae34132654d33a62bf", + "gen_hash_verilog": "sha256:782c77f2b0bab05f81d64e984a9d7c4382bf255efdab74f006d8d09dd4fac6d8", + "gen_hash_zig": "sha256:b5dba4fbc940be802394201a2492b52bfded48e4eab2dca87fb36aa27c142feb", + "module": "igla-coder-preflight", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T09:29:18Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:fec8fddc4eb79c195b7cfdc6eb540f69c631771de20df6d517ef2ed8a9d1c8c7", + "spec_path": "specs/igla/coder/preflight.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 13, + "total": 13, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/specs/igla/coder/kill_rule.t27 b/specs/igla/coder/kill_rule.t27 new file mode 100644 index 0000000000..e18bf54731 --- /dev/null +++ b/specs/igla/coder/kill_rule.t27 @@ -0,0 +1,234 @@ +// SPDX-License-Identifier: Apache-2.0 +// t27/specs/igla/coder/kill_rule.t27 +// IGLA-Coder kill rule: CONTINUE, WARN or KILL at an eval point of a training run +// phi^2 + 1/phi^2 = 3 | TRINITY +// +// Why this exists. See preflight.t27: the kernels stay Python, the decisions are +// .t27. A run that has diverged or is stuck at the initial loss burns GPU hours +// until the queue timeout; a rule that stops it at the next eval point saves an +// expected $8-15 on a 500M run (2026-10-18 study). +// +// The rule is deliberately lax. EXP-025 (hslm-experiment-ledger): thresholds tuned +// too tight killed 72/72 runs of a wave and nobody noticed until the kills were +// counted instead of the results. So: +// * the first eval only warns for a threshold breach (it never kills); +// * below MIN_KILL_TOKENS no threshold applies at all (warm-up and the 60-step +// smoke run sit far above any curve); +// * the loss curve bound is SLACK x the reference curve; +// * a test counts the kills on a healthy trace and asserts zero. +// A non-finite number is not a threshold: it kills at any eval, first included. +// +// Reference curve: the 100m ternary run reached 0.4722 bits per byte at 10B tokens +// (research/DECOMPOSED_ROADMAP_2026.md); its 2.5B-token ladder run reached 0.5248. +// Between them bpb ~ T^-a with a = 0.076; this spec uses 5/64 = 0.078125, which +// needs only square roots (sqrt six times is the 64th root) and lands at 0.5262 on +// the 2.5B point (0.3 % high). The curve describes fully decayed runs; a WSD run in +// its stable phase sits higher, which is why SLACK is 2.5 and not 1.1. +// +// Calibration data, all real (igla-coder-gpu results/report_2026-09-24.md and the +// Hugging Face summary.json of the 10B pair): ladder endpoints 0.8901 / 0.7460 / +// 0.6093 / 0.5248 / 0.4722 for 13m..100m, the 25m ternary LR sweep (0.7460 healthy, +// 0.8170 at x2, 1.6257 at x4 = a run that diverged), the fp100m final 0.4217, and +// the train.py fine-tune log c_infer/t27_tuned/log.jsonl. The per-eval trace of the +// 10B pair did not survive (runs/ is not committed): the "healthy trace" test below +// uses an assumed plateau factor of 1.3 over the curve, which is stated, not measured. +// +// Verdict codes: 0 CONTINUE, 1 WARN (a threshold breach on the first eval), 2 KILL. +// Reason codes: 0 none, 1 non-finite, 2 grad_norm spike, 3 val_bpb above the curve. + +module igla-coder-kill-rule; +use base::types; + +// ============================================================================ +// 1. Codes and constants +// ============================================================================ + +pub const CONTINUE : i32 = 0; +pub const WARN : i32 = 1; +pub const KILL : i32 = 2; + +pub const REASON_NONE : i32 = 0; +pub const REASON_NONFINITE: i32 = 1; +pub const REASON_GRAD : i32 = 2; +pub const REASON_BPB : i32 = 3; + +// Anchor: 100m ternary at 10B tokens. +pub const BPB_AT_10B : f64 = 0.4722; +pub const TOKENS_AT_10B : f64 = 10000000000.0; +// Healthy grad norms: 1.04 .. 0.05 (smoke) and 0.5 .. 0.7 (fine-tune); the clip is 1.0. +pub const GRAD_SPIKE : f64 = 100.0; +pub const SLACK : f64 = 2.5; +// 1000 steps of the 524288-token batch: well past the 381-step warm-up. +pub const MIN_KILL_TOKENS : f64 = 500000000.0; + +// ============================================================================ +// 2. The reference curve +// ============================================================================ + +// NaN is the one value not equal to itself; inf - inf is NaN +fn is_finite(x: f64) -> bool { + return x == x and (x - x) == (x - x); +} + +// a / b at run time, where IEEE gives NaN for 0 / 0 and inf for 1 / 0 +fn ratio(a: f64, b: f64) -> f64 { + return a / b; +} + +// x^(5/64): the 64th root by six square roots, then the fifth power. +fn pow_5_64(x: f64) -> f64 { + const r = sqrt(sqrt(sqrt(sqrt(sqrt(sqrt(x)))))); + return r * r * r * r * r; +} + +// Fully decayed 100m ternary bits per byte after `tokens` tokens. +pub fn curve_bpb(tokens: f64) -> f64 { + return BPB_AT_10B * pow_5_64(TOKENS_AT_10B / tokens); +} + +// The most val_bpb a run may show at `tokens` before it counts as off the curve. +pub fn bpb_bound(tokens: f64) -> f64 { + return SLACK * curve_bpb(tokens); +} + +// ============================================================================ +// 3. The decision +// ============================================================================ + +pub fn kill_reason(step: i64, batch_tokens: i64, loss: f64, grad_norm: f64, val_bpb: f64) -> i32 { + if (!is_finite(loss) or !is_finite(grad_norm) or !is_finite(val_bpb)) { + return REASON_NONFINITE; + } + const tokens : f64 = (step as f64) * (batch_tokens as f64); + if (!(tokens >= MIN_KILL_TOKENS)) { + return REASON_NONE; + } + if (grad_norm > GRAD_SPIKE) { + return REASON_GRAD; + } + if (val_bpb > bpb_bound(tokens)) { + return REASON_BPB; + } + return REASON_NONE; +} + +// eval_idx counts the evals of this run, first one is 1. +pub fn verdict(step: i64, batch_tokens: i64, eval_idx: i32, loss: f64, grad_norm: f64, val_bpb: f64) -> i32 { + const why = kill_reason(step, batch_tokens, loss, grad_norm, val_bpb); + if (why == REASON_NONE) { + return CONTINUE; + } + if (why == REASON_NONFINITE) { + return KILL; + } + if (eval_idx <= 1) { + return WARN; + } + return KILL; +} + +// ============================================================================ +// 4. Tests +// ============================================================================ + +// The curve hits its anchors: exactly 0.4722 at 10B, 0.5262 at 2.5B (real: 0.5248). +test curve_anchors + given at_10b = curve_bpb(10000000000.0) + when at_2_5b = curve_bpb(2500000000.0) + then at_10b > 0.472199 and at_10b < 0.472201 and at_2_5b > 0.5248 and at_2_5b < 0.5300 + +// The bound at the first kill-eligible points, 100m pair evals at 1B, 2B tokens. +test bound_values + given b1 = bpb_bound(1000000000.0) + when b2 = bpb_bound(2000000000.0) + then b1 > 1.38 and b1 < 1.44 and b2 > 1.31 and b2 < 1.37 + +// ---- negative controls: healthy runs are never killed ------------------------ + +// The real finals of the 10B pair, as the last eval (step 19073, eval 10 of 10). +test healthy_finals_continue + given tern = verdict(19073, 524288, 10, 1.2718, 0.5, 0.47219) + when fp = verdict(19073, 524288, 10, 1.1354, 0.5, 0.42166) + then tern == 0 and fp == 0 + +// The real ladder endpoints (ternary arm), each at its own token count, eval 3: +// 25m 0.5B 0.7460, 52m 1B 0.6093, 100m 2.5B 0.5248. 13m (0.25B) is below the gate. +test healthy_ladder_continue + given m25 = verdict(1908, 262144, 3, 1.4, 0.6, 0.7460) + when m52 = verdict(1907, 524288, 3, 1.2, 0.6, 0.6093) + then m25 == 0 and m52 == 0 and verdict(4768, 524288, 3, 1.1, 0.6, 0.5248) == 0 and verdict(954, 262144, 3, 1.6, 0.6, 0.8901) == 0 + +// The LR sweep runs that were healthy at 25m / 0.5B: x0.25 .. x2. +test healthy_lr_sweep_continue + given a = verdict(1908, 262144, 2, 1.4, 0.6, 0.7623) + when b = verdict(1908, 262144, 2, 1.4, 0.6, 0.7549) + then a == 0 and b == 0 and verdict(1908, 262144, 2, 1.5, 0.6, 0.8170) == 0 + +// The real train.py fine-tune log (c_infer/t27_tuned/log.jsonl): five eval records at +// steps 84, 168, 252, 336, 337 of a 65536-token batch, grad_norm 0.5 .. 0.7. Far below +// MIN_KILL_TOKENS, so every one continues. +test healthy_finetune_log_continues + given a = verdict(84, 65536, 1, 1.3949, 0.72, 0.7558) + when b = verdict(168, 65536, 2, 1.4230, 0.58, 0.7710) + then a == 0 and b == 0 and verdict(252, 65536, 3, 1.2376, 0.49, 0.6706) == 0 and verdict(336, 65536, 4, 1.1276, 0.68, 0.6110) == 0 and verdict(337, 65536, 5, 1.1268, 0.68, 0.6105) == 0 + +// The 60-step smoke run of the 100m ternary model (real: loss 10.38, grad_norm 0.05, +// an untrained model at bpb ~3.85) evals every 10 steps and must never be killed: +// it stops by its own max_steps (exit 3). +test smoke_run_is_not_killed + given a = verdict(60, 524288, 6, 10.3811, 0.05, 3.85) + when b = verdict(20, 524288, 2, 10.5254, 1.04, 3.9) + then a == 0 and b == 0 + +// A healthy-shaped trace at an ASSUMED plateau factor of 1.3 over the curve (a WSD run +// in its stable phase sits above a decayed one): ten evals of 1B tokens, zero kills. +// EXP-025: count the kills on a healthy run. The 1.3 is not measured. +fn healthy_kills() -> i32 { + var k : i32 = 1; + var kills : i32 = 0; + while (k <= 10) { + const step : i64 = (k as i64) * 1907; + const bpb : f64 = 1.3 * curve_bpb((step as f64) * 524288.0); + if (verdict(step, 524288, k, 3.0, 0.5, bpb) == KILL) { + kills = kills + 1; + } + k = k + 1; + } + return kills; +} + +test healthy_trace_has_no_kills + given kills = healthy_kills() + then kills == 0 + +// ---- the runs it must stop --------------------------------------------------- + +// The 25m LR x4 run that diverged: 1.6257 at 0.5B tokens. First eval warns, second kills. +test lr_x4_run_is_killed + given first = verdict(1908, 262144, 1, 3.0, 0.9, 1.6257) + when second = verdict(1908, 262144, 2, 3.0, 0.9, 1.6257) + then first == 1 and second == 2 and kill_reason(1908, 262144, 3.0, 0.9, 1.6257) == 3 + +// Stuck at the initial loss: real init is loss 10.4, bpb 3.85. At 2B tokens. +test stuck_loss_run_is_killed + given a = verdict(3815, 524288, 2, 10.4, 0.05, 3.85) + when b = verdict(3815, 524288, 1, 10.4, 0.05, 3.85) + then a == 2 and b == 1 + +// A NaN loss kills even on the first eval, at any token count (not a threshold). +test nan_loss_is_killed_at_once + given a = verdict(100, 524288, 1, ratio(0.0, 0.0), 0.5, 0.9) + when b = verdict(3815, 524288, 2, 2.0, ratio(0.0, 0.0), 0.9) + then a == 2 and b == 2 and verdict(3815, 524288, 2, 2.0, 0.5, ratio(1.0, 0.0)) == 2 and kill_reason(100, 524288, ratio(0.0, 0.0), 0.5, 0.9) == 1 + +// A grad_norm spike: healthy is <= 1.04, the rule fires above 100. +test grad_spike_is_killed + given a = verdict(3815, 524288, 3, 2.0, 400.0, 0.9) + when b = verdict(3815, 524288, 1, 2.0, 400.0, 0.9) + then a == 2 and b == 1 and kill_reason(3815, 524288, 2.0, 400.0, 0.9) == 2 and verdict(3815, 524288, 3, 2.0, 99.0, 0.9) == 0 + +invariant kill_slack_is_lax + assert SLACK >= 2.0 and GRAD_SPIKE >= 10.0 and MIN_KILL_TOKENS >= 500000000.0 + +invariant kill_codes_are_distinct + assert CONTINUE == 0 and WARN != KILL and KILL == 2 and REASON_GRAD != REASON_BPB diff --git a/specs/igla/coder/preflight.t27 b/specs/igla/coder/preflight.t27 new file mode 100644 index 0000000000..590725afdf --- /dev/null +++ b/specs/igla/coder/preflight.t27 @@ -0,0 +1,202 @@ +// SPDX-License-Identifier: Apache-2.0 +// t27/specs/igla/coder/preflight.t27 +// IGLA-Coder pre-flight: decide GO or REFUSE before a training run is launched +// phi^2 + 1/phi^2 = 3 | TRINITY +// +// Why this exists. The training kernels (PyTorch) stay Python because t27c has no +// GPU backend, but the decisions around a run -- launch, kill, resume -- are plain +// logic and live in .t27. A 2026-10-18 read-only study of the igla-coder-gpu +// pipeline ranked two rules as the real savings on a 500M run: a pre-flight check +// (up to $80 insured) and a kill rule (kill_rule.t27, $8-15 expected). +// +// What it checks, in this order (first failure wins, so the code is stable): +// 6 input is not a usable number (non-finite, zero or negative where it must not be) +// 3 batch_tokens is not a multiple of micro * seq_len (train.py: seqs % micro) +// 4 d_model is not a multiple of n_head +// 5 n_head is not a multiple of n_kv_head +// 1 the run would reach the queue timeout (runq.py timeout_h, default 24) +// 2 the run would cost more than the budget cap +// 0 is GO. +// +// The speed comes from the 60-step smoke run (queues.smoke). A smoke run is a +// little faster than the full run, so the planned speed is derated: the real +// tern100m pair on an RTX 4090 ran 19.74 h against 19.49 h predicted from the +// smoke speed (1.3 % slower); SPEED_DERATE = 0.95 leaves room for that and for +// the eval passes. +// +// The python glue calls preflight() and prints the code; it holds no logic. + +module igla-coder-preflight; +use base::types; + +// ============================================================================ +// 1. Codes and constants +// ============================================================================ + +pub const GO : i32 = 0; +pub const REFUSE_TIMEOUT : i32 = 1; +pub const REFUSE_CAP : i32 = 2; +pub const REFUSE_BATCH : i32 = 3; +pub const REFUSE_HEADS : i32 = 4; +pub const REFUSE_KV_HEADS : i32 = 5; +pub const REFUSE_INPUT : i32 = 6; + +// Planned speed is this fraction of the smoke-run speed. +pub const SPEED_DERATE : f64 = 0.95; +pub const SECONDS_PER_HOUR: f64 = 3600.0; + +// ============================================================================ +// 2. Helpers +// ============================================================================ + +// NaN is the one value not equal to itself; inf - inf is NaN +fn is_finite(x: f64) -> bool { + return x == x and (x - x) == (x - x); +} + +// a / b at run time, where IEEE gives NaN for 0 / 0 and inf for 1 / 0 +fn ratio(a: f64, b: f64) -> f64 { + return a / b; +} + +// Wall-clock hours for `tokens` at the smoke speed tok_s, derated. +pub fn planned_hours(tokens: f64, tok_s: f64) -> f64 { + return tokens / (tok_s * SPEED_DERATE) / SECONDS_PER_HOUR; +} + +// Dollars for those hours at price_h dollars per hour. +pub fn planned_cost(tokens: f64, tok_s: f64, price_h: f64) -> f64 { + return planned_hours(tokens, tok_s) * price_h; +} + +fn inputs_ok(tokens: f64, tok_s: f64, timeout_h: f64, price_h: f64, cap_usd: f64, + micro: i64, seq_len: i64, n_head: i64, n_kv_head: i64) -> bool { + if (!is_finite(tokens) or !is_finite(tok_s) or !is_finite(timeout_h) or !is_finite(price_h) or !is_finite(cap_usd)) { + return false; + } + if (!(tokens > 0.0) or !(tok_s > 0.0) or !(timeout_h > 0.0) or !(cap_usd > 0.0) or price_h < 0.0) { + return false; + } + return micro > 0 and seq_len > 0 and n_head > 0 and n_kv_head > 0; +} + +// ============================================================================ +// 3. The decision +// ============================================================================ + +pub fn preflight(tokens: f64, tok_s: f64, timeout_h: f64, price_h: f64, cap_usd: f64, + batch_tokens: i64, micro: i64, seq_len: i64, + d_model: i64, n_head: i64, n_kv_head: i64) -> i32 { + if (!inputs_ok(tokens, tok_s, timeout_h, price_h, cap_usd, micro, seq_len, n_head, n_kv_head)) { + return REFUSE_INPUT; + } + if (batch_tokens <= 0 or batch_tokens % (micro * seq_len) != 0) { + return REFUSE_BATCH; + } + if (d_model <= 0 or d_model % n_head != 0) { + return REFUSE_HEADS; + } + if (n_head % n_kv_head != 0) { + return REFUSE_KV_HEADS; + } + // A run that ends exactly at the timeout is killed by it: refuse on >=. + if (planned_hours(tokens, tok_s) >= timeout_h) { + return REFUSE_TIMEOUT; + } + if (planned_cost(tokens, tok_s, price_h) > cap_usd) { + return REFUSE_CAP; + } + return GO; +} + +// The 100m ternary shape of train.py / model.py, for the tests: +// seq 2048, batch 524288, micro 64, d_model 768, 12 heads, 4 kv heads. +fn tern100m(tokens: f64, tok_s: f64, timeout_h: f64, price_h: f64, cap_usd: f64) -> i32 { + return preflight(tokens, tok_s, timeout_h, price_h, cap_usd, 524288, 64, 2048, 768, 12, 4); +} + +// ============================================================================ +// 4. Tests -- real numbers from igla-coder-gpu README.md and results/ +// ============================================================================ + +// tern100m, 10B tokens (9,999,745,024 as trained), H100 SXM 457,172 tok/s, $3.49/h: +// 6.40 h derated, $22.3. The queue allows 24 h, the budget 50 USD. +test go_tern100m_h100 + given code = tern100m(9999745024.0, 457172.0, 24.0, 3.49, 50.0) + when hours = planned_hours(9999745024.0, 457172.0) + then code == 0 and hours > 6.3 and hours < 6.5 and planned_cost(9999745024.0, 457172.0, 3.49) < 23.0 + +// The same run on an RTX 4090 at 142,550 tok/s, $0.74/h: 20.5 h predicted. It really +// ran 19.74 h (results/tern100m_pair/summary.json), so the derate is conservative. +test go_tern100m_rtx4090_prediction_covers_the_real_run + given code = tern100m(9999745024.0, 142550.0, 24.0, 0.74, 50.0) + when hours = planned_hours(9999745024.0, 142550.0) + then code == 0 and hours > 19.74 and hours < 21.0 + +// A 500M-class plan: the 100m speed divided by the 5x flops. The 500m rate is +// scaled, not measured. 32 h does not fit the 24 h queue timeout. +test refuse_500m_class_plan_hits_the_timeout + given code = tern100m(9999745024.0, 91434.0, 24.0, 3.49, 200.0) + when hours = planned_hours(9999745024.0, 91434.0) + then code == 1 and hours > 31.0 and hours < 33.0 + +// With a 36 h timeout the same plan fits the clock but costs about 112 USD, over an +// 80 USD cap. +test refuse_500m_class_plan_hits_the_cap + given code = tern100m(9999745024.0, 91434.0, 36.0, 3.49, 80.0) + when cost = planned_cost(9999745024.0, 91434.0, 3.49) + then code == 2 and cost > 110.0 and cost < 114.0 + +// Timeout is checked before the cap, so a run over both reports the timeout. +test refuse_timeout_wins_over_cap + given code = tern100m(9999745024.0, 91434.0, 24.0, 3.49, 10.0) + then code == 1 + +// The 4090 run under a 15 USD cap: 20.5 h * 0.74 = 15.2 USD, refused on the cap only. +test refuse_cap_alone + given code = tern100m(9999745024.0, 142550.0, 24.0, 0.74, 15.0) + then code == 2 + +// Equal to the cap is allowed; equal to the timeout is not. +test boundaries + given at_cap = tern100m(9999745024.0, 142550.0, 24.0, 0.74, 15.2) + when at_timeout = tern100m(9999745024.0, 142550.0, 20.511, 0.74, 50.0) + then at_cap != 2 and at_timeout == 1 + +// Shape checks. 100m: batch 524288 = 256 sequences of 2048, micro 64 divides it. +test shape_batch_not_a_multiple + given a = preflight(9999745024.0, 457172.0, 24.0, 3.49, 50.0, 500000, 64, 2048, 768, 12, 4) + when b = preflight(9999745024.0, 457172.0, 24.0, 3.49, 50.0, 524288, 96, 2048, 768, 12, 4) + then a == 3 and b == 3 + +test shape_d_model_not_a_multiple_of_heads + given code = preflight(9999745024.0, 457172.0, 24.0, 3.49, 50.0, 524288, 64, 2048, 770, 12, 4) + then code == 4 + +test shape_heads_not_a_multiple_of_kv_heads + given code = preflight(9999745024.0, 457172.0, 24.0, 3.49, 50.0, 524288, 64, 2048, 768, 12, 5) + then code == 5 + +// The other real shapes of model.py: 25m (384, 6 heads, 2 kv) at batch 262144, micro 64; +// 13m (256, 4, 2) and 52m (512, 8, 4) at the 524288 batch. +test go_the_other_ladder_shapes + given m25 = preflight(500000000.0, 1425322.0, 24.0, 3.49, 50.0, 262144, 64, 2048, 384, 6, 2) + when m13 = preflight(250000000.0, 1425322.0, 24.0, 3.49, 50.0, 524288, 64, 2048, 256, 4, 2) + then m25 == 0 and m13 == 0 and preflight(1000000000.0, 1000000.0, 24.0, 3.49, 50.0, 524288, 64, 2048, 512, 8, 4) == 0 + +// Garbage in is refused, not computed: a zero speed would divide by zero. +test refuse_unusable_inputs + given zero_speed = tern100m(9999745024.0, 0.0, 24.0, 3.49, 50.0) + when nan_speed = tern100m(9999745024.0, ratio(0.0, 0.0), 24.0, 3.49, 50.0) + then zero_speed == 6 and nan_speed == 6 and tern100m(9999745024.0, ratio(1.0, 0.0), 24.0, 3.49, 50.0) == 6 and tern100m(0.0, 457172.0, 24.0, 3.49, 50.0) == 6 and tern100m(9999745024.0, 457172.0, 24.0, 3.49, 0.0) == 6 + +// A zero head count must be refused before it can divide. +test refuse_zero_heads + given code = preflight(9999745024.0, 457172.0, 24.0, 3.49, 50.0, 524288, 64, 2048, 768, 0, 4) + then code == 6 + +invariant preflight_derate_is_a_fraction + assert SPEED_DERATE > 0.0 and SPEED_DERATE <= 1.0 + +invariant preflight_codes_are_distinct + assert GO == 0 and REFUSE_TIMEOUT != REFUSE_CAP and REFUSE_BATCH != REFUSE_HEADS and REFUSE_HEADS != REFUSE_KV_HEADS and REFUSE_INPUT == 6