Skip to content

API.md

Latest commit

 

History

History
491 lines (358 loc) · 13.1 KB

API.md

File metadata and controls

491 lines (358 loc) · 13.1 KB

Framework API Documentation

This document provides comprehensive API documentation for the Hybrid Verification Framework.

Table of Contents

  1. System Interface API
  2. Adapter API
  3. Template Loader API
  4. Code Generation API
  5. Counterexample Conversion API
  6. Property Analysis API

System Interface API

Header: core/system_interface.h

The system interface defines the abstract operations that all protocol adapters must implement.

Types

SystemNode

typedef void* SystemNode;

Opaque pointer representing a system node. Implementation-specific.

SystemMessage

typedef void* SystemMessage;

Opaque pointer representing a system message. Implementation-specific.

SystemState

typedef enum {
    STATE_INITIAL,
    STATE_ACTIVE,
    STATE_TRANSITIONAL,
    STATE_TERMINATED
} SystemState;

Enumeration of system states.

SystemConfig

typedef struct {
    int num_nodes;              // Number of nodes in the system
    int max_rounds;             // Maximum number of execution rounds
    int timeout_range[2];       // [min_timeout, max_timeout]
    void* domain_specific;      // For domain-specific configurations
} SystemConfig;

Configuration structure for system parameters.

Function Pointer Types

init_node_fn

typedef void (*init_node_fn)(SystemNode* node, int id, SystemConfig* config);

Initialize a system node with the given ID and configuration.

Parameters:

  • node: Pointer to node to initialize
  • id: Node identifier
  • config: System configuration

process_msg_fn

typedef void (*process_msg_fn)(SystemNode* node, SystemMessage* msg, 
                               void* network_state, void* metrics);

Process an incoming message for a node.

Parameters:

  • node: Node receiving the message
  • msg: Message to process
  • network_state: Network state (can be NULL)
  • metrics: Metrics structure (can be NULL)

gen_msg_fn

typedef SystemMessage* (*gen_msg_fn)(SystemNode* node, int target_id);

Generate a message from a node to a target node.

Parameters:

  • node: Source node
  • target_id: Target node ID

Returns: Pointer to generated message (or NULL if no message)

should_send_msg_fn

typedef int (*should_send_msg_fn)(SystemNode* node, int target_id);

Determine if a node should send a message to a target.

Parameters:

  • node: Source node
  • target_id: Target node ID

Returns: Non-zero if message should be sent, 0 otherwise

verify_safety_fn

typedef int (*verify_safety_fn)(SystemNode* nodes[], int num_nodes, void* metrics);

Verify safety properties across all nodes.

Parameters:

  • nodes: Array of nodes
  • num_nodes: Number of nodes
  • metrics: Metrics structure (can be NULL)

Returns: Non-zero if safety properties hold, 0 if violated

verify_liveness_fn

typedef int (*verify_liveness_fn)(SystemNode* nodes[], int num_nodes, 
                                  int round, void* metrics);

Verify liveness properties across all nodes at a given round.

Parameters:

  • nodes: Array of nodes
  • num_nodes: Number of nodes
  • round: Current execution round
  • metrics: Metrics structure (can be NULL)

Returns: Non-zero if liveness properties hold, 0 if violated

verify_invariant_fn

typedef int (*verify_invariant_fn)(SystemNode* nodes[], int num_nodes, void* metrics);

Verify system invariants across all nodes.

Parameters:

  • nodes: Array of nodes
  • num_nodes: Number of nodes
  • metrics: Metrics structure (can be NULL)

Returns: Non-zero if invariants hold, 0 if violated

Memory Management Functions

typedef void (*alloc_nodes_fn)(SystemNode** nodes, int num_nodes);
typedef void (*free_nodes_fn)(SystemNode* nodes, int num_nodes);
typedef void (*free_msg_fn)(SystemMessage* msg);

Structures

SystemOperations

