Pysmt
Satisfiability Modulo Theory and Python
If you’ve heard about z3 you probably know what SMT is already. If not, this piece of open source technology can solve equations, come up with counter examples to prove/disprove conjectures and even solve sudoku!
Existing Python Interfaces
There are things like pysmt, z3-solver and a few good tutorials. There is also typpete a python type inference solver written using this code.
What’s wrong with them?
In short, the design by contract APIs in python are not easy to use. The earliest effort seems to be from 2003. It’s called PEP 316.
It has examples that look like this
1
2
3
4
5
6
7
8
9
10
class circbuf:
def __init__(self, leng):
"""Construct an empty circular buffer.
pre: leng > 0
post[self]:
self.is_empty()
len(self.buf) == leng
"""
While this idea is good, the syntax leaves a lot to be desired. No IDE will assist you in editing it and if there are syntax errors, nothing breaks.
It feels like type comments in python2. The python3 type hints are much more robust.
How can I write verifiably correct code in python?
First, you can start using type hints for non-trivial cases. For trivial cases, you’re better off letting the type checker use inference and keep your code less noisy. This typically means making sure that every function has type hints.
However, the python type system can’t express all the constraints. If you have a user_id that’s a special type with the constraint 1 < user_id < 1000, nothing helps you enforce it today.
On researching the topic a bit, I came across two interesting projects crosshair and deal. Both methods are not well integrated into the type system and involve decorators and metaprogramming.
A transpiler based solution
The z3 python API to prove demorgan’s law looks like this:
1
2
3
4
5
6
p = Bool('pvar')
q = Bool('qvar')
demorgan1 = And(p, q) == Not(Or(Not(p), Not(q)))
solver1 = Solver()
solver1.add(Not(demorgan1))
solver1.check() == unsat
People don’t write python this way. Even if they did, they would do it separately from the production code to verify that the spec is valid. The problem with this approach is two fold:
- Not integrated into the type system
- The implementation and the spec could go out of sync
The P-programming language and Fstar are state of the art in this space. But they use syntax that’s unfamiliar to people working on popular programming languages such as Javascript and Python.
I’ve been thinking about what does it take to bring some of those capabilities to python
Transpiler backend
py2many now has a new backend called smt, which can transpile the following code:
1
2
3
4
5
6
def demorgan(a: bool, b: bool) -> bool:
(a and b) == (not ((not a) or (not b)))
assert not demorgan
check_sat()
to
1
2
3
4
5
6
7
8
9
10
(declare-const a Bool)
(declare-const b Bool)
(define-fun demorgan () Bool
(= (and a b) (not (or (not a) (not b)))))
(assert (not demorgan))
(check-sat)
z3 -smt2 accepts the above standardized output SMT LIB 2.0 and proves demorgan law.
Real World Usage
Most people aren’t interested in proving laws of boolean algebra. But they’d like to get their code checked by static checkers, which go beyond what type checkers such as mypy and pyright do.
1
2
3
4
5
6
7
8
9
10
11
class circbuf:
def __init__(self, leng):
"""Construct an empty circular buffer.
"""
if smt.pre:
assert leng > 0
if smt.post:
assert self.is_empty()
assert len(self.buf) == leng
When run through the transpiler, it would generate smt2 scripts, verify correctness and then generate python code without these assertions (or we use some type of runtime toggle to optimize away these static checks).
But some assertions are based on types, rather than functions. They need to be checked at all the places where the types are used.
1
2
3
4
5
6
7
8
9
10
11
UserId = NewType('UserId', int)
assert UserId > 0 and UserId < 1000
...
def delete_user(userid: UserId) -> None:
"""statically check that userid is in the right range"""
...
delete_user(120) # ok
delete_user(2000) # fails static check
Final Thoughts
In order for such an integrated type system + constraint solver to work, it has to produce good error messages. That could mean producing counter examples via get_model() and tightly integrate with the python type system.
On the flip side, you get refinement types, dependent types and a whole lot of functional programming goodies in python for free. This is not on the radar for most python type checkers today.