Teach the typechecker a bit more about exponents.

This fixes issue #734, and partially addresses #930.
The basic issue with 734 was that the solver was chosing
spurious counterexamples for the exponent function; in particular,
models where the output was not at least 1.  The fairly restricted
axiom we add here just says that the exponent function is at least
as large as its base for positive inputs.

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

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)

tests/issues/issue734.icry

@@ -0,0 +1,6 @@
+:l issue734.cry
+
+f`{3} 0b1010101
+
+asdf1`{8}
+asdf2`{8}

tests/issues/issue734.icry.stdout

@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x156ad5
+0x100
+0xff