diff options
Diffstat (limited to 'kvx/PostpassSchedulingproof.v')
-rw-r--r-- | kvx/PostpassSchedulingproof.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/kvx/PostpassSchedulingproof.v b/kvx/PostpassSchedulingproof.v index c290387b..937b3be6 100644 --- a/kvx/PostpassSchedulingproof.v +++ b/kvx/PostpassSchedulingproof.v @@ -20,6 +20,7 @@ Require Import Asmblockgenproof0 Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. +Require Import Lia. Local Open Scope error_monad_scope. @@ -93,12 +94,12 @@ Proof. rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. assert (size bb = size a + size b). { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. - repeat (rewrite Nat2Z.inj_add). omega. } + repeat (rewrite Nat2Z.inj_add). lia. } clear EXA H0 H1. rewrite H in EXEB. assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } rewrite H0. rewrite <- pc_set_add; auto. - exploit size_positive. instantiate (1 := a). intro. omega. - exploit size_positive. instantiate (1 := b). intro. omega. + exploit size_positive. instantiate (1 := a). intro. lia. + exploit size_positive. instantiate (1 := b). intro. lia. Qed. Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : @@ -140,7 +141,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. - omega. + lia. Qed. Lemma symbols_preserved: @@ -224,7 +225,7 @@ Proof. + apply IHlbb in H. destruct H as (c & TAIL). exists c. enough (pos = pos - size a + size a) as ->. apply code_tail_S; auto. - omega. + lia. Qed. Lemma code_tail_head_app: @@ -291,7 +292,7 @@ Lemma verified_schedule_not_empty: verified_schedule bb = OK lbb -> lbb <> nil. Proof. intros. apply verified_schedule_size in H. - pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. + pose (size_positive bb). assert (size_blocks lbb > 0) by lia. clear H g. destruct lbb; simpl in *; discriminate. Qed. @@ -356,7 +357,7 @@ Proof. induction tc. - intros. simpl in H. discriminate. - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. - + inv H. assert (k = k') by omega. subst. reflexivity. + + inv H. assert (k = k') by lia. subst. reflexivity. + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto. Qed. |