Merge branch 'master' of github.com:GaloisInc/cryptol

cryptol.cabal

@@ -64,7 +64,7 @@ library
                        random            >= 1.0.1,
                        sbv               >= 7.0,
                        smtLib            >= 1.0.7,
-                       simple-smt        >= 0.7.0,
+                       simple-smt        >= 0.7.1,
                        strict,
                        syb               >= 0.4,
                        text              >= 1.1,

docs/Syntax.md

@@ -107,12 +107,12 @@ Operator                                   Associativity
   `==>`                                    right
   `\/`                                     right
   `/\`                                     right
-  `||`                                     right
-  `&&`                                     right
   `->` (types)                             right
   `!=` `==`                                not associative
   `>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$`  not associative
+  `||`                                     right 
   `^`                                      left
+  `&&`                                     right 
   `#`                                      right
   `>>` `<<` `>>>` `<<<` `>>$`              left
   `+` `-`                                  left
@@ -168,11 +168,11 @@ Operator                                   Associativity       Description
  `==>`                                     right               Short-cut implication
  `\/`                                      right               Short-cut or
  `/\`                                      right               Short-cut and
-  `||`                                     right               Logical or
-  `&&`                                     right               Logical and
   `!=` `==`                                none                Not equals, equals
   `>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$`  none                Comparisons
+  `||`                                     right               Logical or 
   `^`                                      left                Exclusive-or
+  `&&`                                     right               Logical and 
   `~`                                      right               Logical negation
 
 Table: Bit operations.

tests/issues/Karatsuba.cry

@@ -0,0 +1,50 @@
+module Karatsuba where
+
+kmult : {limb,n} (fin n, fin limb, limb >= 6, n>=1) => [n] -> [n] -> [2*n]
+kmult x y =
+ if `n <= (demote`{limb, max (width limb) (width n)}) then
+   (zero#x)*(zero#y)
+ else
+   take (splitmult`{limb} (make_atleast`{limb} x) (make_atleast`{limb} y))
+
+make_atleast : {n, m, a} (fin n, fin m, Zero a) => [m]a -> [max n m]a
+make_atleast x = zero#x
+
+splitmult : {limb,n} (fin n, fin limb, limb >= 6, n>=6)
+         => [n] -> [n] -> [2*n]
+
+splitmult x y = (ac # bd) + (zero # ad_bc # (zero:[low]))
+  where
+   type hi  = n/2
+   type low = n - hi
+
+   (a,b) = splitAt`{hi} x
+   (c,d) = splitAt`{hi} y
+
+   ac : [2*hi]
+   ac = kmult`{limb,hi} a c
+
+   bd : [2*low]
+   bd = kmult`{limb,low} b d
+
+   a_b = (zext a) + (zext b)
+   c_d = (zext c) + (zext d)
+
+   ad_bc : [2*(low+1)]
+   ad_bc = (kmult`{limb,low+1} a_b c_d) - (zext ac) - (zext bd)
+
+
+property splitmult_correct_tiny (x:[9]) (y:[9]) =
+  zext x * zext y == splitmult`{limb=7} x y
+
+property splitmult_correct_small (x:[11]) (y:[11]) =
+  zext x * zext y == splitmult`{limb=7} x y
+
+property splitmult_correct_medium(x:[17]) (y:[17]) =
+  zext x * zext y == splitmult`{limb=7} x y
+
+property splitmult_correct_large (x:[59]) (y:[59]) =
+  zext x * zext y == splitmult`{limb=7} x y
+
+property splitmult_correct_huge (x:[511]) (y:[511]) =
+  zext x * zext y == splitmult`{limb=63} x y

tests/issues/T146.icry.fails

@@ -1 +1,2 @@
 Known problem. See #146.
+See also #323, which seems to be another instance of the same problem.

tests/issues/issue325.icry

@@ -0,0 +1,3 @@
+:set tests=100
+:l Karatsuba.cry
+:check splitmult_correct_large

tests/issues/issue325.icry.stdout

@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Karatsuba
+Using random testing.
+testing...passed 100 tests.
+Coverage: 0.00% (100 of 2^^118 values)

tests/issues/issue389.cry

@@ -0,0 +1,7 @@
+pad : {n, m, b} (64>=width(n), b==512-((n+65)%512), m==65+n+b) => [n]->[m]
+pad message = (message#[True])#(0:[b])#sz 
+     where 
+                sz : [64]
+                sz = width message
+
+test = pad

tests/issues/issue389.icry

@@ -0,0 +1,3 @@
+:l issue389.cry
+pad (join "a") 
+test (join "a")

tests/issues/issue389.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x61800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008
+0x61800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008

tests/issues/issue78.cry

@@ -0,0 +1,6 @@
+unique : {a,b} (fin a, fin b, a>=1) => [a][b] -> Bit
+unique xs = [ exist x (i+1) | x <- xs | i <- [0..(a-1)] ] == 0
+  where exist : [b] -> [width a] -> Bit
+        exist x i = if(i>=`a) then False
+                    else if(x==(xs@i)) then True
+                    else exist x (i+1)

tests/issues/issue78.icry

@@ -0,0 +1,2 @@
+:l issue78.cry
+:t unique

tests/issues/issue78.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+unique : {a, b} (fin a, fin b, a >= 1) => [a][b] -> Bit