diff options
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index d55d94ad..33e2db61 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -847,6 +847,16 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. +Remark cast32unsigned_from_cast32signed: + forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). +Proof. + intros. apply Int64.same_bits_eq; intros. + rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. + rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). + change Int.zwordsize with 32. + destruct (zlt i0 32). auto. apply Int.bits_above. auto. +Qed. + (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall |