Skip to content

Commit d2916f8

Browse files
mergify[bot]mergify[bot]
authored
Merge pull request #1342 from GaloisInc/suiteb-ecc-prims
cryptol-saw-core: SuiteB and ECC prims
2 parents 4254dd0 + a885cc8 commit d2916f8

File tree

3 files changed

+123
-5
lines changed

3 files changed

+123
-5
lines changed

‎cryptol-saw-core/saw/Cryptol.sawcore

+83
Original file line numberDiff line numberDiff line change
@@ -1657,6 +1657,89 @@ ecArrayLookup = arrayLookup;
16571657
ecArrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
16581658
ecArrayUpdate = arrayUpdate;
16591659

1660+
--------------------------------------------------------------------------------
1661+
-- Suite-B Primitives
1662+
1663+
AESEncRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
1664+
AESEncRound x =
1665+
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESEncRound";
1666+
1667+
AESEncFinalRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
1668+
AESEncFinalRound x =
1669+
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESEncFinalRound";
1670+
1671+
AESDecRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
1672+
AESDecRound x =
1673+
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESDecRound";
1674+
1675+
AESDecFinalRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
1676+
AESDecFinalRound x =
1677+
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESDecFinalRound";
1678+
1679+
AESInvMixColumns : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
1680+
AESInvMixColumns x =
1681+
error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESInvMixColumns";
1682+
1683+
AESKeyExpand :
1684+
(k : Num) ->
1685+
seq k (Vec 32 Bool) ->
1686+
seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool);
1687+
AESKeyExpand k x =
1688+
error
1689+
(seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool))
1690+
"Unimplemented: AESKeyExpand";
1691+
1692+
processSHA2_224 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 7 (Vec 32 Bool);
1693+
processSHA2_224 n x =
1694+
error (Vec 7 (Vec 32 Bool)) "Unimplemented: processSHA2_224";
1695+
1696+
processSHA2_256 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 8 (Vec 32 Bool);
1697+
processSHA2_256 n x =
1698+
error (Vec 8 (Vec 32 Bool)) "Unimplemented: processSHA2_256";
1699+
1700+
processSHA2_384 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 6 (Vec 64 Bool);
1701+
processSHA2_384 n x =
1702+
error (Vec 6 (Vec 64 Bool)) "Unimplemented: processSHA2_384";
1703+
1704+
processSHA2_512 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 8 (Vec 64 Bool);
1705+
processSHA2_512 n x =
1706+
error (Vec 8 (Vec 64 Bool)) "Unimplemented: processSHA2_512";
1707+
1708+
--------------------------------------------------------------------------------
1709+
-- Prime-EC Primitives
1710+
1711+
ec_double :
1712+
(p : Num) ->
1713+
IntModNum p * IntModNum p * IntModNum p ->
1714+
IntModNum p * IntModNum p * IntModNum p;
1715+
ec_double p x =
1716+
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_double";
1717+
1718+
ec_add_nonzero :
1719+
(p : Num) ->
1720+
IntModNum p * IntModNum p * IntModNum p ->
1721+
IntModNum p * IntModNum p * IntModNum p ->
1722+
IntModNum p * IntModNum p * IntModNum p;
1723+
ec_add_nonzero p x y =
1724+
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_add_nonzero";
1725+
1726+
ec_mult :
1727+
(p : Num) ->
1728+
IntModNum p ->
1729+
IntModNum p * IntModNum p * IntModNum p ->
1730+
IntModNum p * IntModNum p * IntModNum p;
1731+
ec_mult p x y =
1732+
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_mult";
1733+
1734+
ec_twin_mult :
1735+
(p : Num) ->
1736+
IntModNum p ->
1737+
IntModNum p * IntModNum p * IntModNum p ->
1738+
IntModNum p * IntModNum p * IntModNum p ->
1739+
IntModNum p * IntModNum p * IntModNum p;
1740+
ec_twin_mult p x y z =
1741+
error (IntModNum p * IntModNum p * IntModNum p) "Unimplemented: ec_twin_mult";
1742+
16601743
--------------------------------------------------------------------------------
16611744
-- Rewrite rules
16621745

‎cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

