Merge pull request #2174 from GaloisInc/bump-cryptol-1751

Adapt to changes from GaloisInc/cryptol#1751, GaloisInc/cryptol#1526, and friends

.github/workflows/ci.yml

@@ -628,13 +628,13 @@ jobs:
           GH_TOKEN: ${{ github.token }}
 
       - name: Upload pages artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v3
         with:
           path: all-html
 
       - name: Deploy to github pages
         id: deployment
-        uses: actions/deploy-pages@v2
+        uses: actions/deploy-pages@v4
 
   build-push-image:
     runs-on: ubuntu-22.04

cabal.GHC-9.4.8.config

@@ -336,7 +336,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.32,
              simple-sendfile +allow-bsd -fallback,
-             any.simple-smt ==0.9.7,
+             any.simple-smt ==0.9.8,
              any.smallcheck ==1.2.1.1,
              any.split ==0.2.5,
              any.splitmix ==0.1.0.5,
@@ -440,4 +440,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zenc ==0.1.2,
              any.zlib ==0.7.1.0,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-08-02T09:23:27Z
+index-state: hackage.haskell.org 2024-12-30T16:38:21Z

cabal.GHC-9.6.6.config

@@ -334,7 +334,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.32,
              simple-sendfile +allow-bsd -fallback,
-             any.simple-smt ==0.9.7,
+             any.simple-smt ==0.9.8,
              any.smallcheck ==1.2.1.1,
              any.split ==0.2.5,
              any.splitmix ==0.1.0.5,
@@ -438,4 +438,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zenc ==0.1.2,
              any.zlib ==0.7.1.0,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-08-02T09:23:27Z
+index-state: hackage.haskell.org 2024-12-30T16:38:21Z

cabal.GHC-9.8.2.config

@@ -335,7 +335,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.simple-get-opt ==0.4,
              any.simple-sendfile ==0.2.32,
              simple-sendfile +allow-bsd -fallback,
-             any.simple-smt ==0.9.7,
+             any.simple-smt ==0.9.8,
              any.smallcheck ==1.2.1.1,
              any.split ==0.2.5,
              any.splitmix ==0.1.0.5,
@@ -441,4 +441,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zenc ==0.1.2,
              any.zlib ==0.7.1.0,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-08-02T09:23:27Z
+index-state: hackage.haskell.org 2024-12-30T16:38:21Z

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

@@ -1910,7 +1910,7 @@ exportValue ty v = case ty of
     case v of
       SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w)
       SC.VVector xs
-        | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) <$>
+        | TV.isTBit e -> V.VWord <$>
             V.bitmapWordVal V.Concrete (toInteger (Vector.length xs))
                  (V.finiteSeqMap V.Concrete . map (V.ready . SC.toBool . SC.runIdentity . force) $ Fold.toList xs)
         | otherwise   -> pure . V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $
@@ -1977,7 +1977,7 @@ exportFirstOrderValue fv =
     FOVIntMod _ i -> pure (V.VInteger i)
     FOVWord w x   -> V.word V.Concrete (toInteger w) x
     FOVVec t vs
-      | t == FOTBit -> V.VWord len <$> (V.bitmapWordVal V.Concrete len
+      | t == FOTBit -> V.VWord <$> (V.bitmapWordVal V.Concrete len
                           (V.finiteSeqMap V.Concrete . map (V.ready . fvAsBool) $ vs))
       | otherwise   -> pure (V.VSeq len (V.finiteSeqMap V.Concrete (map exportFirstOrderValue vs)))
       where len = toInteger (length vs)
@@ -1994,7 +1994,7 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
   go t v = case (t,v) of
     (FOTBit         , V.VBit b)        -> return (FOVBit b)
     (FOTInt         , V.VInteger i)    -> return (FOVInt i)
-    (FOTVec _ FOTBit, V.VWord w wv)    -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete wv)
+    (FOTVec _ FOTBit, V.VWord wv)      -> FOVWord (fromIntegral (V.wordValWidth wv)) . V.bvVal <$> (V.asWordVal V.Concrete wv)
     (FOTVec _ ty    , V.VSeq len xs)   -> FOVVec ty <$> traverse (go ty =<<) (V.enumerateSeqMap len xs)
     (FOTTuple tys   , V.VTuple xs)     -> FOVTuple <$> traverse (\(ty, x) -> go ty =<< x) (zip tys xs)
     (FOTRec fs      , V.VRecord xs)    ->