kdrag.contracts

Contracts are a database of lemmas associated with a function symbol. They are usually used to specify intended pre and postconditions for functions as an abstraction over their definition. This can also be though of as a subtyping refinement.

There is a registry which can be queried.

This registry is not trusted code.

Functions

contract(f, args, pre, post[, by])

Register the contract for function f: for all args, pre => post.

lemmas(e[, into_binders])

Instantiate all contract lemmas found in a pexression.

Classes

Contract(f, args, pre, post, proof)

class kdrag.contracts.Contract(f: z3.z3.FuncDeclRef, args: list[z3.z3.ExprRef], pre: z3.z3.BoolRef, post: z3.z3.BoolRef, proof: kdrag.kernel.Proof)

Bases: object

Parameters:

  • f (FuncDeclRef)

  • args (list[ExprRef])

  • pre (BoolRef)

  • post (BoolRef)

  • proof (Proof)

args: list[ExprRef]
f: FuncDeclRef
post: BoolRef
pre: BoolRef
proof: Proof
kdrag.contracts.contract(f: FuncDeclRef, args: list[ExprRef], pre, post, by=None, **kwargs) → Proof

Register the contract for function f: for all args, pre => post.

>>> x = smt.Int("x")
>>> foo = kd.define("foo4392", [x], x + 1)
>>> c = contract(foo, [x], x > 0, foo(x) > 0, by=[foo.defn])
>>> c
|= ForAll(x, Implies(x > 0, foo4392(x) > 0))
>>> c.thm.pattern(0)
foo4392(Var(0))
>>> kd.prove(foo(5) > 0, contracts=True)
|= foo4392(5) > 0
>>> kd.prove(foo(5) > 5, contracts=True)
Traceback (most recent call last):
    ...
LemmaError: ...
Parameters:

  • f (FuncDeclRef)

  • args (list[ExprRef])

Return type:

Proof

kdrag.contracts.lemmas(e: ExprRef, into_binders=True) → list[Proof]

Instantiate all contract lemmas found in a pexression. This sweeps the expression and instantiates the contract lemma with the arguments to the function. Once it goes under binders, this becomes more difficult, so it returns the quantified form of the lemmas

Parameters:

e (ExprRef)

Return type:

list[Proof]