agenticraft_foundation.protocols.specifications

Formal protocol specifications — property definitions for protocol verification.

Formal protocol specifications for verifying routing correctness.

Provides executable formal specifications following the pattern from specifications/consensus_spec.py.

Key properties: - ProtocolValidPath: all (u,v) in path use supported protocols - SemanticPreservation: meaning(m) = meaning(T_{p→p'}(m)) - OptimalRouting: no path with lower cost exists

ProtocolPropertyType

Bases: str, Enum

Types of protocol formal properties.

VALIDITY = 'validity' class-attribute instance-attribute

Path validity constraints

SEMANTIC = 'semantic' class-attribute instance-attribute

Semantic preservation constraints

OPTIMALITY = 'optimality' class-attribute instance-attribute

Optimality constraints

INVARIANT = 'invariant' class-attribute instance-attribute

Invariants that must always hold

ProtocolPropertyStatus

Bases: str, Enum

Status of protocol property verification.

ProtocolPropertyResult dataclass

Result of protocol property verification.

ATTRIBUTE	DESCRIPTION
property_name	Name of the property checked TYPE: str
property_type	Type of property TYPE: ProtocolPropertyType
status	Verification status TYPE: ProtocolPropertyStatus
message	Human-readable message TYPE: str
counterexample	Counterexample if violated TYPE: Any | None
details	Additional verification details TYPE: dict[str, Any]
timestamp	When verification was performed TYPE: float

is_satisfied()

Check if property was satisfied.

ProtocolFormalProperty

Bases: ABC

Base class for protocol formal properties.

Properties are executable specifications that can be checked against protocol routing states.

__init__(name, property_type)

Initialize property.

PARAMETER	DESCRIPTION
name	Property name TYPE: str
property_type	Type of property TYPE: ProtocolPropertyType

check(**kwargs) abstractmethod

Check if property holds.

RETURNS	DESCRIPTION
ProtocolPropertyResult	ProtocolPropertyResult with verification outcome

ProtocolValidPath

Bases: ProtocolFormalProperty

Protocol-valid path property.

Constraint: ∀ (u,v) ∈ π: pᵢ ∈ Φ(u,v)

Verifies that every edge in the path supports the protocol used on it.

__init__()

Initialize ProtocolValidPath property.

check(path=None, protocol_sequence=None, graph=None, **kwargs)

Check if path is protocol-valid.

PARAMETER	DESCRIPTION
path	Sequence of agent IDs TYPE: list[str] | None DEFAULT: None
protocol_sequence	Protocol used on each edge TYPE: list[ProtocolName] | None DEFAULT: None
graph	Protocol graph TYPE: ProtocolGraph | None DEFAULT: None

RETURNS	DESCRIPTION
ProtocolPropertyResult	ProtocolPropertyResult indicating validity

SemanticPreservation

Bases: ProtocolFormalProperty

Semantic preservation property.

Constraint: meaning(m) = meaning(T_{p→p'}(m))

Verifies that protocol translations preserve semantic meaning.

__init__(max_semantic_loss=0.1)

Initialize SemanticPreservation property.

PARAMETER	DESCRIPTION
max_semantic_loss	Maximum allowed semantic loss (0.0 to 1.0) TYPE: float DEFAULT: 0.1

check(route=None, semantic_loss=None, **kwargs)

Check if semantic preservation holds.

PARAMETER	DESCRIPTION
route	OptimalRoute with semantic_loss_estimate TYPE: OptimalRoute | None DEFAULT: None
semantic_loss	Direct semantic loss value (alternative to route) TYPE: float | None DEFAULT: None

RETURNS	DESCRIPTION
ProtocolPropertyResult	ProtocolPropertyResult indicating preservation

OptimalRouting

Bases: ProtocolFormalProperty

Optimal routing property.

Constraint: No path π' exists with cost(π') < cost(π)

Verifies that the chosen route is optimal among alternatives.

__init__(tolerance=0.001)

Initialize OptimalRouting property.

PARAMETER	DESCRIPTION
tolerance	Tolerance for floating-point comparison TYPE: float DEFAULT: 0.001

check(route=None, all_routes=None, **kwargs)

Check if route is optimal.

PARAMETER	DESCRIPTION
route	The route claimed to be optimal TYPE: OptimalRoute | None DEFAULT: None
all_routes	All possible routes for comparison TYPE: list[OptimalRoute] | None DEFAULT: None

RETURNS	DESCRIPTION
ProtocolPropertyResult	ProtocolPropertyResult indicating optimality

TranslationBoundProperty

Bases: ProtocolFormalProperty

Translation bound property.

Constraint: Number of protocol translations ≤ max_translations

Verifies that routing doesn't exceed translation limits.

__init__(max_translations=3)

Initialize TranslationBoundProperty.

PARAMETER	DESCRIPTION
max_translations	Maximum allowed translations TYPE: int DEFAULT: 3

check(route=None, num_translations=None, **kwargs)

Check if translation count is within bounds.

PARAMETER	DESCRIPTION
route	OptimalRoute to check TYPE: OptimalRoute | None DEFAULT: None
num_translations	Direct translation count (alternative) TYPE: int | None DEFAULT: None

RETURNS	DESCRIPTION
ProtocolPropertyResult	ProtocolPropertyResult indicating if bound holds

ProtocolResilience

Bases: ProtocolFormalProperty

k-Protocol resilience verification.

Theorem 1: A mesh achieves at most (|P|-1)-protocol resilience. Verifies that removing any k-1 protocols preserves graph connectivity.

This checks: for each subset S of protocols with |S| = k-1, removing all edges that ONLY support protocols in S still leaves the graph connected.

__init__(k=1)

Initialize ProtocolResilience property.

PARAMETER	DESCRIPTION
k	Resilience level to verify. The mesh is k-protocol-resilient if it remains connected when any k-1 protocols fail. TYPE: int DEFAULT: 1

check(graph=None, **kwargs)

Check if mesh is k-protocol-resilient.

PARAMETER	DESCRIPTION
graph	Protocol graph to verify TYPE: ProtocolGraph | None DEFAULT: None

RETURNS	DESCRIPTION
ProtocolPropertyResult	ProtocolPropertyResult indicating resilience status

ProtocolSpecification

Complete specification for protocol routing.

Combines all protocol properties and provides verification API.

__init__(max_semantic_loss=0.1, max_translations=3, custom_properties=None)

Initialize specification.

PARAMETER	DESCRIPTION
max_semantic_loss	Threshold for semantic preservation TYPE: float DEFAULT: 0.1
max_translations	Maximum allowed translations TYPE: int DEFAULT: 3
custom_properties	Additional custom properties TYPE: list[ProtocolFormalProperty] | None DEFAULT: None

verify(route, graph, all_routes=None)

Verify all properties for a route.

PARAMETER	DESCRIPTION
route	Route to verify TYPE: OptimalRoute
graph	Protocol graph TYPE: ProtocolGraph
all_routes	Alternative routes for optimality check TYPE: list[OptimalRoute] | None DEFAULT: None

RETURNS	DESCRIPTION
list[ProtocolPropertyResult]	List of property results

verify_validity(path, protocol_sequence, graph)

Verify only path validity.

PARAMETER	DESCRIPTION
path	Path to verify TYPE: list[str]
protocol_sequence	Protocols used TYPE: list[ProtocolName]
graph	Protocol graph TYPE: ProtocolGraph

RETURNS	DESCRIPTION
ProtocolPropertyResult	Validity property result

is_valid(route, graph)

Check if route satisfies all properties.

PARAMETER	DESCRIPTION
route	Route to check TYPE: OptimalRoute
graph	Protocol graph TYPE: ProtocolGraph

RETURNS	DESCRIPTION
bool	True if all properties satisfied

summary(route, graph, all_routes=None)

Generate verification summary.

PARAMETER	DESCRIPTION
route	Route to summarize TYPE: OptimalRoute
graph	Protocol graph TYPE: ProtocolGraph
all_routes	Alternative routes TYPE: list[OptimalRoute] | None DEFAULT: None

RETURNS	DESCRIPTION
str	Human-readable summary