Custom Type Plugin for Contract Verification

Build a plugin that extends a symbolic execution tool to support custom contract verification for a domain-specific type.

You are building support for a Coordinate class that represents geographic coordinates with latitude and longitude values. The plugin must enable symbolic analysis of functions that use this custom type.

Requirements

Custom Type Support

Implement a plugin that registers symbolic value creation for the Coordinate type. The plugin should:

• Create symbolic coordinate instances with constrained latitude ([-90, 90]) and longitude ([-180, 180]) values
• Support symbolic execution of coordinate operations
• Enable the tool to generate test inputs using coordinate values

Contract Registration

Add programmatic contract registration for a third-party function calculate_distance(coord1, coord2) that computes distance between coordinates. Register contracts that specify:

• Precondition: Both arguments must be valid Coordinate instances
• Postcondition: Result must be non-negative
• Use the appropriate registration function from the tool's API

Test Cases

• Given a function find_nearest(target, locations) that returns the closest location to a target coordinate, the plugin enables finding counterexamples when the function violates its postcondition. @test
• The symbolic Coordinate type generates values with latitude constrained to [-90, 90] and longitude constrained to [-180, 180]. @test
• Registered contracts for calculate_distance are enforced during analysis, catching violations where the function returns negative distances. @test

Implementation

@generates

API

class Coordinate:
    """Represents a geographic coordinate with latitude and longitude."""
    def __init__(self, lat: float, lon: float):
        pass

    @property
    def lat(self) -> float:
        pass

    @property
    def lon(self) -> float:
        pass

def calculate_distance(coord1: Coordinate, coord2: Coordinate) -> float:
    """Calculate distance between two coordinates in kilometers."""
    pass

def find_nearest(target: Coordinate, locations: list[Coordinate]) -> Coordinate:
    """
    Find the nearest coordinate from a list of locations.

    post: __return__ in locations
    post: all(calculate_distance(target, __return__) <= calculate_distance(target, loc) for loc in locations)
    """
    pass

def setup_plugin():
    """
    Configure the plugin by registering symbolic type creators and contracts.
    This function should be called to initialize the plugin.
    """
    pass

Dependencies { .dependencies }

crosshair-tool { .dependency }

Provides symbolic execution and contract verification capabilities.