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 Kanban app is the primary stress test for dafny-replay’s sequence and map reasoning. It models a task board with dynamic columns, ordered cards, and per-column work-in-progress limits. The domain must prove two non-local invariants that span the entire board state—making it substantially harder to verify than the counter example—and it has been proved against three different kernels.

​
Domain model

The domain is defined in kanban/KanbanDomain.dfy. Column identifiers are strings supplied by the UI; card identifiers are natural numbers allocated by the model itself. 
module KanbanDomain refines Domain {
  type ColId = string
  type CardId = nat

  datatype Card = Card(title: string)

  datatype Model = Model(
    cols: seq<ColId>,               // authoritative column order
    lanes: map<ColId, seq<CardId>>, // column -> ordered card IDs
    wip: map<ColId, nat>,           // column -> WIP limit
    cards: map<CardId, Card>,       // ID -> payload
    nextId: nat                     // fresh allocator
  )

  datatype Action =
    | AddColumn(col: ColId, limit: nat)
    | SetWip(col: ColId, limit: nat)
    | AddCard(col: ColId, title: string)
    | MoveCard(id: CardId, toCol: ColId, pos: int)
}

​
Key invariants

The Inv predicate encodes two structural guarantees plus column well-formedness: 
ghost predicate Inv(m: Model) {
  // Column list has no duplicates
  NoDupSeq(m.cols) &&

  // Lanes and WIP defined exactly on existing columns
  (forall i :: 0 <= i < |m.cols| ==> m.cols[i] in m.lanes && m.cols[i] in m.wip) &&
  (forall c :: c in m.lanes ==> c in m.cols) &&
  (forall c :: c in m.wip   ==> c in m.cols) &&

  // A1: exact partition — no card appears twice or goes missing
  NoDupSeq(AllIds(m)) &&
  (forall id :: id in m.cards <==> OccursInLanes(m, id)) &&

  // B: WIP limits respected
  (forall i :: 0 <= i < |m.cols| ==>
    |m.lanes[m.cols[i]]| <= m.wip[m.cols[i]]) &&

  // Allocator freshness
  (forall id :: id in m.cards ==> id < m.nextId)
}
Exact partition (A1) is the harder invariant. AllIds flattens all lanes into one sequence; NoDupSeq on that sequence means every card ID appears in exactly one column. The equivalence id in m.cards <==> OccursInLanes(m, id) ensures no card is lost or invented. Proving this for MoveCard requires reasoning about RemoveFirst and InsertAt across the full flattened sequence. WIP limits (B) guarantee that no column holds more cards than its limit. AddCard and MoveCard both check the destination limit before accepting—if the limit would be exceeded the action is a no-op.

​
Normalize

Normalize is the identity function in this domain: 
function Normalize(m: Model): Model { m }
Every action is designed to be a no-op on invalid input rather than producing an invalid intermediate state, so no repair step is needed.

​
Kernel variants

Three separate app directories prove the Kanban domain against different kernels:
DirectoryKernelExtra features
kanban/ReplayUndo/redo only
kanban-multi-collaboration/Multi-CollaborationOffline clients, anchor-based moves, candidate fallback
kanban-cloud/Multi-Collaboration + Effect State MachinePersistent backend (Supabase or Cloudflare)
The Multi-Collaboration variant adds anchor-based placement (Place.AtEnd, Place.Before, Place.After) so concurrent card moves resolve gracefully when the anchor card has moved. The Effect State Machine variant adds bounded retry logic and pending-action preservation for the client-side network layer.

​
Running the app

cd kanban          # or kanban-multi-collaboration
npm install
npm run dev
For kanban-cloud, follow the backend setup in the Supabase or Cloudflare guides before running.

Replay kernel

Generic undo/redo kernel—the simplest Kanban variant uses only this.

Multi-Collaboration kernel

Anchor-based moves, candidate fallback, and minimal rejection for concurrent clients.

Effect State Machine

Bounded retries, FIFO pending queue, and no silent data loss for the network layer.

Backend overview

Choose between Supabase (managed auth, RLS) and Cloudflare (D1, Workers) for the cloud variant.

Build docs developers (and LLMs) love

Get started for freeTalk to us