Failure to compile copilot-verifier with GHC 9.10

[ivanperez-keera]

I'm testing Copilot with different versions of GHC. There's been new releases of crucible/crux related packages, but they are failing to compile atm.

This is what I'm trying:

FROM ubuntu:jammy

WORKDIR /root
SHELL ["/bin/bash", "-c"]

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config \
      z3

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

RUN ghcup install ghc 9.10
RUN ghcup install cabal 3.16
RUN ghcup set ghc 9.10.3
RUN cabal update

ARG GIT_COMMIT=HEAD
ARG NAME=copilot
ARG REPO=https://github.com/copilot-language/copilot

RUN git clone ${REPO} ${NAME}
RUN cd ${NAME} && git checkout ${GIT_COMMIT}

WORKDIR ${NAME}

RUN echo "  copilot-verifier/copilot-verifier.cabal" >> cabal.project
RUN echo "  copilot-visualizer/copilot-visualizer.cabal" >> cabal.project
RUN cabal install \
         --package-env . \
         --lib \
         --constraint="copilot==4.8.1" \
         --constraint="copilot-bluespec==4.8.1" \
         --constraint="copilot-c99==4.8.1" \
         --constraint="copilot-core==4.8.1" \
         --constraint="copilot-prettyprinter==4.8.1" \
         --constraint="copilot-interpreter==4.8.1" \
         --constraint="copilot-language==4.8.1" \
         --constraint="copilot-libraries==4.8.1" \
         --constraint="copilot-theorem==4.8.1" \
         --constraint="copilot-verifier==4.8.1" \
         --constraint="copilot-visualizer==4.8.1" \
         copilot**/
RUN echo "Success"

Build with:

docker build --build-arg "REPO=https://github.com/ivanperez-keera/copilot" --build-arg "NAME=copilot" --build-arg "GIT_COMMIT=cb0183a83d80ad8502b34ba491f84162846fcc98" -t copilot-verify-ghc-9.10 -f Dockerfile-verify-ghc-9.10 .

Branch: develop-ghc-9.10

Error log (last lines):

