Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cryptol-saw-core: SuiteB and ECC prims #1342

Merged
merged 3 commits into from
Jun 16, 2021
Merged

cryptol-saw-core: SuiteB and ECC prims #1342

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c02256e
Add stubs for SuiteB and PrimeEC primitives to `Cryptol.sawcore`.
Jun 16, 2021
5e54096
Support SuiteB and PrimeEC primitives in translator.
Jun 16, 2021
a885cc8
Extend cryptol-saw-core tests to include SuiteB.cry and PrimeEC.cry.
Jun 16, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
83 changes: 83 additions & 0 deletions cryptol-saw-core/saw/Cryptol.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1657,6 +1657,89 @@ ecArrayLookup = arrayLookup;
ecArrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
ecArrayUpdate = arrayUpdate;

--------------------------------------------------------------------------------
-- Suite-B Primitives

AESEncRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
AESEncRound x =
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESEncRound";

AESEncFinalRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
AESEncFinalRound x =
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESEncFinalRound";

AESDecRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
AESDecRound x =
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESDecRound";

AESDecFinalRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
AESDecFinalRound x =
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESDecFinalRound";

AESInvMixColumns : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
AESInvMixColumns x =
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESInvMixColumns";

AESKeyExpand :
(k : Num) ->
seq k (Vec 32 Bool) ->
seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool);
AESKeyExpand k x =
error
(seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool))
"Unimplemented: AESKeyExpand";

processSHA2_224 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 7 (Vec 32 Bool);
processSHA2_224 n x =
error (Vec 7 (Vec 32 Bool)) "Unimplemented: processSHA2_224";

processSHA2_256 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 8 (Vec 32 Bool);
processSHA2_256 n x =
error (Vec 8 (Vec 32 Bool)) "Unimplemented: processSHA2_256";

processSHA2_384 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 6 (Vec 64 Bool);
processSHA2_384 n x =
error (Vec 6 (Vec 64 Bool)) "Unimplemented: processSHA2_384";

processSHA2_512 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 8 (Vec 64 Bool);
processSHA2_512 n x =
error (Vec 8 (Vec 64 Bool)) "Unimplemented: processSHA2_512";

--------------------------------------------------------------------------------
-- Prime-EC Primitives

ec_double :
(p : Num) ->
IntModNum p * IntModNum p * IntModNum p ->
IntModNum p * IntModNum p * IntModNum p;
ec_double p x =
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_double";

ec_add_nonzero :
(p : Num) ->
IntModNum p * IntModNum p * IntModNum p ->
IntModNum p * IntModNum p * IntModNum p ->
IntModNum p * IntModNum p * IntModNum p;
ec_add_nonzero p x y =
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_add_nonzero";

ec_mult :
(p : Num) ->
IntModNum p ->
IntModNum p * IntModNum p * IntModNum p ->
IntModNum p * IntModNum p * IntModNum p;
ec_mult p x y =
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_mult";

ec_twin_mult :
(p : Num) ->
IntModNum p ->
IntModNum p * IntModNum p * IntModNum p ->
IntModNum p * IntModNum p * IntModNum p ->
IntModNum p * IntModNum p * IntModNum p;
ec_twin_mult p x y z =
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_twin_mult";

--------------------------------------------------------------------------------
-- Rewrite rules

Expand Down
33 changes: 31 additions & 2 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,8 @@ import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, single
import qualified Cryptol.ModuleSystem.Name as C
(asPrim, nameUnique, nameIdent, nameInfo, NameInfo(..))
import qualified Cryptol.Utils.Ident as C
( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim
( Ident, PrimIdent(..), mkIdent
, prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim
, ModName, modNameToText, identText, interactiveName
, ModPath(..), modPathSplit
)
Expand Down Expand Up @@ -654,7 +655,7 @@ proveProp sc env prop =

importPrimitive :: SharedContext -> Env -> C.Name -> C.Schema -> IO Term
importPrimitive sc env n sch
| Just nm <- C.asPrim n, Just term <- Map.lookup nm (prelPrims <> arrayPrims <> floatPrims) = term sc
| Just nm <- C.asPrim n, Just term <- Map.lookup nm allPrims = term sc
| Just nm <- C.asPrim n, Just expr <- Map.lookup nm (envRefPrims env) =
do t <- importSchema sc env sch
e <- importExpr sc env expr
Expand All @@ -663,6 +664,9 @@ importPrimitive sc env n sch
| Just nm <- C.asPrim n = panic "Unknown Cryptol primitive name" [show nm]
| otherwise = panic "Improper Cryptol primitive name" [show n]

allPrims :: Map C.PrimIdent (SharedContext -> IO Term)
allPrims = prelPrims <> arrayPrims <> floatPrims <> suiteBPrims <> primeECPrims

prelPrims :: Map C.PrimIdent (SharedContext -> IO Term)
prelPrims =
Map.fromList $
Expand Down Expand Up @@ -817,6 +821,31 @@ floatPrims =
, ("fpSqrt", flip scGlobalDef "Cryptol.fpSqrt")
]

