.. DO NOT EDIT.
.. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY.
.. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE:
.. "api/gallery/vm/contracts/plot_02_bytecode_verification.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_vm_contracts_plot_02_bytecode_verification.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_vm_contracts_plot_02_bytecode_verification.py:


Bytecode verification: check before you run (Gosling 1995)
==========================================================

Java let browsers download and run code from strangers. Its virtual
machine first *verifies* the bytecode: by following every path through the
program without running it, it proves that no instruction can pop from an
empty stack and that every instruction is always reached with the same
stack height. Verified code needs no run-time stack checks and its maximum
stack size is known in advance. Ethereum's EOF format brings similar
validation at deployment.

What to look for
----------------

The verifier accepts the contracts in this package and computes their
maximum stack depth, which matches the deepest stack any run reaches. It
rejects a program with an underflow on a path that a test run happens not
to take, and a loop that grows the stack on every turn.

The history behind this experiment: :doc:`/history/vm_breakthroughs`.

.. GENERATED FROM PYTHON SOURCE LINES 25-27

Verify the library's contracts
------------------------------

.. GENERATED FROM PYTHON SOURCE LINES 27-45

.. code-block:: Python

    import matplotlib.pyplot as plt

    import blockchainkit as bk

    programs = {
        "vending machine": (bk.vm.vending_machine(), 1),
        "batch transfer": (bk.vm.batch_transfer(1, [2, 3], checked=True), 1),
        "expression": (bk.vm.compile_expression("1 + (2 * (3 + (4 * 5)))"), 0),
    }
    bounds = {}
    for name, (program, arguments) in programs.items():
        report = bk.vm.verify_bytecode(program, arguments=arguments)
        assert report.ok, report.errors
        bounds[name] = report.max_depth
    print(bounds)
    run = bk.vm.execute(programs["expression"][0], trace=True)
    assert max(len(step.stack) for step in run.trace) == bounds["expression"]





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

 .. code-block:: none

    {'vending machine': 3, 'batch transfer': 4, 'expression': 5}




.. GENERATED FROM PYTHON SOURCE LINES 46-49

A bug a test run can miss
-------------------------
The ADD after ``zero`` underflows, but only when the input is 0.

.. GENERATED FROM PYTHON SOURCE LINES 49-71

.. code-block:: Python

    buggy = bk.vm.assemble("""
        JZ zero
        PUSH 1
        PUSH 2
        ADD
        STOP
    zero:
        ADD
    """)
    assert bk.vm.execute(buggy, arguments=(1,)).stack == (3,)  # The tested path works.
    report = bk.vm.verify_bytecode(buggy, arguments=1)
    print(report.errors)
    assert not report.ok

    growing = bk.vm.assemble("top:\n    PUSH 1\n    JMP top")
    print(bk.vm.verify_bytecode(growing).errors)

    fig, ax = plt.subplots(figsize=(6, 3.5))
    ax.barh(list(bounds), list(bounds.values()), color="#0d9488")
    ax.set(xlabel="maximum stack depth, proved before running", title="Verified programs")
    fig.tight_layout()




.. image-sg:: /api/gallery/vm/contracts/images/sphx_glr_plot_02_bytecode_verification_001.png
   :alt: Verified programs
   :srcset: /api/gallery/vm/contracts/images/sphx_glr_plot_02_bytecode_verification_001.png
   :class: sphx-glr-single-img


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

 .. code-block:: none

    ('pc 5: ADD needs 2 values but only 0 can be on the stack',)
    ('pc 0: reached with stack heights 0 and 1',)




.. GENERATED FROM PYTHON SOURCE LINES 72-77

Exercise
--------
The verifier rejects every program whose stack height depends on the path,
even some that would never fail. Write such a program, and explain why
Java accepted this loss of expressiveness.


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

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


.. _sphx_glr_download_api_gallery_vm_contracts_plot_02_bytecode_verification.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/vm/contracts/plot_02_bytecode_verification.ipynb
        :alt: Launch JupyterLite
        :width: 150 px

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

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

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

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

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

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


.. only:: html

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

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