mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-18 05:21:57 +03:00
19 lines
587 B
Plaintext
19 lines
587 B
Plaintext
:set warnDefaulting=off
|
|
:l HighAssurance.tex
|
|
:prove caesarCorrect : ([8], String 12) -> Bit
|
|
:prove sqDiffsCorrect
|
|
:prove revRev : ([16] -> Bit)
|
|
:prove appAssoc : ([16], [12], [28]) -> Bit
|
|
:prove revApp : ([10][8], [5][8]) -> Bit
|
|
:prove lshMul : ([32], [32]) -> Bit
|
|
:prove inctest
|
|
:prove multShift : ([32] -> Bit)
|
|
:prove flipNeverIdentity : ([32] -> Bit)
|
|
:prove widthPoly : ([15] -> Bit)
|
|
:prove widthPoly : ([16] -> Bit)
|
|
:prove evenWidth : ([16] -> Bit)
|
|
:prove evenWidth : ([15] -> Bit)
|
|
:prove divModMul : ([12], [12]) -> Bit
|
|
:prove modelEnigmaCorrect : (String 12 -> Bit)
|
|
:prove easyBug
|