The BCS transform turns the SWIRL IOP into a non-interactive proof. We prove in Lean that the compiled protocol stays knowledge sound in the random permutation model, and that its verifier is the one SWIRL actually runs.
Fiat-Shamir security is proven using the BCS transformation. We prove that the BCS transformation preserves knowledge soundness when compiling an interactive oracle protocol (IOP) into a non-interactive random oracle protocol (NIROP). We apply the BCS transformation to the SWIRL IOP to get knowledge soundness of the SWIRL NIROP with respect to the BCS-compiled verifier. We then prove equivalence between this compiled verifier and the SWIRL reference verifier.
