Verification example

verification-example.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": [],
      "collapsed_sections": [],
      "authorship_tag": "ABX9TyPGDDWdJLCr9t20Iuik80A8",
      "include_colab_link": true
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/gist/duytai/6cdea5d768cfcfad970658d37afea00b/verification-example.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "# 1. Theory of Arrays $T_A$\n",
        "\n",
        "$\\Sigma_A : \\{select, store, =\\}$ where\n",
        "\n",
        "- $select(a,i)$ is a binary function that reads array $a$ at index $i$\n",
        "- $store(a, i, v)$ s a ternary function that writes value $v$ to index $i$ of array $a$\n",
        "\n",
        "Axioms of $T_A$ [McCarthy]\n",
        "\n",
        "- $\\forall a, i, j. i = j \\Rightarrow select(a,i) = select(a,j)$ (array congruence)\n",
        "- $\\forall a,v,i,j. i = j \\Rightarrow select(store(a,i,v),j) = v$ (read-over-write)\n",
        "- $\\forall a,v,i,j. i \\neq j \\Rightarrow select(store(a,i,v),j) = select(a,j)$\n",
        "- $\\forall a, b. \\exists i. a \\neq b \\Rightarrow select(a, i) \\neq select(b, i)$\n",
        "\n",
        "Z3 employs the theories of equality with uninterpreted functions (UEF) to implement axioms above.\n",
        "\n",
        "### Example 1:\n",
        "$a, b$ are 1-dimension arrays and $x$ is an index\n",
        "\n",
        "$a[x] = 10$ **encode**: $Store(a, x, 10)$\n",
        "\n",
        "$a[x] = 10; a[x] + 100 > 10$ \n",
        "**encode**: $b = Store(a, x, 10) \\land Select(b, x) + 100 > 10$\n",
        "\n",
        "### Example 2:\n",
        "$a, b$ are 2-dimension arrays and $x, y$ are indexes\n",
        "\n",
        "$a[x][y] = 10$ **encode**: $Store(a, x, Store(Select(a, x), y, 10))$\n",
        "\n",
        "$a[x][y] = 10; a[x][y] + 100 > 10$ **encode**: $b = Store(a, x, Store(Select(a, x), y, 10)) \\land  Select(Select(b, x), y) + 100 > 10$\n",
        "\n",
        "# 2. Algebraic Datatypes\n",
        "\n",
        "The theory of first-order algebraic data-types captures the theory of finite trees. It is characterized by the properties that:\n",
        "\n",
        "- All trees are finite (occurs check).\n",
        "- All trees are generated from the constructors (no junk).\n",
        "- Two trees are equal if and only if they are constructed exactly the same way (no confusion).\n",
        "\n",
        "Example 3: Binary tree\n",
        "```python\n",
        "Z = IntSort() # type int\n",
        "Tree = Datatype('Tree')\n",
        "Tree.declare('Empty')\n",
        "Tree.declare('Node', ('left', Tree), ('data', Z), ('right', Tree))\n",
        "Tree = Tree.create()\n",
        "```"
      ],
      "metadata": {
        "id": "7LxNfX6Qm9VQ"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "# Demo"
      ],
      "metadata": {
        "id": "08ptX191n5tl"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "!pip install z3-solver\n",
        "from z3 import *"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 0
        },
        "id": "IhtDkfr0XjLW",
        "outputId": "ccd0042a-c1c4-48d0-be81-ebb932628de6"
      },
      "execution_count": 41,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Looking in indexes: https://pypi.org/simple, https://us-python.pkg.dev/colab-wheels/public/simple/\n",
            "Requirement already satisfied: z3-solver in /usr/local/lib/python3.7/dist-packages (4.11.2.0)\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "Z = IntSort()\n",
        "B = BoolSort()\n",
        "A = ArraySort(Z, ArraySort(Z, Z)) # A: Z -> (Z -> Z)"
      ],
      "metadata": {
        "id": "usU1S5FcXLkI"
      },
      "execution_count": 95,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "source": [
        "# code\n",
        "\n",
        "```javascript\n",
        "struct ABC {uint a; bool b}\n",
        "uint[][] xs;\n",
        "bool ok;\n",
        "int z;\n",
        "ABC abc = ABC(10, 20);\n",
        "xs[0][10] = 100;\n",
        "z = 2 + xs[0][10] + abc.a;\n",
        "assert(z == 112)\n",
        "```"
      ],
      "metadata": {
        "id": "gAHvvt0Llgpm"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "# Verification"
      ],
      "metadata": {
        "id": "LD0HOl0gloo-"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "\n",
        "# Create type ABC\n",
        "ABC = Datatype('ABC')\n",
        "ABC.declare('data', ('a', Z), ('b', B))\n",
        "ABC = ABC.create()\n",
        "\n",
        "# Create type Sigma\n",
        "Sigma = Datatype('Sigma')\n",
        "Sigma.declare('data', ('xs', A), ('ok', B), ('z', Z), ('abc', ABC))\n",
        "Sigma = Sigma.create()\n",
        "\n",
        "# Create initial state sigma\n",
        "sigma = Const('sigma', Sigma)\n",
        "\n",
        "# ❮ abc := ABC(10, 20), sigma_0 ❯ ⇩ sigma_1\n",
        "abc = TSelect(sigma, 'abc')\n",
        "abc = TStore(abc, 'a', 10) # abc.a = 10\n",
        "abc = TStore(abc, 'b', BoolVal(True)) # abc.b = True\n",
        "sigma = TStore(sigma, 'abc', abc)\n",
        "\n",
        "# ❮ xs[0][10] := 100, sigma_1 ❯ ⇩ sigma_2\n",
        "xs = TSelect(sigma, 'xs') \n",
        "xs = Store(xs, 0, Store(Select(xs, 0), 10, 100)) # xs[0][10] = 100\n",
        "sigma = TStore(sigma, 'xs', xs)\n",
        "\n",
        "# ❮ z := 2 + xs[0][10] + abc.a, sigma_2 ❯ ⇩ sigma_3\n",
        "z = TSelect(sigma, 'z')\n",
        "xs = TSelect(sigma, 'xs')\n",
        "abc = TSelect(sigma, 'abc')\n",
        "z = 2 + Select(Select(xs, 0), 10) + TSelect(abc, 'a') # z = xs[0][10] + 2 + abc.a\n",
        "sigma = TStore(sigma, 'z', z)\n",
        "\n",
        "# assert(z == 112)\n",
        "z = TSelect(sigma, 'z')\n",
        "xs = TSelect(sigma, 'xs')\n",
        "abc = TSelect(sigma, 'abc')\n",
        "\n",
        "solver = Solver()\n",
        "print('result: {}'.format(solver.check(z == 112)))\n",
        "print(solver.model().eval(z))\n",
        "print(solver.model().eval(abc))\n",
        "print(solver.model().eval(xs[0][10]))"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "koNWWFVWYm_i",
        "outputId": "f37b18a4-865f-4552-a262-860bbabb1e96"
      },
      "execution_count": 101,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "result: sat\n",
            "112\n",
            "data(10, True)\n",
            "100\n"
          ]
        }
      ]
    },
    {
      "cell_type": "code",
      "source": [
        "# Similar to Store. However it works on struct\n",
        "def TStore(sigma, name, val):\n",
        "    values = []\n",
        "    sort = sigma.sort()\n",
        "    for idx in range(sort.constructor(0).arity()):\n",
        "        acc = sort.accessor(0, idx)\n",
        "        if acc.name() == name:\n",
        "            values.append(val)\n",
        "        else:\n",
        "            values.append(acc(sigma))\n",
        "    return sort.constructor(0)(values)\n",
        "\n",
        "# Similar to Select. However it works on struct\n",
        "def TSelect(sigma, name):\n",
        "    sort = sigma.sort()\n",
        "    for idx in range(sort.constructor(0).arity()):\n",
        "        acc = sort.accessor(0, idx)\n",
        "        if acc.name() == name:\n",
        "            return acc(sigma)\n",
        "    return None"
      ],
      "metadata": {
        "id": "uiIehZEeZ2Ts"
      },
      "execution_count": 97,
      "outputs": []
    },
    {
      "cell_type": "code",
      "source": [],
      "metadata": {
        "id": "LGZF8b5uohMw"
      },
      "execution_count": null,
      "outputs": []
    }
  ]
}