Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 51 additions & 0 deletions demos/verification_2026-09-12-braille-termination.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
# Braille termination verification - 2026-09-12

This record covers the source and binary built from implementation commit
`62690ca94ea1113eee538c5270123a3b25c5c7b9` on branch
`fix/braille-termination`.

## Build identity

| Field | Value |
| --- | --- |
| UTC capture time | `2026-09-12T05:59:22Z` |
| Working-tree dirty count at build | `0` (`git status --porcelain=v1`) |
| Build command | `cargo build --locked` (exit 0) |
| Binary | `target/debug/grainx` |
| Binary SHA-256 | `a51a95c018cf5b41cb6892a79f9de8672fc2756fa3478a8ea00f2c7bd6a8bcce` |
| Toolchain | `rustc 1.94.1 (e408947bf 2026-03-25)` / `cargo 1.94.1 (29ea6fb6a 2026-03-24)` |

## PTY proof

An owned, uncommitted Python standard-library driver created a fresh PTY,
set its window size, ran the actual binary with
`GRAINX_REFRESH_INTERVAL_MS=100`, parsed the flushed `| Frame: N` suffixes,
sent `q` after five completed frames, and allowed four seconds for graceful
exit. It did not use `demos/capture_tui.py`, TERM, or KILL.

| Size | Duration | Completed frames | Increasing | `q` exit | Signals |
| --- | ---: | --- | --- | ---: | --- |
| `80x24` | 2345 ms | `1, 2, 3, 4, 5` | yes | 0 | none |
| `110x50` | 2344 ms | `1, 2, 3, 4, 5` | yes | 0 | none |

The proof establishes bounded completion and graceful input handling for these
two sizes on this host. It is not a performance or cross-platform claim.

## Command outcomes

All commands used the committed lockfile and passed:

```text
cargo fmt --check exit 0
cargo check --locked --all-targets exit 0
cargo clippy --locked --all-targets -- -D warnings exit 0
cargo test --locked exit 0; 75 passed, 0 failed
cargo bench --locked --no-run exit 0; 3 executables built
cargo +1.88.0 check --locked --all-targets exit 0
```

The rasterizer integration tests execute `braille_grid` and
`AdvancedCanvas::draw_braille_line` inside killable subprocess workers with a
two-second deadline. They cover empty and zero-sized inputs, the explicit
single-point edge policy, integer/fractional/repeated lines, clipping,
non-finite inputs, edge-adjacent rounding, and finite `f64::MAX` crossings.
306 changes: 259 additions & 47 deletions src/rendering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,13 +37,15 @@ impl DashboardLayout {

let cpu_rect = Rect {
x: 0,
y: 1,
// Row 0 holds the header, row 1 the CPU label; the graph's clear
// and braille passes start below both.
y: 2,
width: term_width,
height: cpu_h,
};
let mem_rect = Rect {
x: 0,
y: cpu_h + 2,
y: cpu_rect.y + cpu_h + 1,
width: term_width,
height: mem_h,
};
Expand All @@ -69,13 +71,243 @@ impl DashboardLayout {
}
}

/// Row for the CPU label, kept just above `cpu_rect` so the CPU graph's
/// clear and braille passes can never overwrite it.
pub fn cpu_label_y(&self) -> u16 {
self.cpu_rect.y.saturating_sub(1)
}

/// Row for the memory label, kept just above `mem_rect` so the memory
/// graph's clear and braille passes can never overwrite it.
pub fn memory_label_y(&self) -> u16 {
self.mem_rect.y.saturating_sub(1)
}
}

/// Rasterize a polyline into a braille dot grid.
///
/// `points` use the same coordinates as [`AdvancedCanvas::draw_braille_line`]:
/// x and y are scaled to `cell_width`/`cell_height` terminal cells. The result
/// is indexed `[gx][gy]` and sized `cell_width * 2` by `cell_height * 4`, the
/// number of braille dots per cell.
///
/// Every finite segment is clipped before its endpoints are quantized, so the
/// amount of work is bounded by the viewport no matter how large the inputs
/// are. Non-finite segments are skipped. A single finite point in the inclusive
/// logical viewport is rounded to the nearest dot, with the right and bottom
/// edges clamped to the final dot cell; points outside are skipped.
pub fn braille_grid(points: &[(f64, f64)], cell_width: u16, cell_height: u16) -> Vec<Vec<bool>> {
let grid_width = cell_width as usize * 2;
let grid_height = cell_height as usize * 4;
let mut grid = vec![vec![false; grid_height]; grid_width];
if grid_width == 0 || grid_height == 0 || points.is_empty() {
return grid;
}

if points.len() == 1 {
if let Some((gx, gy)) =
point_cell(points[0], cell_width, cell_height, grid_width, grid_height)
{
grid[gx][gy] = true;
}
return grid;
}

for pair in points.windows(2) {
let (x1, y1) = pair[0];
let (x2, y2) = pair[1];
if let Some(((gx1, gy1), (gx2, gy2))) = clip_to_grid(
x1,
y1,
x2,
y2,
cell_width,
cell_height,
grid_width,
grid_height,
) {
plot_segment(&mut grid, gx1, gy1, gx2, gy2);
}
}
grid
}

