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 Authority kernel models a single authoritative server that accepts or rejects client requests through a versioned protocol. It proves that the server state always satisfies the domain invariant — independent of client correctness. Clients may apply actions optimistically, but the server evolves only through verified transitions.

​
ServerState

datatype S =
  S(ver: nat, present: D.Model)
The server holds a monotonically increasing version number and the current authoritative model. The version is incremented on every successful dispatch. The server invariant lifts directly from the domain invariant: 
ghost predicate SInv(s: S) {
  D.Inv(s.present)
}

​
Protocol operations

​
Dispatch

Dispatch is the core protocol operation. It accepts or rejects a client request based on version freshness and domain validity: 
function Dispatch(s: S, clientVer: nat, a: D.Action): (S, Response)
{
  if clientVer != s.ver then
    (s, Response(s.ver, Failure(Stale)))
  else
    match D.TryStep(s.present, a)
      case Ok(m') =>
        (S(s.ver + 1, m'), Response(s.ver + 1, Success(m')))
      case Invalid(msg) =>
        (s, Response(s.ver, Failure(InvalidAction(msg))))
}
Each request follows exactly one of three paths:
1

Stale version

The client’s version does not match the server’s. The server rejects with Failure(Stale) and returns its current version. The client must call Sync to refresh before retrying.
2

Invalid action

The version matches but TryStep returns Invalid(msg). The server rejects with Failure(InvalidAction(msg)). State is unchanged.
3

Valid action

The version matches and TryStep returns Ok(m'). The server transitions to m', increments its version, and returns Success(m').

​
Sync

Sync is a read-only snapshot of the current server state: 
function Sync(s: S): SyncResponse
  ensures Sync(s).ver == s.ver
  ensures Sync(s).present == s.present
{
  SyncResponse(s.ver, s.present)
}
Clients call Sync after a stale rejection to get the latest version and model, then rebase their pending actions.

​
Response types

datatype FailureReason =
  | Stale
  | InvalidAction(msg: string)

datatype Result =
  | Success(present: D.Model)
  | Failure(reason: FailureReason)

datatype Response =
  Response(ver: nat, res: Result)
The response always includes the authoritative version. On success, it includes the new model. On failure, the model is omitted and the state is unchanged.

​
Domain obligations

To use the Authority kernel, a concrete domain must prove two lemmas: 
lemma InitSatisfiesInv()
  ensures Inv(Init())
The server is initialized with D.Init(). This lemma seeds the proof.
lemma TryStepOkPreservesInv(m: Model, a: Action)
  requires Inv(m)
  ensures  TryStep(m, a).Ok? ==> Inv(TryStep(m, a).m')
Only successful TryStep results need to preserve Inv. Failed results leave the state unchanged, so no proof is needed for those paths.

​
Kernel theorems

These properties are proved once in the generic kernel assuming A1 and A2:
The main preservation lemma proves that Dispatch keeps SInv no matter what the client sends:
lemma DispatchPreservesSInv(s: S, clientVer: nat, a: D.Action)
  requires SInv(s)
  ensures  SInv(Dispatch(s, clientVer, a).0)
The proof branches on all three paths in Dispatch. Stale and invalid cases leave state unchanged; the valid case invokes TryStepOkPreservesInv.Stated at the trace level: for any protocol trace involving arbitrary client behavior, the authoritative server state always satisfies Inv.
Both Failure(Stale) and Failure(InvalidAction(...)) return the original s unchanged. This is structural — it follows directly from the Dispatch definition.

​
Initialization

function InitServer(): S {
  S(0, D.Init())
}

lemma InitServerSatisfiesSInv()
  ensures SInv(InitServer())
{
  D.InitSatisfiesInv();
}
The server starts at version 0 with the domain’s initial model. The InitServerSatisfiesSInv lemma is proved immediately from A1.

​
Relationship to Multi-Collaboration

The Authority kernel is intentionally minimal. It models a single authoritative state and a simple versioned protocol. It does not handle:
  • clients that submit actions based on stale versions without first resyncing,
  • rebasing or candidate fallback for concurrent edits,
  • offline clients and their pending queues.
The Multi-Collaboration kernel generalizes the Authority kernel with rebasing, anchor-based placement, and intent-relative minimal rejection for exactly these scenarios.
Server-side safety is independent of client correctness. Even if a client sends arbitrary or malformed requests, the server state never violates the domain invariant.

​
Integration boundary (trusted)

  • Networking, authentication, and authorization
  • Database persistence and concurrency beyond the modeled protocol
  • JavaScript/edge function wiring
  • End-to-end liveness

Replay kernel

The local undo/redo kernel that the Authority kernel extends conceptually.

Multi-Collaboration kernel

Generalizes Authority with rebasing, offline support, and minimal rejection.

Domain obligations guide

How to write A1 and A2 for your concrete domain.

Counter authority app

Minimal working example of the Authority kernel with a counter domain.

Build docs developers (and LLMs) love

Get started for freeTalk to us