Fix unsigned/signed issues.

1 files changed, 15 insertions, 13 deletions

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.