fn point_cell(
point: (f64, f64),
cell_width: u16,
cell_height: u16,
grid_width: usize,
grid_height: usize,
) -> Option<(usize, usize)> {
if !point.0.is_finite() || !point.1.is_finite() {
return None;
}
if point.0 < 0.0 || point.1 < 0.0 || point.0 > cell_width as f64 || point.1 > cell_height as f64
{
return None;
}
Some(quantize_point(point, grid_width, grid_height))
}

fn quantize_point(point: (f64, f64), grid_width: usize, grid_height: usize) -> (usize, usize) {
let gx = (point.0 * 2.0).round() as usize;
let gy = (point.1 * 4.0).round() as usize;
(gx.min(grid_width - 1), gy.min(grid_height - 1))
}

/// Clip a segment to the logical canvas and return quantized endpoint cells.
///
/// Boundary intersections are computed from half-differences rather than
/// `end - start`, which remains finite even for `-f64::MAX..f64::MAX`.
#[allow(clippy::too_many_arguments)]
fn clip_to_grid(
x1: f64,
y1: f64,
x2: f64,
y2: f64,
cell_width: u16,
cell_height: u16,
grid_width: usize,
grid_height: usize,
) -> Option<((usize, usize), (usize, usize))> {
if !x1.is_finite() || !y1.is_finite() || !x2.is_finite() || !y2.is_finite() {
return None;
}

let max_x = cell_width as f64;
let max_y = cell_height as f64;
let mut cells = Vec::with_capacity(6);

if inside(x1, y1, max_x, max_y) {
push_unique_cell(
&mut cells,
quantize_point((x1, y1), grid_width, grid_height),
);
}
if inside(x2, y2, max_x, max_y) {
push_unique_cell(
&mut cells,
quantize_point((x2, y2), grid_width, grid_height),
);
}

if x1 != x2 {
for boundary_x in [0.0, max_x] {
if between(boundary_x, x1, x2) {
let y = interpolate_at(x1, x2, boundary_x, y1, y2);
if y.is_finite() && (0.0..=max_y).contains(&y) {
push_unique_cell(
&mut cells,
quantize_point((boundary_x, y), grid_width, grid_height),
);
}
}
}
}
if y1 != y2 {
for boundary_y in [0.0, max_y] {
if between(boundary_y, y1, y2) {
let x = interpolate_at(y1, y2, boundary_y, x1, x2);
if x.is_finite() && (0.0..=max_x).contains(&x) {
push_unique_cell(
&mut cells,
quantize_point((x, boundary_y), grid_width, grid_height),
);
}
}
}
}

match cells.as_slice() {
[] => None,
[cell] => Some((*cell, *cell)),
_ => {
let mut endpoints = (cells[0], cells[1]);
let mut greatest_distance = cell_distance_squared(cells[0], cells[1]);
for (index, &first) in cells.iter().enumerate() {
for &second in &cells[index + 1..] {
let distance = cell_distance_squared(first, second);
if distance > greatest_distance {
endpoints = (first, second);
greatest_distance = distance;
}
}
}
Some(endpoints)
}
}
}

fn inside(x: f64, y: f64, max_x: f64, max_y: f64) -> bool {
(0.0..=max_x).contains(&x) && (0.0..=max_y).contains(&y)
}

fn between(value: f64, first: f64, second: f64) -> bool {
value >= first.min(second) && value <= first.max(second)
}

