[RyanGlScott]

The implementation proves relatively straightforward, as struct field accessors always correspond to a concrete index value, which can then be used to update the value at the corresponding index in the list of struct fields.

I have also updated the what4-structs example in copilot's example suite to demonstrate the use of a Copilot property involving struct updates, and I have added a similar test case to copilot-theorem's test suite.

Fixes #524.

[ivanperez-keera]

Change Manager: Could you please make the following changes?

• Update the changelog of the copilot package, since you changed something there. That should be a separate commit and come last.

• Update the first commit message to read:

copilot-theorem: Support translating `UpdateField` to what4. Refs #524.
   
A new kind of `Op2`, called `UpdateField`, was added to `copilot-core`
in a prior commit to support defining streams with updates to struct fields.

This commit extends `copilot-theorem` to support reasoning about streams
involving struct updates. We do so by providing a new case for the operation
that translates a `copilot-core` `UpdateField` into a What4 representations of
a Copilot expression.

The implementation proves relatively straightforward, as struct field accessors
always correspond to a concrete index value, which can then be used to update
the value at the corresponding index in the list of struct fields.

• Update the second commit message to read:

copilot: Update example to demonstrate struct update support. Refs #524.
    
This commit updates the `what4-structs` example in `copilot` (which depends
on `copilot-theorem`) in order to demonstrate that `copilot-theorem` supports
reasoning about a basic theorem involving a struct field update.

Thanks!

[RyanGlScott]

Done.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • The code proposed compiles and passes all tests. Details:
    Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/272114388

  • The solution proposed produces the expected result. Details:
    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/GaloisInc/copilot-1" -e "NAME=copilot-1" -e "COMMIT=bf0f4548f07484d8a262eba1784036ff17e5e3aa" -it copilot-verify-524
    

• Implementation is documented. Details:
  New functions are documented.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  Updated example demonstrates reasoning with struct updates.
• Required version bumps are evaluated. Details:
  Bump not needed (bug fix).