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.

CollabTodo is the most feature-complete domain in dafny-replay. It models a collaborative task management system with projects, ordered lists, tasks, tags, and soft delete. The domain is proved against the Multi-Project kernel, which extends Multi-Collaboration to support operations that span multiple projects—MoveTaskTo, CopyTaskTo, and MoveListTo.

​
Domain model

The model covers four entity types plus soft-delete semantics. Lists are ordered by a sequence of list IDs; tasks belong to exactly one list; tags are scoped to their project. 
datatype Model = Model(
  owner: UserId,
  members: set<UserId>,
  mode: ProjectMode,       // Personal | Collaborative
  lists: seq<ListId>,
  listNames: map<ListId, string>,
  tasks: map<ListId, seq<TaskId>>,
  taskData: map<TaskId, Task>,
  tags: map<TagId, Tag>,
  nextListId: ListId,
  nextTaskId: TaskId,
  nextTagId: TagId
)

datatype Task = Task(
  title: string,
  notes: string,
  completed: bool,
  starred: bool,
  dueDate: Option<Date>,
  assignees: set<UserId>,
  tags: set<TagId>,
  deleted: bool,
  ...
)
Cross-project actions are defined in TodoMultiProjectDomain.dfy: 
datatype MultiAction =
  | Single(project: ProjectId, action: Action)
  | MoveTaskTo(srcProject: ProjectId, dstProject: ProjectId,
               taskId: TaskId, dstList: ListId, anchor: Place)
  | CopyTaskTo(srcProject: ProjectId, dstProject: ProjectId,
               taskId: TaskId, dstList: ListId)
  | MoveListTo(srcProject: ProjectId, dstProject: ProjectId,
               listId: ListId)

​
Key invariants

The Inv predicate enforces six structural properties:
  1. Exact partition — every non-deleted task exists in exactly one list; no task is orphaned or duplicated.
  2. Unique list names — list names are unique within a project (case-insensitive comparison).
  3. Unique task titles per list — task titles are unique within each list (case-insensitive).
  4. Membership constraints — task assignees must be project members; the owner is always a member; personal projects have exactly one member.
  5. Referential integrity — tags referenced by tasks must exist; all allocator IDs are fresh.
  6. Valid dates — all due dates represent valid calendar dates.
The Multi-Project kernel lifts these per-project invariants to the multi-model setting: 
MultiInv(mm) ≜ ∀pid ∈ dom(mm.projects). Inv(mm.projects[pid])
Each cross-project action must preserve MultiInv. MultiStepPreservesInv proves this by chaining the per-project invariant preservation lemmas.

​
Cross-project operations

MoveTaskTo soft-deletes the task in the source project and recreates it in the destination list. CopyTaskTo leaves the source unchanged and adds a copy to the destination. MoveListTo deletes the list and all its tasks from the source and recreates them in the destination—clearing assignees and tags, which are project-scoped. When a concurrent update deletes a task before a MoveTaskTo reaches the server, MultiRebase converts the operation to a NoOp for the source project, preventing errors.

​
Backend support

CollabTodo supports two backends:
BackendAuthDatabaseRealtime
SupabaseOAuth (managed)Postgres + RLSBuilt-in
CloudflareCustom JWTD1 + Durable ObjectsWorkers
Both backends use the same compiled Dafny logic for all state transitions. The edge function calls MultiStep and writes results atomically; the realtime layer propagates updates to other clients.
Cross-project operations update two projects in a single database transaction. Realtime notifications for the two projects arrive separately, so clients may briefly see partial state until both arrive.

​
Running the app

cd collab-todo
npm install
npm run dev
A backend is required for full functionality. See the Supabase or Cloudflare guide for setup instructions.

Multi-Project kernel

The kernel that proves per-project invariants are preserved across cross-project operations.

Effect State Machine

Client-side orchestration: bounded retries, FIFO pending queue, no silent data loss.

Supabase backend

Managed auth, database-level RLS, and built-in realtime for CollabTodo.

Cloudflare backend

D1, Workers, and Durable Objects with application-level authorization.

Build docs developers (and LLMs) love

Get started for freeTalk to us