Merge pull request #54 from Copilot-Language/T53

Release 3.19. Refs #53.

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).
 

copilot-verifier/CHANGELOG

@@ -0,0 +1,7 @@
+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)
+
+2024-02-06
+        * Initial release of `copilot-verifier`.

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:    [email protected]
 Copyright:     (c) Galois, Inc 2021-2024
@@ -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
@@ -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,

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

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)

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) []