acw/cryptonum
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add a bunch of QuickCheck properties for binary operators.

Browse Source
This commit is contained in:
Adam Wick
2019-07-30 18:24:49 -07:00
parent 1d8907539d
commit d7665acf64
1 changed files with 53 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

52
generation/src/BinaryOps.hs
View File

@@ -22,6 +22,10 @@ declareBinaryOperators bitsize =
out "use core::ops::{BitOr,BitOrAssign};" out "use core::ops::{BitOr,BitOrAssign};"
out "use core::ops::{BitXor,BitXorAssign};" out "use core::ops::{BitXor,BitXorAssign};"
out "use core::ops::Not;" out "use core::ops::Not;"
out "#[cfg(test)]"
out "use crate::CryptoNum;"
out "#[cfg(test)]"
out "use quickcheck::quickcheck;"
out ("use super::U" ++ show bitsize ++ ";") out ("use super::U" ++ show bitsize ++ ";")
blank blank
generateBinOps "BitAnd" name "bitand" "&=" entries generateBinOps "BitAnd" name "bitand" "&=" entries
@@ -46,6 +50,8 @@ declareBinaryOperators bitsize =
forM_ [0..entries-1] $ \ i -> forM_ [0..entries-1] $ \ i ->
out ("output.value[" ++ show i ++ "] = !self.value[" ++ show i ++ "];") out ("output.value[" ++ show i ++ "] = !self.value[" ++ show i ++ "];")
out "output" out "output"
blank
addBinaryLaws name
generateBinOps :: String -> String -> String -> String -> Word -> Gen () generateBinOps :: String -> String -> String -> String -> Word -> Gen ()
generateBinOps trait name fun op entries = generateBinOps trait name fun op entries =
@@ -91,3 +97,49 @@ generateBinOpsFromAssigns trait name fun op =
do out "let mut output = self.clone();" do out "let mut output = self.clone();"
out ("output " ++ op ++ " rhs;") out ("output " ++ op ++ " rhs;")
out "output" out "output"
addBinaryLaws :: String -> Gen ()
addBinaryLaws name =
do let args3 = "(a: " ++ name ++ ", b: " ++ name ++ ", c: " ++ name ++ ")"
args2 = "(a: " ++ name ++ ", b: " ++ name ++ ")"
out "#[cfg(test)]"
wrapIndent "quickcheck!" $
do wrapIndent ("fn and_associative" ++ args3 ++ " -> bool") $
out ("((&a & &b) & &c) == (&a & (&b & &c))")
blank
wrapIndent ("fn and_commutative" ++ args2 ++ " -> bool") $
out ("(&a & &b) == (&b & &a)")
blank
wrapIndent ("fn and_idempotent" ++ args2 ++ " -> bool") $
out ("(&a & &b) == (&a & &b & &a)")
blank
wrapIndent ("fn xor_associative" ++ args3 ++ " -> bool") $
out ("((&a ^ &b) ^ &c) == (&a ^ (&b ^ &c))")
blank
wrapIndent ("fn xor_commutative" ++ args2 ++ " -> bool") $
out ("(&a ^ &b) == (&b ^ &a)")
blank
wrapIndent ("fn or_associative" ++ args3 ++ " -> bool") $
out ("((&a | &b) | &c) == (&a | (&b | &c))")
blank
wrapIndent ("fn or_commutative" ++ args2 ++ " -> bool") $
out ("(&a | &b) == (&b | &a)")
blank
wrapIndent ("fn or_idempotent" ++ args2 ++ " -> bool") $
out ("(&a | &b) == (&a | &b | &a)")
blank
wrapIndent ("fn and_or_distribution" ++ args3 ++ "-> bool") $
out ("(&a & (&b | &c)) == ((&a & &b) | (&a & &c))")
blank
wrapIndent ("fn xor_clears(a: " ++ name ++ ") -> bool") $
out (name ++ "::zero() == (&a ^ &a)")
blank
wrapIndent ("fn double_neg_ident(a: " ++ name ++ ") -> bool") $
out ("a == !!&a")
blank
wrapIndent ("fn and_ident(a: " ++ name ++ ") -> bool") $
do out ("let ones = !" ++ name ++ "::zero();")
out ("(&a & &ones) == a")
blank
wrapIndent ("fn or_ident(a: " ++ name ++ ") -> bool") $
out ("(&a | " ++ name ++ "::zero()) == a")