GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity

More precise rule for k >= width var interval derivation

Browse Source
This commit is contained in:
Trevor Elliott 2017-03-27 16:47:26 -07:00
parent 5a43c1d1fe
commit 576df9fa95
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs
View File

@ -125,18 +125,18 @@ propInterval varInts prop = catMaybes
-- k >= width x -- k >= width x
, do (l,r) <- pIsGeq prop , do (l,r) <- pIsGeq prop
x <- tIsVar =<< pIsWidth r x <- tIsVar =<< pIsWidth r
let int = typeInterval varInts l
-- record the exact upper bound when it produces values within 128 -- record the exact upper bound when it produces values within 128
-- bits -- bits
ub = case iUpper int of let ub = case iIsExact (typeInterval varInts l) of
Just (Nat val) | val < 128 -> Just (Nat (2 ^ val - 1)) Just (Nat val) | val < 128 -> Just (Nat (2 ^ val - 1))
| otherwise -> Nothing | otherwise -> Nothing
_ -> iUpper int upper -> upper
return (x, Interval { iLower = Nat 0, iUpper = ub }) return (x, Interval { iLower = Nat 0, iUpper = ub })
] ]
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
data Interval = Interval data Interval = Interval