Add proof using to ifconversionproof

3 files changed, 30 insertions, 171 deletions

diff --git a/README.md b/README.md
deleted file mode 100644
index b45a5ab..0000000
--- a/README.md
+++ /dev/null
@@ -1,147 +0,0 @@
-- [Features](#features)
-  - [Building](#building)
-    - [Downloading Vericert and CompCert](#downloading-compcert)
-    - [Setting up Nix](#setting-up-nix)
-    - [Makefile build](#makefile-build)
-  - [Running](#running)
-  - [Citation](#org28fad40)
-  - [License](#org5eb199f)
-
-<a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a>
-
-<p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a>&nbsp;<a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p>
-
-A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [CompCert](https://github.com/AbsInt/CompCert). This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert&rsquo;s C semantics, removing the need to check the resulting hardware for behavioural correctness.
-
-
-<a id="features"></a>
-
-# Features
-
-Currently all proofs of the following features have been completed.
-
--   all int operations,
--   non-recursive function calls,
--   local arrays and pointers
--   control-flow structures such as if-statements, for-loops, etc&#x2026;
-
-
-<a id="building"></a>
-
-# Building
-
-To build Vericert, the provided [Makefile](file:///Makefile) can be used. External dependencies are needed to build the project, which can be pulled in automatically with [nix](https://nixos.org/nix/) using the provided [default.nix](file:///default.nix) and [shell.nix](file:///shell.nix) files.
-
-The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:
-
--   [Coq](https://coq.inria.fr/): theorem prover that is used to also program the HLS tool.
--   [OCaml](https://ocaml.org/): the OCaml compiler to compile the extracted files.
--   [dune](https://github.com/ocaml/dune): build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
--   [menhir](http://gallium.inria.fr/~fpottier/menhir/): parser generator for ocaml.
--   [findlib](https://github.com/ocaml/ocamlfind) to find installed OCaml libraries.
--   [GCC](https://gcc.gnu.org/): compiler to help build CompCert.
-
-These dependencies can be installed manually, or automatically through Nix.
-
-
-<a id="downloading-compcert"></a>
-
-## Downloading Vericert and CompCert
-
-CompCert is added as a submodule in the `lib/CompCert` directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, and check it out at the correct revision, you can run:
-
-```shell
-git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert
-```
-
-If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded and the correct branch is checked out:
-
-```shell
-git checkout v1.2.2
-git submodule update --init
-```
-
-
-<a id="setting-up-nix"></a>
-
-## Setting up Nix
-
-Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.
-
-To open a shell which includes all the necessary dependencies, one can use:
-
-```shell
-nix-shell
-```
-
-which will open a shell that has all the dependencies loaded.
-
-
-<a id="makefile-build"></a>
-
-## Makefile build
-
-If the dependencies were installed manually, or if one is in the `nix-shell`, the project can be built by running:
-
-```shell
-make -j8
-```
-
-and installed locally, or under the `PREFIX` location using:
-
-```shell
-  make install
-```
-
-Which will install the binary in `./bin/vericert` by default. However, this can be changed by changing the `PREFIX` environment variable, in which case the binary will be installed in `$PREFIX/bin/vericert`.
-
-
-<a id="running"></a>
-
-# Running
-
-To test out `vericert` you can try the following examples which are in the test folder using the following:
-
-```shell
-./bin/vericert test/loop.c -o loop.v
-./bin/vericert test/conditional.c -o conditional.v
-./bin/vericert test/add.c -o add.v
-```
-
-
-<a id="org28fad40"></a>
-
-# Citation
-
-If you use Vericert in any way, please cite it using our [OOPSLA&rsquo;21 paper](https://yannherklotz.com/papers/fvhls_oopsla21.pdf):
-
-```bibtex
-@inproceedings{herklotz21_fvhls,
-  author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
-  title = {Formal Verification of High-Level Synthesis},
-  year = {2021},
-  number = {OOPSLA},
-  numpages = {30},
-  month = {11},
-  journal = {Proc. ACM Program. Lang.},
-  volume = {5},
-  publisher = {Association for Computing Machinery},
-  address = {New York, NY, USA},
-  doi = {10.1145/3485494}
-}
-```
-
-
-<a id="org5eb199f"></a>
-
-# License
-
-This project is licensed under [GPLv3](https://www.gnu.org/licenses/gpl-3.0.en.html). The license can be seen in [LICENSE](LICENSE).
-
-The following external code and its license is present in this repository:
-
--   **[src/pipelining](src/pipelining):** MIT
-
-```text
-Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
-```
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index 5cb87ba..70d5fe3 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -179,9 +179,15 @@ Qed.
 Lemma transf_spec_correct_in :
   forall l pc c b c' z,
     (fold_left (fun s n => if_convert c s (fst n) (snd n)) l b) = c' ->
-    b ! pc = Some z \/ (exists pc' y, c ! pc' = Some y /\ decide_if_convert y = true /\ b ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z))) ->
+    b ! pc = Some z \/ (exists pc' y,
+                          c ! pc' = Some y
+                          /\ decide_if_convert y = true
+                          /\ b ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z))) ->
     c ! pc = Some z ->
-    c' ! pc = Some z \/ exists pc' y, c ! pc' = Some y /\ decide_if_convert y = true /\ c' ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z)).
+    c' ! pc = Some z \/ exists pc' y,
+                          c ! pc' = Some y
+                          /\ decide_if_convert y = true
+                          /\ c' ! pc = Some (snd (replace_section (wrap_unit (if_convert_block pc' y)) tt z)).
 Proof.
   induction l; crush. inv H0. tauto.
   simplify. right. eauto.
@@ -448,7 +454,7 @@ Section CORRECTNESS.
         (plus step tge s1 t s2 \/
            star step tge s1 t s2 /\ ltof _ measure b' b) /\
           match_states b' s s2.
-  Proof. intros; simplify. do 3 econstructor; eauto. Qed.
+  Proof using. intros; simplify. do 3 econstructor; eauto. Qed.
 
   Lemma sim_plus :
     forall s1 b t s,
@@ -457,13 +463,13 @@ Section CORRECTNESS.
         (plus step tge s1 t s2 \/
            star step tge s1 t s2 /\ ltof _ measure b' b) /\
           match_states b' s s2.
-  Proof. intros; simplify. do 3 econstructor; eauto. Qed.
+  Proof using. intros; simplify. do 3 econstructor; eauto. Qed.
 
   Lemma step_instr :
     forall sp s1 s2 a,
       step_instr ge sp s1 a s2 ->
       step_instr tge sp s1 a s2.
-  Proof.
+  Proof using TRANSL.
     inversion 1; subst; econstructor; eauto.
     - now rewrite <- eval_op_eq.
     - now rewrite <- eval_addressing_eq.
@@ -474,7 +480,7 @@ Section CORRECTNESS.
     forall bb sp rs pr m rs' pr' m' cf,
       SeqBB.step ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
       SeqBB.step tge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf).
-  Proof.
+  Proof using TRANSL.
     induction bb; crush; inv H.
     - econstructor; eauto. apply step_instr; eassumption.
       destruct state'. eapply IHbb; eauto.
@@ -541,7 +547,7 @@ Section CORRECTNESS.
 
   Definition wf_trans_dec :
     forall p b, {wf_trans p b} + {~ wf_trans p b}.
-  Proof.
+  Proof using.
     intros; destruct (wf_transition_block_opt p b) eqn:?.
     left. apply wf_transition_block_opt_prop; auto.
     right. unfold not; intros. apply wf_transition_block_opt_prop in H.
@@ -550,7 +556,7 @@ Section CORRECTNESS.
 
   Definition cf_wf_dec :
     forall p b a pc, {a = RBgoto pc /\ wf_trans p b} + {a <> RBgoto pc \/ ~ wf_trans p b}.
-  Proof.
+  Proof using.
     intros; destruct (cf_dec a pc); destruct (wf_trans_dec p b); tauto.
   Qed.
 
@@ -558,7 +564,7 @@ Section CORRECTNESS.
     forall n pc' x b',
       RBgoto n <> RBgoto pc' \/ ~ wf_trans x b' ->
       (pc' =? n) && wf_transition_block_opt x b' = false.
-  Proof.
+  Proof using.
     inversion 1; subst; simplify.
     destruct (peq n pc'); subst; [exfalso; auto|]; [].
     apply Pos.eqb_neq in n0. rewrite Pos.eqb_sym in n0.
@@ -573,7 +579,7 @@ Section CORRECTNESS.
       step_list2 (Gible.step_instr ge) sp i'' b i' ->
       step_list2 (Gible.step_instr ge) sp i a i'' ->
       step_list2 (Gible.step_instr ge) sp i (a ++ b) i'.
-  Proof.
+  Proof using.
     induction a; crush.
     - inv H0; auto.
     - inv H0. econstructor.
@@ -583,7 +589,7 @@ Section CORRECTNESS.
   Lemma map_if_convert_None :
     forall b',
       map (map_if_convert None) b' = b'.
-  Proof.
+  Proof using.
     induction b'; crush.
     rewrite IHb'; f_equal. destruct a; crush; destruct o; auto.
   Qed.
@@ -593,7 +599,7 @@ Section CORRECTNESS.
       truthy pr x ->
       truthy pr p ->
       truthy pr (combine_pred x p).
-  Proof.
+  Proof using.
     intros.
     inv H; inv H0; cbn [combine_pred] in *; constructor; auto;
     rewrite eval_predf_Pand; apply andb_true_intro; auto.
@@ -604,7 +610,7 @@ Section CORRECTNESS.
     forall i' a x,
       instr_falsy (is_ps i') a ->
       instr_falsy (is_ps i') (map_if_convert x a).
-  Proof.
+  Proof using.
     inversion 1; subst; destruct x; crush; constructor; rewrite eval_predf_Pand;
       auto using andb_false_intro2.
   Qed.
@@ -615,7 +621,7 @@ Section CORRECTNESS.
       truthy (is_ps i) x ->
       Gible.step_instr ge sp (Iexec i) a i' ->
       Gible.step_instr ge sp (Iexec i) (map_if_convert x a) i'.
-  Proof.
+  Proof using.
     inversion 2; subst; crush;
       try (solve [econstructor; eauto]).
   Qed.
@@ -624,7 +630,7 @@ Section CORRECTNESS.
     forall A B (ge: Genv.t A B) sp i a x,
       eval_predf (is_ps i) x = false ->
       Gible.step_instr ge sp (Iexec i) (map_if_convert (Some x) a) (Iexec i).
-  Proof.
+  Proof using.
     intros; destruct a; constructor; cbn; destruct o; constructor; auto;
       rewrite eval_predf_Pand; rewrite H; auto.
   Qed.
@@ -633,7 +639,7 @@ Section CORRECTNESS.
     forall A B (ge: Genv.t A B) sp b' p i0,
       eval_predf (is_ps i0) p = false ->
       step_list2 (Gible.step_instr ge) sp (Iexec i0) (map (map_if_convert (Some p)) b') (Iexec i0).
-  Proof.
+  Proof using.
     induction b'; crush; try constructor.
     econstructor; eauto.
     apply map_falsy_instr; auto.
@@ -643,7 +649,7 @@ Section CORRECTNESS.
     forall A B (ge: Genv.t A B) sp a pc' b' i i0,
       Gible.step_instr ge sp (Iexec i) a (Iexec i0) ->
       step_list2 (Gible.step_instr ge) sp (Iexec i) (if_convert_block pc' b' a) (Iexec i0).
-  Proof with (simplify; try (solve [econstructor; eauto; constructor])).
+  Proof with (simplify; try (solve [econstructor; eauto; constructor])) using.
     inversion 1; subst... destruct a... destruct c...
     destruct ((pc' =? n) && wf_transition_block_opt o b') eqn:?...
     apply wf_transition_block_opt_prop in H1. inv H1. inv H4.
@@ -658,7 +664,7 @@ Section CORRECTNESS.
       exists b rb,
         tb = b ++ RBexit x cf :: rb
         /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i').
-  Proof.
+  Proof using.
     induction x0; simplify.
     - inv H1. inv H. exists nil. exists b'0.
       split; [|constructor]. rewrite app_nil_l.
@@ -679,7 +685,7 @@ Section CORRECTNESS.
       ~ In p0 (predicate_use p1) ->
       eval_predf pr p1 = b1 ->
       eval_predf pr # p0 <- b0 p1 = b1.
-  Proof.
+  Proof using.
     induction p1; crush.
     - destruct_match. inv Heqp1. simplify.
       unfold not in *.
@@ -707,7 +713,7 @@ Section CORRECTNESS.
       In a b ->
       truthy (is_ps i) p ->
       truthy (is_ps i') p.
-  Proof.
+  Proof using.
     inversion 1; subst; auto; intros;
     cbn [ is_ps ] in *.
     inv H0; constructor; [].
@@ -719,7 +725,7 @@ Section CORRECTNESS.
     forall x a b',
       wf_trans x (a :: b') ->
       wf_trans x b'.
-  Proof. inversion 1; subst; cbn in *; constructor; eauto. Qed.
+  Proof using. inversion 1; subst; cbn in *; constructor; eauto. Qed.
 
   Lemma map_truthy_step:
     forall A B (ge: Genv.t A B) b' sp i x i' c,
@@ -727,7 +733,7 @@ Section CORRECTNESS.
       wf_trans x b' ->
       SeqBB.step tge sp (Iexec i) b' (Iterm i' c) ->
       SeqBB.step tge sp (Iexec i) (map (map_if_convert x) b') (Iterm i' c).
-  Proof.
+  Proof using.
     induction b'; crush.
     inv H1.
     - econstructor.
@@ -746,7 +752,7 @@ Section CORRECTNESS.
       exists b rb,
         tb = b ++ (map (map_if_convert x) b') ++ rb
         /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i').
-  Proof.
+  Proof using.
     induction x0; simplify.
     - inv H1. inv H. exists nil. exists b'0.
       split; [|constructor]. rewrite app_nil_l.
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 6067719..8dbd0f6 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -178,7 +178,7 @@ Proof. crush. Qed.
   { equiv := sat_equiv; }.
 
 #[global]
- Instance PandProper : Proper (SetoidClass.equiv ==> SetoidClass.equiv ==> SetoidClass.equiv) Pand.
+ Instance PandProper : Proper (equiv ==> equiv ==> equiv) Pand.
 Proof.
   unfold Proper. simplify. unfold "==>".
   intros.