From 1d0ab9c31967d839787f1ff38062dd6dc35b47b8 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 9 Sep 2024 11:31:37 -0400
Subject: [PATCH 1/2] Add example demonstrating struct update support. Refs
 #57.

This is adapted from a similar example in the upstream `copilot` repo.
---
 copilot-verifier/copilot-verifier.cabal       |  1 +
 .../examples/Copilot/Verifier/Examples.hs     |  2 +
 .../Examples/ShouldPass/UpdateStruct.hs       | 62 +++++++++++++++++++
 3 files changed, 65 insertions(+)
 create mode 100644 copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs

diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
index 1bac053..dec767b 100644
--- a/copilot-verifier/copilot-verifier.cabal
+++ b/copilot-verifier/copilot-verifier.cabal
@@ -117,6 +117,7 @@ library copilot-verifier-examples
     Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
     Copilot.Verifier.Examples.ShouldPass.Structs
     Copilot.Verifier.Examples.ShouldPass.UpdateArray
+    Copilot.Verifier.Examples.ShouldPass.UpdateStruct
     Copilot.Verifier.Examples.ShouldPass.Voting
     Copilot.Verifier.Examples.ShouldPass.WCV
 
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples.hs b/copilot-verifier/examples/Copilot/Verifier/Examples.hs
index d3ef537..04f84a6 100644
--- a/copilot-verifier/examples/Copilot/Verifier/Examples.hs
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples.hs
@@ -42,6 +42,7 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge   a
 import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap    as Pass.SubSignedWrap
 import qualified Copilot.Verifier.Examples.ShouldPass.Structs                  as Structs
 import qualified Copilot.Verifier.Examples.ShouldPass.UpdateArray              as UpdateArray
+import qualified Copilot.Verifier.Examples.ShouldPass.UpdateStruct             as UpdateStruct
 import qualified Copilot.Verifier.Examples.ShouldPass.Voting                   as Voting
 import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV
 
@@ -74,6 +75,7 @@ shouldPassExamples verb = Map.fromList
     , example "IntOps" (IntOps.verifySpec verb)
     , example "Structs" (Structs.verifySpec verb)
     , example "UpdateArray" (UpdateArray.verifySpec verb)
+    , example "UpdateStruct" (UpdateStruct.verifySpec verb)
     , example "Voting" (Voting.verifySpec verb)
     , example "WCV" (WCV.verifySpec verb)
 
diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs
new file mode 100644
index 0000000..ecf3f4b
--- /dev/null
+++ b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds        #-}
+
+-- | An example showing of using @copilot-verifier@ to verify a specification
+-- involving structs where individual fields are updated.
+module Copilot.Verifier.Examples.ShouldPass.UpdateStruct where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+-- | Definition for `Volts`.
+data Volts = Volts
+  { numVolts :: Field "numVolts" Word32
+  , flag     :: Field "flag"     Bool
+  }
+
+-- | `Struct` instance for `Volts`.
+instance Struct Volts where
+  typeName _ = "volts"
+  toValues vlts = [ Value Word32 (numVolts vlts)
+                  , Value Bool   (flag vlts)
+                  ]
+
+-- | `Volts` instance for `Typed`.
+instance Typed Volts where
+  typeOf = Struct (Volts (Field 0) (Field False))
+
+data Battery = Battery
+  { temp  :: Field "temp"  Word32
+  , volts :: Field "volts" (Array 10 Volts)
+  , other :: Field "other" (Array 10 (Array 5 Word32))
+  }
+
+-- | `Battery` instance for `Struct`.
+instance Struct Battery where
+  typeName _ = "battery"
+  toValues battery = [ Value typeOf (temp battery)
+                     , Value typeOf (volts battery)
+                     , Value typeOf (other battery)
+                     ]
+
+-- | `Battery` instance for `Typed`. Note that `undefined` is used as an
+-- argument to `Field`. This argument is never used, so `undefined` will never
+-- throw an error.
+instance Typed Battery where
+  typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))
+
+spec :: Spec
+spec = do
+  let battery :: Stream Battery
+      battery = extern "battery" Nothing
+
+  -- Update a struct field, then check it for equality.
+  trigger "updateTrig"
+    ((battery ## temp =$ (+1))#temp == (battery#temp + 1))
+    [arg battery]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "updateStruct"

From a2eb9038041ac20fde7e9619495f66e495e26cdb Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 9 Sep 2024 11:32:24 -0400
Subject: [PATCH 2/2] Document changes in the CHANGELOG. Refs #57.

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

diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
index 0e51eae..2b1b699 100644
--- a/copilot-verifier/CHANGELOG
+++ b/copilot-verifier/CHANGELOG
@@ -1,5 +1,6 @@
 2024-09-09
         * Support verifying programs that use array updates. (#63)
+        * Support verifying programs that use struct updates. (#57)
 
 2024-08-03
         * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)