a bit more

Author: namin

README_LemmaScript.md

@@ -19,7 +19,9 @@ Gates connections so the graph stays acyclic. Node-level (source/target ids), ne
 
 **Acyclicity bridge** — `acyclic(edges) ==> ( acyclic(edges + e) <==> !wouldCreateCycle(edges, src, tgt) )`: gated insertion never creates a cycle, and never blocks a safe edge.
 
-Predicate `reach` and the path lemmas are hand-written in `graph.dfy` (additions-only). Trust manifest: proof is over `EdgeBase[]`/node ids (no React), and holds only if every commit routes through the gate. Demonstrated in the `CycleGate` example (`examples/react/src/examples/CycleGate/`) via `onConnect` (commit) + `isValidConnection` (drag feedback); drag a loop and it is rejected on screen.
+**Topological-rank witness** — `rank(n)` = number of nodes that can reach `n`; proven (`TopoRankMonotone`) to strictly increase along every edge of an acyclic graph, so sorting nodes by `rank` is a safe evaluation order. `canReach` is exported as a public primitive; the count + sort are trusted glue over it.
+
+Predicate `reach` and the path lemmas are hand-written in `graph.dfy` (additions-only). Trust manifest: proof is over `EdgeBase[]`/node ids (no React), and holds only if every commit routes through the gate. Demonstrated in the `CycleGate` example (`examples/react/src/examples/CycleGate/`) via `onConnect` (commit) + `isValidConnection` (drag feedback): drag a loop and it is rejected on screen (red dashed line), while a live "safe evaluation order" reflects the topological rank.
 
 ### Edge Utilities (`packages/system/src/utils/edges/general.ts`)
 

examples/react/src/examples/CycleGate/index.tsx

@@ -10,6 +10,7 @@ import {
   useEdgesState,
   useReactFlow,
   wouldCreateCycle,
+  canReach,
   MarkerType,
   type Node,
   type Edge,
@@ -64,6 +65,14 @@ const CycleGateFlow = () => {
     [getEdges, setEdges]
   );
 
+  // Stage 3: a safe evaluation order. rank(n) = #nodes that can reach n; sorting by
+  // ascending rank is a topological order — `TopoRankMonotone` (graph.dfy) proves rank
+  // strictly increases along every edge of an acyclic graph. The verified primitive is
+  // `canReach`; the count + sort here are trusted glue over it.
+  const ids = nodes.map((n) => n.id);
+  const rankOf = (n: string) => ids.filter((m) => canReach(edges, m, n)).length;
+  const order = [...ids].sort((a, b) => rankOf(a) - rankOf(b));
+
   return (
     <>
       {/* Make a cycle-creating drag obviously rejected: React Flow tags the in-progress
@@ -106,6 +115,9 @@ const CycleGateFlow = () => {
               <span style={{ color: '#e74c3c', fontWeight: 600 }}>red &amp; dashed</span> and is refused —
               proven in <code>graph.ts</code>.
             </div>
+            <div style={{ marginTop: 8, color: '#2c3e50' }}>
+              Safe evaluation order: <strong>{order.join(' → ')}</strong>
+            </div>
           </div>
         </Panel>
       </ReactFlow>

packages/react/src/index.ts

@@ -141,6 +141,7 @@ export {
   getOutgoers,
   getConnectedEdges,
   wouldCreateCycle,
+  canReach,
 } from '@xyflow/system';
 
 export { addEdge, reconnectEdge } from './utils/edges';

packages/system/src/utils/graph.dfy

@@ -324,3 +324,38 @@ lemma AcyclicBridge(edges: seq<EdgeBase>, e: EdgeBase)
     }
   }
 }
+
+// ── Stage 3: verified topological-rank witness ─────────────────────────────────────
+// rank(n) = number of nodes that can reach n (its ancestors). For an acyclic graph this
+// is a topological numbering: it strictly increases along every edge, so processing
+// nodes by increasing rank is a safe evaluation order. (Sorting by the rank is trusted
+// glue; the monotonicity is what is proven.)
+ghost function ancestorsWithin(edges: seq<EdgeBase>, nodes: set<string>, n: string): set<string>
+{
+  set m | m in nodes && reach(edges, m, n)
+}
+
+lemma TopoRankMonotone(edges: seq<EdgeBase>, nodes: set<string>, u: string, v: string)
+  requires acyclic(edges)
+  requires hasEdge(edges, u, v)
+  requires u in nodes && v in nodes
+  ensures |ancestorsWithin(edges, nodes, u)| < |ancestorsWithin(edges, nodes, v)|
+{
+  HasEdgeReach(edges, u, v);   // reach(u, v)
+  // Every ancestor of u is an ancestor of v (m ->* u -> v).
+  forall m | m in ancestorsWithin(edges, nodes, u)
+    ensures m in ancestorsWithin(edges, nodes, v)
+  {
+    ReachTrans(edges, m, u, v);
+  }
+  ReachRefl(edges, v);
+  assert !reach(edges, v, u);   // acyclic: hasEdge(u,v) ==> !reach(v,u)
+  var au := ancestorsWithin(edges, nodes, u);
+  var av := ancestorsWithin(edges, nodes, v);
+  assert au <= av;                              // from the forall
+  assert v in av && v !in au;                   // v is an ancestor of v, not of u
+  // |av| = |au| + |av - au| (disjoint union), and av - au is non-empty (contains v).
+  assert au !! (av - au) && au + (av - au) == av;
+  assert |av| == |au| + |av - au|;
+  assert |av - au| >= 1;
+}

packages/system/src/utils/graph.ts

@@ -143,7 +143,7 @@ export const getIncomers = <NodeType extends NodeBase = NodeBase, EdgeType exten
 
 // Reflexive reachability over the edge list: bounded BFS from `from`, terminating
 // because `visited` grows monotonically toward the finite set of node ids.
-function canReach(edges: EdgeBase[], from: string, to: string): boolean {
+export function canReach(edges: EdgeBase[], from: string, to: string): boolean {
   //@ verify
   let frontier: string[] = [from];
   let visited: string[] = [];