Merge branch 'develop-copilot-verifier-upstream'. Close #622.

**Description**

The `copilot-verifier` was developed outside of this repo, but there's interest
in having all Copilot projects and libraries merged into a main repo for ease
of management.

**Type**

- Management: files need to be moved between repos.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

The last state of the `copilot-verifier` is included in this repository,
disregarding history, and adjusting the changelog to make the old issues refer
to `copilot-verifier#<ISSUE_NUM>` so that they are not interpreted as related
to the main Copilot repo.

The following dockerfile checks out the latest version of `copilot-verifier`,
v4.4, and compares it against the version being merged, ignoring differences in
the CHANGELOG (which is expected to be different), checking that there are no
other differences, after which it prints the message "Success":

```Dockerfile
FROM ubuntu:noble

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes git
RUN git config --global advice.detachedHead false

CMD git clone $REPO $NAME \
    && cd $NAME \
    && git checkout $COMMIT \
    && cd .. \
    && git clone -b v4.4 https://github.com/Copilot-Language/copilot-verifier copilot-verifier-original \
    && diff --exclude 'CHANGELOG' -r $NAME/copilot-verifier copilot-verifier-original/copilot-verifier \
    && echo "Success"
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-622
```

**Solution implemented**

Copy last state of `copilot-verifier` as subdirectory of main repo.

Adjust Changelog in `copilot-verifier` to make older issues point to correct
repo.

List cabal files explicitly in cabal.project file, without including
copilot-verifier, to prevent CI from failing with older versions of GHC.

**Further notes**

None.

Author: ivanperez-keera

cabal.project

@@ -1,2 +1,10 @@
 packages:
-  */*.cabal
+  copilot-bluespec/copilot-bluespec.cabal
+  copilot-c99/copilot-c99.cabal
+  copilot-core/copilot-core.cabal
+  copilot-interpreter/copilot-interpreter.cabal
+  copilot-language/copilot-language.cabal
+  copilot-libraries/copilot-libraries.cabal
+  copilot-prettyprinter/copilot-prettyprinter.cabal
+  copilot-theorem/copilot-theorem.cabal
+  copilot/copilot.cabal

copilot-verifier/CHANGELOG

@@ -0,0 +1,49 @@
+2025-06-20
+        * Include `copilot-verifier` in mainline `copilot` repo. (#622)
+
+2025-05-08
+        * Version bump (4.4). (copilot-verifier#85)
+
+2025-03-10
+        * Version bump (4.3). (copilot-verifier#82)
+        * Add `smtSolver` option to `VerifierOptions`. (copilot-verifier#78)
+        * Add `smtFloatMode` option to `VerifierOptions`. (copilot-verifier#79)
+
+2025-01-20
+        * Version bump (4.2). (copilot-verifier#76)
+        * Reject specs that use multiple triggers with the same name.
+          (copilot-verifier#74)
+
+2024-11-08
+        * Version bump (4.1). (copilot-verifier#72)
+
+2024-09-09
+        * Version bump (4.0). (copilot-verifier#69)
+        * Support verifying programs that use array updates.
+          (copilot-verifier#63)
+        * Support verifying programs that use struct updates.
+          (copilot-verifier#57)
+
+2024-08-03
+        * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`.
+          (copilot-verifier#64)
+        * Support GHC 9.4 through 9.8. (copilot-verifier#65)
+
+2024-07-30
+        * When using `Noisy` verbosity, always log proof goals related to the
+          core correspondence proof, even if the goals are trivial.
+          (copilot-verifier#51)
+        * When using `Noisy` verbosity, log more information about which proof
+          goals arise before or after calling the `step()` function.
+          (copilot-verifier#52)
+
+2024-07-11
+        * Version bump (3.20). (copilot-verifier#58)
+
+2024-03-08
+        * Version bump (3.19). (copilot-verifier#53)
+        * Provide more detailed feedback upon a successful run of the verifier.
+        * Make the examples build with Copilot 3.19. (copilot-verifier#53)
+
+2024-02-06
+        * Initial release of `copilot-verifier`.

copilot-verifier/LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2021-2024 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * Neither the name of Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.