aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-05 18:03:07 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-10-18 23:01:29 -0400
commit6983ac1dce0411657dda4be7f49a0899e8a2b326 (patch)
tree32eae1977cfb74572a1f72f4ef5d4d3dac69d361
parent239356d3a22af3b065dfae10bd6d84dd509251e8 (diff)
Factor out specific code underlying ReificationTypes
After | File Name | Before || Change ------------------------------------------------------------------------------ 4m29.48s | Total | 4m30.12s || -0m00.63s ------------------------------------------------------------------------------ 0m27.97s | Specific/X25519/C32/fesquare | 0m26.68s || +0m01.28s 0m00.73s | Specific/X25519/C32/ReificationTypes | 0m02.43s || -0m01.70s 1m54.60s | Specific/X25519/C64/ladderstep | 1m55.11s || -0m00.51s 0m52.88s | Specific/X25519/C32/femul | 0m53.07s || -0m00.18s 0m29.56s | Specific/X25519/C32/ArithmeticSynthesisTest | 0m29.57s || -0m00.01s 0m10.01s | Specific/X25519/C64/femul | 0m10.08s || -0m00.07s 0m08.84s | Specific/IntegrationTestSub | 0m08.39s || +0m00.44s 0m08.42s | Specific/X25519/C64/ArithmeticSynthesisTest | 0m08.17s || +0m00.25s 0m07.64s | Specific/IntegrationTestFreeze | 0m08.01s || -0m00.37s 0m07.23s | Specific/X25519/C64/fesquare | 0m07.31s || -0m00.07s 0m00.86s | Specific/ReificationTypes | N/A || +0m00.86s 0m00.74s | Specific/X25519/C64/ReificationTypes | 0m01.30s || -0m00.56s
-rw-r--r--_CoqProject1
-rw-r--r--src/Specific/ReificationTypes.v201
-rw-r--r--src/Specific/X25519/C32/ArithmeticSynthesisTest.v2
-rw-r--r--src/Specific/X25519/C32/ReificationTypes.v62
-rw-r--r--src/Specific/X25519/C64/ArithmeticSynthesisTest.v2
-rw-r--r--src/Specific/X25519/C64/ReificationTypes.v62
-rw-r--r--src/Specific/X25519/C64/ladderstepDisplay.log4
7 files changed, 224 insertions, 110 deletions
diff --git a/_CoqProject b/_CoqProject
index 54615d4e6..3f2d895f5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -253,6 +253,7 @@ src/Specific/IntegrationTestSubDisplay.v
src/Specific/IntegrationTestTemporaryMiscCommon.v
src/Specific/Karatsuba.v
src/Specific/MontgomeryP256_128.v
+src/Specific/ReificationTypes.v
src/Specific/NISTP256/AMD64/MontgomeryP256.v
src/Specific/NISTP256/AMD64/feadd.v
src/Specific/NISTP256/AMD64/feaddDisplay.v
diff --git a/src/Specific/ReificationTypes.v b/src/Specific/ReificationTypes.v
new file mode 100644
index 000000000..cc705689b
--- /dev/null
+++ b/src/Specific/ReificationTypes.v
@@ -0,0 +1,201 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.romega.ROmega.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Decidable.
+
+Require Import Crypto.Util.Tactics.PoseTermWithName.
+Require Import Crypto.Util.Tactics.CacheTerm.
+
+Ltac pose_limb_widths wt sz limb_widths :=
+ pose_term_with
+ ltac:(fun _ => (eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz))))
+ limb_widths.
+
+Ltac get_b_of upper_bound_of_exponent :=
+ constr:(fun exp => {| lower := 0 ; upper := upper_bound_of_exponent exp |}%Z). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
+
+(* The definition [bounds_exp] is a tuple-version of the limb-widths,
+ which are the [exp] argument in [b_of] above, i.e., the approximate
+ base-2 exponent of the bounds on the limb in that position. *)
+Ltac pose_bounds_exp sz limb_widths bounds_exp :=
+ pose_term_with_type
+ (Tuple.tuple Z sz)
+ ltac:(fun _ => eval compute in
+ (Tuple.from_list sz limb_widths eq_refl))
+ bounds_exp.
+
+Ltac pose_bounds sz b_of bounds_exp bounds :=
+ pose_term_with_type
+ (Tuple.tuple zrange sz)
+ ltac:(fun _ => eval compute in
+ (Tuple.map (fun e => b_of e) bounds_exp))
+ bounds.
+
+Ltac pose_lgbitwidth limb_widths lgbitwidth :=
+ pose_term_with
+ ltac:(fun _ => eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))))
+ lgbitwidth.
+
+Ltac pose_bitwidth lgbitwidth bitwidth :=
+ pose_term_with
+ ltac:(fun _ => eval compute in (2^lgbitwidth)%nat)
+ bitwidth.
+
+Ltac pose_feZ sz feZ :=
+ pose_term_with
+ ltac:(fun _ => constr:(tuple Z sz))
+ feZ.
+
+Ltac pose_feW sz lgbitwidth feW :=
+ cache_term_with_type_by
+ Type
+ ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v)
+ feW.
+Ltac pose_feW_bounded feW bounds feW_bounded :=
+ cache_term_with_type_by
+ (feW -> Prop)
+ ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v)
+ feW_bounded.
+Ltac pose_feBW sz bitwidth bounds feBW :=
+ cache_term_with_type_by
+ Type
+ ltac:(let v := eval cbv [bitwidth bounds] in (BoundedWord sz bitwidth bounds) in exact v)
+ feBW.
+
+Lemma feBW_bounded_helper'
+ sz bitwidth bounds
+ (feBW := BoundedWord sz bitwidth bounds)
+ (wt : nat -> Z)
+ (Hwt : forall i, 0 <= wt i)
+ : forall (a : feBW),
+ B.Positional.eval wt (map lower bounds)
+ <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a)
+ <= B.Positional.eval wt (map upper bounds).
+Proof.
+ let a := fresh "a" in
+ intro a;
+ destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
+ destruct sz as [|sz].
+ { cbv -[Z.le Z.lt Z.mul]; lia. }
+ { cbn [tuple map] in *.
+ revert dependent wt; induction sz as [|sz IHsz]; intros.
+ { cbv -[Z.le Z.lt wordToZ Z.mul Z.pow Z.add lower upper Nat.log2 wordT] in *.
+ repeat match goal with
+ | [ |- context[@wordToZ ?n ?x] ]
+ => generalize dependent (@wordToZ n x); intros
+ | [ H : forall j, 0 <= wt j |- context[wt ?i] ]
+ => pose proof (H i); generalize dependent (wt i); intros
+ end.
+ nia. }
+ { pose proof (Hwt 0%nat).
+ cbn [tuple' map'] in *.
+ destruct a as [a' a], bounds as [bounds b], H as [H [H' _]].
+ cbn [fst snd] in *.
+ setoid_rewrite (@B.Positional.eval_step (S _)).
+ specialize (IHsz bounds a' H (fun i => wt (S i)) (fun i => Hwt _)).
+ nia. } }
+Qed.
+Lemma feBW_bounded_helper
+ sz bitwidth bounds
+ (feBW := BoundedWord sz bitwidth bounds)
+ (wt : nat -> Z)
+ (Hwt : forall i, 0 <= wt i)
+ l u
+ : l <= B.Positional.eval wt (map lower bounds)
+ /\ B.Positional.eval wt (map upper bounds) < u
+ -> forall (a : feBW),
+ l <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < u.
+Proof.
+ intros [Hl Hu] a; split;
+ [ eapply Z.le_trans | eapply Z.le_lt_trans ];
+ [ | eapply feBW_bounded_helper' | eapply feBW_bounded_helper' | ];
+ assumption.
+Qed.
+
+Ltac pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded :=
+ cache_proof_with_type_by
+ (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m)
+ ltac:(apply (@feBW_bounded_helper sz bitwidth bounds wt wt_nonneg);
+ vm_compute; clear; split; congruence)
+ feBW_bounded.
+
+Ltac pose_phiW feW m wt phiW :=
+ cache_term_with_type_by
+ (feW -> F m)
+ ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x)))
+ phiW.
+Ltac pose_phiBW feBW m wt phiBW :=
+ cache_term_with_type_by
+ (feBW -> F m)
+ ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x)))
+ phiBW.
+
+Ltac get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent :=
+ let limb_widths := fresh "limb_widths" in
+ let bounds_exp := fresh "bounds_exp" in
+ let bounds := fresh "bounds" in
+ let lgbitwidth := fresh "lgbitwidth" in
+ let bitwidth := fresh "bitwidth" in
+ let feZ := fresh "feZ" in
+ let feW := fresh "feW" in
+ let feW_bounded := fresh "feW_bounded" in
+ let feBW := fresh "feBW" in
+ let feBW_bounded := fresh "feBW_bounded" in
+ let phiW := fresh "phiW" in
+ let phiBW := fresh "phiBW" in
+ let limb_widths := pose_limb_widths wt sz limb_widths in
+ let b_of := get_b_of upper_bound_of_exponent in
+ let bounds_exp := pose_bounds_exp sz limb_widths bounds_exp in
+ let bounds := pose_bounds sz b_of bounds_exp bounds in
+ let lgbitwidth := pose_lgbitwidth limb_widths lgbitwidth in
+ let bitwidth := pose_bitwidth lgbitwidth bitwidth in
+ let feZ := pose_feZ sz feZ in
+ let feW := pose_feW sz lgbitwidth feW in
+ let feW_bounded := pose_feW_bounded feW bounds feW_bounded in
+ let feBW := pose_feBW sz bitwidth bounds feBW in
+ let feBW_bounded := pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded in
+ let phiW := pose_phiW feW m wt phiW in
+ let phiBW := pose_phiBW feBW m wt phiBW in
+ constr:((feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW)).
+Ltac make_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent :=
+ lazymatch goal with
+ | [ |- { T : _ & T } ] => eexists
+ | [ |- _ ] => idtac
+ end;
+ let pkg := get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent in
+ exact pkg.
+
+Module Type ReificationTypesPrePackage.
+ Parameter ReificationTypes_package' : { T : _ & T }.
+ Parameter ReificationTypes_package : projT1 ReificationTypes_package'.
+End ReificationTypesPrePackage.
+
+Module MakeReificationTypes (RP : ReificationTypesPrePackage).
+ Definition ReificationTypes_package := RP.ReificationTypes_package.
+ Ltac reduce_proj x :=
+ let RP_ReificationTypes_package := (eval cbv [ReificationTypes_package] in ReificationTypes_package) in
+ let v := (eval cbv [ReificationTypes_package RP_ReificationTypes_package] in x) in
+ exact v.
+ (**
+<<
+terms = 'feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW'
+for i in terms.split(', '):
+ print(" Notation %s := (ltac:(reduce_proj (let '(%s) := ReificationTypes_package in %s))) (only parsing)." % (i, terms, i))
+>> *)
+ Notation feZ := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feZ))) (only parsing).
+ Notation feW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW))) (only parsing).
+ Notation feW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW_bounded))) (only parsing).
+ Notation feBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW))) (only parsing).
+ Notation feBW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW_bounded))) (only parsing).
+ Notation phiW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiW))) (only parsing).
+ Notation phiBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiBW))) (only parsing).
+End MakeReificationTypes.
diff --git a/src/Specific/X25519/C32/ArithmeticSynthesisTest.v b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
index 6b1d5ee11..c961afd69 100644
--- a/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
+++ b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
@@ -52,6 +52,8 @@ Section Ops.
Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
Lemma wt_nonzero i : wt i <> 0.
Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+ Lemma wt_nonneg i : 0 <= wt i.
+ Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed.
Lemma wt_divides i : wt (S i) / wt i > 0.
Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
Lemma wt_divides' i : wt (S i) / wt i <> 0.
diff --git a/src/Specific/X25519/C32/ReificationTypes.v b/src/Specific/X25519/C32/ReificationTypes.v
index 6b2a47070..c5a9e0fd3 100644
--- a/src/Specific/X25519/C32/ReificationTypes.v
+++ b/src/Specific/X25519/C32/ReificationTypes.v
@@ -1,58 +1,12 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.romega.ROmega.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Specific.ReificationTypes.
Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest.
-Section BoundedField.
- Local Coercion Z.of_nat : nat >-> Z.
-
- Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-
- Local Notation b_of exp := {| lower := 0 ; upper := P.upper_bound_of_exponent exp |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
- (* The definition [bounds_exp] is a tuple-version of the
- limb-widths, which are the [exp] argument in [b_of] above, i.e.,
- the approximate base-2 exponent of the bounds on the limb in that
- position. *)
- Let bounds_exp : Tuple.tuple Z sz
- := Eval compute in
- Tuple.from_list sz limb_widths eq_refl.
- Let bounds : Tuple.tuple zrange sz
- := Eval compute in
- Tuple.map (fun e => b_of e) bounds_exp.
-
- Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
- Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
- Let feZ : Type := tuple Z sz.
- Definition feW : Type := Eval cbv [lgbitwidth] in tuple (wordT lgbitwidth) sz.
- Definition feW_bounded : feW -> Prop
- := Eval cbv [bounds] in fun w => is_bounded_by None bounds (map wordToZ w).
- Definition feBW : Type := Eval cbv [bitwidth bounds] in BoundedWord sz bitwidth bounds.
+Module RP <: ReificationTypesPrePackage.
+ Definition ReificationTypes_package' : { T : _ & T }.
+ Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined.
- Lemma feBW_bounded (a : feBW)
- : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
- Proof.
- destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
- destruct_head_hnf' and.
- cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt] in *; cbn [fst snd] in *.
- repeat match goal with
- | [ |- context[@wordToZ ?n ?x] ]
- => generalize dependent (@wordToZ n x); intros
- | [ |- context[wt ?n] ]
- => let v := (eval compute in (wt n)) in change (wt n) with v
- end.
- romega.
- Qed.
+ Definition ReificationTypes_package
+ := Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'.
+End RP.
- Definition phiW : feW -> F m :=
- fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
- Definition phiBW : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-End BoundedField.
+Module Export ReificationTypes := MakeReificationTypes RP.
diff --git a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
index f4ef43f20..6994e13be 100644
--- a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
+++ b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
@@ -52,6 +52,8 @@ Section Ops.
Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
Lemma wt_nonzero i : wt i <> 0.
Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+ Lemma wt_nonneg i : 0 <= wt i.
+ Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed.
Lemma wt_divides i : wt (S i) / wt i > 0.
Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
Lemma wt_divides' i : wt (S i) / wt i <> 0.
diff --git a/src/Specific/X25519/C64/ReificationTypes.v b/src/Specific/X25519/C64/ReificationTypes.v
index 009145467..0e999b2fc 100644
--- a/src/Specific/X25519/C64/ReificationTypes.v
+++ b/src/Specific/X25519/C64/ReificationTypes.v
@@ -1,58 +1,12 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.romega.ROmega.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Specific.ReificationTypes.
Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
-Section BoundedField.
- Local Coercion Z.of_nat : nat >-> Z.
-
- Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
-
- Local Notation b_of exp := {| lower := 0 ; upper := P.upper_bound_of_exponent exp |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
- (* The definition [bounds_exp] is a tuple-version of the
- limb-widths, which are the [exp] argument in [b_of] above, i.e.,
- the approximate base-2 exponent of the bounds on the limb in that
- position. *)
- Let bounds_exp : Tuple.tuple Z sz
- := Eval compute in
- Tuple.from_list sz limb_widths eq_refl.
- Let bounds : Tuple.tuple zrange sz
- := Eval compute in
- Tuple.map (fun e => b_of e) bounds_exp.
-
- Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
- Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
- Let feZ : Type := tuple Z sz.
- Definition feW : Type := Eval cbv [lgbitwidth] in tuple (wordT lgbitwidth) sz.
- Definition feW_bounded : feW -> Prop
- := Eval cbv [bounds] in fun w => is_bounded_by None bounds (map wordToZ w).
- Definition feBW : Type := Eval cbv [bitwidth bounds] in BoundedWord sz bitwidth bounds.
+Module RP <: ReificationTypesPrePackage.
+ Definition ReificationTypes_package' : { T : _ & T }.
+ Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined.
- Lemma feBW_bounded (a : feBW)
- : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
- Proof.
- destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
- destruct_head_hnf' and.
- cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt] in *; cbn [fst snd] in *.
- repeat match goal with
- | [ |- context[@wordToZ ?n ?x] ]
- => generalize dependent (@wordToZ n x); intros
- | [ |- context[wt ?n] ]
- => let v := (eval compute in (wt n)) in change (wt n) with v
- end.
- romega.
- Qed.
+ Definition ReificationTypes_package
+ := Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'.
+End RP.
- Definition phiW : feW -> F m :=
- fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
- Definition phiBW : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-End BoundedField.
+Module Export ReificationTypes := MakeReificationTypes RP.
diff --git a/src/Specific/X25519/C64/ladderstepDisplay.log b/src/Specific/X25519/C64/ladderstepDisplay.log
index ca8ba4396..4e22b729f 100644
--- a/src/Specific/X25519/C64/ladderstepDisplay.log
+++ b/src/Specific/X25519/C64/ladderstepDisplay.log
@@ -1,4 +1,4 @@
-λ x x0 x1 x2 x3 : ReificationTypes.feW,
+λ x x0 x1 x2 x3 : ReificationTypes.RP.feW,
let (a, b) := Interp-η
(λ var : Syntax.base_type → Type,
λ '(x15, x16, x14, x12, x10, (x25, x26, x24, x22, x20, (x33, x34, x32, x30, x28)), (x43, x44, x42, x40, x38, (x51, x52, x50, x48, x46)))%core,
@@ -367,4 +367,4 @@ let (a, b) := Interp-η
(let (a0, b0) := a in
(a0, b0), let (a0, b0) := b in
(a0, b0))%core
- : ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW * ReificationTypes.feW * (ReificationTypes.feW * ReificationTypes.feW)
+ : ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW * ReificationTypes.RP.feW * (ReificationTypes.RP.feW * ReificationTypes.RP.feW)