#20 1215.7 Starting     crucible-0.9 (lib)
#20 1216.8 Building     copilot-theorem-4.8.1 (lib)
#20 1216.8 Building     crucible-0.9 (lib)
#20 1235.5 Installing   copilot-theorem-4.8.1 (lib)
#20 1236.3 Completed    copilot-theorem-4.8.1 (lib)
#20 1236.3 Starting     copilot-language-4.8.1 (lib)
#20 1237.4 Building     copilot-language-4.8.1 (lib)
#20 1242.1 Installing   copilot-language-4.8.1 (lib)
#20 1243.1 Completed    copilot-language-4.8.1 (lib)
#20 1243.1 Starting     copilot-libraries-4.8.1 (lib)
#20 1244.4 Building     copilot-libraries-4.8.1 (lib)
#20 1250.3 Installing   copilot-libraries-4.8.1 (lib)
#20 1251.4 Completed    copilot-libraries-4.8.1 (lib)
#20 1251.4 Starting     copilot-4.8.1 (lib)
#20 1252.6 Building     copilot-4.8.1 (lib)
#20 1254.2 Installing   copilot-4.8.1 (lib)
#20 1255.1 Completed    copilot-4.8.1 (lib)
#20 1255.1 Starting     copilot-visualizer-4.8.1 (lib)
#20 1256.4 Building     copilot-visualizer-4.8.1 (lib)
#20 1262.5 Installing   copilot-visualizer-4.8.1 (lib)
#20 1263.4 Completed    copilot-visualizer-4.8.1 (lib)
#20 1290.2 Installing   crucible-0.9 (lib)
#20 1291.0 Completed    crucible-0.9 (lib)
#20 1291.1 Starting     crucible-syntax-0.5.0.0 (lib)
#20 1291.1 Starting     crucible-symio-0.2.0.0 (lib)
#20 1291.1 Starting     crux-0.7.1 (lib)
#20 1292.5 Building     crucible-syntax-0.5.0.0 (lib)
#20 1292.5 Building     crucible-symio-0.2.0.0 (lib)
#20 1292.6 Building     crux-0.7.1 (lib)
#20 1303.9 Installing   crucible-symio-0.2.0.0 (lib)
#20 1305.4 Completed    crucible-symio-0.2.0.0 (lib)
#20 1305.5 Starting     crucible-llvm-0.9 (lib)
#20 1307.5 Building     crucible-llvm-0.9 (lib)
#20 1322.6 Installing   crux-0.7.1 (lib)
#20 1324.1 Completed    crux-0.7.1 (lib)
#20 1333.6 Installing   crucible-syntax-0.5.0.0 (lib)
#20 1334.5 Completed    crucible-syntax-0.5.0.0 (lib)
#20 1334.5 Starting     crucible-debug-0.1.2.0 (lib)
#20 1336.0 Building     crucible-debug-0.1.2.0 (lib)
#20 1349.8 Installing   crucible-debug-0.1.2.0 (lib)
#20 1350.9 Completed    crucible-debug-0.1.2.0 (lib)
#20 1408.9 Installing   crucible-llvm-0.9 (lib)
#20 1409.8 Completed    crucible-llvm-0.9 (lib)
#20 1409.9 Starting     crux-llvm-0.12 (lib)
#20 1410.9 Building     crux-llvm-0.12 (lib)
#20 1416.6 
#20 1416.6 Failed to build crux-llvm-0.12.
#20 1416.6 Build log (
#20 1416.6 /root/.cache/cabal/logs/ghc-9.10.3/crux-llvm-0.12-5c9103e728c677f5b252727f48b7b88774e682d9212acca7c8075cf27d4b1442.log
#20 1416.6 ):
#20 1416.6 Configuring library for crux-llvm-0.12...
#20 1416.6 Preprocessing library for crux-llvm-0.12...
#20 1416.6 Building library for crux-llvm-0.12...
#20 1416.6 [1 of 7] Compiling Crux.LLVM.Log    ( src/Crux/LLVM/Log.hs, dist/build/Crux/LLVM/Log.o, dist/build/Crux/LLVM/Log.dyn_o )
#20 1416.6 [2 of 7] Compiling Crux.LLVM.Overrides ( src/Crux/LLVM/Overrides.hs, dist/build/Crux/LLVM/Overrides.o, dist/build/Crux/LLVM/Overrides.dyn_o )
#20 1416.6 [3 of 7] Compiling Paths_crux_llvm  ( dist/build/autogen/Paths_crux_llvm.hs, dist/build/Paths_crux_llvm.o, dist/build/Paths_crux_llvm.dyn_o )
#20 1416.6 [4 of 7] Compiling Crux.LLVM.Config ( src/Crux/LLVM/Config.hs, dist/build/Crux/LLVM/Config.o, dist/build/Crux/LLVM/Config.dyn_o )
#20 1416.6 [5 of 7] Compiling Crux.LLVM.Simulate ( src/Crux/LLVM/Simulate.hs, dist/build/Crux/LLVM/Simulate.o, dist/build/Crux/LLVM/Simulate.dyn_o )
#20 1416.6 src/Crux/LLVM/Simulate.hs:194:3: error: [GHC-83865]
#20 1416.6     * Expected kind `* -> *',
#20 1416.6         but `Crux.SimulatorCallbacks msgs st' has kind `*'
#20 1416.6     * In the type signature:
#20 1416.6         simulateLLVMFile :: Crux.Logs msgs =>
#20 1416.6                             Log.SupportsCruxLLVMLogMessage msgs =>
#20 1416.6                             FilePath
#20 1416.6                             -> LLVMOptions
#20 1416.6                                -> Crux.SimulatorCallbacks msgs st CruxSimulationResult
#20 1416.6     |
#20 1416.6 194 |   Crux.SimulatorCallbacks msgs st Crux.Types.CruxSimulationResult
#20 1416.6     |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
#20 1416.6 
#20 1416.6 [6 of 7] Compiling Crux.LLVM.Compile ( src/Crux/LLVM/Compile.hs, dist/build/Crux/LLVM/Compile.o, dist/build/Crux/LLVM/Compile.dyn_o )
#20 1416.6 src/Crux/LLVM/Compile.hs:38:41: error: [GHC-61689]
#20 1416.6     Module `Crux.Model' does not export `showBVLiteralSigned'.
#20 1416.6    |
#20 1416.6 38 | import           Crux.Model ( toDouble, showBVLiteralSigned, showFloatLiteral
#20 1416.6    |                                         ^^^^^^^^^^^^^^^^^^^
#20 1416.6 
#20 1416.6 Error: [Cabal-7125]
#20 1416.6 Failed to build crux-llvm-0.12 (which is required by lib:copilot-verifier-examples from copilot-verifier-4.8.1). See the build log above for details.
#20 1416.6 
#20 ERROR: process "/bin/bash -c cabal install          --package-env .          --lib          --constraint=\"copilot==4.8.1\"          --constraint=\"copilot-bluespec==4.8.1\"          --constraint=\"copilot-c99==4.8.1\"          --constraint=\"copilot-core==4.8.1\"          --constraint=\"copilot-prettyprinter==4.8.1\"          --constraint=\"copilot-interpreter==4.8.1\"          --constraint=\"copilot-language==4.8.1\"          --constraint=\"copilot-libraries==4.8.1\"          --constraint=\"copilot-theorem==4.8.1\"          --constraint=\"copilot-verifier==4.8.1\"          --constraint=\"copilot-visualizer==4.8.1\"          copilot**/" did not complete successfully: exit code: 1
------
 > [17/18] RUN cabal install          --package-env .          --lib          --constraint="copilot==4.8.1"          --constraint="copilot-bluespec==4.8.1"          --constraint="copilot-c99==4.8.1"          --constraint="copilot-core==4.8.1"          --constraint="copilot-prettyprinter==4.8.1"          --constraint="copilot-interpreter==4.8.1"          --constraint="copilot-language==4.8.1"          --constraint="copilot-libraries==4.8.1"          --constraint="copilot-theorem==4.8.1"          --constraint="copilot-verifier==4.8.1"          --constraint="copilot-visualizer==4.8.1"          copilot**/:
