VCVio: A Formally Verified Forking Lemma and Fiat-Shamir Transform, via a Flexible and Expressive Oracle Representation. - Devon Tuma; Nicholas Hopper (IACR Cryptol. ePrint Arch., 2024)