From 1d8afa5949cd192620e4649ae32df49bca4da3f8 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 2 Jul 2020 21:57:03 +0100 Subject: Switch to uvalueToZ in lessdef. --- src/common/Coquplib.v | 26 +++++++++++++---- src/common/IntegerExtra.v | 57 +++++++++++++++++++++--------------- src/translation/HTLgenproof.v | 67 ++++++++++++++++++++----------------------- src/verilog/Value.v | 4 +-- 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. -- cgit