diff options
| -rw-r--r-- | src/common/Coquplib.v | 52 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 135 |
2 files changed, 175 insertions, 12 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 8ad557b..2295ff6 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -34,6 +34,27 @@ From compcert Require Import Integers. Local Open Scope Z_scope. +(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to + allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) +Inductive Learnt {A: Type} (a: A) := + | AlreadyKnown : Learnt a. + +Ltac learn_tac fact name := + lazymatch goal with + | [ H: Learnt fact |- _ ] => + fail 0 "fact" fact "has already been learnt" + | _ => let type := type of fact in + lazymatch goal with + | [ H: @Learnt type _ |- _ ] => + fail 0 "fact" fact "of type" type "was already learnt through" H + | _ => let learnt := fresh "Learn" in + pose proof (AlreadyKnown fact) as learnt; pose proof fact as name + end + end. + +Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name. +Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name. + Ltac unfold_rec c := unfold c; fold c. Ltac solve_by_inverts n := @@ -51,10 +72,11 @@ Ltac invert x := inversion x; subst; clear x. Ltac destruct_match := match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end. -Ltac clear_obvious := +Ltac nicify_hypotheses := repeat match goal with | [ H : ex _ |- _ ] => invert H | [ H : Some _ = Some _ |- _ ] => invert H + | [ H : ?x = ?x |- _ ] => clear H | [ H : _ /\ _ |- _ ] => invert H end. @@ -131,22 +153,32 @@ Ltac unfold_constants := end end. +Ltac substpp := + repeat match goal with + | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] => + let EQ := fresh "EQ" in + learn H1 as EQ; rewrite H2 in EQ; invert EQ + | _ => idtac + end. + Ltac simplify := intros; unfold_constants; simpl in *; - repeat (clear_obvious; nicify_goals; kill_bools); + repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); simpl in *. Infix "==nat" := eq_nat_dec (no associativity, at level 50). Infix "==Z" := Z.eq_dec (no associativity, at level 50). Ltac liapp := - match goal with - | [ |- (?x | ?y) ] => - match (eval compute in (Z.rem y x ==Z 0)) with - | left _ => let q := (eval compute in (Z.div y x)) in exists q; reflexivity - | _ => idtac - end - | _ => idtac - end. + repeat match goal with + | [ |- (?x | ?y) ] => + match (eval compute in (Z.rem y x ==Z 0)) with + | left _ => + let q := (eval compute in (Z.div y x)) + in exists q; reflexivity + | _ => idtac + end + | _ => idtac + end. Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index f5916ad..3c1b36f 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -522,7 +522,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2, stmnt_runp f asr0 asa0 st1 asr1 asa1 -> stmnt_runp f asr1 asa1 st2 asr2 asa2 -> - stmnt_runp f asr0 asa1 (Vseq st1 st2) asr2 asa2 + stmnt_runp f asr0 asa0 (Vseq st1 st2) asr2 asa2 | stmnt_runp_Vcond_true: forall asr0 asa0 asr1 asa1 f c vc stt stf, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> @@ -602,7 +602,7 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := | mi_stepp_Valways : forall f sr0 sa0 st sr1 sa1 c, - stmnt_runp f sr0 sa0 st sr1 sa0 -> + stmnt_runp f sr0 sa0 st sr1 sa1 -> mi_stepp f sr0 sa0 (Valways c st) sr1 sa1 | mi_stepp_Valways_ff : forall f sr0 sa0 st sr1 sa1 c, @@ -716,6 +716,7 @@ Definition empty_stack (m : module) : assocmap_arr := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + asr!(m.(mod_finish)) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some ist -> valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) @@ -764,3 +765,133 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + +Lemma expr_runp_determinate : + forall f e asr asa v, + expr_runp f asr asa e v -> + forall v', + expr_runp f asr asa e v' -> + v' = v. +Proof. + induction e; intros; + + repeat (try match goal with + | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H + + | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, + H2 : expr_runp _ _ _ ?e _ |- _ ] => + learn (H1 _ _ _ H2) + | [ H1 : forall v, expr_runp _ ?asr ?asa ?e v -> _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (H1 _ H2) + end; crush). +Qed. +Hint Resolve expr_runp_determinate : verilog. + +Lemma location_is_determinate : + forall f asr asa e l, + location_is f asr asa e l -> + forall l', + location_is f asr asa e l' -> + l' = l. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : location_is _ _ _ _ _ |- _ ] => invert H + | [ H1 : expr_runp _ ?asr ?asa ?e _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (expr_runp_determinate H1 H2) + end; crush). +Qed. + +Lemma stmnt_runp_determinate : + forall f s asr0 asa0 asr1 asa1, + stmnt_runp f asr0 asa0 s asr1 asa1 -> + forall asr1' asa1', + stmnt_runp f asr0 asa0 s asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. + induction 1; intros; + + repeat (try match goal with + | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H + + | [ H1 : expr_runp _ ?asr ?asa ?e _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (expr_runp_determinate H1 H2) + + | [ H1 : location_is _ ?asr ?asa ?e _, + H2 : location_is _ ?asr ?asa ?e _ |- _ ] => + learn (location_is_determinate H1 H2) + + | [ H1 : forall asr1 asa1, stmnt_runp _ ?asr0 ?asa0 ?s asr1 asa1 -> _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. +Hint Resolve stmnt_runp_determinate : verilog. + +Lemma mi_stepp_determinate : + forall f asr0 asa0 m asr1 asa1, + mi_stepp f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mi_stepp f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + intros. destruct m; invert H; invert H0; + + repeat (try match goal with + | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (stmnt_runp_determinate H1 H2) + end; crush). +Qed. + +Lemma mis_stepp_determinate : + forall f asr0 asa0 m asr1 asa1, + mis_stepp f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mis_stepp f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H + | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H + + | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _, + H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (mi_stepp_determinate H1 H2) + + | [ H1 : forall asr1 asa1, mis_stepp _ ?asr0 ?asa0 ?m asr1 asa1 -> _, + H2 : mis_stepp _ ?asr0 ?asa0 ?m _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. + +Lemma semantics_determinate : + forall (p: program), Smallstep.determinate (semantics p). +Proof. + intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. + - invert H; invert H0; constructor. (* Traces are always empty *) + - invert H; invert H0; crush. + pose proof (mis_stepp_determinate H4 H13) + admit. + - constructor. invert H; crush. + - invert H; invert H0; unfold ge0, ge1 in *; crush. + - red; simplify; intro; invert H0; invert H; crush. + - invert H; invert H0; crush. +Admitted. |