Merge branch 'develop-copilot-theorem-UpdateField'. Close #524.

**Description**

Copilot currently supports modifying values from streams of structs, but
not reasoning about them using `copilot-theorem`.

**Type**

- Bug: exception produced when executing valid specification.

**Additional context**

- Issue #520 introduced support for modifying structs.

**Requester**

- Ryan Scott (Galois)

**Method to check presence of bug**

The following Dockerfile installs copilot and runs a spec that uses
copilot-theorem to prove that a stream with an update is equal to
itself, in which case it prints the message "valid", followed by
"Success":

```
--- Dockerfile
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc g++ make libgmp3-dev
RUN apt-get install --yes pkg-config
RUN apt-get install --yes z3

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.4.8
RUN cabal update

ADD UpdateField.hs /tmp/UpdateField.hs

CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && cabal v1-sandbox init \
    && cabal v1-install alex happy \
    && cabal v1-install copilot**/ \
    && cabal v1-exec -- runhaskell /tmp/UpdateField.hs \
    && echo Success

--- UpdateField.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Data.Foldable (for_)
import Data.Functor (void)
import Data.Word (Word32)

import qualified Copilot.Theorem.What4 as CT
import Language.Copilot

data S = S
  { unS :: Field "unS" Word32
  }

instance Struct S where
  typeName _ = "s"
  toValues s = [Value typeOf (unS s)]

instance Typed S where
  typeOf = Struct (S (Field 0))

spec :: Spec
spec = do
  let externS :: Stream S
      externS = extern "extern_s" Nothing

      example :: Stream Word32
      example = (externS ## unS =: 42) # unS

  void $ prop "example" (forAll $ example == example)

main :: IO ()
main = do
  spec' <- reify spec

  -- Use Z3 to prove the properties.
  results <- CT.prove CT.Z3 spec'

  -- Print the results.
  for_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      CT.Valid -> putStrLn "valid"
      CT.Invalid -> putStrLn "invalid"
      CT.Unknown -> putStrLn "unknown"
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-524
```

**Expected result**

Running the dockerfile above prints the message "valid", followed by
"Success", indicating that Copilot allows using struct updates in
`copilot-theorem` and to reason about them.

**Solution implemented**

Translate struct updates to `what4`.

Update example to demonstrate support for struct updates in
`copilot-theorem`.

Include a test that checks that struct updates are supported in
`copilot-theorem`.

**Further notes**

None.

Author: ivanperez-keera

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