+31-2
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,8 @@ import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, single
4545
import qualified Cryptol.ModuleSystem.Name as C
4646
(asPrim, nameUnique, nameIdent, nameInfo, NameInfo(..))
4747
import qualified Cryptol.Utils.Ident as C
48-
( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim
48+
( Ident, PrimIdent(..), mkIdent
49+
, prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim
4950
, ModName, modNameToText, identText, interactiveName
5051
, ModPath(..), modPathSplit
5152
)
@@ -654,7 +655,7 @@ proveProp sc env prop =
654655

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

667+
allPrims :: Map C.PrimIdent (SharedContext -> IO Term)
668+
allPrims = prelPrims <> arrayPrims <> floatPrims <> suiteBPrims <> primeECPrims
669+
666670
prelPrims :: Map C.PrimIdent (SharedContext -> IO Term)
667671
prelPrims =
668672
Map.fromList $
@@ -817,6 +821,31 @@ floatPrims =
817821
, ("fpSqrt", flip scGlobalDef "Cryptol.fpSqrt")
818822
]
819823

824+
suiteBPrims :: Map C.PrimIdent (SharedContext -> IO Term)
825+
suiteBPrims =
826+
Map.fromList $
827+
first C.suiteBPrim <$>
828+
[ ("AESEncRound", flip scGlobalDef "Cryptol.AESEncRound")
829+
, ("AESEncFinalRound", flip scGlobalDef "Cryptol.AESEncFinalRound")
830+
, ("AESDecRound", flip scGlobalDef "Cryptol.AESDecRound")
831+
, ("AESDecFinalRound", flip scGlobalDef "Cryptol.AESDecFinalRound")
832+
, ("AESInvMixColumns", flip scGlobalDef "Cryptol.AESInvMixColumns")
833+
, ("AESKeyExpand", flip scGlobalDef "Cryptol.AESKeyExpand")
834+
, ("processSHA2_224", flip scGlobalDef "Cryptol.processSHA2_224")
835+
, ("processSHA2_256", flip scGlobalDef "Cryptol.processSHA2_256")
836+
, ("processSHA2_384", flip scGlobalDef "Cryptol.processSHA2_384")
837+
, ("processSHA2_512", flip scGlobalDef "Cryptol.processSHA2_512")
838+
]
839+
840+
primeECPrims :: Map C.PrimIdent (SharedContext -> IO Term)
841+
primeECPrims =
842+
Map.fromList $
843+
first C.primeECPrim <$>
844+
[ ("ec_double", flip scGlobalDef "Cryptol.ec_double")
845+
, ("ec_add_nonzero", flip scGlobalDef "Cryptol.ec_add_nonzero")
846+
, ("ec_mult", flip scGlobalDef "Cryptol.ec_mult")
847+
, ("ec_twin_mult", flip scGlobalDef "Cryptol.ec_twin_mult")
848+
]
820849

821850
-- | Convert a Cryptol expression to a SAW-Core term. Calling
822851
-- 'scTypeOf' on the result of @'importExpr' sc env expr@ must yield a

‎cryptol-saw-core/test/CryptolVerifierTC.hs

+9-3
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,17 @@ main =
3131
putStrLn "Translated Float.cry!"
3232
cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing CEnv.OnlyPublic Nothing
3333
putStrLn "Translated Array.cry!"
34-
cenv3 <- CEnv.parseDecls sc cenv2 (CEnv.InputText superclassContents "superclass.cry" 1 1)
34+
cenv3 <- CEnv.importModule sc cenv2 (Right N.suiteBName) Nothing CEnv.OnlyPublic Nothing
35+
putStrLn "Translated SuiteB.cry!"
36+
cenv4 <- CEnv.importModule sc cenv3 (Right N.primeECName) Nothing CEnv.OnlyPublic Nothing
37+
putStrLn "Translated PrimeEC.cry!"
38+
cenv5 <- CEnv.importModule sc cenv4 (Right N.preludeReferenceName) Nothing CEnv.OnlyPublic Nothing
39+
putStrLn "Translated Reference.cry!"
40+
cenv6 <- CEnv.parseDecls sc cenv5 (CEnv.InputText superclassContents "superclass.cry" 1 1)
3541
putStrLn "Translated superclass.cry!"
36-
cenv4 <- CEnv.parseDecls sc cenv3 (CEnv.InputText instanceContents "instance.cry" 1 1)
42+
cenv7 <- CEnv.parseDecls sc cenv6 (CEnv.InputText instanceContents "instance.cry" 1 1)
3743
putStrLn "Translated instance.cry!"
38-
mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv4)
44+
mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv7)
3945
putStrLn "Checked all terms!"
4046

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

0 commit comments

Comments
 (0)