diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective')
9 files changed, 102 insertions, 109 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index c7b1a69fb..dd78063a8 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Util.Tower. Require Import Crypto.Util.LetIn. @@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Notation Expr := (Expr base_type WordW.interp_base_type op). +Notation Expr := (Expr base_type op). Local Ltac make_type_from' T := let T := (eval compute in T) in @@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition expr_nm_Op count_in count_out interp_base_type var : Type - := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). -Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. -Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). -Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. -Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. -Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. -Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. -Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. -Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Definition expr_nm_Op count_in count_out var : Type + := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out). +Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT. +Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT. +Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT. +Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT. +Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ). +Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT. +Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET. +Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT. +Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT. +Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT. +Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT. +Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT. Local Ltac bounds_from_list_cps ls := lazymatch (eval hnf in ls) with @@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_64 op) Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in let ropZ_sig := ropZ_sigv in - let ropW := MapInterp (fun _ x => x) ropW' in - let ropZ := MapInterp WordW.to_Z ropW' in - let ropBounds := MapInterp ZBounds.of_wordW ropW' in - let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in + let ropW := ropW' in + let ropZ := ropW' in + let ropBounds := ropW' in + let ropBoundedWordW := ropW' in ropZ = proj1_sig ropZ_sig /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ) /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds) @@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in - refine (LetIn (UnReturn x) _); + let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in + refine (LetIn (invert_Return x) _); let x'' := fresh "x''" in intro x''; let xv := assoc_right_tuple x'' (@None) in refine (SmartVarf (xv : interp_flat_type _ t')). -Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var. +Definition unop_make_args {var} (x : exprArg var) : exprArgRev var. Proof. make_args x. Defined. -Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var. +Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var. Proof. make_args x. Defined. Local Ltac args_to_bounded x H := @@ -432,31 +432,31 @@ Defined. Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool. Proof. make_bounds_prop bounds Expr4Op_bounds. Defined. -Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var +Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_64 f k)). -Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_64 f k)). +Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var := fun x y - => LetIn (UnReturn (unop_make_args x)) + => LetIn (invert_Return (unop_make_args x)) (fun x' - => LetIn (UnReturn (unop_make_args y)) + => LetIn (invert_Return (unop_make_args y)) (fun y' - => UnReturn (Apply length_fe25519_64 + => invert_Return (Apply length_fe25519_64 (Apply length_fe25519_64 f x') y'))). -Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var +Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_64 f k)). -Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_64 f k)). +Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var := fun x - => LetIn (UnReturn (unop_wire_make_args x)) - (fun k => UnReturn (Apply (List.length wire_widths) f k)). -Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var + => LetIn (invert_Return (unop_wire_make_args x)) + (fun k => invert_Return (Apply (List.length wire_widths) f k)). +Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var := fun x - => LetIn (UnReturn (unop_make_args x)) - (fun k => UnReturn (Apply length_fe25519_64 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_64 f k)). (* FIXME TODO(jgross): This is a horrible tactic. We should unify the @@ -545,17 +545,14 @@ Ltac rexpr_correct := assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl); cbv zeta; repeat apply conj; [ vm_compute; reflexivity - | apply @InterpRelWf; - [ | apply @RelWfMapInterp, wf_ropW ].. ]; + | apply @InterpWf; + [ | apply wf_ropW ].. ]; auto with interp_related. -Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing). - -Definition rword128ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word128ize end) x. +Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds) (only parsing). @@ -586,6 +583,7 @@ Module Export PrettyPrinting. | in_range _ _ => no | enlargen _ => borked end + | Unit => fun _ => no | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with | no, no => no | yes, no | no, yes | yes, yes => yes diff --git a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v index 634ec3388..9699d43b4 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded let (Hx7, Hx8) := (eta_and Hx78) in let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x'))) with | Some bounds => op9_4_bounds_good bounds = true | None => False end) - : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. + : op9_4_correct_and_bounded ropW op. Proof. intros x0 x1 x2 x3 x4 x5 x6 x7 x8. intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v index c8872efc5..5ebff74a9 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded let Hy := let (Hx, Hy) := Hxy in Hy in let args := binop_args_to_bounded xy Hx Hy in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) 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. + : binop_correct_and_bounded ropW op. Proof. intros x y Hx Hy. pose x as x'; pose y as y'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v index f6a71740a..53b0c372f 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) 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. + : unop_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v index 7bd176749..b9c642d43 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) 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. + : unop_FEToWire_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v index d6b8bb2c7..fcc07a651 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded (Hx : is_bounded (fe25519_64WToZ x) = true), let args := unop_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded let args := unop_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) 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. + : unop_FEToZ_correct ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v index baadad3c3..09292ea2c 100644 --- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Util.Tactics. Local Opaque Interp. @@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), let args := unopWireToFE_args_to_bounded x Hx in match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) + (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW) (LiftOption.to' (Some args))) with | Some _ => True @@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded let args := unopWireToFE_args_to_bounded x Hx in let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x'))) + (ApplyInterpedAll (Interp (@ZBounds.interp_op) 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. + : unop_WireToFE_correct_and_bounded ropW op. Proof. intros x Hx. pose x as x'. diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v index 4143ad79b..a109ec89b 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations128. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add. @@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2 (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y) (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) twice_d _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) P1 P2. -Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _ +Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 -> GF25519_64.fe25519_64) (x' y' : GF25519_64.fe25519_64) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_64 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_64 interp_flat_type] in H. simpl @interp_base_type in *. @@ -103,14 +103,14 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_64 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -121,7 +121,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519_64 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 add_coordinates]. intros. - unfold UnReturn at 13 14 15 16. + unfold invert_Return at 13 14 15 16. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -144,9 +144,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v index 38bd20c08..c105a2846 100644 --- a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Export Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.Z.Interpretations128. @@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify. Require Export Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.InterpWfRel. Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.MapInterpWf. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Spec.MxDH. Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add. @@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2 (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y) a24 _ - (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr) - (fun v f => LetIn (UnReturn v) + (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr) + (fun v f => LetIn (invert_Return v) (fun k => f (Return (SmartVarf k)))) x0 P1 P2. -Definition rladderstepZ'' : Syntax.Expr _ _ _ _ +Definition rladderstepZ'' : Syntax.Expr _ _ _ := Linearize (fun var => apply9 (fun A B => SmartAbs (A := A) (B := B)) @@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf := clearbody k'; subst k'. Lemma interp_helper - (f : Syntax.Expr base_type interp_base_type op ExprBinOpT) - (x y : exprArg interp_base_type interp_base_type) + (f : Syntax.Expr base_type op ExprBinOpT) + (x y : exprArg interp_base_type) (f' : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 -> GF25519_64.fe25519_64) (x' y' : GF25519_64.fe25519_64) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_64 f')) - (Hx : interpf interp_op (UnReturn x) = x') - (Hy : interpf interp_op (UnReturn y) = y') - : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. + (Hx : interpf interp_op (invert_Return x) = x') + (Hy : interpf interp_op (invert_Return y) = y') + : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'. Proof. cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519_64 interp_flat_type] in H. simpl @interp_base_type in *. @@ -107,14 +107,15 @@ Proof. change (fun t => interp_base_type t) with interp_base_type in *. generalize (f interp_base_type); clear f; intro f. cbv [Apply length_fe25519_64 Apply' interp fst snd]. - rewrite <- (UnAbs_eta f). + let f := match goal with f : expr _ _ _ |- _ => f end in + rewrite (invert_Abs_Some (e:=f) eq_refl). repeat match goal with - | [ |- appcontext[UnAbs ?f ?x] ] - => generalize (UnAbs f x); clear f; + | [ |- appcontext[invert_Abs ?f ?x] ] + => generalize (invert_Abs f x); clear f; let f' := fresh "f" in intro f'; - first [ rewrite <- (UnAbs_eta f') - | rewrite <- (UnReturn_eta f') ] + first [ rewrite (invert_Abs_Some (e:=f') eq_refl) + | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ] end. reflexivity. Qed. @@ -125,7 +126,7 @@ Proof. etransitivity; [ apply Interp_Linearize | ]. cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519_64 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_64 ladderstep]. intros; cbv beta zeta. - unfold UnReturn at 14 15 16 17. + unfold invert_Return at 14 15 16 17. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?B ?v] ] => let k := fresh "f" in @@ -148,9 +149,9 @@ Proof. cbv beta; intros end; repeat match goal with - | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ] + | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ] => apply interp_helper; [ assumption | | ] - | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ] + | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ] => vm_compute; reflexivity | [ |- (_, _) = (_, _) ] => reflexivity |