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.

Canon is a diagram editor that lets users place nodes, connect them with directed edges, and attach geometric constraints—horizontal/vertical alignment and even-spacing. A constraint solver called Canon reapplies all active constraints in order, producing a deterministic layout. The domain invariant guarantees that all constraints and edges reference only nodes that actually exist, and that constraint IDs remain fresh.

​
Domain model

The model is defined in canon/Canon.dfy and imported by canon/CanonDomain.dfy. Nodes have string identifiers and integer (x, y) coordinates. Constraints are first-class values with allocated IDs. 
type NodeId = string

datatype Node = Node(id: NodeId, x: int, y: int)

datatype Axis = X | Y

datatype Constraint =
  | Align(cid: int, targets: seq<NodeId>, axis: Axis)
  | EvenSpace(cid: int, targets: seq<NodeId>, axis: Axis)

datatype Edge = Edge(from: NodeId, to: NodeId)

datatype Model = Model(
  nodes: map<NodeId, Node>,
  edges: seq<Edge>,
  constraints: seq<Constraint>,
  nextCid: int
)
The CanonDomain module wraps this model with an Action datatype: 
datatype Action =
  | AddNode(id: NodeId, x: int, y: int)
  | AddAlign(sel: seq<NodeId>)
  | AddEvenSpace(sel: seq<NodeId>)
  | AddEdge(from: NodeId, to: NodeId)
  | DeleteConstraint(cid: int)
  | DeleteEdge(from: NodeId, to: NodeId)
  | RemoveNode(nodeId: NodeId)
  | MoveNode(id: NodeId, newX: int, newY: int)

​
Key invariants

predicate Inv(m: Model) {
  AllConstraintsValid(m.constraints, m.nodes)
  && AllEdgesValid(m.edges, m.nodes)
}
Referential integrity — every node ID referenced in a constraint or edge must be present in m.nodes. This is maintained by filtering out missing nodes when adding constraints (FilterPresent) and by cleaning up constraints and edges when a node is removed (ShrinkConstraints, FilterOutIncidentEdges). Constraint ID freshness — there is no explicit freshness invariant in Inv (freshness is enforced by the allocator pattern in AddAlign and AddEvenSpace which increment nextCid). The allocator ensures that each new constraint receives a unique ID.

​
Constraint solver

The Canon function runs a bounded fixpoint of CanonOnce. Each pass applies all constraints in sequence:
  • Align — sets all target nodes’ coordinate along the specified axis to the mean of the group.
  • EvenSpace — sorts target nodes by coordinate along the axis and spaces them evenly between the endpoints.
// One pass of all constraints, then iterate to fixpoint (up to 10 rounds)
function Canon(m: Model): (result: Model)
  requires Inv(m)
  ensures Inv(result)
{
  CanonFixpoint(m, 10)
}
The solver is called explicitly via CanonHistory in the AppCore module, which applies Canon to the present state without adding a history entry—so undo skips past the solved layout back to the user-authored one.

​
RemoveNode cascade

When a node is removed, RemoveNode cleans up all dangling references:
  1. Constraints that mention the removed node have that node stripped from their target list. Constraints that become degenerate (fewer than 2 targets for Align, fewer than 3 for EvenSpace) are dropped entirely.
  2. Edges that start or end at the removed node are filtered out.
This keeps Inv satisfied without requiring the caller to manually manage referential integrity.

​
Running the app

cd canon
npm install
npm run dev
The UI lets you add nodes by clicking on the canvas, connect them with edges, select multiple nodes to add alignment or even-spacing constraints, and trigger the constraint solver. Undo/redo works across all operations including constraint additions.

Replay kernel

Canon uses the Replay kernel for undo/redo, with CanonHistory applying the solver outside the history stack.

Domain obligations

The two lemmas every domain must prove to plug into a kernel.

Build docs developers (and LLMs) love

Get started for freeTalk to us