Skip to content

Commit 0cd137e

Browse files
committed
feat(graphs): add canonical graph6 decoding and verification
1 parent 5e45a93 commit 0cd137e

6 files changed

Lines changed: 363 additions & 2 deletions

File tree

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
"""Typed graph6 operation and checker declaration."""
2+
3+
from __future__ import annotations
4+
5+
from pydantic import Field, StrictStr
6+
7+
from jacobian.capability_service import CapabilityDiagnostic
8+
from jacobian.checker_operations import ExactReplayCheckerDeclaration
9+
from jacobian.contracts.base import ContractModel
10+
from jacobian.domains._examples import example
11+
from jacobian.math.graphs.graph6 import Graph6DecodeValue, decode_graph6
12+
from jacobian.operation_bindings import inline_operation
13+
from jacobian.operations import OperationRefusalError, OperationSpec
14+
15+
16+
class Graph6DecodeRequest(ContractModel):
17+
graph6: StrictStr = Field(min_length=1, max_length=352)
18+
19+
20+
def _decode(request: Graph6DecodeRequest) -> Graph6DecodeValue:
21+
try:
22+
return decode_graph6(request.graph6)
23+
except ValueError as exc:
24+
raise OperationRefusalError(
25+
CapabilityDiagnostic(
26+
code="GRAPH6_DECODE_REFUSED",
27+
stage="graph6_decoding",
28+
message=str(exc),
29+
hint=(
30+
"Supply standard small-order graph6 (orders 0-62), optionally "
31+
"prefixed by >>graph6<<; sparse6, digraph6, extended headers, "
32+
"invalid lengths, characters, and padding are rejected."
33+
),
34+
)
35+
) from exc
36+
37+
38+
GRAPH6_CAPABILITIES = (
39+
inline_operation(
40+
OperationSpec(
41+
operation_id="graph.encoding.graph6.decode.compute",
42+
version="1",
43+
title="Decode canonical small-order graph6",
44+
description=(
45+
"Decode a headerless or standard-header graph6 string of order at "
46+
"most 62 using the column-major upper-triangle bit convention, "
47+
"returning sorted edges, degrees, and a canonical graph digest."
48+
),
49+
request_type=Graph6DecodeRequest,
50+
result_type=Graph6DecodeValue,
51+
execute=_decode,
52+
tags=("graph", "encoding", "graph6", "deterministic", "exact"),
53+
invocation_examples=(
54+
example(
55+
"triangle_graph6",
56+
"Decode the graph6 representation of the triangle graph.",
57+
{"graph6": "Bw"},
58+
),
59+
),
60+
)
61+
),
62+
)
63+
64+
GRAPH6_CHECKER_DECLARATIONS = (
65+
ExactReplayCheckerDeclaration(
66+
"graph.encoding.graph6.decode.compute",
67+
Graph6DecodeRequest,
68+
"check_graph6_decode",
69+
"graph.graph6-decode.standard-library-v1",
70+
entrypoint_module="jacobian_checkers.graph6",
71+
replay_method="standard-library graph6 bitstream replay",
72+
reason=(
73+
"operator-authorized standard-library checker independently decodes "
74+
"the graph6 bitstream without importing the producer"
75+
),
76+
verification_capability_id="graph.encoding.graph6.decode.verify",
77+
verification_title="Verify a canonical graph6 decode",
78+
verification_description=(
79+
"Independently replay the small-order graph6 header, upper-triangle "
80+
"bits, padding, sorted edges, degrees, and canonical graph digest."
81+
),
82+
verification_tags=("verification", "exact", "graph", "encoding", "graph6"),
83+
),
84+
)
85+
86+
__all__ = ["GRAPH6_CAPABILITIES", "GRAPH6_CHECKER_DECLARATIONS"]

src/jacobian/domains/graph_optimization/invariant_bundle.py

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@
77
from jacobian.domains.graph_optimization.checkers import (
88
GRAPH_INVARIANT_EXACT_REPLAY_CHECKERS,
99
)
10+
from jacobian.domains.graph_optimization.graph6 import (
11+
GRAPH6_CAPABILITIES,
12+
GRAPH6_CHECKER_DECLARATIONS,
13+
)
1014
from jacobian.domains.graph_optimization.invariants import (
1115
EXACT_GRAPH_INVARIANT_CAPABILITIES,
1216
)
@@ -66,7 +70,7 @@ def build_graph_invariant_bundle() -> DomainBundle:
6670
),
6771
),
6872
backend_version=f"networkx-{NETWORKX_VERSION};sympy-{SYMPY_VERSION}",
69-
capabilities=EXACT_GRAPH_INVARIANT_CAPABILITIES,
73+
capabilities=(*GRAPH6_CAPABILITIES, *EXACT_GRAPH_INVARIANT_CAPABILITIES),
7074
diagnostics=DomainDiagnostics(
7175
invalid_request=CapabilityDiagnostic(
7276
code="INVALID_GRAPH_INVARIANT_REQUEST",
@@ -75,5 +79,8 @@ def build_graph_invariant_bundle() -> DomainBundle:
7579
hint="Supply a canonical simple graph with at most 32 vertices.",
7680
)
7781
),
78-
checker_declarations=GRAPH_INVARIANT_EXACT_REPLAY_CHECKERS,
82+
checker_declarations=(
83+
*GRAPH6_CHECKER_DECLARATIONS,
84+
*GRAPH_INVARIANT_EXACT_REPLAY_CHECKERS,
85+
),
7986
)

