diff options
Diffstat (limited to 'verilog/SelectOpproof.v')
| -rw-r--r-- | verilog/SelectOpproof.v | 43 |
1 files changed, 1 insertions, 42 deletions
diff --git a/verilog/SelectOpproof.v b/verilog/SelectOpproof.v index f450fe6c..789e38dc 100644 --- a/verilog/SelectOpproof.v +++ b/verilog/SelectOpproof.v @@ -172,7 +172,6 @@ Proof. destruct Archi.ptr64 eqn:SF; auto. apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. rewrite (Ptrofs.add_commut (Ptrofs.of_int n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. econstructor; split. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto. destruct sp; simpl; auto. @@ -180,7 +179,6 @@ Proof. destruct Archi.ptr64 eqn:SF; auto. apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal. rewrite Ptrofs.add_commut. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. replace (Val.add (Val.add v1 (Vint n1)) y) with (Val.add (Val.add v1 y) (Vint n1)). @@ -965,43 +963,6 @@ Proof. destruct Archi.ptr64 eqn:PTR64. 2: discriminate. destruct ty; cbn in *; try discriminate. - - (* Tint *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption. - * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. - - - (* Tfloat *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. - apply ExtValues.float_bits_normalize. - * rewrite ExtValues.select01_long_false. - apply ExtValues.float_bits_normalize. - - - (* Tlong *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. reflexivity. - * rewrite ExtValues.select01_long_false. reflexivity. - - - (* Tsingle *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. - rewrite normalize_low_long by assumption. - apply ExtValues.single_bits_normalize. - * rewrite ExtValues.select01_long_false. - rewrite normalize_low_long by assumption. - apply ExtValues.single_bits_normalize. Qed. Theorem eval_addressing: @@ -1024,8 +985,7 @@ Proof. destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. simpl. auto. - exists (v1 :: nil); split. eauto with evalexpr. simpl. - destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. - simpl. auto. + destruct v1; simpl in H; try discriminate. - exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto. Qed. @@ -1045,7 +1005,6 @@ Proof. + constructor; auto. + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vint n) else Val.add v1 (Vint n)). repeat constructor; auto. - rewrite SF; auto. - destruct Archi.ptr64 eqn:SF. + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vlong n) else Val.add v1 (Vlong n)). repeat constructor; auto. |