Safety & Correctness Guarantees

FrankenTUI is built on three pillars: a zero-unsafe policy on the hot path, saturating/checked integer arithmetic for every coordinate operation, and formal proof sketches that pin down flicker-free rendering.

Zero Unsafe Code Policy

The render pipeline, runtime, and layout engine each carry an explicit forbiddance of unsafe:

// ftui-render/src/lib.rs
#![forbid(unsafe_code)]
 
// ftui-runtime/src/lib.rs
#![forbid(unsafe_code)]
 
// ftui-layout/src/lib.rs
#![forbid(unsafe_code)]

The entire render pipeline, runtime, and layout engine contain zero unsafe blocks. The compiler rejects any unsafe expression at crate scope, so the guarantee is mechanically enforced rather than audited.

Integer Overflow Protection

All coordinate arithmetic uses saturating or checked operations so that resizing, scrolling, and pane math never wrap silently:

// Cursor positioning (saturating)
let next_x = current_x.saturating_add(width as u16);
 
// Bounds checking (checked)
let Some(target_x) = x.checked_add(offset) else { continue };
 
// Intentional wrapping (PRNG only)
seed.wrapping_mul(6364136223846793005).wrapping_add(1)

The three-form idiom is intentional:

• Saturating for positions and sizes where “clamp to the screen edge” is the desired behavior on overflow.
• Checked for offsets, where overflow usually means a logic error and the right response is to skip the operation.
• Wrapping reserved for pseudorandom number generators and hash mixing, where wrapping is part of the algorithm.

Flicker-Free Proof Sketches

The codebase includes formal proof sketches in no_flicker_proof.rs. The four theorems below are stated as machine-checked invariants: if any test derived from them fails, the theorem is false.

Theorem 1 (Sync Bracket Completeness)

Every byte emitted by Presenter is wrapped in DEC 2026 sync brackets.

Consequence: the terminal never displays a partial frame. The user either sees the previous state or the new state, never an in-progress write.

Theorem 2 (Diff Completeness)

BufferDiff::compute(old, new) produces exactly {(x,y) | old[x,y] ≠ new[x,y]}.

Consequence: the diff is sound and complete — no missed cells (would cause stale pixels on screen) and no spurious cells (would waste bandwidth).

Theorem 3 (Dirty Tracking Soundness)

If any cell in row y was mutated, is_row_dirty(y) == true.

Consequence: the row-skip fast path in the diff is safe. Rows reported as clean truly contain no changes, so skipping them cannot produce stale output.

Theorem 4 (Diff-Dirty Equivalence)

compute() and compute_dirty() produce identical output when dirty invariants hold.

Consequence: the expensive full-scan diff and the cheap dirty-row diff are observationally equivalent. Choosing one over the other is a pure performance decision, not a correctness trade-off.

Proof by Counterexample

Each theorem is paired with a counterexample test:

// Proof by counterexample: if this test fails, the theorem is false
#[test]
fn counterexample_dirty_soundness() {
    let mut buf = Buffer::new(10, 10);
    buf.set(5, 5, Cell::from_char('X'));
    assert!(buf.is_row_dirty(5), "Theorem 3 violated: mutation without dirty flag");
}

If a future refactor loses the invariant, the test fails loudly and the theorem’s consequence (for example, stale rendering after a row-skip) is the observable symptom.

Supporting Invariants

Beyond the four named theorems, the render stack maintains several supporting invariants:

• Cursor-bounded emission. The presenter never emits a cursor move that would place the cursor outside the active buffer region.
• SGR non-leakage. Style state (bold, color, hyperlink) is reset between non-adjacent runs so that an unstyled cell is never rendered with the previous cell’s style. See ADR-002.
• Hyperlink balance. Every OSC 8 open is paired with an OSC 8 close before the present completes, preventing “sticky links” in surrounding terminal output.
• Scissor monotonicity. Push/pop of the scissor stack produces a monotonically decreasing intersection — a child clip never enlarges the parent’s region.
• Opacity stack range. The product of stacked alphas stays in [0.0, 1.0] at all times.
• Grapheme pool reference counting. GraphemeId references into the pool are refcounted; a pool slot is only freed when its refcount reaches zero.

Cleanup Guarantees

Terminal cleanup is guaranteed by RAII, not by try/finally discipline at call sites:

• TerminalSession::Drop restores raw mode, cursor visibility, alt-screen state, and feature flags (mouse, paste, focus, kitty keyboard) in the reverse of their setup order.
• Drop runs on normal exit, early return via ?, and panic unwinding.
• The terminal-mode teardown sequence is exercised by PTY tests that simulate panics (see ADR-003).

One-Writer Rule

Terminals are a shared mutable resource. FrankenTUI enforces that only one writer touches stdout at a time via ownership and routing through TerminalWriter. See ADR-005 and /operations/one-writer-rule.

Without this rule:

• Concurrent cursor moves become undefined.
• Partial escape sequences corrupt styling.
• UI and log lines interleave unpredictably.

Untrusted Output Policy

All log-path and user-content writes are sanitized by default — escape sequences and most C0 controls are stripped. Raw passthrough is explicitly opt-in. See ADR-006.

Testing the Guarantees

The invariants above are tested by three complementary suites:

• Property tests (proptest) exercise random buffers, random mutations, and random styles to look for diff or styling regressions.
• Snapshot tests (insta) lock down byte-exact presenter output for representative frames. BLESS=1 cargo test updates baselines after an intentional change.
• PTY tests drive a real pseudo-terminal, asserting cleanup on both normal exit and panic.

See Also