kdrag.reflect

Reflecting and reifying SMT expressions from/into Python values.

Functions

`coverage_check`(stmt, everything, path_cond, ...)
`datatype`(s[, locals, globals])	Use python type syntax to define an algebraic datatype datatype.
`ensures`(e)
`eval_`(e[, globals, locals, default])	Evaluate a z3 expression in a given environment.
`expr`(expr[, globals, locals])	Turn a string of a python expression into a z3 expressions.
`infer_sort`(x)
`merge_branches`(test, body, orelse)
`namedtuple_of_constructor`(sort, idx)	Given a datatype sort and an index, return a named tuple with field names and the constructor.
`nbe`(x)	Normalization by evaluation.
`reflect`(f[, globals, by])	Reflect a function definition by injecting the parameters and recursive self call into the local environment.
`reify`(s, x)	sort directed reification of a python value.
`requires`(e)
`sort_of_type`(t)	Give equivalent SMT sort for a given Python type.
`struct`(cls)	Use a dataclass to define a struct datatype.
`type_of_sort`(s)	Give equivalent Python type for a given SMT sort.

Classes

`Env`()
`KnuckleClosure`(lam, globals, locals, default)	A closure that can be used to evaluate expressions in a given environment.
`Return`()

class kdrag.reflect.Env

Bases: object

globals: dict[str, object]

locals: dict[str, object]

path_cond: list[BoolRef]

class kdrag.reflect.KnuckleClosure(lam: QuantifierRef, globals: dict[str, object], locals: dict[str, object], default: Callable[[ExprRef], object])

Bases: object

A closure that can be used to evaluate expressions in a given environment. We don’t use lambda so that we can inspect

Parameters:

lam (QuantifierRef)
globals (dict[str, object])
locals (dict[str, object])
default (Callable[[ExprRef], object])

default: Callable[[ExprRef], object]

globals: dict[str, object]

lam: QuantifierRef

locals: dict[str, object]

class kdrag.reflect.Return

Bases: object

value: ExprRef

kdrag.reflect.coverage_check(stmt: stmt, everything: BoolRef, path_cond: list[BoolRef], locals: dict[str, object])

Parameters:

stmt (stmt)
everything (BoolRef)
path_cond (list[BoolRef])
locals (dict[str, object])

kdrag.reflect.datatype(s: str, locals=None, globals=None) → DatatypeSortRef

Use python type syntax to define an algebraic datatype datatype. Fields can be specified positionally or by name. Reads the inner types from current environment.

>>> Int = smt.IntSort()
>>> Real = smt.RealSort()
>>> Foo = datatype("type Foo = Biz | Bar | Baz(Int, Int, smt.IntSort()) | Boz(x = Int, y = Int)")
>>> Foo.Baz.domain(1)
Int
>>> Foo.x.range()
Int

Parameters:: s (str)
Return type:: DatatypeSortRef

kdrag.reflect.ensures(e: BoolRef)

Parameters:: e (BoolRef)

kdrag.reflect.eval_(e: ExprRef, globals={}, locals={}, default=<function __default_error>)

Evaluate a z3 expression in a given environment. The analog of python’s eval.

>>> eval_(smt.IntVal(42))
42
>>> eval_(smt.IntVal(1) + smt.IntVal(2))
3
>>> x = smt.Int("x")
>>> eval_(smt.Lambda([x], x + 1)[3])
4
>>> R = kd.Struct("R", ("x", kd.Z), ("y", smt.BoolSort()))
>>> eval_(R(42, True).x)
42
>>> eval_(R(42,True).is_R)
True

Parameters:: e (ExprRef)

kdrag.reflect.expr(expr: str, globals=None, locals=None) → ExprRef

Turn a string of a python expression into a z3 expressions. Globals are inferred to be current scope if not given.

>>> expr("x + 1", globals={"x": smt.Int("x")})
x + 1
>>> x = smt.Int("x")
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort())
>>> expr("f(x) + 1 if 0 < x < 5 < 7 else x * x")
If(And(x > 0, x < 5, True), f(x) + 1, x*x)

Parameters:: expr (str)
Return type:: ExprRef

kdrag.reflect.infer_sort(x: object) → SortRef

Parameters:: x (object)
Return type:: SortRef

kdrag.reflect.merge_branches(test: BoolRef, body: dict[str, object] | ExprRef, orelse: dict[str, object] | ExprRef) → ExprRef | dict[str, object]

Parameters:

test (BoolRef)
body (dict[str, object] | ExprRef)
orelse (dict[str, object] | ExprRef)

Return type:

ExprRef | dict[str, object]

kdrag.reflect.namedtuple_of_constructor(sort: DatatypeSortRef, idx: int)

Given a datatype sort and an index, return a named tuple with field names and the constructor. >>> Nat = smt.Datatype(“Nat”) >>> Nat.declare(“Z”) >>> Nat.declare(“S”, (“pred”, Nat)) >>> Nat = Nat.create() >>> namedtuple_of_constructor(Nat, 1)(0) S(pred=0)

Parameters:

sort (DatatypeSortRef)
idx (int)

kdrag.reflect.nbe(x: ExprRef) → ExprRef

Normalization by evaluation.

>>> nbe(smt.IntVal(41) + smt.IntVal(1))
42
>>> x,y = smt.Ints("x y")
>>> nbe(smt.Lambda([x], x + 1)[3])
4
>>> nbe(smt.Lambda([x], x + 1))
Lambda(x, x + 1)
>>> nbe(smt.Lambda([x], smt.IntVal(3) + 1))
Lambda(x, 3 + 1)

Parameters:: x (ExprRef)
Return type:: ExprRef

kdrag.reflect.reflect(f, globals=None, by=[]) → FuncDeclRef

