<link rel="alternate" type="application/rss+xml" href="/rss.xml" title="IOG Engineering RSS Feed">
<link rel="alternate" type="application/atom+xml" href="/atom.xml" title="IOG Engineering Atom Feed">
<link rel="alternate" type="application/json" href="/feed.json" title="IOG Engineering JSON Feed"><title data-react-helmet="true">Model-Based Testing with QuickCheck | IOG Engineering</title><meta data-react-helmet="true" name="twitter:card" content="summary_large_image"><meta data-react-helmet="true" property="og:url" content="https://engineering.iog.io/2022-09-28-introduce-q-d"><meta data-react-helmet="true" name="docusaurus_locale" content="en"><meta data-react-helmet="true" name="docusaurus_tag" content="default"><meta data-react-helmet="true" property="og:title" content="Model-Based Testing with QuickCheck | IOG Engineering"><meta data-react-helmet="true" name="description" content="quickcheck-dynamic is a library jointly developed by Quviq and IOG, whose purpose is to leverage QuickCheck to test stateful programs against a Model. In other words, it's a Model-Based Testing tool. This article wants to be a gentle introduction to the use of quickcheck-dynamic for Model-Based Testing. It describes the overall approach, how the library works, and how it's being applied within IOG to improve the reach of our testing efforts."><meta data-react-helmet="true" property="og:description" content="quickcheck-dynamic is a library jointly developed by Quviq and IOG, whose purpose is to leverage QuickCheck to test stateful programs against a Model. In other words, it's a Model-Based Testing tool. This article wants to be a gentle introduction to the use of quickcheck-dynamic for Model-Based Testing. It describes the overall approach, how the library works, and how it's being applied within IOG to improve the reach of our testing efforts."><meta data-react-helmet="true" property="og:type" content="article"><meta data-react-helmet="true" property="article:published_time" content="2022-10-04T00:00:00.000Z"><meta data-react-helmet="true" property="article:tag" content="testing quickcheck"><link data-react-helmet="true" rel="icon" href="/img/favicon.ico"><link data-react-helmet="true" rel="canonical" href="https://engineering.iog.io/2022-09-28-introduce-q-d"><link data-react-helmet="true" rel="alternate" href="https://engineering.iog.io/2022-09-28-introduce-q-d" hreflang="en"><link data-react-helmet="true" rel="alternate" href="https://engineering.iog.io/2022-09-28-introduce-q-d" hreflang="x-default"><link rel="stylesheet" href="/assets/css/styles.10ad4647.css">
-
<link rel="preload" href="/assets/js/runtime~main.3aaa02eb.js" as="script">
-
<link rel="preload" href="/assets/js/main.602e5b06.js" as="script">
+
<link rel="preload" href="/assets/js/runtime~main.bf3bf9fc.js" as="script">
+
<link rel="preload" href="/assets/js/main.569da444.js" as="script">
<script>!function(){function t(t){document.documentElement.setAttribute("data-theme",t)}var e=function(){var t=null;try{t=localStorage.getItem("theme")}catch(t){}return t}();t(null!==e?e:"light")}()</script><div id="__docusaurus">
-
<div role="region"><a href="#" class="skipToContent_ZgBM">Skip to main content</a></div><nav class="navbar navbar--fixed-top"><div class="navbar__inner"><div class="navbar__items"><button aria-label="Navigation bar toggle" class="navbar__toggle clean-btn" type="button" tabindex="0"><svg width="30" height="30" viewBox="0 0 30 30" aria-hidden="true"><path stroke="currentColor" stroke-linecap="round" stroke-miterlimit="10" stroke-width="2" d="M4 7h22M4 15h22M4 23h22"></path></svg></button><a class="navbar__brand" href="/"><div class="navbar__logo"><img src="/img/iohk-logo.jpg" alt="IOG" class="themedImage_W2Cr themedImage--light_TfLj"><img src="/img/iohk-logo.jpg" alt="IOG" class="themedImage_W2Cr themedImage--dark_oUvU"></div><b class="navbar__title">Engineering</b></a><a aria-current="page" class="navbar__item navbar__link navbar__link--active" href="/">Recent</a><a class="navbar__item navbar__link" href="/tags">Tags</a><a class="navbar__item navbar__link" href="/archive">Archive</a></div><div class="navbar__items navbar__items--right"><div class="toggle_Pssr toggle_TdHA toggleDisabled_jDku"><div class="toggleTrack_SSoT" role="button" tabindex="-1"><div class="toggleTrackCheck_XobZ"><span class="toggleIcon_eZtF">🌜</span></div><div class="toggleTrackX_YkSC"><span class="toggleIcon_eZtF">🌞</span></div><div class="toggleTrackThumb_uRm4"></div></div><input type="checkbox" class="toggleScreenReader_JnkT" aria-label="Switch between dark and light mode"></div></div></div><div role="presentation" class="navbar-sidebar__backdrop"></div></nav><div class="main-wrapper blog-wrapper blog-post-page"><div class="container margin-vert--lg"><div class="row"><aside class="col col--3"><nav class="sidebar_a9qW thin-scrollbar" aria-label="Blog recent posts navigation"><div class="sidebarItemTitle_uKok margin-bottom--md">Recent posts</div><ul class="sidebarItemList_Kvuv"><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2023-01-24-javascript-browser-tutorial">Using GHC's JavaScript Backend in the Browser</a></li><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2023-01-12-ghc-update">GHC DevX Update 2023-01-12</a></li><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2022-12-13-ghc-js-backend-merged">JavaScript backend merged into GHC</a></li><li class="sidebarItem_CF0Q"><a aria-current="page" class="sidebarItemLink_miNk sidebarItemLinkActive_RRTD" href="/2022-09-28-introduce-q-d">Model-Based Testing with QuickCheck</a></li><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2022-09-23-ghcjs-heap-representation">GHCJS heap representation</a></li></ul></nav></aside><main class="col col--7" itemscope="" itemtype="http://schema.org/Blog"><article itemprop="blogPost" itemscope="" itemtype="http://schema.org/BlogPosting"><header><h1 class="blogPostTitle_rzP5" itemprop="headline">Model-Based Testing with QuickCheck</h1><div class="blogPostData_Zg1s margin-vert--md"><time datetime="2022-10-04T00:00:00.000Z" itemprop="datePublished">October 4, 2022</time> · <!-- -->15 min read</div><div class="margin-top--md margin-bottom--sm row"><div class="col col--6 authorCol_FlmR"><div class="avatar margin-bottom--sm"><div class="avatar__intro" itemprop="author" itemscope="" itemtype="https://schema.org/Person"><div class="avatar__name"><a itemprop="url"><span itemprop="name">Arnaud Bailly</span></a></div><small class="avatar__subtitle" itemprop="description">Technical Architect @ IOG</small></div></div></div></div></header><div id="post-content" class="markdown" itemprop="articleBody"><p><a href="https://github.com/input-output-hk/quickcheck-dynamic" target="_blank" rel="noopener noreferrer">quickcheck-dynamic</a> is a library jointly developed by Quviq and IOG, whose purpose is to leverage <a href="https://hackage.haskell.org/package/QuickCheck" target="_blank" rel="noopener noreferrer">QuickCheck</a> to test stateful programs against a <em>Model</em>. In other words, it's a <a href="https://en.wikipedia.org/wiki/Model-based_testing" target="_blank" rel="noopener noreferrer"><em>Model-Based Testing</em></a> tool. This article wants to be a gentle introduction to the use of quickcheck-dynamic for Model-Based Testing. It describes the overall approach, how the library works, and how it's being applied within IOG to improve the reach of our testing efforts.</p><h2 class="anchor anchorWithStickyNavbar_mojV" id="background">Background<a class="hash-link" href="#background" title="Direct link to heading"></a></h2><p>Testing stateful or rather effectful code using QuickCheck is not new: In particular, techniques to test <em>Monadic</em> code with QuickCheck have been introduced in <a href="https://dl.acm.org/doi/10.1145/636517.636527" target="_blank" rel="noopener noreferrer">Claessen & Hughes, 2002</a>. <code>quickcheck-dynamic</code> is based on a state-machine approach originally implemented by Quviq in closed-source <a href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.148.6554&rep=rep1&type=pdf" target="_blank" rel="noopener noreferrer">Erlang version of QuickCheck</a> and put to use to test various systems as explained in John Hughes' <a href="https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf" target="_blank" rel="noopener noreferrer">paper</a>.</p><p>IOG already has had experience with state-machine based testing in the Consensus <a href="https://github.com/input-output-hk/ouroboros-network/blob/nfrisby/old-benchmark-ledger-ops/ouroboros-consensus-test/README.md#L1" target="_blank" rel="noopener noreferrer">Storage layer</a> using <a href="https://hackage.haskell.org/package/quickcheck-state-machine" target="_blank" rel="noopener noreferrer">quickcheck-state-machine</a> library, but this was not widespread practice across the various teams.</p><p>When IOG started working on the Plutus Smart Contracts language and application framework, Quviq's consultancy was sought after to help test the platform and build tools for future Smart Contract implementors. This effort lead to the development of a custom library for testing smart contracts based on quickcheck-dynamic's state-machine model and dynamic logic language adapted from Erlang QuickCheck.</p><p>As quickcheck-dynamic matured, it attracted interest from other teams willing to invest into model-based testing and reuse existing effort. This finally lead to publication of the library as an independent package on <a href="https://hackage.haskell.org/package/quickcheck-dynamic" target="_blank" rel="noopener noreferrer">Hackage</a>, independently of the Plutus framework, in the hope it will be useful to a wider audience.</p><h2 class="anchor anchorWithStickyNavbar_mojV" id="use-cases">Use Cases<a class="hash-link" href="#use-cases" title="Direct link to heading"></a></h2><h3 class="anchor anchorWithStickyNavbar_mojV" id="example-thread-registry">Example: Thread Registry<a class="hash-link" href="#example-thread-registry" title="Direct link to heading"></a></h3><p>The library comes with a complete example defining a model and reference implementation for a <em>Thread Registry</em>. It's inspired by a similar example in Erlang from a couple of papers:</p><ul><li><a href="https://publications.lib.chalmers.se/records/fulltext/232552/local_232552.pdf" target="_blank" rel="noopener noreferrer">How well are your requirements tested?</a></li><li>and <a href="https://mengwangoxf.github.io/Papers/Erlang18.pdf" target="_blank" rel="noopener noreferrer">Understanding Formal Specifications through Good Examples</a></li></ul><p>The tests here use IOG's concurrent execution simulator library <a href="https://github.com/input-output-hk/io-sim" target="_blank" rel="noopener noreferrer">io-sim</a> to speed-up testing.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="lockstep-testing">Lockstep Testing<a class="hash-link" href="#lockstep-testing" title="Direct link to heading"></a></h3><p>Edsko de Vries wrote a <a href="https://well-typed.com/blog/2022/09/lockstep-with-quickcheck-dynamic/" target="_blank" rel="noopener noreferrer">nice blog post</a> to compare <code>quickcheck-dynamic</code> with <a href="https://hackage.haskell.org/package/quickcheck-state-machine" target="_blank" rel="noopener noreferrer">quickcheck-state-machine</a>, another library to write model-based tests on top of QuickCheck. This blog post introduces <a href="https://github.com/well-typed/quickcheck-lockstep" target="_blank" rel="noopener noreferrer">quickcheck-lockstep</a> which provides <em>lockstep-style</em> testing on top of quickcheck-dynamic.</p><p>Lockstep-style testing is a special case of Model-Based Testing whereby what's tested at each execution step of a test sequence is the equivalence up to some observability function, of the return values expected by the <em>Model</em> and the one provided by the <em>Implementation</em>. In other words, if we consider each step in the state-machine as a transition that, given some input and a starting state, produces some output and possibly a new state, then lockstep-style testing checks equivalence of the <em>output traces</em> from the model and the implementation.</p><p>The quickcheck-lockstep library provides generic implementations for most of the methods of the <code>StateModel</code> typeclass and dedicated type-classes to relate the Model and the Implementation.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="plutus-contracts">Plutus Contracts<a class="hash-link" href="#plutus-contracts" title="Direct link to heading"></a></h3><p>Within IOG, the quickcheck-dynamic testing approach was initially applied to provide a testing framework for Smart Contracts developers within the Plutus Application Backend. The Plutus documentation contains a <a href="https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html" target="_blank" rel="noopener noreferrer">detailed tutorial</a> on how to model smart contracts and tests them using underlying <em>Emulator</em>.</p><p>While the <em>Contract Model</em> is a specialised library dedicated to Smart contracts modeling and testing, the underlying principles are similar:</p><ul><li>Define a <code>ContractModel</code> with some state and actions representing the system behaviour,</li><li>Define a <code>perform</code> function that describes how the model's actions translate to real world calls to a Contract's <em>endpoints</em>,</li><li>then test the contracts implementation using properties written in the <em>Dynamic Logic</em> language provided by the framework.</li></ul><p>On top of quickcheck-dynamic, the <em>Contract Model</em> provides machinery to simplify definition of a model in the case of Plutus smart contracts and running tests against a set of _Wallets. More importantly, it predefines critical properties that all Smart Contracts should validate, like the <a href="https://github.com/input-output-hk/plutus-apps/blob/main/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs#L1719" target="_blank" rel="noopener noreferrer">No Locked Funds</a> or the more subtle <a href="https://github.com/input-output-hk/plutus-apps/blob/main/plutus-contract/src/Plutus/Contract/Test/ContractModel/DoubleSatisfaction.hs" target="_blank" rel="noopener noreferrer">Double Satisfaction</a> property. Smart contracts are somewhat infamous for being subject to subtle coding errors leading into loopholes which attackers can abuse to steal currencies from innocent users, because of the intrisic complexity of programming in a highly distributed and asynchronous model.</p><p>The Model-Based Testing approach supported by quickcheck-dynamic gives developers the tools to explore the state space in a much more systematic way.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="hydra">Hydra<a class="hash-link" href="#hydra" title="Direct link to heading"></a></h3><p><a href="https://hydra.family" target="_blank" rel="noopener noreferrer">Hydra</a> is a so-called <em>Layer 2</em> solution for Cardano that aims at increasing the throughput and latency of Cardano transactions by moving most of the traffic out of the main chain (<em>Layer 1</em>) and into smaller networks. The <em>Hydra Head</em> protocol is described in great details in a <a href="https://eprint.iacr.org/2020/299.pdf" target="_blank" rel="noopener noreferrer">research paper</a>.</p><p>At its core, Hydra is a state machine whose transitions are Layer 1 transactions, as depicted in the following picture:</p><p><img src="https://hydra.family/head-protocol/assets/images/hydra-head-lifecycle-b8449385e9041a214bf8c6e52830de3c.svg" alt="Hydra State Machine"></p><p>While the overall state machine appears relatively simple on the surface, the actual protocol is actually quite complex, involving cryptographic signatures and <em>Plutus Smart Contracts</em> to ensure the safety of the protocol. This safety is formally expressed in the paper as <em>properties</em> that are proven against an <em>Adversary Environment</em> whose capabilities are well-defined.</p><p>In order to guarantee the implementation provides those safety properties, the Hydra team has developed a diversified palette of testing techniques, including the use of quickcheck-dynamic. While the careful Test-Driven Development approach taken gives reasonable confidence most use cases and issues are covered, hopes are high that such a model is able to explore more corner cases and reveal subtle issues in the protocol implementation.</p><p>What was sought after is to be able to define and test Hydra Head security properties against the real implementation. As a first example the team tackled to get a feel of how quickcheck-dynamic could used, here one of the properties from the original paper is stated:</p><blockquote><p>• Conflict-Free Liveness (Head):</p><p>In presence of a network adversary, a conflict-free execution satisfies the following condition:
+
<div role="region"><a href="#" class="skipToContent_ZgBM">Skip to main content</a></div><nav class="navbar navbar--fixed-top"><div class="navbar__inner"><div class="navbar__items"><button aria-label="Navigation bar toggle" class="navbar__toggle clean-btn" type="button" tabindex="0"><svg width="30" height="30" viewBox="0 0 30 30" aria-hidden="true"><path stroke="currentColor" stroke-linecap="round" stroke-miterlimit="10" stroke-width="2" d="M4 7h22M4 15h22M4 23h22"></path></svg></button><a class="navbar__brand" href="/"><div class="navbar__logo"><img src="/img/iohk-logo.jpg" alt="IOG" class="themedImage_W2Cr themedImage--light_TfLj"><img src="/img/iohk-logo.jpg" alt="IOG" class="themedImage_W2Cr themedImage--dark_oUvU"></div><b class="navbar__title">Engineering</b></a><a aria-current="page" class="navbar__item navbar__link navbar__link--active" href="/">Recent</a><a class="navbar__item navbar__link" href="/tags">Tags</a><a class="navbar__item navbar__link" href="/archive">Archive</a></div><div class="navbar__items navbar__items--right"><div class="toggle_Pssr toggle_TdHA toggleDisabled_jDku"><div class="toggleTrack_SSoT" role="button" tabindex="-1"><div class="toggleTrackCheck_XobZ"><span class="toggleIcon_eZtF">🌜</span></div><div class="toggleTrackX_YkSC"><span class="toggleIcon_eZtF">🌞</span></div><div class="toggleTrackThumb_uRm4"></div></div><input type="checkbox" class="toggleScreenReader_JnkT" aria-label="Switch between dark and light mode"></div></div></div><div role="presentation" class="navbar-sidebar__backdrop"></div></nav><div class="main-wrapper blog-wrapper blog-post-page"><div class="container margin-vert--lg"><div class="row"><aside class="col col--3"><nav class="sidebar_a9qW thin-scrollbar" aria-label="Blog recent posts navigation"><div class="sidebarItemTitle_uKok margin-bottom--md">Recent posts</div><ul class="sidebarItemList_Kvuv"><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2023-01-26-hs-bindgen-introduction">One step forward, an easier interoperability between Rust and Haskell</a></li><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2023-01-24-javascript-browser-tutorial">Using GHC's JavaScript Backend in the Browser</a></li><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2023-01-12-ghc-update">GHC DevX Update 2023-01-12</a></li><li class="sidebarItem_CF0Q"><a class="sidebarItemLink_miNk" href="/2022-12-13-ghc-js-backend-merged">JavaScript backend merged into GHC</a></li><li class="sidebarItem_CF0Q"><a aria-current="page" class="sidebarItemLink_miNk sidebarItemLinkActive_RRTD" href="/2022-09-28-introduce-q-d">Model-Based Testing with QuickCheck</a></li></ul></nav></aside><main class="col col--7" itemscope="" itemtype="http://schema.org/Blog"><article itemprop="blogPost" itemscope="" itemtype="http://schema.org/BlogPosting"><header><h1 class="blogPostTitle_rzP5" itemprop="headline">Model-Based Testing with QuickCheck</h1><div class="blogPostData_Zg1s margin-vert--md"><time datetime="2022-10-04T00:00:00.000Z" itemprop="datePublished">October 4, 2022</time> · <!-- -->15 min read</div><div class="margin-top--md margin-bottom--sm row"><div class="col col--6 authorCol_FlmR"><div class="avatar margin-bottom--sm"><div class="avatar__intro" itemprop="author" itemscope="" itemtype="https://schema.org/Person"><div class="avatar__name"><a itemprop="url"><span itemprop="name">Arnaud Bailly</span></a></div><small class="avatar__subtitle" itemprop="description">Technical Architect @ IOG</small></div></div></div></div></header><div id="post-content" class="markdown" itemprop="articleBody"><p><a href="https://github.com/input-output-hk/quickcheck-dynamic" target="_blank" rel="noopener noreferrer">quickcheck-dynamic</a> is a library jointly developed by Quviq and IOG, whose purpose is to leverage <a href="https://hackage.haskell.org/package/QuickCheck" target="_blank" rel="noopener noreferrer">QuickCheck</a> to test stateful programs against a <em>Model</em>. In other words, it's a <a href="https://en.wikipedia.org/wiki/Model-based_testing" target="_blank" rel="noopener noreferrer"><em>Model-Based Testing</em></a> tool. This article wants to be a gentle introduction to the use of quickcheck-dynamic for Model-Based Testing. It describes the overall approach, how the library works, and how it's being applied within IOG to improve the reach of our testing efforts.</p><h2 class="anchor anchorWithStickyNavbar_mojV" id="background">Background<a class="hash-link" href="#background" title="Direct link to heading"></a></h2><p>Testing stateful or rather effectful code using QuickCheck is not new: In particular, techniques to test <em>Monadic</em> code with QuickCheck have been introduced in <a href="https://dl.acm.org/doi/10.1145/636517.636527" target="_blank" rel="noopener noreferrer">Claessen & Hughes, 2002</a>. <code>quickcheck-dynamic</code> is based on a state-machine approach originally implemented by Quviq in closed-source <a href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.148.6554&rep=rep1&type=pdf" target="_blank" rel="noopener noreferrer">Erlang version of QuickCheck</a> and put to use to test various systems as explained in John Hughes' <a href="https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf" target="_blank" rel="noopener noreferrer">paper</a>.</p><p>IOG already has had experience with state-machine based testing in the Consensus <a href="https://github.com/input-output-hk/ouroboros-network/blob/nfrisby/old-benchmark-ledger-ops/ouroboros-consensus-test/README.md#L1" target="_blank" rel="noopener noreferrer">Storage layer</a> using <a href="https://hackage.haskell.org/package/quickcheck-state-machine" target="_blank" rel="noopener noreferrer">quickcheck-state-machine</a> library, but this was not widespread practice across the various teams.</p><p>When IOG started working on the Plutus Smart Contracts language and application framework, Quviq's consultancy was sought after to help test the platform and build tools for future Smart Contract implementors. This effort lead to the development of a custom library for testing smart contracts based on quickcheck-dynamic's state-machine model and dynamic logic language adapted from Erlang QuickCheck.</p><p>As quickcheck-dynamic matured, it attracted interest from other teams willing to invest into model-based testing and reuse existing effort. This finally lead to publication of the library as an independent package on <a href="https://hackage.haskell.org/package/quickcheck-dynamic" target="_blank" rel="noopener noreferrer">Hackage</a>, independently of the Plutus framework, in the hope it will be useful to a wider audience.</p><h2 class="anchor anchorWithStickyNavbar_mojV" id="use-cases">Use Cases<a class="hash-link" href="#use-cases" title="Direct link to heading"></a></h2><h3 class="anchor anchorWithStickyNavbar_mojV" id="example-thread-registry">Example: Thread Registry<a class="hash-link" href="#example-thread-registry" title="Direct link to heading"></a></h3><p>The library comes with a complete example defining a model and reference implementation for a <em>Thread Registry</em>. It's inspired by a similar example in Erlang from a couple of papers:</p><ul><li><a href="https://publications.lib.chalmers.se/records/fulltext/232552/local_232552.pdf" target="_blank" rel="noopener noreferrer">How well are your requirements tested?</a></li><li>and <a href="https://mengwangoxf.github.io/Papers/Erlang18.pdf" target="_blank" rel="noopener noreferrer">Understanding Formal Specifications through Good Examples</a></li></ul><p>The tests here use IOG's concurrent execution simulator library <a href="https://github.com/input-output-hk/io-sim" target="_blank" rel="noopener noreferrer">io-sim</a> to speed-up testing.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="lockstep-testing">Lockstep Testing<a class="hash-link" href="#lockstep-testing" title="Direct link to heading"></a></h3><p>Edsko de Vries wrote a <a href="https://well-typed.com/blog/2022/09/lockstep-with-quickcheck-dynamic/" target="_blank" rel="noopener noreferrer">nice blog post</a> to compare <code>quickcheck-dynamic</code> with <a href="https://hackage.haskell.org/package/quickcheck-state-machine" target="_blank" rel="noopener noreferrer">quickcheck-state-machine</a>, another library to write model-based tests on top of QuickCheck. This blog post introduces <a href="https://github.com/well-typed/quickcheck-lockstep" target="_blank" rel="noopener noreferrer">quickcheck-lockstep</a> which provides <em>lockstep-style</em> testing on top of quickcheck-dynamic.</p><p>Lockstep-style testing is a special case of Model-Based Testing whereby what's tested at each execution step of a test sequence is the equivalence up to some observability function, of the return values expected by the <em>Model</em> and the one provided by the <em>Implementation</em>. In other words, if we consider each step in the state-machine as a transition that, given some input and a starting state, produces some output and possibly a new state, then lockstep-style testing checks equivalence of the <em>output traces</em> from the model and the implementation.</p><p>The quickcheck-lockstep library provides generic implementations for most of the methods of the <code>StateModel</code> typeclass and dedicated type-classes to relate the Model and the Implementation.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="plutus-contracts">Plutus Contracts<a class="hash-link" href="#plutus-contracts" title="Direct link to heading"></a></h3><p>Within IOG, the quickcheck-dynamic testing approach was initially applied to provide a testing framework for Smart Contracts developers within the Plutus Application Backend. The Plutus documentation contains a <a href="https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html" target="_blank" rel="noopener noreferrer">detailed tutorial</a> on how to model smart contracts and tests them using underlying <em>Emulator</em>.</p><p>While the <em>Contract Model</em> is a specialised library dedicated to Smart contracts modeling and testing, the underlying principles are similar:</p><ul><li>Define a <code>ContractModel</code> with some state and actions representing the system behaviour,</li><li>Define a <code>perform</code> function that describes how the model's actions translate to real world calls to a Contract's <em>endpoints</em>,</li><li>then test the contracts implementation using properties written in the <em>Dynamic Logic</em> language provided by the framework.</li></ul><p>On top of quickcheck-dynamic, the <em>Contract Model</em> provides machinery to simplify definition of a model in the case of Plutus smart contracts and running tests against a set of _Wallets. More importantly, it predefines critical properties that all Smart Contracts should validate, like the <a href="https://github.com/input-output-hk/plutus-apps/blob/main/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs#L1719" target="_blank" rel="noopener noreferrer">No Locked Funds</a> or the more subtle <a href="https://github.com/input-output-hk/plutus-apps/blob/main/plutus-contract/src/Plutus/Contract/Test/ContractModel/DoubleSatisfaction.hs" target="_blank" rel="noopener noreferrer">Double Satisfaction</a> property. Smart contracts are somewhat infamous for being subject to subtle coding errors leading into loopholes which attackers can abuse to steal currencies from innocent users, because of the intrisic complexity of programming in a highly distributed and asynchronous model.</p><p>The Model-Based Testing approach supported by quickcheck-dynamic gives developers the tools to explore the state space in a much more systematic way.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="hydra">Hydra<a class="hash-link" href="#hydra" title="Direct link to heading"></a></h3><p><a href="https://hydra.family" target="_blank" rel="noopener noreferrer">Hydra</a> is a so-called <em>Layer 2</em> solution for Cardano that aims at increasing the throughput and latency of Cardano transactions by moving most of the traffic out of the main chain (<em>Layer 1</em>) and into smaller networks. The <em>Hydra Head</em> protocol is described in great details in a <a href="https://eprint.iacr.org/2020/299.pdf" target="_blank" rel="noopener noreferrer">research paper</a>.</p><p>At its core, Hydra is a state machine whose transitions are Layer 1 transactions, as depicted in the following picture:</p><p><img src="https://hydra.family/head-protocol/assets/images/hydra-head-lifecycle-b8449385e9041a214bf8c6e52830de3c.svg" alt="Hydra State Machine"></p><p>While the overall state machine appears relatively simple on the surface, the actual protocol is actually quite complex, involving cryptographic signatures and <em>Plutus Smart Contracts</em> to ensure the safety of the protocol. This safety is formally expressed in the paper as <em>properties</em> that are proven against an <em>Adversary Environment</em> whose capabilities are well-defined.</p><p>In order to guarantee the implementation provides those safety properties, the Hydra team has developed a diversified palette of testing techniques, including the use of quickcheck-dynamic. While the careful Test-Driven Development approach taken gives reasonable confidence most use cases and issues are covered, hopes are high that such a model is able to explore more corner cases and reveal subtle issues in the protocol implementation.</p><p>What was sought after is to be able to define and test Hydra Head security properties against the real implementation. As a first example the team tackled to get a feel of how quickcheck-dynamic could used, here one of the properties from the original paper is stated:</p><blockquote><p>• Conflict-Free Liveness (Head):</p><p>In presence of a network adversary, a conflict-free execution satisfies the following condition:
For any transaction tx input via (new,tx), tx ∈ T i∈<!-- -->[n]<!-- --> Ci eventually holds.</p></blockquote><p>This property and similar ones are encoded as a <em>Dynamic Logic</em> expressions, and a suitable Model of a Hydra network is defined as an instance of <code>StateModel</code> from which test sequences representing User actions are generated.</p><p>Hydra is a distributed system where nodes are interconnected through a network layer, and each node needs to be connected to a cardano-node in order to preserve the security of the protocol. While testing an actual "cluster" of hydra and cardano nodes is definitely possible, and certainly desirable at some point in order to strengthen confidence in the whole system, it would also be very slow: Spinning up processes, establishing network connections, producing blocks on a chain, all take seconds if not minutes which makes any signficant exploration of the model state space practically infeasible.</p><p>Generated test traces are run within the <a href="https://github.com/input-output-hk/hydra-poc/blob/master/hydra-node/test/Hydra/ModelSpec.hs#L220" target="_blank" rel="noopener noreferrer">IOSim</a> monad which allows testing 100s of traces within seconds.</p><p>Of course, this means we won't be using real TCP/IP networking stack nor connection to a real Cardano node and chain to create a Hydra network, but this is actually not a liability but an asset. By <a href="https://abailly.github.io/posts/mocking-good-idea.html" target="_blank" rel="noopener noreferrer">mocking</a> the interfaces Hydra nodes use to communicate with other nodes and Cardano network, we are able to control the behaviour of the communication layer and <em>inject faults</em> representing some <em>Adversary</em>: Reordering or dropping messages, tampering the data, delaying requests...</p><h2 class="anchor anchorWithStickyNavbar_mojV" id="principles">Principles<a class="hash-link" href="#principles" title="Direct link to heading"></a></h2><p>We'll use the latter example to illustrate quickcheck-dynamic's principles and give the reader an intuition on the four steps that need to be defined in order to use it: Defining a test <em>Model</em>, stating how the model relates to the <em>Implementation</em>, expressing <em>Properties</em> and, last but not least, checking properties.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="defining-a-model">Defining a Model<a class="hash-link" href="#defining-a-model" title="Direct link to heading"></a></h3><p>In quickcheck-dynamic, a <em>Model</em> is some type, a representation of the expected state of the system-under-test, for which there exists an instance of the <a href="https://github.com/input-output-hk/quickcheck-dynamic/blob/abailly-iohk/blog-post/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs#L56" target="_blank" rel="noopener noreferrer">StateModel class</a> which sets the building blocks needed to generate and validate test sequences.</p><p>In the case of Hydra, the Model is a <code>IdealWorld</code> data type that control the Head parties and maintains a <code>GlobalState</code> which reflects the expected Head state:</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain">data IdealWorld = IdealWorld</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> { hydraParties :: [(SigningKey HydraKey, CardanoSigningKey)]</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> , hydraState :: GlobalState</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> }</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>We won't bother the reader with details of the <code>GlobalState</code> which basically encode the states as depicted in the state-machine picture hereabove in the form of an Algebraic Data-Type.</p><p>As the old saying from Alfred Korzybski goes, "The map is not the territory", hence to be useful a <em>Model</em> should abstract away irrelevant details for the purpose of testing. Furthermore, it's perfectly fine to use different models to test different aspects of the same implementation.</p><p>While the real Hydra layer two ledger does support a myriad of possible Cardano transactions, our model at hand is simpler and only uses <em>Two Party Payment</em> transactions:</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain">data Payment = Payment</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> { from :: CardanoSigningKey</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> , to :: CardanoSigningKey</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> , value :: Value</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> }</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>The first important part of the <code>StateModel</code> instance to define is the type of <code>Action</code> that are meaningful for the given <em>Model</em> and that can also be executed against the concrete implementation. The <code>Action</code> associated data-type is a GADT which allows the model to represent the type of <em>observable output</em> that can be produced by the implementation and which can be part of the model's validation logic.</p><p>The Hydra model needs to represent both on-chain and off-chain actions as the properties required from Hydra relates the two. The <code>Action</code> data-type represent user-facing commands and observations that can be made on the state of the system (please note at the time of writing this, the model is incomplete):</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain"> data Action IdealWorld a where</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Seed :: {seedKeys :: [(SigningKey HydraKey, CardanoSigningKey)]} -> Action IdealWorld ()</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Init :: Party -> ContestationPeriod -> Action IdealWorld ()</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Commit :: Party -> UTxOType Payment -> Action IdealWorld ActualCommitted</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Abort :: Party -> Action IdealWorld ()</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> NewTx :: Party -> Payment -> Action IdealWorld ()</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Wait :: DiffTime -> Action IdealWorld ()</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> ObserveConfirmedTx :: Payment -> Action IdealWorld ()</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>Then one needs to define:</p><ul><li>An <code>initialState</code>,</li><li>How to generate <code>arbitraryAction</code>s which will be used to produce sequences (or traces) of <code>Action</code>s to execute, depending on the current state,</li><li>A <code>precondition</code> function ensuring some <code>Action</code> is valid in some state. This function may seem redundant with the generator but is actually important when <em>shrinking</em> a failing test sequences: The execution engine will ensure the reduced sequence is still valid with respect to the model,</li><li>A <code>nextState</code> (transition) function that evolves the model state according to the <code>Action</code>s,</li><li>Auxiliary function <code>actionName</code> to providea human-readable representation of actions.</li></ul><p>The reader is invited to check the <a href="https://hackage.haskell.org/package/quickcheck-dynamic-1.1.0/docs/Test-QuickCheck-StateModel.html" target="_blank" rel="noopener noreferrer">Haddock</a> documentation of the library for further details.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="exercising-implementation">Exercising Implementation<a class="hash-link" href="#exercising-implementation" title="Direct link to heading"></a></h3><p>A <em>Model</em> alone is somewhat useless if we don't provide a way to relate it to the actual implementation of the system-under-test. <code>quickcheck-dynamic</code> provides the <a href="https://hackage.haskell.org/package/quickcheck-dynamic-1.1.0/docs/Test-QuickCheck-StateModel.html#t:RunModel" target="_blank" rel="noopener noreferrer"><code>RunModel</code></a> typeclass for this purpose. The most important function to define is <code>perform</code> which defines how <code>StateModel</code>'s <code>Action</code> should be executed against the implementation within some monadic context <code>m</code>. Having the actual execution <code>Monad m</code> be a parameter of the <code>RunModel</code> gives more flexibility to the implementor which is not tied to <code>IO</code> for example.</p><p>In the case of Hydra, the <code>perform</code> function is defined as:</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain"> perform ::</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> IdealWorld -></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Action IdealWorld a -></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> LookUp (StateT (Nodes m) m -></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> StateT (Nodes m) m a</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> perform st command _ = do</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> case command of</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Seed{seedKeys} -></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> seedWorld seedKeys</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Commit party utxo -></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> performCommit (snd <$> hydraParties st) party utxo</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain">...</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>The actual monad used is a classical <code>State</code> monad whose state maps a <code>Party</code> to the corresponding client connection to the Hydra node:</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain">data Nodes m = Nodes</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> { nodes :: Map.Map Party (TestHydraNode Tx m)</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> , logger :: Tracer m (HydraNodeLog Tx)</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> }</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>The <code>m</code> parameter is here kept somewhat unconstrained in order to make it possible to run properties within the <code>IOSim</code> monad for faster tests execution. Also note the presence of the <code>logger</code> field which is used to capture logging output from all the nodes: Should an error happen or a postcondition fail, we can dump the log of each node which is invaluable to troubleshoot such failures. In general, testing systems in a black-box way emphasises the importance of good logging to provide as much context as possible should issues arise, and using quickcheck-dynamic makes no exception.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="expressing-properties-with-dynamic-logic">Expressing Properties with Dynamic Logic<a class="hash-link" href="#expressing-properties-with-dynamic-logic" title="Direct link to heading"></a></h3><p>Once we have a <code>StateModel</code> we can express interesting <em>properties</em> to check against our <code>RunModel</code>. <a href="https://github.com/input-output-hk/quickcheck-dynamic/blob/abailly-iohk/link-to-blog-post/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs" target="_blank" rel="noopener noreferrer">Dynamic Logic</a> allows one to express properties through monadic expressions relating actions, states and logic predicates.</p><p>Dynamic Logic is a form of <em>modal logic</em>, similar to <a href="https://en.wikipedia.org/wiki/Temporal_logic" target="_blank" rel="noopener noreferrer">temporal logic</a>, but whose modalities are the <em>actions</em> (or programs) themselves. One can intertwine <em>programs</em> and logic predicates to specify the behaviour of the former when executing some statements and actually <a href="https://en.wikipedia.org/wiki/Dynamic_logic_(modal_logic)" target="_blank" rel="noopener noreferrer">Dynamic Logic</a> evolved from <em>Hoare's Triples</em>.</p><p>Here is the dynamic logic reformulation of the previously stated Hydra property which has been kept as close as possible to the original English statement:</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain">conflictFreeLiveness :: DL IdealWorld ()</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain">conflictFreeLiveness = do</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> anyActions_</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> getModelStateDL >>= \case</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> [email protected]{hydraState = Open{}} -> do</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> (party, payment) <- forAllQ (nonConflictingTx st)</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> action $ Model.NewTx party payment</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> eventually (ObserveConfirmedTx payment)</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> _ -> pass</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> where</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> nonConflictingTx st = withGenQ (genPayment st) (const [])</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> eventually a = action (Wait 10) >> action a</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>Note that in order to define this property we have introduced two "pseudo-actions" in the <em>Model</em>, <code>Wait</code> and <code>ObserveConfirmedTx</code>: Those <code>Action</code>s have no effect on the model itself, the former being used to introduce some delay in the context of distributed and asynchronous execution, and the latter serving the purpose of <em>observing</em> the current state of the SUT. An alternative formulation would have been to make <code>ObserveConfirmedTx</code> return the set of confirmed transactions and then express the condition as a logic predicate within the <code>conflictFreeLiveness</code> property's body.</p><h3 class="anchor anchorWithStickyNavbar_mojV" id="checking-properties">Checking Properties<a class="hash-link" href="#checking-properties" title="Direct link to heading"></a></h3><p>The last step in putting quickcheck-dynamic at work is to be able to connect the <em>StateModel</em>, the <em>RunModel</em>, and the <em>DynamicLogic</em> expression and turn those into a QuickCheck <code>Property</code> which can then be checked using the standard testing framework.</p><p>quickcheck-dynamic provides 2 functions for that purpose. The <code>forAllDL_</code> function (actually more a family of functions) will leverage <code>DL</code> formulae to generate sequences of <code>Action</code>s:</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain">prop_checkConflictFreeLiveness :: Property</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain">prop_checkConflictFreeLiveness =</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> forAllDL_ conflictFreeLiveness prop_HydraModel</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>The <code>runActions</code> function will execute the generated trace against the <code>RunModel</code>.</p><div class="codeBlockContainer_I0IT language-haskell theme-code-block"><div class="codeBlockContent_wNvx haskell"><pre tabindex="0" class="prism-code language-haskell codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain">prop_HydraModel :: Actions IdealWorld -> Property</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain">prop_HydraModel actions = property $</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> runIOSimProp $ do</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> _ <- runActions runIt actions</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> assert True</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>In this particular instance from Hydra, we need some additional machinery (the <code>runIOSimProp</code> function) to handle the execution of some monadic <code>PropertyM</code> into <code>IOSim</code> monad, turning it into a <code>Property</code>.</p><p>When run and successful, this <code>Property</code> generates the following output:</p><div class="codeBlockContainer_I0IT theme-code-block"><div class="codeBlockContent_wNvx"><pre tabindex="0" class="prism-code language-text codeBlock_jd64 thin-scrollbar" style="color:#393A34;background-color:#f6f8fa"><code class="codeBlockLines_mRuA"><span class="token-line" style="color:#393A34"><span class="token plain"> check conflict-free liveness</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> +++ OK, passed 100 tests.</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Actions (1334 in total):</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 49.93% NewTx</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 25.86% Commit</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 7.50% Seed</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 7.42% Init</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 4.80% Abort</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 2.25% ObserveConfirmedTx</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 2.25% Wait</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> Transitions (1334 in total):</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 54.42% Open -> Open</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 23.61% Initial -> Initial</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 7.50% Start -> Idle</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 7.42% Idle -> Initial</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 4.80% Initial -> Final</span><br></span><span class="token-line" style="color:#393A34"><span class="token plain"> 2.25% Initial -> Open</span><br></span></code></pre><button type="button" aria-label="Copy code to clipboard" class="copyButton_wuS7 clean-btn">Copy</button></div></div><p>By default, <code>runActions</code> decorate the QuickCheck output <em>tabulating</em> the executed <code>Action</code>. And thanks to the <code>monitoring</code> helper provided by the <code>RunModel</code>, this example also tabulates the executed <em>transitions</em> between each of the possible values for <code>GlobalState</code>. These pieces of information are important to assess the "quality" of the model: We want to make sure its generators and the properties execution covers all interesting parts of the Model, hence exercise all relevant parts of the implementation. Please note that, as we mentioned before, the Hydra model is still a work in progress hence the reason why there's no <code>Open -> Final</code> transition!</p><h2 class="anchor anchorWithStickyNavbar_mojV" id="conclusion">Conclusion<a class="hash-link" href="#conclusion" title="Direct link to heading"></a></h2><p>This articled introduced <a href="https://hackage.org/packages/quickcheck-dynamic" target="_blank" rel="noopener noreferrer">quickcheck-dynamic</a>, a novel Model-Based Testing library initially developed by Quviq for testing Plutus Smart Contracts and which has recently been open-sourced by IOG. I have tried to convey to the user a sense of the <em>Whys</em>, <em>Whats</em> and <em>Hows</em> questions this library answers through various examples and a high-level walkthrough of the steps needed to use this library for testing an implementation.</p><p><em>Model-Based Testing</em> is a powerful tool that simultaneously addresses both aspects of <a href="http://www.exampler.com/old-blog/2003/09/05.1.html#agile-testing-project-4" target="_blank" rel="noopener noreferrer">Customer-facing tests</a> as Brian Marick puts it in his famous <em>Agile Testing Quadrant</em> popularised by Lisa Crispin and Janet Gregory through their <a href="https://agiletester.ca/wp-content/uploads/sites/26/2015/07/Agile-tips-final.pdf" target="_blank" rel="noopener noreferrer">Agile Testing</a> books: <em>Supporting the team</em> by providing a reference model to build against, and <em>Critiquing the product</em> through the unique state-space exploration QuickCheck provides, possibly uncovering corner cases and blind spots in either the specification or the implementation.</p><p>The library is still evolving towards better developer experience and flexibility but it's already in a state that makes it possible to test something as significant as a Hydra network. And while it may appear somewhat involved when compared to more traditional forms of writing <em>Functional tests</em>, I hope I have demonstrated quickcheck-dynamic lowers the barrier to entry associated with most MBT tools.</p></div><footer class="row docusaurus-mt-lg blogPostDetailsFull_h6_j"><div class="col"><b>Tags:</b><ul class="tags_XVD_ padding--none margin-left--sm"><li class="tag_JSN8"><a class="tag_hD8n tagRegular_D6E_" href="/tags/testing-quickcheck">testing quickcheck</a></li></ul></div></footer></article><nav class="pagination-nav docusaurus-mt-lg" aria-label="Blog post page navigation"><div class="pagination-nav__item"><a class="pagination-nav__link" href="/2022-12-13-ghc-js-backend-merged"><div class="pagination-nav__sublabel">Newer Post</div><div class="pagination-nav__label">JavaScript backend merged into GHC</div></a></div><div class="pagination-nav__item pagination-nav__item--next"><a class="pagination-nav__link" href="/2022-09-23-ghcjs-heap-representation"><div class="pagination-nav__sublabel">Older Post</div><div class="pagination-nav__label">GHCJS heap representation</div></a></div></nav></main><div class="col col--2"><div class="tableOfContents_cNA8 thin-scrollbar"><ul class="table-of-contents table-of-contents__left-border"><li><a href="#background" class="table-of-contents__link toc-highlight">Background</a></li><li><a href="#use-cases" class="table-of-contents__link toc-highlight">Use Cases</a><ul><li><a href="#example-thread-registry" class="table-of-contents__link toc-highlight">Example: Thread Registry</a></li><li><a href="#lockstep-testing" class="table-of-contents__link toc-highlight">Lockstep Testing</a></li><li><a href="#plutus-contracts" class="table-of-contents__link toc-highlight">Plutus Contracts</a></li><li><a href="#hydra" class="table-of-contents__link toc-highlight">Hydra</a></li></ul></li><li><a href="#principles" class="table-of-contents__link toc-highlight">Principles</a><ul><li><a href="#defining-a-model" class="table-of-contents__link toc-highlight">Defining a Model</a></li><li><a href="#exercising-implementation" class="table-of-contents__link toc-highlight">Exercising Implementation</a></li><li><a href="#expressing-properties-with-dynamic-logic" class="table-of-contents__link toc-highlight">Expressing Properties with Dynamic Logic</a></li><li><a href="#checking-properties" class="table-of-contents__link toc-highlight">Checking Properties</a></li></ul></li><li><a href="#conclusion" class="table-of-contents__link toc-highlight">Conclusion</a></li></ul></div></div></div></div></div><footer class="footer footer--dark"><div class="container container-fluid"><div class="row footer__links"><div class="col footer__col"><div class="footer__title">Community</div><ul class="footer__items"><li class="footer__item"><a href="https://twitter.com/iog_eng" target="_blank" rel="noopener noreferrer" class="footer__link-item"><span>Twitter<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_I5OW"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></span></a></li></ul></div><div class="col footer__col"><div class="footer__title">More</div><ul class="footer__items"><li class="footer__item"><a href="https://iohk.io/en/blog" target="_blank" rel="noopener noreferrer" class="footer__link-item">IOG Blog</a></li><li class="footer__item"><a href="https://github.com/input-output-hk/" target="_blank" rel="noopener noreferrer" class="footer__link-item"><span>GitHub<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_I5OW"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></span></a></li></ul></div></div><div class="footer__bottom text--center"><div class="footer__copyright">Copyright © 2023 IOG Engineering, Inc. Built with Docusaurus.</div></div></div></footer></div>
-
<script src="/assets/js/runtime~main.3aaa02eb.js"></script>
-
<script src="/assets/js/main.602e5b06.js"></script>
+
<script src="/assets/js/runtime~main.bf3bf9fc.js"></script>
+
<script src="/assets/js/main.569da444.js"></script>
\ No newline at end of file
