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 architectural split in a dafny-replay React app is deliberate: Dafny owns state transitions and invariant enforcement, React owns rendering and user interaction. React’s useState holds the Dafny History object as an opaque value. Every state change goes through App.Dispatch, App.Undo, or App.Redo — functions that are proved to preserve your domain’s invariant. React never mutates state directly; it only calls the verified transition functions and re-renders when they return a new history.

​
Prerequisites

  • A verified Dafny domain module (see domain obligations)
  • A compiled .cjs bundle and generated app.js from dafny2js (see dafny2js)
  • A Vite React app created with npm create vite@latest my-app -- --template react

​
Install dependencies

npm install bignumber.js
The Dafny-compiled JavaScript uses bignumber.js for arbitrary-precision integers. You must install it in your Vite app so the require stub in app.js can resolve it.

​
Configure Vite

Edit vite.config.js to tell Vite’s optimizer to pre-bundle bignumber.js: 
import { defineConfig } from 'vite'
import react from '@vitejs/plugin-react'

export default defineConfig({
  plugins: [react()],
  optimizeDeps: {
    include: ['bignumber.js'],
  },
})
Without optimizeDeps.include, Vite may fail to pre-bundle bignumber.js correctly when it is loaded indirectly through the new Function evaluator that app.js uses to bootstrap the Dafny runtime.

​
Loading the Dafny bundle

The generated app.js handles loading automatically. Behind the scenes it uses Vite’s ?raw import to load the .cjs bundle as a string, then evaluates it with a minimal require stub that supplies bignumber.js: 
import BigNumber from 'bignumber.js';
BigNumber.config({ MODULO_MODE: BigNumber.EUCLID });

import dafnyCode from './Counter.cjs?raw';

const require = (mod) => {
  if (mod === 'bignumber.js') return BigNumber;
  throw new Error(`Unknown module: ${mod}`);
};

const initDafny = new Function('require', `
  ${dafnyCode}
  return { _dafny, CounterDomain, CounterKernel, AppCore };
`);

const { _dafny, CounterDomain, CounterKernel, AppCore } = initDafny(require);
You do not write this code yourself — dafny2js generates it. You just need to ensure bignumber.js is installed and the Vite config is correct.
The MODULO_MODE: BigNumber.EUCLID setting is required because Dafny’s modulo operation follows Euclidean division semantics, which differs from JavaScript’s % operator for negative numbers.

​
The useState History pattern

Store the Dafny History object in React state. Every user action creates a new history by calling the appropriate App function, then updates state with setH: 
import { useState } from 'react'
import App from './dafny/app.js'

function Counter() {
  const [h, setH] = useState(() => App.Init())

  const inc  = () => setH(App.Dispatch(h, App.Inc()))
  const dec  = () => setH(App.Dispatch(h, App.Dec()))
  const undo = () => setH(App.Undo(h))
  const redo = () => setH(App.Redo(h))

  return (
    <>
      <h1>Dafny Replay Demo</h1>
      <p className="subtitle">Verified, replayable reducer kernel</p>

      <div className="card">
        <div className="value">{App.Present(h)}</div>

        <div className="button-row">
          <button onClick={dec}>Dec</button>
          <button onClick={inc}>Inc</button>
        </div>

        <div className="button-row">
          <button onClick={undo} disabled={!App.CanUndo(h)}>
            Undo
          </button>
          <button onClick={redo} disabled={!App.CanRedo(h)}>
            Redo
          </button>
        </div>
      </div>

      <p className="info">
        React owns rendering, Dafny owns state transitions.
        <br />
        The invariant (value &gt;= 0) is verified at compile time.
      </p>
    </>
  )
}

export default Counter
Key points about this pattern:
  • useState(() => App.Init()) uses a lazy initializer so App.Init() is only called once.
  • App.Present(h) extracts the current model value from the history object for rendering.
  • App.CanUndo(h) and App.CanRedo(h) return booleans used to disable buttons. These are simple checks on whether h.past or h.future are non-empty.
  • Every action (Dispatch, Undo, Redo) returns a brand-new History object. React sees a new reference and re-renders.

​
Using Present, CanUndo, and CanRedo

These three accessors cover the most common rendering needs. 
// Extract the current model value
const value = App.Present(h)
// value is a plain JS number (or object for complex domains)

​
BigNumber handling

Dafny integers compile to BigNumber values. The generated app.js converts them to plain JavaScript numbers automatically wherever the model surface returns an integer. For example, App.Present(h) returns a plain number, not a BigNumber. If you use app-extras.js or access _internal modules directly, you may encounter raw BigNumber values. Convert them with .toNumber(): 
const bn = someRawDafnyInt;
const n  = bn.toNumber();   // plain JS number
For the reverse direction — passing a JavaScript number into a Dafny function that expects an integer: 
new BigNumber(42)
If you pass a plain JavaScript number where Dafny expects a BigNumber, the Dafny runtime will throw at runtime. Always use new BigNumber(n) when calling _internal module functions directly.

​
Kanban board example

The Kanban app demonstrates a richer domain with a complex model, multiple action types, and model accessors used in JSX: 
function KanbanBoard() {
  const [h, setH] = useState(() => App.Init())

  const model = App.Present(h)
  const cols  = App.GetCols(model)

  const dispatch = (action) => setH(App.Dispatch(h, action))
  const undo     = () => setH(App.Undo(h))
  const redo     = () => setH(App.Redo(h))

  const handleAddCard = (col, title) => {
    dispatch(App.AddCard(col, title))
  }

  const handleMoveCard = (cardId, toCol, pos) => {
    dispatch(App.MoveCard(cardId, toCol, pos))
  }

  return (
    <>
      <div className="controls">
        <button onClick={undo} disabled={!App.CanUndo(h)}>Undo</button>
        <button onClick={redo} disabled={!App.CanRedo(h)}>Redo</button>
      </div>

      <div className="board">
        {cols.map((col) => (
          <Column
            key={col}
            name={col}
            cards={App.GetLane(model, col)}
            wip={App.GetWip(model, col)}
            model={model}
            onAddCard={handleAddCard}
            onDrop={handleMoveCard}
          />
        ))}
      </div>
    </>
  )
}
The pattern is identical to the Counter: useState holds the history, App.Present extracts the model, and every mutation goes through App.Dispatch. The difference is that the Kanban model is a record with cols, lanes, wip, and cards fields, and AppCore exposes accessors (GetCols, GetLane, GetWip, GetCardTitle) that shield React from the internal Dafny map types.

​
Running the app

cd my-app
npm run dev
Open http://localhost:5173. Vite’s hot-module replacement works normally — edits to .jsx files reload instantly without re-evaluating the Dafny bundle.

dafny2js tool

Generate app.js from your Dafny source files.

app-extras.js pattern

Add convenience wrappers on top of the generated API.

Build docs developers (and LLMs) love

Get started for freeTalk to us