Work on specification of RTLBlock generation

4 files changed, 258 insertions, 162 deletions

diff --git a/src/common/DecEq.v b/src/common/DecEq.v
new file mode 100644
index 0000000..e9d716f
--- /dev/null
+++ b/src/common/DecEq.v
@@ -0,0 +1,150 @@
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+====================
+Decidable Equalities
+====================
+|*)
+
+Require compcert.backend.RTL.
+Require Import compcert.common.AST.
+Require Import compcert.lib.Maps.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Floats.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.RTLBlock.
+
+Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
+Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
+Proof.
+  generalize comparison_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  decide equality.
+Defined.
+
+Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
+Proof.
+  generalize Int.eq_dec; intro.
+  generalize AST.ident_eq; intro.
+  generalize Z.eq_dec; intro.
+  generalize Ptrofs.eq_dec; intro.
+  decide equality.
+Defined.
+
+Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
+Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
+Proof.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  generalize Float.eq_dec; intro.
+  generalize Float32.eq_dec; intro.
+  generalize AST.ident_eq; intro.
+  generalize condition_eq; intro.
+  generalize addressing_eq; intro.
+  generalize typ_eq; intro.
+  decide equality.
+Defined.
+
+Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
+
+Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
+Proof.
+  generalize typ_eq; intro.
+  decide equality.
+Defined.
+
+Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
+Proof.
+  generalize typ_eq; intro.
+  decide equality.
+Defined.
+
+Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
+Proof.
+  repeat decide equality.
+Defined.
+
+Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
+Proof.
+  generalize operation_eq; intro.
+  decide equality.
+Defined.
+
+Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intros.
+  decide equality.
+Defined.
+
+Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
+Proof.
+  repeat decide equality.
+Defined.
+
+Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intro.
+  generalize typ_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize memory_chunk_eq; intro.
+  generalize addressing_eq; intro.
+  generalize operation_eq; intro.
+  generalize condition_eq; intro.
+  generalize signature_eq; intro.
+  generalize list_operation_eq; intro.
+  generalize list_pos_eq; intro.
+  generalize AST.ident_eq; intro.
+  repeat decide equality.
+Defined.
+
+Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
+Proof.
+  generalize Pos.eq_dec; intro.
+  generalize typ_eq; intro.
+  generalize Int.eq_dec; intro.
+  generalize Int64.eq_dec; intro.
+  generalize Float.eq_dec; intro.
+  generalize Float32.eq_dec; intro.
+  generalize Ptrofs.eq_dec; intro.
+  generalize memory_chunk_eq; intro.
+  generalize addressing_eq; intro.
+  generalize operation_eq; intro.
+  generalize condition_eq; intro.
+  generalize signature_eq; intro.
+  generalize list_operation_eq; intro.
+  generalize list_pos_eq; intro.
+  generalize AST.ident_eq; intro.
+  repeat decide equality.
+Defined.
+
+Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
+  if eqd a b then true else false.
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index d308366..cd23da3 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -46,6 +46,9 @@ Require Import Vericertlib.
 Definition node := positive.
 
 (*|
+.. index::
+   triple: definition; RTLBlockInstr; instruction
+
 Instruction Definition
 ======================
 
@@ -67,6 +70,9 @@ Inductive instr : Type :=
   option pred_op -> condition -> list reg -> predicate -> instr.
 
 (*|
+.. index::
+   triple: definition; RTLBlockInstr; control-flow instruction
+
 Control-Flow Instruction Definition
 ===================================
 
@@ -312,6 +318,14 @@ Section RELSEM.
   | eval_pred_none:
       forall i i', eval_pred None i i' i.
 
+(*|
+.. index::
+   triple: semantics; RTLBlockInstr; instruction
+
+Step Instruction
+=============================
+|*)
+
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
       forall sp ist,
@@ -346,6 +360,14 @@ Section RELSEM.
       step_instr sp (mk_instr_state rs pr m)
                     (RBsetpred p' c args p) ist.
 
+(*|
+.. index::
+   triple: semantics; RTLBlockInstr; control-flow instruction
+
+Step Control-Flow Instruction
+=============================
+|*)
+
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
     forall s f sp rs m res fd ros sig args pc pc' pr,
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index 5d7376d..a29709b 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -1,20 +1,25 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+===========
+RTLBlockgen
+===========
+|*)
 
 Require compcert.backend.RTL.
 Require Import compcert.common.AST.
@@ -22,137 +27,18 @@ Require Import compcert.lib.Maps.
 Require Import compcert.lib.Integers.
 Require Import compcert.lib.Floats.
 
+Require Import vericert.common.DecEq.
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 
 #[local] Open Scope positive.
 
-Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
-Proof.
-  generalize comparison_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  decide equality.
-Defined.
-
-Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
-Proof.
-  generalize Int.eq_dec; intro.
-  generalize AST.ident_eq; intro.
-  generalize Z.eq_dec; intro.
-  generalize Ptrofs.eq_dec; intro.
-  decide equality.
-Defined.
-
-Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
-Proof.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  generalize AST.ident_eq; intro.
-  generalize condition_eq; intro.
-  generalize addressing_eq; intro.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
-Proof.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
-Proof.
-  generalize typ_eq; intro.
-  decide equality.
-Defined.
-
-Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
-Proof.
-  repeat decide equality.
-Defined.
-
-Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
-Proof.
-  generalize operation_eq; intro.
-  decide equality.
-Defined.
-
-Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intros.
-  decide equality.
-Defined.
-
-Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
-Proof.
-  repeat decide equality.
-Defined.
-
-Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intro.
-  generalize typ_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize memory_chunk_eq; intro.
-  generalize addressing_eq; intro.
-  generalize operation_eq; intro.
-  generalize condition_eq; intro.
-  generalize signature_eq; intro.
-  generalize list_operation_eq; intro.
-  generalize list_pos_eq; intro.
-  generalize AST.ident_eq; intro.
-  repeat decide equality.
-Defined.
-
-Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
-Proof.
-  generalize Pos.eq_dec; intro.
-  generalize typ_eq; intro.
-  generalize Int.eq_dec; intro.
-  generalize Int64.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  generalize Ptrofs.eq_dec; intro.
-  generalize memory_chunk_eq; intro.
-  generalize addressing_eq; intro.
-  generalize operation_eq; intro.
-  generalize condition_eq; intro.
-  generalize signature_eq; intro.
-  generalize list_operation_eq; intro.
-  generalize list_pos_eq; intro.
-  generalize AST.ident_eq; intro.
-  repeat decide equality.
-Defined.
-
-Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
-  if eqd a b then true else false.
-
 Parameter partition : RTL.function -> Errors.res function.
 
 (*|
 ``find_block max nodes index``: Does not need to be sorted, because we use
 filter and the max fold function to find the desired element.
-
-    .. coq::
 |*)
 
 Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive :=
@@ -160,6 +46,17 @@ Definition find_block (max: positive) (nodes: list positive) (index: positive) :
 
 (*Compute find_block 100 (2::94::48::39::19::nil) 40.*)
 
+(*|
+.. index::
+   triple: abstract interpretation; check instruction; RTLBlockgen
+
+Check Instruction
+=================
+
+Check if an instruction is a standard instruction that should be in a basic
+block.
+|*)
+
 Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) :=
   match istr, istr' with
   | RTL.Inop n', RBnop => (n' + 1 =? n)
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index 4568185..1544b5f 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -1,33 +1,41 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
+
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
+
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
+
+   You should have received a copy of the GNU General Public License
+   along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+================
+RTLBlockgenproof
+================
+|*)
 
 Require compcert.backend.RTL.
 Require Import compcert.common.AST.
 Require Import compcert.lib.Maps.
 Require Import compcert.common.Errors.
 
+Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLBlockgen.
 
+#[local] Open Scope positive.
+
 (*|
 Defining a find block specification
------------------------------------
+===================================
 
 Basically, it should be able to find the location of the block without using the
 ``find_block`` function, so that this is more useful for the proofs.  There are
@@ -40,15 +48,34 @@ various different types of options that could come up though:
 For case number 1, there should exist a value in the list of instructions, such
 that the instructions match exactly, and the indices match as well.  In the
 original code, this instruction must have been going from the current node to
-the node - 1.  For case number 2, there should be an instruction at the right
-index again, however, this time there will also be a ``goto`` instruction in the
-control-flow part of the basic block.
+the node - 1.
+
+For case number 2, there should be an instruction at the right index again,
+however, this time there will also be a ``goto`` instruction in the control-flow
+part of the basic block.
+
+For case number 3, there should be a ``nop`` instruction in the basic block, and
+then the equivalent control-flow instruction ending the basic block.
 |*)
 
-(*Definition find_block_spec (c1: RTL.code) (c2: code) :=
-  forall x i,
-    c1 ! x = Some i ->
-    exists y li, c2 ! y = Some li /\ nth_error li.(bb_body) ((Pos.to_nat y) - (Pos.to_nat x))%nat = Some i.
+Parameter find_block_spec : code -> node -> RTL.instruction -> node -> Prop.
+
+Definition find_instr_spec (c: code) (n: node) (i: RTL.instruction) (n': node) (i': instr) :=
+    find_block_spec c n i n'
+    /\ exists il,
+      c ! n' = Some il
+      /\ nth_error il.(bb_body) (Pos.to_nat n - Pos.to_nat n')%nat = Some i'.
+
+Inductive transl_code_spec (c: RTL.code) (tc: code) :=
+| transl_code_standard_bb :
+  forall x x' i i',
+    c ! x = Some i ->
+    find_instr_spec tc x i x' i' ->
+    check_instr x i i' = true ->
+    transl_code_spec c tc
+| transl_code_standard_goto :
+  forall
+.
 
 Inductive match_states : RTL.state -> RTLBlock.state -> Prop :=
 | match_state :