kdrag

Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof assistant in python. It is not attempting to be the most interesting, expressive, or flexible logic in the world.

The goal is to support applications like software/hardware verification, calculus, equational reasoning, and numerical bounds.

class kdrag.Calc(vars: list[ExprRef], lhs: ExprRef, assume=[])

Bases: object

Calc is for equational reasoning. One can write a sequence of formulas interspersed with useful lemmas.

Parameters:

vars (list[ExprRef])
lhs (ExprRef)

eq(rhs, by=[], **kwargs)

ge(rhs, by=[])

gt(rhs, by=[])

le(rhs, by=[])

lt(rhs, by=[])

qed(**kwargs)

kdrag.FreshVar(prefix: str, sort: SortRef) → ExprRef

Generate a fresh variable. This is distinguished from FreshConst by the fact that it has freshness evidence. This is intended to be used for constants that represent arbitrary terms (implicitly universally quantified). For example, axioms like c_fresh = t should never be asserted about bare FreshVars as they imply a probably inconsistent axiom, whereas asserting such an axiom about FreshConst is ok, effectively defining a new rigid constant.

>>> FreshVar("x", smt.IntSort()).fresh_evidence
_FreshVarEvidence(v=x!...)

Parameters:

prefix (str)
sort (SortRef)

Return type:

ExprRef

kdrag.FreshVars(names: str, sort: SortRef) → list[ExprRef]

Create a list of schema variables with the given names and sort.

Parameters:

names (str)
sort (SortRef)

Return type:

list[ExprRef]

kdrag.Inductive(name: str) → Datatype

Declare datatypes with auto generated induction principles. Wrapper around z3.Datatype

>>> Nat = Inductive("Nat")
>>> Nat.declare("zero")
>>> Nat.declare("succ", ("pred", Nat))
>>> Nat = Nat.create()
>>> Nat.succ(Nat.zero)
succ(zero)

Parameters:: name (str)
Return type:: Datatype

kdrag.Lemma(goal: BoolRef, fixes=None, assumes=None) → ProofState

Parameters:: goal (BoolRef)
Return type:: ProofState

kdrag.NewType(name: str, sort: SortRef, pred=None) → DatatypeSortRef

Minimal wrapper around a sort for sort based overloading

>>> NatI = NewType("NatI", smt.IntSort(), pred = lambda x: x.val >= 0)
>>> x = smt.Const("x", NatI)
>>> kd.QForAll([x], x.val >= -7)
ForAll(x, Implies(val(x) >= 0, val(x) >= -7))

Parameters:

name (str)
sort (SortRef)

Return type:

DatatypeSortRef

kdrag.PTheorem(goal: BoolRef | str)

A decorator to create a theorem from a function that takes a ProofState as argument.

>>> x = smt.Int("x")
>>> @PTheorem(x + 1 > x)
... def mytheorem(l: ProofState):
...     "An example theorem"
...     l.auto()
Lemma Complete! Change PTheorem to Theorem

Parameters:: goal (BoolRef | str)

class kdrag.Proof(thm: BoolRef, reason: list[Any], admit: bool = False)

Bases: Judgement

It is unlikely that users should be accessing the Proof constructor directly. This is not ironclad. If you really want the Proof constructor, I can’t stop you.

Parameters:

thm (BoolRef)
reason (list[Any])
admit (bool)

__call__(*args: ExprRef | Proof)

>>> x,y = smt.Ints("x y")
>>> p = prove(smt.ForAll([y], smt.ForAll([x], x >= x - 1)))
>>> p(x)
|= ForAll(x, x >= x - 1)
>>> p(x, 7)
|= 7 >= 7 - 1

>>> a,b,c = smt.Bools("a b c")
>>> ab = prove(smt.Implies(a,smt.Implies(a, a)))
>>> a = axiom(a)
>>> ab(a)
|= Implies(a, a)
>>> ab(a,a)
|= a

Parameters:: args (ExprRef | Proof)

admit: bool = False

forall(fresh_vars: list[ExprRef]) → Proof

Generalize a proof involved schematic variables generated by FreshVar

>>> x = FreshVar("x", smt.IntSort())
>>> prove(x + 1 > x).forall([x])
|= ForAll(x!..., x!... + 1 > x!...)