fn interpolate_at(
axis_start: f64,
axis_end: f64,
axis_value: f64,
other_start: f64,
other_end: f64,
) -> f64 {
let axis_midpoint = axis_start / 2.0 + axis_end / 2.0;
let axis_half_delta = axis_end / 2.0 - axis_start / 2.0;
let other_midpoint = other_start / 2.0 + other_end / 2.0;
let other_half_delta = other_end / 2.0 - other_start / 2.0;

if axis_half_delta == 0.0 {
let ratio = (axis_value - axis_start) / (axis_end - axis_start);
other_start + ratio * (other_end - other_start)
} else {
let centered_parameter = (axis_value - axis_midpoint) / axis_half_delta;
other_midpoint + centered_parameter * other_half_delta
}
}

fn push_unique_cell(cells: &mut Vec<(usize, usize)>, cell: (usize, usize)) {
if !cells.contains(&cell) {
cells.push(cell);
}
}

fn cell_distance_squared(first: (usize, usize), second: (usize, usize)) -> usize {
let dx = first.0.abs_diff(second.0);
let dy = first.1.abs_diff(second.1);
dx * dx + dy * dy
}

/// Integer Bresenham walk between two cells that are already inside the grid.
fn plot_segment(grid: &mut [Vec<bool>], x1: usize, y1: usize, x2: usize, y2: usize) {
let end_x = x2 as isize;
let end_y = y2 as isize;
let mut x = x1 as isize;
let mut y = y1 as isize;
let dx = (end_x - x).abs();
let dy = (end_y - y).abs();
let sx = if x < end_x { 1 } else { -1 };
let sy = if y < end_y { 1 } else { -1 };
let mut err = dx - dy;

loop {
grid[x as usize][y as usize] = true;
if x == end_x && y == end_y {
return;
}
let e2 = 2 * err;
if e2 > -dy {
err -= dy;
x += sx;
}
if e2 < dx {
err += dx;
y += sy;
}
}
}

pub struct AdvancedCanvas {
stdout: io::Stdout,
}
Expand Down Expand Up @@ -105,53 +337,13 @@ impl AdvancedCanvas {
self.stdout.write_all(s.as_bytes())
}

pub fn flush(&mut self) -> io::Result<()> {
self.stdout.flush()
}

/// Draw a braille-based graph line for high-resolution
pub fn draw_braille_line(&mut self, points: &[(f64, f64)], rect: &Rect) -> io::Result<()> {
let braille_width = rect.width * 2;
let braille_height = rect.height * 4;

let mut grid = vec![vec![false; braille_height as usize]; braille_width as usize];

// Map each point to the grid
for i in 0..points.len() - 1 {
// Simple line drawing algorithm (Bresenham's or similar could be used)
let (x1, y1) = points[i];
let (x2, y2) = points[i + 1];

let dx = (x2 - x1).abs();
let dy = (y2 - y1).abs();

let sx = if x1 < x2 { 1.0 } else { -1.0 };
let sy = if y1 < y2 { 1.0 } else { -1.0 };

let mut err = dx - dy;

let mut current_x = x1;
let mut current_y = y1;

loop {
let gx = (current_x / rect.width as f64 * braille_width as f64).round() as usize;
let gy = (current_y / rect.height as f64 * braille_height as f64).round() as usize;

if gx < braille_width as usize && gy < braille_height as usize {
grid[gx][gy] = true;
}

if current_x == x2 && current_y == y2 {
break;
}

let e2 = 2.0 * err;
if e2 > -dy {
err -= dy;
current_x += sx;
}
if e2 < dx {
err += dx;
current_y += sy;
}
}
}
let grid = braille_grid(points, rect.width, rect.height);

for y in 0..rect.height {
for x in 0..rect.width {
Expand Down Expand Up @@ -235,4 +427,24 @@ mod tests {
assert!(layout.network_start_y > layout.net_rect.y);
assert!(layout.proc_start_y > layout.network_start_y);
}

#[test]
fn cpu_label_row_is_between_header_and_graph() {
for (width, height) in [(60, 20), (80, 24), (110, 50), (200, 80)] {
let layout = DashboardLayout::from_terminal_size(width, height);
let label_y = layout.cpu_label_y();
assert!(
label_y >= 1,
"CPU label row {label_y} collides with the header at {width}x{height}"
);
assert!(
label_y < layout.cpu_rect.y,
"CPU label row {label_y} overlaps the CPU graph at {width}x{height}"
);
assert!(
label_y < layout.memory_label_y(),
"CPU and memory label rows collide at {width}x{height}"
);
}
}
}
Loading
Loading