AVI-530: shortest-path reachability + SCC decomposition (AVI-518 Haskell)

[jeremiepas]

Summary

Implements the AVI-518 math requirements (docs/math-requirements/AVI-518-shortest-path-scc.md) in Graphos.Domain.Graph.Query, repairing and completing the preserved work from d0785ef:

• shortestPathReachable / shortestPathReachableWithCached — forward reachability decision u :-> v (Thm 2.4), consistent with shortestPath /= Nothing.
• stronglyConnectedComponents / stronglyConnectedComponentsWithCached — iterative Tarjan SCC (§3.1), O(N+E), iterative frame stack (no per-node recursion), component ids by ascending minimum NodeId (deterministic under key permutation, INV-9).
• Fixes three defects in the preserved code: tree-edge lowlink propagated idx[u] instead of low[u] (split cycles like a→b→c→a incorrectly); component flattening zipped ids over nodes instead of components (destroyed the partition); subgraph had lost its type signature.
• New test suite tests/Graphos/Domain/Graph/SCCSpec.hs (19 tests).

Acceptance criteria → how met

#	Criterion	Evidence
1	Golden §8 example: SCCs {a,b,c},{d,e},{f}, condensation chain, shortestPath a f == Just [a,b,c,d,f], shortestPath a a == Just [a], shortestPath f a == Nothing	stronglyConnectedComponents (§8 golden example) + shortestPathReachable (§8 golden example) describe blocks (11 tests)
2	INV-7 partition property on random graphs	INV-7 (property) — (M . concatMap snd) == M (Map.keys gNodes), pairwise disjoint, non-empty
3	INV-8: every shortestPath result is a valid hop-minimal E-walk; arcs ⇒ Just [u,v]	Two properties: E-walk validity + hop-minimality via independent BFS oracle; arc property restricted to u /= v (self-loops correctly yield Just [u], covered by an explicit test)
4	Determinism: repeated calls identical regardless of key order	INV-9 repeat-call equality property (components are order-canonical: sorted members, ids by ascending min NodeId)
+	INV-10: adding an arc only merges SCCs	Golden f->a merge test + coarsening property over random graphs via addEdges

Verification

• cabal build lib:graphos — clean
• cabal test graphos-test --enable-tests — 781 examples, 0 failures, 3 pending (includes new SCC suite)
• SCC/reachability complexity: single DFS pass, O(N+E); no all-pairs at scale (§4 guard respected)

Notes / open items (from doc §6/§10, unchanged)

• O1: shortestPath kept hop-minimal (per issue instruction).
• O2: traversal stays forward-only via FGL; documented as canonical reachability in Haddock. Product alignment can follow in a separate ticket.

Refs: AVI-518, AVI-530

[jeremiepas]

Implementation complete and tests added for AVI-518 (shortest-path reachability + SCC).

• shortestPathReachable/WithCached (Thm 2.4) and iterative Tarjan stronglyConnectedComponents/WithCached (§3.1, O(N+E)) in Graphos.Domain.Graph.Query
• Fixed tree-edge lowlink propagation (low not idx), partition mapping, and restored subgraph signature
• New tests/Graphos/Domain/Graph/SCCSpec.hs: §8 golden example, INV-7/8/9/10 properties; full suite 781 examples, 0 failures
• Open items unchanged: O1 hop-minimal kept; O2 forward-only traversal documented as canonical reachability

Requesting review per PDCA handoff (head-of-dev dispatches haskell-reviewer → pr-validator → openspec-verifier).

[jeremiepas]

Haskell Code Review — AVI-530 shortest-path reachability + SCC

Verdict: LGTM — code review passed (no blockers / majors)

Reviewed Query.hs (reachability + iterative Tarjan SCC), SCCSpec.hs (new 19-test suite), and graphos.cabal. Reviewed statically; relying on the submitter's reported clean cabal build lib:graphos + full cabal test (781 examples, 0 failures).

Correctness

• Tarjan (sccIndices): iterative frame-stack variant, O(N+E). Tree-edge propagation uses low[child] (relow); back/cross-edge uses idx[target] (relowIdx) — the two fixes from draft d0785ef are correctly applied. Hand-traced the §8 cycle a->b->c->a, a chain, and a diamond; all yield correct SCC partitions and canonical component ids.
• Partition result: maps component id -> sorted member NodeIds (restored from the flattening bug). sortOn minimum then Map.fromList (zip [0..] …) yields deterministic ids by ascending min NodeId; members sorted, seeds visited in ascending index order -> INV-9 canonical under key permutation.
• shortestPathReachable: defined as shortestPath … /= Nothing (Thm 2.4), the reflexive-transitive closure; returns False for missing src/tgt via the pattern guard. Total function.
• No unsafePerformIO / unsafeCoerce; state is ST-based through runST (no leak); no new FFI dependencies.

Tests

• Every acceptance criterion maps to a test (§8 golden = 11 tests; INV-7/8/9/10 properties). INV-8 hop-minimality uses an independent BFS oracle (good separation of concerns); INV-7 partition (cover + disjoint + non-empty) and INV-10 coarsening are strong.

Findings (non-blocking)

Minor

• SCCSpec.hs INV-9 property (stronglyConnectedComponents g == stronglyConnectedComponents g) is vacuous — it is x == x on the same graph and can never fail. It does not exercise permutation-invariance or canonical labeling over random graphs. Build a key-permuted variant of g and assert equality (or assert the mapping equals an independent canonical construction).

Nits

• Query.hs: comps \deepseq` mapped `deepseq` mappedis redundant —Map.fromListalready forces the map to WHNF; a plainmapped(or an explicitrnf/seq`) reads clearer.
• SCCSpec.hs isValidWalk: the || u == v clause in the E-walk edge check is unnecessary — shortestPath returns simple paths with no repeated consecutive nodes. Harmless, but slightly misleading about what is being asserted.

Suggested for devhaskell in remediation (non-blocking): strengthen the INV-9 property as above and tidy the deepseq expression.