tutorial.ipynb

{
    "cells": [
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "# Welcome to Knuckledragger!\n",
                "\n",
                "This tutorial can be used online at \n",
                "[![Open In Colab](https://colab.research.google.com/assets/colab-badge.svg)](http://colab.research.google.com/github/philzook58/knuckledragger/blob/main/tutorial.ipynb)\n",
                "\n",
                "The documentation for knuckledragger is available [here](https://www.philipzucker.com/knuckledragger/)\n",
                "\n",
                "Running the following cell will install Knuckledragger on your colab instance."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {
                "tags": [
                    "test_skip"
                ]
            },
            "outputs": [],
            "source": [
                "!git clone https://github.com/philzook58/knuckledragger.git"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {
                "tags": [
                    "test_skip"
                ]
            },
            "outputs": [],
            "source": [
                "!cd knuckledragger && python3 -m pip install -e ."
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "You may need to restart your colab instance to get the installation to take. You can do so in the menu or by running the following cell."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {
                "tags": [
                    "test_skip"
                ]
            },
            "outputs": [],
            "source": [
                "import os\n",
                "os.kill(os.getpid(), 9)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "# A Quick Tour\n",
                "\n",
                "Knuckledragger is heavily built around the well used and appreciated python bindings to the SMT solver [Z3](https://microsoft.github.io/z3guide/). The terms and formulas are literally reexported Z3Py objects and there should be ZERO overhead interoperating any usage of Z3Py from other software into Knuckledragger. \n",
                "\n",
                "Anything Z3 can do on it's own, we can \"prove\" with no extra work"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 1,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "&#8870;Implies(p, Or(p, q))"
                        ],
                        "text/plain": [
                            "|- Implies(p, Or(p, q))"
                        ]
                    },
                    "execution_count": 1,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "import kdrag as kd\n",
                "import kdrag.smt as smt # smt is literally a reexporting of z3\n",
                "\n",
                "\n",
                "p,q = smt.Bools(\"p q\")\n",
                "simple_taut = kd.prove(smt.Implies(p, smt.Or(p, q)))\n",
                "simple_taut"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "The returned objects are `Proof`, not `smt.ExprRef` formulas"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 5,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/plain": [
                            "kdrag.kernel.Proof"
                        ]
                    },
                    "execution_count": 5,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "assert kd.kernel.is_proof(simple_taut)\n",
                "assert not isinstance(simple_taut, smt.ExprRef)\n",
                "type(simple_taut)"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 7,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "p &rArr; p &or; q"
                        ],
                        "text/plain": [
                            "Implies(p, Or(p, q))"
                        ]
                    },
                    "execution_count": 7,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "simple_taut.thm"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 8,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/plain": [
                            "z3.z3.BoolRef"
                        ]
                    },
                    "execution_count": 8,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "type(simple_taut.thm)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "`kd.prove` will throw an error if the theorem is not provable"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 9,
            "metadata": {},
            "outputs": [],
            "source": [
                "try:\n",
                "    false_lemma = kd.prove(smt.Implies(p, smt.And(p, q)), timeout=10)\n",
                "    print(\"This will not be reached\")\n",
                "except kd.kernel.LemmaError as _:\n",
                "    pass"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "Z3 also supports things like Reals, Ints, BitVectors and strings"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 10,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "&#8870;ForAll(x, Or(x < 0, x == 0, x > 0))"
                        ],
                        "text/plain": [
                            "|- ForAll(x, Or(x < 0, x == 0, x > 0))"
                        ]
                    },
                    "execution_count": 10,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "x = smt.Real(\"x\")\n",
                "real_trich = kd.prove(smt.ForAll([x], smt.Or(x < 0, x == 0, 0 < x)))\n",
                "real_trich"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 11,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "&#8870;ForAll(x, x | x == x)"
                        ],
                        "text/plain": [
                            "|- ForAll(x, x | x == x)"
                        ]
                    },
                    "execution_count": 11,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "x = smt.BitVec(\"x\", 32)\n",
                "or_idem = kd.prove(smt.ForAll([x], x | x == x))\n",
                "or_idem"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "## Help Z3 Out\n",
                "\n",
                "But the point of Knuckledragger is really for the things Z3 can't do in one shot. Knuckledragger supports a wrapped Z3 Boolean object called `kd.Proof` that only Knuckledragger knows how to build. This is how we distinguish between Z3 formulas that are _to be proven_ from those that _have been proven_. This `kd.Proof` object also retains a record of the previous calls to Z3, which can be considered a form of proof.\n",
                "\n",
                "Knuckledragger support algebraic datatypes and induction"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 12,
            "metadata": {},
            "outputs": [],
            "source": [
                "Nat = kd.Inductive(\"MyNat\")\n",
                "Zero = Nat.declare(\"Zero\")\n",
                "Succ = Nat.declare(\"Succ\", (\"pred\", Nat))\n",
                "Nat = Nat.create()"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 15,
            "metadata": {},
            "outputs": [
                {
                    "name": "stdout",
                    "output_type": "stream",
                    "text": [
                        "WARNING: Redefining function add from |- ForAll([n, m],\n",
                        "       add(n, m) ==\n",
                        "       If(is(Zero, n),\n",
                        "          m,\n",
                        "          If(is(Succ, n),\n",
                        "             Succ(add(pred(n), m)),\n",
                        "             unreachable!10))) to ForAll([n, m],\n",
                        "       add(n, m) ==\n",
                        "       If(is(Zero, n),\n",
                        "          m,\n",
                        "          If(is(Succ, n),\n",
                        "             Succ(add(pred(n), m)),\n",
                        "             unreachable!11)))\n"
                    ]
                },
                {
                    "data": {
                        "text/html": [
                            "&#8870;ForAll([n, m],\n",
                            "       add(n, m) ==\n",
                            "       If(is(Zero, n),\n",
                            "          m,\n",
                            "          If(is(Succ, n),\n",
                            "             Succ(add(pred(n), m)),\n",
                            "             unreachable!11)))"
                        ],
                        "text/plain": [
                            "|- ForAll([n, m],\n",
                            "       add(n, m) ==\n",
                            "       If(is(Zero, n),\n",
                            "          m,\n",
                            "          If(is(Succ, n),\n",
                            "             Succ(add(pred(n), m)),\n",
                            "             unreachable!11)))"
                        ]
                    },
                    "execution_count": 15,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "# We can define an addition function by cases\n",
                "n,m = smt.Consts(\"n m\", Nat)\n",
                "add = smt.Function(\"add\", Nat, Nat, Nat)\n",
                "add = kd.define(\"add\", [n,m], \n",
                "    kd.cond(\n",
                "        (n.is_Zero, m),\n",
                "        (n.is_Succ, Nat.Succ(add(n.pred, m)))\n",
                "))\n",
                "add.defn"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 14,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "add(n, m)"
                        ],
                        "text/plain": [
                            "add(n, m)"
                        ]
                    },
                    "execution_count": 14,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "# There is a notation overloading mechanism modelled after python's singledispatch\n",
                "kd.notation.add.register(Nat, add)\n",
                "n + m"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {},
            "outputs": [],
            "source": [
                "# The definitional lemma is not available to the solver unless you give it\n",
                "add_zero_x = kd.prove(smt.ForAll([n], Nat.Zero + n == n), by=[add.defn])\n",
                "add_succ_x = kd.prove(smt.ForAll([n,m], Nat.Succ(n) + m == Nat.Succ(n + m)), by=[add.defn])"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 16,
            "metadata": {},
            "outputs": [],
            "source": [
                "# More involved proofs can be more easily done in an interactive tactic\n",
                "# Under the hood, this boils down to calls to kd.prove\n",
                "# These proofs are best understood by seeing the interactive output in a Jupyter notebook\n",
                "l = kd.Lemma(smt.ForAll([n], n + Nat.Zero == n))\n",
                "\n",
                "# [] ?|- ForAll(n, add(n, Zero) == n)\n",
                "_n = l.fix()            \n",
                "\n",
                "# [] ?|- add(n!0, Zero) == n!2213\n",
                "l.induct(_n)              \n",
                "\n",
                "# Case n!0 == Nat.Zero\n",
                "# [] ?|- add(Zero, Zero) == Zero\n",
                "l.auto(by=[add.defn])\n",
                "\n",
                "# Case n!0 == Nat.Succ(n.pred)\n",
                "# [] ?|- ForAll(a!0, Implies(add(a!0, Zero) == a!0, add(Succ(a!0), Zero) == Succ(a!0)))\n",
                "l.auto(by=[add.defn])\n",
                "\n",
                "# Finally the actual Proof is built\n",
                "add_x_zero = l.qed()"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "## Axiomatic Theories\n",
                "\n",
                "But we can also build our own sorts and axiomatic theories, like a theory of groups <https://en.wikipedia.org/wiki/Group_(mathematics)>. The following defines a signature of a group."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {},
            "outputs": [],
            "source": [
                "G = smt.DeclareSort(\"G\")\n",
                "mul = smt.Function(\"mul\", G, G, G)\n",
                "e = smt.Const(\"e\", G)\n",
                "inv = smt.Function(\"inv\", G, G)\n",
                "kd.notation.mul.register(G, mul)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "There are also some axioms a group satisfies."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {},
            "outputs": [],
            "source": [
                "x, y, z = smt.Consts(\"x y z\", G)\n",
                "mul_assoc = kd.axiom(smt.ForAll([x, y, z], x * (y * z) == (x * y) * z))\n",
                "id_left = kd.axiom(smt.ForAll([x], e * x == x))\n",
                "inv_left = kd.axiom(smt.ForAll([x], inv(x) * x == e))"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "The right inverse law actually follows from this minimal set of axioms. This proof was constructed by following the wikipedia page."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {},
            "outputs": [],
            "source": [
                "# The Calc tactic can allow one to write explicit equational proofs\n",
                "c = kd.Calc([x], x * inv(x))\n",
                "c.eq(e * (x * inv(x)), by=[id_left])\n",
                "c.eq((inv(inv(x)) * inv(x)) * (x * inv(x)), by=[inv_left])\n",
                "c.eq(inv(inv(x)) * ((inv(x) * x) * inv(x)), by=[mul_assoc])\n",
                "c.eq(inv(inv(x)) * (e * inv(x)), by=[inv_left])\n",
                "c.eq(inv(inv(x)) * inv(x), by=[id_left])\n",
                "c.eq(e, by=[inv_left])\n",
                "inv_right = c.qed()"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "# Intro to Z3\n",
                "\n",
                "Knuckledragger is heavily based around the preexisting SMT solver Z3. Knowing about Z3 is useful even if you aren't interested \n",
                "\n",
                "You can find a tutorial notebook and video I made here https://github.com/philzook58/z3_tutorial\n"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 2,
            "metadata": {},
            "outputs": [],
            "source": [
                "import z3"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "We then declare our variables, state a set of constraints we wish to hold, and then call the convenience function solve to get a solution."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 3,
            "metadata": {},
            "outputs": [
                {
                    "name": "stdout",
                    "output_type": "stream",
                    "text": [
                        "[y = 0, x = 7]\n"
                    ]
                }
            ],
            "source": [
                "x = z3.Int('x')\n",
                "y = z3.Int('y')\n",
                "z3.solve(x > 2, y < 10, x + 2*y == 7)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "We can also use z3 to prove properties and theorems."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 4,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "p &rArr; p"
                        ],
                        "text/plain": [
                            "Implies(p, p)"
                        ]
                    },
                    "execution_count": 4,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "p = z3.Bool(\"p\")\n",
                "my_true_thm = z3.Implies(p, p)\n",
                "my_true_thm"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 5,
            "metadata": {},
            "outputs": [
                {
                    "name": "stdout",
                    "output_type": "stream",
                    "text": [
                        "proved\n"
                    ]
                }
            ],
            "source": [
                "z3.prove(my_true_thm)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "If the property is not true, smt can supply a counterexample. "
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 6,
            "metadata": {},
            "outputs": [
                {
                    "data": {
                        "text/html": [
                            "q &rArr; p"
                        ],
                        "text/plain": [
                            "Implies(q, p)"
                        ]
                    },
                    "execution_count": 6,
                    "metadata": {},
                    "output_type": "execute_result"
                }
            ],
            "source": [
                "q = z3.Bool(\"q\")\n",
                "my_false_thm = z3.Implies(q, p)\n",
                "my_false_thm"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 7,
            "metadata": {},
            "outputs": [
                {
                    "name": "stdout",
                    "output_type": "stream",
                    "text": [
                        "counterexample\n",
                        "[p = False, q = True]\n"
                    ]
                }
            ],
            "source": [
                "z3.prove(my_false_thm)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "# Why Knuckledragger?\n",
                "\n",
                "Z3 is a tour de force. It's beautiful. However, it falls short of solving or verifying many kinds of problems we may be interested in.\n",
                "\n",
                "1. It may in principle be able to solve something, but times out\n",
                "2. Many mathematical and verification questions involve induction, which Z3 does not have strong built in support for. In general automating this is a tough problem\n",
                "3. We may want to spell out what Z3 can do for use automatically, to make sure we understand\n",
                "4. Z3 may not have good built in understanding of problem domains other systems like Mathematica and sympy do\n",
                "5. A systematic approach to hide or abstract things z3 should not care about\n",
                "\n",
                "For all these reasons, we may want a principled way to use Z3 to confirm \n",
                "\n",
                "In comes Knuckledragger.\n",
                "\n",
                "In principle, Knuckledragger is designed to be extremely minimalist. It can be implemented as a small number of idioms. There is a library however.\n",
                "\n",
                "1. Lots of little niceties. Pretty printing, useful combinators, tactics. The more easily you can write your statements, the more likely they are to correspond to what's in your head\n",
                "2. A library of axiomatized theories\n",
                "3. A bit of rigidity to guide you towards proofs that are more likely to be sound. \n"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 12,
            "metadata": {},
            "outputs": [],
            "source": [
                "def axiom(thm):\n",
                "    return thm\n",
                "\n",
                "def lemma(thm,by=[]):\n",
                "    z3.prove(z3.Implies(z3.And(by), thm))\n",
                "    return thm"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "1. Distinguishing between theorems to be proven and theorems that have been proven\n",
                "2. It is convenient and builds confidence to record a trace of the result coming in through these functions. These traces are recorded in a `Proof` tree which exactly reflects the call tree to `lemma` and `axiom` that produced to the Proof."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 11,
            "metadata": {},
            "outputs": [],
            "source": [
                "from dataclasses import dataclass\n",
                "\n",
                "@dataclass\n",
                "class Proof:\n",
                "    thm: z3.BoolRef\n",
                "    reasons: list[\"Proof\"]\n",
                "\n",
                "def axiom(thm):\n",
                "    return Proof(thm,[])\n",
                "\n",
                "def lemma(thm,by=[]):\n",
                "    assert all(isinstance(x,Proof) for x in by)\n",
                "    z3.prove(z3.Implies(z3.And(by), thm))\n",
                "    return Proof(thm,by)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "This is in essence the contents of `knuckledragger.kernel`."
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "# Knuckledragger\n",
                "\n",
                "But this has been packaged up for you in the `knuckledragger` package alongside many other goodies."
            ]
        },
        {
            "cell_type": "code",
            "execution_count": 3,
            "metadata": {},
            "outputs": [],
            "source": [
                "import kdrag as kd\n",
                "import kdrag.smt as smt # z3 is re-exported as kdrag.smt\n",
                "# or from kdrag.all import *"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {},
            "outputs": [],
            "source": [
                "G = smt.DeclareSort(\"G\")\n",
                "inv = smt.Function(\"inv\", G, G)\n",
                "mul = smt.Function(\"mul\", G, G, G)\n",
                "kd.notation.mul.register(G, mul) # enables e * inv(e) notation\n",
                "e = smt.Const(\"e\", G)\n",
                "x,y,z = smt.Consts(\"x y z\", G)\n",
                "mul_assoc = kd.axiom(smt.ForAll([x,y,z], x * (y * z) == (x * y) * z))\n",
                "mul_id = kd.axiom(smt.ForAll([x], x * e == x))\n",
                "mul_inv = kd.axiom(smt.ForAll([x], x * inv(x) == e))\n",
                "\n",
                "group_db = [mul_assoc, mul_id, mul_inv]\n",
                "def glemma(thm,by=[]):\n",
                "    return kd.prove(thm,by + group_db)"
            ]
        },
        {
            "cell_type": "markdown",
            "metadata": {},
            "source": [
                "# External Solvers\n",
                "\n",
                "Knuckledragger is designed to be used with other solvers. The experience using Z3 is by far the most polished due to the excellence of it's bindings. For some domain specific problems, or those requiring significant quantifier reasoning, the architecture of Z3 is not the best choice.\n",
                "\n",
                "Some of the installed solvers include\n",
                "\n",
                "- Vampire\n",
                "- E Prover\n",
                "- Twee\n",
                "- nanoCoP-i\n",
                "- Gappa\n",
                "- and More!\n"
            ]
        },
        {
            "cell_type": "code",
            "execution_count": null,
            "metadata": {
                "tags": [
                    "test_skip"
                ]
            },
            "outputs": [],
            "source": [
                "! cd knuckledragger && ./install.sh # get and build external solvers"
            ]
        }
    ],
    "metadata": {
        "kernelspec": {
            "display_name": ".venv",
            "language": "python",
            "name": "python3"
        },
        "language_info": {
            "codemirror_mode": {
                "name": "ipython",
                "version": 3
            },
            "file_extension": ".py",
            "mimetype": "text/x-python",
            "name": "python",
            "nbconvert_exporter": "python",
            "pygments_lexer": "ipython3",
            "version": "3.12.3"
        }
    },
    "nbformat": 4,
    "nbformat_minor": 2
}