While I haven't looked at the BitVM in detail, I would like to mention that Simplicity's core language (excluding introspection primitives) has the same expressivity as Boolean circuits.
A few years ago I did some experiments to compile Simplicity expressions to a system of polynomial constraints (R1CS). The experiments were successful. For instance, I was able to compile our Sha256 compression function specification written in Simplicity to a set of approximately 128,000 constraints. Under this "circuit" interpretation, Simplicity types represent cables, which are a bundle of wires equal to the 'bit size' of the given type. The 'case' combinator ends up being the only "active" component (implementing a demux). The 'injr' and 'injr' combinators output some fixed Boolean values. The rest of the combinations end up only connecting, bundling and unbundling wires, and contribute no constraints at all.
While my previous experiment was generating constraints, it is clear to me that a similar interpretation could instead generate logic gates, and I would expect the same order of magnitude in the number of gates generated as the number of constraints generated above. Thus Simplicity could be used as a source of ready made expressions to generate useful circuits for the BitVM, should someone be interested in pursuing this angle.