From 647efc8f8e960fe5e73f05307b62f8b3447709f0 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 9 Jan 2025 12:42:07 -0500 Subject: [PATCH 1/3] CI: Use latest versions of upload-pages-artifact and deploy-pages --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 44bb6f42c..7a8b65f41 100644 --- a/.github/workflows/ci.yml +++ b/.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 From efce7b3ca7e3a15512b323f38cafabb3d6c7df6a Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 7 Jan 2025 10:37:25 -0600 Subject: [PATCH 2/3] Adapt `cryptol-saw-core` to changes from GaloisInc/cryptol#1751 GaloisInc/cryptol#1751 removed the width field from word values, which requires mechanical changes on the `cryptol-saw-core` side to make it build. This bumps the `cryptol` submodule and makes the corresponding code changes. --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 6 +++--- deps/cryptol | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 476478193..a8e32683d 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/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) -> diff --git a/deps/cryptol b/deps/cryptol index 098532511..b1bdfd0e3 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 09853251186d4590f3b093dbdf2b324c9a7e6ca0 +Subproject commit b1bdfd0e3ff0ff8d16e94fd6e6402a3d1fb497f2 From 68a404cc477d63aaab0f4d3a21844966ee4aec18 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 21 Jan 2025 07:16:54 -0500 Subject: [PATCH 3/3] Adapt cryptol-saw-core to changes from GaloisInc/cryptol#1526, GaloisInc/cryptol#1783, and GaloisInc/cryptol#1791 This is a collection of `cryptol` submodule bumps that is squashed together in order to ensure that the SAW CI continues to pass with this commit: * GaloisInc/cryptol#1783 bumps Cryptol's lower version bounds on `simple-smt` to `>=0.9.8`, which requires updating SAW's `cabal.GHC-*.config` files accordingly. * GaloisInc/cryptol#1526 is brought along for the ride as part of this bump, but this will not pass SAW's integration tests without also including the bugfix from GaloisInc/cryptol#1791. As a result, I've also included GaloisInc/cryptol#1791. GaloisInc/cryptol#1791 is latest of the three patchsets, so I have bumped the `cryptol` submodule to point to the merge commit from that PR. --- cabal.GHC-9.4.8.config | 4 ++-- cabal.GHC-9.6.6.config | 4 ++-- cabal.GHC-9.8.2.config | 4 ++-- deps/cryptol | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/cabal.GHC-9.4.8.config b/cabal.GHC-9.4.8.config index 7dd73aae6..24a96c3bc 100644 --- a/cabal.GHC-9.4.8.config +++ b/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 diff --git a/cabal.GHC-9.6.6.config b/cabal.GHC-9.6.6.config index a65c456fd..b0c0cfc98 100644 --- a/cabal.GHC-9.6.6.config +++ b/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 diff --git a/cabal.GHC-9.8.2.config b/cabal.GHC-9.8.2.config index 8cf73ddd2..5b86d9139 100644 --- a/cabal.GHC-9.8.2.config +++ b/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 diff --git a/deps/cryptol b/deps/cryptol index b1bdfd0e3..d108257f7 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit b1bdfd0e3ff0ff8d16e94fd6e6402a3d1fb497f2 +Subproject commit d108257f705e35315186c5ed911d2a21f2099ffa