.. DO NOT EDIT.
.. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY.
.. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE:
.. "api/gallery/contracts/verification/plot_02_symbolic_execution.py"
.. LINE NUMBERS ARE GIVEN BELOW.

.. only:: html

    .. note::
        :class: sphx-glr-download-link-note

        :ref:`Go to the end <sphx_glr_download_api_gallery_contracts_verification_plot_02_symbolic_execution.py>`
        to download the full example code or to run this example in your browser via JupyterLite.

.. rst-class:: sphx-glr-example-title

.. _sphx_glr_api_gallery_contracts_verification_plot_02_symbolic_execution.py:


King's symbolic execution: every path of a fee schedule (1976)
==============================================================

James King proposed running a program on symbols instead of numbers. Every
variable holds an expression over the inputs, and each branch on such an
expression forks the run in two. Each path then carries a *path condition*,
the conjunction of the decisions it took:

.. math::

   \mathrm{pc} = c_1 \wedge \neg c_2 \wedge \dots

Any input satisfying the path condition drives a concrete run down exactly
that path, so solving the condition of a path that fails an assertion
produces a bug-triggering input, without guessing.

The program charges a fee that depends on the amount. Its check only
requires ``amount <= balance``, forgetting the fee. Symbolic execution
finds five paths, and solving the two that fail the assertion yields inputs
that leave a negative balance.

.. GENERATED FROM PYTHON SOURCE LINES 25-30

.. code-block:: Python

    import matplotlib.pyplot as plt

    import blockchainkit as bk
    from blockchainkit.contracts.visualizers import plot_symbolic_paths








.. GENERATED FROM PYTHON SOURCE LINES 31-33

Explore every path
------------------

.. GENERATED FROM PYTHON SOURCE LINES 33-50

.. code-block:: Python


    program = """
    require(amount <= balance)
    if amount > 100:
        fee = 2
    else:
        fee = 1
    balance = balance - amount - fee
    assert balance >= 0
    """
    result = bk.contracts.symbolic_execute(program)
    print(result.outcomes)
    for path in result.paths:
        condition = " and ".join(bk.contracts.to_source(c) for c in path.conditions)
        print(f"{path.outcome:9s} if {condition}")
    assert result.outcomes == {"reverted": 1, "assertion": 2, "ok": 2}





.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    {'reverted': 1, 'assertion': 2, 'ok': 2}
    reverted  if not amount <= balance
    assertion if amount <= balance and amount > 100 and not balance - amount - 2 >= 0
    ok        if amount <= balance and amount > 100 and balance - amount - 2 >= 0
    assertion if amount <= balance and not amount > 100 and not balance - amount - 1 >= 0
    ok        if amount <= balance and not amount > 100 and balance - amount - 1 >= 0




.. GENERATED FROM PYTHON SOURCE LINES 51-55

Solve the failing paths
-----------------------
The solver tries boundary values: 0, 1, 2, and every constant in the
condition with its neighbors.

.. GENERATED FROM PYTHON SOURCE LINES 55-77

.. code-block:: Python


    for path in result.paths:
        if path.outcome == "assertion":
            witness = bk.contracts.solve(path.conditions)
            outcome, final = bk.contracts.run_program(program, witness)
            print(witness, "->", outcome, "balance", final["balance"])
            assert outcome == "assertion" and final["balance"] < 0

    fixed = program.replace("amount <= balance", "amount + 2 <= balance")
    fixed_paths = bk.contracts.symbolic_execute(fixed).paths
    assert all(
        bk.contracts.solve(path.conditions) is None
        for path in fixed_paths
        if path.outcome == "assertion"
    )

    fig, ax = plt.subplots(figsize=(7, 4))
    plot_symbolic_paths(result, ax=ax)
    fig.tight_layout()

    plt.show()




.. image-sg:: /api/gallery/contracts/verification/images/sphx_glr_plot_02_symbolic_execution_001.png
   :alt: 5 paths over amount, balance
   :srcset: /api/gallery/contracts/verification/images/sphx_glr_plot_02_symbolic_execution_001.png
   :class: sphx-glr-single-img


.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    {'amount': 101, 'balance': 101} -> assertion balance -2
    {'amount': 0, 'balance': 0} -> assertion balance -1




.. GENERATED FROM PYTHON SOURCE LINES 78-83

Exercise
--------
Add a third fee tier (``amount > 1000`` pays 5). How many paths does
symbolic execution find now, and how many does a program with ``n``
independent ``if`` statements have in the worst case?


.. rst-class:: sphx-glr-timing

   **Total running time of the script:** (0 minutes 0.029 seconds)


.. _sphx_glr_download_api_gallery_contracts_verification_plot_02_symbolic_execution.py:

.. only:: html

  .. container:: sphx-glr-footer sphx-glr-footer-example

    .. container:: lite-badge

      .. image:: images/jupyterlite_badge_logo.svg
        :target: ../../../../lite/lab/index.html?path=api/gallery/contracts/verification/plot_02_symbolic_execution.ipynb
        :alt: Launch JupyterLite
        :width: 150 px

    .. container:: sphx-glr-download sphx-glr-download-jupyter

      :download:`Download Jupyter notebook: plot_02_symbolic_execution.ipynb <plot_02_symbolic_execution.ipynb>`

    .. container:: sphx-glr-download sphx-glr-download-python

      :download:`Download Python source code: plot_02_symbolic_execution.py <plot_02_symbolic_execution.py>`

    .. container:: sphx-glr-download sphx-glr-download-zip

      :download:`Download zipped: plot_02_symbolic_execution.zip <plot_02_symbolic_execution.zip>`


.. only:: html

 .. rst-class:: sphx-glr-signature

    `Gallery generated by Sphinx-Gallery <https://sphinx-gallery.github.io>`_