libvgraph

libvgraph is the formally specified, deterministic structural-graph substrate for Vinary projects. It provides a production Rust implementation backed by machine-checked semantics, explicit work and heap bounds, exhaustive independent oracles, bounded model checking, and documentation verification.

The first contract covers canonical compressed sparse row (CSR) graphs, strongly connected component (SCC) quotients, condensation directed acyclic graphs (DAGs), and dependency wavefronts. It preserves the semantics already exercised by libcpg while remaining independent of code property graphs, equality graphs, parsers, and weighted automata.

The core has no serialization or hashing dependency. Portable snapshots, schema identities, digests, and provenance sidecars belong to the separately versioned libvgraph-interop boundary.

On validated canonical CSR, the required SCC path is iterative, uses strict linear work, retains all graph-depth state on the heap, and preserves a constant native control depth. Arbitrary stable labels are canonicalized at a separately named comparison-model boundary so their unavoidable ordering cost is never conflated with graph-analysis complexity.

Start here

• Graph quotient theory
• Canonical snapshot laws
• Formal-first architecture
• Portable snapshot boundary
• Exhaustive validation method
• Snapshot validation method
• Implementation refinement matrix
• Snapshot refinement matrix
• Resource and input safety
• Snapshot security and resource safety
• Rust API and usage
• Canonical snapshot wire format
• Performance and deterministic concurrency
• Verification workflow
• Formal verification guide
• Diagram catalog

Run scripts/verify-formal.sh all before changing production semantics. The runner places every heavy proof layer in an explicit no-swap systemd memory scope. Run scripts/verify-docs.sh for every documentation update.

Status

The graph-kernel contract and implementation are tracked by pgmcp tasks vco-e2-formal-contracts, vco-e2-kernel-implementation, and vco-e2-kernel-release. The independent snapshot/digest contract is tracked by vco-e2-interop-formal; its required-red properties intentionally name the separately owned libvgraph-interop package.

License

Apache-2.0. See LICENSE.