Invariant Prover

A step-through proof viewer for loop invariants. The caller supplies a block of code, an ordered array of states (one snapshot per iteration), and the component renders the code with the active line highlighted, a panel of named variables for the current state, the state's narration, and one or more invariant banners that flip between holds, breaks, and neutral per step.

Pure layout / playback primitive — it does not run an algorithm, score, or grade. The caller authors the states; the component renders them. Drives the canonical "prove the invariant" lesson (binary search, two-pointer, sliding-window monotonicity, partition correctness) and any side-by-side "what-the-code-does vs what-stays-true" narration.

Binary search invariants

1function binarySearch(arr, target) {

2 let lo = 0, hi = arr.length - 1;

3 while (lo <= hi) {

4 const mid = Math.floor((lo + hi) / 2);

5 if (arr[mid] === target) return mid;

6 if (arr[mid] < target) lo = mid + 1;

7 else hi = mid - 1;

8 }

9 return -1;

10}

lo=0hi=6mid=3arr[mid]=7target=9

arr[3] is 7, less than 9 — move lo to 4.

target is in arr[lo..hi]

search space shrinks each iteration

1 / 3

Customize

Highlight

tone1

hide controls

Installation

npx shadcn@latest add https://craftbits.dev/r/invariant-prover.json

Usage

import { InvariantProver, type InvariantProverState } from "@craft-bits/core";
 
const states: InvariantProverState[] = [
  {
    variables: [
      { name: "lo", value: "0" },
      { name: "hi", value: "6" },
      { name: "mid", value: "3" },
    ],
    description: "arr[3] is less than target — move lo.",
    activeLine: 6,
    invariants: [
      { text: "target is in arr[lo..hi]", status: "holds" },
    ],
  },
];
 
<InvariantProver code={code} states={states} />

Controlled — the parent owns the step and can drive it from a prediction gate or an autoplay timer:

const [step, setStep] = useState(0);
 
<InvariantProver
  code={code}
  states={states}
  step={step}
  onStepChange={setStep}
/>

Hide the built-in prev / next controls when the step is driven entirely from outside:

<InvariantProver code={code} states={states} step={step} hideControls />

Per-step invariant verdicts let the same banner change verdict as the proof advances:

const states: InvariantProverState[] = [
  { variables: vars1, invariants: [{ text: "P", status: "holds" }] },
  { variables: vars2, invariants: [{ text: "P", status: "holds" }] },
  { variables: vars3, invariants: [{ text: "P", status: "breaks" }] },
];

Understanding the component

Pure state replay. Each entry in states describes one snapshot — variables, narration, active line, optional per-step invariant verdicts. The component clamps step to [0, states.length - 1] and renders that snapshot. The same (code, states, step) triple always produces the same view.
Controlled and uncontrolled step. Pair step with onStepChange for Radix-style control, or pass defaultStep and let the component own its step. Built-in prev / next chrome can be hidden when a parent drives the step from outside.
Per-step invariant verdicts. Each state may carry its own invariants array. When a state omits invariants, the component falls back to the top-level invariants prop — letting the caller declare a stable banner list and flip verdicts step by step.
Active-line highlight. The active line is painted with an accent-tinted background and a 3-px inset left border in the current tone. Line numbers are dimmed except for the active line, which adopts the tone colour.
State panel. Variables render as name = value pairs in a single wrapping row. Tabular numerals keep digits aligned as values change, and the panel re-keys on step so a soft cross-fade marks the change without a layout jump.
Invariant banners. Each banner shows a check (holds), cross (breaks), or bullet (neutral) glyph next to the proposition. Banners use semantic tone colour and add a 3-px left rule that matches the glyph, so status reads at a glance.
Step dots. The dot strip carries each step's "any-banner-broke" verdict — dots whose state contains a breaking invariant render in the error tone, so the timeline visually announces where the proof falls apart.
Hit targets. Step dots and prev / next buttons all clear the 44 by 44 px WCAG 2.5.8 floor — the visible 10-px dot sits inside a 44-px transparent hit pad.
Reduced motion. State cross-fades, banner shake / pulse, line highlight transitions, and dot scale all collapse to instant under prefers-reduced-motion: reduce. The proof still advances; only the motion drops.

Props

Prop	Type	Default	Description
`code`	`string`	required	Source code rendered with line numbers and active-line highlight.
`states`	`readonly InvariantProverState[]`	required	Ordered proof states; step `i` renders `states[i]`.
`invariants`	`readonly InvariantProverInvariant[]`	—	Default banner set used when a state omits its own `invariants`.
`step`	`number`	—	Controlled current step. Pair with `onStepChange`.
`defaultStep`	`number`	`0`	Uncontrolled initial step.
`onStepChange`	`(next: number) => void`	—	Fires when the active step changes.
`tone`	`"default" \| "accent" \| "success" \| "warning" \| "error"`	`"accent"`	Highlight palette for the active line and holding invariants.
`title`	`ReactNode`	—	Optional title rendered above the code panel.
`prevLabel`	`string`	`"Prev"`	Label for the previous-step button.
`nextLabel`	`string`	`"Next"`	Label for the next-step button.
`hideControls`	`boolean`	`false`	Hide the built-in prev / next chrome.
`transition`	`Transition`	`SPRINGS.smooth`	Override transitions. Reduced-motion users snap regardless.
`className`	`string`	—	Merged onto the root via `cn()`.

Accessibility

A visually-hidden aria-live="polite" region narrates the current step, variables, and description so screen readers stay current as the proof advances.
The root carries aria-roledescription="loop invariant proof" plus data-state, data-tone, and data-status attributes so assistive tooling and consumer styles can hook into the proof's overall verdict.
Each step dot is a real <button> with an explicit aria-label and an aria-current="step" flag on the active one. The visible dot is 10 by 10 px; the hit pad expands to 44 by 44 px to satisfy WCAG 2.5.8 AAA.
Each invariant banner exposes data-status (holds / breaks / neutral) so styles can react to verdict changes without relying on tone hue alone. The glyph (check / cross / bullet) is paired with a 3-px left rule and a tinted background — verdict is never communicated by colour alone.
Prev / next buttons render at 44 by 44 px minimum, disable themselves at the ends, and respond to keyboard Enter and Space. Arrow-left / arrow-right keys on the root advance the step too.
Motion respects prefers-reduced-motion: reduce — state cross-fades, banner shake / pulse, line highlight transitions, and dot scale collapse to instant. The proof still advances; only the motion drops.

Credits

Extracted from: algoflashcards (src/lessons/primitives/construction/InvariantProver.tsx). The source was a 2,000-line three-act game (Encounter → Discover → Apply) that drove a buggy binary search to infinite-loop, then taught the student to build / refine / apply a loop invariant through prediction gates, inline blank fills, line identification, and a bug fix — wired to a reducer with 18 phases, per-step audio cues, a hardcoded generateBuggyBinarySearchTrace simulator, and a built-in scoring formula. The library extract drops the game, the reducer, the scoring, the audio, and the simulator. What remains is the proof spine: a code panel, a per-state variable row, narration, and a stack of invariant banners whose verdict flips per step. Consumers compose any narrative on top.