copilot-libraries: Add stream analysis module

Description

There is a need to have in Copilot a module that includes stream and spec analysis functions. Such functions have been useful in other projects, and they could be added as part of Copilot's standard library so that they are available to all users.

Type

Feature: Add new module with stream analysis functions.

Additional context

None.

Requester

Ivan Perez.

Method to check presence of bug

Not applicable (not a bug).

Expected result

copilot-libraries includes a stream analysis module that provides ways to perform checks and formal analysis on Copilot streams and specs.

Desired result

copilot-libraries includes a stream analysis module that provides ways to perform basic checks on Copilot streams.

Proposed solution

Add a new module to copilot-libraries that includes functions to detect whether a stream is always true or always false.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@ivanperez-keera

Technical Lead: Issue scheduled for fixing in Copilot 4.7.1.

Fix assigned to: @ivanperez-keera .

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

Implementor: Solution implemented, review requested.

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

copilot-libraries: Add stream analysis module. Refs Copilot-Language#726

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

copilot-libraries: Add stream analysis module. Refs Copilot-Language#726

copilot-libraries: Document changes in CHANGELOG. Refs Copilot-Langua…

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/278084383

The solution proposed produces the expected result. Details:
The following Dockerfile checks that all the stream analysis functions can be used to determine if a stream is always true or always false by testing several definitions against an expectation, after which it prints the message "Success":

--- Dockerfile-verify-726
FROM ubuntu:jammy

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

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config \
      z3

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -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 ghcup install ghc 9.8.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.8.4
RUN cabal update

ADD expectation /tmp/
ADD Test.hs /tmp/

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install \
       $NAME/copilot/ \
       $NAME/copilot-c99/ \
       $NAME/copilot-core/ \
       $NAME/copilot-prettyprinter/ \
       $NAME/copilot-interpreter/ \
       $NAME/copilot-language/ \
       $NAME/copilot-libraries/ \
       $NAME/copilot-theorem/ \
  && cabal v1-exec -- runhaskell /tmp/Test.hs > /tmp/output \
  && diff -q /tmp/expectation /tmp/output \
  && echo "Success"

--- expectation
Is true trivially true?: Yes
Is false trivially false?: Yes
Is something not always true trivially true?: No
Is something not always false trivially false?: No
Is stream and its negation trivially true?: Yes

--- Test.hs
module Main where

import           Control.Monad (forM_, void)
import qualified Prelude       as P

import Copilot.Library.Analysis
import Copilot.Theorem.What4
import Language.Copilot

spec :: Spec
spec = do
  void $ prop "Is true trivially true?" (triviallyTrue true)

  void $ prop "Is false trivially false?" (triviallyFalse false)

  let a = [False] ++ true
      b = not a

  void $ prop "Is something not always true trivially true?"  (triviallyTrue a)
  void $ prop "Is something not always false trivially false?" (triviallyFalse a)

  let c = extern "c" Nothing

  void $ prop "Is stream and its negation trivially true?" (triviallyTrue (c || not c))

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

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

  -- Print the results.
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      Valid   -> putStrLn "Yes"
      Invalid -> putStrLn "No"
      Unknown -> putStrLn "I don't know"

Command (substitute variables based on new path after merge):

$ docker run -e REPO=https://github.com/ivanperez-keera/copilot -e NAME=copilot -e COMMIT=fb249d239ed3722b1cbe03e2c6be86e112a2afb4 copilot-verify-726

Implementation is documented. Details:
The new module and functions include documentation.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed; change does not affect existing examples.
Author is internal or has provided signed CLA.
Required version bumps are evaluated. Details:
Bump not needed, change adds definitions but does not alter existing ones.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-analysis'. Close Copilot-Language#726.

Navigation Menu

Repository navigation

`copilot-libraries`: Add stream analysis module #726

5 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-libraries: Add stream analysis module #726

Description

Activity

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

5 remaining items

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

ivanperez-keera commented on May 8, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-libraries`: Add stream analysis module #726