copilot-theorem: Support translating struct updates to what4

Copilot 3.20 added support for struct updates via the new UpdateField operation. At the moment, there is no support on the copilot-theorem side for translating UpdateField operations into equivalent what4 expressions. For example, this means that the following Copilot specification will fail when executed:

{-# 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"

$ runghc UpdateField.hs 
UpdateField.hs: src/Copilot/Theorem/What4/Translate.hs:(707,40)-(802,2): Non-exhaustive patterns in case

This limitation currently blocks copilot-verifier support for struct updates, as copilot-verifier makes us of copilot-theorem's what4 translation capabilities.

I have a prototype implementation in this branch which could be used as a starting point for a patch.

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 copilot-language: Support modifying fields of structs #520 introduced support for modifying structs.

Requester

Ryan Scott (Galois)

Method to check presence of bug

Running the following specification that tries to assert a trivial equality:

{-# 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"

produces an error message:

$ runghc UpdateField.hs 
UpdateField.hs: src/Copilot/Theorem/What4/Translate.hs:(707,40)-(802,2): Non-exhaustive patterns in case

when it should instead execute correctly and print valid, invalid, or unknown.

Expected result

Copilot allows using struct updates in copilot-theorem and to reason about them.

Desired result

Copilot allows using struct updates in copilot-theorem and to reason about them.

Proposed solution

Translate struct updates to what4.

Include an example that demonstrates the support for struct updates in copilot-theorem.

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

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@RyanGlScott

Technical Lead: Issue scheduled for fixing in Copilot 4.

Fix assigned to: @RyanGlScott .

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

Implementor: Solution implemented, review requested.

copilot-theorem: Support translating `UpdateField` to what4. Refs Cop…

copilot: Update example to demonstrate struct update support. Refs Co…

copilot-theorem: Add a test case for struct updates. Refs Copilot-Lan…

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

copilot: Document changes in CHANGELOG. Refs Copilot-Language#524.

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

Change Manager: Implementation ready to be merged.

Merge branch 'develop-copilot-theorem-UpdateField'. Close Copilot-Lan…

Navigation Menu

Repository navigation

`copilot-theorem`: Support translating struct updates to `what4` #524

4 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-theorem: Support translating struct updates to what4 #524

Description

Activity

ivanperez-keera commented on Aug 21, 2024

ivanperez-keera commented on Aug 21, 2024

ivanperez-keera commented on Aug 21, 2024

ivanperez-keera commented on Aug 21, 2024

4 remaining items

RyanGlScott commented on Aug 21, 2024

ivanperez-keera commented on Aug 30, 2024

ivanperez-keera commented on Aug 30, 2024

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-theorem`: Support translating struct updates to `what4` #524