Arithmetic Comparison of Algebraic Datatypes

[adsharma]

I'm trying to arrange fixed width integer types in a separate type hierarchy for a type checker.

>>> mytype = Datatype('Type')
>>> mytype.declare("u8")
>>> mytype.declare("u16")
>>> m = mytype.create()
>>> x = Const("x", m)
>>> x >= 0
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: '>=' not supported between instances of 'DatatypeRef' and 'int'

Such comparison is of course possible with IntSort/ArithSort. Looking for advice on how to get around this error.

[adsharma]

This seems to work. Would love to get feedback on if this is the right way to express the constraints.

mytype = Datatype('Type')
mytype.declare("u8", ("val", IntSort()))
mytype.declare("u16", ("val", IntSort()))
m = mytype.create()
u8 = m.u8
u16 = m.u16
val = m.val

u8v = Const("u8", m)
u16v = Const("u16", m)

axioms = [ 
  val(u8v) >= 0, 
  val(u8v) <  (1 << 8),
  val(u16v) >= 0, 
  val(u16v) <  (1 << 16),
]

[NikolajBjorner]

This formulation doesn't capture your intent. You want:

axioms = [ForAll(ub, Implies(m.is_u8(ub), And(0 <= val(ub), val(ub) < (1 << 8))),
...

[adsharma]

Thank you for pointing me in the right direction. I noticed ForAll, but couldn't figure out how to use it correctly based on documentation. Here is what I tried:

from z3 import *

mytype = Datatype('Type')
mytype.declare("u8", ("u8val", IntSort()))
mytype.declare("u16", ("u16val", IntSort()))
m = mytype.create()
u8 = m.u8
u16 = m.u16
u8val = m.u8val
u16val = m.u16val

ub = Const("u8", m)
us = Const("u16", m)

axioms = [
  ForAll(ub, Implies(m.is_u8(ub), And(0 <= u8val(ub), u8val(ub) < (1 << 8)))),
  ForAll(us, Implies(m.is_u16(us), And(0 <= u16val(us), u16val(us) < (1 << 16)))),
  u8val(ub) == 100,
  u16val(us) == 300,
]

s = Solver()
#s.set(auto_config=False, mbqi=False)
print(s.check(*axioms))
print(s.model())

Prints unsat for me. I was expecting it to print sat with [u8=u8(100), u16=u16(300)]. My objective is to type check python code:

u1: u8 = 100  # ok
u2: u8 = -10  # error

What am I doing wrong?

[adsharma]

Uncommenting this line:

#s.set(auto_config=False, mbqi=False)

and using:

axioms = [
  ForAll(ub, Implies(m.is_u8(ub), And(0 <= u8val(ub), u8val(ub) < (1 << 8)))),
  ForAll(us, Implies(m.is_u16(us), And(0 <= u16val(us), u16val(us) < (1 << 16)))),
  ub == u8(100),
  us == u16(300)
]

works better.

unknown
[u16 = u16(300), u8 = u8(100)]

If I change the numbers to something out of range, I get unsat, which is good.

If this is the right direction, how can I get the unknown to become sat?

[adsharma]

I played around with dafny (which I read uses z3 under the covers).

type u8 = x: int | 0 <= x < 255
type u16 = x: int | 0 <= x < 65536

has the intended effect in dafny. I couldn't figure out from the dafny source code if dafny passes these constraints to z3 or solves them on its own. Any pointers to how dafny handles these constraints would be great, since I'm trying to replicate similar functionality in python.

[adsharma]

I made some progress on this via dafny-lang/dafny#1323.
But still stuck on a final problem: changing the type of u8 + u8 to u16 should make it satisfied, but I still get unsat.

[adsharma]

The solution in dafny-lang/dafny#1323 works for me. Things that took me a while to grok:

• tools like typpete use unsat (error) or unknown (ok) to distinguish. I was expecting unsat vs sat.
• I think about z3 as a black box (I can't single step through it and rely on examples in z3py documentation - especially advanced part to understand). More examples on how to implement a simple type system with some constraints would have helped me greatly.
• Boogie as an intermediate language seems more readable than the s-expression log. I'm thinking of a boogie equivalent with pythonic syntax:

@sealed
class Integer:
   i: int
  ub: u8
  us: u16
  ui: u32
  ul: u64

axiom: x is Integer.ub and 0 <= u8val(ub) < (1 << 8)
axiom: x is Integer.us and 0 <= u8val(us) < (1 << 16)
...

This is somewhat nicer than z3py API which feels like writing s-expressions with python syntax as opposed to writing python expressions in infix order. I have some support for this in py2many using the transpiler infra.

Thank you for writing z3. Hope my ramblings above are useful to the next person walking down this path.