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.

dafny-replay apps talk to the cloud through a thin abstraction layer rather than directly importing a provider SDK. This separation keeps your React components, Dafny dispatch logic, and effect state machine identical across deployments — only the adapter file changes. The same application ships against Supabase for managed infrastructure or Cloudflare Workers for a lower-cost, bring-your-own setup.

​
Directory structure

Every app that supports multiple backends has a src/backend/ directory: 
src/backend/
├── types.ts        # Interface definitions (Backend, DispatchResult, User)
├── supabase.ts     # Supabase implementation
├── cloudflare.ts   # Cloudflare Workers implementation
└── index.ts        # Selects backend based on VITE_BACKEND
index.ts reads the VITE_BACKEND environment variable at build time and exports the appropriate implementation as backend: 
const mode = import.meta.env.VITE_BACKEND || 'supabase'

export const backend: Backend =
  mode === 'cloudflare' ? createCloudflareBackend(apiUrl) :
  createSupabaseBackend()

​
Switching backends

Set VITE_BACKEND in your .env file before building or running the dev server: 
# Use Supabase (default)
VITE_BACKEND=supabase
VITE_SUPABASE_URL=https://your-project.supabase.co
VITE_SUPABASE_ANON_KEY=eyJ...

# Use Cloudflare Workers
VITE_BACKEND=cloudflare
VITE_API_URL=https://your-worker.workers.dev
No code changes are required — Vite inlines the correct adapter at build time.

​
The Backend interface

All providers implement the same Backend interface. The three generic sections — auth, dispatch, and realtime — are identical in shape across all backends: 
interface Backend {
  readonly isConfigured: boolean

  auth: {
    getCurrentUser(): Promise<User | null>
    getAccessToken(): Promise<string | null>
    signIn(email: string, password: string): Promise<void>
    signUp(email: string, password: string): Promise<void>
    signOut(): Promise<void>
    onAuthChange(callback: (user: User | null) => void): () => void
  }

  dispatch: {
    single(entityId: string, baseVersion: number, action: any): Promise<DispatchResult>
  }

  realtime: {
    subscribe(entityId: string, onUpdate: (version: number, state: any) => void): () => void
  }
}

interface User {
  id: string
  email: string
}

​
DispatchResult

The dispatch method returns one of three statuses: 
interface DispatchResult {
  status: 'accepted' | 'rejected' | 'conflict'
  version?: number   // present on 'accepted'
  state?: any        // present on 'accepted'
  error?: string     // present on 'rejected'
}
  • accepted — the action was valid and persisted; version and state reflect the new server state.
  • rejected — the Dafny domain checker refused the action (invariant violation); error explains why.
  • conflict — another writer updated the entity between your read and write; the client should rebase and retry.

​
Using the backend in React hooks

Frontend code imports from backend/index.ts and remains agnostic to which provider is active: 
import { backend } from '../backend/index.ts'

// Auth
const user = await backend.auth.getCurrentUser()

// Data (domain-specific methods added per app)
const projects = await backend.projects.list(user.id)

// Dispatch
const result = await backend.dispatch.single(projectId, version, action)

// Realtime subscription
useEffect(() => {
  return backend.realtime.subscribe(projectId, (version, state) => {
    // handle update from another client
  })
}, [projectId])
The hooks never import from @supabase/supabase-js or call fetch directly — that responsibility belongs entirely to the adapter.

​
Provider comparison

The table below shows what each provider brings and what stays the same regardless of choice:
ComponentSupabaseCloudflare
DatabasePostgreSQL + RLSD1 (SQLite)
Server functionsEdge Functions (Deno)Workers (JavaScript)
Realtimepostgres_changesDurable Objects (WebSocket)
AuthSupabase Auth (OAuth)Simple JWT
Access controlDatabase-level RLSApplication-level checks

​
What stays the same

Changing backends does not touch any of the following:
  • Dafny-compiled dispatch logic — pure JavaScript, runs identically in any environment
  • Effect state machine — client-side verified state, backend-agnostic
  • React components — all backend calls go through the abstraction
  • Domain model and proofs — Dafny source and compiled output are unchanged
Both backends run the same compiled Dafny code server-side. The dispatch logic is not re-implemented per provider — the same .cjs bundle is imported into the Supabase Edge Function (Deno) or the Cloudflare Worker (V8), with a provider-specific build flag (--deno or --cloudflare) to handle module format differences.

​
Adding a new backend

To add a third provider:
  1. Create src/backend/newbackend.ts implementing the Backend interface.
  2. Update src/backend/index.ts to handle the new value:
export const backend: Backend =
  mode === 'cloudflare' ? createCloudflareBackend(apiUrl) :
  mode === 'newbackend'  ? createNewBackend(...)           :
  createSupabaseBackend()
The React layer requires no changes.

​
Explore the backends

Supabase backend

Managed auth, PostgreSQL with RLS, built-in realtime, and Deno Edge Functions. Batteries included.

Cloudflare backend

D1 SQLite, Workers, Durable Objects for WebSocket realtime, and custom JWT auth. Lower cost.

Build docs developers (and LLMs) love

Get started for freeTalk to us