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.

Every dafny-replay kernel is generic: it works with any domain that satisfies a small set of proof obligations. Before the kernel can guarantee anything — that undo cannot corrupt state, that rejected requests leave the server unchanged, that cards are never duplicated — your domain must prove that its initial state is valid and that every transition preserves validity. Discharging those two obligations is all it takes to unlock the full set of kernel theorems for your domain.

​
The two core obligations

The Replay.dfy kernel requires concrete domains to prove exactly two lemmas. R1 — Initial state satisfies the invariant: 
lemma InitSatisfiesInv()
  ensures Inv(Init())
R2 — Every transition preserves the invariant (possibly after normalization): 
lemma StepPreservesInv(m: Model, a: Action)
  requires Inv(m)
  ensures Inv(Normalize(Apply(m, a)))
The Normalize function is the domain’s safety valve. When an action would violate Inv — such as decrementing a counter below zero — Normalize clamps the result back into the valid region. This lets Apply be a total function that never needs to reject or fail; Normalize makes the result well-formed unconditionally.
The precondition requires Inv(m) in StepPreservesInv is not circular. It says: if the current state is valid, then the next state (after normalization) is also valid. R1 seeds the induction, and R2 carries it through every reachable state.

​
What these obligations unlock

Once R1 and R2 are proved, the Replay kernel’s theorems follow automatically for your domain:
  • (RK1) For every reachable history h, Inv(Present(h)) holds.
  • (RK2) Do, Undo, and Redo all preserve Inv on the present state.
In other words, undo and redo cannot violate your invariant — not because those operations happen to be correct, but because the kernel proof is generic over any domain that satisfies R1 and R2.

​
The three-module pattern

Every dafny-replay application uses three Dafny modules in a single .dfy file. 
include "../kernels/Replay.dfy"

// 1. Domain: the core state machine
module MyAppDomain refines Domain { ... }

// 2. Kernel: wires the domain into undo/redo history
module MyAppKernel refines Kernel {
  import D = MyAppDomain
}

// 3. AppCore: the public API exposed to JavaScript
module AppCore {
  import K = MyAppKernel
  import D = MyAppDomain
  ...
}
1

MyAppDomain refines Domain

Provide the concrete types (Model, Action), the invariant (Inv), the transition function (Apply), and the normalization function (Normalize). Prove the two domain obligations here.
2

MyAppKernel refines Kernel

A single import line. The kernel’s Do, Undo, Redo, and all related lemmas are inherited from Replay.dfy and apply to your domain automatically.
3

AppCore

Expose Init, Dispatch, Undo, Redo, Present, CanUndo, and CanRedo as top-level functions. This is the surface that dafny2js reads to generate the JavaScript API.

​
Worked example: the Counter domain

The Counter is the minimal domain in the repository. The model is an integer, the invariant is non-negativity, and Normalize clamps negative results to zero. 
include "../kernels/Replay.dfy"

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)))
  {
  }
}
Both lemma bodies are empty. Dafny’s verifier proves them automatically from the definitions — 0 >= 0 is trivially true, and if m < 0 then 0 else m >= 0 holds for all integers. For more complex domains (such as Kanban’s WIP limit and partition invariants), lemma bodies contain explicit case splits and helper lemmas, but the obligations themselves remain the same two shapes.

​
The kernel module

module CounterKernel refines Kernel {
  import D = CounterDomain
}
That is the entire module. The Kernel abstract module in Replay.dfy provides Do, Undo, Redo, Preview, CommitFrom, and all their invariant lemmas. Refining it with CounterDomain instantiates all of them for integers.

​
AppCore

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 }
}
AppCore is the contract that dafny2js reads. Every function here becomes a named entry point in the generated app.js.

​
Verifying the domain

Run Dafny verification before compiling to JavaScript: 
dafny verify CounterDomain.dfy
A clean run confirms both obligations are discharged and all module refinements are valid. Any proof failure appears here — never silently at runtime.

​
Additional obligations for other kernels

The Replay kernel requires the minimal two obligations. More powerful kernels require additional proofs.

​
Authority kernel

For server-authoritative state, the domain replaces Apply/Normalize with a TryStep function that returns a Result:
  • (A1) Inv(Init())
  • (A2) Inv(m) ∧ TryStep(m, a) = Ok(m′) ⇒ Inv(m′)
The Authority kernel then proves that the server’s present state always satisfies Inv, independent of what clients send.

​
Multi-Collaboration kernel

Multi-Collaboration shares A1 and A2 and adds three more:
  • (MC3a) A total Rebase function for rebasing client operations
  • (MC3b) A Candidates function and Explains predicate defining the domain’s intent envelope
  • (MC3c) CandidatesComplete — a proof that the intent envelope covers all valid candidate actions
These obligations are what give the kernel its intent-relative minimal rejection guarantee: if a rebased request is rejected, no action within the domain’s defined intent could have succeeded either.

dafny2js tool

Generate a JavaScript API wrapper from your verified Dafny modules.

Guarantees reference

Full statement of what is proved for each kernel, including integration boundaries.

Build docs developers (and LLMs) love

Get started for freeTalk to us