From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- common/Switch.v | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'common/Switch.v') diff --git a/common/Switch.v b/common/Switch.v index e5b3827e..0df2bbc8 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -118,7 +118,7 @@ Definition refine_low_bound (v lo: Z) := Definition refine_high_bound (v hi: Z) := if zeq v hi then hi - 1 else hi. -Fixpoint validate_jumptable (cases: ZMap.t nat) +Fixpoint validate_jumptable (cases: ZMap.t nat) (tbl: list nat) (n: Z) {struct tbl} : bool := match tbl with | nil => true @@ -143,7 +143,7 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree) | (None, _) => false | (Some act', others) => - beq_nat act act' + beq_nat act act' && validate default others t' (refine_low_bound pivot lo) (refine_high_bound pivot hi) @@ -192,10 +192,10 @@ Proof. induction t; simpl; intros; InvBooleans. - constructor. - destruct (split_eq key cases) as [[act'|] others]; try discriminate; InvBooleans. - constructor; eauto. + constructor; eauto. - destruct (split_lt key cases) as [lc rc]; InvBooleans. constructor; eauto. -- destruct (split_between default ofs sz cases) as [ins out]; InvBooleans. +- destruct (split_between default ofs sz cases) as [ins out]; InvBooleans. constructor; eauto. Qed. @@ -213,10 +213,10 @@ Proof. - intros. inv H. simpl. destruct (zeq v n); auto. - destruct a as [key act]. destruct (split_eq n cases) as [same other] eqn:SEQ. - rewrite (IHcases same other) by auto. + rewrite (IHcases same other) by auto. destruct (zeq key n); intros EQ; inv EQ. -+ destruct (zeq v n); auto. -+ simpl. destruct (zeq v key). ++ destruct (zeq v n); auto. ++ simpl. destruct (zeq v key). * subst v. rewrite zeq_false by auto. auto. * auto. Qed. @@ -231,7 +231,7 @@ Lemma split_lt_prop: Proof. induction cases; intros until rcases; simpl. - intros. inv H. simpl. destruct (zlt v n); auto. -- destruct a as [key act]. +- destruct a as [key act]. destruct (split_lt n cases) as [lc rc] eqn:SEQ. rewrite (IHcases lc rc) by auto. destruct (zlt key n); intros EQ; inv EQ; simpl. @@ -249,7 +249,7 @@ Lemma split_between_prop: Proof. induction cases; intros until outside; simpl; intros SEQ. - inv SEQ. rewrite ZMap.gi. simpl. destruct (zlt ((v - ofs) mod modulus) sz); auto. -- destruct a as [key act]. +- destruct a as [key act]. destruct (split_between default ofs sz cases) as [ins outs]. erewrite IHcases; eauto. destruct (zlt ((key - ofs) mod modulus) sz); inv SEQ. @@ -257,7 +257,7 @@ Proof. destruct (zeq v key). subst v. rewrite zlt_true by auto. auto. auto. -+ simpl. destruct (zeq v key). ++ simpl. destruct (zeq v key). subst v. rewrite zlt_false by auto. auto. auto. Qed. @@ -270,11 +270,11 @@ Lemma validate_jumptable_correct_rec: Proof. induction tbl; simpl; intros. - unfold list_length_z in H0. simpl in H0. omegaContradiction. -- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. +- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. destruct (zeq v 0). + replace (base + v) with base by omega. congruence. - + replace (base + v) with (Z.succ base + Z.pred v) by omega. - apply IHtbl. auto. omega. + + replace (base + v) with (Z.succ base + Z.pred v) by omega. + apply IHtbl. auto. omega. Qed. Lemma validate_jumptable_correct: @@ -288,12 +288,12 @@ Lemma validate_jumptable_correct: Proof. intros. rewrite (validate_jumptable_correct_rec cases tbl ofs); auto. -- f_equal. f_equal. rewrite Zmod_small. omega. - destruct (zle ofs v). omega. +- f_equal. f_equal. rewrite Zmod_small. omega. + destruct (zle ofs v). omega. assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus). { rewrite Zmod_small. omega. omega. } rewrite Z_mod_plus in M by auto. rewrite M in H0. omega. -- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. +- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. Qed. Lemma validate_correct_rec: @@ -307,23 +307,23 @@ Proof. intros default v VRANGE. induction t; simpl; intros until hi. - (* base case *) destruct cases as [ | [key1 act1] cases1]; intros. -+ apply beq_nat_true in H. subst act. reflexivity. -+ InvBooleans. apply beq_nat_true in H2. subst. simpl. ++ apply beq_nat_true in H. subst act. reflexivity. ++ InvBooleans. apply beq_nat_true in H2. subst. simpl. destruct (zeq v hi). auto. omegaContradiction. - (* eq node *) destruct (split_eq key cases) as [optact others] eqn:EQ. intros. destruct optact as [act1|]; InvBooleans; try discriminate. apply beq_nat_true in H. rewrite (split_eq_prop v default _ _ _ _ EQ). - destruct (zeq v key). + destruct (zeq v key). + congruence. - + eapply IHt; eauto. + + eapply IHt; eauto. unfold refine_low_bound, refine_high_bound. split. - destruct (zeq key lo); omega. + destruct (zeq key lo); omega. destruct (zeq key hi); omega. - (* lt node *) destruct (split_lt key cases) as [lcases rcases] eqn:EQ; intros; InvBooleans. - rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key). + rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key). eapply IHt1. eauto. omega. eapply IHt2. eauto. omega. - (* jumptable node *) @@ -331,8 +331,8 @@ Proof. rewrite (split_between_prop v _ _ _ _ _ _ EQ). assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega). destruct (zlt ((v - ofs) mod modulus) sz). - rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto. - eapply IHt; eauto. + rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto. + eapply IHt; eauto. Qed. Definition table_tree_agree @@ -345,8 +345,8 @@ Theorem validate_switch_correct: wf_comptree t /\ table_tree_agree default cases t. Proof. unfold validate_switch, table_tree_agree; split. - eapply validate_wf; eauto. - intros; eapply validate_correct_rec; eauto. omega. + eapply validate_wf; eauto. + intros; eapply validate_correct_rec; eauto. omega. Qed. End COMPTREE. -- cgit