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 counter is the smallest possible domain in dafny-replay. It uses a single integer as its model, enforces one invariant (m >= 0), and plugs directly into the Replay kernel. Start here when you want to understand the full pipeline—Dafny domain, compiled JavaScript, and React wiring—before tackling a more complex domain.

​
Domain model

The counter domain lives in counter/CounterDomain.dfy. The model type is just int, the action datatype has two constructors, and the invariant requires non-negativity. 
module CounterDomain refines Domain {
  type Model = int

  datatype Action = Inc | Dec

  predicate Inv(m: Model) {
    m >= 0
  }

  function Init(): Model {
    0
  }

  function Apply(m: Model, a: Action): Model {
    match a
    case Inc => m + 1
    case Dec => m - 1
  }

  function Normalize(m: Model): Model {
    if m < 0 then 0 else m
  }

  lemma InitSatisfiesInv()
    ensures Inv(Init())
  {}

  lemma StepPreservesInv(m: Model, a: Action)
    ensures Inv(Normalize(Apply(m, a)))
  {}
}

​
Key invariant: non-negativity

The invariant m >= 0 prevents the counter from going negative. Because Dec can produce -1 when m is 0, the domain includes a Normalize function that clamps any negative result back to 0. The proof obligation is: 
Inv(m) ⇒ Inv(Normalize(Apply(m, a)))
Both StepPreservesInv lemmas discharge automatically—Dafny verifies them without manual proof steps. Together with InitSatisfiesInv, these two lemmas are the only proofs you owe to the Replay kernel.

​
How Normalize clamps to zero

Normalize is the hook that lets you repair a model after Apply produces an out-of-invariant intermediate state. For the counter, Apply(0, Dec) produces -1, which violates Inv. Normalize replaces any negative value with 0, restoring the invariant before the kernel stores the new state.
Normalize is applied after every Apply call inside the kernel. If your domain transitions are already total and always produce valid states, Normalize can be the identity function—as it is in the Kanban domain.

​
AppCore and the kernel

After the domain, CounterDomain.dfy defines a thin AppCore module that exports the React-facing API: 
module AppCore {
  import K = CounterKernel
  import D = CounterDomain

  function Init(): K.History { K.InitHistory() }
  function Inc(): D.Action { D.Inc }
  function Dec(): D.Action { D.Dec }

  function Dispatch(h: K.History, a: D.Action): K.History
    requires K.HistInv(h) { K.Do(h, a) }
  function Undo(h: K.History): K.History { K.Undo(h) }
  function Redo(h: K.History): K.History { K.Redo(h) }

  function Present(h: K.History): D.Model { h.present }
  function CanUndo(h: K.History): bool { |h.past| > 0 }
  function CanRedo(h: K.History): bool { |h.future| > 0 }
}
The Replay kernel proves once that Do, Undo, and Redo all preserve Inv on the present state. The counter domain only has to discharge the two per-domain obligations.

​
Running the app

cd counter
npm install
npm run dev
The dev server starts at http://localhost:5173. The UI renders the current count with increment, decrement, undo, and redo buttons. Clicking decrement at zero clamps back to zero—the invariant is preserved by construction.

Replay kernel

The generic kernel that powers undo/redo and proves invariant preservation across all replay operations.

Domain obligations

The two lemmas every domain must prove to plug into a kernel.

Build docs developers (and LLMs) love

Get started for freeTalk to us