diff options
Diffstat (limited to 'src/LegacyArithmetic')
26 files changed, 0 insertions, 3677 deletions
diff --git a/src/LegacyArithmetic/ArchitectureToZLike.v b/src/LegacyArithmetic/ArchitectureToZLike.v deleted file mode 100644 index 19450f831..000000000 --- a/src/LegacyArithmetic/ArchitectureToZLike.v +++ /dev/null @@ -1,38 +0,0 @@ -(*** Implementing ℤ-Like via Architecture *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.LetIn. - -Local Open Scope Z_scope. - -Section fancy_machine_p256_montgomery_foundation. - Context {n_over_two : Z}. - Local Notation n := (2 * n_over_two). - Context (ops : fancy_machine.instructions n) (modulus : Z). - - Local Instance ZLikeOps_of_ArchitectureBoundedOps_Factored (smaller_bound_exp : Z) - ldi_modulus ldi_0 - : ZLikeOps (2^n) (2^smaller_bound_exp) modulus := - { LargeT := tuple fancy_machine.W 2; - SmallT := fancy_machine.W; - modulus_digits := ldi_modulus; - decode_large := decode; - decode_small := decode; - Mod_SmallBound v := fst v; - DivBy_SmallBound v := snd v; - DivBy_SmallerBound v := if smaller_bound_exp =? n - then snd v - else dlet v := v in shrd (snd v) (fst v) smaller_bound_exp; - Mul x y := muldw x y; - CarryAdd x y := adc x y false; - CarrySubSmall x y := subc x y false; - ConditionalSubtract b x := let v := selc b (ldi_modulus) (ldi_0) in snd (subc x v false); - ConditionalSubtractModulus y := addm y (ldi_0) (ldi_modulus) }. - - Global Instance ZLikeOps_of_ArchitectureBoundedOps (smaller_bound_exp : Z) - : ZLikeOps (2^n) (2^smaller_bound_exp) modulus := - @ZLikeOps_of_ArchitectureBoundedOps_Factored smaller_bound_exp (ldi modulus) (ldi 0). -End fancy_machine_p256_montgomery_foundation. diff --git a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v deleted file mode 100644 index 899b10162..000000000 --- a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v +++ /dev/null @@ -1,128 +0,0 @@ -(*** Proving ℤ-Like via Architecture *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Multiply. -Require Import Crypto.LegacyArithmetic.ArchitectureToZLike. -Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.LetIn. - -Local Open Scope nat_scope. -Local Open Scope Z_scope. -Local Open Scope type_scope. - -Local Coercion Z.of_nat : nat >-> Z. - -Section fancy_machine_p256_montgomery_foundation. - Context {n_over_two : Z}. - Local Notation n := (2 * n_over_two)%Z. - Context (ops : fancy_machine.instructions n) (modulus : Z). - - Local Arguments Z.mul !_ !_. - Local Arguments BaseSystem.decode !_ !_ / . - Local Arguments BaseSystem.accumulate / _ _. - Local Arguments BaseSystem.decode' !_ !_ / . - - Local Ltac introduce_t_step := - match goal with - | [ |- forall x : bool, _ ] => intros [|] - | [ |- True -> _ ] => intros _ - | [ |- _ <= _ < _ -> _ ] => intro - | _ => let x := fresh "x" in - intro x; - try pose proof (decode_range (fst x)); - try pose proof (decode_range (snd x)); - pose proof (decode_range x) - end. - Local Ltac unfolder_t := - progress unfold LargeT, SmallT, modulus_digits, decode_large, decode_small, Mod_SmallBound, DivBy_SmallBound, DivBy_SmallerBound, Mul, CarryAdd, CarrySubSmall, ConditionalSubtract, ConditionalSubtractModulus, ZLikeOps_of_ArchitectureBoundedOps, ZLikeOps_of_ArchitectureBoundedOps_Factored in *. - Local Ltac saturate_context_step := - match goal with - | _ => unique assert (0 <= 2 * n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ] - | _ => unique assert (0 <= n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ] - | _ => unique assert (0 <= 2 * (2 * n_over_two)) by (eauto using decode_exponent_nonnegative with typeclass_instances) - | [ H : 0 <= ?x < _ |- _ ] => unique pose proof (proj1 H); unique pose proof (proj2 H) - end. - Local Ltac pre_t := - repeat first [ tauto - | introduce_t_step - | unfolder_t - | saturate_context_step ]. - Local Ltac post_t_step := - match goal with - | _ => reflexivity - | _ => progress subst - | _ => progress unfold Let_In - | _ => progress autorewrite with zsimplify_const - | [ |- fst ?x = (?a <=? ?b) :> bool ] - => cut (((if fst x then 1 else 0) = (if a <=? b then 1 else 0))%Z); - [ destruct (fst x), (a <=? b); intro; congruence | ] - | [ H : (_ =? _) = true |- _ ] => apply Z.eqb_eq in H; subst - | [ H : (_ =? _) = false |- _ ] => apply Z.eqb_neq in H - | _ => autorewrite with push_Zpow in *; solve [ reflexivity | assumption ] - | _ => autorewrite with pull_Zpow in *; pull_decode; reflexivity - | _ => progress push_decode - | _ => rewrite (Z.add_comm (_ << _) _); progress pull_decode - | [ |- context[if ?x =? ?y then _ else _] ] => destruct (x =? y) eqn:? - | _ => autorewrite with Zshift_to_pow; Z.rewrite_mod_small; reflexivity - end. - Local Ltac post_t := repeat post_t_step. - Local Ltac t := pre_t; post_t. - - Global Instance ZLikeProperties_of_ArchitectureBoundedOps_Factored - {arith : fancy_machine.arithmetic ops} - ldi_modulus ldi_0 - (Hldi_modulus : ldi_modulus = ldi modulus) - (Hldi_0 : ldi_0 = ldi 0) - (modulus_in_range : 0 <= modulus < 2^n) - (smaller_bound_exp : Z) - (smaller_bound_smaller : 0 <= smaller_bound_exp <= n) - (n_pos : 0 < n) - : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps_Factored ops modulus smaller_bound_exp ldi_modulus ldi_0). - Proof. - refine {| large_valid v := True; - medium_valid v := 0 <= decode_large v < 2^n * 2^smaller_bound_exp; - small_valid v := True |}. - (* In 8.5: *) - (* par:t. *) - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - Defined. - - Global Instance ZLikeProperties_of_ArchitectureBoundedOps - {arith : fancy_machine.arithmetic ops} - (modulus_in_range : 0 <= modulus < 2^n) - (smaller_bound_exp : Z) - (smaller_bound_smaller : 0 <= smaller_bound_exp <= n) - (n_pos : 0 < n) - : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps ops modulus smaller_bound_exp) - := ZLikeProperties_of_ArchitectureBoundedOps_Factored _ _ eq_refl eq_refl modulus_in_range _ smaller_bound_smaller n_pos. -End fancy_machine_p256_montgomery_foundation. diff --git a/src/LegacyArithmetic/BarretReduction.v b/src/LegacyArithmetic/BarretReduction.v deleted file mode 100644 index 37c4d4915..000000000 --- a/src/LegacyArithmetic/BarretReduction.v +++ /dev/null @@ -1,98 +0,0 @@ -(*** Barrett Reduction *) -(** This file implements Barrett Reduction on [ZLikeOps]. We follow - [BarretReduction/ZHandbook.v]. *) -Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. -Require Import Crypto.Arithmetic.BarrettReduction.HAC. -Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.Notations. - -Local Open Scope small_zlike_scope. -Local Open Scope large_zlike_scope. -Local Open Scope Z_scope. - -Section barrett. - Context (m b k μ offset : Z) - (m_pos : 0 < m) - (base_pos : 0 < b) - (k_good : m < b^k) - (μ_good : μ = b^(2*k) / m) (* [/] is [Z.div], which is truncated *) - (offset_nonneg : 0 <= offset) - (k_big_enough : offset <= k) - (m_small : 3 * m <= b^(k+offset)) - (m_large : b^(k-offset) <= m + 1). - Context {ops : ZLikeOps (b^(k+offset)) (b^(k-offset)) m} {props : ZLikeProperties ops} - (μ' : SmallT) - (μ'_good : small_valid μ') - (μ'_eq : decode_small μ' = μ). - - Definition barrett_reduce : forall x : LargeT, - { barrett_reduce : SmallT - | medium_valid x - -> decode_small barrett_reduce = (decode_large x) mod m - /\ small_valid barrett_reduce }. - Proof. - intro x. evar (pr : SmallT); exists pr. intros x_valid. - assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by auto using decode_medium_valid. - assert (0 <= decode_large x < b^(2 * k)) by (autorewrite with pull_Zpow zsimplify in *; omega). - assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith omega. - rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by omega. - rewrite <- μ'_eq. - pull_zlike_decode; cbv zeta; pull_zlike_decode. (* Extra [cbv iota; pull_zlike_decode] to work around bug #4165 (https://coq.inria.fr/bugs/show_bug.cgi?id=4165) in 8.4 *) - subst pr; split; [ reflexivity | exact _ ]. - Defined. - - Definition barrett_reduce_function : LargeT -> SmallT - := Eval cbv [proj1_sig barrett_reduce] - in fun x => proj1_sig (barrett_reduce x). - Lemma barrett_reduce_correct x - : medium_valid x - -> decode_small (barrett_reduce_function x) = (decode_large x) mod m - /\ small_valid (barrett_reduce_function x). - Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg μ'_eq μ'_good μ_good. - exact (proj2_sig (barrett_reduce x)). - Qed. -End barrett. - -Module BarrettBundled. - Class BarrettParameters := - { m : Z; - b : Z; - k : Z; - offset : Z; - μ := b ^ (2 * k) / m; - ops : ZLikeOps (b ^ (k + offset)) (b ^ (k - offset)) m; - μ' : SmallT }. - Global Existing Instance ops. - - Class BarrettParametersCorrect {params : BarrettParameters} := - { m_pos : 0 < m; - base_pos : 0 < b; - offset_nonneg : 0 <= offset; - k_big_enough : offset <= k; - m_small : 3 * m <= b ^ (k + offset); - m_large : b ^ (k - offset) <= m + 1; - props : ZLikeProperties ops; - μ'_good : small_valid μ'; - μ'_eq : decode_small μ' = μ }. - Global Arguments BarrettParametersCorrect : clear implicits. - Global Existing Instance props. - - Module Export functions. - Definition barrett_reduce_function_bundled {params : BarrettParameters} - : LargeT -> SmallT - := barrett_reduce_function m b k offset μ'. - Definition barrett_reduce_correct_bundled {params : BarrettParameters} {params_proofs : BarrettParametersCorrect params} - : forall x, medium_valid x - -> decode_small (barrett_reduce_function_bundled x) = (decode_large x) mod m - /\ small_valid (barrett_reduce_function_bundled x) - := @barrett_reduce_correct - m b k μ offset - m_pos base_pos eq_refl offset_nonneg - k_big_enough m_small m_large - ops props μ' μ'_good μ'_eq. - End functions. -End BarrettBundled. -Export BarrettBundled.functions. -Global Existing Instance BarrettBundled.ops. -Global Arguments BarrettBundled.BarrettParametersCorrect : clear implicits. -Global Existing Instance BarrettBundled.props. diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v deleted file mode 100644 index 359b4313b..000000000 --- a/src/LegacyArithmetic/BaseSystem.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. -Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Notations. -Require Export Crypto.Util.FixCoqMistakes. -Import Nat. - -Local Open Scope Z. - -Class BaseVector (base : list Z):= { - base_positive : forall b, In b base -> b > 0; (* nonzero would probably work too... *) - b0_1 : forall x, nth_default x base 0 = 1; (** TODO(jadep,jgross): change to [nth_error base 0 = Some 1], then use [nth_error_value_eq_nth_default] to prove a [forall x, nth_default x base 0 = 1] as a lemma *) - base_good : - forall i j, (i+j < length base)%nat -> - let b := nth_default 0 base in - let r := (b i * b j) / b (i+j)%nat in - b i * b j = r * b (i+j)%nat -}. - -Section BaseSystem. - Context (base : list Z). - (** [BaseSystem] implements an constrained positional number system. - A wide variety of bases are supported: the base coefficients are not - required to be powers of 2, and it is NOT necessarily the case that - $b_{i+j} = b_i b_j$. Implementations of addition and multiplication are - provided, with focus on near-optimal multiplication performance on - non-trivial but small operands: maybe 10 32-bit integers or so. This - module does not handle carries automatically: if no restrictions are put - on the use of a [BaseSystem], each digit is unbounded. This has nothing - to do with modular arithmetic either. - *) - Definition digits : Type := list Z. - - Definition accumulate p acc := fst p * snd p + acc. - Definition decode' bs u := fold_right accumulate 0 (combine u bs). - Definition decode := decode' base. - Definition mul_each u := map (Z.mul u). -End BaseSystem. diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v deleted file mode 100644 index 042fdb270..000000000 --- a/src/LegacyArithmetic/BaseSystemProofs.v +++ /dev/null @@ -1,134 +0,0 @@ -Require Import Coq.Lists.List Coq.micromega.Psatz. -Require Import Crypto.Util.ListUtil. -Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. -Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.LegacyArithmetic.BaseSystem. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Notations. -Import Morphisms. -Local Open Scope Z. - -Local Hint Extern 1 (@eq Z _ _) => ring. - -Section BaseSystemProofs. - Context `(base_vector : BaseVector). - - Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us). - Proof using Type. - unfold decode'; intros; f_equal; apply combine_truncate_l. - Qed. - - Lemma decode'_splice : forall xs ys bs, - decode' bs (xs ++ ys) = - decode' (firstn (length xs) bs) xs + decode' (skipn (length xs) bs) ys. - Proof using Type. - unfold decode'. - induction xs; destruct ys, bs; boring. - + rewrite combine_truncate_r. - do 2 rewrite Z.add_0_r; auto. - + unfold accumulate. - apply Z.add_assoc. - Qed. - - Lemma decode_nil : forall bs, decode' bs nil = 0. - Proof using Type. - - auto. - Qed. - Hint Rewrite decode_nil. - - Lemma decode_base_nil : forall us, decode' nil us = 0. - Proof using Type. - intros; rewrite decode'_truncate; auto. - Qed. - - Lemma mul_each_rep : forall bs u vs, - decode' bs (mul_each u vs) = u * decode' bs vs. - Proof using Type. - unfold decode', accumulate; induction bs; destruct vs; boring; ring. - Qed. - - Lemma base_eq_1cons: base = 1 :: skipn 1 base. - Proof using Type*. - pose proof (b0_1 0) as H. - destruct base; compute in H; try discriminate; boring. - Qed. - - Lemma decode'_cons : forall x1 x2 xs1 xs2, - decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2. - Proof using Type. - unfold decode', accumulate; boring; ring. - Qed. - Hint Rewrite decode'_cons. - - Lemma decode_cons : forall x us, - decode base (x :: us) = x + decode base (0 :: us). - Proof using Type*. - unfold decode; intros. - rewrite base_eq_1cons. - autorewrite with core; ring_simplify; auto. - Qed. - - Lemma decode'_map_mul : forall v xs bs, - decode' (map (Z.mul v) bs) xs = - Z.mul v (decode' bs xs). - Proof using Type. - unfold decode'. - induction xs; destruct bs; boring. - unfold accumulate; simpl; nia. - Qed. - - Lemma decode_map_mul : forall v xs, - decode (map (Z.mul v) base) xs = - Z.mul v (decode base xs). - Proof using Type. - unfold decode; intros; apply decode'_map_mul. - Qed. - - Lemma mul_each_base : forall us bs c, - decode' bs (mul_each c us) = decode' (mul_each c bs) us. - Proof using Type. - induction us; destruct bs; boring; ring. - Qed. - - Hint Rewrite (@nth_default_nil Z). - Hint Rewrite (@firstn_nil Z). - Hint Rewrite (@skipn_nil Z). - - Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys. - Proof using Type. - boring. - Qed. - Hint Rewrite peel_decode. - - Hint Rewrite plus_0_r. - - Lemma set_higher : forall bs vs x, - decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x. - Proof using Type. - intros. - rewrite !decode'_splice. - cbv [decode' nth_default]; break_match; ring_simplify; - match goal with - | [H:_ |- _] => unique pose proof (nth_error_error_length _ _ _ H) - | [H:_ |- _] => unique pose proof (nth_error_value_length _ _ _ _ H) - end; - repeat match goal with - | _ => solve [simpl;ring_simplify; trivial] - | _ => progress ring_simplify - | _ => progress rewrite skipn_all by trivial - | _ => progress rewrite combine_nil_r - | _ => progress rewrite firstn_all2 by trivial - end. - rewrite (combine_truncate_r vs bs); apply (f_equal2 Z.add); trivial; []. - unfold combine; break_match. - { let Heql := match goal with H : _ = nil |- _ => H end in - apply (f_equal (@length _)) in Heql; simpl length in Heql; rewrite skipn_length in Heql; omega. } - { cbv -[Z.add Z.mul]; ring_simplify; f_equal. - assert (HH: nth_error (z0 :: l) 0 = Some z) by - ( - pose proof @nth_error_skipn _ (length vs) bs 0; - rewrite plus_0_r in *; - congruence); simpl in HH; congruence. } - Qed. -End BaseSystemProofs. diff --git a/src/LegacyArithmetic/Double/Core.v b/src/LegacyArithmetic/Double/Core.v deleted file mode 100644 index 53f20801c..000000000 --- a/src/LegacyArithmetic/Double/Core.v +++ /dev/null @@ -1,253 +0,0 @@ -(*** Implementing Large Bounded Arithmetic via pairs *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.LetIn. -Import Bug5107WorkAround. - -Require Crypto.LegacyArithmetic.BaseSystem. -Require Crypto.LegacyArithmetic.Pow2Base. - -Local Open Scope nat_scope. -Local Open Scope Z_scope. -Local Open Scope type_scope. - -Local Coercion Z.of_nat : nat >-> Z. -Local Notation eta x := (fst x, snd x). - -(** The list is low to high; the tuple is low to high *) -Definition tuple_decoder {n W} {decode : decoder n W} {k : nat} : decoder (k * n) (tuple W k) - := {| decode w := BaseSystem.decode (Pow2Base.base_from_limb_widths (List.repeat n k)) - (List.map decode (List.rev (Tuple.to_list _ w))) |}. -Global Arguments tuple_decoder : simpl never. -Hint Extern 3 (decoder _ (tuple ?W ?k)) => let kv := (eval simpl in (Z.of_nat k)) in apply (fun n decode => (@tuple_decoder n W decode k : decoder (kv * n) (tuple W k))) : typeclass_instances. - -Section ripple_carry_definitions. - (** tuple is high to low ([to_list] reverses) *) - Fixpoint ripple_carry_tuple' {T} (f : T -> T -> bool -> bool * T) k - : forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k - := match k return forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k with - | O => f - | S k' => fun xss yss carry => dlet xss := xss in - dlet yss := yss in - let (xs, x) := eta xss in - let (ys, y) := eta yss in - dlet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in - let (carry, zs) := eta addv in - dlet fxy := (f x y carry) in - let (carry, z) := eta fxy in - (carry, (zs, z)) - end. - - Definition ripple_carry_tuple {T} (f : T -> T -> bool -> bool * T) k - : forall (xs ys : tuple T k) (carry : bool), bool * tuple T k - := match k return forall (xs ys : tuple T k) (carry : bool), bool * tuple T k with - | O => fun xs ys carry => (carry, tt) - | S k' => ripple_carry_tuple' f k' - end. -End ripple_carry_definitions. - -Global Instance ripple_carry_adc - {W} (adc : add_with_carry W) {k} - : add_with_carry (tuple W k) - := { adc := ripple_carry_tuple adc k }. - -Global Instance ripple_carry_subc - {W} (subc : sub_with_carry W) {k} - : sub_with_carry (tuple W k) - := { subc := ripple_carry_tuple subc k }. - -(** constructions on [tuple W 2] *) -Section tuple2. - Section select_conditional. - Context {W} - {selc : select_conditional W}. - - Definition select_conditional_double (b : bool) (x : tuple W 2) (y : tuple W 2) : tuple W 2 - := dlet x := x in - dlet y := y in - let (x1, x2) := eta x in - let (y1, y2) := eta y in - (selc b x1 y1, selc b x2 y2). - - Global Instance selc_double : select_conditional (tuple W 2) - := { selc := select_conditional_double }. - End select_conditional. - - Section load_immediate. - Context (n : Z) {W} - {ldi : load_immediate W}. - - Definition load_immediate_double (r : Z) : tuple W 2 - := (ldi (r mod 2^n), ldi (r / 2^n)). - - (** Require a [decoder] instance to aid typeclass search in - resolving [n] *) - Global Instance ldi_double {decode : decoder n W} : load_immediate (tuple W 2) - := { ldi := load_immediate_double }. - End load_immediate. - - Section bitwise_or. - Context {W} - {or : bitwise_or W}. - - Definition bitwise_or_double (x : tuple W 2) (y : tuple W 2) : tuple W 2 - := dlet x := x in - dlet y := y in - let (x1, x2) := eta x in - let (y1, y2) := eta y in - (or x1 y1, or x2 y2). - - Global Instance or_double : bitwise_or (tuple W 2) - := { or := bitwise_or_double }. - End bitwise_or. - - Section bitwise_and. - Context {W} - {and : bitwise_and W}. - - Definition bitwise_and_double (x : tuple W 2) (y : tuple W 2) : tuple W 2 - := dlet x := x in - dlet y := y in - let (x1, x2) := eta x in - let (y1, y2) := eta y in - (and x1 y1, and x2 y2). - - Global Instance and_double : bitwise_and (tuple W 2) - := { and := bitwise_and_double }. - End bitwise_and. - - Section spread_left. - Context (n : Z) {W} - {ldi : load_immediate W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W}. - - Definition spread_left_from_shift (r : W) (count : Z) : tuple W 2 - := dlet r := r in - (shl r count, if count =? 0 then ldi 0 else shr r (n - count)). - - (** Require a [decoder] instance to aid typeclass search in - resolving [n] *) - Global Instance sprl_from_shift {decode : decoder n W} : spread_left_immediate W - := { sprl := spread_left_from_shift }. - End spread_left. - - Section shl_shr. - Context (n : Z) {W} - {ldi : load_immediate W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {or : bitwise_or W}. - - Definition shift_left_immediate_double (r : tuple W 2) (count : Z) : tuple W 2 - := dlet r := r in - let (r1, r2) := eta r in - (if count =? 0 - then r1 - else if count <? n - then shl r1 count - else ldi 0, - if count =? 0 - then r2 - else if count <? n - then or (shr r1 (n - count)) (shl r2 count) - else shl r1 (count - n)). - - Definition shift_right_immediate_double (r : tuple W 2) (count : Z) : tuple W 2 - := dlet r := r in - let (r1, r2) := eta r in - (if count =? 0 - then r1 - else if count <? n - then or (shr r1 count) (shl r2 (n - count)) - else shr r2 (count - n), - if count =? 0 - then r2 - else if count <? n - then shr r2 count - else ldi 0). - - (** Require a [decoder] instance to aid typeclass search in - resolving [n] *) - Global Instance shl_double {decode : decoder n W} : shift_left_immediate (tuple W 2) - := { shl := shift_left_immediate_double }. - Global Instance shr_double {decode : decoder n W} : shift_right_immediate (tuple W 2) - := { shr := shift_right_immediate_double }. - End shl_shr. - - Section shrd. - Context (n : Z) {W} - {ldi : load_immediate W} - {shrd : shift_right_doubleword_immediate W}. - - Definition shift_right_doubleword_immediate_double (high low : tuple W 2) (count : Z) : tuple W 2 - := dlet high := high in - dlet low := low in - let (high1, high2) := eta high in - let (low1, low2) := eta low in - (if count =? 0 - then low1 - else if count <? n - then shrd low2 low1 count - else if count <? 2 * n - then shrd high1 low2 (count - n) - else shrd high2 high1 (count - 2 * n), - if count =? 0 - then low2 - else if count <? n - then shrd high1 low2 count - else if count <? 2 * n - then shrd high2 high1 (count - n) - else shrd (ldi 0) high2 (count - 2 * n)). - - (** Require a [decoder] instance to aid typeclass search in - resolving [n] *) - Global Instance shrd_double {decode : decoder n W} : shift_right_doubleword_immediate (tuple W 2) - := { shrd := shift_right_doubleword_immediate_double }. - End shrd. - - Section double_from_half. - Context {half_n : Z} {W} - {mulhwll : multiply_low_low W} - {mulhwhl : multiply_high_low W} - {mulhwhh : multiply_high_high W} - {adc : add_with_carry W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {ldi : load_immediate W}. - - Definition mul_double (a b : W) : tuple W 2 - := dlet a := a in - dlet b := b in - let out : tuple W 2 := (mulhwll a b, mulhwhh a b) in - dlet out := out in - dlet tmp := mulhwhl a b in - dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in - let (_, out) := eta addv in - dlet tmp := mulhwhl b a in - dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in - let (_, out) := eta addv in - out. - - (** Require a dummy [decoder] for these instances to allow - typeclass inference of the [half_n] argument *) - Global Instance mul_double_multiply {decode : decoder (2 * half_n) W} : multiply_double W - := { muldw a b := mul_double a b }. - End double_from_half. - - Global Instance mul_double_multiply_low_low {W} {muldw : multiply_double W} - : multiply_low_low (tuple W 2) - := { mulhwll a b := muldw (fst a) (fst b) }. - Global Instance mul_double_multiply_high_low {W} {muldw : multiply_double W} - : multiply_high_low (tuple W 2) - := { mulhwhl a b := muldw (snd a) (fst b) }. - Global Instance mul_double_multiply_high_high {W} {muldw : multiply_double W} - : multiply_high_high (tuple W 2) - := { mulhwhh a b := muldw (snd a) (snd b) }. -End tuple2. - -Global Arguments mul_double half_n {_ _ _ _ _ _ _} _ _. diff --git a/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v deleted file mode 100644 index 8588836ee..000000000 --- a/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v +++ /dev/null @@ -1,32 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.LandLorShiftBounds. -Require Import Crypto.Util.Tactics.BreakMatch. - -Local Open Scope Z_scope. - -Section bitwise_or. - Context {n W} - {decode : decoder n W} - {is_decode : is_decode decode} - {or : bitwise_or W} - {is_or : is_bitwise_or or}. - - Global Instance is_bitwise_or_double - : is_bitwise_or or_double. - Proof using Type*. - constructor; intros x y. - destruct n as [|p|]. - { rewrite !(tuple_decoder_n_O (W:=W) 2); easy. } - { assert (0 <= Z.lor (decode (fst x)) (decode (fst y)) < 2^Z.pos p) by auto with zarith. - rewrite (tuple_decoder_2 x), (tuple_decoder_2 y), (tuple_decoder_2 (or_double x y)) - by apply Zle_0_pos. - push_decode. - apply Z.bits_inj'; intros; autorewrite with Ztestbit. - break_match; Z.ltb_to_lt; autorewrite with Ztestbit; reflexivity. } - { rewrite !(tuple_decoder_n_neg (W:=W) 2); easy. } - Qed. -End bitwise_or. diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v deleted file mode 100644 index 5b3445208..000000000 --- a/src/LegacyArithmetic/Double/Proofs/Decode.v +++ /dev/null @@ -1,188 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.Notations. - -Require Crypto.LegacyArithmetic.Pow2Base. -Require Crypto.LegacyArithmetic.Pow2BaseProofs. - -Local Open Scope nat_scope. -Local Open Scope type_scope. - -Local Coercion Z.of_nat : nat >-> Z. - -Import BoundedRewriteNotations. -Local Open Scope Z_scope. - -Section decode. - Context {n W} {decode : decoder n W}. - Section with_k. - Context {k : nat}. - Local Notation limb_widths := (List.repeat n k). - - Lemma decode_bounded {isdecode : is_decode decode} w - : 0 <= n -> Pow2Base.bounded limb_widths (List.map decode (rev (to_list k w))). - Proof using Type. - intro. - eapply Pow2BaseProofs.bounded_uniform; try solve [ eauto using repeat_spec ]. - { distr_length. } - { intros z H'. - apply in_map_iff in H'. - destruct H' as [? [? H'] ]; subst; apply decode_range. } - Qed. - - (** TODO: Clean up this proof *) - Global Instance tuple_is_decode {isdecode : is_decode decode} - : is_decode (tuple_decoder (k := k)). - Proof using Type. - unfold tuple_decoder; hnf; simpl. - intro w. - destruct (zerop k); [ subst | ]. - { cbv; intuition congruence. } - assert (0 <= n) - by (destruct k as [ | [|] ]; [ omega | | destruct w ]; - eauto using decode_exponent_nonnegative). - replace (2^(k * n)) with (Pow2Base.upper_bound limb_widths) - by (erewrite Pow2BaseProofs.upper_bound_uniform by eauto using repeat_spec; distr_length). - apply Pow2BaseProofs.decode_upper_bound; auto using decode_bounded. - { intros ? H'. - apply repeat_spec in H'; omega. } - { distr_length. } - Qed. - End with_k. - - Local Arguments Pow2Base.base_from_limb_widths : simpl never. - Local Arguments List.repeat : simpl never. - Local Arguments Z.mul !_ !_. - Lemma tuple_decoder_S {k} w : 0 <= n -> (tuple_decoder (k := S (S k)) w = tuple_decoder (k := S k) (fst w) + (decode (snd w) << (S k * n)))%Z. - Proof using Type. - intro Hn. - destruct w as [? w]; simpl. - replace (decode w) with (decode w * 1 + 0)%Z by omega. - rewrite map_app, map_cons, map_nil. - erewrite Pow2BaseProofs.decode_shift_uniform_app by (eauto using repeat_spec; distr_length). - distr_length. - autorewrite with push_skipn natsimplify push_firstn. - reflexivity. - Qed. - Global Instance tuple_decoder_O w : tuple_decoder (k := 1) w =~> decode w. - Proof using Type. - cbv [tuple_decoder LegacyArithmetic.BaseSystem.decode LegacyArithmetic.BaseSystem.decode' LegacyArithmetic.BaseSystem.accumulate Pow2Base.base_from_limb_widths repeat]. - simpl; hnf; lia. - Qed. - Global Instance tuple_decoder_m1 w : tuple_decoder (k := 0) w =~> 0. - Proof using Type. reflexivity. Qed. - - Lemma tuple_decoder_n_neg k w {H : is_decode decode} : n <= 0 -> tuple_decoder (k := k) w =~> 0. - Proof using Type. - pose proof (tuple_is_decode w) as H'; hnf in H'. - intro; assert (k * n <= 0) by nia. - assert (2^(k * n) <= 2^0) by (apply Z.pow_le_mono_r; omega). - simpl in *; hnf. - omega. - Qed. - Lemma tuple_decoder_O_ind_prod - (P : forall n, decoder n W -> Type) - (P_ext : forall n (a b : decoder n W), (forall x, a x = b x) -> P _ a -> P _ b) - : (P _ (tuple_decoder (k := 1)) -> P _ decode) - * (P _ decode -> P _ (tuple_decoder (k := 1))). - Proof using Type. - unfold tuple_decoder, BaseSystem.decode, BaseSystem.decode', BaseSystem.accumulate, Pow2Base.base_from_limb_widths, repeat. - simpl; hnf. - rewrite Z.mul_1_l. - split; apply P_ext; simpl; intro; autorewrite with zsimplify_const; reflexivity. - Qed. - - Global Instance tuple_decoder_2' w : (0 <= n)%bounded_rewrite -> tuple_decoder (k := 2) w <~= (decode (fst w) + decode (snd w) << (1%nat * n))%Z. - Proof using Type. - intros; rewrite !tuple_decoder_S, !tuple_decoder_O by assumption. - reflexivity. - Qed. - Global Instance tuple_decoder_2 w : (0 <= n)%bounded_rewrite -> tuple_decoder (k := 2) w <~= (decode (fst w) + decode (snd w) << n)%Z. - Proof using Type. - intros; rewrite !tuple_decoder_S, !tuple_decoder_O by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. -End decode. - -Global Arguments tuple_decoder : simpl never. -Local Opaque tuple_decoder. - -Global Instance tuple_decoder_n_O - {W} {decode : decoder 0 W} - {is_decode : is_decode decode} - : forall k w, tuple_decoder (k := k) w =~> 0. -Proof. intros; apply tuple_decoder_n_neg; easy. Qed. - -Lemma is_add_with_carry_1tuple {n W decode adc} - (H : @is_add_with_carry n W decode adc) - : @is_add_with_carry (1 * n) W (@tuple_decoder n W decode 1) adc. -Proof. - apply tuple_decoder_O_ind_prod; try assumption. - intros ??? ext [H0 H1]; apply Build_is_add_with_carry'. - intros x y c; specialize (H0 x y c); specialize (H1 x y c). - rewrite <- !ext; split; assumption. -Qed. - -Hint Extern 1 (@is_add_with_carry _ _ (@tuple_decoder ?n ?W ?decode 1) ?adc) -=> apply (@is_add_with_carry_1tuple n W decode adc) : typeclass_instances. - -Hint Resolve (fun n W decode pf => (@tuple_is_decode n W decode 2 pf : @is_decode (2 * n) (tuple W 2) (@tuple_decoder n W decode 2))) : typeclass_instances. -Hint Extern 3 (@is_decode _ (tuple ?W ?k) _) => let kv := (eval simpl in (Z.of_nat k)) in apply (fun n decode pf => (@tuple_is_decode n W decode k pf : @is_decode (kv * n) (tuple W k) (@tuple_decoder n W decode k : decoder (kv * n)%Z (tuple W k)))) : typeclass_instances. - -Hint Rewrite @tuple_decoder_S @tuple_decoder_O @tuple_decoder_m1 @tuple_decoder_n_O using solve [ auto with zarith ] : simpl_tuple_decoder. -Hint Rewrite Z.mul_1_l : simpl_tuple_decoder. -Hint Rewrite - (fun n W (decode : decoder n W) w pf => (@tuple_decoder_S n W decode 0 w pf : @Interface.decode (2 * n) (tuple W 2) (@tuple_decoder n W decode 2) w = _)) - (fun n W (decode : decoder n W) w pf => (@tuple_decoder_S n W decode 0 w pf : @Interface.decode (2 * n) (W * W) (@tuple_decoder n W decode 2) w = _)) - (fun n W decode w => @tuple_decoder_m1 n W decode w : @Interface.decode (Z.of_nat 0 * n) unit (@tuple_decoder n W decode 0) w = _) - using solve [ auto with zarith ] - : simpl_tuple_decoder. - -Hint Rewrite @tuple_decoder_S @tuple_decoder_O @tuple_decoder_m1 using solve [ auto with zarith ] : simpl_tuple_decoder. - -Global Instance tuple_decoder_mod : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))), - tuple_decoder (k := S k) (fst w) <~= tuple_decoder w mod 2^(S k * n). -Proof. - intros n W decode k isdecode w. - pose proof (snd w). - assert (0 <= n) by eauto using decode_exponent_nonnegative. - assert (0 <= (S k) * n) by nia. - assert (0 <= tuple_decoder (k := S k) (fst w) < 2^(S k * n)) by apply decode_range. - autorewrite with simpl_tuple_decoder Zshift_to_pow zsimplify. - reflexivity. -Qed. - -Global Instance tuple_decoder_div : forall {n W} {decode : decoder n W} {k} {isdecode : is_decode decode} (w : tuple W (S (S k))), - decode (snd w) <~= tuple_decoder w / 2^(S k * n). -Proof. - intros n W decode k isdecode w. - pose proof (snd w). - assert (0 <= n) by eauto using decode_exponent_nonnegative. - assert (0 <= (S k) * n) by nia. - assert (0 <= k * n) by nia. - assert (0 < 2^n) by auto with zarith. - assert (0 <= tuple_decoder (k := S k) (fst w) < 2^(S k * n)) by apply decode_range. - autorewrite with simpl_tuple_decoder Zshift_to_pow zsimplify. - reflexivity. -Qed. - -Global Instance tuple2_decoder_mod : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2), - decode (fst w) <~= tuple_decoder w mod 2^n. -Proof. - intros n W decode isdecode w. - generalize (@tuple_decoder_mod n W decode 0 isdecode w). - autorewrite with simpl_tuple_decoder; trivial. -Qed. - -Global Instance tuple2_decoder_div : forall {n W} {decode : decoder n W} {isdecode : is_decode decode} (w : tuple W 2), - decode (snd w) <~= tuple_decoder w / 2^n. -Proof. - intros n W decode isdecode w. - generalize (@tuple_decoder_div n W decode 0 isdecode w). - autorewrite with simpl_tuple_decoder; trivial. -Qed. diff --git a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v deleted file mode 100644 index 13847b50a..000000000 --- a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v +++ /dev/null @@ -1,32 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. - -Local Open Scope Z_scope. -Local Opaque tuple_decoder. -Local Arguments Z.mul !_ !_. - -Section load_immediate. - Context {n W} - {decode : decoder n W} - {is_decode : is_decode decode} - {ldi : load_immediate W} - {is_ldi : is_load_immediate ldi}. - - Global Instance is_load_immediate_double - : is_load_immediate (ldi_double n). - Proof using Type*. - intros x H; hnf in H. - pose proof (decode_exponent_nonnegative decode (ldi x)). - assert (0 <= x mod 2^n < 2^n) by auto with zarith. - assert (x / 2^n < 2^n) - by (apply Z.div_lt_upper_bound; autorewrite with pull_Zpow zsimplify; auto with zarith). - assert (0 <= x / 2^n < 2^n) by (split; Z.zero_bounds). - unfold ldi_double, load_immediate_double; simpl. - autorewrite with simpl_tuple_decoder Zshift_to_pow; simpl; push_decode. - autorewrite with zsimplify; reflexivity. - Qed. -End load_immediate. diff --git a/src/LegacyArithmetic/Double/Proofs/Multiply.v b/src/LegacyArithmetic/Double/Proofs/Multiply.v deleted file mode 100644 index ebe19cc46..000000000 --- a/src/LegacyArithmetic/Double/Proofs/Multiply.v +++ /dev/null @@ -1,135 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.LegacyArithmetic.Double.Proofs.SpreadLeftImmediate. -Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Modulo. -Require Import Crypto.Util.Tactics.SimplifyProjections. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Prod. -Import Bug5107WorkAround. -Import BoundedRewriteNotations. - -Local Open Scope Z_scope. - -Local Opaque tuple_decoder. - -Lemma decode_mul_double_iff - {n W} - {decode : decoder n W} - {muldw : multiply_double W} - {isdecode : is_decode decode} - : is_mul_double muldw - <-> (forall x y, tuple_decoder (muldw x y) = (decode x * decode y)%Z). -Proof. - rewrite is_mul_double_alt by assumption. - split; intros H x y; specialize (H x y); revert H; - pose proof (decode_range x); pose proof (decode_range y); - assert (0 <= decode x * decode y < 2^n * 2^n) by nia; - assert (0 <= n) by eauto using decode_exponent_nonnegative; - autorewrite with simpl_tuple_decoder; - simpl; intro H'; rewrite H'; - Z.rewrite_mod_small; reflexivity. -Qed. - -Global Instance decode_mul_double - {n W} - {decode : decoder n W} - {muldw : multiply_double W} - {isdecode : is_decode decode} - {ismuldw : is_mul_double muldw} - : forall x y, tuple_decoder (muldw x y) <~=~> (decode x * decode y)%Z - := proj1 decode_mul_double_iff _. - -Section tuple2. - Local Arguments Z.pow !_ !_. - Local Arguments Z.mul !_ !_. - - Local Opaque ripple_carry_adc. - Section full_from_half. - Context {W} - {mulhwll : multiply_low_low W} - {mulhwhl : multiply_high_low W} - {mulhwhh : multiply_high_high W} - {adc : add_with_carry W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {half_n : Z} - {ldi : load_immediate W} - {decode : decoder (2 * half_n) W} - {ismulhwll : is_mul_low_low half_n mulhwll} - {ismulhwhl : is_mul_high_low half_n mulhwhl} - {ismulhwhh : is_mul_high_high half_n mulhwhh} - {isadc : is_add_with_carry adc} - {isshl : is_shift_left_immediate shl} - {isshr : is_shift_right_immediate shr} - {isldi : is_load_immediate ldi} - {isdecode : is_decode decode}. - - Local Arguments Z.mul !_ !_. - - Lemma decode_mul_double_mod x y - : (tuple_decoder (mul_double half_n x y) = (decode x * decode y) mod (2^(2 * half_n) * 2^(2*half_n)))%Z. - Proof using Type*. - assert (0 <= 2 * half_n) by eauto using decode_exponent_nonnegative. - assert (0 <= half_n) by omega. - unfold mul_double, Let_In. - push_decode; autorewrite with simpl_tuple_decoder; simplify_projections. - autorewrite with zsimplify Zshift_to_pow push_Zpow. - rewrite !spread_left_from_shift_half_correct. - push_decode. - generalize_decode_var. - simpl in *. - autorewrite with push_Zpow in *. - repeat autorewrite with Zshift_to_pow zsimplify push_Zpow. - rewrite <- !(Z.mul_mod_distr_r_full _ _ (_^_ * _^_)), ?Z.mul_assoc. - Z.rewrite_mod_small. - push_Zmod; pull_Zmod. - apply f_equal2; [ | reflexivity ]. - Z.div_mod_to_quot_rem_in_goal; nia. - Qed. - - Lemma decode_mul_double_function x y - : tuple_decoder (mul_double half_n x y) = (decode x * decode y)%Z. - Proof using Type*. - rewrite decode_mul_double_mod; generalize_decode_var. - simpl in *; Z.rewrite_mod_small; reflexivity. - Qed. - - Global Instance mul_double_is_multiply_double : is_mul_double mul_double_multiply. - Proof using Type*. - apply decode_mul_double_iff; apply decode_mul_double_function. - Qed. - End full_from_half. - - Section half_from_full. - Context {n W} - {decode : decoder n W} - {muldw : multiply_double W} - {isdecode : is_decode decode} - {ismuldw : is_mul_double muldw}. - - Local Ltac t := - hnf; intros [??] [??]; - assert (0 <= n) by eauto using decode_exponent_nonnegative; - assert (0 < 2^n) by auto with zarith; - assert (forall x y, 0 <= x < 2^n -> 0 <= y < 2^n -> 0 <= x * y < 2^n * 2^n) by auto with zarith; - simpl @Interface.mulhwhh; simpl @Interface.mulhwhl; simpl @Interface.mulhwll; - rewrite decode_mul_double; autorewrite with simpl_tuple_decoder Zshift_to_pow zsimplify push_Zpow; - Z.rewrite_mod_small; - try reflexivity. - - Global Instance mul_double_is_multiply_low_low : is_mul_low_low n mul_double_multiply_low_low. - Proof using Type*. t. Qed. - Global Instance mul_double_is_multiply_high_low : is_mul_high_low n mul_double_multiply_high_low. - Proof using Type*. t. Qed. - Global Instance mul_double_is_multiply_high_high : is_mul_high_high n mul_double_multiply_high_high. - Proof using Type*. t. Qed. - End half_from_full. -End tuple2. diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v deleted file mode 100644 index b2d53a33a..000000000 --- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v +++ /dev/null @@ -1,203 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SimplifyProjections. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Prod. -Import Bug5107WorkAround. -Import BoundedRewriteNotations. - -Local Coercion Z.of_nat : nat >-> Z. -Local Notation eta x := (fst x, snd x). - -Local Open Scope Z_scope. -Local Opaque tuple_decoder. - -Lemma ripple_carry_tuple_SS' {T} f k xss yss carry - : @ripple_carry_tuple T f (S (S k)) xss yss carry - = dlet xss := xss in - dlet yss := yss in - let '(xs, x) := eta xss in - let '(ys, y) := eta yss in - dlet addv := (@ripple_carry_tuple _ f (S k) xs ys carry) in - let '(carry, zs) := eta addv in - dlet fxy := (f x y carry) in - let '(carry, z) := eta fxy in - (carry, (zs, z)). -Proof. reflexivity. Qed. - -Lemma ripple_carry_tuple_SS {T} f k xss yss carry - : @ripple_carry_tuple T f (S (S k)) xss yss carry - = let '(xs, x) := eta xss in - let '(ys, y) := eta yss in - let '(carry, zs) := eta (@ripple_carry_tuple _ f (S k) xs ys carry) in - let '(carry, z) := eta (f x y carry) in - (carry, (zs, z)). -Proof. - rewrite ripple_carry_tuple_SS'. - eta_expand. - reflexivity. -Qed. - -Lemma carry_is_good (n z0 z1 k : Z) - : 0 <= n -> - 0 <= k -> - (z1 + z0 >> k) >> n = (z0 + z1 << k) >> (k + n) /\ - (z0 mod 2 ^ k + ((z1 + z0 >> k) mod 2 ^ n) << k)%Z = (z0 + z1 << k) mod (2 ^ k * 2 ^ n). -Proof. - intros. - assert (0 < 2 ^ n) by auto with zarith. - assert (0 < 2 ^ k) by auto with zarith. - assert (0 < 2^n * 2^k) by nia. - autorewrite with Zshift_to_pow push_Zpow. - rewrite <- (Zmod_small ((z0 mod _) + _) (2^k * 2^n)) by (Z.div_mod_to_quot_rem_in_goal; nia). - rewrite <- !Z.mul_mod_distr_r by lia. - rewrite !(Z.mul_comm (2^k)); pull_Zmod. - split; [ | apply f_equal2 ]; - Z.div_mod_to_quot_rem_in_goal; nia. -Qed. -Section carry_sub_is_good. - Context (n k z0 z1 : Z) - (Hn : 0 <= n) - (Hk : 0 <= k) - (Hz1 : -2^n < z1 < 2^n) - (Hz0 : -2^k <= z0 < 2^k). - - Lemma carry_sub_is_good_carry - : ((z1 - if z0 <? 0 then 1 else 0) <? 0) = ((z0 + z1 << k) <? 0). - Proof using Hk Hz0. - clear n Hn Hz1. - assert (0 < 2 ^ k) by auto with zarith. - autorewrite with Zshift_to_pow. - repeat match goal with - | _ => progress break_match - | [ |- context[?x <? ?y] ] => destruct (x <? y) eqn:? - | _ => reflexivity - | _ => progress Z.ltb_to_lt - | [ |- true = false ] => exfalso - | [ |- false = true ] => exfalso - | [ |- False ] => nia - end. - Qed. - Lemma carry_sub_is_good_value - : (z0 mod 2 ^ k + ((z1 - if z0 <? 0 then 1 else 0) mod 2 ^ n) << k)%Z - = (z0 + z1 << k) mod (2 ^ k * 2 ^ n). - Proof using Type*. - assert (0 < 2 ^ n) by auto with zarith. - assert (0 < 2 ^ k) by auto with zarith. - assert (0 < 2^n * 2^k) by nia. - autorewrite with Zshift_to_pow push_Zpow. - rewrite <- (Zmod_small ((z0 mod _) + _) (2^k * 2^n)) by (Z.div_mod_to_quot_rem_in_goal; nia). - rewrite <- !Z.mul_mod_distr_r by lia. - rewrite !(Z.mul_comm (2^k)); pull_Zmod. - apply f_equal2; Z.div_mod_to_quot_rem_in_goal; break_match; Z.ltb_to_lt; try reflexivity; - match goal with - | [ q : Z |- _ = _ :> Z ] - => first [ cut (q = -1); [ intro; subst; ring | nia ] - | cut (q = 0); [ intro; subst; ring | nia ] - | cut (q = 1); [ intro; subst; ring | nia ] ] - end. - Qed. -End carry_sub_is_good. - -Definition carry_is_good_carry n z0 z1 k H0 H1 := proj1 (@carry_is_good n z0 z1 k H0 H1). -Definition carry_is_good_value n z0 z1 k H0 H1 := proj2 (@carry_is_good n z0 z1 k H0 H1). - -Section ripple_carry_adc. - Context {n W} {decode : decoder n W} (adc : add_with_carry W). - - Lemma ripple_carry_adc_SS k xss yss carry - : ripple_carry_adc (k := S (S k)) adc xss yss carry - = let '(xs, x) := eta xss in - let '(ys, y) := eta yss in - let '(carry, zs) := eta (ripple_carry_adc (k := S k) adc xs ys carry) in - let '(carry, z) := eta (adc x y carry) in - (carry, (zs, z)). - Proof using Type. apply ripple_carry_tuple_SS. Qed. - - Local Opaque Z.of_nat. - Global Instance ripple_carry_is_add_with_carry - : forall {k} - {isdecode : is_decode decode} - {is_adc : is_add_with_carry adc}, - is_add_with_carry (ripple_carry_adc (k := k) adc). - Proof using Type. - destruct k as [|k]; intros isdecode is_adc. - { constructor; simpl; intros; autorewrite with zsimplify; reflexivity. } - { induction k as [|k IHk]. - { cbv [ripple_carry_adc ripple_carry_tuple to_list]. - constructor; simpl @fst; simpl @snd; intros; - simpl; pull_decode; reflexivity. } - { apply Build_is_add_with_carry'; intros x y c. - assert (0 <= n) by (destruct x; eauto using decode_exponent_nonnegative). - assert (2^n <> 0) by auto with zarith. - assert (0 <= S k * n) by nia. - rewrite !tuple_decoder_S, !ripple_carry_adc_SS by assumption. - simplify_projections; push_decode; generalize_decode. - erewrite carry_is_good_carry, carry_is_good_value by lia. - autorewrite with pull_Zpow push_Zof_nat zsimplify Zshift_to_pow. - split; apply f_equal2; nia. } } - Qed. - -End ripple_carry_adc. - -Hint Extern 2 (@is_add_with_carry _ (tuple ?W ?k) (@tuple_decoder ?n _ ?decode _) (@ripple_carry_adc _ ?adc _)) -=> apply (@ripple_carry_is_add_with_carry n W decode adc k) : typeclass_instances. -Hint Resolve (fun n W decode adc isdecode isadc - => @ripple_carry_is_add_with_carry n W decode adc 2 isdecode isadc - : @is_add_with_carry (Z.of_nat 2 * n) (W * W) (@tuple_decoder n W decode 2) (@ripple_carry_adc W adc 2)) - : typeclass_instances. - -Section ripple_carry_subc. - Context {n W} {decode : decoder n W} (subc : sub_with_carry W). - - Lemma ripple_carry_subc_SS k xss yss carry - : ripple_carry_subc (k := S (S k)) subc xss yss carry - = let '(xs, x) := eta xss in - let '(ys, y) := eta yss in - let '(carry, zs) := eta (ripple_carry_subc (k := S k) subc xs ys carry) in - let '(carry, z) := eta (subc x y carry) in - (carry, (zs, z)). - Proof using Type. apply ripple_carry_tuple_SS. Qed. - - Local Opaque Z.of_nat. - Global Instance ripple_carry_is_sub_with_carry - : forall {k} - {isdecode : is_decode decode} - {is_subc : is_sub_with_carry subc}, - is_sub_with_carry (ripple_carry_subc (k := k) subc). - Proof using Type. - destruct k as [|k]; intros isdecode is_subc. - { constructor; repeat (intros [] || intro); autorewrite with simpl_tuple_decoder zsimplify; reflexivity. } - { induction k as [|k IHk]. - { cbv [ripple_carry_subc ripple_carry_tuple to_list]. - constructor; simpl @fst; simpl @snd; intros; - simpl; push_decode; autorewrite with zsimplify; reflexivity. } - { apply Build_is_sub_with_carry'; intros x y c. - assert (0 <= n) by (destruct x; eauto using decode_exponent_nonnegative). - assert (2^n <> 0) by auto with zarith. - assert (0 <= S k * n) by nia. - rewrite !tuple_decoder_S, !ripple_carry_subc_SS by assumption. - simplify_projections; push_decode; generalize_decode. - erewrite (carry_sub_is_good_carry (S k * n)), carry_sub_is_good_value by (break_match; lia). - autorewrite with pull_Zpow push_Zof_nat zsimplify Zshift_to_pow. - split; apply f_equal2; nia. } } - Qed. - -End ripple_carry_subc. - -Hint Extern 2 (@is_sub_with_carry _ (tuple ?W ?k) (@tuple_decoder ?n _ ?decode _) (@ripple_carry_subc _ ?subc _)) -=> apply (@ripple_carry_is_sub_with_carry n W decode subc k) : typeclass_instances. -Hint Resolve (fun n W decode subc isdecode issubc - => @ripple_carry_is_sub_with_carry n W decode subc 2 isdecode issubc - : @is_sub_with_carry (Z.of_nat 2 * n) (W * W) (@tuple_decoder n W decode 2) (@ripple_carry_subc W subc 2)) - : typeclass_instances. diff --git a/src/LegacyArithmetic/Double/Proofs/SelectConditional.v b/src/LegacyArithmetic/Double/Proofs/SelectConditional.v deleted file mode 100644 index 953acf056..000000000 --- a/src/LegacyArithmetic/Double/Proofs/SelectConditional.v +++ /dev/null @@ -1,25 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. - -Section select_conditional. - Context {n W} - {decode : decoder n W} - {is_decode : is_decode decode} - {selc : select_conditional W} - {is_selc : is_select_conditional selc}. - - Global Instance is_select_conditional_double - : is_select_conditional selc_double. - Proof using Type*. - intros b x y. - destruct n. - { rewrite !(tuple_decoder_n_O (W:=W) 2); now destruct b. } - { rewrite (tuple_decoder_2 x), (tuple_decoder_2 y), (tuple_decoder_2 (selc_double b x y)) - by apply Zle_0_pos. - push_decode. - now destruct b. } - { rewrite !(tuple_decoder_n_neg (W:=W) 2); now destruct b. } - Qed. -End select_conditional. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v deleted file mode 100644 index 1944f99b2..000000000 --- a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v +++ /dev/null @@ -1,43 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Definitions. - -Local Open Scope Z_scope. - -Local Opaque tuple_decoder. -Local Arguments Z.pow !_ !_. -Local Arguments Z.mul !_ !_. - -Section shl. - Context (n : Z) {W} - {ldi : load_immediate W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {or : bitwise_or W} - {decode : decoder n W} - {isdecode : is_decode decode} - {isldi : is_load_immediate ldi} - {isshl : is_shift_left_immediate shl} - {isshr : is_shift_right_immediate shr} - {isor : is_bitwise_or or}. - - Global Instance is_shift_left_immediate_double : is_shift_left_immediate (shl_double n). - Proof using Type*. - intros r count H; hnf in H. - assert (0 < 2^count) by auto with zarith. - assert (0 < 2^(n+count)) by auto with zarith. - assert (forall x, 0 <= Z.pow2_mod x n < 2^n) by auto with zarith. - unfold shl_double; simpl. - generalize (decode_range r). - pose proof (decode_range (fst r)). - pose proof (decode_range (snd r)). - assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by (simpl in *; auto with zarith). - assert (forall n', n <= n' -> 0 <= decode (fst r) < 2^n') by auto with zarith omega. - autorewrite with simpl_tuple_decoder; push_decode. - shift_left_right_t. - Qed. -End shl. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v deleted file mode 100644 index 98cf3cf9c..000000000 --- a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v +++ /dev/null @@ -1,50 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Testbit. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.Ztestbit. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Export Crypto.Util.ZUtil.ZSimplify.Autogenerated. -Require Export Crypto.Util.ZUtil.ZSimplify.Core. -Require Export Crypto.Util.ZUtil.ZSimplify.Simple. -Require Export Crypto.Util.ZUtil.LandLorShiftBounds. - -Local Open Scope Z_scope. - -Local Arguments Z.pow !_ !_. -Local Arguments Z.mul !_ !_. - -Ltac shift_left_right_t := - repeat match goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- Z.testbit ?x ?n = Z.testbit ?x ?n' ] => apply f_equal; try omega - | [ |- orb (Z.testbit ?x _) (Z.testbit ?y _) = orb (Z.testbit ?x _) (Z.testbit ?y _) ] - => apply f_equal2 - | _ => progress Z.ltb_to_lt - | _ => progress subst - | _ => progress unfold AutoRewrite.rewrite_eq - | _ => progress intros - | _ => omega - | _ => solve [ trivial ] - | _ => progress break_match_step ltac:(fun _ => idtac) - | [ |- context[Z.lor (?x >> ?count) (Z.pow2_mod (?y << (?n - ?count)) ?n)] ] - => unique assert (0 <= Z.lor (x >> count) (Z.pow2_mod (y << (n - count)) n) < 2 ^ n) by (autorewrite with Zshift_to_pow; auto with zarith nia) - | _ => progress push_decode - | [ |- context[Interface.decode (fst ?x)] ] => is_var x; destruct x; simpl in * - | [ |- context[@Interface.decode ?n ?W ?d ?x] ] => is_var x; generalize dependent (@Interface.decode n W d x); intros - | _ => progress Z.rewrite_mod_small - | _ => progress autorewrite with convert_to_Ztestbit - | _ => progress autorewrite with zsimplify_fast - | [ |- _ = _ :> Z ] => apply Z.bits_inj'; intros - | _ => progress autorewrite with Ztestbit_full - | _ => progress autorewrite with bool_congr - | [ |- Z.testbit _ (?x - ?y + (?y - ?z)) = false ] - => autorewrite with zsimplify - | [ H : 0 <= ?x < 2^?n |- Z.testbit ?x ?n' = false ] - => assert (n <= n') by auto with zarith; progress Ztestbit - | _ => progress Ztestbit_full - end. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v deleted file mode 100644 index 245e03480..000000000 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. - -Local Open Scope Z_scope. - -Local Opaque tuple_decoder. -Local Arguments Z.pow !_ !_. -Local Arguments Z.mul !_ !_. - -Section shr. - Context (n : Z) {W} - {ldi : load_immediate W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {or : bitwise_or W} - {decode : decoder n W} - {isdecode : is_decode decode} - {isldi : is_load_immediate ldi} - {isshl : is_shift_left_immediate shl} - {isshr : is_shift_right_immediate shr} - {isor : is_bitwise_or or}. - - Global Instance is_shift_right_immediate_double : is_shift_right_immediate (shr_double n). - Proof using Type*. - intros r count H; hnf in H. - assert (0 < 2^count) by auto with zarith. - assert (0 < 2^(n+count)) by auto with zarith. - assert (forall n', ~n' + count < n -> 2^n <= 2^(n'+count)) by auto with zarith omega. - assert (forall n', ~n' + count < n -> 2^n <= 2^(n'+count)) by auto with zarith omega. - unfold shr_double; simpl. - generalize (decode_range r). - pose proof (decode_range (fst r)). - pose proof (decode_range (snd r)). - assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by (simpl in *; auto with zarith). - assert (forall n', n <= n' -> 0 <= decode (fst r) < 2^n') by auto with zarith omega. - autorewrite with simpl_tuple_decoder; push_decode. - shift_left_right_t. - Qed. -End shr. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v deleted file mode 100644 index 7210d80d5..000000000 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Definitions. - -Local Open Scope Z_scope. - -Local Opaque tuple_decoder. -Local Arguments Z.pow !_ !_. -Local Arguments Z.mul !_ !_. - -Section shrd. - Context (n : Z) {W} - {ldi : load_immediate W} - {shrd : shift_right_doubleword_immediate W} - {decode : decoder n W} - {isdecode : is_decode decode} - {isldi : is_load_immediate ldi} - {isshrd : is_shift_right_doubleword_immediate shrd}. - - Local Ltac zutil_arith ::= solve [ auto with nocore omega ]. - - Global Instance is_shift_right_doubleword_immediate_double : is_shift_right_doubleword_immediate (shrd_double n). - Proof using isdecode isshrd. - intros high low count Hcount; hnf in Hcount. - unfold shrd_double, shift_right_doubleword_immediate_double; simpl. - generalize (decode_range low). - generalize (decode_range high). - generalize (decode_range (fst low)). - generalize (decode_range (snd low)). - generalize (decode_range (fst high)). - generalize (decode_range (snd high)). - assert (forall x, 0 <= Z.pow2_mod x n < 2^n) by auto with zarith. - assert (forall n' x, 2^n <= 2^n' -> 0 <= x < 2^n -> 0 <= x < 2^n') by auto with zarith. - assert (forall n' x, n <= n' -> 0 <= x < 2^n -> 0 <= x < 2^n') by auto with zarith omega. - autorewrite with simpl_tuple_decoder; push_decode. - shift_left_right_t. - Qed. -End shrd. diff --git a/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v deleted file mode 100644 index 0cbc237d2..000000000 --- a/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v +++ /dev/null @@ -1,152 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Modulo. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.LetIn. -Import Bug5107WorkAround. -Import BoundedRewriteNotations. - -Local Open Scope Z_scope. - -Lemma decode_is_spread_left_immediate_iff - {n W} - {decode : decoder n W} - {sprl : spread_left_immediate W} - {isdecode : is_decode decode} - : is_spread_left_immediate sprl - <-> (forall r count, - 0 <= count < n - -> tuple_decoder (sprl r count) = decode r << count). -Proof. - rewrite is_spread_left_immediate_alt by assumption. - split; intros H r count Hc; specialize (H r count Hc); revert H; - pose proof (decode_range r); - assert (0 < 2^count < 2^n) by auto with zarith; - autorewrite with simpl_tuple_decoder; - simpl; intro H'; rewrite H'; - autorewrite with Zshift_to_pow; - Z.rewrite_mod_small; reflexivity. -Qed. - -Global Instance decode_is_spread_left_immediate - {n W} - {decode : decoder n W} - {sprl : spread_left_immediate W} - {isdecode : is_decode decode} - {issprl : is_spread_left_immediate sprl} - : forall r count, - (0 <= count < n)%bounded_rewrite - -> tuple_decoder (sprl r count) <~=~> decode r << count - := proj1 decode_is_spread_left_immediate_iff _. - - -Section tuple2. - Section spread_left. - Context (n : Z) {W} - {ldi : load_immediate W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {decode : decoder n W} - {isdecode : is_decode decode} - {isldi : is_load_immediate ldi} - {isshl : is_shift_left_immediate shl} - {isshr : is_shift_right_immediate shr}. - - Lemma spread_left_from_shift_correct - r count - (H : 0 < count < n) - : (decode (shl r count) + decode (shr r (n - count)) << n = decode r << count mod (2^n*2^n))%Z. - Proof using isdecode isshl isshr. - assert (0 <= count < n) by lia. - assert (0 <= n - count < n) by lia. - assert (0 < 2^(n-count)) by auto with zarith. - assert (2^count < 2^n) by auto with zarith. - pose proof (decode_range r). - assert (0 <= decode r * 2 ^ count < 2 ^ n * 2^n) by auto with zarith. - push_decode; autorewrite with Zshift_to_pow zsimplify. - replace (decode r / 2^(n-count) * 2^n)%Z with ((decode r / 2^(n-count) * 2^(n-count)) * 2^count)%Z - by (rewrite <- Z.mul_assoc; autorewrite with pull_Zpow zsimplify; reflexivity). - rewrite Z.mul_div_eq' by lia. - autorewrite with push_Zmul zsimplify. - rewrite <- Z.mul_mod_distr_r_full, Z.add_sub_assoc. - repeat autorewrite with pull_Zpow zsimplify in *. - reflexivity. - Qed. - - Global Instance is_spread_left_from_shift - : is_spread_left_immediate (sprl_from_shift n). - Proof using Type*. - apply is_spread_left_immediate_alt. - intros r count; intros. - pose proof (decode_range r). - assert (0 < 2^n) by auto with zarith. - assert (decode r < 2^n * 2^n) by (generalize dependent (decode r); intros; nia). - autorewrite with simpl_tuple_decoder. - destruct (Z_zerop count). - { subst; autorewrite with Zshift_to_pow zsimplify. - simpl; push_decode. - autorewrite with push_Zpow zsimplify. - reflexivity. } - simpl. - rewrite <- spread_left_from_shift_correct by lia. - autorewrite with zsimplify Zpow_to_shift. - reflexivity. - Qed. - End spread_left. - - Section full_from_half. - Context {W} - {mulhwll : multiply_low_low W} - {mulhwhl : multiply_high_low W} - {mulhwhh : multiply_high_high W} - {adc : add_with_carry W} - {shl : shift_left_immediate W} - {shr : shift_right_immediate W} - {half_n : Z} - {ldi : load_immediate W} - {decode : decoder (2 * half_n) W} - {ismulhwll : is_mul_low_low half_n mulhwll} - {ismulhwhl : is_mul_high_low half_n mulhwhl} - {ismulhwhh : is_mul_high_high half_n mulhwhh} - {isadc : is_add_with_carry adc} - {isshl : is_shift_left_immediate shl} - {isshr : is_shift_right_immediate shr} - {isldi : is_load_immediate ldi} - {isdecode : is_decode decode}. - - Local Arguments Z.mul !_ !_. - Lemma spread_left_from_shift_half_correct - r - : (decode (shl r half_n) + decode (shr r half_n) * (2^half_n * 2^half_n) - = (decode r * 2^half_n) mod (2^half_n*2^half_n*2^half_n*2^half_n))%Z. - Proof using Type*. - destruct (0 <? half_n) eqn:Hn; Z.ltb_to_lt. - { pose proof (spread_left_from_shift_correct (2*half_n) r half_n) as H. - specialize_by lia. - autorewrite with Zshift_to_pow push_Zpow zsimplify in *. - rewrite !Z.mul_assoc in *. - simpl in *; rewrite <- H; reflexivity. } - { pose proof (decode_range r). - pose proof (decode_range (shr r half_n)). - pose proof (decode_range (shl r half_n)). - simpl in *. - autorewrite with push_Zpow in *. - destruct (Z_zerop half_n). - { subst; simpl in *. - autorewrite with zsimplify. - nia. } - assert (half_n < 0) by lia. - assert (2^half_n = 0) by auto with zarith. - assert (0 < 0) by nia; omega. } - Qed. - End full_from_half. -End tuple2. diff --git a/src/LegacyArithmetic/Interface.v b/src/LegacyArithmetic/Interface.v deleted file mode 100644 index 9a652bbd4..000000000 --- a/src/LegacyArithmetic/Interface.v +++ /dev/null @@ -1,451 +0,0 @@ -(*** Interface for bounded arithmetic *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil.Notations. - -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.AutoRewrite. -Require Import Crypto.Util.Notations. - -Local Open Scope type_scope. -Local Open Scope Z_scope. - -Class decoder (n : Z) W := - { decode : W -> Z }. -Coercion decode : decoder >-> Funclass. -Global Arguments decode {n W _} _. - -Class is_decode {n W} (decode : decoder n W) := - decode_range : forall x, 0 <= decode x < 2^n. - -Class bounded_in_range_cls (x y z : Z) := is_bounded_in_range : x <= y < z. -Ltac bounded_solver_tac := - solve [ eassumption | typeclasses eauto | omega ]. -Hint Extern 0 (bounded_in_range_cls _ _ _) => unfold bounded_in_range_cls; bounded_solver_tac : typeclass_instances. -Global Arguments bounded_in_range_cls / _ _ _. -Global Instance decode_range_bound {n W} {decode : decoder n W} {H : is_decode decode} - : forall x, bounded_in_range_cls 0 (decode x) (2^n) - := H. - -Class bounded_le_cls (x y : Z) := is_bounded_le : x <= y. -Hint Extern 0 (bounded_le_cls _ _) => unfold bounded_le_cls; bounded_solver_tac : typeclass_instances. -Global Arguments bounded_le_cls / _ _. - -Inductive bounded_decode_pusher_tag := decode_tag. - -Ltac push_decode_step := - match goal with - | [ |- context[@decode ?n ?W ?decoder ?w] ] - => tc_rewrite (decode_tag) (@decode n W decoder w) -> - | [ |- context[match @fst ?A ?B ?x with true => 1 | false => 0 end] ] - => tc_rewrite (decode_tag) (match @fst A B x with true => 1 | false => 0 end) -> - | [ |- context[@fst bool ?B ?x] ] - => tc_rewrite (decode_tag) (@fst bool B x) -> - end. -Ltac push_decode := repeat push_decode_step. -Ltac pull_decode_step := - match goal with - | [ |- context[?E] ] - => lazymatch type of E with - | Z => idtac - | bool => idtac - end; - tc_rewrite (decode_tag) <- E - end. -Ltac pull_decode := repeat pull_decode_step. - -Delimit Scope bounded_rewrite_scope with bounded_rewrite. - -Infix "<~=~>" := (rewrite_eq decode_tag) : bounded_rewrite_scope. -Infix "=~>" := (rewrite_left_to_right_eq decode_tag) : bounded_rewrite_scope. -Infix "<~=" := (rewrite_right_to_left_eq decode_tag) : bounded_rewrite_scope. -Notation "x <= y" := (bounded_le_cls x y) : bounded_rewrite_scope. -Notation "x <= y < z" := (bounded_in_range_cls x y z) : bounded_rewrite_scope. - -Module Import BoundedRewriteNotations. - Infix "<~=~>" := (rewrite_eq decode_tag) : type_scope. - Infix "=~>" := (rewrite_left_to_right_eq decode_tag) : type_scope. - Infix "<~=" := (rewrite_right_to_left_eq decode_tag) : type_scope. - Open Scope bounded_rewrite_scope. -End BoundedRewriteNotations. - -(** This is required for typeclass resolution to be fast. *) -Typeclasses Opaque decode. - -Section InstructionGallery. - Context (n : Z) (* bit-width of width of [W] *) - {W : Type} (* bounded type, [W] for word *) - (Wdecoder : decoder n W). - Local Notation imm := Z (only parsing). (* immediate (compile-time) argument *) - - Class load_immediate := { ldi : imm -> W }. - Global Coercion ldi : load_immediate >-> Funclass. - - Class is_load_immediate {ldi : load_immediate} := - decode_load_immediate :> forall x, 0 <= x < 2^n -> decode (ldi x) =~> x. - - Class shift_right_doubleword_immediate := { shrd : W -> W -> imm -> W }. - Global Coercion shrd : shift_right_doubleword_immediate >-> Funclass. - - Class is_shift_right_doubleword_immediate (shrd : shift_right_doubleword_immediate) := - decode_shift_right_doubleword :> - forall high low count, - 0 <= count < n - -> decode (shrd high low count) <~=~> (((decode high << n) + decode low) >> count) mod 2^n. - - (** Quoting http://www.felixcloutier.com/x86/SHRD.html: - - If the count is 1 or greater, the CF flag is filled with the - last bit shifted out of the destination operand and the SF, ZF, - and PF flags are set according to the value of the result. For a - 1-bit shift, the OF flag is set if a sign change occurred; - otherwise, it is cleared. For shifts greater than 1 bit, the OF - flag is undefined. If a shift occurs, the AF flag is - unde-fined. If the count operand is 0, the flags are not - affected. If the count is greater than the operand size, the - flags are undefined. - - We ignore the CF in the specification; we only have it so that - we can ensure that the CF flag gets appropriately clobbered. *) - Class shift_right_doubleword_immediate_with_CF := { shrdf : W -> W -> imm -> bool * W }. - Global Coercion shrdf : shift_right_doubleword_immediate_with_CF >-> Funclass. - - Class is_shift_right_doubleword_immediate_with_CF (shrdf : shift_right_doubleword_immediate_with_CF) := - decode_snd_shift_right_doubleword_with_CF :> - forall high low count, - 0 <= count < n - -> decode (snd (shrdf high low count)) <~=~> (((decode high << n) + decode low) >> count) mod 2^n. - - Class shift_left_immediate := { shl : W -> imm -> W }. - Global Coercion shl : shift_left_immediate >-> Funclass. - - Class is_shift_left_immediate (shl : shift_left_immediate) := - decode_shift_left_immediate :> - forall r count, 0 <= count < n -> decode (shl r count) <~=~> (decode r << count) mod 2^n. - - (** Quoting http://www.felixcloutier.com/x86/SAL:SAR:SHL:SHR.html: - - The CF flag contains the value of the last bit shifted out of - the destination operand; it is undefined for SHL and SHR - instructions where the count is greater than or equal to the - size (in bits) of the destination operand. The OF flag is - affected only for 1-bit shifts (see “Description” above); - otherwise, it is undefined. The SF, ZF, and PF flags are set - according to the result. If the count is 0, the flags are not - affected. For a non-zero count, the AF flag is undefined. - - We ignore the CF in the specification; we only have it so that - we can ensure that the CF flag gets appropriately clobbered. *) - Class shift_left_immediate_with_CF := { shlf : W -> imm -> bool * W }. - Global Coercion shlf : shift_left_immediate_with_CF >-> Funclass. - - Class is_shift_left_immediate_with_CF (shlf : shift_left_immediate_with_CF) := - decode_shift_left_immediate_with_CF :> - forall r count, 0 <= count < n -> decode (snd (shlf r count)) <~=~> (decode r << count) mod 2^n. - - Class shift_right_immediate := { shr : W -> imm -> W }. - Global Coercion shr : shift_right_immediate >-> Funclass. - - Class is_shift_right_immediate (shr : shift_right_immediate) := - decode_shift_right_immediate :> - forall r count, 0 <= count < n -> decode (shr r count) <~=~> (decode r >> count). - - Class shift_right_immediate_with_CF := { shrf : W -> imm -> bool * W }. - Global Coercion shrf : shift_right_immediate_with_CF >-> Funclass. - - Class is_shift_right_immediate_with_CF (shrf : shift_right_immediate_with_CF) := - decode_shift_right_immediate_with_CF :> - forall r count, 0 <= count < n -> decode (snd (shrf r count)) <~=~> (decode r >> count). - - Class spread_left_immediate := { sprl : W -> imm -> tuple W 2 (* [(low, high)] *) }. - Global Coercion sprl : spread_left_immediate >-> Funclass. - - Class is_spread_left_immediate (sprl : spread_left_immediate) := - { - decode_fst_spread_left_immediate :> forall r count, - 0 <= count < n - -> decode (fst (sprl r count)) =~> (decode r << count) mod 2^n; - decode_snd_spread_left_immediate :> forall r count, - 0 <= count < n - -> decode (snd (sprl r count)) =~> (decode r << count) >> n - - }. - - Class mask_keep_low := { mkl :> W -> imm -> W }. - Global Coercion mkl : mask_keep_low >-> Funclass. - - Class is_mask_keep_low (mkl : mask_keep_low) := - decode_mask_keep_low :> forall r count, - 0 <= count < n -> decode (mkl r count) <~=~> decode r mod 2^count. - - Class bitwise_and := { and : W -> W -> W }. - Global Coercion and : bitwise_and >-> Funclass. - - Class is_bitwise_and (and : bitwise_and) := - { - decode_bitwise_and :> forall x y, decode (and x y) <~=~> Z.land (decode x) (decode y) - }. - - (** Quoting http://www.felixcloutier.com/x86/AND.html: - - The OF and CF flags are cleared; the SF, ZF, and PF flags are set - according to the result. The state of the AF flag is - undefined. *) - Class bitwise_and_with_CF := { andf : W -> W -> bool * W }. - Global Coercion andf : bitwise_and_with_CF >-> Funclass. - - Class is_bitwise_and_with_CF (andf : bitwise_and_with_CF) := - { - decode_snd_bitwise_and_with_CF :> forall x y, decode (snd (andf x y)) <~=~> Z.land (decode x) (decode y); - fst_bitwise_and_with_CF :> forall x y, fst (andf x y) =~> false - }. - - Class bitwise_or := { or : W -> W -> W }. - Global Coercion or : bitwise_or >-> Funclass. - - Class is_bitwise_or (or : bitwise_or) := - { - decode_bitwise_or :> forall x y, decode (or x y) <~=~> Z.lor (decode x) (decode y) - }. - - (** Quoting http://www.felixcloutier.com/x86/OR.html: - - The OF or CF flags are cleared; the SF, ZF, or PF flags are set - according to the result. The state of the AF flag is - undefined. *) - Class bitwise_or_with_CF := { orf : W -> W -> bool * W }. - Global Coercion orf : bitwise_or_with_CF >-> Funclass. - - Class is_bitwise_or_with_CF (orf : bitwise_or_with_CF) := - { - decode_snd_bitwise_or_with_CF :> forall x y, decode (snd (orf x y)) <~=~> Z.lor (decode x) (decode y); - fst_bitwise_or_with_CF :> forall x y, fst (orf x y) =~> false - }. - - Local Notation bit b := (if b then 1 else 0). - - Class add_with_carry := { adc : W -> W -> bool -> bool * W }. - Global Coercion adc : add_with_carry >-> Funclass. - - Class is_add_with_carry (adc : add_with_carry) := - { - bit_fst_add_with_carry :> forall x y c, bit (fst (adc x y c)) <~=~> (decode x + decode y + bit c) >> n; - decode_snd_add_with_carry :> forall x y c, decode (snd (adc x y c)) <~=~> (decode x + decode y + bit c) mod (2^n) - }. - - Class sub_with_carry := { subc : W -> W -> bool -> bool * W }. - Global Coercion subc : sub_with_carry >-> Funclass. - - Class is_sub_with_carry (subc:W->W->bool->bool*W) := - { - fst_sub_with_carry :> forall x y c, fst (subc x y c) <~=~> ((decode x - decode y - bit c) <? 0); - decode_snd_sub_with_carry :> forall x y c, decode (snd (subc x y c)) <~=~> (decode x - decode y - bit c) mod 2^n - }. - - Class multiply := { mul : W -> W -> W }. - Global Coercion mul : multiply >-> Funclass. - - Class is_mul (mul : multiply) := - decode_mul :> forall x y, decode (mul x y) <~=~> (decode x * decode y). - - Class multiply_low_low := { mulhwll : W -> W -> W }. - Global Coercion mulhwll : multiply_low_low >-> Funclass. - Class multiply_high_low := { mulhwhl : W -> W -> W }. - Global Coercion mulhwhl : multiply_high_low >-> Funclass. - Class multiply_high_high := { mulhwhh : W -> W -> W }. - Global Coercion mulhwhh : multiply_high_high >-> Funclass. - Class multiply_double := { muldw : W -> W -> tuple W 2 }. - Global Coercion muldw : multiply_double >-> Funclass. - (** Quoting http://www.felixcloutier.com/x86/MUL.html: - - The OF and CF flags are set to 0 if the upper half of the result - is 0; otherwise, they are set to 1. The SF, ZF, AF, and PF flags - are undefined. - - We ignore the CF in the specification; we only have it so that - we can ensure that the CF flag gets appropriately clobbered. *) - Class multiply_double_with_CF := { muldwf : W -> W -> bool * tuple W 2 }. - Global Coercion muldwf : multiply_double_with_CF >-> Funclass. - - Class is_mul_low_low (w:Z) (mulhwll : multiply_low_low) := - decode_mul_low_low :> - forall x y, decode (mulhwll x y) <~=~> ((decode x mod 2^w) * (decode y mod 2^w)) mod 2^n. - Class is_mul_high_low (w:Z) (mulhwhl : multiply_high_low) := - decode_mul_high_low :> - forall x y, decode (mulhwhl x y) <~=~> ((decode x >> w) * (decode y mod 2^w)) mod 2^n. - Class is_mul_high_high (w:Z) (mulhwhh : multiply_high_high) := - decode_mul_high_high :> - forall x y, decode (mulhwhh x y) <~=~> ((decode x >> w) * (decode y >> w)) mod 2^n. - Class is_mul_double (muldw : multiply_double) := - { - decode_fst_mul_double :> - forall x y, decode (fst (muldw x y)) =~> (decode x * decode y) mod 2^n; - decode_snd_mul_double :> - forall x y, decode (snd (muldw x y)) =~> (decode x * decode y) >> n - }. - - Class is_mul_double_with_CF (muldwf : multiply_double_with_CF) := - { - decode_fst_mul_double_with_CF :> - forall x y, decode (fst (snd (muldwf x y))) =~> (decode x * decode y) mod 2^n; - decode_snd_mul_double_with_CF :> - forall x y, decode (snd (snd (muldwf x y))) =~> (decode x * decode y) >> n - }. - - Class select_conditional := { selc : bool -> W -> W -> W }. - Global Coercion selc : select_conditional >-> Funclass. - - Class is_select_conditional (selc : select_conditional) := - decode_select_conditional :> forall b x y, - decode (selc b x y) <~=~> if b then decode x else decode y. - - Class add_modulo := { addm : W -> W -> W (* modulus *) -> W }. - Global Coercion addm : add_modulo >-> Funclass. - - Class is_add_modulo (addm : add_modulo) := - decode_add_modulo :> forall x y modulus, - decode (addm x y modulus) <~=~> (if (decode x + decode y) <? decode modulus - then (decode x + decode y) - else (decode x + decode y) - decode modulus). -End InstructionGallery. - -Global Arguments load_immediate : clear implicits. -Global Arguments shift_right_doubleword_immediate : clear implicits. -Global Arguments shift_right_doubleword_immediate_with_CF : clear implicits. -Global Arguments shift_left_immediate : clear implicits. -Global Arguments shift_left_immediate_with_CF : clear implicits. -Global Arguments shift_right_immediate : clear implicits. -Global Arguments shift_right_immediate_with_CF : clear implicits. -Global Arguments spread_left_immediate : clear implicits. -Global Arguments mask_keep_low : clear implicits. -Global Arguments bitwise_and : clear implicits. -Global Arguments bitwise_and_with_CF : clear implicits. -Global Arguments bitwise_or : clear implicits. -Global Arguments bitwise_or_with_CF : clear implicits. -Global Arguments add_with_carry : clear implicits. -Global Arguments sub_with_carry : clear implicits. -Global Arguments multiply : clear implicits. -Global Arguments multiply_low_low : clear implicits. -Global Arguments multiply_high_low : clear implicits. -Global Arguments multiply_high_high : clear implicits. -Global Arguments multiply_double : clear implicits. -Global Arguments multiply_double_with_CF : clear implicits. -Global Arguments select_conditional : clear implicits. -Global Arguments add_modulo : clear implicits. -Global Arguments ldi {_ _} _. -Global Arguments shrdf {_ _} _ _ _. -Global Arguments shrd {_ _} _ _ _. -Global Arguments shl {_ _} _ _. -Global Arguments shlf {_ _} _ _. -Global Arguments shr {_ _} _ _. -Global Arguments shrf {_ _} _ _. -Global Arguments sprl {_ _} _ _. -Global Arguments mkl {_ _} _ _. -Global Arguments and {_ _} _ _. -Global Arguments andf {_ _} _ _. -Global Arguments or {_ _} _ _. -Global Arguments orf {_ _} _ _. -Global Arguments adc {_ _} _ _ _. -Global Arguments subc {_ _} _ _ _. -Global Arguments mul {_ _} _ _. -Global Arguments mulhwll {_ _} _ _. -Global Arguments mulhwhl {_ _} _ _. -Global Arguments mulhwhh {_ _} _ _. -Global Arguments muldw {_ _} _ _. -Global Arguments muldwf {_ _} _ _. -Global Arguments selc {_ _} _ _ _. -Global Arguments addm {_ _} _ _ _. - -Global Arguments is_decode {_ _} _. -Global Arguments is_load_immediate {_ _ _} _. -Global Arguments is_shift_right_doubleword_immediate {_ _ _} _. -Global Arguments is_shift_right_doubleword_immediate_with_CF {_ _ _} _. -Global Arguments is_shift_left_immediate {_ _ _} _. -Global Arguments is_shift_left_immediate_with_CF {_ _ _} _. -Global Arguments is_shift_right_immediate {_ _ _} _. -Global Arguments is_shift_right_immediate_with_CF {_ _ _} _. -Global Arguments is_spread_left_immediate {_ _ _} _. -Global Arguments is_mask_keep_low {_ _ _} _. -Global Arguments is_bitwise_and {_ _ _} _. -Global Arguments is_bitwise_and_with_CF {_ _ _} _. -Global Arguments is_bitwise_or {_ _ _} _. -Global Arguments is_bitwise_or_with_CF {_ _ _} _. -Global Arguments is_add_with_carry {_ _ _} _. -Global Arguments is_sub_with_carry {_ _ _} _. -Global Arguments is_mul {_ _ _} _. -Global Arguments is_mul_low_low {_ _ _} _ _. -Global Arguments is_mul_high_low {_ _ _} _ _. -Global Arguments is_mul_high_high {_ _ _} _ _. -Global Arguments is_mul_double {_ _ _} _. -Global Arguments is_mul_double_with_CF {_ _ _} _. -Global Arguments is_select_conditional {_ _ _} _. -Global Arguments is_add_modulo {_ _ _} _. - -Module fancy_machine. - Local Notation imm := Z (only parsing). - - Class instructions (n : Z) := - { - W : Type (* [n]-bit word *); - decode :> decoder n W; - ldi :> load_immediate W; - shrd :> shift_right_doubleword_immediate W; - shl :> shift_left_immediate W; - shr :> shift_right_immediate W; - adc :> add_with_carry W; - subc :> sub_with_carry W; - mulhwll :> multiply_low_low W; - mulhwhl :> multiply_high_low W; - mulhwhh :> multiply_high_high W; - selc :> select_conditional W; - addm :> add_modulo W - }. - - Class arithmetic {n_over_two} (ops:instructions (2 * n_over_two)) := - { - decode_range :> is_decode decode; - load_immediate :> is_load_immediate ldi; - shift_right_doubleword_immediate :> is_shift_right_doubleword_immediate shrd; - shift_left_immediate :> is_shift_left_immediate shl; - shift_right_immediate :> is_shift_right_immediate shr; - add_with_carry :> is_add_with_carry adc; - sub_with_carry :> is_sub_with_carry subc; - multiply_low_low :> is_mul_low_low n_over_two mulhwll; - multiply_high_low :> is_mul_high_low n_over_two mulhwhl; - multiply_high_high :> is_mul_high_high n_over_two mulhwhh; - select_conditional :> is_select_conditional selc; - add_modulo :> is_add_modulo addm - }. -End fancy_machine. - -Module x86. - Local Notation imm := Z (only parsing). - - Class instructions (n : Z) := - { - W : Type (* [n]-bit word *); - decode :> decoder n W; - ldi :> load_immediate W; - shrdf :> shift_right_doubleword_immediate_with_CF W; - shlf :> shift_left_immediate_with_CF W; - shrf :> shift_right_immediate_with_CF W; - adc :> add_with_carry W; - subc :> sub_with_carry W; - muldwf :> multiply_double_with_CF W; - selc :> select_conditional W; - orf :> bitwise_or_with_CF W - }. - - Class arithmetic {n} (ops:instructions n) := - { - decode_range :> is_decode decode; - load_immediate :> is_load_immediate ldi; - shift_right_doubleword_immediate_with_CF :> is_shift_right_doubleword_immediate_with_CF shrdf; - shift_left_immediate_with_CF :> is_shift_left_immediate_with_CF shlf; - shift_right_immediate_with_CF :> is_shift_right_immediate_with_CF shrf; - add_with_carry :> is_add_with_carry adc; - sub_with_carry :> is_sub_with_carry subc; - multiply_double_with_CF :> is_mul_double_with_CF muldwf; - select_conditional :> is_select_conditional selc; - bitwise_or_with_CF :> is_bitwise_or_with_CF orf - }. -End x86. diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v deleted file mode 100644 index a2c8d9de5..000000000 --- a/src/LegacyArithmetic/InterfaceProofs.v +++ /dev/null @@ -1,231 +0,0 @@ -(** * Alternate forms for Interface for bounded arithmetic *) -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Hints. -Require Import Crypto.Util.ZUtil.Hints.ZArith. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.AutoRewrite. -Require Import Crypto.Util.Notations. - -Local Open Scope type_scope. -Local Open Scope Z_scope. - -Import BoundedRewriteNotations. -Local Notation bit b := (if b then 1 else 0). - -Lemma decoder_eta {n W} (decode : decoder n W) : decode = {| Interface.decode := decode |}. -Proof. destruct decode; reflexivity. Defined. - -Section InstructionGallery. - Context (n : Z) (* bit-width of width of [W] *) - {W : Type} (* bounded type, [W] for word *) - (Wdecoder : decoder n W). - Local Notation imm := Z (only parsing). (* immediate (compile-time) argument *) - - Definition Build_is_spread_left_immediate' (sprl : spread_left_immediate W) - (pf : forall r count, 0 <= count < n - -> _ /\ _) - := {| decode_fst_spread_left_immediate r count H := proj1 (pf r count H); - decode_snd_spread_left_immediate r count H := proj2 (pf r count H) |}. - - Definition Build_is_add_with_carry' (adc : add_with_carry W) - (pf : forall x y c, _ /\ _) - := {| bit_fst_add_with_carry x y c := proj1 (pf x y c); - decode_snd_add_with_carry x y c := proj2 (pf x y c) |}. - - Definition Build_is_sub_with_carry' (subc : sub_with_carry W) - (pf : forall x y c, _ /\ _) - : is_sub_with_carry subc - := {| fst_sub_with_carry x y c := proj1 (pf x y c); - decode_snd_sub_with_carry x y c := proj2 (pf x y c) |}. - - Definition Build_is_mul_double' (muldw : multiply_double W) - (pf : forall x y, _ /\ _) - := {| decode_fst_mul_double x y := proj1 (pf x y); - decode_snd_mul_double x y := proj2 (pf x y) |}. - - Lemma is_spread_left_immediate_alt - {sprl : spread_left_immediate W} - {isdecode : is_decode Wdecoder} - : is_spread_left_immediate sprl - <-> (forall r count, 0 <= count < n -> decode (fst (sprl r count)) + decode (snd (sprl r count)) << n = (decode r << count) mod (2^n*2^n))%Z. - Proof using Type. - split; intro H; [ | apply Build_is_spread_left_immediate' ]; - intros r count Hc; - [ | specialize (H r count Hc); revert H ]; - unfold bounded_in_range_cls in *; - pose proof (decode_range r); - assert (0 < 2^n) by auto with zarith; - assert (0 <= 2^count < 2^n)%Z by auto with zarith; - assert (0 <= decode r * 2^count < 2^n * 2^n)%Z by (generalize dependent (decode r); intros; nia); - rewrite ?decode_fst_spread_left_immediate, ?decode_snd_spread_left_immediate - by typeclasses eauto with typeclass_instances core; - autorewrite with Zshift_to_pow zsimplify push_Zpow. - { reflexivity. } - { intro H'; rewrite <- H'. - autorewrite with zsimplify; split; reflexivity. } - Qed. - - Lemma is_mul_double_alt - {muldw : multiply_double W} - {isdecode : is_decode Wdecoder} - : is_mul_double muldw - <-> (forall x y, decode (fst (muldw x y)) + decode (snd (muldw x y)) << n = (decode x * decode y) mod (2^n*2^n)). - Proof using Type. - split; intro H; [ | apply Build_is_mul_double' ]; - intros x y; - [ | specialize (H x y); revert H ]; - pose proof (decode_range x); - pose proof (decode_range y); - assert (0 < 2^n) by auto with zarith; - assert (0 <= decode x * decode y < 2^n * 2^n)%Z by nia; - (destruct (0 <=? n) eqn:?; Z.ltb_to_lt; - [ | assert (2^n = 0) by auto with zarith; exfalso; omega ]); - rewrite ?decode_fst_mul_double, ?decode_snd_mul_double - by typeclasses eauto with typeclass_instances core; - autorewrite with Zshift_to_pow zsimplify push_Zpow. - { reflexivity. } - { intro H'; rewrite <- H'. - autorewrite with zsimplify; split; reflexivity. } - Qed. -End InstructionGallery. - -Global Arguments is_spread_left_immediate_alt {_ _ _ _ _}. -Global Arguments is_mul_double_alt {_ _ _ _ _}. - -Ltac bounded_solver_tac := - solve [ eassumption | typeclasses eauto | omega ]. - -Global Instance decode_proj n W (dec : W -> Z) - : @decode n W {| decode := dec |} =~> dec. -Proof. reflexivity. Qed. - -Global Instance decode_if_bool n W (decode : decoder n W) - : forall (b : bool) x y, - decode (if b then x else y) - =~> if b then decode x else decode y. -Proof. destruct b; reflexivity. Qed. - -Global Instance decode_mod_small {n W} {decode : decoder n W} {x b} - {H : bounded_in_range_cls 0 (decode x) b} - : decode x <~= decode x mod b. -Proof. - Z.rewrite_mod_small; reflexivity. -Qed. - -Global Instance decode_mod_range {n W decode} {H : @is_decode n W decode} x - : decode x <~= decode x mod 2^n. -Proof. exact _. Qed. - -Lemma decode_exponent_nonnegative {n W} (decode : decoder n W) {isdecode : is_decode decode} - (isinhabited : W) - : (0 <= n)%Z. -Proof. - pose proof (decode_range isinhabited). - assert (0 < 2^n) by omega. - destruct (Z_lt_ge_dec n 0) as [H'|]; [ | omega ]. - assert (2^n = 0) by auto using Z.pow_neg_r. - omega. -Qed. - -Section adc_subc. - Context {n W} - {decode : decoder n W} - {adc : add_with_carry W} - {subc : sub_with_carry W} - {isdecode : is_decode decode} - {isadc : is_add_with_carry adc} - {issubc : is_sub_with_carry subc}. - Global Instance bit_fst_add_with_carry_false - : forall x y, bit (fst (adc x y false)) <~=~> (decode x + decode y) >> n. - Proof using isadc. - intros; erewrite bit_fst_add_with_carry by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. - Global Instance bit_fst_add_with_carry_true - : forall x y, bit (fst (adc x y true)) <~=~> (decode x + decode y + 1) >> n. - Proof using isadc. - intros; erewrite bit_fst_add_with_carry by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. - Global Instance fst_add_with_carry_leb - : forall x y c, fst (adc x y c) <~= (2^n <=? (decode x + decode y + bit c)). - Proof using isadc isdecode. - intros x y c; hnf. - assert (0 <= n)%Z by eauto using decode_exponent_nonnegative. - pose proof (decode_range x); pose proof (decode_range y). - assert (0 <= bit c <= 1)%Z by (destruct c; omega). - lazymatch goal with - | [ |- fst ?x = (?a <=? ?b) :> bool ] - => cut (((if fst x then 1 else 0) = (if a <=? b then 1 else 0))%Z); - [ destruct (fst x), (a <=? b); intro; congruence | ] - end. - push_decode. - autorewrite with Zshift_to_pow. - rewrite Z.div_between_0_if by auto with zarith. - reflexivity. - Qed. - Global Instance fst_add_with_carry_false_leb - : forall x y, fst (adc x y false) <~= (2^n <=? (decode x + decode y)). - Proof using isadc isdecode. - intros; erewrite fst_add_with_carry_leb by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. - Global Instance fst_add_with_carry_true_leb - : forall x y, fst (adc x y true) <~=~> (2^n <=? (decode x + decode y + 1)). - Proof using isadc isdecode. - intros; erewrite fst_add_with_carry_leb by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. - Global Instance fst_sub_with_carry_false - : forall x y, fst (subc x y false) <~=~> ((decode x - decode y) <? 0). - Proof using issubc. - intros; erewrite fst_sub_with_carry by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. - Global Instance fst_sub_with_carry_true - : forall x y, fst (subc x y true) <~=~> ((decode x - decode y - 1) <? 0). - Proof using issubc. - intros; erewrite fst_sub_with_carry by assumption. - autorewrite with zsimplify_const; reflexivity. - Qed. -End adc_subc. - -Hint Extern 2 (rewrite_right_to_left_eq decode_tag _ (_ <=? (@decode ?n ?W ?decoder ?x + @decode _ _ _ ?y))) -=> apply @fst_add_with_carry_false_leb : typeclass_instances. -Hint Extern 2 (rewrite_right_to_left_eq decode_tag _ (_ <=? (@decode ?n ?W ?decoder ?x + @decode _ _ _ ?y + 1))) -=> apply @fst_add_with_carry_true_leb : typeclass_instances. -Hint Extern 2 (rewrite_right_to_left_eq decode_tag _ (_ <=? (@decode ?n ?W ?decoder ?x + @decode _ _ _ ?y + if ?c then _ else _))) -=> apply @fst_add_with_carry_leb : typeclass_instances. - - -(* We take special care to handle the case where the decoder is - syntactically different but the decoded expression is judgmentally - the same; we don't want to split apart variables that should be the - same. *) -Ltac set_decode_step check := - match goal with - | [ |- context G[@decode ?n ?W ?dr ?w] ] - => check w; - first [ match goal with - | [ d := @decode _ _ _ w |- _ ] - => change (@decode n W dr w) with d - end - | generalize (@decode_range n W dr _ w); - let d := fresh "d" in - set (d := @decode n W dr w); - intro ] - end. -Ltac set_decode check := repeat set_decode_step check. -Ltac clearbody_decode := - repeat match goal with - | [ H := @decode _ _ _ _ |- _ ] => clearbody H - end. -Ltac generalize_decode_by check := set_decode check; clearbody_decode. -Ltac generalize_decode := generalize_decode_by ltac:(fun w => idtac). -Ltac generalize_decode_var := generalize_decode_by ltac:(fun w => is_var w). diff --git a/src/LegacyArithmetic/MontgomeryReduction.v b/src/LegacyArithmetic/MontgomeryReduction.v deleted file mode 100644 index 786e08d28..000000000 --- a/src/LegacyArithmetic/MontgomeryReduction.v +++ /dev/null @@ -1,114 +0,0 @@ -(*** Montgomery Multiplication *) -(** This file implements Montgomery Form, Montgomery Reduction, and - Montgomery Multiplication on [ZLikeOps]. We follow [Montgomery/Z.v]. *) -Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. -Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Tactics.Test. -Require Import Crypto.Util.Tactics.Not. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Notations. - -Local Open Scope small_zlike_scope. -Local Open Scope large_zlike_scope. -Local Open Scope Z_scope. - -Section montgomery. - Context (small_bound modulus : Z) {ops : ZLikeOps small_bound small_bound modulus} {props : ZLikeProperties ops} - (modulus' : SmallT) - (modulus'_valid : small_valid modulus') - (modulus_nonzero : modulus <> 0). - - (** pull out a common subexpression *) - Local Ltac cse := - let RHS := match goal with |- _ = ?decode ?RHS /\ _ => RHS end in - let v := fresh in - match RHS with - | context[?e] => not is_var e; set (v := e) at 1 2; test clearbody v - end; - revert v; - match goal with - | [ |- let v := ?val in ?LHS = ?decode ?RHS /\ ?P ] - => change (LHS = decode (dlet v := val in RHS) /\ P) - end. - - Definition partial_reduce : forall v : LargeT, - { partial_reduce : SmallT - | large_valid v - -> decode_small partial_reduce = MontgomeryReduction.Definition.partial_reduce modulus small_bound (decode_small modulus') (decode_large v) - /\ small_valid partial_reduce }. - Proof. - intro T. evar (pr : SmallT); exists pr. intros T_valid. - assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid. - assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid. - assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid. - assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid. - assert (0 <= modulus) by apply (modulus_nonneg _). - assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; omega). - rewrite <- partial_reduce_alt_eq by omega. - cbv [MontgomeryReduction.Definition.partial_reduce MontgomeryReduction.Definition.partial_reduce_alt MontgomeryReduction.Definition.prereduce]. - pull_zlike_decode. - cse. - subst pr; split; [ reflexivity | exact _ ]. - Defined. - - Definition reduce_via_partial : forall v : LargeT, - { reduce : SmallT - | large_valid v - -> decode_small reduce = MontgomeryReduction.Definition.reduce_via_partial modulus small_bound (decode_small modulus') (decode_large v) - /\ small_valid reduce }. - Proof. - intro T. evar (pr : SmallT); exists pr. intros T_valid. - assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid. - assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid. - assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid. - assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid. - assert (0 <= modulus) by apply (modulus_nonneg _). - assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; omega). - unfold reduce_via_partial. - rewrite <- partial_reduce_alt_eq by omega. - cbv [MontgomeryReduction.Definition.partial_reduce MontgomeryReduction.Definition.partial_reduce_alt MontgomeryReduction.Definition.prereduce]. - pull_zlike_decode. - cse. - subst pr; split; [ reflexivity | exact _ ]. - Defined. - - Section correctness. - Context (R' : Z) - (Hmod : Z.equiv_modulo modulus (small_bound * R') 1) - (Hmod' : Z.equiv_modulo small_bound (modulus * (decode_small modulus')) (-1)) - (v : LargeT) - (H : large_valid v) - (Hv : 0 <= decode_large v <= small_bound * modulus). - Lemma reduce_via_partial_correct' - : Z.equiv_modulo modulus - (decode_small (proj1_sig (reduce_via_partial v))) - (decode_large v * R') - /\ Z.min 0 (small_bound - modulus) <= (decode_small (proj1_sig (reduce_via_partial v))) < modulus. - Proof using H Hmod Hmod' Hv. - rewrite (proj1 (proj2_sig (reduce_via_partial v) H)). - eauto 6 using reduce_via_partial_correct, reduce_via_partial_in_range, decode_small_valid. - Qed. - - Lemma reduce_via_partial_correct'' - : Z.equiv_modulo modulus - (decode_small (proj1_sig (reduce_via_partial v))) - (decode_large v * R') - /\ 0 <= (decode_small (proj1_sig (reduce_via_partial v))) < modulus. - Proof using H Hmod Hmod' Hv. - pose proof (proj2 (proj2_sig (reduce_via_partial v) H)) as H'. - apply decode_small_valid in H'. - destruct reduce_via_partial_correct'; split; eauto; omega. - Qed. - - Theorem reduce_via_partial_correct - : decode_small (proj1_sig (reduce_via_partial v)) = (decode_large v * R') mod modulus. - Proof using H Hmod Hmod' Hv. - rewrite <- (proj1 reduce_via_partial_correct''). - rewrite Z.mod_small by apply reduce_via_partial_correct''. - reflexivity. - Qed. - End correctness. -End montgomery. diff --git a/src/LegacyArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v deleted file mode 100644 index c5c69e684..000000000 --- a/src/LegacyArithmetic/Pow2Base.v +++ /dev/null @@ -1,18 +0,0 @@ -Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. -Require Import Crypto.Util.ListUtil. -Require Import Coq.Lists.List. - -Local Open Scope Z_scope. - -Section Pow2Base. - Context (limb_widths : list Z). - Local Notation "w[ i ]" := (nth_default 0 limb_widths i). - Fixpoint base_from_limb_widths limb_widths := - match limb_widths with - | nil => nil - | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw) - end. - Local Notation base := (base_from_limb_widths limb_widths). - Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i]. - Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)). -End Pow2Base. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v deleted file mode 100644 index 495636be7..000000000 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ /dev/null @@ -1,564 +0,0 @@ -Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Coq.Lists.List. -Require Import Coq.funind.Recdef. -Require Import Crypto.Util.ListUtil Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Testbit. -Require Import Crypto.Util.ZUtil.Pow2Mod. -Require Import Crypto.Util.ZUtil.Notations. -Require Import Crypto.Util.ZUtil.Shift. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.LegacyArithmetic.VerdiTactics. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Tactics.RewriteHyp. -Require Import Crypto.LegacyArithmetic.Pow2Base. -Require Import Crypto.Util.Notations. -Require Export Crypto.Util.Bool. -Require Export Crypto.Util.FixCoqMistakes. -Local Open Scope Z_scope. - -Require Crypto.LegacyArithmetic.BaseSystemProofs. - -Create HintDb simpl_add_to_nth discriminated. -Create HintDb push_upper_bound discriminated. -Create HintDb pull_upper_bound discriminated. -Create HintDb push_base_from_limb_widths discriminated. -Create HintDb pull_base_from_limb_widths discriminated. - -Hint Extern 1 => progress autorewrite with push_upper_bound in * : push_upper_bound. -Hint Extern 1 => progress autorewrite with pull_upper_bound in * : pull_upper_bound. -Hint Extern 1 => progress autorewrite with push_base_from_limb_widths in * : push_base_from_limb_widths. -Hint Extern 1 => progress autorewrite with pull_base_from_limb_widths in * : pull_base_from_limb_widths. - -Section Pow2BaseProofs. - Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). - Local Notation base := (base_from_limb_widths limb_widths). - - Lemma base_from_limb_widths_length ls : length (base_from_limb_widths ls) = length ls. - Proof using Type. - clear limb_widths limb_widths_nonneg. - induction ls; [ reflexivity | simpl in * ]. - autorewrite with distr_length; auto. - Qed. - Hint Rewrite base_from_limb_widths_length : distr_length. - - Lemma base_from_limb_widths_cons : forall l0 l, - base_from_limb_widths (l0 :: l) = 1 :: map (Z.mul (two_p l0)) (base_from_limb_widths l). - Proof using Type. reflexivity. Qed. - Hint Rewrite base_from_limb_widths_cons : push_base_from_limb_widths. - Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths. - - Lemma base_from_limb_widths_nil : base_from_limb_widths nil = nil. - Proof using Type. reflexivity. Qed. - Hint Rewrite base_from_limb_widths_nil : push_base_from_limb_widths. - - Lemma firstn_base_from_limb_widths : forall n, firstn n (base_from_limb_widths limb_widths) = base_from_limb_widths (firstn n limb_widths). - Proof using Type. - clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) - induction limb_widths as [|l ls IHls]; intros [|n]; try reflexivity. - autorewrite with push_base_from_limb_widths push_firstn; boring. - Qed. - Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths. - Hint Rewrite <- @firstn_base_from_limb_widths : pull_firstn. - Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths. - Hint Rewrite @firstn_base_from_limb_widths : push_firstn. - - Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. - Proof using Type*. - unfold sum_firstn; intros. - apply fold_right_invariant; try omega. - eauto using Z.add_nonneg_nonneg, limb_widths_nonneg, In_firstn. - Qed. Hint Resolve sum_firstn_limb_widths_nonneg. - - Lemma base_from_limb_widths_step : forall i b w, (S i < length limb_widths)%nat -> - nth_error base i = Some b -> - nth_error limb_widths i = Some w -> - nth_error base (S i) = Some (two_p w * b). - Proof using Type. - clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *) - induction limb_widths; intros i b w ? nth_err_w nth_err_b; - unfold base_from_limb_widths in *; fold base_from_limb_widths in *; - [rewrite (@nil_length0 Z) in *; omega | ]. - simpl in *. - case_eq i; intros; subst. - + subst; apply nth_error_first in nth_err_w. - apply nth_error_first in nth_err_b; subst. - apply map_nth_error. - case_eq l; intros; subst; [simpl in *; omega | ]. - unfold base_from_limb_widths; fold base_from_limb_widths. - reflexivity. - + simpl in nth_err_w. - apply nth_error_map in nth_err_w. - destruct nth_err_w as [x [A B] ]. - subst. - replace (two_p w * (two_p a * x)) with (two_p a * (two_p w * x)) by ring. - apply map_nth_error. - apply IHl; auto. omega. - Qed. - - - Lemma nth_error_base : forall i, (i < length limb_widths)%nat -> - nth_error base i = Some (two_p (sum_firstn limb_widths i)). - Proof using Type*. - induction i as [|i IHi]; intros H. - + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. - intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. - + assert (i < length limb_widths)%nat as lt_i_length by omega. - specialize (IHi lt_i_length). - destruct (nth_error_length_exists_value _ _ lt_i_length) as [w nth_err_w]. - erewrite base_from_limb_widths_step; eauto. - f_equal. - simpl. - destruct (NPeano.Nat.eq_dec i 0). - - subst; unfold sum_firstn; simpl. - apply nth_error_exists_first in nth_err_w. - destruct nth_err_w as [l' lw_destruct]; subst. - simpl; ring_simplify. - f_equal; ring. - - erewrite sum_firstn_succ; eauto. - symmetry. - apply two_p_is_exp; auto using sum_firstn_limb_widths_nonneg. - apply limb_widths_nonneg. - eapply nth_error_value_In; eauto. - Qed. - - Lemma nth_default_base : forall d i, (i < length limb_widths)%nat -> - nth_default d base i = 2 ^ (sum_firstn limb_widths i). - Proof using Type*. - intros ? ? i_lt_length. - apply nth_error_value_eq_nth_default. - rewrite nth_error_base, two_p_correct by assumption. - reflexivity. - Qed. - - Lemma b0_1 : forall x : Z, limb_widths <> nil -> nth_default x base 0 = 1. - Proof using Type. - case_eq limb_widths; intros; [congruence | reflexivity]. - Qed. - - Lemma base_from_limb_widths_app : forall l0 l - (l0_nonneg : forall x, In x l0 -> 0 <= x) - (l_nonneg : forall x, In x l -> 0 <= x), - base_from_limb_widths (l0 ++ l) - = base_from_limb_widths l0 ++ map (Z.mul (two_p (sum_firstn l0 (length l0)))) (base_from_limb_widths l). - Proof using Type. - induction l0 as [|?? IHl0]. - { simpl; intros; rewrite <- map_id at 1; apply map_ext; intros; omega. } - { simpl; intros; rewrite !IHl0, !map_app, map_map, sum_firstn_succ_cons, two_p_is_exp by auto with znonzero. - do 2 f_equal; apply map_ext; intros; lia. } - Qed. - - Lemma skipn_base_from_limb_widths : forall n, skipn n (base_from_limb_widths limb_widths) = map (Z.mul (two_p (sum_firstn limb_widths n))) (base_from_limb_widths (skipn n limb_widths)). - Proof using Type*. - intro n; pose proof (base_from_limb_widths_app (firstn n limb_widths) (skipn n limb_widths)) as H. - specialize_by eauto using In_firstn, In_skipn. - autorewrite with simpl_firstn simpl_skipn in *. - rewrite H, skipn_app, skipn_all by auto with arith distr_length; clear H. - simpl; distr_length. - apply Min.min_case_strong; intro; - unfold sum_firstn; autorewrite with natsimplify simpl_skipn simpl_firstn; - reflexivity. - Qed. - Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths. - Hint Rewrite <- @skipn_base_from_limb_widths : pull_skipn. - Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths. - Hint Rewrite @skipn_base_from_limb_widths : push_skipn. - - Lemma pow2_mod_bounded :forall lw us i, (forall w, In w lw -> 0 <= w) -> bounded lw us -> - Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i. - Proof using Type. - clear. - cbv [bounded]; intros lw us i H H0. - repeat match goal with - | |- _ => progress (cbv [bounded]; intros) - | |- _ => break_if - | |- _ => apply Z.bits_inj' - | |- _ => rewrite Z.testbit_pow2_mod by (apply nth_default_preserves_properties; auto; omega) - | |- _ => reflexivity - end. - specialize (H0 i). - symmetry. - let n := match goal with n : Z |- _ => n end in - rewrite <- (Z.mod_pow2_bits_high (nth_default 0 us i) (nth_default 0 lw i) n); - [ rewrite Z.mod_small by omega; reflexivity | ]. - split; try omega. - apply nth_default_preserves_properties; auto; omega. - Qed. - - Lemma bounded_nil_iff : forall us, bounded nil us <-> (forall u, In u us -> u = 0). - Proof using Type. - clear. - intros us; split; cbv [bounded]; [ intros H u H0 | intros H i ]. - + edestruct (In_nth_error_value us u) as [x]; try assumption. - specialize (H x). - replace u with (nth_default 0 us x) by (auto using nth_error_value_eq_nth_default). - rewrite nth_default_nil, Z.pow_0_r in H. - omega. - + rewrite nth_default_nil, Z.pow_0_r. - apply nth_default_preserves_properties; try omega. - intros x H0. - apply H in H0. - omega. - Qed. - - Lemma bounded_iff : forall lw us, bounded lw us <-> forall i, 0 <= nth_default 0 us i < 2 ^ nth_default 0 lw i. - Proof using Type. - clear. - cbv [bounded]; intros. - reflexivity. - Qed. - - Lemma digit_select : forall us i, bounded limb_widths us -> - nth_default 0 us i = Z.pow2_mod (BaseSystem.decode base us >> sum_firstn limb_widths i) (nth_default 0 limb_widths i). - Proof using Type*. - intro us; revert limb_widths limb_widths_nonneg; induction us as [|a us IHus]; - intros limb_widths limb_widths_nonneg i H. - + rewrite nth_default_nil, BaseSystemProofs.decode_nil, Z.shiftr_0_l, Z.pow2_mod_spec, Z.mod_0_l by - (try (apply Z.pow_nonzero; try omega); apply nth_default_preserves_properties; auto; omega). - reflexivity. - + destruct i. - - rewrite nth_default_cons, sum_firstn_0, Z.shiftr_0_r. - destruct limb_widths as [|w lw]. - * cbv [base_from_limb_widths]. - rewrite <-pow2_mod_bounded with (lw := nil); rewrite bounded_nil_iff in *; auto using in_cons; - try solve [intros; exfalso; eauto using in_nil]. - rewrite !nth_default_nil, BaseSystemProofs.decode_base_nil; auto. - cbv. auto using in_eq. - * rewrite nth_default_cons, base_from_limb_widths_cons, BaseSystemProofs.peel_decode. - fold (BaseSystem.mul_each (two_p w)). - rewrite <-BaseSystemProofs.mul_each_base, BaseSystemProofs.mul_each_rep. - rewrite two_p_correct, (Z.mul_comm (2 ^ w)). - rewrite <-Z.shiftl_mul_pow2 by auto using in_eq. - rewrite bounded_iff in *. - specialize (H 0%nat); rewrite !nth_default_cons in H. - rewrite <-Z.lor_shiftl by (auto using in_eq; omega). - apply Z.bits_inj'; intros n H0. - rewrite Z.testbit_pow2_mod by auto using in_eq. - break_if. { - autorewrite with Ztestbit; break_match; - try rewrite Z.testbit_neg_r with (n := n - w) by omega; - autorewrite with bool_congr; - f_equal; ring. - } { - replace a with (a mod 2 ^ w) by (auto using Z.mod_small). - apply Z.mod_pow2_bits_high. split; auto using in_eq; omega. - } - - rewrite nth_default_cons_S. - destruct limb_widths as [|w lw]. - * cbv [base_from_limb_widths]. - rewrite <-pow2_mod_bounded with (lw := nil); rewrite bounded_nil_iff in *; auto using in_cons. - rewrite sum_firstn_nil, !nth_default_nil, BaseSystemProofs.decode_base_nil, Z.shiftr_0_r. - apply nth_default_preserves_properties; intros; auto using in_cons. - f_equal; auto using in_cons. - * rewrite sum_firstn_succ_cons, nth_default_cons_S, base_from_limb_widths_cons, BaseSystemProofs.peel_decode. - fold (BaseSystem.mul_each (two_p w)). - rewrite <-BaseSystemProofs.mul_each_base, BaseSystemProofs.mul_each_rep. - rewrite two_p_correct, (Z.mul_comm (2 ^ w)). - rewrite <-Z.shiftl_mul_pow2 by auto using in_eq. - rewrite bounded_iff in *. - rewrite Z.shiftr_add_shiftl_high by first - [ pose proof (sum_firstn_nonnegative i lw); split; auto using in_eq; specialize_by auto using in_cons; omega - | specialize (H 0%nat); rewrite !nth_default_cons in H; omega ]. - rewrite IHus with (limb_widths := lw) by - (auto using in_cons; rewrite ?bounded_iff; intro j; specialize (H (S j)); - rewrite !nth_default_cons_S in H; assumption). - repeat f_equal; try ring. - Qed. - - Lemma nth_default_limb_widths_nonneg : forall i, 0 <= nth_default 0 limb_widths i. - Proof using Type*. - intros; apply nth_default_preserves_properties; auto; omega. - Qed. Hint Resolve nth_default_limb_widths_nonneg. - - Lemma decode_firstn_pow2_mod : forall us i, - (i <= length us)%nat -> - length us = length limb_widths -> - bounded limb_widths us -> - BaseSystem.decode' base (firstn i us) = Z.pow2_mod (BaseSystem.decode' base us) (sum_firstn limb_widths i). - Proof using Type*. - intros us i H H0 H1; induction i; - repeat match goal with - | |- _ => rewrite sum_firstn_0, BaseSystemProofs.decode_nil, Z.pow2_mod_0_r; reflexivity - | |- _ => progress distr_length - | |- _ => progress autorewrite with simpl_firstn - | |- _ => rewrite firstn_succ with (d := 0) - | |- _ => rewrite BaseSystemProofs.set_higher - | |- _ => rewrite nth_default_base - | |- _ => rewrite IHi - | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; Z.zero_bounds) - | |- context[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) - | |- context[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 - | |- _ => solve [auto] - | |- _ => lia - end. - rewrite digit_select by assumption; apply Z.bits_inj'. - repeat match goal with - | |- _ => progress intros - | |- _ => progress autorewrite with Ztestbit - | |- _ => rewrite Z.testbit_pow2_mod by (omega || trivial) - | |- _ => break_if; try omega - | H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] => - rewrite (Z.testbit_neg_r _ (a-b)) by omega - | |- _ => reflexivity - | |- _ => solve [f_equal; ring] - | |- _ => rewrite sum_firstn_succ_default in *; - pose proof (nth_default_limb_widths_nonneg i); omega - end. - Qed. - - Lemma testbit_decode_firstn_high : forall us i n, - (i <= length us)%nat -> - length us = length limb_widths -> - bounded limb_widths us -> - sum_firstn limb_widths i <= n -> - Z.testbit (BaseSystem.decode base (firstn i us)) n = false. - Proof using Type*. - repeat match goal with - | |- _ => progress intros - | |- _ => progress autorewrite with Ztestbit - | |- _ => rewrite decode_firstn_pow2_mod - | |- _ => rewrite Z.testbit_pow2_mod - | |- _ => break_if - | |- _ => assumption - | |- _ => solve [auto] - | H : ?a <= ?b |- 0 <= ?b => assert (0 <= a) by (omega || auto); omega - end. - Qed. - - Lemma testbit_decode_high : forall us n, - length us = length limb_widths -> - bounded limb_widths us -> - sum_firstn limb_widths (length us) <= n -> - Z.testbit (BaseSystem.decode base us) n = false. - Proof using Type*. - intros us n H H0 H1. - erewrite <-(firstn_all _ us) by reflexivity. - auto using testbit_decode_firstn_high. - Qed. - - (** TODO: Figure out how to automate and clean up this proof *) - Lemma decode_nonneg : forall us, - length us = length limb_widths -> - bounded limb_widths us -> - 0 <= BaseSystem.decode base us. - Proof using Type*. - intros us H H0. - unfold bounded, BaseSystem.decode, BaseSystem.decode' in *; simpl in *. - pose 0 as zero. - assert (0 <= zero) by reflexivity. - replace base with (map (Z.mul (two_p zero)) base) - by (etransitivity; [ | apply map_id ]; apply map_ext; auto with zarith). - clearbody zero. - revert dependent zero. - generalize dependent limb_widths. - induction us as [|u us IHus]; intros [|w limb_widths'] ?? Hbounded ??; simpl in *; - try (reflexivity || congruence). - pose proof (Hbounded 0%nat) as Hbounded0. - pose proof (fun n => Hbounded (S n)) as HboundedS. - unfold nth_default, nth_error in Hbounded0. - unfold nth_default in HboundedS. - rewrite map_map. - unfold BaseSystem.accumulate at 1; simpl. - assert (0 < two_p zero) by (rewrite two_p_equiv; auto with zarith). - replace (map (fun x => two_p zero * (two_p w * x)) (base_from_limb_widths limb_widths')) with (map (Z.mul (two_p (zero + w))) (base_from_limb_widths limb_widths')) - by (apply map_ext; rewrite two_p_is_exp by auto with zarith omega; auto with zarith). - change 0 with (0 + 0) at 1. - apply Z.add_le_mono; simpl in *; auto with zarith. - Qed. - - Lemma decode_upper_bound : forall us, - length us = length limb_widths -> - bounded limb_widths us -> - 0 <= BaseSystem.decode base us < upper_bound limb_widths. - Proof using Type*. - cbv [upper_bound]; intros us H H0. - split. - { apply decode_nonneg; auto. } - { apply Z.testbit_false_bound; auto; intros. - rewrite testbit_decode_high; auto; - replace (length us) with (length limb_widths); try omega. } - Qed. - - Lemma decode_shift_app : forall us0 us1, (length (us0 ++ us1) <= length limb_widths)%nat -> - BaseSystem.decode base (us0 ++ us1) = (BaseSystem.decode (base_from_limb_widths (firstn (length us0) limb_widths)) us0) + ((BaseSystem.decode (base_from_limb_widths (skipn (length us0) limb_widths)) us1) << sum_firstn limb_widths (length us0)). - Proof using Type*. - unfold BaseSystem.decode; intros us0 us1 ?. - assert (0 <= sum_firstn limb_widths (length us0)) by auto using sum_firstn_nonnegative. - rewrite BaseSystemProofs.decode'_splice; autorewrite with push_firstn. - apply Z.add_cancel_l. - autorewrite with pull_base_from_limb_widths Zshift_to_pow zsimplify. - rewrite BaseSystemProofs.decode'_map_mul, two_p_correct; nia. - Qed. - - Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> - BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0)). - Proof using Type*. - intros us u0 H; etransitivity; [ apply (decode_shift_app (u0::nil)); assumption | ]. - transitivity (u0 * 1 + 0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << (nth_default 0 limb_widths 0 + 0))); [ | autorewrite with zsimplify; reflexivity ]. - destruct limb_widths; distr_length; reflexivity. - Qed. - - Lemma upper_bound_nil : upper_bound nil = 1. - Proof using Type. reflexivity. Qed. - - Lemma upper_bound_cons x xs : 0 <= x -> 0 <= sum_firstn xs (length xs) -> upper_bound (x::xs) = 2^x * upper_bound xs. - Proof using Type. - intros Hx Hxs. - unfold upper_bound; simpl. - autorewrite with simpl_sum_firstn pull_Zpow. - reflexivity. - Qed. - - Lemma upper_bound_app xs ys : 0 <= sum_firstn xs (length xs) -> 0 <= sum_firstn ys (length ys) -> upper_bound (xs ++ ys) = upper_bound xs * upper_bound ys. - Proof using Type. - intros Hxs Hys. - unfold upper_bound; simpl. - autorewrite with distr_length simpl_sum_firstn pull_Zpow. - reflexivity. - Qed. - -End Pow2BaseProofs. -Hint Rewrite base_from_limb_widths_cons base_from_limb_widths_nil : push_base_from_limb_widths. -Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths. - -Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths. -Hint Rewrite <- @firstn_base_from_limb_widths : pull_firstn. -Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths. -Hint Rewrite @firstn_base_from_limb_widths : push_firstn. -Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths. -Hint Rewrite <- @skipn_base_from_limb_widths : pull_skipn. -Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths. -Hint Rewrite @skipn_base_from_limb_widths : push_skipn. - -Hint Rewrite @base_from_limb_widths_length : distr_length. -Hint Rewrite @upper_bound_nil @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : push_upper_bound. -Hint Rewrite <- @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : pull_upper_bound. - -Section UniformBase. - Context {width : Z} (limb_width_nonneg : 0 <= width). - Context (limb_widths : list Z) - (limb_widths_uniform : forall w, In w limb_widths -> w = width). - Local Notation base := (base_from_limb_widths limb_widths). - - Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat -> - (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)). - Proof using Type*. - cbv [bounded]; intros us H; split; intro A; [ intros u H0 | intros i ]. - + let G := fresh "G" in - match goal with H : In _ us |- _ => - eapply In_nth in H; destruct H as [x G]; destruct G as [? G]; - rewrite <-nth_default_eq in G; rewrite <-G end. - specialize (A x). - split; try eapply A. - eapply Z.lt_le_trans; try apply A. - apply nth_default_preserves_properties; [ | apply Z.pow_le_mono_r; omega ] . - intros; apply Z.eq_le_incl. - f_equal; auto. - + apply nth_default_preserves_properties_length_dep; - try solve [apply nth_default_preserves_properties; split; Z.zero_bounds; rewrite limb_widths_uniform; auto || omega]. - intros; apply nth_default_preserves_properties_length_dep; try solve [intros; omega]. - let x := fresh "x" in intro x; intros; - replace x with width; try symmetry; auto. - Qed. - - Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. - Proof using Type*. - intros w H. - replace w with width by (symmetry; auto). - assumption. - Qed. - - Lemma nth_default_uniform_base_full : forall i, - nth_default 0 limb_widths i = if lt_dec i (length limb_widths) - then width else 0. - Admitted. - - Lemma nth_default_uniform_base : forall i, (i < length limb_widths)%nat -> - nth_default 0 limb_widths i = width. - Proof using Type*. - intros; rewrite nth_default_uniform_base_full. - edestruct lt_dec; omega. - Qed. - - Lemma sum_firstn_uniform_base : forall i, (i <= length limb_widths)%nat -> - sum_firstn limb_widths i = Z.of_nat i * width. - Proof using limb_widths_uniform. - clear limb_width_nonneg. (* clear this before induction so we don't depend on this *) - induction limb_widths as [|x xs IHxs]; (intros [|i] ?); - simpl @length in *; - autorewrite with simpl_sum_firstn push_Zof_nat zsimplify; - try reflexivity; - try omega. - assert (x = width) by auto with datatypes; subst. - rewrite IHxs by auto with datatypes omega; omega. - Qed. - - Lemma sum_firstn_uniform_base_strong : forall i, (length limb_widths <= i)%nat -> - sum_firstn limb_widths i = Z.of_nat (length limb_widths) * width. - Proof using limb_widths_uniform. - intros; rewrite sum_firstn_all, sum_firstn_uniform_base by omega; reflexivity. - Qed. - - Lemma upper_bound_uniform : upper_bound limb_widths = 2^(Z.of_nat (length limb_widths) * width). - Proof using limb_widths_uniform. - unfold upper_bound; rewrite sum_firstn_uniform_base_strong by omega; reflexivity. - Qed. - - (* TODO : move *) - Lemma decode_truncate_base : forall us bs, BaseSystem.decode bs us = BaseSystem.decode (firstn (length us) bs) us. - Proof using Type. - clear. - induction us as [|a us IHus]; intros bs. - + rewrite !BaseSystemProofs.decode_nil; reflexivity. - + distr_length. - destruct bs. - - rewrite firstn_nil, !BaseSystemProofs.decode_base_nil; reflexivity. - - rewrite firstn_cons, !BaseSystemProofs.peel_decode. - f_equal. - apply IHus. - Qed. - - (* TODO : move *) - Lemma tl_repeat : forall {A} xs n (x : A), (forall y, In y xs -> y = x) -> - (n < length xs)%nat -> - firstn n xs = firstn n (tl xs). - Proof using Type. - intros A xs n x H H0. - erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ]. - rewrite ListUtil.tl_repeat. - autorewrite with push_firstn. - apply f_equal; omega *. - Qed. - - Lemma decode_tl_base : forall us, (length us < length limb_widths)%nat -> - BaseSystem.decode base us = BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us. - Proof using limb_widths_uniform. - intros. - match goal with |- BaseSystem.decode ?b1 _ = BaseSystem.decode ?b2 _ => - rewrite (decode_truncate_base _ b1), (decode_truncate_base _ b2) end. - rewrite !firstn_base_from_limb_widths. - do 2 f_equal. - eauto using tl_repeat. - Qed. - - Lemma decode_shift_uniform_tl : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> - BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode (base_from_limb_widths (tl limb_widths)) us) << width). - Proof using Type*. - intros. - rewrite <- (nth_default_uniform_base 0) by distr_length. - rewrite decode_shift by auto using uniform_limb_widths_nonneg. - reflexivity. - Qed. - - Lemma decode_shift_uniform_app : forall us0 us1, (length (us0 ++ us1) <= length limb_widths)%nat -> - BaseSystem.decode base (us0 ++ us1) = (BaseSystem.decode (base_from_limb_widths (firstn (length us0) limb_widths)) us0) + ((BaseSystem.decode (base_from_limb_widths (skipn (length us0) limb_widths)) us1) << (Z.of_nat (length us0) * width)). - Proof using Type*. - intros. - rewrite <- sum_firstn_uniform_base by (distr_length; omega). - rewrite decode_shift_app by auto using uniform_limb_widths_nonneg. - reflexivity. - Qed. -End UniformBase. diff --git a/src/LegacyArithmetic/README.md b/src/LegacyArithmetic/README.md deleted file mode 100644 index b0137664c..000000000 --- a/src/LegacyArithmetic/README.md +++ /dev/null @@ -1,3 +0,0 @@ -The development of this directory predates `src/Arithmetic`, and should probably -be considered to be superseded by it. The p256 Montgomery reduction for -a 128-bit cpu synthesized here still works. diff --git a/src/LegacyArithmetic/VerdiTactics.v b/src/LegacyArithmetic/VerdiTactics.v deleted file mode 100644 index 4060fc675..000000000 --- a/src/LegacyArithmetic/VerdiTactics.v +++ /dev/null @@ -1,414 +0,0 @@ -(* -Copyright (c) 2014-2015, Verdi Team -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are -met: - -1. Redistributions of source code must retain the above copyright -notice, this list of conditions and the following disclaimer. - -2. Redistributions in binary form must reproduce the above copyright -notice, this list of conditions and the following disclaimer in the -documentation and/or other materials provided with the distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -*) - -Ltac subst_max := idtac "VerdiTactics is deprecated in fiat-crypto"; - repeat match goal with - | [ H : ?X = _ |- _ ] => subst X - | [H : _ = ?X |- _] => subst X - end. - -Ltac inv H := idtac "VerdiTactics is deprecated in fiat-crypto"; inversion H; subst_max. -Ltac invc H := idtac "VerdiTactics is deprecated in fiat-crypto"; inv H; clear H. -Ltac invcs H := idtac "VerdiTactics is deprecated in fiat-crypto"; invc H; simpl in *. - -Ltac break_if := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ |- context [ if ?X then _ else _ ] ] => - match type of X with - | sumbool _ _ => destruct X - | _ => destruct X eqn:? - end - | [ H : context [ if ?X then _ else _ ] |- _] => - match type of X with - | sumbool _ _ => destruct X - | _ => destruct X eqn:? - end - end. - -Ltac break_match_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : context [ match ?X with _ => _ end ] |- _] => - match type of X with - | sumbool _ _ => destruct X - | _ => destruct X eqn:? - end - end. - -Ltac break_match_goal := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ |- context [ match ?X with _ => _ end ] ] => - match type of X with - | sumbool _ _ => destruct X - | _ => destruct X eqn:? - end - end. - -Ltac break_match := idtac "VerdiTactics is deprecated in fiat-crypto"; break_match_goal || break_match_hyp. - - -Ltac break_exists := idtac "VerdiTactics is deprecated in fiat-crypto"; - repeat match goal with - | [H : exists _, _ |- _ ] => destruct H - end. - -Ltac break_exists_exists := idtac "VerdiTactics is deprecated in fiat-crypto"; - repeat match goal with - | H:exists _, _ |- _ => - let x := fresh "x" in - destruct H as [x]; exists x - end. - -Ltac break_and := idtac "VerdiTactics is deprecated in fiat-crypto"; - repeat match goal with - | [H : _ /\ _ |- _ ] => destruct H - end. - -Ltac solve_by_inversion' tac := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [H : _ |- _] => solve [inv H; tac] - end. - -Ltac solve_by_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; solve_by_inversion' auto. - -Ltac apply_fun f H:= idtac "VerdiTactics is deprecated in fiat-crypto"; - match type of H with - | ?X = ?Y => assert (f X = f Y) - end. - -Ltac conclude H tac := idtac "VerdiTactics is deprecated in fiat-crypto"; - (let H' := fresh in - match type of H with - | ?P -> _ => assert P as H' by (tac) - end; specialize (H H'); clear H'). - -Ltac concludes := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?P -> _ |- _ ] => conclude H auto - end. - -Ltac forward H := idtac "VerdiTactics is deprecated in fiat-crypto"; - let H' := fresh in - match type of H with - | ?P -> _ => assert P as H' - end. - -Ltac forwards := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?P -> _ |- _ ] => forward H - end. - -Ltac find_contradiction := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?X = _, H' : ?X = _ |- _ ] => rewrite H in H'; solve_by_inversion - end. - -Ltac find_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?X _ _ _ _ = _, H' : ?X _ _ _ _ = _ |- _ ] => rewrite H in H' - | [ H : ?X = _, H' : ?X = _ |- _ ] => rewrite H in H' - | [ H : ?X = _, H' : context [ ?X ] |- _ ] => rewrite H in H' - | [ H : ?X = _ |- context [ ?X ] ] => rewrite H - end. - -Ltac find_rewrite_lem lem := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => - rewrite lem in H; [idtac] - end. - -Ltac find_rewrite_lem_by lem t := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => - rewrite lem in H by t - end. - -Ltac find_erewrite_lem lem := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _] => erewrite lem in H by eauto - end. - -Ltac find_reverse_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ = ?X _ _ _ _, H' : ?X _ _ _ _ = _ |- _ ] => rewrite <- H in H' - | [ H : _ = ?X, H' : context [ ?X ] |- _ ] => rewrite <- H in H' - | [ H : _ = ?X |- context [ ?X ] ] => rewrite <- H - end. - -Ltac find_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?X _ _ _ _ _ _ = ?X _ _ _ _ _ _ |- _ ] => invc H - | [ H : ?X _ _ _ _ _ = ?X _ _ _ _ _ |- _ ] => invc H - | [ H : ?X _ _ _ _ = ?X _ _ _ _ |- _ ] => invc H - | [ H : ?X _ _ _ = ?X _ _ _ |- _ ] => invc H - | [ H : ?X _ _ = ?X _ _ |- _ ] => invc H - | [ H : ?X _ = ?X _ |- _ ] => invc H - end. - -Ltac prove_eq := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?X ?x1 ?x2 ?x3 = ?X ?y1 ?y2 ?y3 |- _ ] => - assert (x1 = y1) by congruence; - assert (x2 = y2) by congruence; - assert (x3 = y3) by congruence; - clear H - | [ H : ?X ?x1 ?x2 = ?X ?y1 ?y2 |- _ ] => - assert (x1 = y1) by congruence; - assert (x2 = y2) by congruence; - clear H - | [ H : ?X ?x1 = ?X ?y1 |- _ ] => - assert (x1 = y1) by congruence; - clear H - end. - -Ltac tuple_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : (_, _, _, _) = (_, _, _, _) |- _ ] => invc H - | [ H : (_, _, _) = (_, _, _) |- _ ] => invc H - | [ H : (_, _) = (_, _) |- _ ] => invc H - end. - -Ltac f_apply H f := idtac "VerdiTactics is deprecated in fiat-crypto"; - match type of H with - | ?X = ?Y => - assert (f X = f Y) by (rewrite H; auto) - end. - -Ltac break_let := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:? - | [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:? - end. - -Ltac break_or_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ \/ _ |- _ ] => invc H - end. - -Ltac copy_apply lem H := idtac "VerdiTactics is deprecated in fiat-crypto"; - let x := fresh in - pose proof H as x; - apply lem in x. - -Ltac copy_eapply lem H := idtac "VerdiTactics is deprecated in fiat-crypto"; - let x := fresh in - pose proof H as x; - eapply lem in x. - -Ltac conclude_using tac := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?P -> _ |- _ ] => conclude H tac - end. - -Ltac find_higher_order_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ = _ |- _ ] => rewrite H in * - | [ H : forall _, _ = _ |- _ ] => rewrite H in * - | [ H : forall _ _, _ = _ |- _ ] => rewrite H in * - end. - -Ltac find_reverse_higher_order_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ = _ |- _ ] => rewrite <- H in * - | [ H : forall _, _ = _ |- _ ] => rewrite <- H in * - | [ H : forall _ _, _ = _ |- _ ] => rewrite <- H in * - end. - -Ltac clean := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?X = ?X |- _ ] => clear H - end. - -Ltac find_apply_hyp_goal := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => solve [apply H] - end. - -Ltac find_copy_apply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => copy_apply lem H - end. - -Ltac find_apply_hyp_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : forall _, _ -> _, - H' : _ |- _ ] => - apply H in H'; [idtac] - | [ H : _ -> _ , H' : _ |- _ ] => - apply H in H'; auto; [idtac] - end. - -Ltac find_copy_apply_hyp_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : forall _, _ -> _, - H' : _ |- _ ] => - copy_apply H H'; [idtac] - | [ H : _ -> _ , H' : _ |- _ ] => - copy_apply H H'; auto; [idtac] - end. - -Ltac find_apply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => apply lem in H - end. - -Ltac find_eapply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => eapply lem in H - end. - -Ltac insterU H := idtac "VerdiTactics is deprecated in fiat-crypto"; - match type of H with - | forall _ : ?T, _ => - let x := fresh "x" in - evar (x : T); - let x' := (eval unfold x in x) in - clear x; specialize (H x') - end. - -Ltac find_insterU := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : forall _, _ |- _ ] => insterU H - end. - -Ltac eapply_prop P := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | H : P _ |- _ => - eapply H - end. - -Ltac isVar t := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | v : _ |- _ => - match t with - | v => idtac - end - end. - -Ltac remGen t := idtac "VerdiTactics is deprecated in fiat-crypto"; - let x := fresh in - let H := fresh in - remember t as x eqn:H; - generalize dependent H. - -Ltac remGenIfNotVar t := idtac "VerdiTactics is deprecated in fiat-crypto"; first [isVar t| remGen t]. - -Ltac rememberNonVars H := idtac "VerdiTactics is deprecated in fiat-crypto"; - match type of H with - | _ ?a ?b ?c ?d ?e => - remGenIfNotVar a; - remGenIfNotVar b; - remGenIfNotVar c; - remGenIfNotVar d; - remGenIfNotVar e - | _ ?a ?b ?c ?d => - remGenIfNotVar a; - remGenIfNotVar b; - remGenIfNotVar c; - remGenIfNotVar d - | _ ?a ?b ?c => - remGenIfNotVar a; - remGenIfNotVar b; - remGenIfNotVar c - | _ ?a ?b => - remGenIfNotVar a; - remGenIfNotVar b - | _ ?a => - remGenIfNotVar a - end. - -Ltac generalizeEverythingElse H := idtac "VerdiTactics is deprecated in fiat-crypto"; - repeat match goal with - | [ x : ?T |- _ ] => - first [ - match H with - | x => fail 2 - end | - match type of H with - | context [x] => fail 2 - end | - revert x] - end. - -Ltac prep_induction H := idtac "VerdiTactics is deprecated in fiat-crypto"; - rememberNonVars H; - generalizeEverythingElse H. - -Ltac econcludes := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?P -> _ |- _ ] => conclude H eauto - end. - -Ltac find_copy_eapply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : _ |- _ ] => copy_eapply lem H - end. - -Ltac apply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : context [ P ], H' : context [ Q ] |- _ ] => - apply H in H' - end. - - -Ltac eapply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : context [ P ], H' : context [ Q ] |- _ ] => - eapply H in H' - end. - -Ltac copy_eapply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : context [ P ], H' : context [ Q ] |- _ ] => - copy_eapply H H' - end. - -Ltac find_false := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | H : _ -> False |- _ => exfalso; apply H - end. - -Ltac injc H := idtac "VerdiTactics is deprecated in fiat-crypto"; - injection H; clear H; intro; subst_max. - -Ltac find_injection := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : ?X _ _ _ _ _ _ = ?X _ _ _ _ _ _ |- _ ] => injc H - | [ H : ?X _ _ _ _ _ = ?X _ _ _ _ _ |- _ ] => injc H - | [ H : ?X _ _ _ _ = ?X _ _ _ _ |- _ ] => injc H - | [ H : ?X _ _ _ = ?X _ _ _ |- _ ] => injc H - | [ H : ?X _ _ = ?X _ _ |- _ ] => injc H - | [ H : ?X _ = ?X _ |- _ ] => injc H - end. - -Ltac aggresive_rewrite_goal := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with H : _ |- _ => rewrite H end. - -Ltac break_exists_name x := idtac "VerdiTactics is deprecated in fiat-crypto"; - match goal with - | [ H : exists _, _ |- _ ] => destruct H as [x H] - end. diff --git a/src/LegacyArithmetic/ZBounded.v b/src/LegacyArithmetic/ZBounded.v deleted file mode 100644 index 2eec4122b..000000000 --- a/src/LegacyArithmetic/ZBounded.v +++ /dev/null @@ -1,158 +0,0 @@ -(*** Bounded ℤ-Like Types *) -(** This file specifies a ℤ-like type of bounded integers, with - operations for Montgomery Reduction and Barrett Reduction. *) -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Notations. - -Local Open Scope Z_scope. - -Class ZLikeOps (small_bound smaller_bound : Z) (modulus : Z) := - { - LargeT : Type; - SmallT : Type; - modulus_digits : SmallT; - decode_large : LargeT -> Z; - decode_small : SmallT -> Z; - Mod_SmallBound : LargeT -> SmallT; - DivBy_SmallBound : LargeT -> SmallT; - DivBy_SmallerBound : LargeT -> SmallT; - Mul : SmallT -> SmallT -> LargeT; - CarryAdd : LargeT -> LargeT -> bool * LargeT; - CarrySubSmall : SmallT -> SmallT -> bool * SmallT; - ConditionalSubtract : bool -> SmallT -> SmallT; - ConditionalSubtractModulus : SmallT -> SmallT - }. - -Delimit Scope small_zlike_scope with small_zlike. -Delimit Scope large_zlike_scope with large_zlike. -Local Open Scope small_zlike_scope. -Local Open Scope large_zlike_scope. -Local Open Scope Z_scope. -Bind Scope small_zlike_scope with SmallT. -Bind Scope large_zlike_scope with LargeT. -Arguments decode_large (_ _ _)%Z _ _%large_zlike. -Arguments decode_small (_ _ _)%Z _ _%small_zlike. -Arguments Mod_SmallBound (_ _ _)%Z _ _%large_zlike. -Arguments DivBy_SmallBound (_ _ _)%Z _ _%large_zlike. -Arguments DivBy_SmallerBound (_ _ _)%Z _ _%large_zlike. -Arguments Mul (_ _ _)%Z _ (_ _)%small_zlike. -Arguments CarryAdd (_ _ _)%Z _ (_ _)%large_zlike. -Arguments CarrySubSmall (_ _ _)%Z _ (_ _)%large_zlike. -Arguments ConditionalSubtract (_ _ _)%Z _ _%bool _%small_zlike. -Arguments ConditionalSubtractModulus (_ _ _)%Z _ _%small_zlike. - -Infix "*" := Mul : large_zlike_scope. -Notation "x + y" := (snd (CarryAdd x y)) : large_zlike_scope. - -Class ZLikeProperties {small_bound smaller_bound modulus : Z} (Zops : ZLikeOps small_bound smaller_bound modulus) := - { - large_valid : LargeT -> Prop; - medium_valid : LargeT -> Prop; - small_valid : SmallT -> Prop; - decode_large_valid : forall v, large_valid v -> 0 <= decode_large v < small_bound * small_bound; - decode_medium_valid : forall v, medium_valid v -> 0 <= decode_large v < small_bound * smaller_bound; - medium_to_large_valid : forall v, medium_valid v -> large_valid v; - decode_small_valid : forall v, small_valid v -> 0 <= decode_small v < small_bound; - modulus_digits_valid : small_valid modulus_digits; - modulus_digits_correct : decode_small modulus_digits = modulus; - Mod_SmallBound_valid : forall v, large_valid v -> small_valid (Mod_SmallBound v); - Mod_SmallBound_correct - : forall v, large_valid v -> decode_small (Mod_SmallBound v) = decode_large v mod small_bound; - DivBy_SmallBound_valid : forall v, large_valid v -> small_valid (DivBy_SmallBound v); - DivBy_SmallBound_correct - : forall v, large_valid v -> decode_small (DivBy_SmallBound v) = decode_large v / small_bound; - DivBy_SmallerBound_valid : forall v, medium_valid v -> small_valid (DivBy_SmallerBound v); - DivBy_SmallerBound_correct - : forall v, medium_valid v -> decode_small (DivBy_SmallerBound v) = decode_large v / smaller_bound; - Mul_valid : forall x y, small_valid x -> small_valid y -> large_valid (Mul x y); - Mul_correct - : forall x y, small_valid x -> small_valid y -> decode_large (Mul x y) = decode_small x * decode_small y; - CarryAdd_valid : forall x y, large_valid x -> large_valid y -> large_valid (snd (CarryAdd x y)); - CarryAdd_correct_fst - : forall x y, large_valid x -> large_valid y -> fst (CarryAdd x y) = (small_bound * small_bound <=? decode_large x + decode_large y); - CarryAdd_correct_snd - : forall x y, large_valid x -> large_valid y -> decode_large (snd (CarryAdd x y)) = (decode_large x + decode_large y) mod (small_bound * small_bound); - CarrySubSmall_valid : forall x y, small_valid x -> small_valid y -> small_valid (snd (CarrySubSmall x y)); - CarrySubSmall_correct_fst - : forall x y, small_valid x -> small_valid y -> fst (CarrySubSmall x y) = (decode_small x - decode_small y <? 0); - CarrySubSmall_correct_snd - : forall x y, small_valid x -> small_valid y -> decode_small (snd (CarrySubSmall x y)) = (decode_small x - decode_small y) mod small_bound; - ConditionalSubtract_valid : forall b x, small_valid x -> small_valid (ConditionalSubtract b x); - ConditionalSubtract_correct - : forall b x, small_valid x -> decode_small (ConditionalSubtract b x) - = if b then (decode_small x - decode_small modulus_digits) mod small_bound else decode_small x; - ConditionalSubtractModulus_valid : forall x, small_valid x -> small_valid (ConditionalSubtractModulus x); - ConditionalSubtractModulus_correct - : forall x, small_valid x -> decode_small (ConditionalSubtractModulus x) - = if (decode_small x <? decode_small modulus_digits) then decode_small x else decode_small x - decode_small modulus_digits - }. - -Arguments ZLikeProperties [small_bound smaller_bound modulus] Zops, small_bound smaller_bound modulus {Zops}. - -Existing Class large_valid. -Existing Class medium_valid. -Existing Class small_valid. -Existing Instances Mod_SmallBound_valid DivBy_SmallerBound_valid DivBy_SmallBound_valid Mul_valid CarryAdd_valid CarrySubSmall_valid ConditionalSubtract_valid ConditionalSubtractModulus_valid modulus_digits_valid medium_to_large_valid. - -Lemma ConditionalSubtractModulus_correct' - {small_bound smaller_bound modulus : Z} {Zops : ZLikeOps small_bound smaller_bound modulus} - {Zprops : ZLikeProperties Zops} - : forall x, small_valid x -> decode_small (ConditionalSubtractModulus x) - = if (decode_small modulus_digits <=? decode_small x) then decode_small x - decode_small modulus_digits else decode_small x. -Proof. - intros; rewrite ConditionalSubtractModulus_correct by assumption. - break_match; Z.ltb_to_lt; omega. -Qed. - -Lemma modulus_nonneg {small_bound smaller_bound modulus} (Zops : ZLikeOps small_bound smaller_bound modulus) {_ : ZLikeProperties Zops} : 0 <= modulus. -Proof. - pose proof (decode_small_valid _ modulus_digits_valid) as H. - rewrite modulus_digits_correct in H. - omega. -Qed. - -Create HintDb push_zlike_decode discriminated. -Create HintDb pull_zlike_decode discriminated. -Hint Rewrite @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @ConditionalSubtractModulus_correct' @modulus_digits_correct using solve [ typeclasses eauto ] : push_zlike_decode. -Hint Rewrite <- @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @modulus_digits_correct using solve [ typeclasses eauto ] : pull_zlike_decode. - -Ltac get_modulus := - match goal with - | [ _ : ZLikeOps _ _ ?modulus |- _ ] => modulus - end. - -Ltac push_zlike_decode := - let modulus := get_modulus in - repeat first [ erewrite !Mod_SmallBound_correct by typeclasses eauto - | erewrite !DivBy_SmallBound_correct by typeclasses eauto - | erewrite !DivBy_SmallerBound_correct by typeclasses eauto - | erewrite !Mul_correct by typeclasses eauto - | erewrite !CarryAdd_correct_fst by typeclasses eauto - | erewrite !CarryAdd_correct_snd by typeclasses eauto - | erewrite !CarrySubSmall_correct_fst by typeclasses eauto - | erewrite !CarrySubSmall_correct_snd by typeclasses eauto - | erewrite !ConditionalSubtract_correct by typeclasses eauto - | erewrite !ConditionalSubtractModulus_correct by typeclasses eauto - | erewrite !ConditionalSubtractModulus_correct' by typeclasses eauto - | erewrite !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ]. -Ltac pull_zlike_decode := - let modulus := get_modulus in - repeat first [ match goal with - | [ |- context G[modulus] ] - => let G' := context G[decode_small modulus_digits] in - cut G'; [ rewrite !modulus_digits_correct by typeclasses eauto; exact (fun x => x) | ] - end - | erewrite <- !Mod_SmallBound_correct by typeclasses eauto - | erewrite <- !DivBy_SmallBound_correct by typeclasses eauto - | erewrite <- !DivBy_SmallerBound_correct by typeclasses eauto - | erewrite <- !Mul_correct by typeclasses eauto - | erewrite <- !CarryAdd_correct_fst by typeclasses eauto - | erewrite <- !CarryAdd_correct_snd by typeclasses eauto - | erewrite <- !ConditionalSubtract_correct by typeclasses eauto - | erewrite <- !CarrySubSmall_correct_fst by typeclasses eauto - | erewrite <- !CarrySubSmall_correct_snd by typeclasses eauto - | erewrite <- !ConditionalSubtractModulus_correct by typeclasses eauto - | erewrite <- !ConditionalSubtractModulus_correct' by typeclasses eauto - | erewrite <- !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ]. diff --git a/src/LegacyArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v deleted file mode 100644 index f0dfc6a40..000000000 --- a/src/LegacyArithmetic/ZBoundedZ.v +++ /dev/null @@ -1,90 +0,0 @@ -(*** ℤ can be a bounded ℤ-Like type *) -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Pow2Mod. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Notations. - -Local Open Scope Z_scope. - -Global Instance ZZLikeOps small_bound_exp smaller_bound_exp modulus : ZLikeOps (2^small_bound_exp) (2^smaller_bound_exp) modulus - := { LargeT := Z; - SmallT := Z; - modulus_digits := modulus; - decode_large x := x; - decode_small x := x; - Mod_SmallBound x := Z.pow2_mod x small_bound_exp; - DivBy_SmallBound x := Z.shiftr x small_bound_exp; - DivBy_SmallerBound x := Z.shiftr x smaller_bound_exp; - Mul x y := (x * y)%Z; - CarryAdd x y := dlet xpy := x + y in - ((2^small_bound_exp * 2^small_bound_exp <=? xpy), Z.pow2_mod xpy (2 * small_bound_exp)); - CarrySubSmall x y := dlet xmy := x - y in (xmy <? 0, Z.pow2_mod xmy small_bound_exp); - ConditionalSubtract b x := dlet x := x in if b then Z.pow2_mod (x - modulus) small_bound_exp else x; - ConditionalSubtractModulus x := dlet x := x in if x <? modulus then x else x - modulus }. - -Local Arguments Z.mul !_ !_. - -Class cls_is_true (x : bool) := build_is_true : x = true. -Hint Extern 1 (cls_is_true ?b) => vm_compute; reflexivity : typeclass_instances. - -Local Ltac pre_t := - unfold cls_is_true, Let_In in *; Z.ltb_to_lt; - match goal with - | [ H : ?smaller_bound_exp <= ?small_bound_exp |- _ ] - => is_var smaller_bound_exp; is_var small_bound_exp; - assert (2^smaller_bound_exp <= 2^small_bound_exp) by auto with zarith; - assert (2^small_bound_exp * 2^smaller_bound_exp <= 2^small_bound_exp * 2^small_bound_exp) by auto with zarith - end. - -Local Ltac t_step := - first [ progress simpl in * - | progress intros - | progress autorewrite with push_Zpow Zshift_to_pow in * - | rewrite Z.pow2_mod_spec by omega - | progress Z.ltb_to_lt - | progress unfold Let_In in * - | solve [ auto with zarith ] - | nia - | progress break_match ]. -Local Ltac t := pre_t; repeat t_step. - -Global Instance ZZLikeProperties {small_bound_exp smaller_bound_exp modulus} - {Hss : cls_is_true (0 <=? smaller_bound_exp)} - {Hs : cls_is_true (0 <=? small_bound_exp)} - {Hs_ss : cls_is_true (smaller_bound_exp <=? small_bound_exp)} - {Hmod0 : cls_is_true (0 <=? modulus)} - {Hmod1 : cls_is_true (modulus <? 2^small_bound_exp)} - : ZLikeProperties (@ZZLikeOps small_bound_exp smaller_bound_exp modulus). -Proof. -refine {| large_valid x := 0 <= x < 2^(2*small_bound_exp); - medium_valid x := 0 <= x < 2^(small_bound_exp + smaller_bound_exp); - small_valid x := 0 <= x < 2^small_bound_exp |}. - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } - { abstract t. } -Defined. |