From 8d0267fc06c25180deb280ea26bbabec769a17ae Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 05:06:39 +0200 Subject: [PATCH] test(explain): cover render_register_panel text and status colour thresholds (Refs #5594) Co-Authored-By: Claude Sonnet 5.5 Agent: aprender-w5382 --- README.md | 4 +- contracts/contracts.nt | 5 ++ contracts/explain-tui-register-panel-v1.yaml | 47 +++++++++++ ...5f0be2f90923120a3027c176ad56723d0d850.json | 6 +- crates/aprender-explain/src/tui/tests.rs | 2 + .../src/tui/tests_register_panel.rs | 83 +++++++++++++++++++ 6 files changed, 142 insertions(+), 5 deletions(-) create mode 100644 contracts/explain-tui-register-panel-v1.yaml create mode 100644 crates/aprender-explain/src/tui/tests_register_panel.rs diff --git a/README.md b/README.md index 027a6b2a7d..191f91b659 100644 --- a/README.md +++ b/README.md @@ -114,7 +114,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **81** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1984** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1985** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **113** CLI commands | `contracts/apr-cli-commands-v1.yaml` §`commands` (parse the list; `apr --help` also lists `help` itself, and `grep -c '^ - name:'` gives 119 — other same-indent `name:` keys exist in the file) | | Book CLI chapters | **114** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **73** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -403,7 +403,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1984 contracts across inference, training, quantization, attention, FFN, +The tree carries 1985 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/contracts.nt b/contracts/contracts.nt index c3ed1fb995..b0a18f7667 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -11730,6 +11730,11 @@ . "contracts/forjar/execution-safety-v1.yaml"^^ . "execution-safety-v1"^^ . + . + . + "contracts/explain-tui-register-panel-v1.yaml"^^ . + "explain-tui-register-panel-v1"^^ . + "pattern"^^ . . . . diff --git a/contracts/explain-tui-register-panel-v1.yaml b/contracts/explain-tui-register-panel-v1.yaml new file mode 100644 index 0000000000..7750dd5f41 --- /dev/null +++ b/contracts/explain-tui-register-panel-v1.yaml @@ -0,0 +1,47 @@ +metadata: + id: C-EXPLAIN-TUI-REGISTER-PANEL + version: 1.0.0 + created: '2026-10-19' + author: PAIML Engineering + kind: pattern + status: ACTIVE_ALGORITHM_LEVEL + description: | + Pins the register panel drawn by the aprender-explain TUI sidebar (#5594): + one line per register class with its limit, a total/occupancy line, and a + status colour that is green below 64 registers, yellow from 64 to 127 and + red from 128. + references: + - 'crates/aprender-explain/src/tui/widgets.rs (render_register_panel)' + +equations: + register_panel_status_colour: + formula: | + colour(total) = green if total < 64, yellow if total < 128, else red + domain: RegisterUsage totals passed through render_sidebar + invariants: + - 'the thresholds are 64 and 128, lower bound inclusive' + +proof_obligations: +- id: ERP-INV-001 + type: invariant + property: register panel text and status colour follow the total register count + formal: 'colour ≡ threshold' + applies_to: register_panel_status_colour + +falsification_tests: +- id: FALSIFY-EXPLAIN-TUI-REGISTER-PANEL-001 + rule: render_register_panel draws exact lines and the threshold colour + prediction: 'totals 63, 64, 127 and 128 give green, yellow, yellow and red borders; the lines show the .f32/.b32/.b64/.pred counts and the Total/occ text' + test: cargo test -p aprender-explain --lib register_panel + if_fails: the TUI misreports register pressure on a kernel + ship_blocking: false + mutation: 'change either < to <=, or print the wrong register field; each must turn RED' + +qa_gate: + id: QA-EXPLAIN-TUI-REGISTER-PANEL-001 + name: Explain TUI register panel gate + description: register panel text and colour thresholds are exact + checks: + - register_panel_status_colour + pass_criteria: FALSIFY-EXPLAIN-TUI-REGISTER-PANEL-001 passes + falsification: Any failure fails the gate diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 6bb276cb32..81cf739988 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,7 +1,7 @@ { - "census_id_set_sha256": "7597b4ad189f534dd58cda55c9b1fe29e6339ddb77fd5f40969b4a028eed8f88", + "census_id_set_sha256": "61a4e41620582ab9708d6cd9a41910e85ba5a7168827134dda645e7c521d0511", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", - "reasoner_git_sha": "461bf9ef1921a8fbea4bc338f21b566ec342a95e", + "reasoner_git_sha": "692cc8a019ddcefbe333c4bcdc4cb2dd3e6864d7", "checkable_n": 87, "result": { "kind": "model", @@ -10,5 +10,5 @@ } }, "pc_reasoner": "fired", - "cpu_ms": 1 + "cpu_ms": 2 } diff --git a/crates/aprender-explain/src/tui/tests.rs b/crates/aprender-explain/src/tui/tests.rs index 0748b87243..80c8c7af74 100644 --- a/crates/aprender-explain/src/tui/tests.rs +++ b/crates/aprender-explain/src/tui/tests.rs @@ -236,3 +236,5 @@ fn f028_sync_scroll_source_asm() { app.handle_key(KeyCode::PageUp); assert_eq!(app.source_scroll, 0, "Should scroll back to top"); } + +include!("tests_register_panel.rs"); diff --git a/crates/aprender-explain/src/tui/tests_register_panel.rs b/crates/aprender-explain/src/tui/tests_register_panel.rs new file mode 100644 index 0000000000..d2a6af66ca --- /dev/null +++ b/crates/aprender-explain/src/tui/tests_register_panel.rs @@ -0,0 +1,83 @@ +// #5594: behavioural tests for widgets::render_register_panel, driven through +// the pub(super) render_sidebar entry point (the panel occupies rows 0..8). +// Included from tests.rs so `super::*` items (TuiApp, sample_report) are in scope. + +fn render_panel_rows(regs: RegisterUsage, occupancy: f32) -> (CellBuffer, Vec) { + let mut report = sample_report(); + report.registers = regs; + report.estimated_occupancy = occupancy; + let app = TuiApp::new(".entry t() { ret; }".to_string(), report); + let mut buffer = CellBuffer::new(44, 30); + { + let mut canvas = DirectTerminalCanvas::new(&mut buffer); + widgets::render_sidebar(&mut canvas, &app, 0.0, 0.0, 44, 30); + } + let rows = (0..8u16) + .map(|y| { + (0..44u16) + .filter_map(|x| buffer.get(x, y).map(|c| c.symbol.to_string())) + .collect::() + }) + .collect(); + (buffer, rows) +} + +fn regs_with_total(f32_regs: u32) -> RegisterUsage { + RegisterUsage { + f32_regs, + ..Default::default() + } +} + +fn border_fg(buffer: &CellBuffer) -> Color { + buffer.get(0, 0).expect("cell (0,0) exists").fg +} + +const PANEL_GREEN: Color = Color { r: 0.3, g: 1.0, b: 0.3, a: 1.0 }; +const PANEL_YELLOW: Color = Color { r: 1.0, g: 1.0, b: 0.3, a: 1.0 }; +const PANEL_RED: Color = Color { r: 1.0, g: 0.3, b: 0.3, a: 1.0 }; + +#[test] +fn register_panel_lines_show_each_register_class() { + let regs = RegisterUsage { + f32_regs: 24, + b32_regs: 18, + b64_regs: 12, + pred_regs: 4, + ..Default::default() + }; + let (_, rows) = render_panel_rows(regs, 0.875); + assert!(rows[0].starts_with("┌─ Registers "), "{}", rows[0]); + assert!(rows[0].trim_end().ends_with('┐'), "{}", rows[0]); + assert!(rows[1].contains(".f32: 24 / 255"), "{}", rows[1]); + assert!(rows[2].contains(".b32: 18 / 255"), "{}", rows[2]); + assert!(rows[3].contains(".b64: 12 / 255"), "{}", rows[3]); + assert!(rows[4].contains(".pred: 4 / 8"), "{}", rows[4]); + assert!(rows[5].contains("Total: 58 -> 88% occ"), "{}", rows[5]); + assert!(rows[7].starts_with('└') && rows[7].trim_end().ends_with('┘'), "{}", rows[7]); +} + +#[test] +fn register_panel_total_below_64_is_green() { + let (buf, _) = render_panel_rows(regs_with_total(63), 0.5); + assert!(color_approx_eq(border_fg(&buf), PANEL_GREEN)); +} + +#[test] +fn register_panel_total_64_is_yellow() { + let (buf, _) = render_panel_rows(regs_with_total(64), 0.5); + assert!(color_approx_eq(border_fg(&buf), PANEL_YELLOW)); +} + +#[test] +fn register_panel_total_127_is_yellow() { + let (buf, _) = render_panel_rows(regs_with_total(127), 0.5); + assert!(color_approx_eq(border_fg(&buf), PANEL_YELLOW)); +} + +#[test] +fn register_panel_total_128_is_red() { + let (buf, rows) = render_panel_rows(regs_with_total(128), 0.25); + assert!(color_approx_eq(border_fg(&buf), PANEL_RED)); + assert!(rows[5].contains("Total: 128 -> 25% occ"), "{}", rows[5]); +}