aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemOpt.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemOpt.v103
1 files changed, 17 insertions, 86 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 116fe10e5..abbb0e573 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -1,5 +1,4 @@
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
@@ -13,6 +12,12 @@ Require Import Coq.QArith.QArith Coq.QArith.Qround.
Require Import Crypto.Tactics.VerdiTactics.
Local Open Scope Z.
+Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
+ coeff : BaseSystem.digits;
+ coeff_length : (length coeff = length PseudoMersenneBaseParamProofs.base)%nat;
+ coeff_mod: (BaseSystem.decode PseudoMersenneBaseParamProofs.base coeff) mod m = 0
+}.
+
(* Computed versions of some functions. *)
Definition Z_add_opt := Eval compute in Z.add.
@@ -95,18 +100,6 @@ Ltac kill_precondition H :=
forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|];
subst_precondition.
-Ltac compute_formula :=
- match goal with
- | [H : _ -> _ -> PseudoMersenneBaseRep.rep _ ?result |- PseudoMersenneBaseRep.rep _ ?result] => kill_precondition H; compute_formula
- | [H : _ -> PseudoMersenneBaseRep.rep _ ?result |- PseudoMersenneBaseRep.rep _ ?result] => kill_precondition H; compute_formula
- | [H : @PseudoMersenneBaseRep.rep ?M ?P _ ?result |- @PseudoMersenneBaseRep.rep ?M ?P _ ?result] =>
- let m := fresh "m" in set (m := M) in H at 1; change M with m at 1;
- let p := fresh "p" in set (p := P) in H at 1; change P with p at 1;
- let r := fresh "r" in set (r := result) in H |- *;
- cbv -[m p r PseudoMersenneBaseRep.rep] in H;
- repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H
- end.
-
Section Carries.
Context `{prm : PseudoMersenneBaseParams}
(* allows caller to precompute k and c *)
@@ -321,58 +314,37 @@ End Carries.
Section Addition.
Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
- Definition add_opt_sig (us vs : T) : { b : digits | b = add us vs }.
+ Definition add_opt_sig (us vs : digits) : { b : digits | b = add us vs }.
Proof.
eexists.
cbv [BaseSystem.add].
reflexivity.
Defined.
- Definition add_opt (us vs : T) : digits
+ Definition add_opt (us vs : digits) : digits
:= Eval cbv [proj1_sig add_opt_sig] in proj1_sig (add_opt_sig us vs).
Definition add_opt_correct us vs
: add_opt us vs = add us vs
:= proj2_sig (add_opt_sig us vs).
-
- Lemma add_opt_rep: forall (u v : T) (x y : F modulus),
- PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
- PseudoMersenneBaseRep.rep (add_opt u v) (x + y)%F.
- Proof.
- intros.
- rewrite add_opt_correct.
- auto using PseudoMersenneBaseRep.add_rep.
- Qed.
-
End Addition.
Section Subtraction.
Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
- Definition sub_opt_sig (us vs : T) : { b : digits | b = sub coeff coeff_mod us vs }.
+ Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff coeff_mod us vs }.
Proof.
eexists.
cbv [BaseSystem.add ModularBaseSystem.sub BaseSystem.sub].
reflexivity.
Defined.
- Definition sub_opt (us vs : T) : digits
+ Definition sub_opt (us vs : digits) : digits
:= Eval cbv [proj1_sig sub_opt_sig] in proj1_sig (sub_opt_sig us vs).
Definition sub_opt_correct us vs
: sub_opt us vs = sub coeff coeff_mod us vs
:= proj2_sig (sub_opt_sig us vs).
-
- Lemma sub_opt_rep: forall (u v : T) (x y : F modulus),
- PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
- PseudoMersenneBaseRep.rep (sub_opt u v) (x - y)%F.
- Proof.
- intros.
- rewrite sub_opt_correct.
- change (sub coeff coeff_mod) with PseudoMersenneBaseRep.sub.
- apply PseudoMersenneBaseRep.sub_rep; auto using coeff_length.
- Qed.
-
End Subtraction.
Section Multiplication.
@@ -493,7 +465,7 @@ Section Multiplication.
reflexivity. }
Qed.
- Definition mul_opt_sig (us vs : T) : { b : digits | b = mul us vs }.
+ Definition mul_opt_sig (us vs : digits) : { b : digits | b = mul us vs }.
Proof.
eexists.
cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce].
@@ -507,14 +479,14 @@ Section Multiplication.
reflexivity.
Defined.
- Definition mul_opt (us vs : T) : digits
+ Definition mul_opt (us vs : digits) : digits
:= Eval cbv [proj1_sig mul_opt_sig] in proj1_sig (mul_opt_sig us vs).
Definition mul_opt_correct us vs
: mul_opt us vs = mul us vs
:= proj2_sig (mul_opt_sig us vs).
- Definition carry_mul_opt_sig (us vs : T) : { b : digits | b = carry_mul us vs }.
+ Definition carry_mul_opt_sig (us vs : digits) : { b : digits | b = carry_mul us vs }.
Proof.
eexists.
cbv [carry_mul].
@@ -523,23 +495,12 @@ Section Multiplication.
reflexivity.
Defined.
- Definition carry_mul_opt (us vs : T) : digits
+ Definition carry_mul_opt (us vs : digits) : digits
:= Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig us vs).
Definition carry_mul_opt_correct us vs
: carry_mul_opt us vs = carry_mul us vs
:= proj2_sig (carry_mul_opt_sig us vs).
-
- Lemma carry_mul_opt_rep:
- forall (u v : T) (x y : F modulus), PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
- PseudoMersenneBaseRep.rep (carry_mul_opt u v) (x * y)%F.
- Proof.
- intros.
- rewrite carry_mul_opt_correct.
- change carry_mul with PseudoMersenneBaseRep.mul.
- auto using PseudoMersenneBaseRep.mul_rep.
- Qed.
-
End Multiplication.
Record freezePreconditions {modulus} (prm : PseudoMersenneBaseParams modulus) int_width :=
@@ -605,7 +566,7 @@ Section Canonicalization.
carry_full_3_opt_cps f us = f (carry_full (carry_full (carry_full us))) :=
proj2_sig (carry_full_3_opt_cps_sig f us).
- Definition freeze_opt_sig (us : T) :
+ Definition freeze_opt_sig (us : digits) :
{ b : digits | b = freeze us }.
Proof.
eexists.
@@ -632,40 +593,10 @@ Section Canonicalization.
reflexivity.
Defined.
- Definition freeze_opt (us : T) : digits
+ Definition freeze_opt (us : digits) : digits
:= Eval cbv beta iota delta [proj1_sig freeze_opt_sig] in proj1_sig (freeze_opt_sig us).
Definition freeze_opt_correct us
: freeze_opt us = freeze us
:= proj2_sig (freeze_opt_sig us).
-
- Lemma freeze_opt_canonical: forall us vs x,
- @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x ->
- @pre_carry_bounds _ _ int_width vs -> PseudoMersenneBaseRep.rep vs x ->
- freeze_opt us = freeze_opt vs.
- Proof.
- intros.
- rewrite !freeze_opt_correct.
- change PseudoMersenneBaseRep.rep with rep in *.
- eapply freeze_canonical with (B := int_width); eauto.
- Qed.
-
- Lemma freeze_opt_preserves_rep : forall us x, PseudoMersenneBaseRep.rep us x ->
- PseudoMersenneBaseRep.rep (freeze_opt us) x.
- Proof.
- intros.
- rewrite freeze_opt_correct.
- change PseudoMersenneBaseRep.rep with rep in *.
- eapply freeze_preserves_rep; eauto.
- Qed.
-
- Lemma freeze_opt_spec : forall us vs x, rep us x -> rep vs x ->
- @pre_carry_bounds _ _ int_width us ->
- @pre_carry_bounds _ _ int_width vs ->
- (PseudoMersenneBaseRep.rep (freeze_opt us) x /\ freeze_opt us = freeze_opt vs).
- Proof.
- split; eauto using freeze_opt_canonical.
- auto using freeze_opt_preserves_rep.
- Qed.
-
-End Canonicalization. \ No newline at end of file
+End Canonicalization.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 02:22:28 +0000