Ctrl + k

or run

tessl search
Log in

Version

Workspace
tessl
Visibility
Public
Created
Last updated
Describes
pypipkg:pypi/crosshair-tool@0.0.x
tile.json

tessl/pypi-crosshair-tool

tessl install tessl/pypi-crosshair-tool@0.0.0

Analyze Python code for correctness using symbolic execution and SMT solving to automatically find counterexamples for functions with type annotations and contracts.

Agent Success

Agent success rate when using this tile

86%

Improvement

Agent success rate improvement when using this tile compared to baseline

1.25x

Baseline

Agent success rate without this tile

69%

task.mdevals/scenario-6/

Generic Type Utilities

A Python library providing utility functions that work with generic types and TypeVars. All functions include contracts that can be verified using symbolic execution.

Capabilities

Swaps elements in a typed pair

  • Swapping two elements of the same type in a tuple returns them in reversed order @test
  • Attempting to create a tuple with mismatched types for the same TypeVar parameter fails contract verification @test

Processes numeric values with type preservation

  • Multiplying numeric values preserves the input type (int stays int, float stays float) @test
  • Using bounded TypeVars correctly restricts inputs to specified types only @test

Retrieves and transforms generic list elements

  • Extracting the first element from a typed list returns the correct element type @test
  • Transforming a list with a default value maintains consistent element types throughout @test

Implementation

@generates

API

from typing import TypeVar, Tuple, List, Union

T = TypeVar('T')
NumericT = TypeVar('NumericT', int, float)

def swap_pair(pair: Tuple[T, T]) -> Tuple[T, T]:
    """
    Swaps the two elements in a pair tuple.

    pre: len(pair) == 2
    post: __return__[0] == pair[1] and __return__[1] == pair[0]
    """
    pass

def process_numeric(value: NumericT, multiplier: NumericT) -> NumericT:
    """
    Multiplies a numeric value by a multiplier of the same numeric type.

    pre: isinstance(value, (int, float)) and isinstance(multiplier, (int, float))
    post: isinstance(__return__, type(value))
    """
    pass

def get_first(items: List[T]) -> T:
    """
    Returns the first element from a non-empty list.

    pre: len(items) > 0
    post: __return__ == items[0]
    """
    pass

def transform_list(items: List[T], default: T) -> List[T]:
    """
    Transforms a list by replacing empty positions with a default value.
    Returns a list of the same type.

    pre: len(items) >= 0
    post: len(__return__) == len(items)
    post: all(isinstance(x, type(default)) for x in __return__)
    """
    pass

Dependencies { .dependencies }

crosshair-tool { .dependency }

Provides symbolic execution and contract verification capabilities for Python code.