diff options
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 154 |
1 files changed, 110 insertions, 44 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 9a7e272..fc7af6b 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1,4 +1,4 @@ - (* +(* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * 2020 James Pollard <j@mes.dev> @@ -40,24 +40,24 @@ Require Import Lia. Local Open Scope assocmap. -Hint Resolve Smallstep.forward_simulation_plus : htlproof. -Hint Resolve AssocMap.gss : htlproof. -Hint Resolve AssocMap.gso : htlproof. +#[local] Hint Resolve Smallstep.forward_simulation_plus : htlproof. +#[local] Hint Resolve AssocMap.gss : htlproof. +#[local] Hint Resolve AssocMap.gso : htlproof. -Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. +#[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := match_assocmap : forall f rs am, (forall r, Ple r (RTL.max_reg_function f) -> val_value_lessdef (Registers.Regmap.get r rs) am#r) -> match_assocmaps f rs am. -Hint Constructors match_assocmaps : htlproof. +#[local] Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := forall st asa asr res, s = HTL.State res m st asa asr -> asa!(m.(HTL.mod_st)) = Some (posToValue st). -Hint Unfold state_st_wf : htlproof. +#[local] Hint Unfold state_st_wf : htlproof. Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : Verilog.assocmap_arr -> Prop := @@ -133,7 +133,7 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := forall f m m0 (TF : tr_module f m), match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). -Hint Constructors match_states : htlproof. +#[local] Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ @@ -187,7 +187,7 @@ Proof. apply Pos.le_lt_trans with _ _ n in H2. unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. Qed. -Hint Resolve regs_lessdef_add_greater : htlproof. +#[local] Hint Resolve regs_lessdef_add_greater : htlproof. Lemma regs_lessdef_add_match : forall f rs am r v v', @@ -206,7 +206,7 @@ Proof. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite AssocMap.gso; eauto. Qed. -Hint Resolve regs_lessdef_add_match : htlproof. +#[local] Hint Resolve regs_lessdef_add_match : htlproof. Lemma list_combine_none : forall n l, @@ -348,7 +348,7 @@ Proof. eexists. unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. Qed. -Hint Resolve arr_lookup_some : htlproof. +#[local] Hint Resolve arr_lookup_some : htlproof. Section CORRECTNESS. @@ -392,7 +392,7 @@ Section CORRECTNESS. Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof (Genv.senv_transf_partial TRANSL'). - Hint Resolve senv_preserved : htlproof. + #[local] Hint Resolve senv_preserved : htlproof. Lemma ptrofs_inj : forall a b, @@ -1030,6 +1030,7 @@ Section CORRECTNESS. Ltac tac0 := match goal with + | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge @@ -1103,7 +1104,7 @@ Section CORRECTNESS. Unshelve. exact tt. Qed. - Hint Resolve transl_inop_correct : htlproof. + #[local] Hint Resolve transl_inop_correct : htlproof. Lemma transl_iop_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -1155,7 +1156,7 @@ Section CORRECTNESS. unfold Ple in HPle. lia. Unshelve. exact tt. Qed. - Hint Resolve transl_iop_correct : htlproof. + #[local] Hint Resolve transl_iop_correct : htlproof. Ltac tac := repeat match goal with @@ -1628,7 +1629,7 @@ Section CORRECTNESS. exact (Values.Vint (Int.repr 0)). exact tt. Qed. - Hint Resolve transl_iload_correct : htlproof. + #[local] Hint Resolve transl_iload_correct : htlproof. Lemma transl_istore_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -1701,7 +1702,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -1735,11 +1736,21 @@ Section CORRECTNESS. crush. unfold Verilog.merge_arrs. - rewrite AssocMap.gcombine. - 2: { reflexivity. } + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. + erewrite Verilog.merge_arr_empty2. unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. rewrite AssocMap.gss. unfold Verilog.merge_arr. + setoid_rewrite H7. + reflexivity. + + rewrite AssocMap.gcombine by reflexivity. + unfold Verilog.merge_arr. + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. rewrite AssocMap.gss. setoid_rewrite H7. reflexivity. @@ -1747,12 +1758,23 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. unfold arr_repeat. crush. + symmetry. apply list_repeat_len. rewrite <- array_set_len. unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. + rewrite H4. + apply list_repeat_len. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. crush. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. crush. + rewrite H4. + apply list_repeat_len. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. @@ -1981,7 +2003,7 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2014,11 +2036,21 @@ Section CORRECTNESS. crush. unfold Verilog.merge_arrs. - rewrite AssocMap.gcombine. - 2: { reflexivity. } + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. + erewrite Verilog.merge_arr_empty2. unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gcombine by reflexivity. rewrite AssocMap.gss. + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H7. + reflexivity. + + rewrite AssocMap.gcombine by reflexivity. unfold Verilog.merge_arr. + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. rewrite AssocMap.gss. setoid_rewrite H7. reflexivity. @@ -2026,12 +2058,23 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. unfold arr_repeat. crush. + symmetry. apply list_repeat_len. rewrite <- array_set_len. unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. + rewrite H4. + apply list_repeat_len. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. crush. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. crush. + rewrite H4. + apply list_repeat_len. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) (Integers.Ptrofs.of_int @@ -2229,7 +2272,7 @@ Section CORRECTNESS. eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. - all: crush. + all: try constructor; crush. (** State Lookup *) unfold Verilog.merge_regs. @@ -2263,11 +2306,21 @@ Section CORRECTNESS. crush. unfold Verilog.merge_arrs. - rewrite AssocMap.gcombine. - 2: { reflexivity. } + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. + erewrite Verilog.merge_arr_empty2. unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gcombine by reflexivity. + rewrite AssocMap.gss. rewrite AssocMap.gss. unfold Verilog.merge_arr. + setoid_rewrite H7. + reflexivity. + + rewrite AssocMap.gcombine by reflexivity. + unfold Verilog.merge_arr. + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. rewrite AssocMap.gss. setoid_rewrite H7. reflexivity. @@ -2275,12 +2328,23 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. unfold arr_repeat. crush. + symmetry. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. crush. + rewrite H4. + apply list_repeat_len. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. crush. apply list_repeat_len. rewrite <- array_set_len. unfold arr_repeat. crush. - rewrite list_repeat_len. - rewrite H4. reflexivity. + rewrite H4. + apply list_repeat_len. remember i0 as OFFSET. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). @@ -2435,7 +2499,7 @@ Section CORRECTNESS. exact tt. exact (Values.Vint (Int.repr 0)). Qed. - Hint Resolve transl_istore_correct : htlproof. + #[local] Hint Resolve transl_istore_correct : htlproof. Lemma transl_icond_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -2463,7 +2527,7 @@ Section CORRECTNESS. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2480,7 +2544,7 @@ Section CORRECTNESS. eapply eval_cond_correct; eauto. intros. intros. eapply RTL.max_reg_function_use. apply H22. auto. econstructor. auto. - simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. inv MARR. inv CONST. @@ -2489,7 +2553,7 @@ Section CORRECTNESS. Unshelve. all: exact tt. Qed. - Hint Resolve transl_icond_correct : htlproof. + #[local] Hint Resolve transl_icond_correct : htlproof. (*Lemma transl_ijumptable_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -2505,7 +2569,7 @@ Section CORRECTNESS. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - Hint Resolve transl_ijumptable_correct : htlproof.*) + #[local] Hint Resolve transl_ijumptable_correct : htlproof.*) Lemma transl_ireturn_correct: forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) @@ -2535,10 +2599,10 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. - constructor. constructor. + constructor. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. - destruct wf as [HCTRL HDATA]. apply HCTRL. + destruct wf1 as [HCTRL HDATA]. apply HCTRL. apply AssocMapExt.elements_iff. eexists. match goal with H: control ! pc = Some _ |- _ => apply H end. @@ -2564,16 +2628,18 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. constructor. constructor. constructor. constructor. constructor. + constructor. unfold state_st_wf in WF; big_tac; eauto. - destruct wf as [HCTRL HDATA]. apply HCTRL. + destruct wf1 as [HCTRL HDATA]. apply HCTRL. apply AssocMapExt.elements_iff. eexists. match goal with H: control ! pc = Some _ |- _ => apply H end. apply HTL.step_finish. unfold Verilog.merge_regs. unfold_merge. + unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. simpl; lia. apply AssocMap.gss. @@ -2591,7 +2657,7 @@ Section CORRECTNESS. Unshelve. all: constructor. Qed. - Hint Resolve transl_ireturn_correct : htlproof. + #[local] Hint Resolve transl_ireturn_correct : htlproof. Lemma transl_callstate_correct: forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) @@ -2699,7 +2765,7 @@ Section CORRECTNESS. Opaque Mem.load. Opaque Mem.store. Qed. - Hint Resolve transl_callstate_correct : htlproof. + #[local] Hint Resolve transl_callstate_correct : htlproof. Lemma transl_returnstate_correct: forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) @@ -2713,7 +2779,7 @@ Section CORRECTNESS. intros res0 f sp pc rs s vres m R1 MSTATE. inversion MSTATE. inversion MF. Qed. - Hint Resolve transl_returnstate_correct : htlproof. + #[local] Hint Resolve transl_returnstate_correct : htlproof. Lemma option_inv : forall A x y, @@ -2773,7 +2839,7 @@ Section CORRECTNESS. rewrite <- H6. setoid_rewrite <- A. trivial. trivial. inv H7. assumption. Qed. - Hint Resolve transl_initial_states : htlproof. + #[local] Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : forall (s1 : Smallstep.state (RTL.semantics prog)) @@ -2785,7 +2851,7 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. Qed. - Hint Resolve transl_final_states : htlproof. + #[local] Hint Resolve transl_final_states : htlproof. Theorem transl_step_correct: forall (S1 : RTL.state) t S2, @@ -2796,7 +2862,7 @@ Section CORRECTNESS. Proof. induction 1; eauto with htlproof; (intros; inv_state). Qed. - Hint Resolve transl_step_correct : htlproof. + #[local] Hint Resolve transl_step_correct : htlproof. Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). |