`copilot-theorem`'s Kind2 backend takes a proposition and attempts to prove
that it is valid at all possible time steps. Currently, this happens regardless
of whether the proposition is universally or existentially quantified. This is
unsound, and it can lead to valid, existentially quantified properties being
incorrectly labeled as invalid.

This commit adds information about propositions' quantifiers to the Kind2
backend's implementation so that it may use the quantifiers when translating
the properties to Kind2. This is accomplished by updating `specProps` to map
each proposition's identifier to its corresponding `copilot-core` `Prop`.

#594.

`copilot-theorem`'s Kind2 backend takes a proposition and attempts to prove
that it is valid at all possible time steps. Currently, this happens regardless
of whether the proposition is universally or existentially quantified. This is
unsound, and it can lead to valid, existentially quantified properties being
incorrectly labeled as invalid.

This commit fixes the translations of propositions to Kind2 (via Kind2's
TransSys backend) such that the translated properties respect quantifier
information. Specifically, this replaces an unsound use of the `extractProp`
function with an analysis that translates the property differently depending on
whether it is universally or existentially quantified. Because all TransSys
propositions use universal quantification, we convert an existentially
quantified property `∃x.P(x)` as `¬(∀x.¬(P(x)))` during the translation to
TransSys.

**Description**

`Copilot.Language.Spec.prop` and `Copilot.Language.Spec.theorem` are both
reified into as a bare stream of booleans, and do not retain information about
whether the `Prop` passed as argument was a `Forall` or an `Exists`. This makes
the use of the Kind2 connection in `copilot-theorem` render incorrect results.

**Type**

- Bug: Information is lost, leading to unexpected results.

**Additional context**

- Issue #254 will introduce enough information in streams to know which
  quantifier has been used, and adjust the What4 connection to use the
information accordingly and refuse to prove properties that it cannot prove.
The scope of this ticket is how to use that information, once available, to
ensure that `copilot-theorem` produces correct results when Kind2 is used.

**Requester**

- Rob Dockins.

**Method to check presence of bug**

The issue can be detected with the following sample programs:

```haskell
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Data.Functor

import Copilot.Theorem.Kind2
import Copilot.Theorem.Prove
import Language.Copilot

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

spec :: Spec
spec = do
  void $ theorem "t1" (forAll trueThenFalses) (check (kind2Prover def))
  void $ theorem "t2" (exists trueThenFalses) (check (kind2Prover def))

main :: IO ()
main = void $ reify spec
```

Running the specs above or a similar variant via Kind2 should print `proof
checked successfully` as part of its output if it can prove a theorem true, and
`proof failed` otherwise, indicating that respects the quantifier is being
respected. For the cases above, `t1` should be falsified, but `t2` should
succeed. If the prover is not able to prove a property of a given type, a
suitable error message should be printed.

**Expected result**

The following Dockerfile uses the kind2 backend to Copilot spec to try to prove
a universal and an existential property, and checks that the result reported by
`copilot-theorem` matches the expectation, after which it prints the message
"Success":

