Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/metareflection/dafny-replay/llms.txt

Use this file to discover all available pages before exploring further.

The Replay kernel is the foundational building block of dafny-replay. It maintains a History = { past, present, future } data structure and provides Do, Undo, Redo, Preview, and CommitFrom operations. The kernel proves once — for any plugged-in domain — that every operation preserves the domain invariant on the present state and on every state stored in the history.

​
Module hierarchy

The architecture flows from specification down to the React-facing API: 
Abstract Domain (spec: Model, Action, Inv, Apply, Normalize)
        ↓ refined by
Concrete Domain (proves InitSatisfiesInv and StepPreservesInv)
        ↓ plugged into
Replay Kernel (generic, proved once for all domains)
        ↓ compiled to JS
AppCore (React-facing API: Dispatch, Undo, Redo)
Each layer has a single responsibility. The kernel never contains domain logic; the domain never contains kernel logic.

​
The History data structure

datatype History =
  History(past: seq<D.Model>, present: D.Model, future: seq<D.Model>)
  • past — sequence of states before the current one (oldest first)
  • present — the live state shown to the user
  • future — states available for redo (cleared on Do)
The invariant HistInv requires that every state in past, present, and future individually satisfies the domain invariant Inv: 
ghost predicate HistInv(h: History) {
  (forall i | 0 <= i < |h.past| :: D.Inv(h.past[i])) &&
  D.Inv(h.present) &&
  (forall j | 0 <= j < |h.future| :: D.Inv(h.future[j]))
}

​
Domain obligations

To use the Replay kernel, a concrete domain must discharge exactly two lemmas: 
lemma InitSatisfiesInv()
  ensures Inv(Init())
The initial model produced by Init() must satisfy Inv. This seeds the induction.
lemma StepPreservesInv(m: Model, a: Action)
  requires Inv(m)
  ensures Inv(Normalize(Apply(m, a)))
Every call to Apply followed by Normalize must produce a model that still satisfies Inv. Normalize gives the domain a hook to canonicalize state (e.g., sort IDs, trim tombstones) before storage.
Once R1 and R2 are proved, no further proofs are required to get correct undo/redo.

​
Kernel API

All operations in the kernel are pure functions — they take a History and return a new History.

​
Do

function Do(h: History, a: D.Action): History
  requires D.Inv(h.present)
{
  History(h.past + [h.present], Step(h.present, a), [])
}
Pushes present onto past, computes the new state, and clears future. A new action always discards the redo branch (linear undo semantics).

​
Undo

function Undo(h: History): History {
  if |h.past| == 0 then h
  else
    var i := |h.past| - 1;
    History(h.past[..i], h.past[i], [h.present] + h.future)
}
Moves present to the front of future, then pops the last element of past into present. No-ops if past is empty.

​
Redo

function Redo(h: History): History {
  if |h.future| == 0 then h
  else
    History(h.past + [h.present], h.future[0], h.future[1..])
}
Moves present to the end of past, then advances to the first element of future.

​
Preview

function Preview(h: History, a: D.Action): History
  requires D.Inv(h.present)
{
  History(h.past, Step(h.present, a), h.future)
}
Applies a to present without recording the current state to past. Useful for live preview during drag operations; the history branches are left intact.

​
CommitFrom

function CommitFrom(h: History, baseline: D.Model): History {
  History(h.past + [baseline], h.present, [])
}
Records baseline (the state at the start of a drag) into past and commits the current present. Pair with Preview to implement drag-and-drop undo: preview during the drag, commit when the user releases.

​
Kernel theorems

These properties are proved once in the generic kernel assuming R1 and R2:
For all reachable histories h (starting from InitHistory() and applying any sequence of Do, Undo, Redo, Preview, or CommitFrom), D.Inv(h.present) holds.
lemma DoPreservesHistInv(h: History, a: D.Action)
  requires HistInv(h)
  ensures  HistInv(Do(h, a))

lemma UndoPreservesHistInv(h: History)
  requires HistInv(h)
  ensures  HistInv(Undo(h))

lemma RedoPreservesHistInv(h: History)
  requires HistInv(h)
  ensures  HistInv(Redo(h))
The kernel also proves structural correctness of the history:
// Undo then Redo returns the original history
lemma UndoRedoRoundTrip(h: History)
  requires |h.past| > 0
  ensures Redo(Undo(h)) == h

// Redo then Undo returns the original history
lemma RedoUndoRoundTrip(h: History)
  requires |h.future| > 0
  ensures Undo(Redo(h)) == h

// Do clears the future (linear undo)
lemma DoHasNoRedoBranch(h: History, a: D.Action)
  requires HistInv(h)
  ensures Redo(Do(h, a)) == Do(h, a)

// Undo at beginning is a no-op
lemma UndoAtBeginningIsNoOp(h: History)
  requires |h.past| == 0
  ensures Undo(h) == h

// Redo at end is a no-op
lemma RedoAtEndIsNoOp(h: History)
  requires |h.future| == 0
  ensures Redo(h) == h

​
Integration boundary (trusted)

The kernel proofs cover the Dafny transition logic. The following are not modeled or proved:
  • JavaScript runtime and Dafny → JS compilation correctness
  • UI wiring, rendering, and React re-render semantics
  • Persistence, serialization, and I/O
Verified transition logic may run inside larger unverified systems. The guarantees apply to the Dafny-generated logic itself, not the surrounding infrastructure.

Authority kernel

Extend replay to client-server with server-authoritative state.

Domain obligations guide

Step-by-step walkthrough of writing R1 and R2 for your domain.

Kanban app

Replay kernel applied to a realistic drag-and-drop board with WIP limits.

Guarantees reference

Precise statement of what is proved, assumed, and trusted.

Build docs developers (and LLMs) love

Get started for freeTalk to us