Switch to uvalueToZ in lessdef.

4 files changed, 87 insertions, 67 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index c9361c2..8ad557b 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -32,6 +32,8 @@ From coqup Require Import Show.
 From compcert.lib Require Export Coqlib.
 From compcert Require Import Integers.
 
+Local Open Scope Z_scope.
+
 Ltac unfold_rec c := unfold c; fold c.
 
 Ltac solve_by_inverts n :=
@@ -129,16 +131,28 @@ Ltac unfold_constants :=
            end
          end.
 
-Ltac crush := intros; unfold_constants; simpl in *;
-              repeat (clear_obvious; nicify_goals; kill_bools);
-              simpl in *; try discriminate; try congruence; try lia; try assumption.
-
-Global Opaque Nat.div.
-Global Opaque Z.mul.
+Ltac simplify := intros; unfold_constants; simpl in *;
+                 repeat (clear_obvious; nicify_goals; kill_bools);
+                 simpl in *.
 
 Infix "==nat" := eq_nat_dec (no associativity, at level 50).
 Infix "==Z" := Z.eq_dec (no associativity, at level 50).
 
+Ltac liapp :=
+  match goal with
+  | [ |- (?x | ?y) ] =>
+    match (eval compute in (Z.rem y x ==Z 0)) with
+    | left _ => let q := (eval compute in (Z.div y x)) in exists q; reflexivity
+    | _ => idtac
+    end
+  | _ => idtac
+  end.
+
+Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption.
+
+Global Opaque Nat.div.
+Global Opaque Z.mul.
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 6bac18d..dcaf3a1 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -70,22 +70,21 @@ Module PtrofsExtra.
 
   Lemma of_int_mod :
     forall x m,
-      Int.signed x mod m = 0 ->
-      Ptrofs.signed (Ptrofs.of_int x) mod m = 0.
+      Int.unsigned x mod m = 0 ->
+      Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0.
   Proof.
     intros.
-    pose proof (Integers.Ptrofs.agree32_of_int eq_refl x) as A.
-    pose proof Ptrofs.agree32_signed.
-    apply H0 in A; try reflexivity.
-    rewrite A. assumption.
+    unfold Ptrofs.of_int.
+    rewrite Ptrofs.unsigned_repr; crush;
+      apply Int.unsigned_range_2.
   Qed.
 
   Lemma mul_mod :
     forall x y m,
       0 < m ->
       (m | Ptrofs.modulus) ->
-      Ptrofs.signed x mod m = 0 ->
-      Ptrofs.signed y mod m = 0 ->
+      Ptrofs.unsigned x mod m = 0 ->
+      Ptrofs.unsigned y mod m = 0 ->
       (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0.
   Proof.
     intros. unfold Ptrofs.mul.
@@ -95,7 +94,6 @@ Module PtrofsExtra.
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
            end; try(crush; lia); ptrofs_mod_tac m.
   Qed.
 
@@ -103,8 +101,8 @@ Module PtrofsExtra.
     forall x y m,
       0 < m ->
       (m | Ptrofs.modulus) ->
-      Ptrofs.signed x mod m = 0 ->
-      Ptrofs.signed y mod m = 0 ->
+      Ptrofs.unsigned x mod m = 0 ->
+      Ptrofs.unsigned y mod m = 0 ->
       (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.
   Proof.
     intros. unfold Ptrofs.add.
@@ -114,7 +112,6 @@ Module PtrofsExtra.
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
            end; try (crush; lia); ptrofs_mod_tac m.
   Qed.
 
@@ -243,22 +240,37 @@ Module IntExtra.
   Ltac int_mod_tac m :=
     repeat (int_mod_match m); lia.
 
-  Lemma mul_mod :
+  Lemma mul_mod1 :
+    forall x y m,
+      0 < m ->
+      (m | Int.modulus) ->
+      Int.unsigned x mod m = 0 ->
+      (Int.unsigned (Int.mul x y)) mod m = 0.
+  Proof.
+    intros. unfold Int.mul.
+    rewrite Int.unsigned_repr_eq.
+
+    repeat match goal with
+           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
+           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
+             rewrite <- Zmod_div_mod; try lia; try assumption
+           end; try (crush; lia); int_mod_tac m.
+  Qed.
+
+  Lemma mul_mod2 :
     forall x y m,
       0 < m ->
       (m | Int.modulus) ->
-      Int.signed x mod m = 0 ->
-      Int.signed y mod m = 0 ->
-      (Int.signed (Int.mul x y)) mod m = 0.
+      Int.unsigned y mod m = 0 ->
+      (Int.unsigned (Int.mul x y)) mod m = 0.
   Proof.
     intros. unfold Int.mul.
-    rewrite Int.signed_repr_eq.
+    rewrite Int.unsigned_repr_eq.
 
     repeat match goal with
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
            end; try (crush; lia); int_mod_tac m.
   Qed.
 
@@ -266,18 +278,17 @@ Module IntExtra.
     forall x y m,
       0 < m ->
       (m | Int.modulus) ->
-      Int.signed x mod m = 0 ->
-      Int.signed y mod m = 0 ->
-      (Int.signed (Int.add x y)) mod m = 0.
+      Int.unsigned x mod m = 0 ->
+      Int.unsigned y mod m = 0 ->
+      (Int.unsigned (Int.add x y)) mod m = 0.
   Proof.
     intros. unfold Int.add.
-    rewrite Int.signed_repr_eq.
+    rewrite Int.unsigned_repr_eq.
 
     repeat match goal with
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
            | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
-           | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
            end; try (crush; lia); int_mod_tac m.
   Qed.
 End IntExtra.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 38fe27a..07417a7 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -635,18 +635,18 @@ Section CORRECTNESS.
       unfold check_address_parameter_signed in *;
       unfold check_address_parameter_unsigned in *; crush.
 
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        rewrite Integers.Ptrofs.signed_repr; try assumption.
-        admit. (* FIXME: Register bounds. *)
+        apply PtrofsExtra.add_mod; crush.
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
         apply PtrofsExtra.of_int_mod.
-        rewrite Integers.Int.signed_repr; crush. }
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
 
       (** Read bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
@@ -775,7 +775,7 @@ Section CORRECTNESS.
       unfold check_address_parameter_signed in *;
       unfold check_address_parameter_unsigned in *; crush.
 
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
                                        (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
                                                          (Integers.Int.repr z0)))) as OFFSET.
