BitVM: Compute Anything on Bitcoin

The email discusses the potential use of Simplicity, a core language with the same expressivity as Boolean circuits, in generating useful circuits for BitVM. The sender mentions that they have previously experimented with compiling Simplicity expressions to a system of polynomial constraints (R1CS) and were successful in generating approximately 128,000 constraints from a Sha256 compression function specification written in Simplicity.

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 'injl' combinators output fixed Boolean values. The other combinations mainly connect, bundle, and unbundle wires, without contributing any constraints.

While the previous experiment generated constraints, the sender suggests that a similar interpretation could generate logic gates instead. They anticipate that the number of gates generated would be in the same order of magnitude as the number of constraints generated previously. Consequently, Simplicity could potentially serve as a source of ready-made expressions to generate useful circuits for BitVM, if someone is interested in exploring this approach further.