Merge pull request #1751 from GaloisInc/issue_1740

Remove bitvectors width from the value tag.

CHANGES.md

@@ -4,6 +4,10 @@
 
 ## Bug fixes
 
+  * Fix #1740, removes duplicated width from word values.
+    Note that since this changes the types, it may require changes to
+    libraries depending on Cryptol.
+
 ## New features
 
 # 3.2.0 -- 2024-08-20

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -566,10 +566,10 @@ readBack ty val =
         _ -> mismatchPanic
     TVSeq len elemTy
       | elemTy == TVBit
-      , VWord width wv <- val -> do
+      , VWord wv <- val -> do
         Concrete.BV w v <- liftEval $ asWordVal Concrete.Concrete wv
         let hexStr = T.pack $ showHex v ""
-        let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1))
+        let paddedLen = fromIntegral ((w `quot` 4) + (if w `rem` 4 == 0 then 0 else 1))
         pure $ Just $  Num Hex (T.justifyRight paddedLen '0' hexStr) w
       | VSeq _l (enumerateSeqMap len -> mVals) <- val -> do
         vals <- liftEval $ sequence mVals

src/Cryptol/Backend.hs

@@ -1,7 +1,9 @@
 {-# Language FlexibleContexts #-}
 {-# Language TypeFamilies #-}
+{-# Language ScopedTypeVariables #-}
 module Cryptol.Backend
   ( Backend(..)
+  , wordLen
   , sDelay
   , invalidIndex
   , cryUserError
@@ -36,6 +38,7 @@ module Cryptol.Backend
 import qualified Control.Exception as X
 import Control.Monad.IO.Class
 import Data.Kind (Type)
+import Data.Proxy(Proxy(..))
 
 import Cryptol.Backend.FloatHelpers (BF)
 import Cryptol.Backend.Monad
@@ -295,7 +298,7 @@ class MonadIO (SEval sym) => Backend sym where
   bitAsLit :: sym -> SBit sym -> Maybe Bool
 
   -- | The number of bits in a word value.
-  wordLen :: sym -> SWord sym -> Integer
+  wordLen' :: proxy sym -> SWord sym -> Integer
 
   -- | Determine if this symbolic word is a literal.
   --   If so, return the bit width and value.
@@ -813,3 +816,7 @@ type FPArith2 sym =
   SFloat sym ->
   SFloat sym ->
   SEval sym (SFloat sym)
+
+wordLen :: forall sym. Backend sym => sym -> SWord sym -> Integer
+wordLen _ x = wordLen' (Proxy :: Proxy sym) x
+{-# INLINE wordLen #-}

src/Cryptol/Backend/Concrete.hs

@@ -144,7 +144,9 @@ instance Backend Concrete where
   assertSideCondition _ True _ = return ()
   assertSideCondition sym False err = raiseError sym err
 
-  wordLen _ (BV w _) = w
+  wordLen' _ (BV w _) = w
+  {-# INLINE wordLen' #-}
+
   wordAsChar _ (BV _ x) = Just $! integerToChar x
 
   wordBit _ (BV w x) idx = pure $! testBit x (fromInteger (w - 1 - idx))

src/Cryptol/Backend/SBV.hs

@@ -201,7 +201,8 @@ instance Backend SBV where
                 SBVResult pz z ->
                   pure $ SBVResult (svAnd (svIte c px py) pz) z
 
-  wordLen _ v = toInteger (intSizeOf v)
+  wordLen' _ v = toInteger (intSizeOf v)
+  {-# INLINE wordLen' #-}
   wordAsChar _ v = integerToChar <$> svAsInteger v
 
   iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y

src/Cryptol/Backend/What4.hs

@@ -273,7 +273,8 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
     | SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv
     | otherwise = Nothing
 
-  wordLen _ bv = SW.bvWidth bv
+  wordLen' _ bv = SW.bvWidth bv
+  {-# INLINE wordLen' #-}
 
   bitLit sym b = W4.backendPred (w4 sym) b
   bitAsLit _ v = W4.asConstantPred v

src/Cryptol/Backend/WordValue.hs

@@ -25,6 +25,7 @@ module Cryptol.Backend.WordValue
   ( -- * WordValue
     WordValue
   , wordVal
+  , wordValWidth
   , bitmapWordVal
   , asWordList
   , asWordVal
@@ -59,6 +60,7 @@ module Cryptol.Backend.WordValue
 
 import Control.Monad (unless)
 import Data.Bits
+import Data.Proxy(Proxy(..))
 import GHC.Generics (Generic)
 
 import Cryptol.Backend
@@ -97,6 +99,14 @@ data WordValue sym
        !(SeqMap sym (SBit sym)) -- ^
  deriving (Generic)
 
+wordValWidth :: forall sym. Backend sym => WordValue sym -> Integer
+wordValWidth val =
+  case val of
+    ThunkWordVal n _ -> n
+    WordVal sv -> wordLen' (Proxy :: Proxy sym) sv
+    BitmapVal n _ _ -> n
+{-# INLINE wordValWidth #-}
+
 wordVal :: SWord sym -> WordValue sym
 wordVal = WordVal
 

src/Cryptol/Eval.hs

@@ -130,7 +130,7 @@ evalExpr sym env expr = case expr of
     -- NB, even if the list cannot be packed, we must use `VWord`
     -- when the element type is `Bit`.
     | isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-}
-        VWord len <$>
+        VWord <$>
           (tryFromBits sym vs >>= \case
              Just w  -> pure (wordVal w)
              Nothing -> do xs <- mapM (\x -> sDelay sym (fromVBit <$> x)) vs
@@ -594,7 +594,7 @@ evalSel sym val sel = case sel of
     case v of
       VSeq _ vs       -> lookupSeqMap vs (toInteger n)
       VStream vs      -> lookupSeqMap vs (toInteger n)
-      VWord _ wv      -> VBit <$> indexWordValue sym wv (toInteger n)
+      VWord wv        -> VBit <$> indexWordValue sym wv (toInteger n)
       _               -> do vdoc <- ppValue sym defaultPPOpts val
                             evalPanic "Cryptol.Eval.evalSel"
                               [ "Unexpected value in list selection"
@@ -643,7 +643,7 @@ evalSetSel sym _tyv e sel v =
     case e of
       VSeq i mp  -> pure $ VSeq i  $ updateSeqMap mp n v
       VStream mp -> pure $ VStream $ updateSeqMap mp n v
-      VWord i m  -> VWord i <$> updateWordValue sym m n asBit
+      VWord m    -> VWord <$> updateWordValue sym m n asBit
       _ -> bad "Sequence update on a non-sequence."
 
   asBit = do res <- v
@@ -781,7 +781,7 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of
         let lenv' = lenv { leVars = fmap stutter (leVars lenv) }
         let vs i = do let (q, r) = i `divMod` nLen
                       lookupSeqMap vss q >>= \case
-                        VWord _ w   -> VBit <$> indexWordValue sym w r
+                        VWord w     -> VBit <$> indexWordValue sym w r
                         VSeq _ xs'  -> lookupSeqMap xs' r
                         VStream xs' -> lookupSeqMap xs' r
                         _           -> evalPanic "evalMatch" ["Not a list value"]
@@ -795,7 +795,7 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of
         let env = EvalEnv (leStatic lenv) (leTypes lenv)
         xs <- evalExpr sym env expr
         let vs i = case xs of
-                     VWord _ w   -> VBit <$> indexWordValue sym w i
+                     VWord w     -> VBit <$> indexWordValue sym w i
                      VSeq _ xs'  -> lookupSeqMap xs' i
                      VStream xs' -> lookupSeqMap xs' i
                      _           -> evalPanic "evalMatch" ["Not a list value"]

src/Cryptol/Eval/Concrete.hs

@@ -134,7 +134,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
       (TVSeq _ b, VSeq n svs) ->
         do ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))
            pure $ EList ses (tValTy b)
-      (TVSeq n TVBit, VWord _ wval) ->
+      (TVSeq n TVBit, VWord wval) ->
         do BV _ v <- lift (asWordVal Concrete wval)
            pure $ ETApp (ETApp (prim "number") (tNum v)) (tWord (tNum n))
 
@@ -206,7 +206,7 @@ primTable getEOpts = let sym = Concrete in
                       F2.pmult (fromInteger (u+1)) x y
                     else
                       F2.pmult (fromInteger (v+1)) y x
-             in return . VWord (1+u+v) . wordVal . mkBv (1+u+v) $! z)
+             in return . VWord . wordVal . mkBv (1+u+v) $! z)
 
    , ("pmod",
         PFinPoly \_u ->
@@ -215,7 +215,7 @@ primTable getEOpts = let sym = Concrete in
         PWordFun \(BV _ m) ->
         PPrim
           do assertSideCondition sym (m /= 0) DivideByZero
-             return . VWord v . wordVal . mkBv v $! F2.pmod (fromInteger w) x m)
+             return . VWord . wordVal . mkBv v $! F2.pmod (fromInteger w) x m)
 
   , ("pdiv",
         PFinPoly \_u ->
@@ -224,7 +224,7 @@ primTable getEOpts = let sym = Concrete in
         PWordFun \(BV _ m) ->
         PPrim
           do assertSideCondition sym (m /= 0) DivideByZero
-             return . VWord w . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m)
+             return . VWord . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m)
   ]
 
 
@@ -297,7 +297,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
               foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))
                     SHA.initialSHA224State blks
            let f :: Word32 -> Eval Value
-               f = pure . VWord 32 . wordVal . BV 32 . toInteger
+               f = pure . VWord . wordVal . BV 32 . toInteger
                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6])
            seq zs (pure (VSeq 7 zs)))
 
