copilot-verifier: Include in mainline copilot repo. Refs #622.

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.