Parameters:: fresh_vars (list[ExprRef])
Return type:: Proof

reason: list[Any]

thm: BoolRef

kdrag.QExists(vs: list[ExprRef], *concs0) → BoolRef

Quantified Exists

Shorthand for ForAll(vars, And(conc[0], conc[1], …))

If variables have a property wf attached, this is anded into the properties.

Parameters:: vs (list[ExprRef])
Return type:: BoolRef

kdrag.QForAll(vs: list[ExprRef], *hyp_conc) → BoolRef

Quantified ForAll

Shorthand for ForAll(vars, Implies(And(hyp[0], hyp[1], …), conc))

If variables have a property wf attached, this is added as a hypothesis.

There is no downside to always using this compared to smt.ForAll and it can avoid some errors.

>>> x,y = smt.Ints("x y")
>>> QForAll([x,y], x > 0, y > 0, x + y > 0)
ForAll([x, y], Implies(And(x > 0, y > 0), x + y > 0))

Parameters:: vs (list[ExprRef])
Return type:: BoolRef

kdrag.QImplies(*hyp_conc) → BoolRef

Quantified Implies

Shorthand for Implies(And(hyp[0], hyp[1], …), conc)

>>> x,y = smt.Ints("x y")
>>> QImplies(x > 0, y > 0, x + y > 0)
Implies(And(x > 0, y > 0), x + y > 0)

Return type:: BoolRef

kdrag.Struct(name: str, *fields: tuple[str, SortRef], pred=None) → DatatypeSortRef

Define a record datatype. This is the analog in many respects of python’s NamedTuple. The optional argument pred will add a well-formedness condition to the record giving something akin to a refinement type.

>>> Point = Struct("Point", ("x", smt.RealSort()), ("y", smt.RealSort()))
>>> Point(1,2)
Point(ToReal(1), ToReal(2))
>>> Point(1,2).x
x(Point(ToReal(1), ToReal(2)))
>>> PosPoint = Struct("PosPoint", ("x", smt.RealSort()), ("y", smt.RealSort()), pred = lambda p: smt.And(p.x > 0, p.y > 0))
>>> p = smt.Const("p", PosPoint)
>>> kd.QForAll([p], p.x > -42)
ForAll(p, Implies(And(x(p) > 0, y(p) > 0), x(p) > -42))

Parameters:

name (str)
fields (tuple[str, SortRef])

Return type:

DatatypeSortRef

kdrag.Theorem(goal: BoolRef | str) → Callable[[Callable[[ProofState], None]], Proof]

A decorator to create a theorem from a function that takes a ProofState as argument.

>>> x = smt.Int("x")
>>> @Theorem(x + 1 > x)
... def mytheorem(l: ProofState):
...     "An example theorem"
...     l.auto()
>>> mytheorem
|= x + 1 > x
>>> mytheorem.__doc__
'An example theorem'
>>> @Theorem("forall (x : Int), x + 1 > x")
... def mytheorem2(l: ProofState):
...     l.auto()
>>> mytheorem2
|= ForAll(x, x + 1 > x)
>>> @Theorem("x + 1 > x") # Getting globals from scope
... def mytheorem3(l: ProofState):
...     l.auto()
>>> mytheorem3
|= x + 1 > x

Parameters:: goal (BoolRef | str)
Return type:: Callable[[Callable[[ProofState], None]], Proof]

kdrag.axiom(thm: BoolRef, by=['axiom']) → Proof

Assert an axiom.

Axioms are necessary and useful. But you must use great care.

Parameters:

thm (BoolRef) – The axiom to assert.
by – A python object explaining why the axiom should exist. Often a string explaining the axiom.

Return type:

Proof

kdrag.cond(*cases, default=None) → ExprRef

Helper for chained ifs defined by cases. Each case is a tuple of a bool condition and a term. If default is not given, a check is performed for totality.

>>> x = smt.Int("x")
>>> kd.cond((x < 0, 2 * x), (x == 0, 3 * x), (x > 0, 5 * x))
If(x < 0,
   2*x,
   If(x == 0, 3*x, If(x > 0, 5*x, unreachable...)))