typedef struct {
    init_node_fn initialize_node;
    process_msg_fn process_message;
    gen_msg_fn generate_message;
    should_send_msg_fn should_send_message;
    verify_safety_fn verify_safety;
    verify_liveness_fn verify_liveness;
    verify_invariant_fn verify_invariant;
    alloc_nodes_fn alloc_nodes;
    free_nodes_fn free_nodes;
    free_msg_fn free_message;
} SystemOperations;

Structure containing all function pointers for system operations.

SystemDefinition

typedef struct {
    const char* name;           // Protocol name (e.g., "Raft", "Paxos")
    const char* domain;         // Domain type (e.g., "consensus", "concurrency")
    SystemOperations* ops;      // Function pointers to operations
    SystemConfig* default_config; // Default configuration
    void* property_definitions;  // Property definitions (implementation-specific)
} SystemDefinition;

Complete system definition linking operations to protocol metadata.

Factory Function Type

typedef SystemDefinition* (*protocol_factory_fn)(void);

Each adapter must provide a factory function that creates and returns a SystemDefinition*.

Helper Macros

#define SYSTEM_NODE(ptr, type) ((type*)(ptr))
#define SYSTEM_MSG(ptr, type) ((type*)(ptr))

Type-safe casting macros for converting opaque pointers to concrete types.

Adapter API

Creating a New Adapter

To create a new protocol adapter:

  1. Create adapter files:

    • examples/{protocol}/adapter/{protocol}_adapter.c - Implementation
    • examples/{protocol}/adapter/{protocol}_adapter.h - Header

  2. Implement all operations:

    • Implement all functions in SystemOperations
    • Create a factory function: create_{protocol}_definition()

  3. Example structure:

#include "core/system_interface.h"

// Implement all required functions
static void my_protocol_init_node(SystemNode* node, int id, SystemConfig* config) {
    // Implementation
}

static void my_protocol_process_message(SystemNode* node, SystemMessage* msg, 
                                        void* network_state, void* metrics) {
    // Implementation
}

// ... implement all other operations

// Create operations structure
static SystemOperations my_protocol_ops = {
    .initialize_node = my_protocol_init_node,
    .process_message = my_protocol_process_message,
    // ... assign all function pointers
};

// Factory function
SystemDefinition* create_my_protocol_definition(void) {
    SystemDefinition* def = malloc(sizeof(SystemDefinition));
    def->name = "MyProtocol";
    def->domain = "consensus";  // or "concurrency", "network", etc.
    def->ops = &my_protocol_ops;
    def->default_config = &my_protocol_default_config;
    return def;
}

Template Loader API

Class: TemplateLoader

Located in tools/template_loader.py

Constructor

loader = TemplateLoader(base_dir=None)

Parameters:

  • base_dir: Base directory path (default: parent of tools directory)

Methods

list_domains() -> List[str]

List all available domain templates.

Returns: List of domain names (e.g., ['distributed', 'concurrent', 'network'])

list_property_templates() -> List[str]

List all available property templates.

Returns: List of property template names

list_protocols() -> List[str]

List all available protocol configurations.

Returns: List of protocol names

load_domain_template(domain: str) -> Dict[str, Any]

Load a domain template by name.

Parameters:

  • domain: Domain name (e.g., 'distributed', 'concurrent', 'network')

Returns: Dictionary containing domain template data

Raises: FileNotFoundError if template not found

load_property_template(template_name: str) -> Dict[str, Any]

Load a property template by name.

Parameters:

  • template_name: Property template name (e.g., 'uniqueness', 'agreement')

Returns: Dictionary containing property template data

Raises: FileNotFoundError if template not found

load_protocol_config(protocol: str) -> Dict[str, Any]

Load a protocol configuration file.

Parameters:

  • protocol: Protocol name (e.g., 'raft')

Returns: Dictionary containing protocol configuration

Raises: FileNotFoundError if configuration not found

expand_property_template(template_name: str, variables: Dict[str, str]) -> Dict[str, str]

Expand a property template with variable substitutions.

Parameters:

  • template_name: Property template name
  • variables: Dictionary of variable substitutions

Returns: Dictionary with 'klee_code' and 'tla_code' keys containing expanded templates

Code Generation API

Property Generator

Class: PropertyGenerator

Located in tools/generate_properties.py