```
--- Dockerfile-verify-594
FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update

RUN apt-get install --yes \
  ghc-8.6.5 cabal-install-2.4 \
  libtool-bin libz-dev libzmq5 opam z3

RUN opam init --auto-setup --yes --bare --disable-sandboxing \
 && opam switch create default 4.01.0 \
 && opam repository add archive git+https://github.com/ocaml/opam-repository-archive \
 && opam install -y -j "$(nproc)" camlp4 menhir \
 && opam clean -a -c -s --logs

ENV KIND2_VER="0.7.2"
RUN wget https://github.com/kind2-mc/kind2/archive/refs/tags/v${KIND2_VER}.zip \
 && unzip v${KIND2_VER}.zip
WORKDIR kind2-${KIND2_VER}
RUN sed -i.bak -e 's/-pedantic -Werror -Wall/-pedantic -Wall/' ocamlczmq/czmq/configure.ac
RUN eval $(opam env) \
 && ./autogen.sh \
 && ./build.sh \
 && make install
WORKDIR /

ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init
RUN apt-get install --yes git

ADD Spec.hs /tmp/Spec.hs

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-install alex happy \
  && cabal v1-install $NAME/copilot**/ \
  && (cabal v1-exec -- runhaskell /tmp/Spec.hs | grep -e "t1: proof failed" -e "t2: proof checked successfully") \
  && echo "Success"

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

import Data.Functor

import Copilot.Theorem.Kind2
import Copilot.Theorem.Prove
import Language.Copilot

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

spec :: Spec
spec = do
  void $ theorem "t1" (forAll trueThenFalses) (check (kind2Prover def))
  void $ theorem "t2" (exists trueThenFalses) (check (kind2Prover def))

main :: IO ()
main = void $ reify spec
```

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-594
```

**Solution implemented**

Modify `copilot-theorem` to add information about propositions' quantifiers to
the Kind2 backend's implementation so that it may use the quantifiers when
translating the properties to Kind2, translate it appropriately before sending
it to Kind2, and use it also when processing the results from Kind2 to give a
sound result.

**Further notes**

None.

The record field uTypeType, part of Copilot.Core.Type.UType, is never really
used within the module or in any other part of Copilot or, as far as we know,
by any user of Copilot. The record field was deprecated in Copilot 4.1 and no
messages have been received requesting that it be kept in this library. As per
our internal policy of waiting 3 versions from deprecation until a public
interface declaration can be removed, this definition can now be removed.

This commit removes the field uTypeType from the definition of
Copilot.Core.Type.UType, making the type no longer a record.

**Description**

The record field `uTypeType`, part of `Copilot.Core.Type.UType`, is never
really used within the module or in any other part of Copilot or, as far as we
know, by any user of Copilot.

The record field was deprecated in Copilot 4.1 and no messages have been
received requesting that it be kept in this library.

As per our internal policy of waiting 3 versions from deprecation until a
public interface declaration can be removed, this definition can now be
removed.

**Type**

- Management: remove deprecated code.

**Additional context**

- Issue #484 , addressed in Copilot 4.1, deprecated the definition.

**Requester**

- Ivan Perez

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

Running the check below prints a message indicating that the field imported
does not exist:

```
$ runhaskell <<< 'import Copilot.Core(uTypeType); main = return ()'
```

The following Dockerfile tries to import the deprecated record field,
succeeding only when the import fails, after which prints the message
"Success":

```Dockerfile
FROM ubuntu:focal

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/

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

RUN ghcup install ghc 9.10.1
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.10.1
RUN cabal update

SHELL ["/bin/bash", "-c"]
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**/ \
  && ! cabal v1-exec -- runhaskell <<< 'import Copilot.Core(uTypeType); main = return ()' \
  && echo "Success"
```

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-615
```

**Solution implemented**

Remove the deprecated definition `copilot-core:Copilot.Core.Type.uTypeType`.

**Further notes**

None.

Currently the badge for the build status in the README doesn't show up
correctly. GitHub has cached the result but it's not providing the
resulting image, so we see "Build Status" instead.

This commit updates the badge URL to the current
"https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master",
which enables the badge to show properly.

**Description**

Version 4.4 of Copilot should be closed and published on Hackage.

**Type**

- Management: release and publication.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

- Cabal files indicate new version number, constraints are adjusted as needed,
  commit is tagged with version number, and packages are published on hackage.

- The following docker image installs copilot enforcing the new version via
  compiler constraints. It prints the message "Success" at the end if all
  completes correctly, and shows an error message otherwise.

```Dockerfile
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

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

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/

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

RUN ghcup install ghc 9.10.1
RUN ghcup install cabal 3.14
RUN ghcup set ghc 9.10.1
RUN cabal update

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && cabal install \
         --package-env . \
         --lib \
         --constraint="copilot==4.4" \
         --constraint="copilot-c99==4.4" \
         --constraint="copilot-core==4.4" \
         --constraint="copilot-prettyprinter==4.4" \
         --constraint="copilot-interpreter==4.4" \
         --constraint="copilot-language==4.4" \
         --constraint="copilot-libraries==4.4" \
         --constraint="copilot-theorem==4.4" \
         copilot**/ \
    && echo Success
```

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-618
```

**Solution implemented**

- Cabal files indicate new version number, constraints are adjusted as needed,
  commit is tagged with version number, and packages are published on hackage.

**Further notes**

None.