@@ -310,7 +310,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
              foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))
                    SHA.initialSHA256State blks
            let f :: Word32 -> Eval Value
-               f = pure . VWord 32 . wordVal . BV 32 . toInteger
+               f = pure . VWord . wordVal . BV 32 . toInteger
                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])
            seq zs (pure (VSeq 8 zs)))
 
@@ -323,7 +323,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))
                    SHA.initialSHA384State blks
            let f :: Word64 -> Eval Value
-               f = pure . VWord 64 . wordVal . BV 64 . toInteger
+               f = pure . VWord . wordVal . BV 64 . toInteger
                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5])
            seq zs (pure (VSeq 6 zs)))
 
@@ -336,7 +336,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))
                    SHA.initialSHA512State blks
            let f :: Word64 -> Eval Value
-               f = pure . VWord 64 . wordVal . BV 64 . toInteger
+               f = pure . VWord . wordVal . BV 64 . toInteger
                zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])
            seq zs (pure (VSeq 8 zs)))
 
@@ -348,7 +348,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
             let toWord :: Integer -> Eval Word32
                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInfKeyExpand" =<< lookupSeqMap ss i)
             let fromWord :: Word32 -> Eval Value
-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger
+                fromWord = pure . VWord . wordVal . BV 32 . toInteger
             kws <- mapM toWord [0 .. k-1]
             let ws = AES.keyExpansionWords k kws
             let len = 4*(k+7)
