e84ced261bPersist `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>
289 lines
11 KiB
Lean4
289 lines
11 KiB
Lean4
import Std
|
||
import Yams.Core
|
||
|
||
namespace Yams.Topology
|
||
|
||
/-- Mirrors `TopologyBuildMode` in `include/yams/topology/topology_artifacts.h`. -/
|
||
inductive TopologyBuildMode where
|
||
| exact
|
||
| incremental
|
||
| approximate
|
||
deriving Repr, BEq, DecidableEq
|
||
|
||
/-- Mirrors `TopologyInputKind`. -/
|
||
inductive TopologyInputKind where
|
||
| semanticNeighborGraph
|
||
| embeddingNeighborhood
|
||
| hybrid
|
||
deriving Repr, BEq, DecidableEq
|
||
|
||
/-- Mirrors `DirtyRegionExpansionMode`. -/
|
||
inductive DirtyRegionExpansionMode where
|
||
| neighborsOnly
|
||
| priorClusterAndNeighbors
|
||
| adaptive
|
||
deriving Repr, BEq, DecidableEq
|
||
|
||
/-- Mirrors `DocumentTopologyRole`. -/
|
||
inductive DocumentTopologyRole where
|
||
| core
|
||
| bridge
|
||
| medoid
|
||
| outlier
|
||
deriving Repr, BEq, DecidableEq
|
||
|
||
/-- Document hash used in topology. Uses Yams.Core.DocumentHash for unification. -/
|
||
abbrev DocumentHash := Yams.Core.DocumentHash
|
||
/-- File path. Uses Yams.Core.FilePath for unification. -/
|
||
abbrev FilePath := Yams.Core.FilePath
|
||
/-- Cluster identifier. Uses Yams.Core.ClusterId for unification. -/
|
||
abbrev ClusterId := Yams.Core.ClusterId
|
||
/-- Embedding vector. Uses Rat for now; consider transitioning to Yams.Core.EmbeddingVector (ℚ). -/
|
||
abbrev Embedding := List Rat
|
||
|
||
structure TopologyNeighbor where
|
||
documentHash : DocumentHash
|
||
score : Rat := 0
|
||
reciprocal : Bool := false
|
||
deriving Repr, BEq
|
||
|
||
structure TopologyDocumentInput where
|
||
documentHash : DocumentHash
|
||
filePath : FilePath := ""
|
||
embedding : Embedding := []
|
||
neighbors : List TopologyNeighbor := []
|
||
metadata : List (String × String) := []
|
||
deriving Repr, BEq
|
||
|
||
structure TopologyBuildConfig where
|
||
mode : TopologyBuildMode := .incremental
|
||
inputKind : TopologyInputKind := .hybrid
|
||
maxDocuments : Nat := 0
|
||
maxNeighborsPerDocument : Nat := 32
|
||
maxDirtyRegionDocs : Nat := 256
|
||
maxDirtyRegionDepth : Nat := 2
|
||
maxDirtySeedCount : Nat := 64
|
||
maxLevels : Nat := 3
|
||
overlapLimit : Nat := 2
|
||
fullRebuildDocThreshold : Nat := 4096
|
||
minEdgeScore : Rat := 0
|
||
reciprocalOnly : Bool := true
|
||
allowOverlap : Bool := true
|
||
emitBridgeAnnotations : Bool := true
|
||
emitOutliers : Bool := true
|
||
dirtyRegionExpansion : DirtyRegionExpansionMode := .priorClusterAndNeighbors
|
||
kmeansK : Nat := 0
|
||
kmeansMaxIterations : Nat := 10
|
||
deriving Repr, BEq
|
||
|
||
structure TopologyDirtyRegion where
|
||
seedDocumentHashes : List DocumentHash := []
|
||
expandedDocumentHashes : List DocumentHash := []
|
||
bfsDepthReached : Nat := 0
|
||
includedPriorClusterMembers : Bool := false
|
||
includedSemanticNeighbors : Bool := false
|
||
coalesced : Bool := false
|
||
exceededRegionBudget : Bool := false
|
||
requiresWiderRebuild : Bool := false
|
||
deriving Repr, BEq
|
||
|
||
structure DocumentClusterMembership where
|
||
documentHash : DocumentHash
|
||
clusterId : ClusterId
|
||
parentClusterId : Option ClusterId := none
|
||
clusterLevel : Nat := 0
|
||
persistenceScore : Rat := 0
|
||
cohesionScore : Rat := 0
|
||
bridgeScore : Rat := 0
|
||
role : DocumentTopologyRole := .core
|
||
overlapClusterIds : List ClusterId := []
|
||
deriving Repr, BEq
|
||
|
||
structure ClusterRepresentative where
|
||
clusterId : ClusterId
|
||
documentHash : DocumentHash
|
||
filePath : FilePath := ""
|
||
representativeScore : Rat := 0
|
||
deriving Repr, BEq
|
||
|
||
structure ClusterArtifact where
|
||
clusterId : ClusterId
|
||
parentClusterId : Option ClusterId := none
|
||
level : Nat := 0
|
||
memberCount : Nat := 0
|
||
persistenceScore : Rat := 0
|
||
cohesionScore : Rat := 0
|
||
bridgeMass : Rat := 0
|
||
medoid : Option ClusterRepresentative := none
|
||
memberDocumentHashes : List DocumentHash := []
|
||
overlapClusterIds : List ClusterId := []
|
||
centroidEmbedding : Embedding := []
|
||
deriving Repr, BEq
|
||
|
||
/-- Mirrors `ClusterRoad`: one cluster's view of an undirected cluster-to-cluster link whose
|
||
weight sums the raw neighbor observations between members of the two clusters. Persisted in a
|
||
sidecar beside the snapshot, never inside the construction payload. -/
|
||
structure ClusterRoad where
|
||
fromClusterId : ClusterId
|
||
toClusterId : ClusterId
|
||
weight : Rat := 0
|
||
deriving Repr, BEq
|
||
|
||
structure TopologyArtifactBatch where
|
||
snapshotId : String := ""
|
||
algorithm : String := ""
|
||
inputKind : TopologyInputKind := .hybrid
|
||
generatedAtUnixSeconds : Nat := 0
|
||
topologyEpoch : Nat := 0
|
||
clusters : List ClusterArtifact := []
|
||
memberships : List DocumentClusterMembership := []
|
||
/-- Roads attached to the batch; empty when roads are off or the sidecar was dropped. -/
|
||
roads : List ClusterRoad := []
|
||
/-- Per-source bound the builder applied to `roads` (sidecar header `maxPerCluster`). -/
|
||
roadMaxPerCluster : Nat := 0
|
||
deriving Repr, BEq
|
||
|
||
structure TopologyUpdateStats where
|
||
documentsProcessed : Nat := 0
|
||
clustersCreated : Nat := 0
|
||
clustersUpdated : Nat := 0
|
||
membershipsUpdated : Nat := 0
|
||
bridgeDocsTagged : Nat := 0
|
||
medoidsSelected : Nat := 0
|
||
dirtySeedCount : Nat := 0
|
||
dirtyRegionDocs : Nat := 0
|
||
coalescedDirtySets : Nat := 0
|
||
fallbackFullRebuilds : Nat := 0
|
||
deriving Repr, BEq
|
||
|
||
inductive RouteScoringMode where
|
||
| current
|
||
| sizeWeighted
|
||
| seedCoverage
|
||
deriving Repr, BEq, DecidableEq
|
||
|
||
structure TopologyRouteRequest where
|
||
queryText : String := ""
|
||
seedDocumentHashes : List DocumentHash := []
|
||
limit : Nat := 8
|
||
scoringMode : RouteScoringMode := .current
|
||
queryEmbedding : Embedding := []
|
||
sparseDenseAlpha : Rat := 1 / 2
|
||
deriving Repr, BEq
|
||
|
||
structure ClusterRoute where
|
||
clusterId : ClusterId
|
||
medoidDocumentHash : Option DocumentHash := none
|
||
routeScore : Rat := 0
|
||
stabilityScore : Rat := 0
|
||
memberCount : Nat := 0
|
||
deriving Repr, BEq
|
||
|
||
/-- Structural invariant every produced cluster should satisfy. -/
|
||
def ClusterArtifact.memberCountMatches (c : ClusterArtifact) : Prop :=
|
||
c.memberCount = c.memberDocumentHashes.length
|
||
|
||
/-- Structural invariant every membership should point at a produced cluster. -/
|
||
def membershipsReferenceClusters (batch : TopologyArtifactBatch) : Prop :=
|
||
∀ m ∈ batch.memberships, ∃ c ∈ batch.clusters, c.clusterId = m.clusterId
|
||
|
||
/-- Structural invariant every cluster member should have a corresponding membership row. -/
|
||
def clusterMembersHaveMemberships (batch : TopologyArtifactBatch) : Prop :=
|
||
∀ c ∈ batch.clusters, ∀ h ∈ c.memberDocumentHashes,
|
||
∃ m ∈ batch.memberships, m.documentHash = h ∧ m.clusterId = c.clusterId
|
||
|
||
/-- Main well-formedness target for topology batches, independent of the algorithm. -/
|
||
def WellFormedBatch (batch : TopologyArtifactBatch) : Prop :=
|
||
(∀ c ∈ batch.clusters, c.memberCountMatches) ∧
|
||
membershipsReferenceClusters batch ∧
|
||
clusterMembersHaveMemberships batch
|
||
|
||
/-! ### Roads
|
||
|
||
Roads are retrieval hints layered over the certified cover. Their well-formedness mirrors the
|
||
soft validation `validateTopologyRoadSidecar` applies when a sidecar is loaded; a sidecar that
|
||
fails it is dropped, and the batch below keeps its construction identity unchanged. -/
|
||
|
||
/-- A cluster id names a cluster of the batch. -/
|
||
def namesCluster (batch : TopologyArtifactBatch) (id : ClusterId) : Prop :=
|
||
∃ c ∈ batch.clusters, c.clusterId = id
|
||
|
||
/-- Both road endpoints are clusters of the batch (`road_endpoint_not_cluster`). -/
|
||
def roadEndpointsAreClusters (batch : TopologyArtifactBatch) : Prop :=
|
||
∀ r ∈ batch.roads, namesCluster batch r.fromClusterId ∧ namesCluster batch r.toClusterId
|
||
|
||
/-- No road links a cluster to itself (`road_self_loop`). -/
|
||
def roadsHaveNoSelfLoop (batch : TopologyArtifactBatch) : Prop :=
|
||
∀ r ∈ batch.roads, r.fromClusterId ≠ r.toClusterId
|
||
|
||
/-- Road weights are non-negative (`road_weight_invalid`; finiteness is implicit over ℚ). -/
|
||
def roadWeightsNonNegative (batch : TopologyArtifactBatch) : Prop :=
|
||
∀ r ∈ batch.roads, 0 ≤ r.weight
|
||
|
||
/-- Roads leaving one source cluster. -/
|
||
def roadsFrom (batch : TopologyArtifactBatch) (source : ClusterId) : List ClusterRoad :=
|
||
batch.roads.filter (fun r => r.fromClusterId == source)
|
||
|
||
/-- Every source keeps at most `roadMaxPerCluster` roads
|
||
(`road_count_exceeds_max_per_cluster`). -/
|
||
def roadsBoundedPerSource (batch : TopologyArtifactBatch) : Prop :=
|
||
∀ source : ClusterId, (roadsFrom batch source).length ≤ batch.roadMaxPerCluster
|
||
|
||
/-- Well-formedness of the road layer; `WellFormedBatch` does not depend on it. -/
|
||
def WellFormedRoads (batch : TopologyArtifactBatch) : Prop :=
|
||
roadEndpointsAreClusters batch ∧
|
||
roadsHaveNoSelfLoop batch ∧
|
||
roadWeightsNonNegative batch ∧
|
||
roadsBoundedPerSource batch
|
||
|
||
/-- A batch with roads removed, as the store yields when the sidecar is missing or rejected. -/
|
||
def TopologyArtifactBatch.withoutRoads (batch : TopologyArtifactBatch) : TopologyArtifactBatch :=
|
||
{ batch with roads := [], roadMaxPerCluster := 0 }
|
||
|
||
/-- A batch with a road layer attached, as the store yields when the sidecar loads. -/
|
||
def TopologyArtifactBatch.withRoads (batch : TopologyArtifactBatch)
|
||
(roads : List ClusterRoad) (k : Nat) : TopologyArtifactBatch :=
|
||
{ batch with roads := roads, roadMaxPerCluster := k }
|
||
|
||
/-- The construction content a routing construction fingerprint is computed from: algorithm,
|
||
input kind, clusters and memberships. Roads are deliberately absent. -/
|
||
def constructionIdentity (batch : TopologyArtifactBatch) :
|
||
String × TopologyInputKind × List ClusterArtifact × List DocumentClusterMembership :=
|
||
(batch.algorithm, batch.inputKind, batch.clusters, batch.memberships)
|
||
|
||
/-- Attaching or replacing roads does not move the construction identity. -/
|
||
theorem constructionIdentity_withRoads (batch : TopologyArtifactBatch)
|
||
(roads : List ClusterRoad) (k : Nat) :
|
||
constructionIdentity (batch.withRoads roads k) = constructionIdentity batch := rfl
|
||
|
||
/-- Dropping roads does not move the construction identity. -/
|
||
theorem constructionIdentity_withoutRoads (batch : TopologyArtifactBatch) :
|
||
constructionIdentity batch.withoutRoads = constructionIdentity batch := rfl
|
||
|
||
/-- The certified cover (cluster/membership well-formedness) is independent of roads: a batch is
|
||
well-formed with any road layer exactly when it is well-formed without one. -/
|
||
theorem wellFormedBatch_withRoads_iff (batch : TopologyArtifactBatch)
|
||
(roads : List ClusterRoad) (k : Nat) :
|
||
WellFormedBatch (batch.withRoads roads k) ↔ WellFormedBatch batch := Iff.rfl
|
||
|
||
/-- Dropping a rejected sidecar never breaks a well-formed cover. -/
|
||
theorem wellFormedBatch_withoutRoads (batch : TopologyArtifactBatch)
|
||
(h : WellFormedBatch batch) : WellFormedBatch batch.withoutRoads := h
|
||
|
||
/-- The empty road layer is always well-formed, so a dropped sidecar leaves a valid batch. -/
|
||
theorem wellFormedRoads_withoutRoads (batch : TopologyArtifactBatch) :
|
||
WellFormedRoads batch.withoutRoads := by
|
||
refine ⟨?_, ?_, ?_, ?_⟩
|
||
· intro r hr; simp [TopologyArtifactBatch.withoutRoads] at hr
|
||
· intro r hr; simp [TopologyArtifactBatch.withoutRoads] at hr
|
||
· intro r hr; simp [TopologyArtifactBatch.withoutRoads] at hr
|
||
· intro source; simp [roadsFrom, TopologyArtifactBatch.withoutRoads]
|
||
|
||
/-- A well-formed road only ever leads to a cluster of the batch, so following it stays inside
|
||
the certified cover. -/
|
||
theorem wellFormedRoads_target_isCluster {batch : TopologyArtifactBatch}
|
||
(h : WellFormedRoads batch) {r : ClusterRoad} (hr : r ∈ batch.roads) :
|
||
namesCluster batch r.toClusterId :=
|
||
(h.1 r hr).2
|
||
|
||
end Yams.Topology
|