aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Specific/Framework/ArithmeticSynthesis/Base.v155
-rw-r--r--src/Specific/Framework/ArithmeticSynthesis/BasePackage.v15
-rw-r--r--src/Specific/Framework/CurveParameters.v20
-rw-r--r--src/Specific/Framework/CurveParametersPackage.v4
4 files changed, 128 insertions, 66 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index 7c80b238d..81aff8dea 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -5,6 +5,7 @@ Require Import Crypto.Specific.Framework.CurveParameters.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
Require Import Crypto.Util.QUtil.
Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.CacheTerm.
@@ -31,68 +32,21 @@ Section wt.
Local Coercion Z.pos : positive >-> Z.
Definition wt_gen (m : positive) (sz : nat) (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i).
End wt.
-Ltac pose_wt m sz wt :=
- let v := (eval cbv [wt_gen] in (wt_gen m sz)) in
- cache_term v wt.
-
-Ltac pose_sz2 sz sz2 :=
- let v := (eval vm_compute in ((sz * 2) - 1)%nat) in
- cache_term v sz2.
-Ltac pose_half_sz sz half_sz :=
- let v := (eval compute in (sz / 2)%nat) in
- cache_term v half_sz.
+Section gen.
+ Context (m : positive)
+ (sz : nat)
+ (coef_div_modulus : nat).
-Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
- cache_proof_with_type_by
- (half_sz <> 0%nat)
- ltac:(cbv; congruence)
- half_sz_nonzero.
-
-Ltac pose_s_nonzero s s_nonzero :=
- cache_proof_with_type_by
- (s <> 0)
- ltac:(vm_decide_no_check)
- s_nonzero.
+ Local Notation wt := (wt_gen m sz).
-Ltac pose_sz_le_log2_m sz m sz_le_log2_m :=
- cache_proof_with_type_by
- (Z.of_nat sz <= Z.log2_up (Z.pos m))
- ltac:(vm_decide_no_check)
- sz_le_log2_m.
+ Definition sz2' := ((sz * 2) - 1)%nat.
-Ltac pose_m_correct m s c m_correct :=
- cache_proof_with_type_by
- (Z.pos m = s - Associational.eval c)
- ltac:(vm_decide_no_check)
- m_correct.
+ Definition half_sz' := (sz / 2)%nat.
-Ltac pose_m_enc sz s c wt m_enc :=
- let v := (eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c))) in
- let v := (eval compute in v) in (* compute away the type arguments *)
- cache_term v m_enc.
-Ltac pose_coef sz wt m_enc coef_div_modulus coef := (* subtraction coefficient *)
- let v := (eval vm_compute in
- ((fix addm (acc: Z^sz) (ctr : nat) : Z^sz :=
- match ctr with
- | O => acc
- | S n => addm (Positional.add_cps wt acc m_enc id) n
- end) (Positional.zeros sz) coef_div_modulus)) in
- cache_term v coef.
+ Definition m_enc'
+ := Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m).
-Ltac pose_coef_mod sz wt m coef coef_mod :=
- cache_term_with_type_by
- (mod_eq m (Positional.eval (n:=sz) wt coef) 0)
- ltac:(exact eq_refl)
- coef_mod.
-Ltac pose_sz_nonzero sz sz_nonzero :=
- cache_proof_with_type_by
- (sz <> 0%nat)
- ltac:(vm_decide_no_check)
- sz_nonzero.
-Section wt_gen.
- Context (m : positive) (sz : nat).
- Local Notation wt := (wt_gen m sz).
Local Ltac Q_cbv :=
cbv [wt_gen Qround.Qceiling QArith_base.Qmult QArith_base.Qdiv QArith_base.inject_Z QArith_base.Qden QArith_base.Qnum QArith_base.Qopp Qround.Qfloor QArith_base.Qinv QArith_base.Qle Z.of_nat].
Lemma wt_gen0_1 : wt 0 = 1.
@@ -169,8 +123,95 @@ Section wt_gen.
constructor; eauto using wt_gen_divides_chain.
Qed.
End divides.
-End wt_gen.
+ Definition coef'
+ := (fix addm (acc: Z^sz) (ctr : nat) : Z^sz :=
+ match ctr with
+ | O => acc
+ | S n => addm (Positional.add_cps wt acc m_enc' id) n
+ end) (Positional.zeros sz) coef_div_modulus.
+
+ Lemma coef_mod'
+ (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m))
+ : mod_eq m (Positional.eval (n:=sz) wt coef') 0.
+ Proof.
+ cbv [coef' m_enc'].
+ remember (Positional.zeros sz) as v eqn:Hv.
+ assert (Hv' : mod_eq m (Positional.eval wt v) 0)
+ by (subst v; autorewrite with push_basesystem_eval; reflexivity);
+ clear Hv.
+ revert dependent v.
+ induction coef_div_modulus as [|n IHn]; clear coef_div_modulus;
+ intros; [ assumption | ].
+ rewrite IHn; [ reflexivity | ].
+ pose proof wt_gen0_1.
+ pose proof wt_gen_nonzero.
+ pose proof div_mod.
+ pose proof wt_gen_divides'.
+ destruct (Nat.eq_dec sz 0).
+ { subst; reflexivity. }
+ { repeat autounfold; autorewrite with uncps push_id push_basesystem_eval.
+ rewrite Positional.eval_encode by auto.
+ cbv [mod_eq] in *.
+ push_Zmod; rewrite Hv'; pull_Zmod.
+ reflexivity. }
+ Qed.
+End gen.
+
+Ltac pose_wt m sz wt :=
+ let v := (eval cbv [wt_gen] in (wt_gen m sz)) in
+ cache_term v wt.
+
+Ltac pose_sz2 sz sz2 :=
+ let v := (eval vm_compute in (sz2' sz)) in
+ cache_term v sz2.
+
+Ltac pose_half_sz sz half_sz :=
+ let v := (eval compute in (half_sz' sz)) in
+ cache_term v half_sz.
+
+Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
+ cache_proof_with_type_by
+ (half_sz <> 0%nat)
+ ltac:(cbv; congruence)
+ half_sz_nonzero.
+
+Ltac pose_s_nonzero s s_nonzero :=
+ cache_proof_with_type_by
+ (s <> 0)
+ ltac:(vm_decide_no_check)
+ s_nonzero.
+
+Ltac pose_sz_le_log2_m sz m sz_le_log2_m :=
+ cache_proof_with_type_by
+ (Z.of_nat sz <= Z.log2_up (Z.pos m))
+ ltac:(vm_decide_no_check)
+ sz_le_log2_m.
+
+Ltac pose_m_correct m s c m_correct :=
+ cache_proof_with_type_by
+ (Z.pos m = s - Associational.eval c)
+ ltac:(vm_decide_no_check)
+ m_correct.
+
+Ltac pose_m_enc sz m m_enc :=
+ let v := (eval vm_compute in (m_enc' m sz)) in
+ let v := (eval compute in v) in (* compute away the type arguments *)
+ cache_term v m_enc.
+Ltac pose_coef sz m coef_div_modulus coef := (* subtraction coefficient *)
+ let v := (eval vm_compute in (coef' m sz coef_div_modulus)) in
+ cache_term v coef.
+
+Ltac pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod :=
+ cache_proof_with_type_by
+ (mod_eq m (Positional.eval (n:=sz) wt coef) 0)
+ ltac:(vm_cast_no_check (coef_mod' m sz coef_div_modulus sz_le_log2_m))
+ coef_mod.
+Ltac pose_sz_nonzero sz sz_nonzero :=
+ cache_proof_with_type_by
+ (sz <> 0%nat)
+ ltac:(vm_decide_no_check)
+ sz_nonzero.
Ltac pose_wt_nonzero wt wt_nonzero :=
cache_proof_with_type_by
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index 791762975..ea53542a1 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
@@ -69,20 +69,17 @@ Ltac add_m_correct pkg :=
Ltac add_m_enc pkg :=
let sz := Tag.get pkg TAG.sz in
- let s := Tag.get pkg TAG.s in
- let c := Tag.get pkg TAG.c in
- let wt := Tag.get pkg TAG.wt in
+ let m := Tag.get pkg TAG.m in
let m_enc := fresh "m_enc" in
- let m_enc := pose_m_enc sz s c wt m_enc in
+ let m_enc := pose_m_enc sz m m_enc in
Tag.update pkg TAG.m_enc m_enc.
Ltac add_coef pkg :=
let sz := Tag.get pkg TAG.sz in
- let wt := Tag.get pkg TAG.wt in
- let m_enc := Tag.get pkg TAG.m_enc in
+ let m := Tag.get pkg TAG.m in
let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
let coef := fresh "coef" in
- let coef := pose_coef sz wt m_enc coef_div_modulus coef in
+ let coef := pose_coef sz m coef_div_modulus coef in
Tag.update pkg TAG.coef coef.
Ltac add_coef_mod pkg :=
@@ -90,8 +87,10 @@ Ltac add_coef_mod pkg :=
let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let coef := Tag.get pkg TAG.coef in
+ let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
+ let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in
let coef_mod := fresh "coef_mod" in
- let coef_mod := pose_coef_mod sz wt m coef coef_mod in
+ let coef_mod := pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod in
Tag.update pkg TAG.coef_mod coef_mod.
Ltac add_sz_nonzero pkg :=
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v
index 89884fec6..472349180 100644
--- a/src/Specific/Framework/CurveParameters.v
+++ b/src/Specific/Framework/CurveParameters.v
@@ -11,7 +11,7 @@ Local Set Primitive Projections.
Module Export Notations := RawCurveParameters.Notations.
Module TAG. (* namespacing *)
- Inductive tags := CP | sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel.
+ Inductive tags := CP | sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code.
End TAG.
Module Export CurveParameters.
@@ -220,6 +220,10 @@ Module Export CurveParameters.
internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent upper_bound_of_exponent.
Ltac pose_modinv_fuel CP modinv_fuel :=
internal_pose_of_CP CP CurveParameters.modinv_fuel modinv_fuel.
+ Ltac pose_mul_code CP mul_code :=
+ internal_pose_of_CP CP CurveParameters.mul_code mul_code.
+ Ltac pose_square_code CP square_code :=
+ internal_pose_of_CP CP CurveParameters.square_code square_code.
(* Everything below this line autogenerated by remake_packages.py *)
Ltac add_sz pkg :=
@@ -300,6 +304,18 @@ Module Export CurveParameters.
let modinv_fuel := pose_modinv_fuel CP modinv_fuel in
Tag.update pkg TAG.modinv_fuel modinv_fuel.
+ Ltac add_mul_code pkg :=
+ let CP := Tag.get pkg TAG.CP in
+ let mul_code := fresh "mul_code" in
+ let mul_code := pose_mul_code CP mul_code in
+ Tag.update pkg TAG.mul_code mul_code.
+
+ Ltac add_square_code pkg :=
+ let CP := Tag.get pkg TAG.CP in
+ let square_code := fresh "square_code" in
+ let square_code := pose_square_code CP square_code in
+ Tag.update pkg TAG.square_code square_code.
+
Ltac add_CurveParameters_package pkg :=
let pkg := add_sz pkg in
let pkg := add_bitwidth pkg in
@@ -314,5 +330,7 @@ Module Export CurveParameters.
let pkg := add_freeze_allowable_bit_widths pkg in
let pkg := add_upper_bound_of_exponent pkg in
let pkg := add_modinv_fuel pkg in
+ let pkg := add_mul_code pkg in
+ let pkg := add_square_code pkg in
Tag.strip_local pkg.
End CurveParameters.
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
index 10b72f2ba..75ef1f7e7 100644
--- a/src/Specific/Framework/CurveParametersPackage.v
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -49,4 +49,8 @@ Module MakeCurveParametersPackage (PKG : PrePackage).
Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing).
Ltac get_modinv_fuel _ := get TAG.modinv_fuel.
Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing).
+ Ltac get_mul_code _ := get TAG.mul_code.
+ Notation mul_code := (ltac:(let v := get_mul_code () in exact v)) (only parsing).
+ Ltac get_square_code _ := get TAG.square_code.
+ Notation square_code := (ltac:(let v := get_square_code () in exact v)) (only parsing).
End MakeCurveParametersPackage.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 14:12:16 +0000