From 4f65a83e13eff9119edb98683864b946a0947f76 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 Jul 2020 13:26:02 +0100 Subject: No addmitted in Veriloggenproof However, there may have been breaking changes to HTLgenproof. --- src/translation/HTLgen.v | 85 ++++++++++---- src/translation/HTLgenproof.v | 1 - src/translation/Veriloggenproof.v | 239 +++++++++++++++++++++++++++----------- src/verilog/HTL.v | 20 ++-- 4 files changed, 245 insertions(+), 100 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 1977f65..e02d759 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -402,7 +402,7 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) then ret (Vvari stack (Vbinop Vdivu (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (ZToValue 4))) + (Vlit (ZToValue 4)))) else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in @@ -510,32 +510,67 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz Pos.max m pc) m 1%positive. + +Lemma max_pc_map_sound: + forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). +Proof. + intros until i. unfold max_pc_function. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. xomega. + apply Ple_trans with a. auto. xomega. +Qed. + +Lemma max_pc_wf : + forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + map_well_formed m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + Definition transf_module (f: function) : mon module := if stack_correct f.(fn_stacksize) then - do fin <- create_reg (Some Voutput) 1; - do rtrn <- create_reg (Some Voutput) 32; - do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); - do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); - do start <- create_reg (Some Vinput) 1; - do rst <- create_reg (Some Vinput) 1; - do clk <- create_reg (Some Vinput) 1; - do current_state <- get; - ret (mkmodule - f.(RTL.fn_params) - current_state.(st_datapath) - current_state.(st_controllogic) - f.(fn_entrypoint) - current_state.(st_st) - stack - stack_len - fin - rtrn - start - rst - clk - current_state.(st_scldecls) - current_state.(st_arrdecls)) + do fin <- create_reg (Some Voutput) 1; + do rtrn <- create_reg (Some Voutput) 32; + do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); + do start <- create_reg (Some Vinput) 1; + do rst <- create_reg (Some Vinput) 1; + do clk <- create_reg (Some Vinput) 1; + do current_state <- get; + match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end else error (Errors.msg "Stack size misalignment."). Definition max_state (f: function) : state := diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 82d4cfc..305c14f 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -342,7 +342,6 @@ Section CORRECTNESS. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Lemma functions_translated: forall (v: Values.val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index ee0aa64..5b467a7 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -From compcert Require Import Smallstep Linking Integers. +From compcert Require Import Smallstep Linking Integers Globalenvs. From coqup Require HTL. From coqup Require Import Coquplib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. @@ -89,6 +89,14 @@ Proof. 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 -> @@ -102,10 +110,17 @@ Proof. 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) -> + (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. @@ -113,13 +128,14 @@ Proof. - 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) -> + (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. @@ -127,24 +143,88 @@ Proof. 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. - apply H0; auto. auto. + 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) -> + (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 H. simplify; auto. + 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. @@ -152,58 +232,42 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. - 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' |}). + 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. - 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 BOUND. right. inv IN. inv H0; contradiction. eapply in_map with (f := fst) in H0. auto. - apply BOUND; auto. auto. - - eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. - trivial. assumption. + 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 mis_stepp_decl : - forall l asr asa f, - mis_stepp f asr asa (map Vdeclaration l) asr asa. + 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. - induction l. - - intros. constructor. - - intros. simplify. econstructor. constructor. auto. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. Qed. + Hint Resolve functions_translated : verilogproof. - Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : genv := Globalenvs.Genv.globalenv tprog. + 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, @@ -214,7 +278,10 @@ Section CORRECTNESS. Proof. induction 1; intros R1 MSTATE; inv MSTATE. - econstructor; split. apply Smallstep.plus_one. econstructor. - assumption. assumption. eassumption. trivial. + 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. @@ -222,25 +289,33 @@ Section CORRECTNESS. econstructor. simpl. auto. auto. eapply transl_list_correct. - assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_controllogic m))) - -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto. + 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. assert (0 < Int.unsigned ist) by admit; auto. - admit. rewrite valueToPos_posToValue. trivial. admit. } + 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. - assert (forall p0 : positive, In p0 (map fst (Maps.PTree.elements (HTL.mod_datapath m))) - -> 0 <= Z.pos p0 <= Int.max_unsigned) by admit; auto. + 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. assert (0 < Int.unsigned ist) by admit; auto. - admit. rewrite valueToPos_posToValue. trivial. admit. } + 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. - constructor; assumption. + rewrite valueToPos_posToValue. constructor; assumption. lia. - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. constructor; assumption. @@ -250,12 +325,44 @@ Section CORRECTNESS. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. apply match_state. assumption. - Admitted. + 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). - Admitted. - + Proof. + eapply Smallstep.forward_simulation_plus; eauto with verilogproof. + apply senv_preserved. + Qed. End CORRECTNESS. - diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index a7a6ecc..3ba5b59 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -36,6 +36,11 @@ Definition node := positive. Definition datapath := PTree.t Verilog.stmnt. Definition controllogic := PTree.t Verilog.stmnt. +Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := + forall p0 : positive, + In p0 (map fst (Maps.PTree.elements m)) -> + Z.pos p0 <= Integers.Int.max_unsigned. + Record module: Type := mkmodule { mod_params : list reg; @@ -52,6 +57,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); }. Definition fundef := AST.fundef module. @@ -97,16 +103,15 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g m st sf ctrl data ist + forall g m st sf ctrl data asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 asr' asa' - f stval pstval, + f pstval, asr!(mod_reset m) = Some (ZToValue 0) -> asr!(mod_finish m) = Some (ZToValue 0) -> - asr!(m.(mod_st)) = Some ist -> - valueToPos ist = st -> + asr!(m.(mod_st)) = Some (posToValue st) -> m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f @@ -115,8 +120,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> - basr1!(m.(mod_st)) = Some ist -> - valueToPos ist = st -> + basr1!(m.(mod_st)) = Some (posToValue st) -> Verilog.stmnt_runp f (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) @@ -125,8 +129,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (Verilog.mkassociations basa2 nasa2) -> asr' = Verilog.merge_regs nasr2 basr2 -> asa' = Verilog.merge_arrs nasa2 basa2 -> - asr'!(m.(mod_st)) = Some stval -> - valueToPos stval = pstval -> + asr'!(m.(mod_st)) = Some (posToValue pstval) -> + Z.pos pstval <= Integers.Int.max_unsigned -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : forall g m st asr asa retval sf, -- cgit