@@ -361,7 +361,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
             let toWord :: Integer -> Eval Word32
                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInvMixColumns" =<< lookupSeqMap ss i)
             let fromWord :: Word32 -> Eval Value
-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger
+                fromWord = pure . VWord . wordVal . BV 32 . toInteger
             ws <- mapM toWord [0,1,2,3]
             let ws' = AES.invMixColumns ws
             pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')
@@ -373,7 +373,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
             let toWord :: Integer -> Eval Word32
                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncRound" =<< lookupSeqMap ss i)
             let fromWord :: Word32 -> Eval Value
-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger
+                fromWord = pure . VWord . wordVal . BV 32 . toInteger
             ws <- mapM toWord [0,1,2,3]
             let ws' = AES.aesRound ws
             pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')
@@ -385,7 +385,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
             let toWord :: Integer -> Eval Word32
                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncFinalRound" =<< lookupSeqMap ss i)
             let fromWord :: Word32 -> Eval Value
-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger
+                fromWord = pure . VWord . wordVal . BV 32 . toInteger
             ws <- mapM toWord [0,1,2,3]
             let ws' = AES.aesFinalRound ws
             pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')
@@ -397,7 +397,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
             let toWord :: Integer -> Eval Word32
                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecRound" =<< lookupSeqMap ss i)
             let fromWord :: Word32 -> Eval Value
-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger
+                fromWord = pure . VWord . wordVal . BV 32 . toInteger
             ws <- mapM toWord [0,1,2,3]
             let ws' = AES.aesInvRound ws
             pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')
@@ -409,7 +409,7 @@ suiteBPrims = Map.fromList $ map (\(n, v) -> (suiteBPrim n, v))
             let toWord :: Integer -> Eval Word32
                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecFinalRound" =<< lookupSeqMap ss i)
             let fromWord :: Word32 -> Eval Value
-                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger
+                fromWord = pure . VWord . wordVal . BV 32 . toInteger
             ws <- mapM toWord [0,1,2,3]
             let ws' = AES.aesInvFinalRound ws
             pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')