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 ++++++----- src/translation/HTLgen.v | 28 ++++++----- src/translation/HTLgenproof.v | 110 ++++++++++++++++++------------------------ 4 files changed, 92 insertions(+), 97 deletions(-) (limited to 'src') 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. diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 54ad77a..59fb70a 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -280,32 +280,36 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. -Definition check_address_parameter (p : Z) : bool := +Definition check_address_parameter_signed (p : Z) : bool := Z.eqb (Z.modulo p 4) 0 && Z.leb Integers.Ptrofs.min_signed p && Z.leb p Integers.Ptrofs.max_signed. +Definition check_address_parameter_unsigned (p : Z) : bool := + Z.eqb (Z.modulo p 4) 0 + && Z.leb p Integers.Ptrofs.max_unsigned. + Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Op.Aindexed off, r1::nil => - if (check_address_parameter off) + if (check_address_parameter_signed off) then ret (boplitz Vadd r1 off) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ascaled scale offset, r1::nil => - if (check_address_parameter scale) && (check_address_parameter offset) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Aindexed2 offset, r1::r2::nil => - if (check_address_parameter offset) + if (check_address_parameter_signed offset) then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter scale) && (check_address_parameter offset) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in - if (check_address_parameter a) + if (check_address_parameter_unsigned a) then ret (Vlit (ZToValue 32 a)) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") @@ -392,19 +396,19 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Mint32, Op.Aindexed off, r1::nil => - if (check_address_parameter off) - then ret (Vvari stack (Vbinop Vdiv (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) + if (check_address_parameter_signed off) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter scale) && (check_address_parameter offset) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vvari stack - (Vbinop Vdiv + (Vbinop Vdivu (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) (ZToValue 32 4))) else error (Errors.msg "HTLgen: translate_arr_access address misaligned") | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.signed a in - if (check_address_parameter a) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 1e16398..eb9ff7a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -594,17 +594,17 @@ Section CORRECTNESS. invert H8. clear H0. clear H6. - unfold check_address_parameter in *. simplify. + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. (** Read bounds assumption *) - assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. (** Modular preservation proof *) - assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE. + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. apply PtrofsExtra.add_mod; simplify; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) @@ -617,34 +617,28 @@ Section CORRECTNESS. (** Normalisation proof *) assert (Integers.Ptrofs.repr (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) as NORMALISE. { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divs; auto. - rewrite Integers.Ptrofs.signed_repr; simplify; lia. } + apply PtrofsExtra.mul_divu; simplify; auto; lia. } (** Normalised bounds proof *) assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) < (RTL.fn_stacksize f / 4)) as NORMALISE_BOUND. { split. apply Integers.Ptrofs.unsigned_range_2. - assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. - unfold Integers.Ptrofs.divs at 2 in H0. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu at 2 in H0. rewrite H0. clear H0. rewrite Integers.Ptrofs.unsigned_repr; simplify. - rewrite Integers.Ptrofs.signed_repr; simplify; try lia. - rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; try lia. - rewrite Integers.Ptrofs.signed_repr. - rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. split. - apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. - apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. - simplify; lia. } + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -687,7 +681,7 @@ Section CORRECTNESS. setoid_rewrite Integers.Ptrofs.add_zero_l in H7. specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). @@ -699,11 +693,11 @@ Section CORRECTNESS. assert (Z.to_nat (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = - valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1)) + valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1)) as EXPR_OK by admit. rewrite <- EXPR_OK. rewrite NORMALISE in I. @@ -757,7 +751,7 @@ Section CORRECTNESS. rewrite Registers.Regmap.gss. unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; auto; intros I. rewrite NORMALISE in I. @@ -804,7 +798,8 @@ Section CORRECTNESS. invert H10. invert H12. clear H0. clear H6. clear H8. - unfold check_address_parameter in *. simplify. + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int @@ -812,11 +807,10 @@ Section CORRECTNESS. (Integers.Int.repr z0)))) as OFFSET. (** Read bounds assumption *) - assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. (** Modular preservation proof *) - assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE. + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. apply PtrofsExtra.add_mod; simplify; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) @@ -835,34 +829,28 @@ Section CORRECTNESS. (** Normalisation proof *) assert (Integers.Ptrofs.repr (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) as NORMALISE. { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divs; auto. - rewrite Integers.Ptrofs.signed_repr; simplify; lia. } + apply PtrofsExtra.mul_divu; simplify; auto; lia. } (** Normalised bounds proof *) assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) < (RTL.fn_stacksize f / 4)) as NORMALISE_BOUND. { split. apply Integers.Ptrofs.unsigned_range_2. - assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. - unfold Integers.Ptrofs.divs at 2 in H0. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu at 2 in H0. rewrite H0. clear H0. rewrite Integers.Ptrofs.unsigned_repr; simplify. - rewrite Integers.Ptrofs.signed_repr; simplify; try lia. - rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; try lia. - rewrite Integers.Ptrofs.signed_repr. - rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. split. - apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. - apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. - simplify; lia. } + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -911,7 +899,7 @@ Section CORRECTNESS. setoid_rewrite Integers.Ptrofs.add_zero_l in H7. specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). @@ -922,12 +910,12 @@ Section CORRECTNESS. intros I. assert (Z.to_nat (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = valueToNat - (vdivs (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5) - (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3)) + (vdiv (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5) + (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3)) as EXPR_OK by admit. rewrite <- EXPR_OK. rewrite NORMALISE in I. @@ -981,7 +969,7 @@ Section CORRECTNESS. rewrite Registers.Regmap.gss. unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; auto; intros I. rewrite NORMALISE in I. @@ -1001,7 +989,8 @@ Section CORRECTNESS. destruct (Archi.ptr64) eqn:ARCHI; simplify. rewrite ARCHI in H0. simplify. - unfold check_address_parameter in EQ; simplify. + unfold check_address_parameter_unsigned in *; + unfold check_address_parameter_signed in *; simplify. assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. rewrite ZERO in H1. clear ZERO. @@ -1010,43 +999,36 @@ Section CORRECTNESS. remember i0 as OFFSET. (** Read bounds assumption *) - assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. (** Modular preservation proof *) - rename H8 into MOD_PRESERVE. + rename H0 into MOD_PRESERVE. (** Normalisation proof *) assert (Integers.Ptrofs.repr (4 * Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) as NORMALISE. { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divs; auto. - rewrite Integers.Ptrofs.signed_repr; simplify; lia. } + apply PtrofsExtra.mul_divu; simplify; auto; try lia. } (** Normalised bounds proof *) assert (0 <= - Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)) + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) < (RTL.fn_stacksize f / 4)) as NORMALISE_BOUND. { split. apply Integers.Ptrofs.unsigned_range_2. - assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity. - unfold Integers.Ptrofs.divs at 2 in H0. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu at 2 in H0. rewrite H0. clear H0. rewrite Integers.Ptrofs.unsigned_repr; simplify. - rewrite Integers.Ptrofs.signed_repr; simplify; try lia. - rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; try lia. - rewrite Integers.Ptrofs.signed_repr. - rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia. split. - apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia. - apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia. - simplify; lia. } + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -1086,7 +1068,7 @@ Section CORRECTNESS. setoid_rewrite Integers.Ptrofs.add_zero_l in H7. specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). @@ -1097,11 +1079,11 @@ Section CORRECTNESS. intros I. assert (Z.to_nat (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = - valueToNat (ZToValue 32 (Integers.Ptrofs.signed OFFSET / 4))) + valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) as EXPR_OK by admit. rewrite <- EXPR_OK. rewrite NORMALISE in I. @@ -1155,7 +1137,7 @@ Section CORRECTNESS. rewrite Registers.Regmap.gss. unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))). + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; auto; intros I. rewrite NORMALISE in I. -- cgit