BitVM: Compute Anything on Bitcoin

Simplicity's core language, excluding introspection primitives, has the same expressivity as Boolean circuits. The author conducted experiments a few years ago to compile Simplicity expressions to a system of polynomial constraints (R1CS) with successful results. For example, the Sha256 compression function specification written in Simplicity was compiled to approximately 128,000 constraints. In this "circuit" interpretation, Simplicity types represent cables, which are bundles of wires equal to the 'bit size' of the type. The 'case' combinator serves as the only active component, implementing a demultiplexer. The 'injr' and 'injr' combinators output fixed Boolean values. Other combinations in Simplicity only connect, bundle, and unbundle wires without contributing any constraints.While the previous experiment focused on generating constraints, the author believes that a similar interpretation could generate logic gates instead. They expect the number of gates generated to be in the same order of magnitude as the number of constraints. This suggests that Simplicity could be used as a source of ready-made expressions to generate useful circuits for the BitVM, should anyone be interested in pursuing this approach.