From 8915ee389973f7fe313eb3e74167f5d853274957 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 5 Apr 2021 13:00:29 -0700
Subject: [PATCH] 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                  | 6 ++++--
 tests/issues/issue734.cry         | 8 ++++++++
 tests/issues/issue734.icry        | 6 ++++++
 tests/issues/issue734.icry.stdout | 6 ++++++
 4 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 tests/issues/issue734.cry
 create mode 100644 tests/issues/issue734.icry
 create mode 100644 tests/issues/issue734.icry.stdout

diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3
index 59741bbe9..7d8736943 100644
--- 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/issue734.cry b/tests/issues/issue734.cry
new file mode 100644
index 000000000..69a506222
--- /dev/null
+++ 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
new file mode 100644
index 000000000..da54efefa
--- /dev/null
+++ 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
new file mode 100644
index 000000000..e47728b24
--- /dev/null
+++ b/tests/issues/issue734.icry.stdout
@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x156ad5
+0x100
+0xff