Merge pull request #1149 from GaloisInc/issue734

Teach the typechecker a bit more about exponents
GaloisInc · Apr 6, 2021 · 78a5d0b · 78a5d0b
2 parents 523a2dc + 3258bb1
commit 78a5d0b
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 3 deletions.
diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3
@@ -267,10 +267,12 @@
   ))
 )
 
-
-
 (declare-fun cryExpUnknown (Int Int) Int)
 
+(assert (forall ((x Int) (y Int))
+  (=> (and (> y 0) (> x 0))
+      (>= (cryExpUnknown x y) x))))
+
 (define-fun cryExpTable ((x Int) (y Int)) Int
   (ite (= y 0) 1
   (ite (= y 1) x

diff --git a/tests/issues/issue148.icry b/tests/issues/issue148.icry
@@ -1,2 +1,3 @@
+:set showExamples = no
 :l issue148.cry
 :sat (\(e:[64]) -> (e@@[8..24]) != zero)
diff --git a/tests/issues/issue148.icry.stdout b/tests/issues/issue148.icry.stdout
@@ -2,4 +2,3 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Satisfiable
-(\(e : [64]) -> (e @@ [8 .. 24]) != zero) 0x00feff8000000000 = True
diff --git a/tests/issues/issue734.cry b/tests/issues/issue734.cry
@@ -0,0 +1,8 @@
+f : {a} (fin a) => [2^^a - 1] -> [3*(2^^a - 1)]
+f x = x # x # x
+
+asdf1 : {r} (fin r, width (2^^r)==r+1) => [r+1]
+asdf1 = `(2^^r)
+
+asdf2 : {r} (fin r, width(2^^r-1)==r) => [r]
+asdf2 = `(2^^r-1)
diff --git a/tests/issues/issue734.icry b/tests/issues/issue734.icry
@@ -0,0 +1,6 @@
+:l issue734.cry
+
+f`{3} 0b1010101
+
+asdf1`{8}
+asdf2`{8}
diff --git a/tests/issues/issue734.icry.stdout b/tests/issues/issue734.icry.stdout
@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x156ad5
+0x100
+0xff