copilot-theorem: Support translating UpdateField to what4. Refs #524.

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2024-08-30
+        * Add support for struct updates in Copilot.Theorem.What4. (#524)
+
 2024-07-07
         * Version bump (3.20). (#522)
         * What4 upper-bound dependency version bump. (#514)

copilot-theorem/src/Copilot/Theorem/What4/Translate.hs

@@ -799,6 +799,8 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
   (CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2
   (CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2
   (CE.Index _, xe1, xe2) -> translateIndex xe1 xe2
+  (CE.UpdateField atp _ftp extractor, structXe, fieldXe) ->
+    translateUpdateField atp extractor structXe fieldXe
   where
     -- Translate an 'CE.Add' operation and its arguments into a what4
     -- representation of the appropriate type.
@@ -964,6 +966,55 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
         liftIO $ buildIndexExpr sym ix xes
       _ -> unexpectedValues "index operation"
 
+    -- Translate an 'CE.UpdateField' operation and its arguments into a what4
+    -- representation. This function will panic if one of the following does not
+    -- hold:
+    --
+    -- - The argument is not a struct.
+    --
+    -- - The struct's field cannot be found.
+    translateUpdateField :: forall struct s.
+                            KnownSymbol s
+                         => CT.Type struct
+                         -- ^ The type of the struct argument
+                         -> (struct -> CT.Field s b)
+                         -- ^ Extract a struct field
+                         -> XExpr sym
+                         -- ^ The first argument value (should be a struct)
+                         -> XExpr sym
+                         -- ^ The second argument value (should be the same type
+                         -- as the struct field)
+                         -> TransM sym (XExpr sym)
+                         -- ^ The first argument value, but with an updated
+                         -- value for the supplied field.
+    translateUpdateField structTp extractor structXe newFieldXe =
+      case (structTp, structXe) of
+        (CT.Struct s, XStruct structFieldXes) ->
+          case mIx s of
+            Just ix -> return $ XStruct $ updateAt ix newFieldXe structFieldXes
+            Nothing ->
+              panic [ "Could not find field " ++ show fieldNameRepr
+                    , show s
+                    ]
+        _ -> unexpectedValues "update-field operation"
+      where
+        -- Update an element of a list at a particular index. This assumes the
+        -- preconditions that the index is a non-negative number that is less
+        -- than the length of the list.
+        updateAt :: forall a. Int -> a -> [a] -> [a]
+        updateAt _ _ [] = []
+        updateAt 0 new (_:xs) = new : xs
+        updateAt n new (x:xs) = x : updateAt (n-1) new xs
+
+        fieldNameRepr :: SymbolRepr s
+        fieldNameRepr = fieldName (extractor undefined)
+
+        structFieldNameReprs :: CT.Struct struct => struct -> [Some SymbolRepr]
+        structFieldNameReprs s = valueName <$> CT.toValues s
+
+        mIx :: CT.Struct struct => struct -> Maybe Int
+        mIx s = elemIndex (Some fieldNameRepr) (structFieldNameReprs s)
+
     -- Check the types of the arguments. If the arguments are bitvector values,
     -- apply the 'BVOp2'. If the arguments are floating-point values, apply the
     -- 'FPOp2'. Otherwise, 'panic'.

copilot-theorem/tests/Test/Copilot/Theorem/What4.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 -- The following warning is disabled due to a necessary instance of SatResult
 -- defined in this module.
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -6,17 +7,22 @@ module Test.Copilot.Theorem.What4 where
 
 -- External imports
 import Data.Int                             (Int8)
+import Data.Word                            (Word32)
 import Test.Framework                       (Test, testGroup)
 import Test.Framework.Providers.QuickCheck2 (testProperty)
-import Test.QuickCheck                      (Property, arbitrary, forAll)
+import Test.QuickCheck                      (Arbitrary (arbitrary), Property,
+                                             arbitrary, forAll)
 import Test.QuickCheck.Monadic              (monadicIO, run)
 
 -- External imports: Copilot
-import           Copilot.Core.Expr      (Expr (Const, Op2))
-import           Copilot.Core.Operators (Op2 (..))
+import           Copilot.Core.Expr      (Expr (Const, Op1, Op2))
+import           Copilot.Core.Operators (Op1 (..), Op2 (..))
 import           Copilot.Core.Spec      (Spec (..))
 import qualified Copilot.Core.Spec      as Copilot
-import           Copilot.Core.Type      (Typed (typeOf))
+import           Copilot.Core.Type      (Field (..),
+                                         Struct (toValues, typeName),
+                                         Type (Struct), Typed (typeOf),
+                                         Value (..))
 
 -- Internal imports: Modules being tested
 import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)
@@ -30,6 +36,7 @@ tests =
     [ testProperty "Prove via Z3 that true is valid"    testProveZ3True
     , testProperty "Prove via Z3 that false is invalid" testProveZ3False
     , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst
+    , testProperty "Prove via Z3 that a struct update is valid" testProveZ3StructUpdate
     ]
 
 -- * Individual tests
@@ -77,6 +84,54 @@ testProveZ3EqConst = forAll arbitrary $ \x ->
     spec x = propSpec propName $
       Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
 
+-- | Test that Z3 is able to prove the following expresion valid:
+-- @
+--   for all (s :: MyStruct),
+--   ((s ## testField =$ (+1)) # testField) == ((s # testField) + 1)
+-- @
+testProveZ3StructUpdate :: Property
+testProveZ3StructUpdate = forAll arbitrary $ \x ->
+    monadicIO $ run $ checkResult Z3 propName (spec x) Valid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: TestStruct -> Spec
+    spec s = propSpec propName $
+      Op2
+        (Eq typeOf)
+        (getField
+          (Op2
+            (UpdateField typeOf typeOf testField)
+            sExpr
+            (add1 (getField sExpr))))
+        (add1 (getField sExpr))
+      where
+        sExpr :: Expr TestStruct
+        sExpr = Const typeOf s
+
+        getField :: Expr TestStruct -> Expr Word32
+        getField = Op1 (GetField typeOf typeOf testField)
+
+        add1 :: Expr Word32 -> Expr Word32
+        add1 x = Op2 (Add typeOf) x (Const typeOf 1)
+
+-- | A simple data type with a 'Struct' instance and a 'Field'. This is only
+-- used as part of 'testProveZ3StructUpdate'.
+newtype TestStruct = TestStruct { testField :: Field "testField" Word32 }
+
+instance Arbitrary TestStruct where
+  arbitrary = do
+    w32 <- arbitrary
+    return (TestStruct (Field w32))
+
+instance Struct TestStruct where
+  typeName _ = "testStruct"
+  toValues s = [Value typeOf (testField s)]
+
+instance Typed TestStruct where
+  typeOf = Struct (TestStruct (Field 0))
+
 -- | Check that the solver's satisfiability result for the given property in
 -- the given spec matches the expectation.
 checkResult :: Solver -> String -> Spec -> SatResult -> IO Bool

copilot/CHANGELOG

@@ -1,3 +1,6 @@
+2024-08-30
+        * Update example to demonstrate struct update support. (#524)
+
 2024-07-07
         * Version bump (3.20). (#522)
         * Update README to reflect support for GHC 9.8. (#518)

copilot/examples/what4/Structs.hs

@@ -64,6 +64,10 @@ spec = do
   void $ prop "Example 2" $ forAll $
     (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
 
+  -- Update a struct field, then check it for equality.
+  void $ prop "Example 3" $ forAll $
+    ((battery ## temp =$ (+1))#temp == (battery#temp + 1))
+
 main :: IO ()
 main = do
   spec' <- reify spec