From 970f0d7ee4d73cb4950fe7646dfe9cebc0789bf0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 9 Nov 2016 14:20:09 -0500 Subject: Split up GF25519Reflective.Common: faster+parallel After | File Name | Before || Change -------------------------------------------------------------------------------- 2m53.12s | Total | 2m52.26s || +0m00.85s -------------------------------------------------------------------------------- 0m01.38s | Specific/GF25519Reflective/Common | 0m43.51s || -0m42.12s 0m14.82s | Specific/GF25519Reflective/CommonBinOp | N/A || +0m14.82s 0m10.91s | Specific/GF25519Reflective/CommonUnOp | N/A || +0m10.91s 0m10.44s | Specific/GF25519Reflective/CommonUnOpWireToFE | N/A || +0m10.43s 0m06.42s | Specific/GF25519Reflective/CommonUnOpFEToWire | N/A || +0m06.41s 1m18.24s | Experiments/Ed25519 | 1m18.57s || -0m00.32s 0m07.97s | Specific/GF25519Reflective/Reified/Mul | 0m08.45s || -0m00.47s 0m07.89s | Specific/GF25519Reflective/Reified/Freeze | 0m07.84s || +0m00.04s 0m06.87s | Specific/GF25519Reflective | 0m06.92s || -0m00.04s 0m03.53s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.63s || -0m00.10s 0m03.27s | Specific/GF25519Reflective/Reified/CarryAdd | 0m03.28s || -0m00.00s 0m03.18s | Specific/GF25519Reflective/Reified/CarryOpp | 0m03.15s || +0m00.03s 0m02.24s | Specific/GF25519Reflective/Reified/Unpack | 0m02.21s || +0m00.03s 0m02.19s | Specific/GF25519Reflective/Reified/Pack | 0m02.28s || -0m00.08s 0m02.16s | Specific/GF25519Reflective/Reified/Sub | 0m02.15s || +0m00.01s 0m02.14s | Specific/GF25519Bounded | 0m02.07s || +0m00.07s 0m02.07s | Experiments/Ed25519Extraction | 0m02.16s || -0m00.09s 0m01.99s | Specific/GF25519Reflective/Reified/Add | 0m01.81s || +0m00.17s 0m01.82s | Specific/GF25519Reflective/Reified/Opp | 0m01.78s || +0m00.04s 0m01.76s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.71s || +0m00.05s 0m00.97s | Specific/GF25519Reflective/CommonUnOpFEToZ | N/A || +0m00.97s 0m00.86s | Specific/GF25519Reflective/Reified | 0m00.75s || +0m00.10s --- src/Specific/GF25519Reflective/Common.v | 344 +++++++-------------- src/Specific/GF25519Reflective/CommonBinOp.v | 50 +++ src/Specific/GF25519Reflective/CommonUnOp.v | 44 +++ .../GF25519Reflective/CommonUnOpFEToWire.v | 44 +++ src/Specific/GF25519Reflective/CommonUnOpFEToZ.v | 44 +++ .../GF25519Reflective/CommonUnOpWireToFE.v | 44 +++ src/Specific/GF25519Reflective/Reified/Add.v | 2 +- src/Specific/GF25519Reflective/Reified/CarryAdd.v | 2 +- src/Specific/GF25519Reflective/Reified/CarryOpp.v | 2 +- src/Specific/GF25519Reflective/Reified/CarrySub.v | 2 +- src/Specific/GF25519Reflective/Reified/Freeze.v | 2 +- src/Specific/GF25519Reflective/Reified/GeModulus.v | 2 +- src/Specific/GF25519Reflective/Reified/Mul.v | 2 +- src/Specific/GF25519Reflective/Reified/Opp.v | 2 +- src/Specific/GF25519Reflective/Reified/Pack.v | 2 +- src/Specific/GF25519Reflective/Reified/Sub.v | 2 +- src/Specific/GF25519Reflective/Reified/Unpack.v | 2 +- .../GF25519Reflective/Reified/rebuild-reified.py | 2 +- 18 files changed, 348 insertions(+), 246 deletions(-) create mode 100644 src/Specific/GF25519Reflective/CommonBinOp.v create mode 100644 src/Specific/GF25519Reflective/CommonUnOp.v create mode 100644 src/Specific/GF25519Reflective/CommonUnOpFEToWire.v create mode 100644 src/Specific/GF25519Reflective/CommonUnOpFEToZ.v create mode 100644 src/Specific/GF25519Reflective/CommonUnOpWireToFE.v (limited to 'src') diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 80932d4df..71267e96a 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -126,48 +126,7 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW)) (only parsing). -Local Ltac args_to_bounded_helper v := - lazymatch v with - | (?x, ?xs) - => args_to_bounded_helper x; [ .. | args_to_bounded_helper xs ] - | ?w - => try refine (_, _); [ refine {| BoundedWord64.value := w |} | .. ] - end. - -Local Ltac make_args x := - let x' := fresh "x'" in - pose (x : id _) as x'; - cbv [fe25519W wire_digitsW] in x; destruct_head' prod; - cbv [fst snd] in *; - simpl @fe25519WToZ in *; - simpl @wire_digitsWToZ in *; - let T := fresh in - evar (T : Type); - cut T; subst T; - [ let H := fresh in - intro H; - let xv := (eval hnf in x') in - args_to_bounded_helper xv; - [ instantiate; - destruct_head' and; - match goal with - | [ H : ?T |- _ ] - => is_evar T; - refine (let c := proj1 H in _); (* work around broken evars in Coq 8.4 *) - lazymatch goal with H := proj1 _ |- _ => refine H end - end.. ] - | instantiate; - repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end; - repeat match goal with H : wire_digits_is_bounded _ = true |- _ => unfold_is_bounded_in H end; - destruct_head' and; - Z.ltb_to_lt; - repeat first [ eexact I - | apply conj; - [ repeat apply conj; [ | eassumption | eassumption | ]; - instantiate; vm_compute; [ refine (fun x => match x with eq_refl => I end) | reflexivity ] - | ] ] ]. - -Local Ltac app_tuples x y := +Ltac app_tuples x y := let tx := type of x in lazymatch (eval hnf in tx) with | prod _ _ => let xs := app_tuples (snd x) y in @@ -175,15 +134,119 @@ Local Ltac app_tuples x y := | _ => constr:((x, y)) end. -Class is_evar {T} (x : T) := make_is_evar : True. -Hint Extern 0 (is_evar ?e) => is_evar e; exact I : typeclass_instances. +Local Arguments Tuple.map2 : simpl never. +Local Arguments Tuple.map : simpl never. + +Fixpoint args_to_bounded_helperT {n} + (v : Tuple.tuple' Word64.word64 n) + (bounds : Tuple.tuple' (Z * Z) n) + (pf : List.fold_right + andb true + (Tuple.to_list + _ + (Tuple.map2 + (n:=S n) + (fun bounds v => + let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool) + bounds + (Tuple.map (n:=S n) Word64.word64ToZ v))) = true) + (res : Type) + {struct n} + : Type. +Proof. + refine (match n return (forall (v : Tuple.tuple' _ n) (bounds : Tuple.tuple' _ n), + List.fold_right + _ _ (Tuple.to_list + _ + (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true + -> Type) + with + | 0 => fun v bounds pf0 => forall pf1 : (0 <= fst bounds /\ Z.log2 (snd bounds) < Z.of_nat Word64.bit_width)%Z, res + | S n' => fun v bounds pf0 => forall pf1 : (0 <= fst (snd bounds) /\ Z.log2 (snd (snd bounds)) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v) (fst bounds) _ res + end v bounds pf). + { clear -pf0. + abstract ( + destruct v, bounds; simpl @fst; + rewrite Tuple.map_S in pf0; + simpl in pf0; + rewrite Tuple.map2_S in pf0; + simpl @List.fold_right in *; + rewrite Bool.andb_true_iff in pf0; tauto + ). } +Defined. + +Fixpoint args_to_bounded_helper {n} res + {struct n} + : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res. +Proof. + refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with + | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |} + | S n' + => fun v bounds pf f pf' + => @args_to_bounded_helper + n' res (fst v) (fst bounds) _ + (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |})) + end. + { clear -pf pf'. + unfold Tuple.map2, Tuple.map in pf; simpl in *. + abstract ( + destruct bounds; + simpl in *; + rewrite !Bool.andb_true_iff in pf; + destruct_head' and; + Z.ltb_to_lt; auto + ). } + { simpl in *. + clear -pf pf'. + abstract ( + destruct bounds as [? [? ?] ], v; simpl in *; + rewrite Tuple.map_S in pf; simpl in pf; rewrite Tuple.map2_S in pf; + simpl in pf; + rewrite !Bool.andb_true_iff in pf; + destruct_head' and; + Z.ltb_to_lt; auto + ). } +Defined. + +Definition assoc_right'' + := Eval cbv [Tuple.assoc_right' Tuple.rsnoc' fst snd] in @Tuple.assoc_right'. + +Definition args_to_bounded {n} v bounds pf + := Eval cbv [args_to_bounded_helper assoc_right''] in + @args_to_bounded_helper n _ v bounds pf (@assoc_right'' _ _). + +Local Ltac get_len T := + match (eval hnf in T) with + | prod ?A ?B + => let a := get_len A in + let b := get_len B in + (eval compute in (a + b)%nat) + | _ => constr:(1%nat) + end. + +Local Ltac args_to_bounded x H := + let x' := fresh in + set (x' := x); + compute in x; + let len := (let T := type of x in get_len T) in + destruct_head' prod; + let c := constr:(args_to_bounded (n:=pred len) x' _ H) in + let bounds := lazymatch c with args_to_bounded _ ?bounds _ => bounds end in + let c := (eval cbv [all_binders_for ExprUnOpT interp_flat_type args_to_bounded bounds pred fst snd] in c) in + apply c; compute; clear; + try abstract ( + repeat split; + solve [ reflexivity + | refine (fun v => match v with eq_refl => I end) ] + ). Definition unop_args_to_bounded (x : fe25519W) (H : is_bounded (fe25519WToZ x) = true) : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT). -Proof. make_args x. Defined. +Proof. args_to_bounded x H. Defined. + Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true) : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET). -Proof. make_args x. Defined. +Proof. args_to_bounded x H. Defined. Definition binop_args_to_bounded (x : fe25519W * fe25519W) (H : is_bounded (fe25519WToZ (fst x)) = true) (H' : is_bounded (fe25519WToZ (snd x)) = true) @@ -225,7 +288,6 @@ Local Ltac make_bounds_prop bounds orig_bounds := | None => false end). - Definition unop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpT)) : bool. Proof. make_bounds_prop bounds ExprUnOp_bounds. Defined. Definition binop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprBinOpT)) : bool. @@ -244,7 +306,7 @@ Defined. various kinds of correct and boundedness, and abstract in Gallina rather than Ltac *) -Local Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := +Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Heq := fresh "Heq" in let Hbounds0 := fresh "Hbounds0" in let Hbounds1 := fresh "Hbounds1" in @@ -311,192 +373,6 @@ Local Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := change Word64.word64ToZ with word64ToZ in *; repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity. -Local Opaque Interp. -Lemma ExprBinOp_correct_and_bounded - ropW op (ropZ_sig : rexpr_binop_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall xy - (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) - (Hxy : is_bounded (fe25519WToZ (fst xy)) = true - /\ is_bounded (fe25519WToZ (snd xy)) = true), - let Hx := let (Hx, Hy) := Hxy in Hx in - let Hy := let (Hx, Hy) := Hxy in Hy in - let args := binop_args_to_bounded xy Hx Hy in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall xy - (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) - (Hxy : is_bounded (fe25519WToZ (fst xy)) = true - /\ is_bounded (fe25519WToZ (snd xy)) = true), - let Hx := let (Hx, Hy) := Hxy in Hx in - let Hy := let (Hx, Hy) := Hxy in Hy in - let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => binop_bounds_good bounds = true - | None => False - end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x y Hx Hy. - pose x as x'; pose y as y'. - hnf in x, y; destruct_head' prod. - specialize (H0 (x', y') (conj Hx Hy)). - specialize (H1 (x', y') (conj Hx Hy)). - let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOp_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unop_bounds_good bounds = true - | None => False - end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unop_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOpFEToWire_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unopFEToWire_bounds_good bounds = true - | None => False - end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unop_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOpWireToFE_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_wire_digitsW x) - (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), - let args := unopWireToFE_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_wire_digitsW x) - (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), - let args := unopWireToFE_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unopWireToFE_bounds_good bounds = true - | None => False - end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unopWireToFE_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOpFEToZ_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unopFEToZ_bounds_good bounds = true - | None => False - end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unop_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. Ltac rexpr_correct := let ropW' := fresh in diff --git a/src/Specific/GF25519Reflective/CommonBinOp.v b/src/Specific/GF25519Reflective/CommonBinOp.v new file mode 100644 index 000000000..32dae16e6 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonBinOp.v @@ -0,0 +1,50 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprBinOp_correct_and_bounded + ropW op (ropZ_sig : rexpr_binop_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall xy + (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) + (Hxy : is_bounded (fe25519WToZ (fst xy)) = true + /\ is_bounded (fe25519WToZ (snd xy)) = true), + let Hx := let (Hx, Hy) := Hxy in Hx in + let Hy := let (Hx, Hy) := Hxy in Hy in + let args := binop_args_to_bounded xy Hx Hy in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall xy + (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) + (Hxy : is_bounded (fe25519WToZ (fst xy)) = true + /\ is_bounded (fe25519WToZ (snd xy)) = true), + let Hx := let (Hx, Hy) := Hxy in Hx in + let Hy := let (Hx, Hy) := Hxy in Hy in + let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => binop_bounds_good bounds = true + | None => False + end) + : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x y Hx Hy. + pose x as x'; pose y as y'. + hnf in x, y; destruct_head' prod. + specialize (H0 (x', y') (conj Hx Hy)). + specialize (H1 (x', y') (conj Hx Hy)). + let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOp.v b/src/Specific/GF25519Reflective/CommonUnOp.v new file mode 100644 index 000000000..eac381b50 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOp.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOp_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unop_bounds_good bounds = true + | None => False + end) + : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v new file mode 100644 index 000000000..2fa1d2ee3 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpFEToWire_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopFEToWire_bounds_good bounds = true + | None => False + end) + : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v new file mode 100644 index 000000000..7528cfc2d --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpFEToZ_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopFEToZ_bounds_good bounds = true + | None => False + end) + : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v new file mode 100644 index 000000000..d61807413 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpWireToFE_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_wire_digitsW x) + (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), + let args := unopWireToFE_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_wire_digitsW x) + (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), + let args := unopWireToFE_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopWireToFE_bounds_good bounds = true + | None => False + end) + : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unopWireToFE_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v index 36357fcb7..ae3a6a4c6 100644 --- a/src/Specific/GF25519Reflective/Reified/Add.v +++ b/src/Specific/GF25519Reflective/Reified/Add.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition raddZ_sig : rexpr_binop_sig add. Proof. reify_sig. Defined. Definition raddW := Eval vm_compute in rword_of_Z raddZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v index 0ff563a8c..3051121c0 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v +++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rcarry_addZ_sig : rexpr_binop_sig carry_add. Proof. reify_sig. Defined. Definition rcarry_addW := Eval vm_compute in rword_of_Z rcarry_addZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v index 4c21fbeb8..571b9db97 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v +++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. Definition rcarry_oppZ_sig : rexpr_unop_sig carry_opp. Proof. reify_sig. Defined. Definition rcarry_oppW := Eval vm_compute in rword_of_Z rcarry_oppZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v index 3acfb1f45..fda466861 100644 --- a/src/Specific/GF25519Reflective/Reified/CarrySub.v +++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rcarry_subZ_sig : rexpr_binop_sig carry_sub. Proof. reify_sig. Defined. Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v index e3ecc62c8..0dcea29e4 100644 --- a/src/Specific/GF25519Reflective/Reified/Freeze.v +++ b/src/Specific/GF25519Reflective/Reified/Freeze.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined. Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v index 73ee6904a..69eb3ba41 100644 --- a/src/Specific/GF25519Reflective/Reified/GeModulus.v +++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOpFEToZ. Definition rge_modulusZ_sig : rexpr_unop_FEToZ_sig ge_modulus. Proof. reify_sig. Defined. Definition rge_modulusW := Eval vm_compute in rword_of_Z rge_modulusZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v index a206f02a1..0c298134d 100644 --- a/src/Specific/GF25519Reflective/Reified/Mul.v +++ b/src/Specific/GF25519Reflective/Reified/Mul.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rmulZ_sig : rexpr_binop_sig mul. Proof. reify_sig. Defined. Definition rmulW := Eval vm_compute in rword_of_Z rmulZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v index 907771b14..58f2a6fbb 100644 --- a/src/Specific/GF25519Reflective/Reified/Opp.v +++ b/src/Specific/GF25519Reflective/Reified/Opp.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. Definition roppZ_sig : rexpr_unop_sig opp. Proof. reify_sig. Defined. Definition roppW := Eval vm_compute in rword_of_Z roppZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v index a7cf4fc13..cd85d0cd7 100644 --- a/src/Specific/GF25519Reflective/Reified/Pack.v +++ b/src/Specific/GF25519Reflective/Reified/Pack.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOpFEToWire. Definition rpackZ_sig : rexpr_unop_FEToWire_sig pack. Proof. reify_sig. Defined. Definition rpackW := Eval vm_compute in rword_of_Z rpackZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v index 9b684248d..03356cd50 100644 --- a/src/Specific/GF25519Reflective/Reified/Sub.v +++ b/src/Specific/GF25519Reflective/Reified/Sub.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined. Definition rsubW := Eval vm_compute in rword_of_Z rsubZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v index 027eedf39..a96f87d96 100644 --- a/src/Specific/GF25519Reflective/Reified/Unpack.v +++ b/src/Specific/GF25519Reflective/Reified/Unpack.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOpWireToFE. Definition runpackZ_sig : rexpr_unop_WireToFE_sig unpack. Proof. reify_sig. Defined. Definition runpackW := Eval vm_compute in rword_of_Z runpackZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py index 76ac2c91b..404afc1ea 100755 --- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py +++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py @@ -25,7 +25,7 @@ Definition r%(lname)sW_correct_and_bounded match proof_admitted with end match proof_admitted with end. """ % locals() with open(name.replace('_', '') + '.v', 'w') as f: - f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common. + f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common%(uopkind)s. Definition r%(lname)sZ_sig : rexpr_%(lopkind)s_sig %(lname)s. Proof. reify_sig. Defined. Definition r%(lname)sW := Eval vm_compute in rword_of_Z r%(lname)sZ_sig. -- cgit v1.2.3