From accf4b273525412801dc21c893d41c890c9fed6d Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 28 Jun 2020 17:15:14 +0100 Subject: Fix unsigned/signed issues. --- src/common/Coquplib.v | 23 +++++++++++++++-------- src/common/IntegerExtra.v | 28 +++++++++++++++------------- 2 files changed, 30 insertions(+), 21 deletions(-) (limited to 'src/common') diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index b8a02d2..5de1e7c 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -69,45 +69,52 @@ Ltac kill_bools := Ltac unfold_constants := repeat match goal with - | [ _ : _ |- context[Integers.Ptrofs.modulus] ] => + | [ |- context[Integers.Ptrofs.modulus] ] => replace Integers.Ptrofs.modulus with 4294967296 by reflexivity | [ H : context[Integers.Ptrofs.modulus] |- _ ] => replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity - | [ _ : _ |- context[Integers.Ptrofs.min_signed] ] => + | [ |- context[Integers.Ptrofs.min_signed] ] => replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity | [ H : context[Integers.Ptrofs.min_signed] |- _ ] => replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity - | [ _ : _ |- context[Integers.Ptrofs.max_signed] ] => + | [ |- context[Integers.Ptrofs.max_signed] ] => replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity | [ H : context[Integers.Ptrofs.max_signed] |- _ ] => replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity - | [ _ : _ |- context[Integers.Ptrofs.max_unsigned] ] => + | [ |- context[Integers.Ptrofs.max_unsigned] ] => replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] => replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity - | [ _ : _ |- context[Integers.Int.modulus] ] => + | [ |- context[Integers.Int.modulus] ] => replace Integers.Int.modulus with 4294967296 by reflexivity | [ H : context[Integers.Int.modulus] |- _ ] => replace Integers.Int.modulus with 4294967296 in H by reflexivity - | [ _ : _ |- context[Integers.Int.min_signed] ] => + | [ |- context[Integers.Int.min_signed] ] => replace Integers.Int.min_signed with (-2147483648) by reflexivity | [ H : context[Integers.Int.min_signed] |- _ ] => replace Integers.Int.min_signed with (-2147483648) in H by reflexivity - | [ _ : _ |- context[Integers.Int.max_signed] ] => + | [ |- context[Integers.Int.max_signed] ] => replace Integers.Int.max_signed with 2147483647 by reflexivity | [ H : context[Integers.Int.max_signed] |- _ ] => replace Integers.Int.max_signed with 2147483647 in H by reflexivity - | [ _ : _ |- context[Integers.Int.max_unsigned] ] => + | [ |- context[Integers.Int.max_unsigned] ] => replace Integers.Int.max_unsigned with 4294967295 by reflexivity | [ H : context[Integers.Int.max_unsigned] |- _ ] => replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity + + | [ |- context[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr ?x) ] ] => + match (eval compute in (0 <=? x)) with + | true => replace (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x)) + with x by reflexivity + | false => idtac + end end. Ltac simplify := unfold_constants; simpl in *; diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 5f06e26..ec1fb07 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -105,10 +105,10 @@ Module PtrofsExtra. (m | Ptrofs.modulus) -> Ptrofs.signed x mod m = 0 -> Ptrofs.signed y mod m = 0 -> - (Ptrofs.signed (Ptrofs.add x y)) mod m = 0. + (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0. Proof. intros. unfold Ptrofs.add. - rewrite Ptrofs.signed_repr_eq. + rewrite Ptrofs.unsigned_repr_eq. repeat match goal with | [ _ : _ |- context[if ?x then _ else _] ] => destruct x @@ -118,21 +118,23 @@ Module PtrofsExtra. end; try (simplify; lia); ptrofs_mod_tac m. Qed. - Lemma mul_divs : + Lemma mul_divu : forall x y, - 0 <= Ptrofs.signed y -> - 0 < Ptrofs.signed x -> - Ptrofs.signed y mod Ptrofs.signed x = 0 -> - (Integers.Ptrofs.mul x (Integers.Ptrofs.divs y x)) = y. + 0 < Ptrofs.unsigned x -> + Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 -> + (Integers.Ptrofs.mul x (Integers.Ptrofs.divu y x)) = y. Proof. intros. - pose proof (Ptrofs.mods_divs_Euclid y x). - pose proof (Zquot.Zrem_Zmod_zero (Ptrofs.signed y) (Ptrofs.signed x)). - apply <- H3 in H1; try lia; clear H3. - unfold Ptrofs.mods in H2. - rewrite H1 in H2. - replace (Ptrofs.repr 0) with (Ptrofs.zero) in H2 by reflexivity. + assert (x <> Ptrofs.zero). + { intro. + rewrite H1 in H. + replace (Ptrofs.unsigned Ptrofs.zero) with 0 in H by reflexivity. + lia. } + + exploit (Ptrofs.modu_divu_Euclid y x); auto; intros. + unfold Ptrofs.modu in H2. rewrite H0 in H2. + replace (Ptrofs.repr 0) with Ptrofs.zero in H2 by reflexivity. rewrite Ptrofs.add_zero in H2. rewrite Ptrofs.mul_commut. congruence. -- cgit