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.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

class kdrag.Lemma(goal: BoolRef)

Bases: object

A tactic class for interactive proofs. Lemma stores a mutational partial proof state that can be changed via tactic methods. Once proof is completed, an actual kd.Proof object is constructed by the Lemma.qed method. Lemma is not part of the trusted code base and bugs in its implementation are not a soundness concern. Lemma “merely” orchestrates and infers info for calls to the kernel. In my experience it is best to run the entire Lemma mutation in a single Jupyter cell while experimenting.

Parameters:: goal (BoolRef)

admit() → Goal

admit the current goal without proof. Don’t feel bad about keeping yourself moving, but be aware that you’re not done.

>>> l = Lemma(smt.BoolVal(False)) # a false goal
>>> _ = l.admit()
>>> l.qed()
|- False

Return type:: Goal

apply(pf: Proof, rev=False)

apply matches the conclusion of a proven clause

Parameters:: pf (Proof)

assumption(): Exact match of goal in the context

auto(**kwargs): auto discharges a goal using z3. It forwards all parameters to kd.prove

cases(t)

cases let’s us consider an object by cases. We consider whether Bools are True or False We consider the different constructors for datatypes

>>> import kdrag.theories.nat as nat
>>> x = smt.Const("x", nat.Nat)
>>> l = Lemma(smt.BoolVal(True))
>>> l.cases(x)
[is(Z, x) == True] ?|- True
>>> l.auto() # next case
[is(S, x) == True] ?|- True

clear(n: int)

Remove a hypothesis from the context

Parameters:: n (int)

copy()

Lemma methods mutates the proof state. This can make you a copy. Does not copy the pushed Lemma stack.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p,q))
>>> l1 = l.copy()
>>> l.intros()
[p] ?|- q
>>> l1
[] ?|- Implies(p, q)

einstan(n): einstan opens an exists quantifier in context and returns the fresh eigenvariable. [exists x, p(x)] ?|- goal becomes p(x) ?|- goal

eq(rhs: ExprRef, **kwargs)

replace rhs in equational goal

Parameters:: rhs (ExprRef)

exists(*ts)

Give terms ts to satisfy an exists goal ?|- exists x, p(x) becomes ?|- p(ts)

>>> x,y = smt.Ints("x y")
>>> Lemma(smt.Exists([x], x == y)).exists(y)
[] ?|- y == y

ext()

Apply extensionality to a goal

>>> x = smt.Int("x")
>>> l = Lemma(smt.Lambda([x], smt.IntVal(1)) == smt.K(smt.IntSort(), smt.IntVal(1)))
>>> _ = l.ext()

fix() → ExprRef

Open a single ForAll quantifier

>>> x = smt.Int("x")
>>> l = Lemma(smt.ForAll([x], x != x + 1))
>>> _x = l.fix()
>>> l
[x!...] ; [] ?|- x!... != x!... + 1
>>> _x.eq(x)
False

Return type:: ExprRef

fixes() → list[ExprRef]

fixes opens a forall quantifier. ?|- forall x, p(x) becomes x ?|- p(x)

>>> x,y = smt.Ints("x y")
>>> l = Lemma(kd.QForAll([x,y], y >= 0, x + y >= x))
>>> _x, _y = l.fixes()
>>> l
[x!..., y!...] ?|- Implies(y!... >= 0, x!... + y!... >= x!...)
>>> _x, _y
(x!..., y!...)
>>> _x.eq(x)
False

Return type:: list[ExprRef]

generalize(*vs: ExprRef)

Put variables forall quantified back on goal. Useful for strengthening induction hypotheses.

Parameters:: vs (ExprRef)

have(conc: BoolRef, **kwargs)

Prove the given formula and add it to the current context

Parameters:: conc (BoolRef)

induct(x: ExprRef, using: Callable[[ExprRef, Callable[[ExprRef, BoolRef], BoolRef]], Proof] | None = None)

Apply an induction lemma instantiated on x.

Parameters:

x (ExprRef)
using (Callable[[ExprRef, Callable[[ExprRef, BoolRef], BoolRef]], Proof] | None)

instan(n, *ts)

Instantiate a universal quantifier in the context.

>>> x,y = smt.Ints("x y")
>>> l = Lemma(smt.Implies(smt.ForAll([x],x == y), True))
>>> l.intros()
[ForAll(x, x == y)] ?|- True
>>> l.instan(0, smt.IntVal(42))
[ForAll(x, x == y), 42 == y] ?|- True

