Back to all posts
2024-04-14

lslpy: A python library for contracts, property-based testing, and symbolic execution

Code
python program verification

lslpy is a library that enables contracts, property-based randomized testing, and verification via symbolic execution in Python, inspired by Logical Student Language (LSL). I wrote lslpy while taking CS2800 with Daniel Patterson. lslpy implements the teaching language (LSL) developed for the course through Python's type hinting syntax.

lslpy makes use of python's existing type-hinting system to define contracts. To define a contract for a function using lslpy, all we need to do is decorate the function with contract and add Contract "type hints" for each of its arguments and return:

from lslpy import contract
from lslpy.contracts import Natural, Real

@contract
def divide(x: Natural, y: Natural) -> Real:
    return x / y

With the function contract defined, the arguments and the return value will be checked every time the function is called. So, if we run divide(1, 2):

>>> divide(1, 2)
>>> 0.5

we get 0.5 (as expected). However, if we call the function with inputs that do not satisfy the contract, a ContractViolation is raised:

>>> divide(1, -1)
lslpy.contracts.exceptions.ContractViolation: divide expected (Natural, Natural), got (1, -1)

We can also check the contract with randomized testing:

>>> from lslpy import check_contract
>>> check_contract(divide)
ZeroDivisionError: division by zero

However, as we can see, a ZeroDivisionError is raised here. 0 is a Natural, and when divide's contract was being checked, 0 must have been passed as the argument y, resulting in division by zero.

To get around this, we can use lslpy's support for custom contracts to define a NonZeroInt contract for y. To define a custom contract, we need to create an instance of an Immediate contract (a contract which can be checked immediately) with two functions:

  • A check function which takes in a value x and returns True if the value satisfies the contract.
  • A generate function which takes in an integer fuel and generates a value that satisfies the contract.

Here is a possible implementation of NonZeroInt:

from lslpy.contracts.primitives import Immediate

NonZeroInt = Immediate(
    check=lambda x: isinstance(x, int) and x != 0,
    generate=lambda fuel: random.choice(list(range(1, fuel+1)) + list(range(-fuel, 0))),
)

With this new contract defined, we can rewrite divide's function contract:

@contract
def divide(x: Natural, y: NonZeroInt) -> Real:
    return x / y

Now check_contract will pass:

>>> check_contract(divide)
>>>

lslpy supports contracts for higher order functions. To write a higher order function contract, we invoke the familiar Callable contract which uses the same syntax as python's typing.Callable. If unfamiliar, typing.Callable takes two arguments: a list of types for each function argument, and a type for the function's return type. The only difference is that lslpy's Callable takes Contracts instead of types.

For example, the contract for any_map is defined like so:

from lslpy import contract
from lslpy.contracts import Callable, Any, List

@contract
def any_map(f: Callable[[Any], Any], lst: List[Any]) -> List[Any]:
	return [f(x) for x in lst]

But we can be more specific and implement a string to integer map:

from lslpy.contracts import String, Integer

@contract
def string_to_int_map(f: Callable[[String], Integer], lst: List[String]) -> List[Integer]:
	return [f(x) for x in lst]

Ideally, we could write a parametric contract for map :

@contract
def map(f: Callable[[X], Y], lst: List[X]) -> List[Y]:
	return [f(x) for x in lst]
	...

but lslpy currently doesn't support parametric contracts.

With the ability to write contracts, we can define and check properties of functions.

Let's say we have implemented a function my_reverse which reverses a list of integers:

from lslpy import contract
from lslpy.contracts import List, Integer

@contract
def my_reverse(l: List[Integer]) -> List[Integer]:
    l.reverse()
    return l

It should be true that for any two lists l1 and l2, calling my_reverse on l2 appended to l1 produces the same list as appending my_reverse(l1) to my_reverse(l2).

We can express this property as a contracted function in lslpy:

@contract
def my_reverse_prop(l1: List[Integer], l2: List[Integer]) -> Constant[True]:
    return my_reverse(l1 + l2) == my_reverse(l2) + my_reverse(l1)

To check the property, we call check_contract on the contracted function:

>>> from lslpy import check_contract
>>> check_contract(my_reverse_prop)
>>>

In addition to randomized testing to check properties, lslpy is able to verify some properties using symbolic execution.

Take a theoretical function called bad_mult, for example:

from lslpy import contract
from lslpy.contracts import Integer

@contract
def bad_mult(x: Integer, y: Integer) -> Integer:
    return 0 if x == 10456 else (x * y)

If x is 10456, bad_mult returns 0, otherwise it behaves correctly and returns x * y. Let's write a property that says that bad_mult(x, y) must always equal x * y:

from lslpy.contracts import Constant

@contract
def bad_mult_prop(x: Integer, y: Integer) -> Constant[True]:
    return bad_mult(x, y) == x * y

If we check the contract through randomized testing, it is highly unlikely we will find the counterexample that breaks the contract (where x = 10456):

>>> from lslpy import check_contract
>>> check_contract(bad_mult_prop)
>>>

Sure enough, check_contract passes.

Instead, let's try to verify the contract using lslpy's verify_contract function. lslpy implements verify_contract by parsing the the abstract syntax tree (AST) of the contracted function and its contract is into a Z3 expression which can then be proved, or used to find a counterexample:

>>> from lslpy import verify_contract
>>> verify_contract(bad_mult_prop, globals())
lslpy.contracts.exceptions.ContractViolation: Found counterexample: bad_mult_prop(y = -7651, x = 10456)

In its current state, in order for lslpy to verify a function's contract, the function must be a single expression and have a Constant return contract.