Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts
span Relax.thy
13 B · 1 line
at main