-
Notifications
You must be signed in to change notification settings - Fork 1
core: Graph substrate skeleton β ZSet-backed retraction-native (8th graduation) #317
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. Weβll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| @@ -0,0 +1,172 @@ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| namespace Zeta.Core | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// **Graph β ZSet-backed retraction-native graph substrate.** | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// A `Graph<'N>` is a structural wrapper around `ZSet<'N * 'N>`: | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// every edge is an entry in the underlying ZSet with a signed | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// `Weight`. Add-edge is a ZSet add; remove-edge is a ZSet sub. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// Net-zero entries compact by the existing ZSet consolidation | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// pass (Spine-backed when persisted). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// **Design contract:** `docs/DECISIONS/2026-04-24-graph- | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// substrate-zset-backed-retraction-native.md` (Otto-123 ADR) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// codifies the 5 tightness properties: ZSet-backed, first-class | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// event support, retractable, storage-format tight, operator- | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// algebra composable. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// **Attribution.** | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// * Aaron β design bar ("tight in all aspects") Otto-121 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// * Amara β formalization (11th + 12th + 13th + 14th ferries | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// + validation-bar Otto-122 "can it detect a dumb cartel in | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// a toy simulation?") | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// * Otto β implementation (8th graduation under Otto-105 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// cadence; first module that completes a cross-ferry arc | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// from concept to running substrate) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// **Scope of this first graduation.** Core type + minimal | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// mutation operators + node/edge accessors + retraction- | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// conservation property test. Detection primitives | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// (`largestEigenvalue`, `modularityScore`) and toy cartel | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// detector ship in follow-up PRs composing on this | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// foundation. Splitting across multiple PRs per Otto-105 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Comment on lines
+13
to
+32
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| /// substrate-zset-backed-retraction-native.md` (Otto-123 ADR) | |
| /// codifies the 5 tightness properties: ZSet-backed, first-class | |
| /// event support, retractable, storage-format tight, operator- | |
| /// algebra composable. | |
| /// | |
| /// **Attribution.** | |
| /// * Aaron β design bar ("tight in all aspects") Otto-121 | |
| /// * Amara β formalization (11th + 12th + 13th + 14th ferries | |
| /// + validation-bar Otto-122 "can it detect a dumb cartel in | |
| /// a toy simulation?") | |
| /// * Otto β implementation (8th graduation under Otto-105 | |
| /// cadence; first module that completes a cross-ferry arc | |
| /// from concept to running substrate) | |
| /// | |
| /// **Scope of this first graduation.** Core type + minimal | |
| /// mutation operators + node/edge accessors + retraction- | |
| /// conservation property test. Detection primitives | |
| /// (`largestEigenvalue`, `modularityScore`) and toy cartel | |
| /// detector ship in follow-up PRs composing on this | |
| /// foundation. Splitting across multiple PRs per Otto-105 | |
| /// substrate-zset-backed-retraction-native.md` (ADR record) | |
| /// codifies the 5 tightness properties: ZSet-backed, first-class | |
| /// event support, retractable, storage-format tight, operator- | |
| /// algebra composable. | |
| /// | |
| /// **Attribution.** | |
| /// * Architect β design bar ("tight in all aspects") | |
| /// * Research courier β formalization across the ferry sequence | |
| /// and validation bar ("can it detect a dumb cartel in a toy | |
| /// simulation?") | |
| /// * Human maintainer β implementation under the small- | |
| /// graduation cadence; first module that completes a cross- | |
| /// ferry arc from concept to running substrate | |
| /// | |
| /// **Scope of this first graduation.** Core type + minimal | |
| /// mutation operators + node/edge accessors + retraction- | |
| /// conservation property test. Detection primitives | |
| /// (`largestEigenvalue`, `modularityScore`) and toy cartel | |
| /// detector ship in follow-up PRs composing on this | |
| /// foundation. Splitting across multiple PRs per the |
Copilot
AI
Apr 24, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P2: The example call form in the doc comment doesnβt match the actual parameter order. edgeWeight is defined as edgeWeight source target g, but the comment says edgeWeight g source target. Update the comment to match the signature so callers arenβt misled.
| /// `edgeWeight g source target` β the signed multiplicity | |
| /// `edgeWeight source target g` β the signed multiplicity |
Copilot
AI
Apr 24, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P2: The example call form in the doc comment doesnβt match the actual parameter order. addEdge is defined as addEdge source target weight g, but the comment says addEdge g source target weight. Update the comment to match the signature.
Copilot
AI
Apr 24, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P1: addEdge/removeEdge only special-case weight = 0L. If a caller passes a negative weight, addEdge will effectively remove and still emit EdgeAdded(β¦, negativeWeight), and removeEdge will effectively add (double-negation). Either validate/normalize weights (e.g., require weight > 0L and reinterpret negative weights consistently) or adjust the API/event naming to explicitly accept signed deltas.
Copilot
AI
Apr 24, 2026
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P2: The example call form in the doc comment doesnβt match the actual parameter order. removeEdge is defined as removeEdge source target weight g, but the comment says removeEdge g source target weight. Update the comment to match the signature.
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,165 @@ | ||
| module Zeta.Tests.Algebra.GraphTests | ||
|
|
||
| open FsUnit.Xunit | ||
| open global.Xunit | ||
| open Zeta.Core | ||
|
|
||
|
|
||
| // βββ empty + basic accessors βββββββββ | ||
|
|
||
| [<Fact>] | ||
| let ``empty graph has zero edges and zero nodes`` () = | ||
| let g : Graph<int> = Graph.empty | ||
| Graph.isEmpty g |> should equal true | ||
| Graph.edgeCount g |> should equal 0 | ||
| Graph.nodeCount g |> should equal 0 | ||
|
|
||
| [<Fact>] | ||
| let ``edgeWeight returns 0 for absent edge`` () = | ||
| let g : Graph<int> = Graph.empty | ||
| Graph.edgeWeight 1 2 g |> should equal 0L | ||
|
|
||
|
|
||
| // βββ addEdge βββββββββ | ||
|
|
||
| [<Fact>] | ||
| let ``addEdge sets edge weight and emits EdgeAdded event`` () = | ||
| let (g, events) = Graph.addEdge 1 2 5L Graph.empty | ||
| Graph.edgeWeight 1 2 g |> should equal 5L | ||
| events |> should equal [ EdgeAdded(1, 2, 5L) ] | ||
|
|
||
| [<Fact>] | ||
| let ``addEdge with zero weight is a no-op`` () = | ||
| let (g, events) = Graph.addEdge 1 2 0L Graph.empty | ||
| Graph.isEmpty g |> should equal true | ||
| events |> should equal ([]: GraphEvent<int> list) | ||
|
|
||
| [<Fact>] | ||
| let ``addEdge accumulates multi-edge weight`` () = | ||
| // Multi-edges are supported via ZSet signed-weight: | ||
| // two adds on the same edge sum to multiplicity 7. | ||
| let (g1, _) = Graph.addEdge 1 2 3L Graph.empty | ||
| let (g2, _) = Graph.addEdge 1 2 4L g1 | ||
| Graph.edgeWeight 1 2 g2 |> should equal 7L | ||
| Graph.edgeCount g2 |> should equal 1 | ||
|
|
||
|
|
||
| // βββ removeEdge / retraction-native βββββββββ | ||
|
|
||
| [<Fact>] | ||
| let ``removeEdge subtracts weight and emits EdgeRemoved event`` () = | ||
| let (g1, _) = Graph.addEdge 1 2 5L Graph.empty | ||
| let (g2, events) = Graph.removeEdge 1 2 5L g1 | ||
| Graph.edgeWeight 1 2 g2 |> should equal 0L | ||
| Graph.isEmpty g2 |> should equal true | ||
| events |> should equal [ EdgeRemoved(1, 2, 5L) ] | ||
|
|
||
| [<Fact>] | ||
| let ``removeEdge partial retraction leaves remainder`` () = | ||
| // Retraction-native: remove 3 from an edge of weight 5 | ||
| // leaves weight 2, not "edge deleted". | ||
| let (g1, _) = Graph.addEdge 1 2 5L Graph.empty | ||
| let (g2, _) = Graph.removeEdge 1 2 3L g1 | ||
| Graph.edgeWeight 1 2 g2 |> should equal 2L | ||
| Graph.edgeCount g2 |> should equal 1 | ||
|
|
||
| [<Fact>] | ||
| let ``retraction-conservation: addEdge then removeEdge restores empty`` () = | ||
| // The load-bearing property from the ADR: apply(delta) | ||
| // followed by apply(-delta) restores prior state modulo | ||
| // compaction metadata. | ||
| let (g1, _) = Graph.addEdge 1 2 7L Graph.empty | ||
| let (g2, _) = Graph.removeEdge 1 2 7L g1 | ||
| Graph.isEmpty g2 |> should equal true | ||
|
|
||
| [<Fact>] | ||
| let ``removeEdge on absent edge produces net-negative weight`` () = | ||
| // Remove-before-add is legal β ZSet signed-weight means | ||
| // the result is an anti-edge (negative multiplicity). | ||
| // Adding it later will cancel. This is what makes | ||
| // retraction-native counterfactuals O(|delta|). | ||
| let (g, _) = Graph.removeEdge 1 2 3L Graph.empty | ||
| Graph.edgeWeight 1 2 g |> should equal -3L | ||
|
|
||
|
|
||
| // βββ nodes + neighbors βββββββββ | ||
|
|
||
| [<Fact>] | ||
| let ``nodes derives from edge endpoints`` () = | ||
| let g = | ||
| Graph.fromEdgeSeq [ | ||
| (1, 2, 1L) | ||
| (2, 3, 1L) | ||
| (3, 1, 1L) | ||
| ] | ||
| Graph.nodes g |> should equal (Set.ofList [1; 2; 3]) | ||
| Graph.nodeCount g |> should equal 3 | ||
|
|
||
| [<Fact>] | ||
| let ``outNeighbors lists target nodes and weights`` () = | ||
| let g = | ||
| Graph.fromEdgeSeq [ | ||
| (1, 2, 3L) | ||
| (1, 3, 5L) | ||
| (2, 3, 1L) | ||
| ] | ||
| let ns = Graph.outNeighbors 1 g | ||
| ns |> should equal [ (2, 3L); (3, 5L) ] | ||
|
|
||
| [<Fact>] | ||
| let ``inNeighbors is dual of outNeighbors`` () = | ||
| let g = | ||
| Graph.fromEdgeSeq [ | ||
| (1, 3, 5L) | ||
| (2, 3, 1L) | ||
| ] | ||
| let ns = Graph.inNeighbors 3 g | ||
| ns |> List.sortBy fst |> should equal [ (1, 5L); (2, 1L) ] | ||
|
|
||
| [<Fact>] | ||
| let ``degree sums in+out edge weights`` () = | ||
| let g = | ||
| Graph.fromEdgeSeq [ | ||
| (1, 2, 3L) // out-edge for 1 | ||
| (2, 1, 4L) // in-edge for 1 | ||
| (1, 3, 5L) // out-edge for 1 | ||
| ] | ||
| Graph.degree 1 g |> should equal (3L + 4L + 5L) | ||
|
|
||
|
|
||
| // βββ self-loop support βββββββββ | ||
|
|
||
| [<Fact>] | ||
| let ``self-loop is a legal edge (source = target)`` () = | ||
| let (g, _) = Graph.addEdge 1 1 5L Graph.empty | ||
| Graph.edgeCount g |> should equal 1 | ||
| Graph.edgeWeight 1 1 g |> should equal 5L | ||
|
|
||
| [<Fact>] | ||
| let ``self-loop counts twice in degree (once in, once out)`` () = | ||
| let (g, _) = Graph.addEdge 1 1 3L Graph.empty | ||
| Graph.degree 1 g |> should equal 6L // 3 in + 3 out | ||
|
|
||
|
|
||
| // βββ fromEdgeSeq βββββββββ | ||
|
|
||
| [<Fact>] | ||
| let ``fromEdgeSeq sums duplicate edges`` () = | ||
| let g = | ||
| Graph.fromEdgeSeq [ | ||
| (1, 2, 3L) | ||
| (1, 2, 4L) | ||
| ] | ||
| Graph.edgeWeight 1 2 g |> should equal 7L | ||
| Graph.edgeCount g |> should equal 1 | ||
|
|
||
| [<Fact>] | ||
| let ``fromEdgeSeq drops zero-weight triples`` () = | ||
| let g = | ||
| Graph.fromEdgeSeq [ | ||
| (1, 2, 0L) | ||
| (2, 3, 1L) | ||
| (3, 4, 0L) | ||
| ] | ||
| Graph.edgeCount g |> should equal 1 | ||
| Graph.edgeWeight 2 3 g |> should equal 1L |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
P1: The βDesign contractβ comment labels the linked ADR as βOtto-123 ADRβ, but the referenced file (docs/DECISIONS/2026-04-24-graph-substrate-zset-backed-retraction-native.md) doesnβt use that identifier. Consider removing the βOtto-123β label or aligning it with the ADRβs actual title/identifier to avoid confusing cross-references.