diff --git a/Makefile b/Makefile index 24230c9b..36a12dbd 100644 --- a/Makefile +++ b/Makefile @@ -13,7 +13,7 @@ TEST_VS := $(shell find $(TEST_DIR) -type f -name '*.v') # We auto-update _CoqProject and _CoqProject.notest, # but only change their timestamp if the set of files that they list changed -PRINT_COQPROJECT_ARGS := printf -- '-Q %s/coqutil/ coqutil\n' '$(SRC_DIR)' +PRINT_COQPROJECT_ARGS := printf -- '-Q ../stdlib/_build/install/default/lib/coq/user-contrib/Stdlib Stdlib\n-Q %s/coqutil/ coqutil\n' '$(SRC_DIR)' PRINT_SRC_VS := printf -- '%s\n' $(sort $(SRC_VS)) PRINT_TEST_VS := printf -- '%s\n' $(sort $(TEST_VS)) PRINT_COQPROJECT_NOTEST := { $(PRINT_COQPROJECT_ARGS); $(PRINT_SRC_VS); } diff --git a/src/coqutil/Word/Naive.v b/src/coqutil/Word/Naive.v index fe31f261..8b34ffb2 100644 --- a/src/coqutil/Word/Naive.v +++ b/src/coqutil/Word/Naive.v @@ -1,28 +1,20 @@ -Require Import Coq.ZArith.BinIntDef Coq.ZArith.BinInt coqutil.Z.Lia. +From Coq Require Import BinInt Zmod Bits. Require Import coqutil.Tactics.destr. Require Import coqutil.sanity coqutil.Word.Interface. Import word. Local Open Scope Z_scope. -(* TODO: move me? *) -Definition minimize_eq_proof{A: Type}(eq_dec: forall (x y: A), {x = y} + {x <> y}){x y: A} (pf: x = y): x = y := - match eq_dec x y with - | left p => p - | right n => match n pf: False with end - end. - Section WithWidth. Local Set Default Proof Using "All". Context {width : Z}. + Definition rep : Set := bits width. + Definition unsigned (w : rep) := Zmod.unsigned w. + + Definition wrap (z:Z) : rep := bits.of_Z width z. + Definition signed (w : rep) := Zmod.signed w. + Let wrap_value z := z mod (2^width). Let swrap_value z := wrap_value (z + 2 ^ (width - 1)) - 2 ^ (width - 1). - Record rep : Set := mk { unsigned : Z ; _unsigned_in_range : wrap_value unsigned = unsigned }. - - Definition wrap (z:Z) : rep := - mk (wrap_value z) (minimize_eq_proof Z.eq_dec (Zdiv.Zmod_mod z _)). - Definition signed w := swrap_value (unsigned w). Record special_cases : Set := { - div_by_zero: Z -> Z; - mod_by_zero: Z -> Z; adjust_too_big_shift_amount: Z -> Z; }. @@ -50,35 +42,31 @@ Section WithWidth. Local Set Default Proof Using "All". word.signed := signed; of_Z := wrap; - add x y := wrap (Z.add (unsigned x) (unsigned y)); - sub x y := wrap (Z.sub (unsigned x) (unsigned y)); - opp x := wrap (Z.opp (unsigned x)); + add := Zmod.add; + sub := Zmod.sub; + opp := Zmod.opp; - or x y := wrap (Z.lor (unsigned x) (unsigned y)); - and x y := wrap (Z.land (unsigned x) (unsigned y)); - xor x y := wrap (Z.lxor (unsigned x) (unsigned y)); - not x := wrap (Z.lnot (unsigned x)); - ndn x y := wrap (Z.ldiff (unsigned x) (unsigned y)); + or := Zmod.or; + and := Zmod.and; + xor := Zmod.xor; + not := Zmod.not; + ndn := Zmod.ndn; - mul x y := wrap (Z.mul (unsigned x) (unsigned y)); + mul := Zmod.mul; mulhss x y := wrap (Z.mul (signed x) (signed y) / 2^width); mulhsu x y := wrap (Z.mul (signed x) (unsigned y) / 2^width); mulhuu x y := wrap (Z.mul (unsigned x) (unsigned y) / 2^width); - divu x y := wrap (if Z.eqb (unsigned y) 0 then sp.(div_by_zero) (unsigned x) - else Z.div (unsigned x) (unsigned y)); - divs x y := wrap (if Z.eqb (signed y) 0 then sp.(div_by_zero) (signed x) - else Z.quot (signed x) (signed y)); - modu x y := wrap (if Z.eqb (unsigned y) 0 then sp.(mod_by_zero) (unsigned x) - else Z.modulo (unsigned x) (unsigned y)); - mods x y := wrap (if Z.eqb (signed y) 0 then sp.(mod_by_zero) (signed x) - else Z.rem (signed x) (signed y)); + divu := Zmod.udiv; + divs := Zmod.squot; + modu := Zmod.umod; + mods := Zmod.srem; - slu x y := wrap (Z.shiftl (unsigned x) (adjust_shift_amount (unsigned y))); - sru x y := wrap (Z.shiftr (unsigned x) (adjust_shift_amount (unsigned y))); - srs x y := wrap (Z.shiftr (signed x) (adjust_shift_amount (unsigned y))); + slu x y := Zmod.slu x (adjust_shift_amount (unsigned y)); + sru x y := Zmod.sru x (adjust_shift_amount (unsigned y)); + srs x y := Zmod.srs x (adjust_shift_amount (unsigned y)); - eqb x y := Z.eqb (unsigned x) (unsigned y); + eqb := Zmod.eqb; ltu x y := Z.ltb (unsigned x) (unsigned y); lts x y := Z.ltb (signed x) (signed y); @@ -86,45 +74,81 @@ Section WithWidth. Local Set Default Proof Using "All". |}. Lemma eq_unsigned {x y : rep} : unsigned x = unsigned y -> x = y. - Proof. - cbv [value]; destruct x as [x px], y as [y py]; cbn. - intro; subst y. - apply f_equal, Eqdep_dec.UIP_dec. eapply Z.eq_dec. - Qed. + Proof. apply Zmod.unsigned_inj. Qed. Lemma of_Z_unsigned x : wrap (unsigned x) = x. - Proof. eapply eq_unsigned; destruct x; cbn; assumption. Qed. + Proof. apply Zmod.of_Z_to_Z. Qed. + + (* Candidate for stdlib inclusion: *) + Lemma smod_swrap z : ZModOffset.Z.smodulo z (2 ^ width) = @swrap width gen_word z. + Proof. + cbv [swrap gen_word]. + cbv [ZModOffset.Z.smodulo ZModOffset.Z.omodulo]. + rewrite Z.add_opp_r, Z.sub_opp_r. + case (Z.eqb_spec width 0) as [->|]; trivial. + case (Z.eqb_spec width 1) as [->|]; trivial. + case (Z.ltb_spec width 0) as []. { rewrite !Z.pow_neg_r by lia; trivial. } + rewrite Z.pow_sub_r by try lia; change (2^1) with 2. + rewrite Z.quot_div_nonneg by lia; trivial. + Qed. Lemma signed_of_Z z : signed (wrap z) = wrap_value (z + 2 ^ (width - 1)) - 2 ^ (width - 1). Proof. + cbv [signed wrap]; rewrite Zmod.signed_of_Z. cbv [unsigned signed wrap wrap_value swrap_value]. - rewrite Zdiv.Zplus_mod_idemp_l; auto. + apply smod_swrap. Qed. Context (width_nonneg : Z.lt 0 width). Global Instance gen_ok : word.ok gen_word. Proof. - split; intros; - repeat match goal with - | a: @word.rep _ _ |- _ => destruct a - end; - cbn in *; - unfold adjust_shift_amount in *; - repeat match goal with - | |- context[if ?b then _ else _] => destr b - end; - eauto using of_Z_unsigned, signed_of_Z; - try (exfalso; blia). - apply eq_unsigned; assumption. + split; trivial; + cbv [gen_word adjust_shift_amount signed unsigned wrap]; intros. + { apply Zmod.unsigned_of_Z. } + { rewrite <-smod_swrap. apply Zmod.signed_of_Z. } + { apply Zmod.of_Z_to_Z. } + { apply Zmod.unsigned_add. } + { apply Zmod.unsigned_sub. } + { apply Zmod.unsigned_opp. } + { apply Zmod.unsigned_of_Z. } + { apply Zmod.unsigned_of_Z. } + { apply Zmod.unsigned_of_Z. } + { apply Zmod.unsigned_of_Z. } + { apply Zmod.unsigned_of_Z. } + { apply Zmod.unsigned_mul. } + { cbv [word.signed mulhss]. rewrite Zmod.signed_of_Z, smod_swrap; trivial. } + { cbv [word.signed mulhsu]. rewrite Zmod.signed_of_Z, smod_swrap; trivial. } + { cbv [word.unsigned mulhuu]. apply Zmod.unsigned_of_Z. } + { cbv [word.unsigned divu]. rewrite Zmod.unsigned_udiv; trivial. } + { cbv [word.signed divs]. rewrite Zmod.signed_squot, <-smod_swrap. + case Z.eqb_spec; [contradiction|]; trivial. } + { cbv [word.unsigned modu] in *. rewrite Zmod.unsigned_umod; trivial. + symmetry; apply Z.mod_small. + pose proof Zmod.unsigned_pos_bound x ltac:(lia). + pose proof Zmod.unsigned_pos_bound y ltac:(lia). + pose proof (Z.mod_pos_bound (Zmod.unsigned x) (Zmod.unsigned y)). + lia. } + { cbv [word.signed mods]. rewrite Zmod.signed_srem, <-smod_swrap; trivial. } + { cbv [word.unsigned slu] in *; case Z.ltb_spec; intros; [|lia]. + apply Zmod.unsigned_slu. } + { cbv [word.unsigned sru] in *; case Z.ltb_spec; intros; [|lia]. + pose proof Zmod.unsigned_pos_bound x ltac:(lia). + pose proof Zmod.unsigned_pos_bound y ltac:(lia). + rewrite Zmod.unsigned_sru, Z.mod_small; + rewrite ?Z.shiftr_div_pow2; try (Z.to_euclidean_division_equations; nia). } + { cbv [word.unsigned word.signed srs] in *; case Z.ltb_spec; intros; [|lia]. + pose proof Zmod.signed_pos_bound x ltac:(lia). + pose proof Zmod.unsigned_pos_bound y ltac:(lia). + rewrite Zmod.signed_srs, <-smod_swrap, Z.smod_even_small; + rewrite ?Z.shiftr_div_pow2; try (Z.to_euclidean_division_equations; nia). + rewrite <-(Z.succ_pred width), Z.pow_succ_r, Z.mul_comm, Z.rem_mul; lia. } Qed. End WithWidth. Arguments gen_word : clear implicits. Arguments gen_ok : clear implicits. Definition default_special_case_handlers width := {| - div_by_zero x := -1; - mod_by_zero x := x; adjust_too_big_shift_amount n := n mod 2 ^ Z.log2 width; |}.