#20 1416.6 [6 of 7] Compiling Crux.LLVM.Compile ( src/Crux/LLVM/Compile.hs, dist/build/Crux/LLVM/Compile.o, dist/build/Crux/LLVM/Compile.dyn_o )
#20 1416.6 src/Crux/LLVM/Compile.hs:38:41: error: [GHC-61689]
#20 1416.6     Module `Crux.Model' does not export `showBVLiteralSigned'.
#20 1416.6    |
#20 1416.6 38 | import           Crux.Model ( toDouble, showBVLiteralSigned, showFloatLiteral
#20 1416.6    |                                         ^^^^^^^^^^^^^^^^^^^
#20 1416.6 
#20 1416.6 Error: [Cabal-7125]
#20 1416.6 Failed to build crux-llvm-0.12 (which is required by lib:copilot-verifier-examples from copilot-verifier-4.8.1). See the build log above for details.
#20 1416.6 

[ivanperez-keera]

Tagging @RyanGlScott for awareness.

[RyanGlScott]

Apologies, the versions of crux-llvm uploaded to Hackage had inaccurate lower version bounds. I've fixed these in Hackage revisions.

Now that I've applied these in Hackage revisions, the copilot commit that you linked (ivanperez-keera@cb0183a) doesn't have a build plan that supports GHC 9.10:

$ cabal build copilot-verifier
Resolving dependencies...
Error: [Cabal-7107]
Could not resolve dependencies:
[__0] trying: copilot-4.8.1 (user goal)
[__1] trying: base-4.20.2.0/installed-f074 (dependency of copilot)
[__2] trying: copilot-verifier-4.8.1 (user goal)
[__3] trying: crux-llvm-0.12 (dependency of copilot-verifier)
[__4] next goal: crux (dependency of copilot-verifier)
[__4] rejecting: crux-0.9 (conflict: copilot-verifier => crux>=0.7.1 && <0.8)
[__4] skipping: crux-0.8.0.0 (has the same characteristics that caused the previous version to fail: excluded by constraint '>=0.7.1 && <0.8' from 'copilot-verifier')
[__4] rejecting: crux-0.7.2 (conflict: crux-llvm => crux>=0.9 && <0.10)
[__4] skipping: crux; 0.7.1, 0.7 (has the same characteristics that caused the previous version to fail: excluded by constraint '>=0.9 && <0.10' from 'crux-llvm')
[__4] fail (backjumping, conflict set: copilot-verifier, crux, crux-llvm)
After searching the rest of the dependency tree exhaustively, these were the goals I've had most trouble fulfilling: base, crux-llvm, copilot-verifier, crux, copilot
Try running with --minimize-conflict-set to improve the error message.

This is expected, as we'll need to make some slight code changes in copilot-verifier in order to support API changes found in crux-0.8 or later. For instance, if you pass --allow-newer=crux, copilot-verifier will fail to build with:

$ cabal build copilot-verifier --allow-newer=crux
Build profile: -w ghc-9.10.3 -O1
In order, the following will be built (use -v for more details):
 - copilot-verifier-4.8.1 (lib) (first run)
 - copilot-verifier-4.8.1 (lib:copilot-verifier-examples) (first run)
 - copilot-verifier-4.8.1 (exe:verify-examples) (first run)
Preprocessing library for copilot-verifier-4.8.1...
Building library for copilot-verifier-4.8.1...
[4 of 4] Compiling Copilot.Verifier ( src/Copilot/Verifier.hs, /home/rscott/Documents/Hacking/Haskell/copilot/dist-newstyle/build/x86_64-linux/ghc-9.10.3/copilot-verifier-4.8.1/build/Copilot/Verifier.o, /home/rscott/Documents/Hacking/Haskell/copilot/dist-newstyle/build/x86_64-linux/ghc-9.10.3/copilot-verifier-4.8.1/build/Copilot/Verifier.dyn_o )
src/Copilot/Verifier.hs:388:20: error: [GHC-83865]
    • Couldn't match expected type: IO
                                      (SimCtxt
                                         Crux.LLVM.Simulate.CruxLLVM
                                         (ExprBuilder t st (Flags fm))
                                         LLVM)
                  with actual type: SimContext p0 sym0 ext0
    • In a record update at field ‘printHandle’,
      with type constructor ‘SimContext’
      and data constructor ‘SimContext’.
      In the expression:
        (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)
          {printHandle = view Log.outputHandle ?outputConfig}
      In an equation for ‘simctx’:
          simctx
            = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)
                {printHandle = view Log.outputHandle ?outputConfig}
    • Relevant bindings include
        simctx :: SimContext p0 sym0 ext0
          (bound at src/Copilot/Verifier.hs:388:11)
        adapter :: SolverAdapter st
          (bound at src/Copilot/Verifier.hs:383:11)
        clRefs :: CopilotLogRefs (ExprBuilder t st (Flags fm))
          (bound at src/Copilot/Verifier.hs:378:7)
        sym :: ExprBuilder t st (Flags fm)
          (bound at src/Copilot/Verifier.hs:376:11)
        bak :: SimpleBackend t st (Flags fm)
          (bound at src/Copilot/Verifier.hs:375:26)
        verifyWithSymBackend :: SimpleBackend t st (Flags fm)
                                -> HandleAllocator -> IO ()
          (bound at src/Copilot/Verifier.hs:375:5)
    |
388 |       let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)
    |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

src/Copilot/Verifier.hs:427:63: error: [GHC-83865]
    • Couldn't match type ‘ext0’ with ‘LLVM’
      Expected: SimCtxt Crux (ExprBuilder t st (Flags fm)) LLVM
        Actual: SimContext p0 sym0 ext0
      ‘ext0’ is untouchable
        inside the constraints: HasPtrWidth (ArchWidth x)
        bound by a type expected by the context:
                   HasPtrWidth (ArchWidth x) => IO ()
        at src/Copilot/Verifier.hs:(410,9)-(447,56)
    • In the fourth argument of ‘verifyInitialState’, namely ‘simctx’
      In a stmt of a 'do' block:
        initGoals <- verifyInitialState
                       cruxOptsInit [adapter] clRefs simctx initialMem
                       (CW4.initialStreamState proofStateBundle)
      In the second argument of ‘($)’, namely
        ‘do emptyMem <- initializeAllMemory bak llvmCtxt llvmMod
            initialMem <- populateAllGlobals
                            bak (trans ^. globalInitMap) emptyMem
            Log.sayCopilot Log.GeneratingProofState
            proofStateBundle <- CW4.computeBisimulationProofBundle
                                  sym properties spec
            ....’
    • Relevant bindings include
        simctx :: SimContext p0 sym0 ext0
          (bound at src/Copilot/Verifier.hs:388:11)
    |
427 |              verifyInitialState cruxOptsInit [adapter] clRefs simctx initialMem
    |                                                               ^^^^^^

src/Copilot/Verifier.hs:752:18: error: [GHC-27346]
    • The data constructor ‘AbortedExit’ should have 2 arguments, but has been given 1
    • In the pattern: AbortedExit ec
      In an equation for ‘gatherReasons’:
          gatherReasons (AbortedExit ec)
            = PP.vcat ["Simulation called exit!", PP.viaShow ec] :| []
      In an equation for ‘executeStep’:
          executeStep
            opts
            csettings
            clRefs
            simctx
            memVar
            mem
            llvmmod
            modTrans
            triggerGlobals
            triggerOverrides
            assums
            sideConds
            = do globSt <- foldM
                             setupTrigger (llvmGlobals memVar mem) triggerGlobals
                 let initSt = ...
                 res <- executeCrucible [] initSt
                 ....
            where
                setupTrigger gs (_, gv, _)
                  = do zero <- liftIO $ natLit sym 0
                       ....
                llvm_ctx = modTrans ^. transContext
                stepName = cSettingsStepFunctionName csettings
                sym = simctx ^. ctxSymInterface
                ....
    |
752 |   gatherReasons (AbortedExit ec) =
    |                  ^^^^^^^^^^^^^^

Error: [Cabal-7125]
Failed to build copilot-verifier-4.8.1 (which is required by exe:verify-examples from copilot-verifier-4.8.1).

I'd be happy to help update the code to support newer crux versions if you'd like.