src/jacobian/exact_domain_checkers.py

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@
7474
_ENTRYPOINT_PROVIDER_RUNTIME_KEYS = {
7575
"jacobian_checkers.exact_domain_operations": "python-flint",
7676
"jacobian_checkers.graph_exact_operations": "finite-graph",
77+
"jacobian_checkers.graph6": "graph6",
7778
"jacobian_checkers.exact_probability_operations": "finite-probability",
7879
"jacobian_checkers.recurrence_series": "combinatorics",
7980
"jacobian_checkers.additive_combinatorics": "combinatorics",
@@ -187,6 +188,15 @@ def install_exact_domain_checkers(
187188
"python-flint": exact_domain_checker_provider_runtime,
188189
"certified-snf": certified_snf_checker_provider_runtime,
189190
"finite-graph": graph_exact_checker_provider_runtime,
191+
"graph6": partial(
192+
source_provider_runtime,
193+
"jacobian.graph6-checker",
194+
version="1",
195+
entrypoint="jacobian_checkers.graph6:check_graph6_decode",
196+
install_tier=CapabilityInstallTier.T1,
197+
license_id="MIT",
198+
features=("standard-library-bitstream-replay", "clean-process-checker"),
199+
),
190200
"finite-probability": probability_exact_checker_provider_runtime,
191201
"combinatorics": combinatorics_exact_checker_provider_runtime,
192202
"poset": poset_exact_checker_provider_runtime,

src/jacobian/math/graphs/graph6.py

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
"""Canonical small-order graph6 decoding."""
2+
3+
from __future__ import annotations
4+
5+
from hashlib import sha256
6+
from typing import Literal, Self
7+
8+
from pydantic import Field, StrictInt, StrictStr, model_validator
9+
10+
from jacobian.canonical import canonicalize_json
11+
from jacobian.contracts.base import ContractModel
12+
from jacobian.contracts.common import Sha256Digest
13+
14+
15+
class Graph6Edge(ContractModel):
16+
first: StrictInt = Field(ge=0, le=62)
17+
second: StrictInt = Field(ge=0, le=62)
18+
19+
@model_validator(mode="after")
20+
def require_canonical_endpoints(self) -> Self:
21+
if self.first >= self.second:
22+
raise ValueError("graph6 edge endpoints must be strictly increasing")
23+
return self
24+
25+
26+
class Graph6DecodeValue(ContractModel):
27+
graph6: StrictStr = Field(min_length=1, max_length=352)
28+
order: StrictInt = Field(ge=0, le=62)
29+
edges: tuple[Graph6Edge, ...] = Field(max_length=1891)
30+
degrees: tuple[StrictInt, ...] = Field(max_length=62)
31+
graph_digest: Sha256Digest
32+
format: Literal["GRAPH6_SMALL_ORDER"] = "GRAPH6_SMALL_ORDER"
33+
bit_order: Literal["COLUMN_MAJOR_UPPER_TRIANGLE"] = (
34+
"COLUMN_MAJOR_UPPER_TRIANGLE"
35+
)
36+
37+
@model_validator(mode="after")
38+
def bind_dimensions(self) -> Self:
39+
if len(self.degrees) != self.order:
40+
raise ValueError("graph6 degree sequence must match graph order")
41+
pairs = tuple((edge.first, edge.second) for edge in self.edges)
42+
if pairs != tuple(sorted(pairs)) or len(pairs) != len(set(pairs)):
43+
raise ValueError("graph6 edges must be unique and sorted")
44+
if any(edge.second >= self.order for edge in self.edges):
45+
raise ValueError("graph6 edge endpoint exceeds graph order")
46+
expected = [0] * self.order
47+
for edge in self.edges:
48+
expected[edge.first] += 1
49+
expected[edge.second] += 1
50+
if tuple(expected) != self.degrees:
51+
raise ValueError("graph6 degree sequence does not match edges")
52+
return self
53+
54+
55+
def decode_graph6(encoded: str) -> Graph6DecodeValue:
56+
value = encoded[10:] if encoded.startswith(">>graph6<<") else encoded
57+
if not value or value[0] in {":", "&"}:
58+
raise ValueError("only standard graph6 is supported")
59+
codes = [ord(character) - 63 for character in value]
60+
if any(code < 0 or code > 63 for code in codes) or codes[0] == 63:
61+
raise ValueError("graph6 payload is malformed or uses an extended header")
62+
order = codes[0]
63+
bit_count = order * (order - 1) // 2
64+
if len(codes) != 1 + (bit_count + 5) // 6:
65+
raise ValueError("graph6 payload length does not match its order header")
66+
bits = [
67+
(code >> shift) & 1
68+
for code in codes[1:]
69+
for shift in range(5, -1, -1)
70+
]
71+
if any(bits[bit_count:]):
72+
raise ValueError("unused graph6 padding bits must be zero")
73+
pairs = [(first, second) for second in range(1, order) for first in range(second)]
74+
edges = tuple(
75+
Graph6Edge(first=first, second=second)
76+
for first, second in sorted(
77+
pair for pair, bit in zip(pairs, bits, strict=False) if bit
78+
)
79+
)
80+
degrees = [0] * order
81+
for edge in edges:
82+
degrees[edge.first] += 1
83+
degrees[edge.second] += 1
84+
digest_payload = {
85+
"order": order,
86+
"edges": [[edge.first, edge.second] for edge in edges],
87+
}
88+
return Graph6DecodeValue(
89+
graph6=value,
90+
order=order,
91+
edges=edges,
92+
degrees=tuple(degrees),
93+
graph_digest="sha256:" + sha256(canonicalize_json(digest_payload)).hexdigest(),
94+
)
95+
96+
97+
__all__ = ["Graph6DecodeValue", "Graph6Edge", "decode_graph6"]

src/jacobian_checkers/graph6.py

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
"""Independent graph6 replay using only the standard library."""
2+
3+
from __future__ import annotations
4+
5+
import hashlib
6+
import json
7+
from typing import Any
8+
9+
from jacobian_checkers.bound_artifacts import bound_request
10+
11+
12+
def _reject(detail: str) -> dict[str, Any]:
13+
return {
14+
"accepted": False,
15+
"conclusion": "UNKNOWN",
16+
"arithmetic": "EXACT_INTEGER",
17+
"method": "DIRECT_WITNESS",
18+
"coverage": "NOT_APPLICABLE",
19+
"detail": detail,
20+
}
21+
22+
23+
def _accept(detail: str) -> dict[str, Any]:
24+
return {
25+
"accepted": True,
26+
"conclusion": "TRUE",
27+
"arithmetic": "EXACT_INTEGER",
28+
"method": "DIRECT_WITNESS",
29+
"coverage": "NOT_APPLICABLE",
30+
"detail": detail,
31+
}
32+
33+
34+
def check_graph6_decode(request: object) -> dict[str, Any]:
35+
try:
36+
source, result = bound_request(
37+
request,
38+
operation_id="graph.encoding.graph6.decode.compute",
39+
witness_format="graph.graph6-decode.standard-library-v1",
40+
)
41+
if set(source) != {"graph6"} or not isinstance(source["graph6"], str):
42+
raise ValueError("graph6 source is malformed")
43+
value = source["graph6"]
44+
value = value[10:] if value.startswith(">>graph6<<") else value
45+
if not value or value[0] in {":", "&"}:
46+
raise ValueError("unsupported graph encoding")
47+
codes = [ord(character) - 63 for character in value]
48+
if any(code < 0 or code > 63 for code in codes) or codes[0] == 63:
49+
raise ValueError("malformed or extended graph6 encoding")
50+
order = codes[0]
51+
bit_count = order * (order - 1) // 2
52+
if len(codes) != 1 + (bit_count + 5) // 6:
53+
raise ValueError("graph6 length does not match order")
54+
bits = [
55+
(code >> shift) & 1
56+
for code in codes[1:]
57+
for shift in range(5, -1, -1)
58+
]
59+
if any(bits[bit_count:]):
60+
raise ValueError("graph6 padding bits are nonzero")
61+
pairs = [(first, second) for second in range(1, order) for first in range(second)]
62+
edges = sorted(pair for pair, bit in zip(pairs, bits, strict=False) if bit)
63+
degrees = [0] * order
64+
for first, second in edges:
65+
degrees[first] += 1
66+
degrees[second] += 1
67+
digest_payload = json.dumps(
68+
{"edges": [list(edge) for edge in edges], "order": order},
69+
allow_nan=False,
70+
ensure_ascii=False,
71+
separators=(",", ":"),
72+
sort_keys=True,
73+
).encode()
74+
expected = {
75+
"graph6": value,
76+
"order": order,
77+
"edges": [{"first": first, "second": second} for first, second in edges],
78+
"degrees": degrees,
79+
"graph_digest": "sha256:" + hashlib.sha256(digest_payload).hexdigest(),
80+
"format": "GRAPH6_SMALL_ORDER",
81+
"bit_order": "COLUMN_MAJOR_UPPER_TRIANGLE",
82+
}
83+
if result != expected:
84+
return _reject("candidate does not match independent graph6 replay")
85+
return _accept("independent graph6 bitstream replay accepted candidate")
86+
except (KeyError, TypeError, ValueError, OverflowError):
87+
return _reject("malformed, unsupported, or mismatched checker request")
88+
89+
90+
__all__ = ["check_graph6_decode"]

0 commit comments

Comments
 (0)