Reflect a function definition by injecting the parameters and recursive self call into the local environment. Uses type annotations to do so.

Only handles a purely functional subset of python. Simple assignment is handled as a let who’s scope extends to the end of it’s subbranch. Every branch must end with a return.

You can still call original function under attribute __wrapped__.

>>> def foo(x : int) -> int:
...     return x + 3
>>> foo = reflect(foo)
>>> foo.__wrapped__(3)
6
>>> foo.defn
|= ForAll(x, foo(x) == x + 3)

>>> @reflect
... def bar(x : int, y : str) -> int:
...     if x > 4:
...         return x + 3
...     elif y == "fred":
...        return 14
...     else:
...        return bar(x - 1, y)
>>> bar.defn
|= ForAll([x, y],
       bar(x, y) ==
       If(x > 4, x + 3, If(y == "fred", 14, bar(x - 1, y))))
>>> @reflect
... def buzzy(n: int) -> int:
...     if n == 0:
...         assert n == 0
...         x = 1
...         y = x
...     else:
...         y = 2
...     return y
>>> @reflect
... def coverage(x : int) -> int:
...     if x + 1 > x:
...         return x
>>> z = smt.Int("z")
>>> @reflect
... def inc_78(n: int, m : "smt.Lambda([z], smt.And(z > 0, z > n))") -> "smt.Lambda([z], z > n)":
...    return n + m
>>> #test_match54.defn
>>> @reflect
... def test_add32(x : kd.Nat, y : kd.Nat) -> kd.Nat:
...     match x:
...         case S(n):
...             return kd.Nat.S(test_add32(n, y))
...         case Z():
...             return y
>>> test_add32.defn
|= ForAll([x, y],
    test_add32(x, y) ==
    If(is(S, x), S(test_add32(pred(x), y)), y))
>>> @reflect
... def test_match54(x: "int", y: int) -> int:
...     match x:
...         case 0:
...             return y
...         case _ if y > 0:
...             return y + 1
...         case _:
...             return y - 1
>>> test_match54.defn
|= ForAll([x, y],
    test_match54(x, y) ==
    If(x == 0, y, If(y > 0, y + 1, y - 1)))
>>> @reflect
... def test_false_pre(x: smt.Lambda([z], z != z)) -> int:
...     assert False
...     return 42
>>> @reflect
... def test_false_match(x: int)-> int:
...     match x:
...         case 4:
...             return x
...         case 4:
...             assert False
...             return x
...         case _:
...             return x
>>> @reflect
... def test_false_if(x: int, p : "smt.ExprRef # x > 0") -> "x > -1":
...     return ()
>>> @reflect
... def test_set_notation(x : "{x for x in int if x > 0}") -> "{y for y in int if y > x and y > 0}":
...     return x + 1
>>> test_set_notation.contract
|= ForAll(x,
    Implies(And(x > 0),
            Implies(And,
                    And(And(And(test_set_notation(x) > x,
                            test_set_notation(x) > 0))))))
>>> myconst = kd.define("myconst12345", [], smt.IntVal(42))
>>> @reflect
... def test_proof_call() -> "{y for y in int if y == myconst}":
...     if myconst != 42:
...         () = myconst.defn
...         assert False
...         return 0
...     else:
...         return 42
>>> test_proof_call.contract
|= Implies(And, And(And(test_proof_call == myconst12345)))
>>> @reflect
... def test_tuple(x : tuple[int, tuple[bool, int]]) -> bool:
...     (_, (b, y)) = x
...     return b
>>> @reflect
... def test_forloop(x : int) -> "{y for y in int if y == x + 6}":
...     for i in range(4):
...         x = x + i
...     return x

Return type:: FuncDeclRef

kdrag.reflect.reify(s: SortRef, x: object) → ExprRef

sort directed reification of a python value. https://en.wikipedia.org/wiki/Normalisation_by_evaluation >>> reify(smt.IntSort(), 42) 42 >>> reify(smt.IntSort(), 42).sort() Int >>> x = smt.Int(“x”) >>> kd.utils.alpha_eq(reify(smt.ArraySort(smt.IntSort(), smt.IntSort()), lambda x: x + 1), smt.Lambda([x], x + 1)) True >>> reify(smt.RealSort(), fractions.Fraction(10,16)) 5/8

Parameters:

s (SortRef)
x (object)

Return type:

ExprRef

kdrag.reflect.requires(e: BoolRef)

Parameters:: e (BoolRef)

kdrag.reflect.sort_of_type(t: type | GenericAlias) → SortRef

Give equivalent SMT sort for a given Python type.

>>> sort_of_type(int)
Int
>>> sort_of_type(list[int])
Seq(Int)
>>> sort_of_type(dict[str, int])
Array(String, Int)
>>> sort_of_type(tuple[int, bool])
Tuple_Int_Bool
>>> sort_of_type(tuple)
Unit

Parameters:: t (type | GenericAlias)
Return type:: SortRef

kdrag.reflect.struct(cls) → DatatypeSortRef

Use a dataclass to define a struct datatype. Fields are specified by type annotations.

>>> @struct
... class MyStruct32:
...     x: int
...     y: smt.BoolSort()
>>> MyStruct32.x.range()
Int
>>> MyStruct32.y.range()
Bool

Return type:: DatatypeSortRef

kdrag.reflect.type_of_sort(s: SortRef) → type

Give equivalent Python type for a given SMT sort.

>>> type_of_sort(smt.IntSort())
<class 'int'>
>>> type_of_sort(smt.ArraySort(smt.StringSort(), smt.IntSort()))
<class 'dict'>
>>> type_of_sort(smt.SeqSort(smt.IntSort()))
<class 'list'>

Parameters:: s (SortRef)
Return type:: type