ビット演算で、それが意図通りに動く事を証明する道具的な学問はなんですか?