Skip to content

Commit

Permalink
Teach the typechecker a bit more about exponents.
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
robdockins committed Apr 6, 2021
1 parent 523a2dc commit 8915ee3
Show file tree
Hide file tree
Showing 4 changed files with 24 additions and 2 deletions.
6 changes: 4 additions & 2 deletions lib/CryptolTC.z3
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 8 additions & 0 deletions tests/issues/issue734.cry
Original file line number Diff line number Diff line change
@@ -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)
6 changes: 6 additions & 0 deletions tests/issues/issue734.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
:l issue734.cry

f`{3} 0b1010101

asdf1`{8}
asdf2`{8}
6 changes: 6 additions & 0 deletions tests/issues/issue734.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
0x156ad5
0x100
0xff

0 comments on commit 8915ee3

Please sign in to comment.