intros() → ExprRef | list[ExprRef] | Goal

intros opens an implication. ?|- p -> q becomes p ?|- q

>>> p,q,r = smt.Bools("p q r")
>>> l = Lemma(smt.Implies(p, q))
>>> l.intros()
[p] ?|- q
>>> l = Lemma(smt.Not(q))
>>> l.intros()
[q] ?|- False

Return type:: ExprRef | list[ExprRef] | Goal

left(n=0)

Select the left case of an Or goal.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Or(p,q))
>>> l.left()
[] ?|- p

newgoal(newgoal: BoolRef, **kwargs)

Try to show newgoal is sufficient to prove current goal

Parameters:: newgoal (BoolRef)

pop(): Pop state off the Lemma stack.

push()

Push a copy of the current Lemma state onto a stack. This why you can try things out, and if they fail

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p,q))
>>> l.push()
[] ?|- Implies(p, q)
>>> l.intros()
[p] ?|- q
>>> l.pop()
[] ?|- Implies(p, q)

qed(**kwargs) → Proof

return the actual final Proof of the lemma that was defined at the beginning.

Return type:: Proof

rewrite(rule: Proof | int, at=None, rev=False)

rewrite allows you to apply rewrite rule (which may either be a Proof or an index into the context) to the goal or to the context.

Parameters:: rule (Proof | int)

right()

Select the right case of an Or goal.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Or(p,q))
>>> l.right()
[] ?|- q

rw(rule: Proof | int, at=None, rev=False)

shorthand for rewrite

Parameters:: rule (Proof | int)

search(*args, at=None, db={})

Search the lemma database for things that may match the current goal.

>>> import kdrag.theories.nat as nat
>>> n = smt.Const("n", nat.Nat)
>>> l = Lemma(smt.ForAll([n], nat.Z + n == n))
>>> ("kdrag.theories.nat.add_Z", nat.add_Z) in l.search().keys()
True
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search().keys()
False
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search(nat.add).keys()
True

show(thm: BoolRef)

To document the current goal

Parameters:: thm (BoolRef)

simp(at=None)

Use built in z3 simplifier. May be useful for boolean, arithmetic, lambda, and array simplifications.

>>> x,y = smt.Ints("x y")
>>> l = Lemma(x + y == y + x)
>>> l.simp()
[] ?|- True
>>> l = Lemma(x == 3 + y + 7)
>>> l.simp()
[] ?|- x == 10 + y
>>> l = Lemma(smt.Lambda([x], x + 1)[3] == y)
>>> l.simp()
[] ?|- 4 == y

split(at=None)

split breaks apart an And or bi-implication == goal. The optional keyword at allows you to break apart an And or Or in the context

>>> p = smt.Bool("p")
>>> l = Lemma(smt.And(True,p))
>>> l.split()
[] ?|- True
>>> l.auto() # next goal
[] ?|- p

symm()

Swap left and right hand side of equational goal

>>> x,y = smt.Ints("x y")
>>> Lemma(x == y).symm()
[] ?|- y == x

top_goal() → Goal

Return type:: Goal

unfold(*decls: FuncDeclRef, at=None)

Unfold all definitions once. If declarations are given, only those are unfolded.

>>> import kdrag.theories.nat as nat
>>> l = Lemma(nat.Z + nat.Z == nat.Z)
>>> l
[] ?|- add(Z, Z) == Z
>>> l.unfold(nat.double) # does not unfold add
[] ?|- add(Z, Z) == Z
>>> l.unfold()
[] ?|- If(is(Z, Z), Z, S(add(pred(Z), Z))) == Z

Parameters:: decls (FuncDeclRef)

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

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

Bases: object

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)

admit: bool = False

reason: list[Any]

thm: BoolRef

kdrag.QExists(vs: list[ExprRef], *concs) → 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.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.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, by: Proof | Sequence[Proof] = [], admit=False, timeout=1000, dump=False, solver=None, defns=True, simps={}) → Proof

Prove a theorem using a list of previously proved lemmas.

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

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.

Returns:

A proof object of thm

Return type:

Proof

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

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

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=None) → 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
`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.
`notation`	The SortDispatch system enables z3 sort based dispatch akin to ` functools.singledispatch`.
`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.
`theories`	Library of axioms, theorems, and theory specific tactics
`utils`	Various term manipulation helpers.