Random Testing of a Higher-Order Blockchain Language (Experience Report)
summary
Integrates QuickChick on Coq with an OCaml implementation of a higher‑order smart‑contract language and builds a semantic harness by turning the monadic reference interpreter into a state‑collection trace reporter. Implements generators for well‑typed System F fragments using type‑sigma instantiation and frequency control. Finds ~11 confirmed bugs across interpreter, cost model and compiler, with 7 of 10 bugs new and one control‑flow analysis case that makes the compiler take cubic time, causing denial‑of‑service. OCaml reference interpreter
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:47Getting Your Code on a Blockchain
- 1:48Using Your Code on a Blockchain
- 3:11Static Semantics Bug
- 4:52Cost Semantics Bug
- 6:23A Compiler Exploit
- 6:40Scenario 3: A Replicated Compiler Exploit
- 7:15Language-Layer Bugs
- 9:35Property-Based Testing
- 9:59Testing Language Properties
- 12:17Generating System F Terms
- 13:58Testing Control- and Type-Flow Analysis in Scilla Compiler
- 14:43Monadic Interpreters to the Rescue
- 16:38Type Variable Shadowing Bug (#2)
related talks
42mSurprise yourself with Property Based Testing
14mVerify, but test: extracting property-based tests from F* specifications
18mMulticoretests - Parallel Testing Libraries for OCaml 5.0
15mGrammar-Based Testing for Little Languages: An Experience Report with Student Compilers
33mLets Generate Tests
47mTesting the Hard Stuff and Staying Sane
28mEtna: An Evaluation Platform for Property-Based Testing
19mCovering All the Bases: Type-Based Verification of Test Input Generators