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

Merge branch 'master' of github.com:GaloisInc/cryptol

Browse Source
This commit is contained in:
Iavor Diatchki 2017-09-27 10:17:06 -07:00
commit 208119fbbf
17 changed files with 155 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
lib/Cryptol.cry
View File

@ -100,7 +100,7 @@ primitive negate : {a} (Arith a) => a -> a
* Bitwise complement. The prefix notation '~ x'
* is syntactic sugar for 'complement x'.
*/
primitive complement : {a} a -> a
primitive complement : {a} (Logic a) => a -> a
/**
* Less-than. Only works on comparable arguments.
@ -259,35 +259,35 @@ a ==> b = if a then b else True
/**
* Logical `and' over bits. Extends element-wise over sequences, tuples.
*/
primitive (&&) : {a} a -> a -> a
primitive (&&) : {a} (Logic a) => a -> a -> a
/**
* Logical `or' over bits. Extends element-wise over sequences, tuples.
*/
primitive (||) : {a} a -> a -> a
primitive (||) : {a} (Logic a) => a -> a -> a
/**
* Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.
*/
primitive (^) : {a} a -> a -> a
primitive (^) : {a} (Logic a) => a -> a -> a
/**
* Gives an arbitrary shaped value whose bits are all False.
* ~zero likewise gives an arbitrary shaped value whose bits are all True.
*/
primitive zero : {a} a
primitive zero : {a} (Zero a) => a
/**
* Left shift. The first argument is the sequence to shift, the second is the
* number of positions to shift by.
*/
primitive (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
primitive (<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
/**
* Right shift. The first argument is the sequence to shift, the second is the
* number of positions to shift by.
*/
primitive (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
primitive (>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
/**
* Left rotate. The first argument is the sequence to rotate, the second is the

6
lib/Cryptol/Extras.cry
View File

@ -12,7 +12,7 @@ module Cryptol::Extras where
/**
* Logical negation
*/
not : {a} a -> a
not : {a} (Logic a) => a -> a
not a = ~ a
/**
@ -66,7 +66,7 @@ foldr f acc xs = ys ! 0
/**
* Compute the sum of the words in the array.
*/
sum : {a,n} (fin n, Arith a) => [n]a -> a
sum : {a,n} (fin n, Zero a, Arith a) => [n]a -> a
sum xs = foldl (+) zero xs
/**
@ -101,7 +101,7 @@ extendSigned xs = repeat (xs @ 0) # xs
* Repeat a value.
*/
repeat : {n, a} a -> [n]a
repeat x = [ x | _ <- zero ]
repeat x = [ x | _ <- zero : [n] ]
/**
* `elem x xs` Returns true if x is equal to a value in xs.

2
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -495,6 +495,8 @@ instance Rename Prop where
CFin t -> CFin <$> rename t
CEqual l r -> CEqual <$> rename l <*> rename r
CGeq l r -> CGeq <$> rename l <*> rename r
CZero t -> CZero <$> rename t
CLogic t -> CLogic <$> rename t
CArith t -> CArith <$> rename t
CCmp t -> CCmp <$> rename t
CSignedCmp t -> CSignedCmp <$> rename t

6
src/Cryptol/Parser/AST.hs
View File

@ -377,6 +377,8 @@ tconNames = Map.fromList
data Prop n = CFin (Type n) -- ^ @ fin x @
| CEqual (Type n) (Type n) -- ^ @ x == 10 @
| CGeq (Type n) (Type n) -- ^ @ x >= 10 @
| CZero (Type n) -- ^ @ Zero a @
| CLogic (Type n) -- ^ @ Logic a @
| CArith (Type n) -- ^ @ Arith a @
| CCmp (Type n) -- ^ @ Cmp a @
| CSignedCmp (Type n) -- ^ @ SignedCmp a @
@ -836,6 +838,8 @@ instance PPName name => PP (Prop name) where
ppPrec n prop =
case prop of
CFin t -> text "fin" <+> ppPrec 4 t
CZero t -> text "Zero" <+> ppPrec 4 t
CLogic t -> text "Logic" <+> ppPrec 4 t
CArith t -> text "Arith" <+> ppPrec 4 t
CCmp t -> text "Cmp" <+> ppPrec 4 t
CSignedCmp t -> text "SignedCmp" <+> ppPrec 4 t
@ -1000,6 +1004,8 @@ instance NoPos (Prop name) where
CEqual x y -> CEqual (noPos x) (noPos y)
CGeq x y -> CGeq (noPos x) (noPos y)
CFin x -> CFin (noPos x)
CZero x -> CZero (noPos x)
CLogic x -> CLogic (noPos x)
CArith x -> CArith (noPos x)
CCmp x -> CCmp (noPos x)
CSignedCmp x -> CSignedCmp (noPos x)

4
src/Cryptol/Parser/Names.hs
View File

@ -180,6 +180,8 @@ namesC vs prop =
CFin t -> namesT vs t
CEqual t1 t2 -> Set.union (namesT vs t1) (namesT vs t2)
CGeq t1 t2 -> Set.union (namesT vs t1) (namesT vs t2)
CZero t -> namesT vs t
CLogic t -> namesT vs t
CArith t -> namesT vs t
CCmp t -> namesT vs t
CSignedCmp t -> namesT vs t
@ -283,6 +285,8 @@ tnamesC prop =
CFin t -> tnamesT t
CEqual t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CGeq t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CZero t -> tnamesT t
CLogic t -> tnamesT t
CArith t -> tnamesT t
CCmp t -> tnamesT t
CSignedCmp t -> tnamesT t

6
src/Cryptol/Parser/ParserUtils.hs
View File

@ -436,6 +436,8 @@ mkProp ty =
-- these can be translated right away
prefixProp r f xs
| i == zeroIdent, [x] <- xs = return [CLocated (CZero x) r]
| i == logicIdent, [x] <- xs = return [CLocated (CLogic x) r]
| i == arithIdent, [x] <- xs = return [CLocated (CArith x) r]
| i == finIdent, [x] <- xs = return [CLocated (CFin x) r]
| i == cmpIdent, [x] <- xs = return [CLocated (CCmp x) r]
@ -444,7 +446,9 @@ mkProp ty =
where
i = getIdent f
arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
zeroIdent, logicIdent, arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
zeroIdent = mkIdent (S.pack "Zero")
logicIdent = mkIdent (S.pack "Logic")
arithIdent = mkIdent (S.pack "Arith")
finIdent = mkIdent (S.pack "fin")
cmpIdent = mkIdent (S.pack "Cmp")

2
src/Cryptol/TypeCheck/Kind.hs
View File

@ -330,6 +330,8 @@ checkProp prop =
P.CFin t1 -> tcon (PC PFin) [t1] (Just KProp)
P.CEqual t1 t2 -> tcon (PC PEqual) [t1,t2] (Just KProp)
P.CGeq t1 t2 -> tcon (PC PGeq) [t1,t2] (Just KProp)
P.CZero t1 -> tcon (PC PZero) [t1] (Just KProp)
P.CLogic t1 -> tcon (PC PLogic) [t1] (Just KProp)
P.CArith t1 -> tcon (PC PArith) [t1] (Just KProp)
P.CCmp t1 -> tcon (PC PCmp) [t1] (Just KProp)
P.CSignedCmp t1 -> tcon (PC PSignedCmp) [t1] (Just KProp)

5
src/Cryptol/TypeCheck/SimpleSolver.hs
View File

@ -7,7 +7,8 @@ import Cryptol.TypeCheck.Type hiding
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst, solveSignedCmpInst)
import Cryptol.TypeCheck.Solver.Class
(solveZeroInst, solveLogicInst, solveArithInst, solveCmpInst, solveSignedCmpInst)
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
@ -36,6 +37,8 @@ simplifyStep ctxt prop =
TCon (PC PTrue) [] -> SolvedIf []
TCon (PC PAnd) [l,r] -> SolvedIf [l,r]
TCon (PC PZero) [ty] -> solveZeroInst ty
TCon (PC PLogic) [ty] -> solveLogicInst ty
TCon (PC PArith) [ty] -> solveArithInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty

53
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -11,6 +11,8 @@
{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.Solver.Class
( classStep
, solveZeroInst
, solveLogicInst
, solveArithInst
, solveCmpInst
, solveSignedCmpInst
@ -22,13 +24,62 @@ import Cryptol.TypeCheck.Solver.Types
-- | Solve class constraints.
-- If not, then we return 'Nothing'.
-- If solved, ther we return 'Just' a list of sub-goals.
-- If solved, then we return 'Just' a list of sub-goals.
classStep :: Prop -> Solved
classStep p = case tNoUser p of
TCon (PC PLogic) [ty] -> solveLogicInst (tNoUser ty)
TCon (PC PArith) [ty] -> solveArithInst (tNoUser ty)
TCon (PC PCmp) [ty] -> solveCmpInst (tNoUser ty)
_ -> Unsolved
-- | Solve a Zero constraint by instance, if possible.
solveZeroInst :: Type -> Solved
solveZeroInst ty = case tNoUser ty of
-- Zero Error -> fails
TCon (TError _ e) _ -> Unsolvable e
-- Zero Bit
TCon (TC TCBit) [] -> SolvedIf []
-- Zero a => Zero [n]a
TCon (TC TCSeq) [_, a] -> SolvedIf [ pZero a ]
-- Zero b => Zero (a -> b)
TCon (TC TCFun) [_, b] -> SolvedIf [ pZero b ]
-- (Zero a, Zero b) => Zero (a,b)
TCon (TC (TCTuple _)) es -> SolvedIf [ pZero e | e <- es ]
-- (Zero a, Zero b) => Zero { x1 : a, x2 : b }
TRec fs -> SolvedIf [ pZero ety | (_,ety) <- fs ]
_ -> Unsolved
-- | Solve a Logic constraint by instance, if possible.
solveLogicInst :: Type -> Solved
solveLogicInst ty = case tNoUser ty of
-- Logic Error -> fails
TCon (TError _ e) _ -> Unsolvable e
-- Logic Bit
TCon (TC TCBit) [] -> SolvedIf []
-- Logic a => Logic [n]a
TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ]
-- Logic b => Logic (a -> b)
TCon (TC TCFun) [_, b] -> SolvedIf [ pLogic b ]
-- (Logic a, Logic b) => Logic (a,b)
TCon (TC (TCTuple _)) es -> SolvedIf [ pLogic e | e <- es ]
-- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
TRec fs -> SolvedIf [ pLogic ety | (_,ety) <- fs ]
_ -> Unsolved
-- | Solve an Arith constraint by instance, if possible.
solveArithInst :: Type -> Solved
solveArithInst ty = case tNoUser ty of

22
src/Cryptol/TypeCheck/Type.hs
View File

@ -97,6 +97,8 @@ data PC = PEqual -- ^ @_ == _@
-- classes
| PHas Selector -- ^ @Has sel type field@ does not appear in schemas
| PZero -- ^ @Zero _@
| PLogic -- ^ @Logic _@
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
@ -188,6 +190,8 @@ instance HasKind PC where
PGeq -> KNum :-> KNum :-> KProp
PFin -> KNum :-> KProp
PHas _ -> KType :-> KType :-> KProp
PZero -> KType :-> KProp
PLogic -> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
@ -398,6 +402,16 @@ pIsEq ty = case tNoUser ty of
TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsZero :: Prop -> Maybe Type
pIsZero ty = case tNoUser ty of
TCon (PC PZero) [t1] -> Just t1
_ -> Nothing
pIsLogic :: Prop -> Maybe Type
pIsLogic ty = case tNoUser ty of
TCon (PC PLogic) [t1] -> Just t1
_ -> Nothing
pIsArith :: Prop -> Maybe Type
pIsArith ty = case tNoUser ty of
TCon (PC PArith) [t1] -> Just t1
@ -550,6 +564,12 @@ x =#= y = TCon (PC PEqual) [x,y]
(=/=) :: Type -> Type -> Prop
x =/= y = TCon (PC PNeq) [x,y]
pZero :: Type -> Prop
pZero t = TCon (PC PZero) [t]
pLogic :: Type -> Prop
pLogic t = TCon (PC PLogic) [t]
pArith :: Type -> Prop
pArith t = TCon (PC PArith) [t]
@ -789,6 +809,8 @@ instance PP PC where
PGeq -> text "(>=)"
PFin -> text "fin"
PHas sel -> parens (ppSelector sel)
PZero -> text "Zero"
PLogic -> text "Logic"
PArith -> text "Arith"
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"

24
src/Cryptol/TypeCheck/TypeOf.hs
View File

@ -65,10 +65,19 @@ fastSchemaOf tyenv expr =
ETAbs tparam e -> case fastSchemaOf tyenv e of
Forall tparams props ty -> Forall (tparam : tparams) props ty
ETApp e t -> case fastSchemaOf tyenv e of
Forall (tparam : tparams) props ty -> Forall tparams (apSubst s props) (apSubst s ty)
where s = singleSubst (tpVar tparam) t
Forall (tparam : tparams) props ty
-> Forall tparams (map (plainSubst s) props) (apSubst s ty)
where s = singleSubst (tpVar tparam) t
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
[ "ETApp body with no type parameters" ]
-- When calling 'fastSchemaOf' on a
-- polymorphic function with instantiated type
-- variables but undischarged type
-- constraints, we would prefer to see the
-- instantiated constraints in an
-- un-simplified form. Thus we use
-- 'plainSubst' instead of 'apSubst' on the
-- type constraints.
EProofAbs p e -> case fastSchemaOf tyenv e of
Forall [] props ty -> Forall [] (p : props) ty
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
@ -95,6 +104,17 @@ fastSchemaOf tyenv expr =
where
monomorphic = Forall [] [] (fastTypeOf tyenv expr)
-- | Apply a substitution to a type *without* simplifying
-- constraints like @Arith [n]a@ to @Arith a@. (This is in contrast to
-- 'apSubst', which performs simplifications wherever possible.)
plainSubst :: Subst -> Type -> Type
plainSubst s ty =
case ty of
TCon tc ts -> TCon tc (map (plainSubst s) ts)
TUser f ts t -> TUser f (map (plainSubst s) ts) (plainSubst s t)
TRec fs -> TRec [ (x, plainSubst s t) | (x, t) <- fs ]
TVar x -> apSubst s (TVar x)
-- | Yields the return type of the selector on the given argument type.
typeSelect :: Type -> Selector -> Type
typeSelect (TUser _ _ ty) sel = typeSelect ty sel

2
tests/issues/issue086.icry.stdout
View File

@ -1,2 +1,2 @@
Loading module Cryptol
(&&) : {a} a -> a -> a
(&&) : {a} (Logic a) => a -> a -> a

14
tests/issues/issue226.icry.stdout
View File

@ -20,7 +20,7 @@ Symbols
a} (fin front) => [front]a -> [back]a -> [front + back]a
(%) : {a} (Arith a) => a -> a -> a
(%$) : {a} (Arith a) => a -> a -> a
(&&) : {a} a -> a -> a
(&&) : {a} (Logic a) => a -> a -> a
(*) : {a} (Arith a) => a -> a -> a
(+) : {a} (Arith a) => a -> a -> a
(-) : {a} (Arith a) => a -> a -> a
@ -29,7 +29,7 @@ Symbols
(/\) : Bit -> Bit -> Bit
(<) : {a} (Cmp a) => a -> a -> Bit
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
(<<) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
(<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(<=) : {a} (Cmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
@ -40,7 +40,7 @@ Symbols
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
(>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
(>>) : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
(>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
(>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(@) : {a, b, c} (fin c) => [a]b -> [c] -> b
@ -48,10 +48,10 @@ Symbols
False : Bit
True : Bit
(\/) : Bit -> Bit -> Bit
(^) : {a} a -> a -> a
(^) : {a} (Logic a) => a -> a -> a
(^^) : {a} (Arith a) => a -> a -> a
carry : {n} (fin n) => [n] -> [n] -> Bit
complement : {a} a -> a
complement : {a} (Logic a) => a -> a
demote : {val, bits} (fin val, fin bits,
bits >= width val) => [bits]
drop : {front, back, elem} (fin front) => [front +
@ -106,7 +106,7 @@ Symbols
fin d) => [a]b -> [d][c] -> [d]b -> [a]b
width : {bits, len, elem} (fin len, fin bits,
bits >= width len) => [len]elem -> [bits]
zero : {a} a
zero : {a} (Zero a) => a
zext : {n, m} (fin m, m >= n) => [n] -> [m]
(||) : {a} a -> a -> a
(||) : {a} (Logic a) => a -> a -> a

8
tests/issues/issue410.icry.stdout
View File

@ -1,6 +1,8 @@
Loading module Cryptol
{a, b} a == min (1 + a) a
{a, b} True
{a, b} (Logic b) => a == min (1 + a) a
{a, b} (Logic b) => Logic b
{a, b} (Logic b) => Logic b
{a, b} (Logic b) => True
(s
where
s x =
@ -9,7 +11,7 @@ Loading module Cryptol
bs = [complement b | b <- [complement x] # bs
| _ <- bs]
)
) : {a, b} b -> [a]b
) : {a, b} (Logic b) => b -> [a]b
{a, b} a == a
(bs
where

12
tests/mono-binds/test05.icry.stdout
View File

@ -14,8 +14,8 @@ test05::foo : [10]
test05::foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */
test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
Cryptol::demote 10 c <> <> <>
where
/* Not recursive */
@ -34,7 +34,7 @@ test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
/* Not recursive */
test05::bar : {e} (fin e) => [e + a]b
test05::bar = \{e} (fin e) ->
(Cryptol::#) e a b <> (Cryptol::zero ([e]b)) test05::foo
(Cryptol::#) e a b <> (Cryptol::zero ([e]b) <>) test05::foo
@ -60,8 +60,8 @@ test05::foo : [10]
test05::foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */
test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
Cryptol::demote 10 c <> <> <>
where
/* Not recursive */
@ -78,7 +78,7 @@ test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
/* Not recursive */
test05::bar : [a]b
test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b)) test05::foo
test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b) <>) test05::foo

2
tests/mono-binds/test06.cry
View File

@ -1,6 +1,6 @@
module test06 where
test : {a} a -> a
test : {a} (Zero a) => a -> a
test a = bar
where
foo : a

12
tests/mono-binds/test06.icry.stdout
View File

@ -4,13 +4,13 @@ Loading module test06
module test06
import Cryptol
/* Not recursive */
test06::test : {a} a -> a
test06::test = \{a} (a : a) ->
test06::test : {a} (Zero a) => a -> a
test06::test = \{a} (Zero a) (a : a) ->
test06::bar
where
/* Not recursive */
test06::foo : a
test06::foo = Cryptol::zero a
test06::foo = Cryptol::zero a <>
/* Not recursive */
test06::bar : a
@ -23,13 +23,13 @@ Loading module test06
module test06
import Cryptol
/* Not recursive */
test06::test : {a} a -> a
test06::test = \{a} (a : a) ->
test06::test : {a} (Zero a) => a -> a
test06::test = \{a} (Zero a) (a : a) ->
test06::bar
where
/* Not recursive */
test06::foo : a
test06::foo = Cryptol::zero a
test06::foo = Cryptol::zero a <>
/* Not recursive */
test06::bar : a