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

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

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) =