@@ -784,17 +784,15 @@ Section CORRECTNESS.
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
         apply PtrofsExtra.add_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        rewrite Integers.Ptrofs.signed_repr; try assumption.
-        admit. (* FIXME: Register bounds. *)
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
         apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        apply IntExtra.mul_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        admit. (* FIXME: Register bounds. *)
-        rewrite Integers.Int.signed_repr; crush.
-        rewrite Integers.Int.signed_repr; crush. }
+        apply IntExtra.add_mod; crush.
+        apply IntExtra.mul_mod2; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
 
       (** Read bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
@@ -1033,18 +1031,18 @@ Section CORRECTNESS.
       unfold check_address_parameter_unsigned in *;
       unfold check_address_parameter_signed in *; crush.
 
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
         apply PtrofsExtra.add_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        rewrite Integers.Ptrofs.signed_repr; try assumption.
-        admit. (* FIXME: Register bounds. *)
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
         apply PtrofsExtra.of_int_mod.
-        rewrite Integers.Int.signed_repr; crush. }
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
 
       (** Write bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
@@ -1133,7 +1131,7 @@ Section CORRECTNESS.
       rewrite list_repeat_len.
       rewrite H4. reflexivity.
 
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
@@ -1311,7 +1309,7 @@ Section CORRECTNESS.
       unfold check_address_parameter_signed in *;
       unfold check_address_parameter_unsigned in *; crush.
 
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
                                        (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
                                                          (Integers.Int.repr z0)))) as OFFSET.
@@ -1320,18 +1318,15 @@ Section CORRECTNESS.
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
         apply PtrofsExtra.add_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        rewrite Integers.Ptrofs.signed_repr; try assumption.
-        admit. (* FIXME: Register bounds. *)
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
         apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        apply IntExtra.mul_mod; crush; try lia.
-        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        admit. (* FIXME: Register bounds. *)
-        rewrite Integers.Int.signed_repr; crush; try split; try assumption.
-        rewrite Integers.Int.signed_repr; crush; try split; try assumption.
-      }
+        apply IntExtra.add_mod; crush.
+        apply IntExtra.mul_mod2; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
 
       (** Write bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
@@ -1423,7 +1418,7 @@ Section CORRECTNESS.
       rewrite list_repeat_len.
       rewrite H4. reflexivity.
 
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
                                        (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
                                                          (Integers.Int.repr z0)))) as OFFSET.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 116986b..acabcf2 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -304,8 +304,8 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | val_value_lessdef_ptr:
     forall b off v',
-    off = Ptrofs.repr (valueToZ v') ->
-    (Z.modulo (valueToZ v') 4) = 0%Z ->
+    off = Ptrofs.repr (uvalueToZ v') ->
+    (Z.modulo (uvalueToZ v') 4) = 0%Z ->
     val_value_lessdef (Vptr b off) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.