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 Multi-Project kernel extends Multi-Collaboration to operations that span multiple projects — for example, moving a task from one project to another. The key insight is that the action itself declares which projects it touches. The kernel lifts all single-project effect state machine guarantees to the multi-project setting while adding per-project version tracking and atomic cross-project transitions.

​
Key insight: actions declare their scope

function TouchedProjects(a: MultiAction): set<ProjectId>
{
  match a
  case Single(pid, _) => {pid}
  case MoveTaskTo(src, dst, _, _, _) => {src, dst}
  case CopyTaskTo(src, dst, _, _) => {src, dst}
}
TouchedProjects is the anchor of the entire architecture. The server loads only the projects listed by this function, verifies membership for each, and writes back only the changed projects — atomically. Cross-project operations are all-or-nothing: if any project’s version check fails, the entire transaction rolls back.

​
Data structures

​
MultiModel

datatype MultiModel = MultiModel(
  projects: map<ProjectId, Model>
)
A MultiModel is a map from project IDs to individual project models. Each project model is independently verified against the single-project domain invariant.

​
MultiAction

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)
Single wraps any single-project action, allowing the same state machine to handle both cases uniformly. MoveTaskTo removes the task from the source project and inserts it into the destination. CopyTaskTo duplicates the task.

​
MultiClientState

datatype MultiClientState = MultiClientState(
  baseVersions: map<ProjectId, nat>,
  present: MultiModel,
  pending: seq<MultiAction>
)
Unlike the single-project ClientState which has a single baseVersion, MultiClientState tracks a separate version per project. A cross-project action carries both versions in the SendDispatch command.

​
MultiInv

ghost predicate MultiInv(mm: MultiModel)
{
  forall pid :: pid in mm.projects ==> Inv(mm.projects[pid])
}
The multi-project invariant holds when every project in the model satisfies its individual domain invariant. There is no cross-project invariant — correctness of each project is proved independently.

​
Domain obligation

Each concrete multi-project domain must prove one lemma: 
lemma MultiStepPreservesInv(mm: MultiModel, a: MultiAction, mm2: MultiModel)
  requires MultiInv(mm)
  requires AllProjectsLoaded(mm, a)
  requires MultiStep(mm, a) == Ok(mm2)
  ensures MultiInv(mm2)
This lifts the single-project StepPreservesInv to the multi-project setting. For Single actions, it delegates to the single-project proof. For MoveTaskTo and CopyTaskTo, the concrete domain proves that the source and destination models both satisfy Inv after the operation.

​
Core functions

​
AllProjectsLoaded

predicate AllProjectsLoaded(mm: MultiModel, a: MultiAction)
{
  forall pid :: pid in TouchedProjects(a) ==> pid in mm.projects
}
A precondition that must hold before calling MultiStep. If a touched project is missing, TryMultiStep returns MissingProject without attempting the transition.

​
MultiStep and TryMultiStep

function MultiStep(mm: MultiModel, a: MultiAction): Result<MultiModel, MultiErr>
  requires AllProjectsLoaded(mm, a)

function TryMultiStep(mm: MultiModel, a: MultiAction): Result<MultiModel, MultiErr>
// Returns MissingProject error if AllProjectsLoaded fails

lemma TryMultiStepEquivalence(mm: MultiModel, a: MultiAction)
  requires AllProjectsLoaded(mm, a)
  ensures TryMultiStep(mm, a) == MultiStep(mm, a)
MultiStep is the verified core function used in proofs. TryMultiStep is the runtime-safe variant used by edge functions — it checks AllProjectsLoaded internally and returns a structured error instead of failing a precondition.

​
ChangedProjects

function ChangedProjects(before: MultiModel, after: MultiModel): set<ProjectId>
{
  set pid | pid in after.projects &&
            (pid !in before.projects || before.projects[pid] != after.projects[pid])
}
Used by the server to determine which projects to write back. Only changed projects are saved; untouched projects are not written even if they were loaded.

​
MultiRebase

function MultiRebase(
  projectLogs: map<ProjectId, seq<Action>>,
  baseVersions: map<ProjectId, nat>,
  a: MultiAction
): MultiAction
Rebases a multi-action through the concurrent changes in each touched project since the client’s base versions. For Single actions, this delegates to the single-project RebaseThroughSuffix. For cross-project actions, the concrete domain defines rebase semantics.

​
Effect state machine events

The multi-project effect state machine uses the same event structure as the single-project version, extended with per-project versions: 
datatype Event =
  | UserAction(action: MultiAction)
  | DispatchAccepted(versions: map<ProjectId, nat>, models: map<ProjectId, Model>)
  | DispatchConflict(versions: map<ProjectId, nat>, models: map<ProjectId, Model>)
  | DispatchRejected(versions: map<ProjectId, nat>, models: map<ProjectId, Model>)
  | NetworkError
  | NetworkRestored
  | Tick

datatype Command =
  | NoOp
  | SendDispatch(touched: set<ProjectId>, versions: map<ProjectId, nat>, action: MultiAction)

​
Kernel theorems

MultiProjectEffectStateMachine.dfy proves the following properties, lifting all single-project guarantees to the multi-project setting:
All effect state transitions preserve the multi-project effect state invariant.
  • PendingNeverLost — pending actions are never arbitrarily lost
  • PendingSequencePreserved — on accept/reject: pending' == pending[1..]
  • ConflictPreservesPendingExactly — conflicts preserve pending exactly
  • RealtimeUpdatePreservesPendingExactly — realtime updates preserve pending exactly
  • UserActionAppendsExact — user actions append exactly the action to pending
  • RetriesAreBounded — retries never exceed MaxRetries
  • ModeConsistent — dispatching mode always implies pending actions exist

​
Module hierarchy

MultiCollaboration.dfy (single-project collaboration)
        ↓ imports
MultiProject.dfy (cross-project interface)        ← abstract
        ↓ refines
TodoMultiProjectDomain.dfy (concrete Todo domain)

MultiProjectEffectStateMachine.dfy (abstract ESM) ← abstract
        ↓ refines
TodoMultiProjectEffectStateMachine.dfy            ← concrete + AppCore
The abstract/concrete refinement pattern means the kernel theorems are proved once in the abstract modules and inherited for free by every concrete instantiation.

​
Trust boundaries

ComponentTrust level
MultiStep, TryMultiStepVerified in Dafny
TouchedProjectsVerified in Dafny
ChangedProjectsVerified in Dafny
Effect state machineVerified in Dafny
JSON conversion (dafny2js output)Generated, tested
Edge function orchestrationUnverified I/O glue
save_multi_update SQL functionTested, not formally verified
Realtime propagation is outside the verified boundary. A cross-project operation updating two projects produces two separate realtime events that arrive independently. Clients may briefly see inconsistent state until both events arrive.

​
Integration boundary (trusted)

  • Atomic application of verified multi-project transitions to storage
  • Realtime skew (partial arrival of multi-project updates)
  • Edge function orchestration around verified transitions
  • Semantics of TouchedProjects beyond what the concrete domain proves

Multi-Collaboration kernel

The single-project foundation that Multi-Project extends.

Effect State Machine

The single-project effect orchestration kernel.

CollabTodo app

Full example of the Multi-Project kernel with MoveTaskTo and CopyTaskTo.

Guarantees reference

Precise trust boundaries for the Multi-Project kernel.

Build docs developers (and LLMs) love

Get started for freeTalk to us