Rebrand Pantomime to SymFC

CHANGELOG.md

@@ -1,4 +1,4 @@
-# Changelog for `pantomime`
+# Changelog for `sym-fc`
 
 All notable changes to this project will be documented in this file.
 

INSTALL.md

@@ -1,10 +1,10 @@
-# `Pantomime` Installation Guide
+# `SymFC` Installation Guide
 
-This document describes the external dependencies of `Pantomime`, how to add the `pantomime` package as a dependency to your project and how to enable the compiler plugin.
+This document describes the external dependencies of `SymFC`, how to add the `sym-fc` package as a dependency to your project and how to enable the compiler plugin.
 
 ## SMT Solver
 
-`Pantomime` assumes that the [`Z3`](https://github.com/z3prover/z3) SMT solver is installed and available from your `PATH`. To see if an installation is available on your machine, run the following command:
+`SymFC` assumes that the [`Z3`](https://github.com/z3prover/z3) SMT solver is installed and available from your `PATH`. To see if an installation is available on your machine, run the following command:
 
 ```sh
 z3 --version
@@ -14,7 +14,7 @@ In the future, we aim to make it configurable which solver is used.
 
 ## Stack or Cabal build
 
-This guide explains how to use either [`Stack`](https://docs.haskellstack.org/en/stable/) or [`Cabal`](https://www.haskell.org/cabal/) to build `Pantomime`. If you don't already have either of these installed yet, we recommend managing them through [`GHCup`](https://www.haskell.org/ghcup/). Throughout the guide, we will also have collapsed fields like the ones below that help you with commands for your respective build tool of choise:
+This guide explains how to use either [`Stack`](https://docs.haskellstack.org/en/stable/) or [`Cabal`](https://www.haskell.org/cabal/) to build `SymFC`. If you don't already have either of these installed yet, we recommend managing them through [`GHCup`](https://www.haskell.org/ghcup/). Throughout the guide, we will also have collapsed fields like the ones below that help you with commands for your respective build tool of choise:
 
 <details>
 <summary><code>Stack</code> setup</summary>
@@ -32,11 +32,11 @@ During this guide, feel free to build your project after any adjustment to the c
 
 ## Example Repository
 
-If you are simply looking to try out `Pantomime`, or want to start a fresh project with `Pantomime`, you may also use the [example repository](https://github.com/PLSec-VU/pantomime-example) as a template. It can also serve as a reference to inspect in case you get stuck. If the guide was unclear in any way (or you have other suggestions), do [let us know](https://github.com/PLSec-VU/pantomime/issues/new) so we can improve it!
+If you are simply looking to try out `SymFC`, or want to start a fresh project with `SymFC`, you may also use the [example repository](https://github.com/PLSec-VU/sym-fc-example) as a template. It can also serve as a reference to inspect in case you get stuck. If the guide was unclear in any way (or you have other suggestions), do [let us know](https://github.com/PLSec-VU/sym-fc/issues/new) so we can improve it!
 
 ## GHC Version
 
-`Pantomime` is a `GHC` compiler plugin, which causes it to heavily rely on the API that `GHC` exposes to its users. At the time of writing, `Pantomime` is built using `GHC` version `9.12.2`. Altough untested, it is likely that `Pantomime` is incompatible with other versions of `GHC`.
+`SymFC` is a `GHC` compiler plugin, which causes it to heavily rely on the API that `GHC` exposes to its users. At the time of writing, `SymFC` is built using `GHC` version `9.12.2`. Altough untested, it is likely that `SymFC` is incompatible with other versions of `GHC`.
 
 <details>
 <summary><code>Stack</code> setup</summary>
@@ -62,12 +62,12 @@ snapshot: ghc-9.12.2
 TODO
 </details>
 
-We aim to make `Pantomime` compatible with a wider range of `GHC` versions in
+We aim to make `SymFC` compatible with a wider range of `GHC` versions in
 the future!
 
 ## Grisette
 
-`Pantomime` uses a custom version of [`Grisette`](https://hackage-content.haskell.org/package/grisette-0.13.0.1), which can be found [here](https://github.com/RobinWebbers/grisette). In the future, we hope the [pull request](https://github.com/lsrcz/grisette/pull/309) for the extension will get merged and pushed to hackage. Sadly, this is one of the blocking factors for `Pantomime` to get pushed as a package on [`Hackage`](https://hackage.haskell.org/).
+`SymFC` uses a custom version of [`Grisette`](https://hackage-content.haskell.org/package/grisette-0.13.0.1), which can be found [here](https://github.com/RobinWebbers/grisette). In the future, we hope the [pull request](https://github.com/lsrcz/grisette/pull/309) for the extension will get merged and pushed to hackage. Sadly, this is one of the blocking factors for `SymFC` to get pushed as a package on [`Hackage`](https://hackage.haskell.org/).
 
 <details>
 <summary><code>Stack</code> setup</summary>
@@ -89,30 +89,30 @@ You may add the `extra-deps` field if it does not already exist.
 TODO
 </details>
 
-## Pantomime
+## SymFC
 
-We can now add a dependency to `Pantomime` in your project. Additionally, we will add a dependency to [`pantomime-base`](https://github.com/PLSec-VU/pantomime-base). It is not important to understand what this contains for the purpose of this setup, but feel free to check it out if you're interested.
+We can now add a dependency to `SymFC` in your project. Additionally, we will add a dependency to [`sym-fc-base`](https://github.com/PLSec-VU/sym-fc-base). It is not important to understand what this contains for the purpose of this setup, but feel free to check it out if you're interested.
 
 <details>
 <summary><code>Stack</code> setup</summary>
 
-Add the `pantomime` and `pantomime-base` packages to the `extra-deps` field of your `stack.yaml` file. This lets stack know which version of these packages to build with, should they be used. For now, `Pantomime` is not available on [`Hackage`](https://hackage.haskell.org/) so we'll have to specify the git repository and which commit hash to use instead. We recommend getting the latest commit from the `main` branch of the respective repositories.
+Add the `sym-fc` and `sym-fc-base` packages to the `extra-deps` field of your `stack.yaml` file. This lets stack know which version of these packages to build with, should they be used. For now, `SymFC` is not available on [`Hackage`](https://hackage.haskell.org/) so we'll have to specify the git repository and which commit hash to use instead. We recommend getting the latest commit from the `main` branch of the respective repositories.
 
 ```yaml
 extra-deps:
-- git: https://github.com/PLSec-VU/pantomime.git
-  commit: <commit-hash-pantomime>
-- git: https://github.com/PLSec-VU/pantomime-base.git
-  commit: <commit-hash-pantomime-base>
+- git: https://github.com/PLSec-VU/sym-fc.git
+  commit: <commit-hash-sym-fc>
+- git: https://github.com/PLSec-VU/sym-fc-base.git
+  commit: <commit-hash-sym-fc-base>
 ```
 
-Additionally, you will need to add these dependencies to a stanza (e.g. `library`, `executables`) of your choise. This exposes `Pantomime` modules to be available to import in your project. The following shows how to add the dependencies to your `library` build:
+Additionally, you will need to add these dependencies to a stanza (e.g. `library`, `executables`) of your choise. This exposes `SymFC` modules to be available to import in your project. The following shows how to add the dependencies to your `library` build:
 
 ```yaml
 library:
   dependencies:
-  - pantomime
-  - pantomime-base
+  - sym-fc
+  - sym-fc-base
 ```
 
 At this point, you can build the project using `stack build` to see if the `snapshot` you picked in one of the [previous steps](#ghc-version) works for the build. Though unusual, `Stack` may refuse to build if the set of packages was not consistent with themselves. You can try different snapshots until you find one that works.
@@ -128,10 +128,10 @@ TODO
 
 ## Enable Plugin
 
-To allow `Pantomime` to run on your code examples, its plugin needs to be enabled during compilation. You may either enable it per module or project wide. To enable `Pantomime` in a single module, add the following pragma at the top of the respective file.
+To allow `SymFC` to run on your code examples, its plugin needs to be enabled during compilation. You may either enable it per module or project wide. To enable `SymFC` in a single module, add the following pragma at the top of the respective file.
 
 ```haskell
-{-# OPTIONS_GHC "-fplugin Pantomime" #-}
+{-# OPTIONS_GHC "-fplugin SymFC" #-}
 
 module Example.Module where
 ```
@@ -141,12 +141,12 @@ You can enable it project wide by passing this same option in your build files.
 <details>
 <summary><code>Stack</code> setup</summary>
 
-To illustrate, here we enable `Pantomime` when building your project's library.
+To illustrate, here we enable `SymFC` when building your project's library.
 
 ```yaml
 library:
   ghc-options:
-  - -fplugin Pantomime
+  - -fplugin SymFC
 ```
 </details>
 
@@ -158,27 +158,27 @@ TODO
 
 ## Try it!
 
-At this point, the project should compile with the `Pantomime` plugin. You can
+At this point, the project should compile with the `SymFC` plugin. You can
 try to build the following example module.
 
 ```haskell
-{-# OPTIONS_GHC "-fplugin Pantomime" #-} -- or use system-wide setup
+{-# OPTIONS_GHC "-fplugin SymFC" #-} -- or use system-wide setup
 
 module Example (example) where
 
-import Pantomime (Theory (..))
-import qualified Pantomime.BuiltIn as Pantomime
-import qualified Pantomime.Base as Base
+import SymFC (Theory (..))
+import qualified SymFC.BuiltIn as SymFC
+import qualified SymFC.Base as Base
 
 {-# ANN example (Theory Base.axioms) #-}
-example :: Int -> Pantomime.Bool
-example x = Pantomime.boolean $ x + x == 2 * x
+example :: Int -> SymFC.Bool
+example x = SymFC.boolean $ x + x == 2 * x
 ```
 
-If all went well, you should see a query to an SMT solver pop up in your terminal during compilation. `Pantomime` should tell you that the stub is indeed valid.
+If all went well, you should see a query to an SMT solver pop up in your terminal during compilation. `SymFC` should tell you that the stub is indeed valid.
 
-**NOTE**: As of writing, `Pantomime` only verifies a function if it is exported in the module. Make sure this is true in case you do not see any result.
+**NOTE**: As of writing, `SymFC` only verifies a function if it is exported in the module. Make sure this is true in case you do not see any result.
 
 ## Documentation
 
-This concludes the setup guide. Sadly, I cannot refer you to a `Hackage` page with documentation as it is not up yet. The [project page](https://github.com/PLSec-VU/pantomime) contains more information on `Pantomime`. You may also want to build the documentation through [`Haddock`](https://haskell-haddock.readthedocs.io/latest/).
+This concludes the setup guide. Sadly, I cannot refer you to a `Hackage` page with documentation as it is not up yet. The [project page](https://github.com/PLSec-VU/sym-fc) contains more information on `SymFC`. You may also want to build the documentation through [`Haddock`](https://haskell-haddock.readthedocs.io/latest/).

README.md

@@ -1,86 +1,86 @@
-# Pantomime
+# SymFC
 
-`Pantomime` is a full-path symbolic execution engine for `GHC` Core—the internal language of `GHC`, which is based on System FC. `Pantomime` is a `GHC` Core plugin, which verifies validity of a boolean statement, given an annotation, as shown below.
+`SymFC` is a full-path symbolic execution engine for `GHC` Core—the internal language of `GHC`, which is based on System FC. `SymFC` is a `GHC` Core plugin, which verifies validity of a boolean statement, given an annotation, as shown below.
 
 ```haskell
-{-# OPTIONS_GHC "-fplugin Pantomime" #-}
+{-# OPTIONS_GHC "-fplugin SymFC" #-}
 
 module Example.Module (example) where
 
-import Pantomime (Theory (..))
+import SymFC (Theory (..))
 
 {-# ANN example (Theory mempty) #-}
-example :: Bool -> Bool -> Pantomime.Bool
-example x y = Pantomime.boolean $ not x && not y == not (x || y)
+example :: Bool -> Bool -> SymFC.Bool
+example x y = SymFC.boolean $ not x && not y == not (x || y)
 ```
 
-In this case, `Pantomime` shows validity of the statement, quantified over all Boolean inputs.
+In this case, `SymFC` shows validity of the statement, quantified over all Boolean inputs.
 
 **NOTE**: The value supplied to `Theory` is extremely important in most real-world scenarios. An explanation can be found in section [Embeddings](#embeddings).
 
 ## Getting Started
 
-See the [installation guide](./INSTALL.md) on how to install `Pantomime` and its dependencies.
+See the [installation guide](./INSTALL.md) on how to install `SymFC` and its dependencies.
 
 ## Documentation
 
 As of writing, this package is not hosted on `Hackage` and thus we do not host the documentation somewhere. We recommend building the documentation through haddock from your own project until we resolve this. Sorry!
 
 ## Annotation
 
-With this, `GHC` will run `Pantomime` on any expression that has an annotation with the `Theory` type, that returns an argument of type `Pantomime.Bool` when saturated:
+With this, `GHC` will run `SymFC` on any expression that has an annotation with the `Theory` type, that returns an argument of type `SymFC.Bool` when saturated:
 
 ```haskell
 {-# ANN expr (Theory mempty) #-}
-expr :: ... -> Pantomime.Bool
+expr :: ... -> SymFC.Bool
 ```
 
-**PITFALL**: `Pantomime` will only run for expressions that are in the export list of the encapsulating module. Hopefully, we can remove this quirk in the future!
+**PITFALL**: `SymFC` will only run for expressions that are in the export list of the encapsulating module. Hopefully, we can remove this quirk in the future!
 
-`Pantomime` will run when `GHC` compiles the program. If the annotated formula is not valid, `Pantomime` will throw an error and display the arguments that were used to get `False` as a result.
+`SymFC` will run when `GHC` compiles the program. If the annotated formula is not valid, `SymFC` will throw an error and display the arguments that were used to get `False` as a result.
 
 ## Built-In Types
 
-`Pantomime` support the following SMT Theories:
+`SymFC` support the following SMT Theories:
 
 - Theory of Bitvectors
 - Theory of Integers
 - Theory of Arrays
 
-These data types and their functions are regarded as primitives and are exported from `Pantomime.BuiltIn`, along with the `Bool` primitive.
+These data types and their functions are regarded as primitives and are exported from `SymFC.BuiltIn`, along with the `Bool` primitive.
 
 ## Embeddings
 
-Pantomime directly supports computation on Algebraic Data Types. For example, we can check a function that uses `Maybe` and `Bool` as exported by `base`:
+SymFC directly supports computation on Algebraic Data Types. For example, we can check a function that uses `Maybe` and `Bool` as exported by `base`:
 
 ```haskell
 -- NOTE: This will return a counterexample to validity when run.
 {-# ANN example (Theory mempty) #-}
-example :: Maybe Bool -> Pantomime.Bool
-example x = Pantomime.boolean $ x == Just False
+example :: Maybe Bool -> SymFC.Bool
+example x = SymFC.boolean $ x == Just False
 ```
 
-For types that are not algebraic, `Pantomime` exposes an interface to interpret them as SMT solver primitives. For example, the `Int64#` type and its operation `plusInt64#` have a natural embedding with the SMT primitive `BitVec 64` and its respective addition operation. In Pantomime, the user can directly encode this mapping within the annotation:
+For types that are not algebraic, `SymFC` exposes an interface to interpret them as SMT solver primitives. For example, the `Int64#` type and its operation `plusInt64#` have a natural embedding with the SMT primitive `BitVec 64` and its respective addition operation. In SymFC, the user can directly encode this mapping within the annotation:
 
 ```haskell
 axioms :: PluginAxioms
 axioms = PluginAxioms
-  { typeAxioms = fromList [(''Int64#, ''Pantomime.BitVec 64)]
-  , termAxioms = [('plusInt64#, 'Pantomime.bvadd)]
+  { typeAxioms = fromList [(''Int64#, ''SymFC.BitVec 64)]
+  , termAxioms = [('plusInt64#, 'SymFC.bvadd)]
   }
 
 {-# ANN example (Theory axioms) #-}
-example :: ... -> Pantomime.Bool
+example :: ... -> SymFC.Bool
 ```
 
-For a reasonable mapping of `base`, check out [`pantomime-base`](https://github.com/PLSec-VU/pantomime-base). We also provide a mapping for `CLaSH` types and functions in [`pantomime-clash`](https://github.com/PLSec-VU/pantomime-clash).
+For a reasonable mapping of `base`, check out [`sym-fc-base`](https://github.com/PLSec-VU/sym-fc-base). We also provide a mapping for `CLaSH` types and functions in [`sym-fc-clash`](https://github.com/PLSec-VU/sym-fc-clash).
 
 ```haskell
-{-# ANN example (Theory Pantomime.Base.axioms) #-}
-example :: ... -> Pantomime.Bool
+{-# ANN example (Theory SymFC.Base.axioms) #-}
+example :: ... -> SymFC.Bool
 ```
 
 TODO: Writing mappings is a bit more involved, we should have some separate document where we go more in depth. There are whole lot of pitfalls...
-TODO: Add explanation in the pantomime-clash and pantomime-base repositories.
+TODO: Add explanation in the sym-fc-clash and sym-fc-base repositories.
 TODO: Extend explanation on PluginAxiom (at least that its a monoid and how it imports and what order).
 TODO: I would actually like to move most of the explanation here into the project documentation. I think it only makes sense once we have a haddock page for it however.

package.yaml

@@ -1,6 +1,6 @@
-name:                pantomime
+name:                sym-fc
 version:             0.1.0.0
-github:              "PLSec-VU/pantomime"
+github:              "PLSec-VU/sym-fc"
 license:             BSD-3-Clause
 author:              "Robin Webbers"
 maintainer:          "robin_webbers_1@hotmail.com"
@@ -17,7 +17,7 @@ extra-source-files:
 # To avoid duplicated efforts in documentation and dealing with the
 # complications of embedding Haddock markup inside cabal files, it is
 # common to point users to the README.md file.
-description:         Please see the README on GitHub at <https://github.com/PLSec-VU/pantomime#readme>
+description:         Please see the README on GitHub at <https://github.com/PLSec-VU/sym-fc#readme>
 
 default-extensions:
 - AllowAmbiguousTypes
@@ -92,15 +92,15 @@ library:
   - recursion-schemes
 
 tests:
-  pantomime-test:
+  sym-fc-test:
     main: Spec.hs
     source-dirs: test
     ghc-options:
     - -threaded
     - -rtsopts
     - -with-rtsopts=-N
     dependencies:
-    - pantomime
+    - sym-fc
     - hspec
     - hspec-expectations
     - HUnit

src/Effectful/GHC/CoreE.hs

@@ -1,6 +1,5 @@
--- TODO: I guess this doesn't really need to be part of Pantomime? Maybe it
--- should be split into a separate package? Otherwise, we can keep it here for
--- now.
+-- TODO: I guess this doesn't really need to be part of this package? Maybe it
+-- should be split into a separate 'effectful-ghc' package?
 module Effectful.GHC.CoreE
   ( CoreE
   , liftCore