From b71b75aa7f9e4db0575b01cf25b7ad6dd88abff4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 4 Jun 2020 20:03:10 +0100 Subject: Finished main proof with small assumptions --- src/translation/HTLgenproof.v | 123 +++++++++++++++++++++++++++++++----------- src/translation/HTLgenspec.v | 5 +- src/verilog/AssocMap.v | 19 ++++--- src/verilog/HTL.v | 60 ++++++++++++++++----- src/verilog/Verilog.v | 9 ++-- 5 files changed, 157 insertions(+), 59 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index e719070..204451c 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -21,7 +21,7 @@ From compcert Require Import Globalenvs. From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap. From coqup Require HTL Verilog. -Import AssocMapNotation. +Local Open Scope assocmap. Hint Resolve Smallstep.forward_simulation_plus : htlproof. Hint Resolve AssocMap.gss : htlproof. @@ -37,25 +37,40 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := - forall st assoc, - s = HTL.State m st assoc -> + forall st assoc res, + s = HTL.State res m st assoc -> assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st). Hint Unfold state_st_wf : htlproof. +Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop := +| match_stacks_nil : + match_stacks nil nil +| match_stacks_cons : + forall cs lr r f sp pc rs m assoc + (TF : tr_module f m) + (ST: match_stacks cs lr) + (MA: match_assocmaps f rs assoc), + match_stacks (RTL.Stackframe r f sp pc rs :: cs) + (HTL.Stackframe r m pc assoc :: lr). + Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st +| match_state : forall assoc sf f sp rs mem m st res (MASSOC : match_assocmaps f rs assoc) (TF : tr_module f m) - (WF : state_st_wf m (HTL.State m st assoc)), + (WF : state_st_wf m (HTL.State res m st assoc)) + (MS : match_stacks sf res), match_states (RTL.State sf f sp st rs mem) - (HTL.State m st assoc) -| match_returnstate : forall v v' stack m, - val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v m) (HTL.Returnstate v') + (HTL.State res m st assoc) +| match_returnstate : + forall + v v' stack m res + (MS : match_stacks stack res), + val_value_lessdef v v' -> + match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v') | match_initial_call : - forall f m m0 st + forall f m m0 (TF : tr_module f m), - match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.State m st empty_assocmap). + match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := @@ -156,6 +171,20 @@ Ltac unfold_func H := | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) end. +Lemma init_reg_assoc_empty : + forall f l, + match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). +Proof. + induction l; simpl; constructor; intros. + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. + + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. +Qed. + Section CORRECTNESS. Variable prog : RTL.program. @@ -234,10 +263,10 @@ Section CORRECTNESS. *) Definition transl_instr_prop (instr : RTL.instruction) : Prop := - forall m assoc fin rtrn st stmt trans, + forall m assoc fin rtrn st stmt trans res, tr_instr fin rtrn st instr stmt trans -> exists assoc', - HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). + HTL.step tge (HTL.State res m st assoc) Events.E0 (HTL.State res m st assoc'). Theorem transl_step_correct: forall (S1 : RTL.state) t S2, @@ -329,7 +358,7 @@ Section CORRECTNESS. (* match_states *) assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. rewrite <- H1. - constructor. apply rs0. + constructor. unfold_merge. apply regs_lessdef_add_match. constructor. @@ -343,6 +372,7 @@ Section CORRECTNESS. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + assumption. - econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -367,7 +397,7 @@ Section CORRECTNESS. destruct b. rewrite assumption_32bit. - apply match_state. apply rs0. + apply match_state. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. assumption. @@ -375,8 +405,9 @@ Section CORRECTNESS. unfold state_st_wf. intros. inversion H1. subst. unfold_merge. apply AssocMap.gss. + assumption. rewrite assumption_32bit. - apply match_state. apply rs0. + apply match_state. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. assumption. @@ -384,6 +415,7 @@ Section CORRECTNESS. unfold state_st_wf. intros. inversion H1. subst. unfold_merge. apply AssocMap.gss. + assumption. - (* Return *) econstructor. split. @@ -400,7 +432,7 @@ Section CORRECTNESS. trivial. rewrite AssocMap.gso. rewrite AssocMap.gso. - unfold state_st_wf in WF. apply WF. trivial. + unfold state_st_wf in WF. eapply WF. trivial. apply st_greater_than_res. apply st_greater_than_res. trivial. apply HTL.step_finish. @@ -410,10 +442,10 @@ Section CORRECTNESS. apply finish_not_return. apply AssocMap.gss. rewrite Events.E0_left. trivial. - - constructor. constructor. - - destruct (assoc!r) eqn:?. - inversion H11. subst. + constructor. + assumption. + constructor. + - inversion H11. subst. econstructor. split. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. @@ -422,14 +454,11 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. econstructor; simpl; trivial. - apply Verilog.erun_Vvar. - rewrite AssocMap.gso. - apply Heqo. apply not_eq_sym. apply finish_not_res. + apply Verilog.erun_Vvar. trivial. unfold_merge. - trivial. rewrite AssocMap.gso. rewrite AssocMap.gso. - unfold state_st_wf in WF. apply WF. trivial. + unfold state_st_wf in WF. eapply WF. trivial. apply st_greater_than_res. apply st_greater_than_res. trivial. apply HTL.step_finish. @@ -440,8 +469,38 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. trivial. - constructor. simpl. - Admitted. + constructor. assumption. simpl. inversion MASSOC. subst. + unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. + apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. + apply st_greater_than_res. + + - inversion MSTATE; subst. inversion TF; subst. + econstructor. split. apply Smallstep.plus_one. + eapply HTL.step_call. + + constructor. apply regs_lessdef_add_greater. + apply greater_than_max_func. + apply init_reg_assoc_empty. assumption. unfold state_st_wf. + intros. inv H1. apply AssocMap.gss. constructor. + - inversion MSTATE; subst. inversion MS; subst. econstructor. + split. apply Smallstep.plus_one. + constructor. + + constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto. + apply regs_lessdef_add_greater. apply greater_than_max_func. auto. + + unfold state_st_wf. intros. inv H. rewrite AssocMap.gso. + rewrite AssocMap.gss. trivial. apply st_greater_than_res. + + Unshelve. + exact (AssocMap.empty value). + exact (AssocMap.empty value). + exact (ZToValue 32 0). + exact (AssocMap.empty value). + exact (AssocMap.empty value). + exact (AssocMap.empty value). + exact (AssocMap.empty value). + Qed. Hint Resolve transl_step_correct : htlproof. Lemma transl_initial_states : @@ -467,12 +526,14 @@ Section CORRECTNESS. Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : - forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog)) + forall (s1 : Smallstep.state (RTL.semantics prog)) + (s2 : Smallstep.state (HTL.semantics tprog)) (r : Integers.Int.int), match_states s1 s2 -> - Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. + Smallstep.final_state (RTL.semantics prog) s1 r -> + Smallstep.final_state (HTL.semantics tprog) s2 r. Proof. - intros. inv H0. inv H. inv H4. constructor. trivial. + intros. inv H0. inv H. inv H4. inv MS. constructor. trivial. Qed. Hint Resolve transl_final_states : htlproof. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index ca069c1..afc6f72 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -300,15 +300,14 @@ Proof. * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; [ discriminate | apply H9 ]. * inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. - eapply in_map with (f := fst) in H9. contradiction. + eapply in_map with (f := fst) in H9; contradiction. * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; [ discriminate | apply H9 ]. * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; [ discriminate | apply H9 ]. * inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor. - eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H9. contradiction. + eapply translate_instr_tr_op. apply EQ1. eapply in_map with (f := fst) in H9. contradiction. * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; [ discriminate | apply H9 ]. diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 88b13a6..5d531d5 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -202,9 +202,16 @@ Ltac unfold_merge := unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); rewrite AssocMapExt.merge_base_1. -Module AssocMapNotation. - Notation "a ! b" := (AssocMap.get b a) (at level 1). - Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). - Notation "a # b" := (find_assocmap 32 b a) (at level 1). - Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). -End AssocMapNotation. +Declare Scope assocmap. +Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap. +Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap. +Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap. +Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap. +Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap. + +Local Open Scope assocmap. +Lemma find_get_assocmap : + forall assoc r v, + assoc ! r = Some v -> + assoc # r = v. +Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index bf38b29..82378b3 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -30,6 +30,8 @@ hardware-like layout that is still similar to the register transfer language instantiations and that we now describe a state machine instead of a control-flow graph. *) +Local Open Scope assocmap. + Definition reg := positive. Definition node := positive. @@ -51,21 +53,42 @@ Definition fundef := AST.fundef module. Definition program := AST.program fundef unit. +Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl') + | _, _ => empty_assocmap + end. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (assoc : assocmap), + stackframe. + Inductive state : Type := | State : - forall (m : module) + forall (stack : list stackframe) + (m : module) (st : node) - (assoc : assocmap), - state -| Returnstate : forall v : value, state. + (assoc : assocmap), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval, + forall g m st ctrl data assoc0 assoc1 assoc2 + assoc3 nbassoc0 nbassoc1 f stval pstval sf, m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f @@ -79,27 +102,38 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := assoc3 = merge_assocmap nbassoc1 assoc2 -> assoc3!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> - step g (State m st assoc0) t (State m pstval assoc3) + step g (State sf m st assoc0) Events.E0 (State sf m pstval assoc3) | step_finish : - forall g t m st assoc retval, + forall g m st assoc retval sf, assoc!(m.(mod_finish)) = Some (1'h"1") -> assoc!(m.(mod_return)) = Some retval -> - step g (State m st assoc) t (Returnstate retval). + step g (State sf m st assoc) Events.E0 (Returnstate sf retval) +| step_call : + forall g m args res, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) + (init_regs args m.(mod_params)))) +| step_return : + forall g m assoc i r sf pc mst, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc assoc :: sf) i) Events.E0 + (State sf m pc ((assoc # mst <- (posToValue 32 pc)) # r <- i)). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b m0 st m, + | initial_state_intro: forall b m0 m, let ge := Globalenvs.Genv.globalenv p in Globalenvs.Genv.init_mem p = Some m0 -> Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> - st = m.(mod_entrypoint) -> - initial_state p (State m st empty_assocmap). + initial_state p (Callstate nil m nil). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, retvali = valueToInt retval -> - final_state (Returnstate retval) retvali. + final_state (Returnstate nil retval) retvali. Definition semantics (m : program) := - Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index ce7ddd9..cccdf9a 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -32,7 +32,8 @@ From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. Import HexNotationValue. -Import AssocMapNotation. + +Local Open Scope assocmap. Definition reg : Type := positive. Definition node : Type := positive. @@ -246,12 +247,8 @@ Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop := expr_runp fext assoc (Vlit v) v | erun_Vvar : forall fext assoc v r, - assoc!r = Some v -> + assoc#r = v -> expr_runp fext assoc (Vvar r) v - | erun_Vvar_empty : - forall fext assoc r sz, - assoc!r = None -> - expr_runp fext assoc (Vvar r) (ZToValue sz 0) | erun_Vinputvar : forall fext assoc r v, fext!r = Some v -> -- cgit