Ah, thanks for the correction. Do I have the soundness bit right? I guess it might apply even if the proof system is only computationally sound, since the simulator has to be efficient, right?