yams/formal/topology
Trevon e84ced261b
feat(topology): road sidecar persistence (#302)
Persist `TopologyArtifactBatch::roads` in a sidecar knowledge-graph node,
`topology:roads:<snapshotId>` of type `topology_road_snapshot`, instead
of growing the main snapshot codec. The sidecar has its own binary magic
('Y','A','M','R'), version 1, and a Zstd JSON envelope with
`format = "topology_roads_zstd_v1"`. The main snapshot stays a plain v1
payload, byte-identical with roads on or off, so memory-sync replicas on
older peers keep decoding it, and an unknown node type is simply never
read by an old store. `deserializeTopologyBatchCompressed` now rejects an
envelope whose `format` it does not know instead of treating it as legacy
raw JSON.

Header layout (little-endian): u32 magic, u32 version, u32 maxPerCluster,
u32 reserved, string snapshotId, u32 cluster-id table count + strings,
u32 road count, then per road u32 from index, u32 to index, f64 weight.
`TopologyArtifactBatch::roadMaxPerCluster` records the bound the builder
applied so the header can carry it; both engines set it.

The store writes the sidecar right after the snapshot node and before
the `topology:snapshot:latest` pointer, so the pointer remains the commit
point: an injected sidecar failure leaves the previous snapshot current.
Retention deletes each pruned snapshot's sidecar with it, and re-storing
a snapshot id without roads removes its stale sidecar. Loading is
optional and soft: a missing sidecar yields empty roads with no error; an
undecodable or invalid one (snapshot mismatch, endpoint not a cluster,
self loop, negative or non-finite weight, more roads per source than the
declared top-K) drops the roads and records
`TopologyArtifactBatch::roadUnavailableReason`, surfaced on the routing
session and as the `topology_road_unavailable_reason` debug key, while
the snapshot still loads and routes.

`topologyRoadFingerprint(batch)` gives roads their own order-independent
identity for cache provenance; the routing construction fingerprint is
unchanged and stays road-free through the persisted path.

Lean (formal/topology/Yams/Topology/Artifacts.lean): `ClusterRoad`,
`WellFormedRoads` (endpoints in clusters, no self loop, non-negative
weight, bounded per source), `constructionIdentity`, and lemmas that the
construction identity and `WellFormedBatch` are independent of roads and
that an empty road layer is well formed. Checked with lake (lean 4.31.0).

Tests: tests/unit/topology/topology_road_sidecar_catch2_test.cpp (codec
round trip, foreign/truncated payload rejection, main payload identical
on/off, validation reasons, store round trip, missing sidecar, every
corrupt-sidecar case with routing still admitted, write-before-pointer,
retention, fingerprints through the persisted path) and the extended
fingerprint invariance test in topology_roads_catch2_test.cpp.

`road_to` knowledge-graph edges are deferred until a consumer needs them.

Signed-off-by: trvon <me@trevon.dev>
2026-10-14 08:47:03 -06:00
..
Yams feat(topology): road sidecar persistence (#302) 2026-10-14 08:47:03 -06:00
lake-manifest.json feat(search): make topology-assisted retrieval the default (#57) 2026-07-13 20:26:43 -04:00
lakefile.toml feat(search): make topology-assisted retrieval the default (#57) 2026-07-13 20:26:43 -04:00
lean-toolchain feat(search): make topology-assisted retrieval the default (#57) 2026-07-13 20:26:43 -04:00