diff --git a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex index 63ee8b8d..ac396718 100644 --- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex +++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex @@ -55,7 +55,12 @@ expression \texttt{sqDiff1 (x, y) == sqDiff2 (x, y)} evaluates to \texttt{True}. Furthermore, the type signature restricts the type of the property to apply to only 8-bit values. As usual, the type signature is optional.\indSignature If not given, Cryptol will infer -one for you. +one for you. Finally, note that the same property can also be +expressed (more concisely) using the \texttt{===} operator: +\begin{code} + sqDiffsCorrect : ([8], [8]) -> Bit + property sqDiffsCorrect = sqDiff1 === sqDiff2 +\end{code} \note{It is important to emphasize that the mathematical equality above and the Cryptol property are \emph{not} stating precisely the diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 893ee281..ee55ad9c 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -1052,7 +1052,7 @@ wordValLogicOp :: BitWord b w i -> Eval (WordValue b w i) wordValLogicOp _ wop (WordVal w1) (WordVal w2) = return $ WordVal (wop w1 w2) wordValLogicOp bop _ (BitsVal xs) (BitsVal ys) = - ready $ BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) xs ys + BitsVal <$> sequence (Seq.zipWith (\x y -> delay Nothing (bop <$> x <*> y)) xs ys) wordValLogicOp bop _ (WordVal w1) (BitsVal ys) = ready $ BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) (Seq.fromList $ map ready $ unpackWord w1) ys wordValLogicOp bop _ (BitsVal xs) (WordVal w2) =