From ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 14:03:40 +0100 Subject: Add RTLBlock intermediate language --- src/hls/Veriloggenproof.v | 368 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 368 insertions(+) create mode 100644 src/hls/Veriloggenproof.v (limited to 'src/hls/Veriloggenproof.v') 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 + * + * 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 . + *) + +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. -- cgit