>>> kd.cond((x < 0, 2 * x), (x == 0, 3 * x), default = 5 * x)
If(x < 0, 2*x, If(x == 0, 3*x, 5*x))

Return type:: ExprRef

kdrag.define(name: str, args: list[ExprRef], body: ExprRef, lift_lambda=False) → FuncDeclRef

Define a non recursive definition. Useful for shorthand and abstraction. Does not currently defend against ill formed definitions. TODO: Check for bad circularity, record dependencies

Parameters:

name (str) – The name of the term to define.
args (list[ExprRef]) – The arguments of the term.
defn – The definition of the term.
body (ExprRef)

Returns:

A tuple of the defined term and the proof of the definition.

Return type:

tuple[smt.FuncDeclRef, Proof]

kdrag.prove(thm: BoolRef, fixes: list[ExprRef] = [], assumes: list[BoolRef] = [], by: Proof | Sequence[Proof] | None = None, admit=False, timeout=1000, dump=False, solver=None, unfold: int | list[FuncDeclRef] | None = None) → Proof

Prove a theorem using a list of previously proved lemmas.

In essence prove(Implies(by, thm)).

This wraps the kernel version in order to provide better counterexamples.

Parameters:

thm (smt.BoolRef) – The theorem to prove.
thm – The theorem to prove.
by (list[Proof]) – A list of previously proved lemmas.
admit (bool) – If True, admit the theorem without proof.
fixes (list[ExprRef])
assumes (list[BoolRef])
unfold (int | list[FuncDeclRef] | None)

Returns:

A proof object of thm

Return type:

Proof

>>> prove(smt.BoolVal(True))
|= True

>>> prove(smt.RealVal(1) >= smt.RealVal(0))
|= 1 >= 0

>>> x = smt.Int("x")
>>> succ = kd.define("succ", [x], x + 1)
>>> prove(succ(x) == x + 1, unfold=1)
|= succ(x) == x + 1
>>> succ2 = kd.define("succ2", [x], succ(succ(x)))
>>> prove(succ2(x) == x + 2, unfold=2)
|= succ2(x) == x + 2
>>> prove(succ(x) == x + 1, unfold=[succ])
|= succ(x) == x + 1

kdrag.search(*es: FuncDeclRef | ExprRef, db: dict[Any, Proof] = {}) → dict[tuple[str, Proof], Any]

Search for function declarations or expressions. Takes intersection of found results if given multiple arguments. Builds a database by scanning loaded modules by default.

Parameters:

es (FuncDeclRef | ExprRef)
db (dict[Any, Proof])

Return type:

dict[tuple[str, Proof], Any]

kdrag.simp(e: ExprRef, trace=None, max_iter=3) → ExprRef

Simplify using definitions and built in z3 simplifier until no progress is made.

>>> import kdrag.theories.nat as nat
>>> simp(nat.one + nat.one + nat.S(nat.one))
S(S(S(S(Z))))

>>> p = smt.Bool("p")
>>> simp(smt.If(p, 42, 3))
If(p, 42, 3)

Parameters:: e (ExprRef)
Return type:: ExprRef

Modules

`all`	A convenience module to import commonly needed other modules as shorthands
`config`	Global configuration of Knuckledragger
`contrib`
`datatype`	Convenience features for datatypes.
`hypothesis`	Helper functions for the hypothesis property based testing library.
`kernel`	The kernel hold core proof datatypes and core inference rules.
`modal`	Treating T -> Bool as a kind of truth value
`notation`	SortDispatch system for z3 sort based dispatch akin to functools.singledispatch.
`parsers`
`printers`
`property`	Generic properties like associativity, commutativity, idempotence, etc.
`reflect`	Reflecting and reifying SMT expressions from/into Python values.
`rewrite`	Utilities for rewriting and simplification including pattern matching and unification.
`smt`	Reexported z3 functionality <https://z3prover.github.io/api/html/namespacez3py.html> This is a shim file to enable the use of cvc5 and vampire as default solvers.
`solvers`	Facilities for pretty printing and calling external solvers
`tactics`	Tactics are helpers that organize calls to the kernel.
`tele`
`theories`	Library of axioms, theorems, and theory specific tactics
`utils`	Various term manipulation helpers.