So there's also reveal() primitive for revealing secrets, as shown by the code for msqrt(). OK, Rune gives you a library for computing stuff in CT, but how do I implement something independent of these things and show that they are CT? Do I still need to rely on FM techniques such as relational symbolic execution? Can I jump into a "constant" mode with a special typing system or something that lets me do this without having to run a more costly verification?