generate_properties(protocol: str, output_file: str = None) -> Dict[str, Any]

Generate property files (JSON, KLEE C, TLA+) for a protocol.

Parameters:

  • protocol: Protocol name
  • output_file: Optional output JSON file path

Returns: Dictionary with keys:

  • 'json': Path to generated JSON file
  • 'klee': Path to generated C file
  • 'tla': Path to generated TLA+ file
  • 'properties': Property definitions dictionary

KLEE Test Generator

Class: KLEETestGenerator

Located in tools/generate_klee_test.py

generate_harness(protocol: str, output_file: str = None) -> str

Generate KLEE test harness C file.

Parameters:

  • protocol: Protocol name
  • output_file: Optional output file path

Returns: Path to generated C file

TLA+ Spec Generator

Class: TLASpecGenerator

Located in tools/generate_tla_spec.py

generate_spec(protocol: str, output_file: str = None) -> str

Generate TLA+ specification file.

Parameters:

  • protocol: Protocol name
  • output_file: Optional output file path

Returns: Path to generated TLA+ file

Counterexample Conversion API

Module: verification.counterexample_converter

convert_klee_to_tla(klee_cex: Dict, protocol_config: Dict = None) -> Dict

Convert a KLEE counterexample to TLA+ format.

Parameters:

  • klee_cex: KLEE counterexample dictionary
  • protocol_config: Optional protocol configuration

Returns: Dictionary with:

  • 'source': 'KLEE'
  • 'tla_code': Generated TLA+ code
  • 'tla_format': Format description

convert_tla_to_klee(tla_cex: Dict, protocol_config: Dict = None) -> Dict

Convert a TLA+ counterexample to KLEE format.

Parameters:

  • tla_cex: TLA+ counterexample dictionary
  • protocol_config: Optional protocol configuration

Returns: Dictionary with:

  • 'source': 'TLA+'
  • 'klee_code': Generated KLEE initialization code
  • 'initial_values': Dictionary of initial values

`convert_counterexamples(klee_json_file: str = None, tla_json_file: str = None,

                        output_dir: str = 'verification', 
                        protocol_name: str = None) -> Dict`

Convert counterexamples from JSON files.

Parameters:

  • klee_json_file: Path to KLEE counterexamples JSON file
  • tla_json_file: Path to TLA+ counterexamples JSON file
  • output_dir: Output directory for converted files
  • protocol_name: Optional protocol name for protocol-specific conversion

Returns: Dictionary with conversion statistics

Command-line usage:

python verification/counterexample_converter.py \
    --klee-to-tla input.json \
    --output-dir output/ \
    --protocol raft

python verification/counterexample_converter.py \
    --tla-to-klee input.json \
    --output-dir output/ \
    --protocol raft

Property Analysis API

Module: synthesis.analyze_counterexample

analyze_counterexample(counterexample_file: str, protocol_name: str = None) -> Dict

Analyze counterexamples to identify property violations.

Parameters:

  • counterexample_file: Path to counterexample JSON file
  • protocol_name: Optional protocol name for protocol-specific analysis

Returns: Dictionary with:

  • 'total_count': Number of counterexamples analyzed
  • 'protocol': Protocol name (if specified)
  • 'analyses': List of analysis results, each containing:
    • 'violation': Violation information
    • 'candidate_property': Suggested property
    • 'pattern': Violation pattern

Command-line usage:

python synthesis/analyze_counterexample.py \
    counterexamples.json \
    --protocol raft

identify_property_violation(counterexample: Dict, protocol_config: Dict = None) -> Dict

Identify which property was violated in a counterexample.

Parameters:

  • counterexample: Counterexample dictionary
  • protocol_config: Optional protocol configuration

Returns: Dictionary with:

  • 'property': Property name
  • 'violation_type': 'Safety' or 'Liveness'
  • 'pattern': Violation pattern
  • 'description': Description of violation

Error Handling

  • File loading functions raise FileNotFoundError if files don't exist
  • JSON processing functions raise json.JSONDecodeError for malformed JSON
  • Code generation functions raise ValueError if required configuration is missing

See Also