From 84c4f639c0f16b265e6370641f9b329122510c18 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Mon, 24 May 2021 14:12:21 -0700
Subject: [PATCH 01/13] add hoist_ifs_in_goal

---
 src/SAWScript/Builtins.hs    |  7 +++++++
 src/SAWScript/Interpreter.hs |  5 +++++
 src/SAWScript/Proof.hs       | 13 +++++++++++++
 3 files changed, 25 insertions(+)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 4dc754678d..dcc113e3d7 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -501,6 +501,13 @@ simplifyGoal ss =
      prop' <- io (simplifyProp sc ss (goalProp goal))
      return (prop', RewriteEvidence ss)
 
+hoistIfsInGoalPrim :: ProofScript ()
+hoistIfsInGoalPrim =
+  execTactic $ tacticChange $ \goal ->
+    do sc <- getSharedContext
+       p <- io (hoistIfsInGoal sc (goalProp goal))
+       return (p, \_ -> TrivialEvidence) -- TODO: what is the evidence here?
+
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
   execTactic $ tacticChange $ \goal ->
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index dcd84c02d4..a604e54bc5 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1194,6 +1194,11 @@ primitives = Map.fromList
     Current
     [ "Apply the given simplifier rule set to the current goal." ]
 
+  , prim "hoist_ifs_in_goal"            "ProofScript ()"
+    (pureVal hoistIfsInGoalPrim)
+    Experimental
+    [ "hoist ifs in the current proof goal" ]
+
   , prim "goal_eval"           "ProofScript ()"
     (pureVal (goal_eval []))
     Current
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 709db3b9b5..f903cc72c8 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -17,6 +17,7 @@ module SAWScript.Proof
   , splitProp
   , unfoldProp
   , simplifyProp
+  , hoistIfsInGoal
   , evalProp
   , betaReduceProp
   , falseProp
@@ -176,6 +177,18 @@ simplifyProp sc ss (Prop tm) =
   do tm' <- rewriteSharedTerm sc ss tm
      return (Prop tm')
 
+hoistIfsInGoal :: SharedContext -> Prop -> IO Prop
+hoistIfsInGoal sc p =
+  case asEqTrue pTerm of
+    Just t -> do
+      tm <- hoistIfs sc t
+      eqTm <- scEqTrue sc tm
+      newP <- termToProp sc eqTm
+      return newP
+    Nothing -> fail "hoist_ifs: expected EqTrue"
+  where
+    pTerm = unProp p
+
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will
 --   perform a variety of simplifications and rewrites.

From 5fe62e109dc0def59ea46736b5e1fa8ac757dcb1 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Fri, 28 May 2021 14:57:09 -0700
Subject: [PATCH 02/13] add evidence for hoistIfs

---
 src/SAWScript/Builtins.hs | 5 +++--
 src/SAWScript/Proof.hs    | 6 ++++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index dcc113e3d7..c0649ade52 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -505,8 +505,9 @@ hoistIfsInGoalPrim :: ProofScript ()
 hoistIfsInGoalPrim =
   execTactic $ tacticChange $ \goal ->
     do sc <- getSharedContext
-       p <- io (hoistIfsInGoal sc (goalProp goal))
-       return (p, \_ -> TrivialEvidence) -- TODO: what is the evidence here?
+       let tac = \sctx g -> hoistIfsInGoal sctx g
+       p <- io $ tac sc (goalProp goal)
+       return (p, InternalTacticEvidence tac)
 
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index f903cc72c8..84f09e0902 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -356,6 +356,8 @@ data Evidence
     --   evidence is use to check the modified goal.
   | EvalEvidence (Set VarIndex) Evidence
 
+  | InternalTacticEvidence (SharedContext -> Prop -> IO Prop) Evidence
+
 -- | The the proposition proved by a given theorem.
 thmProp :: Theorem -> Prop
 thmProp (LocalAssumption p) = p
@@ -601,6 +603,10 @@ checkEvidence sc = check mempty
         do p' <- simplifyProp sc ss p
            check hyps e' p'
 
+      InternalTacticEvidence tac e' ->
+        do p' <- tac sc p
+           check hyps e' p'
+
       EvalEvidence vars e' ->
         do p' <- evalProp sc vars p
            check hyps e' p'

From ed7e4c5f6cf51e0cfba175541ae5725f3695c03d Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Fri, 14 May 2021 11:03:13 -0700
Subject: [PATCH 03/13] Add draft contributor guidelines

---
 CONTRIBUTING.md | 204 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 204 insertions(+)
 create mode 100644 CONTRIBUTING.md

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 0000000000..56ae3985e8
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,204 @@
+# SAW development
+
+This document explains our standards for developing SAW. Our goals are
+to have a development process that:
+
+- consistently yields reliable software artifacts,
+- quickly incorporates improvements and gets them into user hands, and
+- allows new contributors to have an immediate impact.
+
+It describes our methods and practices for:
+
+- testing and continuous integration;
+- organizing, branching, and merging this repository;
+- producing and publishing release artifacts; and
+- feature and release planning.
+
+This is a living document that is not (and possibly cannot be)
+comprehensive. If something is missing or unclear, or if you have
+suggestions for improving our processes, please file an issue or open a
+pull request.
+
+# Building
+
+See guidance in [README.md](README.md) for information on building SAW.
+
+# Testing
+
+The core test suite for SAW consists of a collection of integration
+tests, in subdirectories of the `intTest` directory. A Cabal test suite
+called `integration_tests` is responsible for invoking these tests.
+
+## Dependency freezing
+
+To ensure repeatable test results, our CI system uses
+`cabal.project.freeze` files to fix the version of all dependencies
+prior to building. It uses one of several version freezing files, each
+named `cabal.GHC-<VER>.config`, for GHC version `<VER>`.
+
+We recommend building and testing using these files unless your explicit
+goal is to assess compatibility with different library versions. To do
+so, run the following before building or testing:
+
+    ln -s `cabal.GHC-<VER>.config cabal.project.freeze
+
+## Running and Creating Tests
+
+For more information on running and creating tests, see the [README.md
+file in the intTests directory](intTests/README.md).
+
+## Other Tests in CI
+
+Although individual developers typically run just the core integration
+tests, our CI system (GitHub Actions) runs several other tests on every
+pull request. These include ensuring that a variety of large proof
+developments, many for the [s2n TLS
+library](https://github.com/aws/s2n-tls), continue to succeed. The
+scripts for running these tests are located in the [s2nTests](s2nTests)
+directory.
+
+# Repository organization and practices
+
+The top-level repository directories are:
+
+* `src` - Source code for the SAWScript interpreter library.
+
+* `saw` - Source for the `saw` executable interpreter for SAWScript.
+
+* `doc` - A tutorial and manual for SAWScript.
+
+* `examples` - Various examples of using SAWScript.
+
+* `intTests` - The central test suite for SAWScript.
+
+* `s2nTests` - Additional tests for SAWScript, confirming that
+  verifications involving the s2n library continue to work.
+
+* `saw-remote-api` - Source for a server that provides a remote API to
+  SAW based on JSON-RPC, and a Python client for that API.
+
+* `saw-core` - Source code for the SAWCore intermediate language used
+  within SAW.
+
+* `saw-core-aig` - A library for translating SAWCore to And-Inverter
+  Graphs.
+
+* `saw-core-coq` - A library for translating SAWCore to Coq's Gallina
+  language.
+
+* `saw-core-sbv` - A library for translating SAWCore predicates to SMT
+  queries using the [SBV](http://leventerkok.github.io/sbv/) library.
+
+* `saw-core-what4` - A library for translating SAWCore predicates to
+  solver queries using the [What4](https://github.com/galoisinc/what4)
+  library.
+
+* `cryptol-saw-core` - A library for translating
+  [Cryptol](https://cryptol.net) code into SAWCore.
+
+* `rme` - A library implementing a Reed-Muller Expansion datatype for
+  representing Boolean formulas.
+
+* `deps` - A location for other dependencies included as Git submodules.
+
+* `crux-mir-comp` - A version of [Crux](https://crux.galois.com/) that
+  can perform modular analysis of Rust code using a form of contracts.
+
+## Branching and merging
+
+Within the `GaloisInc/saw-script` repository, we use a variation on the
+[git-flow
+model](http://nvie.com/posts/a-successful-git-branching-model/) for
+branches and merging with they key difference that our `master` (rather
+than `develop`) branch serves as the cutting edge development branch,
+and our `release-*` (rather than `master`) branches are where only
+pristine, tagged releases are committed.
+
+In short:
+
+- All changes should be developed on branches and then merged into
+  `master` when completed.
+
+- When we reach a feature freeze for a release, we create a new branch
+  prefixed with `release-`, for example `release-0.3`. When the release
+  is made, we merge those changes back into `master` and tag the `HEAD`
+  of the `release` branch.
+
+- If a critical bug emerges in already-released software, we create a
+  branch off of the relevant `release` branch. When the hotfix is
+  complete, we merge those changes back into `master` and add a tag on
+  the `release` branch.
+
+- Merging PRs requires a review from at least one other committer, and
+  requires successful completion of a CI workflow including a wide
+  variety of tests. Branches must be up-to-date with `master` before
+  merging.
+  
+## Using Mergify
+
+Due to the requirement that PRs pass CI and code review and are
+up-to-date with `master` before merging, it can be time-consuming to
+manually manage a large queue of changes to be merged. To help reduce
+this burden we use the [Mergify](https://mergify.io/) tool. It
+automatically queues up CI runs and merges PRs once CI and code review
+have succeeded. To indicate that a PR is ready for Mergify to merge, add
+the `ready-to-merge` label.
+
+# Releases
+
+We take the stability and reliability of our releases very seriously. To
+that end, our release process is based on principles of _automation_,
+_reproducibility_, and _assurance_.
+
+Automation is essential for reducing the possibility of human error. The
+checklist for a successful release is fairly lengthy, and most of the
+steps need not be done by hand. The real points of judgment for an
+individual release are deciding _when_ the codebase is ready to be
+released, not _how_ it is released.
+
+Reproducibility is essential for fixing bugs both in hotfixes and future
+mainline development. If we cannot reproduce the circumstances of a
+release, we might not be able to reproduce bugs that are reported by
+users of that release. Bugs are often very particular about the
+environment where they will arise, so it is critical to make the
+environment of a release consistent.
+
+## Creating releases
+
+The release process is:
+
+1. Make sure the `release-n.n` branch is in a release/ready state, including:
+   - successful build artifacts across all platforms,
+   - successful tests on all test suites, and
+   - an up-to-date [CHANGES.md](CHANGES.md) file.
+1. Create a draft release on GitHub
+1. Make a commit on the `release-n.n` branch updating the version in the
+   `saw-script.cabal` file to `n.n`. This will trigger a build.
+1. Once the build is done, download the release artifacts from the
+   outputs of the build. These are `.zip` files containing `.tar.gz` and
+   `.sig` files.
+1. Unpack the `.zip` files and attach the `.tar.gz` and `.sig` files to
+   the draft release.
+1. Publish the release. This will add a tag to the release branch, as
+   well.
+1. Announce the release and update release-relevant information in the following places:
+
+    - <http://saw.galois.com>
+    - <saw@galois.com>
+    - <saw-users@galois.com>
+    - @galois on Twitter (for major releases)
+
+# Copyright and License
+
+Copyright 2011-2021 [Galois, Inc.](https://galois.com)
+
+Licensed under the BSD 3-Clause License; you may not use this work
+except in compliance with the License. A copy of the License is included
+in the [LICENSE](LICENSE) file.
+
+# Code of Conduct
+
+This project adheres to the [Contributor Covenant code of
+conduct](CODE_OF_CONDUCT.md). By participating, you are expected to
+uphold this code. Please report unacceptable behavior to
+[saw@galois.com](mailto:saw@galois.com).

From 82d62bcd091bc0d51a5dca9c8e87aae6ab22e06a Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Fri, 14 May 2021 11:13:05 -0700
Subject: [PATCH 04/13] Add missing file

---
 CODE_OF_CONDUCT.md | 49 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 CODE_OF_CONDUCT.md

diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
new file mode 100644
index 0000000000..50dcfa0bb6
--- /dev/null
+++ b/CODE_OF_CONDUCT.md
@@ -0,0 +1,49 @@
+# Contributor Code of Conduct
+
+As contributors and maintainers of this project, and in the interest of
+fostering an open and welcoming community, we pledge to respect all people who
+contribute through reporting issues, posting feature requests, updating
+documentation, submitting pull requests or patches, and other activities.
+
+We are committed to making participation in this project a harassment-free
+experience for everyone, regardless of level of experience, gender, gender
+identity and expression, sexual orientation, disability, personal appearance,
+body size, race, ethnicity, age, religion, or nationality.
+
+Examples of unacceptable behavior by participants include:
+
+* The use of sexualized language or imagery
+* Personal attacks
+* Trolling or insulting/derogatory comments
+* Public or private harassment
+* Publishing other's private information, such as physical or electronic
+  addresses, without explicit permission
+* Other unethical or unprofessional conduct
+
+Project maintainers have the right and responsibility to remove, edit, or
+reject comments, commits, code, wiki edits, issues, and other contributions
+that are not aligned to this Code of Conduct, or to ban temporarily or
+permanently any contributor for other behaviors that they deem inappropriate,
+threatening, offensive, or harmful.
+
+By adopting this Code of Conduct, project maintainers commit themselves to
+fairly and consistently applying these principles to every aspect of managing
+this project. Project maintainers who do not follow or enforce the Code of
+Conduct may be permanently removed from the project team.
+
+This Code of Conduct applies both within project spaces and in public spaces
+when an individual is representing the project or its community.
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may
+be reported by contacting a project maintainer at
+[saw@galois.com](mailto:saw@galois.com). All complaints will be reviewed
+and investigated and will result in a response that is deemed necessary
+and appropriate to the circumstances. Maintainers are obligated to
+maintain confidentiality with regard to the reporter of an incident.
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage],
+version 1.3.0, available at
+[http://contributor-covenant.org/version/1/3/0/][version]
+
+[homepage]: http://contributor-covenant.org
+[version]: http://contributor-covenant.org/version/1/3/0/

From 15e1640eda71db12e462495747f5a6e09db1b61e Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Fri, 14 May 2021 16:32:42 -0700
Subject: [PATCH 05/13] Address contrib guidelines comments from @kquick

---
 CONTRIBUTING.md  | 58 +++++++++---------------------------------------
 doc/RELEASING.md | 43 +++++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 47 deletions(-)
 create mode 100644 doc/RELEASING.md

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 56ae3985e8..7164f839e0 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -40,7 +40,7 @@ We recommend building and testing using these files unless your explicit
 goal is to assess compatibility with different library versions. To do
 so, run the following before building or testing:
 
-    ln -s `cabal.GHC-<VER>.config cabal.project.freeze
+    ln -s cabal.GHC-<VER>.config cabal.project.freeze
 
 ## Running and Creating Tests
 
@@ -90,7 +90,7 @@ The top-level repository directories are:
   queries using the [SBV](http://leventerkok.github.io/sbv/) library.
 
 * `saw-core-what4` - A library for translating SAWCore predicates to
-  solver queries using the [What4](https://github.com/galoisinc/what4)
+  solver queries using the [What4](https://github.com/GaloisInc/what4)
   library.
 
 * `cryptol-saw-core` - A library for translating
@@ -133,7 +133,15 @@ In short:
   requires successful completion of a CI workflow including a wide
   variety of tests. Branches must be up-to-date with `master` before
   merging.
-  
+
+- A PR is normally merged by the author of the PR following a review
+  acceptance and valid CI completion. This allows the author to
+  determine when they are fully ready for the merge to be performed. We
+  suggest the use of Mergify (see below) although the merge can also be
+  performed manually, and if you as an author do not have merge
+  permissions, please indicate this in a comment when asking for
+  reviews.
+
 ## Using Mergify
 
 Due to the requirement that PRs pass CI and code review and are
@@ -144,50 +152,6 @@ automatically queues up CI runs and merges PRs once CI and code review
 have succeeded. To indicate that a PR is ready for Mergify to merge, add
 the `ready-to-merge` label.
 
-# Releases
-
-We take the stability and reliability of our releases very seriously. To
-that end, our release process is based on principles of _automation_,
-_reproducibility_, and _assurance_.
-
-Automation is essential for reducing the possibility of human error. The
-checklist for a successful release is fairly lengthy, and most of the
-steps need not be done by hand. The real points of judgment for an
-individual release are deciding _when_ the codebase is ready to be
-released, not _how_ it is released.
-
-Reproducibility is essential for fixing bugs both in hotfixes and future
-mainline development. If we cannot reproduce the circumstances of a
-release, we might not be able to reproduce bugs that are reported by
-users of that release. Bugs are often very particular about the
-environment where they will arise, so it is critical to make the
-environment of a release consistent.
-
-## Creating releases
-
-The release process is:
-
-1. Make sure the `release-n.n` branch is in a release/ready state, including:
-   - successful build artifacts across all platforms,
-   - successful tests on all test suites, and
-   - an up-to-date [CHANGES.md](CHANGES.md) file.
-1. Create a draft release on GitHub
-1. Make a commit on the `release-n.n` branch updating the version in the
-   `saw-script.cabal` file to `n.n`. This will trigger a build.
-1. Once the build is done, download the release artifacts from the
-   outputs of the build. These are `.zip` files containing `.tar.gz` and
-   `.sig` files.
-1. Unpack the `.zip` files and attach the `.tar.gz` and `.sig` files to
-   the draft release.
-1. Publish the release. This will add a tag to the release branch, as
-   well.
-1. Announce the release and update release-relevant information in the following places:
-
-    - <http://saw.galois.com>
-    - <saw@galois.com>
-    - <saw-users@galois.com>
-    - @galois on Twitter (for major releases)
-
 # Copyright and License
 
 Copyright 2011-2021 [Galois, Inc.](https://galois.com)
diff --git a/doc/RELEASING.md b/doc/RELEASING.md
new file mode 100644
index 0000000000..69a9cfbbd9
--- /dev/null
+++ b/doc/RELEASING.md
@@ -0,0 +1,43 @@
+# Releases
+
+We take the stability and reliability of our releases very seriously. To
+that end, our release process is based on principles of _automation_,
+_reproducibility_, and _assurance_.
+
+Automation is essential for reducing the possibility of human error. The
+checklist for a successful release is fairly lengthy, and most of the
+steps need not be done by hand. The real points of judgment for an
+individual release are deciding _when_ the codebase is ready to be
+released, not _how_ it is released.
+
+Reproducibility is essential for fixing bugs both in hotfixes and future
+mainline development. If we cannot reproduce the circumstances of a
+release, we might not be able to reproduce bugs that are reported by
+users of that release. Bugs are often very particular about the
+environment where they will arise, so it is critical to make the
+environment of a release consistent.
+
+## Creating releases
+
+The release process is:
+
+1. Make sure the `release-n.n` branch is in a release/ready state, including:
+   - successful build artifacts across all platforms,
+   - successful tests on all test suites, and
+   - an up-to-date [CHANGES.md](CHANGES.md) file.
+1. Create a draft release on GitHub
+1. Make a commit on the `release-n.n` branch updating the version in the
+   `saw-script.cabal` file to `n.n`. This will trigger a build.
+1. Once the build is done, download the release artifacts from the
+   outputs of the build. These are `.zip` files containing `.tar.gz` and
+   `.sig` files.
+1. Unpack the `.zip` files and attach the `.tar.gz` and `.sig` files to
+   the draft release.
+1. Publish the release. This will add a tag to the release branch, as
+   well.
+1. Announce the release and update release-relevant information in the following places:
+
+    - <http://saw.galois.com>
+    - <saw@galois.com>
+    - <saw-users@galois.com>
+    - @galois on Twitter (for major releases)

From e707b96ceddde56f7786898cc1c09dac498cb9fa Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Fri, 28 May 2021 11:04:36 -0700
Subject: [PATCH 06/13] Remove code of conduct for now

We may put a custom one in place later
---
 CODE_OF_CONDUCT.md | 49 ----------------------------------------------
 1 file changed, 49 deletions(-)
 delete mode 100644 CODE_OF_CONDUCT.md

diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
deleted file mode 100644
index 50dcfa0bb6..0000000000
--- a/CODE_OF_CONDUCT.md
+++ /dev/null
@@ -1,49 +0,0 @@
-# Contributor Code of Conduct
-
-As contributors and maintainers of this project, and in the interest of
-fostering an open and welcoming community, we pledge to respect all people who
-contribute through reporting issues, posting feature requests, updating
-documentation, submitting pull requests or patches, and other activities.
-
-We are committed to making participation in this project a harassment-free
-experience for everyone, regardless of level of experience, gender, gender
-identity and expression, sexual orientation, disability, personal appearance,
-body size, race, ethnicity, age, religion, or nationality.
-
-Examples of unacceptable behavior by participants include:
-
-* The use of sexualized language or imagery
-* Personal attacks
-* Trolling or insulting/derogatory comments
-* Public or private harassment
-* Publishing other's private information, such as physical or electronic
-  addresses, without explicit permission
-* Other unethical or unprofessional conduct
-
-Project maintainers have the right and responsibility to remove, edit, or
-reject comments, commits, code, wiki edits, issues, and other contributions
-that are not aligned to this Code of Conduct, or to ban temporarily or
-permanently any contributor for other behaviors that they deem inappropriate,
-threatening, offensive, or harmful.
-
-By adopting this Code of Conduct, project maintainers commit themselves to
-fairly and consistently applying these principles to every aspect of managing
-this project. Project maintainers who do not follow or enforce the Code of
-Conduct may be permanently removed from the project team.
-
-This Code of Conduct applies both within project spaces and in public spaces
-when an individual is representing the project or its community.
-
-Instances of abusive, harassing, or otherwise unacceptable behavior may
-be reported by contacting a project maintainer at
-[saw@galois.com](mailto:saw@galois.com). All complaints will be reviewed
-and investigated and will result in a response that is deemed necessary
-and appropriate to the circumstances. Maintainers are obligated to
-maintain confidentiality with regard to the reporter of an incident.
-
-This Code of Conduct is adapted from the [Contributor Covenant][homepage],
-version 1.3.0, available at
-[http://contributor-covenant.org/version/1/3/0/][version]
-
-[homepage]: http://contributor-covenant.org
-[version]: http://contributor-covenant.org/version/1/3/0/

From 1ae2adb0c5cc88127f3d223744d9b943b1e8cafc Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Fri, 28 May 2021 14:26:42 -0700
Subject: [PATCH 07/13] Remove dead link to code of conduct

---
 CONTRIBUTING.md | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 7164f839e0..e38339a462 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -159,10 +159,3 @@ Copyright 2011-2021 [Galois, Inc.](https://galois.com)
 Licensed under the BSD 3-Clause License; you may not use this work
 except in compliance with the License. A copy of the License is included
 in the [LICENSE](LICENSE) file.
-
-# Code of Conduct
-
-This project adheres to the [Contributor Covenant code of
-conduct](CODE_OF_CONDUCT.md). By participating, you are expected to
-uphold this code. Please report unacceptable behavior to
-[saw@galois.com](mailto:saw@galois.com).

From 1117b58414e27d7a7a5088488554028e782d18a5 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Fri, 28 May 2021 15:33:20 -0700
Subject: [PATCH 08/13] add explanation string to InternalTacticEvidence

---
 src/SAWScript/Builtins.hs |  2 +-
 src/SAWScript/Proof.hs    | 11 ++++-------
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index c0649ade52..b98e044a3a 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -507,7 +507,7 @@ hoistIfsInGoalPrim =
     do sc <- getSharedContext
        let tac = \sctx g -> hoistIfsInGoal sctx g
        p <- io $ tac sc (goalProp goal)
-       return (p, InternalTacticEvidence tac)
+       return (p, InternalTacticEvidence "hoistIfsInGoal" tac)
 
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 84f09e0902..eca0232298 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -179,15 +179,12 @@ simplifyProp sc ss (Prop tm) =
 
 hoistIfsInGoal :: SharedContext -> Prop -> IO Prop
 hoistIfsInGoal sc p =
-  case asEqTrue pTerm of
+  case asEqTrue (unProp p) of -- peel off eqTrue to avoid getting ite terms above it
     Just t -> do
       tm <- hoistIfs sc t
       eqTm <- scEqTrue sc tm
-      newP <- termToProp sc eqTm
-      return newP
+      termToProp sc eqTm
     Nothing -> fail "hoist_ifs: expected EqTrue"
-  where
-    pTerm = unProp p
 
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will
@@ -356,7 +353,7 @@ data Evidence
     --   evidence is use to check the modified goal.
   | EvalEvidence (Set VarIndex) Evidence
 
-  | InternalTacticEvidence (SharedContext -> Prop -> IO Prop) Evidence
+  | InternalTacticEvidence String (SharedContext -> Prop -> IO Prop) Evidence
 
 -- | The the proposition proved by a given theorem.
 thmProp :: Theorem -> Prop
@@ -603,7 +600,7 @@ checkEvidence sc = check mempty
         do p' <- simplifyProp sc ss p
            check hyps e' p'
 
-      InternalTacticEvidence tac e' ->
+      InternalTacticEvidence _ tac e' ->
         do p' <- tac sc p
            check hyps e' p'
 

From 1c128e1eeefc154d3750e1a092386dc9ce6b6151 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Fri, 28 May 2021 15:47:56 -0700
Subject: [PATCH 09/13] minor

---
 src/SAWScript/Builtins.hs | 5 ++---
 src/SAWScript/Proof.hs    | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index b98e044a3a..285362b435 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -505,9 +505,8 @@ hoistIfsInGoalPrim :: ProofScript ()
 hoistIfsInGoalPrim =
   execTactic $ tacticChange $ \goal ->
     do sc <- getSharedContext
-       let tac = \sctx g -> hoistIfsInGoal sctx g
-       p <- io $ tac sc (goalProp goal)
-       return (p, InternalTacticEvidence "hoistIfsInGoal" tac)
+       p <- io $ hoistIfsInGoal sc (goalProp goal)
+       return (p, InternalTacticEvidence "hoistIfsInGoal" hoistIfsInGoal)
 
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index eca0232298..8d90012982 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -184,7 +184,7 @@ hoistIfsInGoal sc p =
       tm <- hoistIfs sc t
       eqTm <- scEqTrue sc tm
       termToProp sc eqTm
-    Nothing -> fail "hoist_ifs: expected EqTrue"
+    Nothing -> fail "hoistIfsInGoal: expected EqTrue"
 
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will

From 2a8994656fc5020582e1f8bc910bf3e702b277fa Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Fri, 28 May 2021 16:41:16 -0700
Subject: [PATCH 10/13] make work when goal is Pi term

---
 intTests/test_hoist_ifs_in_goal/test.saw | 22 ++++++++++++++++++++++
 intTests/test_hoist_ifs_in_goal/test.sh  |  1 +
 src/SAWScript/Proof.hs                   | 20 +++++++++++++-------
 3 files changed, 36 insertions(+), 7 deletions(-)
 create mode 100644 intTests/test_hoist_ifs_in_goal/test.saw
 create mode 100644 intTests/test_hoist_ifs_in_goal/test.sh

diff --git a/intTests/test_hoist_ifs_in_goal/test.saw b/intTests/test_hoist_ifs_in_goal/test.saw
new file mode 100644
index 0000000000..4c8b44b9c6
--- /dev/null
+++ b/intTests/test_hoist_ifs_in_goal/test.saw
@@ -0,0 +1,22 @@
+enable_experimental;
+
+let {{
+  f : Integer -> Integer
+  f x = undefined
+  g : Integer -> Integer
+  g x = undefined
+}};
+
+let prop = {{ \c x y -> f (if c then g x else g y) == if c then x else y }};
+
+l1 <- prove_print assume_unsat {{ \x -> f (g x) == x }};
+
+prove
+  (do {
+    hoist_ifs_in_goal;
+    simplify (addsimps [l1] empty_ss);
+    w4;
+  })
+  prop;
+
+print "Done";
diff --git a/intTests/test_hoist_ifs_in_goal/test.sh b/intTests/test_hoist_ifs_in_goal/test.sh
new file mode 100644
index 0000000000..0b864017cd
--- /dev/null
+++ b/intTests/test_hoist_ifs_in_goal/test.sh
@@ -0,0 +1 @@
+$SAW test.saw
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 8d90012982..9aee09bcd6 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -178,13 +178,19 @@ simplifyProp sc ss (Prop tm) =
      return (Prop tm')
 
 hoistIfsInGoal :: SharedContext -> Prop -> IO Prop
-hoistIfsInGoal sc p =
-  case asEqTrue (unProp p) of -- peel off eqTrue to avoid getting ite terms above it
-    Just t -> do
-      tm <- hoistIfs sc t
-      eqTm <- scEqTrue sc tm
-      termToProp sc eqTm
-    Nothing -> fail "hoistIfsInGoal: expected EqTrue"
+hoistIfsInGoal sc (Prop p) = do
+  let (args, body) = asPiList p
+  body' <-
+    case asEqTrue body of
+      Just t -> pure t
+      Nothing -> fail "hoistIfsInGoal: expected EqTrue"
+  ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args
+  vars <- traverse (scExtCns sc) ecs
+  t0 <- instantiateVarList sc 0 (reverse vars) body'
+  t1 <- hoistIfs sc t0
+  t2 <- scEqTrue sc t1
+  t3 <- scGeneralizeExts sc ecs t2
+  return (Prop t3)
 
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will

From 00368b5b0da7e130ee96aba5273f98b8f6924745 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Tue, 1 Jun 2021 20:11:43 -0700
Subject: [PATCH 11/13] rm InternalTacticEvidence, add HoistIfsEvidence

---
 src/SAWScript/Builtins.hs | 3 ++-
 src/SAWScript/Proof.hs    | 6 +++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 285362b435..469a7f663a 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -505,8 +505,9 @@ hoistIfsInGoalPrim :: ProofScript ()
 hoistIfsInGoalPrim =
   execTactic $ tacticChange $ \goal ->
     do sc <- getSharedContext
+       let tac = \sctx g -> hoistIfsInGoal sctx g
        p <- io $ hoistIfsInGoal sc (goalProp goal)
-       return (p, InternalTacticEvidence "hoistIfsInGoal" hoistIfsInGoal)
+       return (p, HoistIfsEvidence)
 
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 9aee09bcd6..4aa0667dce 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -359,7 +359,7 @@ data Evidence
     --   evidence is use to check the modified goal.
   | EvalEvidence (Set VarIndex) Evidence
 
-  | InternalTacticEvidence String (SharedContext -> Prop -> IO Prop) Evidence
+  | HoistIfsEvidence Evidence
 
 -- | The the proposition proved by a given theorem.
 thmProp :: Theorem -> Prop
@@ -606,8 +606,8 @@ checkEvidence sc = check mempty
         do p' <- simplifyProp sc ss p
            check hyps e' p'
 
-      InternalTacticEvidence _ tac e' ->
-        do p' <- tac sc p
+      HoistIfsEvidence e' ->
+        do p' <- hoistIfsInGoal sc p
            check hyps e' p'
 
       EvalEvidence vars e' ->

From 630469afe5b2b0976647d49c86d5f91848bae311 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Wed, 2 Jun 2021 09:18:26 -0700
Subject: [PATCH 12/13] remove spurious line

---
 src/SAWScript/Builtins.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 469a7f663a..4fab621a68 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -505,7 +505,6 @@ hoistIfsInGoalPrim :: ProofScript ()
 hoistIfsInGoalPrim =
   execTactic $ tacticChange $ \goal ->
     do sc <- getSharedContext
-       let tac = \sctx g -> hoistIfsInGoal sctx g
        p <- io $ hoistIfsInGoal sc (goalProp goal)
        return (p, HoistIfsEvidence)
 

From 519266123cfea7d5947c04747ec2b1ba50b8df10 Mon Sep 17 00:00:00 2001
From: Giuliano Losa <giuliano@galois.com>
Date: Wed, 2 Jun 2021 14:59:37 -0700
Subject: [PATCH 13/13] add comment for HoistIfsEvidence

---
 src/SAWScript/Proof.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 4aa0667dce..07e37d7a0e 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -359,6 +359,8 @@ data Evidence
     --   evidence is use to check the modified goal.
   | EvalEvidence (Set VarIndex) Evidence
 
+    -- | This type of evidence is used to modify a goal to prove by applying
+    -- 'hoistIfsInGoal'.
   | HoistIfsEvidence Evidence
 
 -- | The the proposition proved by a given theorem.