From 213267be33d714dabd19ca09210b5dc1ad4f6254 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 27 May 2020 23:38:40 +0100 Subject: Add more proofs and remove Admitted --- src/translation/HTLgenproof.v | 92 ++++++++++++++++++++----------------------- src/verilog/AssocMap.v | 45 +++++++++++++++++---- src/verilog/Value.v | 22 +++++++---- 3 files changed, 94 insertions(+), 65 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index b07c654..499b6b5 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -26,10 +26,11 @@ Hint Resolve Smallstep.forward_simulation_plus : htlproof. Hint Resolve AssocMap.gss : htlproof. Hint Resolve AssocMap.gso : htlproof. -Inductive match_assocmaps : RTL.regset -> assocmap -> Prop := -| match_assocmap : forall rs am, - (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) -> - match_assocmaps rs am. +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. Definition state_st_wf (m : HTL.module) (s : HTL.state) := @@ -40,7 +41,7 @@ Hint Unfold state_st_wf : htlproof. Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st - (MASSOC : match_assocmaps rs assoc) + (MASSOC : match_assocmaps f rs assoc) (TF : tr_module f m) (WF : state_st_wf m (HTL.State m st assoc)), match_states (RTL.State sf f sp st rs mem) @@ -61,27 +62,45 @@ Inductive match_program : RTL.program -> HTL.module -> Prop := Hint Constructors match_program : htlproof. Lemma regs_lessdef_regs : - forall rs1 rs2 n v, - match_assocmaps rs1 rs2 -> - match_assocmaps rs1 (AssocMap.add n v rs2). -Admitted. + forall f rs1 rs2 n v, + Plt (RTL.max_reg_function f) n -> + match_assocmaps f rs1 rs2 -> + match_assocmaps f rs1 (AssocMap.add n v rs2). +Proof. + inversion 2; subst. + intros. constructor. + intros. unfold find_assocmap. unfold AssocMapExt.find_default. + rewrite AssocMap.gso. eauto. + apply Pos.le_lt_trans with _ _ n in H2. + unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. +Qed. Lemma regs_add_match : - forall rs am r v v', - match_assocmaps rs am -> + forall f rs am r v v', val_value_lessdef v v' -> - match_assocmaps (Registers.Regmap.set r v rs) (AssocMap.add r v' am). -Admitted. - -Lemma merge_inj : - forall am am' r v, - merge_assocmap (AssocMap.add r v am) am' = AssocMap.add r v (merge_assocmap am am'). -Admitted. + match_assocmaps f rs am -> + match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.add r v' am). +Proof. + inversion 2; subst. + constructor. intros. + destruct (peq r0 r); subst. + rewrite Registers.Regmap.gss. + unfold find_assocmap. unfold AssocMapExt.find_default. + rewrite AssocMap.gss. assumption. + + rewrite Registers.Regmap.gso; try assumption. + unfold find_assocmap. unfold AssocMapExt.find_default. + rewrite AssocMap.gso; eauto. +Qed. Lemma valToValue_lessdef : - forall v, - val_value_lessdef v (valToValue v). -Admitted. + forall v v', + valToValue v = Some v' <-> + val_value_lessdef v v'. +Proof. + split; intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. unfold intToValue (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : @@ -94,28 +113,6 @@ Lemma assumption_32bit_bool : valueToBool (boolToValue 32 b) = b. Admitted. -Lemma regset_assocmap_get : - forall r rs am v v', - match_assocmaps rs am -> - v = Registers.Regmap.get r rs -> - v' = am#r -> - val_value_lessdef v v'. -Proof. inversion 1. intros. subst. apply H0. Qed. - -Lemma regset_assocmap_wf : - forall r rs am i, - match_assocmaps rs am -> - Values.Vint i <> Registers.Regmap.get r rs -> - am!r = None. -Admitted. - -Lemma regset_assocmap_wf2 : - forall r rs am i, - match_assocmaps rs am -> - Values.Vint i = Registers.Regmap.get r rs -> - am!r = Some (intToValue i). -Admitted. - Lemma st_greater_than_res : forall m res : positive, m <> res. @@ -131,9 +128,6 @@ Lemma finish_not_res : f <> r. Admitted. -Ltac unfold_merge := - try (repeat (rewrite merge_inj)); unfold merge_assocmap; rewrite AssocMapExt.merge_base. - Ltac inv_state := match goal with MSTATE : match_states _ _ |- _ => @@ -222,12 +216,12 @@ Section CORRECTNESS. econstructor. (* prove stval *) - unfold_merge; simpl. - apply AssocMap.gss. + unfold merge_assocmap. apply AssocMapExt.merge_add. simpl. apply AssocMap.gss. (* prove match_state *) - unfold_merge. rewrite assumption_32bit. + rewrite assumption_32bit. constructor; auto. + unfold merge_assocmap. rewrite AssocMapExt.merge_add. simpl. apply AssocMap.gss. apply regs_lessdef_regs. assumption. unfold state_st_wf. inversion 1. subst. apply AssocMap.gss. - (* Iop *) diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index cac2c02..7db800b 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -26,6 +26,11 @@ Module AssocMap := PositiveMap. Module AssocMapExt. Import AssocMap. + Hint Resolve elements_3w : assocmap. + Hint Resolve elements_correct : assocmap. + Hint Resolve gss : assocmap. + Hint Resolve gso : assocmap. + Section Operations. Variable elt : Type. @@ -36,16 +41,40 @@ Module AssocMapExt. | Some v => v end. - Definition merge (m1 m2 : t elt) : t elt := - fold_right (fun el m => match el with (k, v) => add k v m end) m2 (elements m1). + Definition merge (am bm : t elt) : t elt := + fold_right (fun p a => add (fst p) (snd p) a) bm (elements am). - Lemma merge_add_assoc2 : - forall am am' r v, - merge (add r v am) am' = add r v (merge am am'). + Lemma add_assoc : + forall k v l bm, + List.In (k, v) l -> + SetoidList.NoDupA (@eq_key elt) l -> + @find elt k (fold_right (fun p a => add (fst p) (snd p) a) bm l) = Some v. Proof. - induction am; intros. - unfold merge. simpl. unfold fold_right. simpl. Search MapsTo. - Abort. + Hint Resolve SetoidList.InA_alt : assocmap. + Hint Extern 1 (exists _, _) => apply list_in_map_inv : assocmap. + + induction l; intros. + - contradiction. + - destruct a as [k' v']. + destruct (peq k k'). + + inversion H. inversion H1. inversion H0. subst. + simpl. auto with assocmap. + + subst. inversion H0. subst. apply in_map with (f := fst) in H1. simpl in *. + unfold not in H4. exfalso. apply H4. apply SetoidList.InA_alt. + auto with assocmap. + + + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption. + apply IHl. contradiction. contradiction. + simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption. + Qed. + Hint Resolve add_assoc : assocmap. + + Lemma merge_add : + forall k v am bm, + find k am = Some v -> + find k (merge am bm) = Some v. + Proof. unfold merge. auto with assocmap. Qed. Lemma merge_base : forall am, diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 0ce0bc5..34cb0d2 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -85,10 +85,11 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (valueToZ i). -Definition valToValue (v : Values.val) := +Definition valToValue (v : Values.val) : option value := match v with - | Values.Vint i => intToValue i - | _ => ZToValue 32 0%Z + | Values.Vint i => Some (intToValue i) + | Values.Vundef => Some (ZToValue 32 0%Z) + | _ => None end. (** Convert a [value] to a [bool], so that choices can be made based on the @@ -295,17 +296,22 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. -Search Z positive. - -Search "wordToZ". +Lemma valueToZ_ZToValue : + forall n z, + (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> + valueToZ (ZToValue (S n) z) = z. +Proof. + unfold valueToZ, ZToValue. simpl. + auto using wordToZ_ZToWord. +Qed. Lemma uvalueToZ_ZToValue : forall n z, (0 <= z < 2 ^ Z.of_nat n)%Z -> uvalueToZ (ZToValue n z) = z. Proof. - intros. unfold uvalueToZ, ZToValue. simpl. - apply uwordToZ_ZToWord. apply H. + unfold uvalueToZ, ZToValue. simpl. + auto using uwordToZ_ZToWord. Qed. Lemma valueToPos_posToValueAuto : -- cgit