Merge pull request #1221 from GaloisInc/what4-bump

What4 bump
GaloisInc · Jun 22, 2021 · 03ca52c · 03ca52c
2 parents 6669193 + 4a68856
commit 03ca52c
Show file tree

Hide file tree

Showing 8 changed files with 58 additions and 4 deletions.
diff --git a/cabal.GHC-8.10.2.config b/cabal.GHC-8.10.2.config
@@ -218,6 +218,8 @@ constraints: any.Cabal ==3.2.0.0,
              void -safe,
              any.wcwidth ==0.0.2,
              wcwidth -cli +split-base,
+             any.what4 ==1.2.1,
+             what4 -drealtestdisable -solvertests -stptestdisable,
              any.wl-pprint-annotated ==0.1.0.1,
              any.xml ==1.3.14,
              any.zenc ==0.1.1,

diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config
@@ -273,7 +273,7 @@ constraints: any.Cabal ==3.2.1.0,
              warp +allow-sendfilefd -network-bytestring -warp-debug,
              any.wcwidth ==0.0.2,
              wcwidth -cli +split-base,
-             any.what4 ==1.1,
+             any.what4 ==1.2.1,
              what4 -drealtestdisable -solvertests -stptestdisable,
              any.word8 ==0.1.3,
              any.x509 ==1.7.5,

diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config
@@ -214,7 +214,7 @@ constraints: any.Cabal ==2.4.0.1,
              void -safe,
              any.wcwidth ==0.0.2,
              wcwidth -cli +split-base,
-             any.what4 ==1.1,
+             any.what4 ==1.2.1,
              what4 -drealtestdisable -solvertests -stptestdisable,
              any.wl-pprint-annotated ==0.1.0.1,
              any.xml ==1.3.14,

diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
@@ -211,7 +211,7 @@ constraints: any.Cabal ==3.0.1.0,
              void -safe,
              any.wcwidth ==0.0.2,
              wcwidth -cli +split-base,
-             any.what4 ==1.1,
+             any.what4 ==1.2.1,
              what4 -drealtestdisable -solvertests -stptestdisable,
              any.wl-pprint-annotated ==0.1.0.1,
              any.xml ==1.3.14,

diff --git a/cryptol.cabal b/cryptol.cabal
@@ -74,7 +74,7 @@ library
                        mtl               >= 2.2.1,
                        time              >= 1.6.0.1,
                        panic             >= 0.3,
-                       what4             >= 1.1 && < 1.2
+                       what4             >= 1.2 && < 1.3
 
   Build-tool-depends:  alex:alex, happy:happy
   hs-source-dirs:      src

diff --git a/tests/issues/issue1210.cry b/tests/issues/issue1210.cry
@@ -0,0 +1,15 @@
+mwe : [2] -> [2][1] -> Bit
+property mwe i r = r@0 == (r@0) << 0*i
+
+mwe' : [2] -> [1] -> Bit
+property mwe' i r = r == (r << 0*i)
+
+mwe'' : Bit
+property mwe'' = r == (r << i)
+ where r = 1:[1]
+       i = 0:[2]
+
+bitget : [12] -> [436][8] -> Bit
+property bitget i r = i < 3488 ==> bit_gf == if bit_bit then 0x0001 else 0x0000
+  where bit_gf = (zext (((r@(i/8)) >> (i%8) ) && 1))
+        bit_bit = (join (map reverse r))@i
diff --git a/tests/issues/issue1210.icry b/tests/issues/issue1210.icry
@@ -0,0 +1,6 @@
+:l issue1210.cry
+:check
+:set prover=sbv-z3
+:prove
+:set prover=w4-z3
+:prove
diff --git a/tests/issues/issue1210.icry.stdout b/tests/issues/issue1210.icry.stdout
@@ -0,0 +1,31 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property mwe Using exhaustive testing.
+Testing... Passed 16 tests.
+Q.E.D.
+property mwe' Using exhaustive testing.
+Testing... Passed 8 tests.
+Q.E.D.
+property mwe'' Using exhaustive testing.
+Testing... Passed 1 tests.
+Q.E.D.
+property bitget Using random testing.
+Testing... Passed 100 tests.
+Expected test coverage: 0.00% (100 of 2^^3500 values)
+:prove mwe
+	Q.E.D.
+:prove mwe'
+	Q.E.D.
+:prove mwe''
+	Q.E.D.
+:prove bitget
+	Q.E.D.
+:prove mwe
+	Q.E.D.
+:prove mwe'
+	Q.E.D.
+:prove mwe''
+	Q.E.D.
+:prove bitget
+	Q.E.D.