Add RTLBlock intermediate language

1 files changed, 368 insertions, 0 deletions

diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
new file mode 100644
index 0000000..9abbd4b
--- /dev/null
+++ b/src/hls/Veriloggenproof.v
@@ -0,0 +1,368 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 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/>.
+ *)
+
+From compcert Require Import Smallstep Linking Integers Globalenvs.
+From vericert Require HTL.
+From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
+Require Import Lia.
+
+Local Open Scope assocmap.
+
+Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
+  match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.
+
+Lemma transf_program_match:
+  forall prog, match_prog prog (transl_program prog).
+Proof.
+  intros. eapply match_transform_program_contextual. auto.
+Qed.
+
+Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
+| match_stack :
+    forall res m pc reg_assoc arr_assoc hstk vstk,
+      match_stacks hstk vstk ->
+      match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
+                   (Stackframe res (transl_module m) pc
+                                       reg_assoc arr_assoc :: vstk)
+| match_stack_nil : match_stacks nil nil.
+
+Inductive match_states : HTL.state -> state -> Prop :=
+| match_state :
+    forall m st reg_assoc arr_assoc hstk vstk,
+      match_stacks hstk vstk ->
+      match_states (HTL.State hstk m st reg_assoc arr_assoc)
+                   (State vstk (transl_module m) st reg_assoc arr_assoc)
+| match_returnstate :
+    forall v hstk vstk,
+      match_stacks hstk vstk ->
+      match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
+| match_initial_call :
+    forall m,
+      match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
+
+Lemma Vlit_inj :
+  forall a b, Vlit a = Vlit b -> a = b.
+Proof. inversion 1. trivial. Qed.
+
+Lemma posToValue_inj :
+  forall a b,
+    0 <= Z.pos a <= Int.max_unsigned ->
+    0 <= Z.pos b <= Int.max_unsigned ->
+    posToValue a = posToValue b ->
+    a = b.
+Proof.
+  intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id.
+  rewrite <- Int.unsigned_repr at 1; try assumption.
+  symmetry.
+  rewrite <- Int.unsigned_repr at 1; try assumption.
+  unfold posToValue in *. rewrite H1; auto.
+Qed.
+
+Lemma valueToPos_inj :
+  forall a b,
+    0 < Int.unsigned a ->
+    0 < Int.unsigned b ->
+    valueToPos a = valueToPos b ->
+    a = b.
+Proof.
+  intros. unfold valueToPos in *.
+  rewrite <- Int.repr_unsigned at 1.
+  rewrite <- Int.repr_unsigned.
+  apply Pos2Z.inj_iff in H1.
+  rewrite Z2Pos.id in H1; auto.
+  rewrite Z2Pos.id in H1; auto.
+  rewrite H1. auto.
+Qed.
+
+Lemma unsigned_posToValue_le :
+  forall p,
+    Z.pos p <= Int.max_unsigned ->
+    0 < Int.unsigned (posToValue p).
+Proof.
+  intros. unfold posToValue. rewrite Int.unsigned_repr; lia.
+Qed.
+
+Lemma transl_list_fun_fst :
+  forall p1 p2 a b,
+    0 <= Z.pos p1 <= Int.max_unsigned ->
+    0 <= Z.pos p2 <= Int.max_unsigned ->
+    transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
+    (p1, a) = (p2, b).
+Proof.
+  intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1.
+  destruct H1. rewrite H2. apply Vlit_inj in H1.
+  apply posToValue_inj in H1; try assumption.
+  rewrite H1; auto.
+Qed.
+
+Lemma Zle_relax :
+  forall p q r,
+  p < q <= r ->
+  p <= q <= r.
+Proof. lia. Qed.
+Hint Resolve Zle_relax : verilogproof.
+
+Lemma transl_in :
+  forall l p,
+  0 <= Z.pos p <= Int.max_unsigned ->
+  (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+  In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
+  In p (map fst l).
+Proof.
+  induction l.
+  - simplify. auto.
+  - intros. destruct a. simplify. destruct (peq p0 p); auto.
+    right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction.
+    auto with verilogproof.
+    apply IHl; auto.
+Qed.
+
+Lemma transl_notin :
+  forall l p,
+    0 <= Z.pos p <= Int.max_unsigned ->
+    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+    ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)).
+Proof.
+  induction l; auto. intros. destruct a. unfold not in *. intros.
+  simplify.
+  destruct (peq p0 p). apply H1. auto. apply H1.
+  unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H.
+  contradiction.
+  auto with verilogproof. auto.
+  right. apply transl_in; auto.
+Qed.
+
+Lemma transl_norepet :
+  forall l,
+    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+    list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)).
+Proof.
+  induction l.
+  - intros. simpl. apply list_norepet_nil.
+  - destruct a. intros. simpl. apply list_norepet_cons.
+    inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto.
+    intros. apply H. destruct (peq p0 p); subst; simplify; auto.
+    assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto.
+    simplify. inv H0. assumption.
+Qed.
+
+Lemma transl_list_correct :
+  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
+    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+    list_norepet (List.map fst l) ->
+    asr!ev = Some v ->
+    (forall p s,
+        In (p, s) l ->
+        v = posToValue p ->
+        stmnt_runp f
+                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
+                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
+                   s
+                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
+                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
+        stmnt_runp f
+                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
+                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
+                   (Vcase (Vvar ev) (transl_list l) (Some Vskip))
+                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
+                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
+Proof.
+  induction l as [| a l IHl].
+  - contradiction.
+  - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.
+    destruct a as [p' s']. simplify.
+    destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match.
+    constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
+    rewrite ASSOC. trivial. constructor. auto.
+    inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption.
+    inv NOREP. eapply in_map with (f := fst) in INV. contradiction.
+
+    eapply stmnt_runp_Vcase_nomatch. constructor. simplify.
+    unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
+    trivial. constructor. unfold not. intros. apply n. apply posToValue_inj.
+    apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction.
+    eapply in_map with (f := fst) in H0. auto.
+    apply Zle_relax. apply BOUND; auto. auto.
+
+    eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
+    trivial. assumption.
+Qed.
+Hint Resolve transl_list_correct : verilogproof.
+
+Lemma pc_wf :
+  forall A m p v,
+  (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
+  m!p = Some v ->
+  0 <= Z.pos p <= Int.max_unsigned.
+Proof.
+  intros A m p v LT S. apply Zle_relax. apply LT.
+  apply AssocMap.elements_correct in S. remember (p, v) as x.
+  exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto.
+Qed.
+
+Lemma mis_stepp_decl :
+  forall l asr asa f,
+    mis_stepp f asr asa (map Vdeclaration l) asr asa.
+Proof.
+  induction l.
+  - intros. constructor.
+  - intros. simplify. econstructor. constructor. auto.
+Qed.
+Hint Resolve mis_stepp_decl : verilogproof.
+
+Section CORRECTNESS.
+
+  Variable prog: HTL.program.
+  Variable tprog: program.
+
+  Hypothesis TRANSL : match_prog prog tprog.
+
+  Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Hint Resolve symbols_preserved : verilogproof.
+
+  Lemma function_ptr_translated:
+    forall (b: Values.block) (f: HTL.fundef),
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf,
+        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf.
+  Proof.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+  Hint Resolve function_ptr_translated : verilogproof.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: HTL.fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transl_fundef f = tf.
+  Proof.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+  Hint Resolve functions_translated : verilogproof.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof.
+    intros. eapply (Genv.senv_match TRANSL).
+  Qed.
+  Hint Resolve senv_preserved : verilogproof.
+
+  Theorem transl_step_correct :
+    forall (S1 : HTL.state) t S2,
+      HTL.step ge S1 t S2 ->
+      forall (R1 : state),
+        match_states S1 R1 ->
+        exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+    induction 1; intros R1 MSTATE; inv MSTATE.
+    - econstructor; split. apply Smallstep.plus_one. econstructor.
+      assumption. assumption. eassumption. apply valueToPos_posToValue.
+      split. lia.
+      eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
+      split. lia. apply HP. eassumption. eassumption.
+      econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
+      simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
+      rewrite H. trivial.
+
+      econstructor. simpl. auto. auto.
+
+      eapply transl_list_correct.
+      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto.
+      apply Maps.PTree.elements_keys_norepet. eassumption.
+      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
+           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption.
+           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
+           destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption. trivial.
+      }
+      apply Maps.PTree.elements_correct. eassumption. eassumption.
+
+      econstructor. econstructor.
+
+      eapply transl_list_correct.
+      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto.
+      apply Maps.PTree.elements_keys_norepet. eassumption.
+      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
+           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption.
+           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
+           destruct HP as [HP _].
+           split. lia. apply HP. eassumption. eassumption. trivial.
+      }
+      apply Maps.PTree.elements_correct. eassumption. eassumption.
+
+      apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto.
+      rewrite valueToPos_posToValue. constructor; assumption. lia.
+
+    - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
+      constructor; assumption.
+    - econstructor; split. apply Smallstep.plus_one. constructor.
+
+      constructor. constructor.
+    - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
+
+      apply match_state. assumption.
+  Qed.
+  Hint Resolve transl_step_correct : verilogproof.
+
+  Lemma transl_initial_states :
+    forall s1 : Smallstep.state (HTL.semantics prog),
+      Smallstep.initial_state (HTL.semantics prog) s1 ->
+      exists s2 : Smallstep.state (Verilog.semantics tprog),
+        Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2.
+  Proof.
+    induction 1.
+    econstructor; split. econstructor.
+    apply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved.
+    replace (AST.prog_main tprog) with (AST.prog_main prog); eauto.
+    symmetry; eapply Linking.match_program_main; eauto.
+    exploit function_ptr_translated; eauto. intros [tf [A B]].
+    inv B. eauto.
+    constructor.
+  Qed.
+  Hint Resolve transl_initial_states : verilogproof.
+
+  Lemma transl_final_states :
+    forall (s1 : Smallstep.state (HTL.semantics prog))
+           (s2 : Smallstep.state (Verilog.semantics tprog))
+           (r : Integers.Int.int),
+      match_states s1 s2 ->
+      Smallstep.final_state (HTL.semantics prog) s1 r ->
+      Smallstep.final_state (Verilog.semantics tprog) s2 r.
+  Proof.
+    intros. inv H0. inv H. inv H3. constructor. reflexivity.
+  Qed.
+  Hint Resolve transl_final_states : verilogproof.
+
+  Theorem transf_program_correct:
+    forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
+  Proof.
+    eapply Smallstep.forward_simulation_plus; eauto with verilogproof.
+    apply senv_preserved.
+  Qed.
+
+End CORRECTNESS.