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

Move the Cryptol implementations of pmod, pdiv and pmult into

Browse Source 
a new `Cryptol::Reference` module. Change the evaluator API slightly
so that primitives can be bound to expressions, in addition to values.
We can use this to inject the reference implementations of the above
operations into the symbolic evaluators.

Because of the exact way evaluation environments are piped around,
the bound expression will be evaluated in the environment that
the primitive symbol is declared.  So, we can't just reference
the name of the reference implementation when we inject it.
Instead, we abuse the `EWhere` construct to add local definitions
corresponding to the entire module.  This works, but is a bit
unsatisfying, as any top-level CAFs will not be shared across
different invocations.  This doesn't matter for these
functions, but might for e.g, AES.
This commit is contained in:
Rob Dockins 2020-10-01 17:03:59 -07:00
parent a41b9be603
commit 5bba75fbb6
9 changed files with 118 additions and 74 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
lib/Cryptol.cry
View File

@ -888,49 +888,17 @@ generate f = [ f i | i <- [0 .. n-1] ]
/**
* Performs multiplication of polynomials over GF(2).
*/
pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
pmult x y = last zs
where
zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]
primitive pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
/**
* Performs division of polynomials over GF(2).
*/
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pdiv x y = [ z ! degree | z <- zs ]
where
degree : [width v]
degree = last (ds : [1 + v]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
reduce : [v] -> [v]
reduce u = if u ! degree then u ^ y else u
zs : [u][v]
zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]
primitive pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
/**
* Performs modulus of polynomials over GF(2).
*/
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
pmod x y = if y == 0 then 0/0 else last zs
where
degree : [width v]
degree = last (ds : [2 + v]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
reduce : [1 + v] -> [1 + v]
reduce u = if u ! degree then u ^ y else u
powers : [inf][1 + v]
powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
primitive fast_pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
primitive fast_pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
primitive fast_pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
primitive pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
// Experimental primitives ------------------------------------------------------------

46
lib/Cryptol/Reference.cry Normal file
View File

@ -0,0 +1,46 @@
module Cryptol::Reference where
/**
* Performs multiplication of polynomials over GF(2).
* Reference implementation.
*/
pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
pmult x y = last zs
where
zs = [0] # [ (z << 1) ^ (if yi then 0 # x else 0) | yi <- y | z <- zs ]
/**
* Performs division of polynomials over GF(2).
* Reference implementation.
*/
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pdiv x y = [ z ! degree | z <- zs ]
where
degree : [width v]
degree = last (ds : [1 + v]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
reduce : [v] -> [v]
reduce u = if u ! degree then u ^ y else u
zs : [u][v]
zs = [ tail (reduce z # [xi]) | z <- [0] # zs | xi <- x ]
/**
* Performs modulus of polynomials over GF(2).
* Reference implementation.
*/
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
pmod x y = if y == 0 then 0/0 else last zs
where
degree : [width v]
degree = last (ds : [2 + v]_)
where ds = [0/0] # [if yi then i else d | yi <- reverse y | i <- [0..v] | d <- ds ]
reduce : [1 + v] -> [1 + v]
reduce u = if u ! degree then u ^ y else u
powers : [inf][1 + v]
powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]

12
src/Cryptol/Eval.hs
View File

@ -63,10 +63,9 @@ import Prelude.Compat
type EvalEnv = GenEvalEnv Concrete
type EvalPrims sym =
( Backend sym, ?evalPrim :: PrimIdent -> Maybe (GenValue sym) )
( Backend sym, ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue sym)) )
type ConcPrims =
?evalPrim :: PrimIdent -> Maybe (GenValue Concrete)
type ConcPrims = ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue Concrete))
-- Expression Evaluation -------------------------------------------------------
@ -158,7 +157,7 @@ evalExpr sym env expr = case expr of
Nothing -> do
envdoc <- ppEnv sym defaultPPOpts env
panic "[Eval] evalExpr"
["var `" ++ show (pp n) ++ "` is not defined"
["var `" ++ show (pp n) ++ "` (" ++ show (nameUnique n) ++ ") is not defined"
, show envdoc
]
@ -526,8 +525,9 @@ evalDecl sym renv env d =
case dDefinition d of
DPrim ->
case ?evalPrim =<< asPrim (dName d) of
Just v -> pure (bindVarDirect (dName d) v env)
Nothing -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env
Just (Right v) -> pure (bindVarDirect (dName d) v env)
Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env
Nothing -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env
DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env

7
src/Cryptol/Eval/Concrete.hs
View File

@ -145,6 +145,7 @@ primTable eOpts = let sym = Concrete in
Map.union (floatPrims sym) $
Map.union suiteBPrims $
Map.union primeECPrims $
Map.fromList $ map (\(n, v) -> (prelPrim n, v))
[ -- Literals
@ -353,7 +354,7 @@ primTable eOpts = let sym = Concrete in
$ if null msg then doc else text msg <+> doc
return yv)
, ("fast_pmult",
, ("pmult",
ilam $ \u ->
ilam $ \v ->
wlam Concrete $ \(BV _ x) -> return $
@ -364,14 +365,14 @@ primTable eOpts = let sym = Concrete in
F2.pmult (fromInteger (v+1)) y x
in return . VWord (1+u+v) . pure . WordVal . mkBv (1+u+v) $! z)
, ("fast_pmod",
, ("pmod",
ilam $ \_u ->
ilam $ \v ->
wlam Concrete $ \(BV w x) -> return $
wlam Concrete $ \(BV _ m) ->
return . VWord v . pure . WordVal . mkBv v $! F2.pmod (fromInteger w) x m)
, ("fast_pdiv",
, ("pdiv",
ilam $ \_u ->
ilam $ \_v ->
wlam Concrete $ \(BV w x) -> return $

15
src/Cryptol/ModuleSystem/Base.hs
View File

@ -42,15 +42,15 @@ import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.PP as T
import qualified Cryptol.TypeCheck.Sanity as TcSanity
import Cryptol.Transform.AddModParams (addModParams)
import Cryptol.Utils.Ident (preludeName, floatName, arrayName, suiteBName, primeECName
, interactiveName, modNameChunks, notParamInstModName
, isParamInstModName )
import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
, preludeReferenceName, interactiveName, modNameChunks
, notParamInstModName, isParamInstModName )
import Cryptol.Utils.PP (pretty)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
import Cryptol.Prelude ( preludeContents, floatContents, arrayContents
, suiteBContents, primeECContents )
, suiteBContents, primeECContents, preludeReferenceContents )
import Cryptol.Transform.MonoValues (rewModule)
import qualified Control.Exception as X
@ -203,7 +203,7 @@ doLoadModule isrc path fp pm0 =
-- extend the eval env, unless a functor.
tbl <- Concrete.primTable <$> getEvalOpts
let ?evalPrim = \i -> Map.lookup i tbl
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)
loadedModule path fp tcm
@ -264,6 +264,7 @@ findModule n = do
| m == arrayName -> pure (InMem "Array" arrayContents)
| m == suiteBName -> pure (InMem "SuiteB" suiteBContents)
| m == primeECName -> pure (InMem "PrimeEC" primeECContents)
| m == preludeReferenceName -> pure (InMem "Cryptol::Reference" preludeReferenceContents)
_ -> moduleNotFound n =<< getSearchPath
-- generate all possible search paths
@ -559,7 +560,7 @@ evalExpr e = do
denv <- getDynEnv
evopts <- getEvalOpts
let tbl = Concrete.primTable evopts
let ?evalPrim = \i -> Map.lookup i tbl
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
io $ E.runEval $ (E.evalExpr Concrete (env <> deEnv denv) e)
evalDecls :: [T.DeclGroup] -> ModuleM ()
@ -569,7 +570,7 @@ evalDecls dgs = do
evOpts <- getEvalOpts
let env' = env <> deEnv denv
let tbl = Concrete.primTable evOpts
let ?evalPrim = \i -> Map.lookup i tbl
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
deEnv' <- io $ E.runEval $ E.evalDecls Concrete dgs env'
let denv' = denv { deDecls = deDecls denv ++ dgs
, deEnv = deEnv'

4
src/Cryptol/Prelude.hs
View File

@ -15,6 +15,7 @@
module Cryptol.Prelude
( preludeContents
, preludeReferenceContents
, floatContents
, arrayContents
, suiteBContents
@ -30,6 +31,9 @@ import Text.Heredoc (there)
preludeContents :: ByteString
preludeContents = B.pack [there|lib/Cryptol.cry|]
preludeReferenceContents :: ByteString
preludeReferenceContents = B.pack [there|lib/Cryptol/Reference.cry|]
floatContents :: ByteString
floatContents = B.pack [there|lib/Float.cry|]

45
src/Cryptol/Symbolic/SBV.hs
View File

@ -27,6 +27,7 @@ module Cryptol.Symbolic.SBV
) where
import Control.Applicative
import Control.Concurrent.Async
import Control.Concurrent.MVar
import Control.Monad.IO.Class
@ -47,6 +48,7 @@ import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Base as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Name as M
import Cryptol.Backend.SBV
import qualified Cryptol.Backend.FloatHelpers as FH
@ -56,12 +58,13 @@ import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Value as Eval
import Cryptol.Eval.SBV
import Cryptol.Symbolic
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (preludeReferenceName, prelPrim, identText)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Logger(logPutStrLn)
import Cryptol.Utils.RecordMap
import Prelude ()
import Prelude.Compat
@ -282,11 +285,17 @@ runProver proverConfig pc@ProverCommand{..} lPutStrLn x =
-- the main goal via a conjunction.
prepareQuery ::
Eval.EvalOpts ->
M.ModuleEnv ->
ProverCommand ->
IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
prepareQuery evo modEnv ProverCommand{..} =
do let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
M.ModuleT IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
prepareQuery evo ProverCommand{..} =
do ds <- do (_mp, m) <- M.loadModuleFrom (M.FromModule preludeReferenceName)
let decls = mDecls m
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (M.genIface m)))
let ds = Map.fromList [ (prelPrim (identText (M.nameIdent nm)), EWhere (EVar nm) decls) | nm <- nms ]
pure ds
modEnv <- M.getModuleEnv
let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
-- The `addAsm` function is used to combine assumptions that
-- arise from the types of symbolic variables (e.g. Z n values
@ -300,7 +309,7 @@ prepareQuery evo modEnv ProverCommand{..} =
case predArgTypes pcQueryType pcSchema of
Left msg -> return (Left msg)
Right ts ->
Right ts -> M.io $
do when pcVerbose $ logPutStrLn (Eval.evalLogger evo) "Simulating..."
pure $ Right $ (ts,
do sbvState <- SBV.symbolicEnv
@ -308,7 +317,8 @@ prepareQuery evo modEnv ProverCommand{..} =
defRelsVar <- liftIO (newMVar SBV.svTrue)
let sym = SBV stateMVar defRelsVar
let tbl = primTable sym
let ?evalPrim = \i -> Map.lookup i tbl
let ?evalPrim = \i -> (Right <$> Map.lookup i tbl) <|>
(Left <$> Map.lookup i ds)
-- Compute the symbolic inputs, and any domain constraints needed
-- according to their types.
args <- map (pure . varShapeToValue sym) <$>
@ -406,7 +416,7 @@ satProve proverCfg pc@ProverCommand {..} =
let lPutStrLn = logPutStrLn (Eval.evalLogger evo)
M.io (prepareQuery evo modEnv pc) >>= \case
prepareQuery evo pc >>= \case
Left msg -> return (Nothing, ProverError msg)
Right (ts, q) ->
do (firstProver, results) <- M.io (runProver proverCfg pc lPutStrLn q)
@ -422,18 +432,15 @@ satProve proverCfg pc@ProverCommand {..} =
satProveOffline :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Either String String)
satProveOffline _proverCfg pc@ProverCommand {..} =
protectStack (\msg (_,_,modEnv) -> return (Right (Left msg, modEnv), [])) $
\(evOpts, _, modEnv) -> do
let isSat = case pcQueryType of
ProveQuery -> False
SafetyQuery -> False
SatQuery _ -> True
prepareQuery evOpts modEnv pc >>= \case
Left msg -> return (Right (Left msg, modEnv), [])
Right (_ts, q) ->
do smtlib <- SBV.generateSMTBenchmark isSat q
return (Right (Right smtlib, modEnv), [])
\(evo, byteReader, modEnv) -> M.runModuleM (evo,byteReader,modEnv) $
do let isSat = case pcQueryType of
ProveQuery -> False
SafetyQuery -> False
SatQuery _ -> True
prepareQuery evo pc >>= \case
Left msg -> return (Left msg)
Right (_ts, q) -> Right <$> M.io (SBV.generateSMTBenchmark isSat q)
protectStack :: (String -> M.ModuleCmd a)
-> M.ModuleCmd a

21
src/Cryptol/Symbolic/What4.hs
View File

@ -29,6 +29,7 @@ module Cryptol.Symbolic.What4
, W4Exception(..)
) where
import Control.Applicative
import Control.Concurrent.Async
import Control.Concurrent.MVar
import Control.Monad.IO.Class
@ -46,6 +47,7 @@ import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Base as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.Backend.FloatHelpers as FH
import Cryptol.Backend.What4
@ -58,6 +60,7 @@ import Cryptol.Eval.What4
import Cryptol.Symbolic
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Logger(logPutStrLn)
import Cryptol.Utils.Ident (preludeReferenceName, prelPrim, identText)
import qualified What4.Config as W4
import qualified What4.Interface as W4
@ -258,12 +261,22 @@ prepareQuery sym ProverCommand { .. } =
simulate args =
do let lPutStrLn = M.withLogger logPutStrLn
when pcVerbose (lPutStrLn "Simulating...")
ds <- do (_mp, m) <- M.loadModuleFrom (M.FromModule preludeReferenceName)
let decls = mDecls m
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (M.genIface m)))
let ds = Map.fromList [ (prelPrim (identText (M.nameIdent nm)), EWhere (EVar nm) decls) | nm <- nms ]
pure ds
let tbl = primTable sym
let ?evalPrim = \i -> (Right <$> Map.lookup i tbl) <|>
(Left <$> Map.lookup i ds)
modEnv <- M.getModuleEnv
let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
doW4Eval (w4 sym)
do let tbl = primTable sym
let ?evalPrim = \i -> Map.lookup i tbl
let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
env <- Eval.evalDecls sym extDgs mempty
do env <- Eval.evalDecls sym extDgs mempty
v <- Eval.evalExpr sym env pcExpr
appliedVal <-
foldM Eval.fromVFun v (map (pure . varShapeToValue sym) args)

4
src/Cryptol/Utils/Ident.hs
View File

@ -16,6 +16,7 @@ module Cryptol.Utils.Ident
, modNameChunks
, packModName
, preludeName
, preludeReferenceName
, floatName
, suiteBName
, arrayName
@ -111,6 +112,9 @@ modInstPref = "`"
preludeName :: ModName
preludeName = packModName ["Cryptol"]
preludeReferenceName :: ModName
preludeReferenceName = packModName ["Cryptol","Reference"]
floatName :: ModName
floatName = packModName ["Float"]