From adf1bbcd5c356a0cb75c412357a3b7af23795f47 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 11 Feb 2021 20:03:49 +0100 Subject: [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof --- riscV/Asmgenproof1.v | 69 ++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 64 insertions(+), 5 deletions(-) (limited to 'riscV/Asmgenproof1.v') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 57d281ec..0b1abe2a 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -494,6 +494,36 @@ Proof. split. rewrite V; destruct normal, b; reflexivity. intros; Simpl. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: (Int.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: negb (Int.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; unfold zero32, Op.zero32 in *; @@ -524,6 +554,36 @@ Proof. unfold zero32, Op.zero32 in *; eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: (Int64.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: negb (Int64.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. - destruct optR0 as [[]|]; unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; unfold zero64, Op.zero64 in *; @@ -1198,13 +1258,15 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 5: econstructor; split; try apply exec_straight_one; simpl; eauto; + 7: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; rewrite Int.add_commut; auto. - 9: econstructor; split; try apply exec_straight_one; simpl; eauto; + 13: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; rewrite Int64.add_commut; auto. all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl. + all: destruct (rs x0); auto. + all: destruct (rs x1); auto. Qed. (** Memory accesses *) @@ -1512,6 +1574,3 @@ Proof. Qed. End CONSTRUCTORS. - - - -- cgit