From 9542b92e85931b53e48107807af83d021e05a01d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Apr 2020 14:58:54 +0100 Subject: Add partial proof of well formed state --- src/translation/Veriloggen.v | 160 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 136 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 8ecb2ac..6b43d55 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -23,6 +23,8 @@ From coqup Require Import Verilog Coquplib. From compcert Require Errors Op AST Integers Maps. From compcert Require Import RTL. +Notation "a ! b" := (PositiveMap.find b a) (at level 1). + Definition node : Type := positive. Definition reg : Type := positive. Definition ident : Type := positive. @@ -31,27 +33,89 @@ Inductive statetrans : Type := | StateGoto (p : node) | StateCond (c : expr) (t f : node). +Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) := + forall (n: node), + Plt n fs \/ stm!n = None. + +Definition states_have_transitions (stm: PositiveMap.t stmnt) (st: PositiveMap.t statetrans) := + forall (n: node), + (forall x, stm!n = Some x -> exists y, st!n = Some y) + /\ (forall x, st!n = Some x -> exists y, stm!n = Some y). + Record state: Type := mkstate { - st_freshreg : reg; - st_freshstate : node; - st_stm : PositiveMap.t stmnt; - st_statetrans : PositiveMap.t statetrans; - st_decl : PositiveMap.t nat; + st_freshreg: reg; + st_freshstate: node; + st_stm: PositiveMap.t stmnt; + st_statetrans: PositiveMap.t statetrans; + st_decl: PositiveMap.t nat; + st_wf: valid_freshstate st_stm st_freshstate + /\ states_have_transitions st_stm st_statetrans; }. -(** Map from initial register allocations to new allocations. *) -Definition mapping: Type := PositiveMap.t reg. +Remark init_state_valid_freshstate: + valid_freshstate (PositiveMap.empty stmnt) 1%positive. +Proof. intros. right. apply PositiveMap.gempty. Qed. + +Remark init_state_states_have_transitions: + states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). +Proof. + unfold states_have_transitions. + split; intros; rewrite PositiveMap.gempty in H; discriminate. +Qed. + +Remark init_state_wf: + valid_freshstate (PositiveMap.empty stmnt) 1%positive + /\ states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). +Proof. split; intros. apply init_state_valid_freshstate. apply init_state_states_have_transitions. Qed. Definition init_state : state := mkstate 1%positive 1%positive (PositiveMap.empty stmnt) (PositiveMap.empty statetrans) - (PositiveMap.empty nat). + (PositiveMap.empty nat) + init_state_wf. + +Inductive state_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, + s1.(st_stm)!n = None \/ s2.(st_stm)!n = s1.(st_stm)!n) -> + (forall n, + s1.(st_statetrans)!n = None + \/ s2.(st_statetrans)!n = s1.(st_statetrans)!n) -> + state_incr s1 s2. + +Lemma state_incr_refl: + forall s, state_incr s s. +Proof. intros. apply state_incr_intro; + try (apply Ple_refl); + try (intros; right; reflexivity). +Qed. + +Lemma state_incr_trans: + forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. +Proof. + intros. inv H. inv H0. apply state_incr_intro. + - apply Ple_trans with (st_freshreg s2); assumption. + - apply Ple_trans with (st_freshstate s2); assumption. + - intros. destruct H3 with n. + + left. assumption. + + destruct H6 with n. + * rewrite <- H0. left. assumption. + * right. rewrite <- H0. apply H8. + - intros. destruct H4 with n. + + left. assumption. + + destruct H7 with n. + * rewrite <- H0. left. assumption. + * right. rewrite <- H0. apply H8. +Qed. Inductive res (A: Type) (s: state): Type := | Error : Errors.errmsg -> res A s -| OK : A -> forall (_ : state), res A s. +| OK : A -> forall (s' : state), state_incr s s' -> res A s. Arguments OK [A s]. Arguments Error [A s]. @@ -59,16 +123,16 @@ Arguments Error [A s]. Definition mon (A: Type) : Type := forall (s: state), res A s. Definition ret {A: Type} (x: A) : mon A := - fun (s : state) => OK x s. + fun (s : state) => OK x s (state_incr_refl s). Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := fun (s : state) => match f s with | Error msg => Error msg - | OK a s' => + | OK a s' i => match g a s' with | Error msg => Error msg - | OK b s'' => OK b s'' + | OK b s'' i' => OK b s'' (state_incr_trans s s' s'' i i') end end. @@ -83,24 +147,25 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s : state) => match f s with - | OK a s' => OK a s' + | OK a s' i => OK a s' i | Error _ => g s end. Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: state) => Error err. -Definition get : mon state := fun s => OK s s. +Definition get : mon state := fun s => OK s s (state_incr_refl s). -Definition set (s: state) : mon unit := fun _ => OK tt s. +Definition set (s: state) (i: forall s', state_incr s' s) : mon unit := + fun s' => OK tt s (i s'). Definition run_mon {A: Type} (s: state) (m: mon A): Errors.res A := match m s with - | OK a s' => Errors.OK a + | OK a s' i => Errors.OK a | Error err => Errors.Error err end. -Definition map_state (f: state -> state): mon state := - fun s => let s' := f s in OK s' s'. +Definition map_state (f: state -> state) (i: forall s, state_incr s (f s)): mon state := + fun s => let s' := f s in OK s' s' (i s). Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) := match l with @@ -204,13 +269,60 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other") end. -Definition add_instr (n : node) (n' : node) (st : stmnt) : mon node := +Remark add_instr_valid_freshstate: + forall (s: state) (n: node) (st: stmnt), + Plt n (st_freshstate s) -> + valid_freshstate (PositiveMap.add n st s.(st_stm)) (st_freshstate s). +Proof. + unfold valid_freshstate. intros. + case (peq n0 n); intro. + subst n0. left. assumption. + rewrite PositiveMap.gso. + apply (st_wf s). assumption. +Qed. + +Remark add_instr_states_have_transitions: + forall (s: state) (n n': node) (st: stmnt), + states_have_transitions + (PositiveMap.add n st s.(st_stm)) + (PositiveMap.add n (StateGoto n') s.(st_statetrans)). +Proof. + unfold states_have_transitions. split; intros. + - case (peq n0 n); intro. + subst. exists (StateGoto n'). apply PositiveMap.gss. + rewrite PositiveMap.gso. rewrite PositiveMap.gso in H. + assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1. + destruct H1 with n0. apply H2 with x. assumption. assumption. assumption. + - case (peq n0 n); intro. + subst. exists st. apply PositiveMap.gss. + rewrite PositiveMap.gso. rewrite PositiveMap.gso in H. + assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1. + destruct H1 with n0. apply H3 with x. assumption. assumption. assumption. +Qed. + +Remark add_instr_state_wf: + forall (s: state) (n n': node) (st: stmnt) (LT: Plt n (st_freshstate s)), + valid_freshstate (PositiveMap.add n st (st_stm s)) (st_freshstate s) + /\ states_have_transitions + (PositiveMap.add n st s.(st_stm)) + (PositiveMap.add n (StateGoto n') s.(st_statetrans)). +Proof. + split; intros. apply add_instr_valid_freshstate. assumption. + apply add_instr_states_have_transitions. +Qed. + +Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := fun s => - OK n' (mkstate s.(st_freshreg) - (Pos.max (Pos.succ n) s.(st_freshstate)) - (PositiveMap.add n st s.(st_stm)) - (PositiveMap.add n (StateGoto n') s.(st_statetrans)) - s.(st_decl)). + match plt n (st_freshstate s) with + | left LT => + OK tt (mkstate s.(st_freshreg) + (st_freshstate s) + (PositiveMap.add n st s.(st_stm)) + (PositiveMap.add n (StateGoto n') s.(st_statetrans)) + s.(st_decl) + (add_instr_state_wf s n n' st LT)) + | _ => Error (Errors.msg "Veriloggen.add_instr") + end. Definition add_reg (r: reg) (s: state) : state := mkstate (Pos.max (Pos.succ r) s.(st_freshreg)) -- cgit