From bd344ce811735164f76862bb3df3a76a5328f80e Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 8 Mar 2024 10:32:24 -0500
Subject: [PATCH 1/6] Fix warnings in WCV example

---
 .../Verifier/Examples/ShouldPass/WCV.hs       | 77 +++++++++----------
 1 file changed, 36 insertions(+), 41 deletions(-)

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
index 1dd727e..118e7a3 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
@@ -9,13 +9,12 @@
 module Copilot.Verifier.Examples.ShouldPass.WCV where
 
 import Language.Copilot
-import qualified Copilot.Theorem.What4 as CT
+-- import qualified Copilot.Theorem.What4 as CT
 import Copilot.Compile.C99
 import Copilot.Verifier ( Verbosity, VerifierOptions(..)
                         , defaultVerifierOptions, verifyWithOptions )
 
-import qualified Prelude as P
-import Data.Foldable (forM_)
+-- import Data.Foldable (forM_)
 import qualified Control.Monad as Monad
 
 
@@ -38,44 +37,6 @@ tcoathr = extern "tcoathr" Nothing
 type Vect2 = (Stream Double, Stream Double)
 
 
---------------------------------
--- External streams for relative position and velocity.
---------------------------------
-
--- | The relative x velocity between ownship and the intruder.
-vx :: Stream Double
-vx = extern "relative_velocity_x" Nothing
-
--- | The relative y velocity between ownship and the intruder.
-vy :: Stream Double
-vy = extern "relative_velocity_y" Nothing
-
--- | The relative z velocity between ownship and the intruder.
-vz :: Stream Double
-vz = extern "relative_velocity_z" Nothing
-
--- | The relative velocity as a 2D vector.
-v :: (Stream Double, Stream Double)
-v = (vx, vy)
-
-
--- | The relative x position between ownship and the intruder.
-sx :: Stream Double
-sx = extern "relative_position_x" Nothing
-
--- | The relative y position between ownship and the intruder.
-sy :: Stream Double
-sy = extern "relative_position_y" Nothing
-
--- | The relative z position between ownship and the intruder.
-sz :: Stream Double
-sz = extern "relative_position_z" Nothing
-
--- | The relative position as a 2D vector.
-s :: (Stream Double, Stream Double)
-s = (sx, sy)
-
-
 ------------------
 -- The following section contains basic libraries for working with vectors.
 ------------------
@@ -169,7 +130,41 @@ horizontalWCV tvar s v =
   (norm s <= dthr) ||
   (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))
 
+spec :: Spec
 spec = do
+  -- External streams for relative position and velocity.
+  let -- The relative x velocity between ownship and the intruder.
+      vx :: Stream Double
+      vx = extern "relative_velocity_x" Nothing
+
+      -- The relative y velocity between ownship and the intruder.
+      vy :: Stream Double
+      vy = extern "relative_velocity_y" Nothing
+
+      -- The relative z velocity between ownship and the intruder.
+      vz :: Stream Double
+      vz = extern "relative_velocity_z" Nothing
+
+      -- The relative velocity as a 2D vector.
+      v :: (Stream Double, Stream Double)
+      v = (vx, vy)
+
+
+      -- The relative x position between ownship and the intruder.
+      sx :: Stream Double
+      sx = extern "relative_position_x" Nothing
+
+      -- The relative y position between ownship and the intruder.
+      sy :: Stream Double
+      sy = extern "relative_position_y" Nothing
+
+      -- The relative z position between ownship and the intruder.
+      sz :: Stream Double
+      sz = extern "relative_position_z" Nothing
+
+      -- The relative position as a 2D vector.
+      s :: (Stream Double, Stream Double)
+      s = (sx, sy)
   Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))
   -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
   trigger "well_clear_violation" (wcv tep s sz v vz) []

From 6d4469efe210f468c3b1175a21327d2b8578392a Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 8 Mar 2024 10:39:39 -0500
Subject: [PATCH 2/6] Use Copilot conventions for CHANGELOG

---
 copilot-verifier/CHANGELOG              | 2 ++
 copilot-verifier/CHANGELOG.md           | 5 -----
 copilot-verifier/copilot-verifier.cabal | 2 +-
 3 files changed, 3 insertions(+), 6 deletions(-)
 create mode 100644 copilot-verifier/CHANGELOG
 delete mode 100644 copilot-verifier/CHANGELOG.md

diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
new file mode 100644
index 0000000..e430570
--- /dev/null
+++ b/copilot-verifier/CHANGELOG
@@ -0,0 +1,2 @@
+2024-02-06
+        * Initial release of `copilot-verifier`.
diff --git a/copilot-verifier/CHANGELOG.md b/copilot-verifier/CHANGELOG.md
deleted file mode 100644
index 358751a..0000000
--- a/copilot-verifier/CHANGELOG.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# Release history for copilot-verifier
-
-## 0.1 (February 2024)
-
-* Initial release of `copilot-verifier.
diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index 02cad35..917ba35 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -21,7 +21,7 @@ Description:
   in a precise way to the meaning of the original stream specification. The
   generated verification conditions are then dispatched to SMT solvers to be
   automatically solved.
-extra-doc-files: CHANGELOG.md, README.md
+extra-doc-files: CHANGELOG, README.md
 
 source-repository head
   type:     git

From dd592221502c51fca74564667fc213589d81133d Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 8 Mar 2024 10:41:57 -0500
Subject: [PATCH 3/6] Require building with Copilot 3.19. Refs #53.

The only code changes required were some minor changes in the
`copilot-verifier` examples to avoid using deprecated (and now removed) alias
for `typeName`.
---
 copilot-verifier/CHANGELOG                         |  3 +++
 copilot-verifier/copilot-verifier.cabal            | 14 +++++++-------
 .../Verifier/Examples/ShouldPass/ArrayOfStructs.hs |  2 +-
 .../Verifier/Examples/ShouldPass/Structs.hs        |  4 ++--
 4 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
index e430570..209b891 100644
--- a/copilot-verifier/CHANGELOG
+++ b/copilot-verifier/CHANGELOG
@@ -1,2 +1,5 @@
+2024-03-08
+        * Make the examples build with Copilot 3.19. (#53)
+
 2024-02-06
         * Initial release of `copilot-verifier`.
diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index 917ba35..a981cb5 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -45,13 +45,13 @@ common bldflags
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot >= 3.18.1 && < 3.19,
-    copilot-c99 >= 3.18.1 && < 3.19,
-    copilot-core >= 3.18.1 && < 3.19,
-    copilot-libraries >= 3.18.1 && < 3.19,
-    copilot-language >= 3.18.1 && < 3.19,
-    copilot-prettyprinter >= 3.18.1 && < 3.19,
-    copilot-theorem >= 3.18.1 && < 3.19,
+    copilot >= 3.19 && < 3.20,
+    copilot-c99 >= 3.19 && < 3.20,
+    copilot-core >= 3.19 && < 3.20,
+    copilot-libraries >= 3.19 && < 3.20,
+    copilot-language >= 3.19 && < 3.20,
+    copilot-prettyprinter >= 3.19 && < 3.20,
+    copilot-theorem >= 3.19 && < 3.20,
     crucible >= 0.7 && < 0.8,
     crucible-llvm >= 0.6 && < 0.7,
     crux >= 0.7 && < 0.8,
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs
index 3ecee99..9edc1ec 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs
@@ -10,7 +10,7 @@ import Language.Copilot
 data S = S { field :: Field "field" Int16 }
 
 instance Struct S where
-  typename _ = "s"
+  typeName _ = "s"
   toValues s = [Value Int16 (field s)]
 
 instance Typed S where
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
index 2cf989b..d778dd7 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
@@ -24,7 +24,7 @@ data Volts = Volts
 
 -- | `Struct` instance for `Volts`.
 instance Struct Volts where
-  typename _ = "volts"
+  typeName _ = "volts"
   toValues vlts = [ Value Word16 (numVolts vlts)
                   , Value Bool   (flag vlts)
                   ]
@@ -41,7 +41,7 @@ data Battery = Battery
 
 -- | `Battery` instance for `Struct`.
 instance Struct Battery where
-  typename _ = "battery"
+  typeName _ = "battery"
   toValues battery = [ Value typeOf (temp battery)
                      , Value typeOf (volts battery)
                      , Value typeOf (other battery)

From 7b67812e289cde2fc423c0b939209bcd7d432f06 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 8 Mar 2024 10:59:15 -0500
Subject: [PATCH 4/6] Fix typo: s/ICFP 2024/ICFP 2023/

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e3eec6f..4a90648 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@ verification conditions are then dispatched to SMT solvers to
 be automatically solved.  We will have more to say about exactly
 what is meant by this correspondence below.
 
-Copilot Verifier is described in the ICFP 2024 paper [_Trustworthy Runtime
+Copilot Verifier is described in the ICFP 2023 paper [_Trustworthy Runtime
 Verification via Bisimulation (Experience
 Report)_](https://dl.acm.org/doi/abs/10.1145/3607841).
 

From 04af09e712de95438d440f0a690caa363cb5d600 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 8 Mar 2024 11:00:17 -0500
Subject: [PATCH 5/6] Mention #50 in the CHANGELOG

---
 copilot-verifier/CHANGELOG | 1 +
 1 file changed, 1 insertion(+)

diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
index 209b891..3324e6a 100644
--- a/copilot-verifier/CHANGELOG
+++ b/copilot-verifier/CHANGELOG
@@ -1,4 +1,5 @@
 2024-03-08
+        * Provide more detailed feedback upon a successful run of the verifier.
         * Make the examples build with Copilot 3.19. (#53)
 
 2024-02-06

From 7304ded9ac43b705a2419294ab27cf760f47249a Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 8 Mar 2024 10:58:02 -0500
Subject: [PATCH 6/6] Bump version number to 3.19. Refs #53.

---
 copilot-verifier/CHANGELOG              | 1 +
 copilot-verifier/copilot-verifier.cabal | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
index 3324e6a..83ee397 100644
--- a/copilot-verifier/CHANGELOG
+++ b/copilot-verifier/CHANGELOG
@@ -1,4 +1,5 @@
 2024-03-08
+        * Version bump (3.19). (#53)
         * Provide more detailed feedback upon a successful run of the verifier.
         * Make the examples build with Copilot 3.19. (#53)
 
diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index a981cb5..18b0d0b 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          copilot-verifier
-Version:       0.1
+Version:       3.19
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com
 Copyright:     (c) Galois, Inc 2021-2024