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

Add a variant of the demote primitive for type Z n.

Browse Source 
intmod : {val, mn} (fin val, n >= val + 1) => Z n
This commit is contained in:
Brian Huffman 2018-06-14 06:17:51 -07:00
parent daac41fdec
commit 5ac32d1ad5
3 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/Cryptol.cry
View File

@ -15,6 +15,11 @@ primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
*/
primitive integer : {val} (fin val) => Integer
/**
* The integer (mod n) value corresponding to a numeric type.
*/
primitive intmod : {val, modulus} (fin val, modulus >= val + 1) => Z modulus
infixr 5 ==>
infixr 10 \/
infixr 15 /\

13
src/Cryptol/Prims/Eval.hs
View File

@ -132,6 +132,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
ecDemoteV)
, ("integer" , {-# SCC "Prelude::integer" #-}
ecIntegerV)
, ("intmod" , {-# SCC "Prelude::intmod" #-}
ecIntModV)
, ("#" , {-# SCC "Prelude::(#)" #-}
nlam $ \ front ->
@ -240,6 +242,17 @@ ecIntegerV = nlam $ \valT ->
, show valT
]
-- | Make an integer (mod n) constant. We assume that valT < modT.
ecIntModV :: BitWord b w i => GenValue b w i
ecIntModV = nlam $ \valT ->
nlam $ \_modT ->
case valT of
Nat v -> VInteger (integerLit v)
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
[ "Unexpected Inf in constant."
, show valT
]
-- | Convert a word to a non-negative integer.
ecToIntegerV :: BitWord b w i => GenValue b w i
ecToIntegerV =

2
src/Cryptol/Symbolic/Prims.hs
View File

@ -39,6 +39,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
transposeV, indexPrim,
ecIntegerV, ecToIntegerV, ecFromIntegerV,
ecDemoteV, updatePrim, randomV, liftWord,
ecIntModV,
cmpValue, lg2)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Decl(..))
@ -81,6 +82,7 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
-- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
, ("integer" , ecIntegerV) -- Converts a numeric type into its corresponding value.
-- { val } (fin val) => Integer
, ("intmod" , ecIntModV) -- {val, n} (fin val, n >= val + 1) => Z n
, ("+" , binary (arithBinary (liftBinArith SBV.svPlus) (liftBin SBV.svPlus)
(const (liftBin SBV.svPlus)))) -- {a} (Arith a) => a -> a -> a
, ("-" , binary (arithBinary (liftBinArith SBV.svMinus) (liftBin SBV.svMinus)