`copilot-theorem`: Examples do not compile

[RyanGlScott]

Description

Some example programs in the copilot-theorem/example subdirectory have bitrotted, as they depend on a Copilot.Theorem.Prover.Z3 module that is no longer included in copilot-theorem.cabal (as of 6a67d89). Attempting to build any of these examples results in compilation failures.

Type

• Bug: Example programs fail to compile.

Additional context

Copilot.Theorem.Prover.Z3 was an early, SMT solver–based approach for proving properties about Copilot specifications. The copilot-theorem library has largely replaced Copilot.Theorem.Prover.Z3 will different APIs, such as those offered by Copilot.Theorem.Prover.SMT and Copilot.Theorem.What4. Of the latter two, the API in Copilot.Theorem.Prover.SMT is closest to what Copilot.Theorem.Prover.Z3 offered.

Requester

• Ryan Scott (Galois)

Method to check presence of bug

First, build the copilot libraries, using a method such as the following:

$ cabal build copilot --write-ghc-environment-files=always

Then invoke ghc on one of the files in the copilot-theorem/examples subdirectory that import Copilot.Theorem.Prover.Z3. The bug manifests as a GHC compilation error, such as in the following example:

$ ghc copilot-theorem/examples/BoyerMoore.hs
Loaded package environment from /Users/rscott/Documents/Hacking/Haskell/copilot/.ghc.environment.aarch64-darwin-9.4.8
[1 of 1] Compiling BoyerMoore ( copilot-theorem/examples/BoyerMoore.hs, copilot-theorem/examples/BoyerMoore.o )

copilot-theorem/examples/BoyerMoore.hs:8:1: error:
 Could not find module ‘Copilot.Theorem.Prover.Z3’
 Perhaps you meant
 Copilot.Theorem.Prover.SMT (from copilot-theorem-4.6)
 Copilot.Theorem.Prover.SMT (needs flag -package-id copilot-theorem-4.3)
 Copilot.Theorem.Prover.SMT (needs flag -package-id copilot-theorem-4.3)
 Use -v (or `:set -v` in ghci) to see a list of the files searched for.
 |
8 | import Copilot.Theorem.Prover.Z3
 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Expected result

Invoking ghc on any of the examples in the copilot-theorem/examples subdirectory should succeed.

Desired result

Invoking ghc on any of the examples in the copilot-theorem/examples subdirectory should succeed.

Proposed solution

Modify the code in each of the examples in copilot-theorem/examples to import from Copilot.Theorem.Prover.SMT instead of Copilot.Theorem.Prover.Z3, making adjustments as needed to adapt to the slightly different API in Copilot.Theorem.Prover.SMT.

Further notes

None.

[chathhorn-galois]

I could do this if you want to assign it to me.

[ivanperez-keera]

Change Manager: modified description to qualify which examples fail, and the nature of the changes proposed.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.7.1.

Fix assigned to: @chathhorn-galois .