suiteBPrims :: Map C.PrimIdent (SharedContext -> IO Term)
suiteBPrims =
Map.fromList $
first C.suiteBPrim <$>
[ ("AESEncRound", flip scGlobalDef "Cryptol.AESEncRound")
, ("AESEncFinalRound", flip scGlobalDef "Cryptol.AESEncFinalRound")
, ("AESDecRound", flip scGlobalDef "Cryptol.AESDecRound")
, ("AESDecFinalRound", flip scGlobalDef "Cryptol.AESDecFinalRound")
, ("AESInvMixColumns", flip scGlobalDef "Cryptol.AESInvMixColumns")
, ("AESKeyExpand", flip scGlobalDef "Cryptol.AESKeyExpand")
, ("processSHA2_224", flip scGlobalDef "Cryptol.processSHA2_224")
, ("processSHA2_256", flip scGlobalDef "Cryptol.processSHA2_256")
, ("processSHA2_384", flip scGlobalDef "Cryptol.processSHA2_384")
, ("processSHA2_512", flip scGlobalDef "Cryptol.processSHA2_512")
]

primeECPrims :: Map C.PrimIdent (SharedContext -> IO Term)
primeECPrims =
Map.fromList $
first C.primeECPrim <$>
[ ("ec_double", flip scGlobalDef "Cryptol.ec_double")
, ("ec_add_nonzero", flip scGlobalDef "Cryptol.ec_add_nonzero")
, ("ec_mult", flip scGlobalDef "Cryptol.ec_mult")
, ("ec_twin_mult", flip scGlobalDef "Cryptol.ec_twin_mult")
]

-- | Convert a Cryptol expression to a SAW-Core term. Calling
-- 'scTypeOf' on the result of @'importExpr' sc env expr@ must yield a
Expand Down
12 changes: 9 additions & 3 deletions cryptol-saw-core/test/CryptolVerifierTC.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,17 @@ main =
putStrLn "Translated Float.cry!"
cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing CEnv.OnlyPublic Nothing
putStrLn "Translated Array.cry!"
cenv3 <- CEnv.parseDecls sc cenv2 (CEnv.InputText superclassContents "superclass.cry" 1 1)
cenv3 <- CEnv.importModule sc cenv2 (Right N.suiteBName) Nothing CEnv.OnlyPublic Nothing
putStrLn "Translated SuiteB.cry!"
cenv4 <- CEnv.importModule sc cenv3 (Right N.primeECName) Nothing CEnv.OnlyPublic Nothing
putStrLn "Translated PrimeEC.cry!"
cenv5 <- CEnv.importModule sc cenv4 (Right N.preludeReferenceName) Nothing CEnv.OnlyPublic Nothing
putStrLn "Translated Reference.cry!"
cenv6 <- CEnv.parseDecls sc cenv5 (CEnv.InputText superclassContents "superclass.cry" 1 1)
putStrLn "Translated superclass.cry!"
cenv4 <- CEnv.parseDecls sc cenv3 (CEnv.InputText instanceContents "instance.cry" 1 1)
cenv7 <- CEnv.parseDecls sc cenv6 (CEnv.InputText instanceContents "instance.cry" 1 1)
putStrLn "Translated instance.cry!"
mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv4)
mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv7)
putStrLn "Checked all terms!"

checkTranslation :: SharedContext -> (N.Name, Term) -> IO ()
Expand Down