diff options
Diffstat (limited to 'src/SpecificGen')
66 files changed, 690 insertions, 744 deletions
diff --git a/src/SpecificGen/GF2213_32Reflective.v b/src/SpecificGen/GF2213_32Reflective.v index 8b09203e9..2f43e92fd 100644 --- a/src/SpecificGen/GF2213_32Reflective.v +++ b/src/SpecificGen/GF2213_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF2213_32BoundedCommon.wire_digitsW -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v index 56e4bc47c..977f47e69 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common.v +++ b/src/SpecificGen/GF2213_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. 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.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.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_fe2213_32 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_fe2213_32 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_fe2213_32 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_fe2213_32 + => invert_Return (Apply length_fe2213_32 (Apply length_fe2213_32 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_fe2213_32 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_fe2213_32 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_fe2213_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2213_32 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 rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize 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/GF2213_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v index d8d55ca04..49a4782eb 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF2213_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v index 23becba34..0cdef8deb 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF2213_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v index 250a64400..5df7f6c98 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe2213_32WToZ 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/GF2213_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v index 2dcae7edd..0751754d7 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe2213_32WToZ 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/GF2213_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v index ef997e3f9..d6cf8653d 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe2213_32WToZ 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/GF2213_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v index 4342ef865..15dc52517 100644 --- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF2213_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v index 76c119adc..c2fb547d0 100644 --- a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. 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.Interpretations64. @@ -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.GF2213_32Reflective.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' : GF2213_32.fe2213_32 -> GF2213_32.fe2213_32 -> GF2213_32.fe2213_32) (x' y' : GF2213_32.fe2213_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2213_32 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_fe2213_32 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_fe2213_32 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_fe2213_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 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/GF2213_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v index 18bbd8289..51b07c4d6 100644 --- a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Export Crypto.SpecificGen.GF2213_32BoundedCommon. 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.Interpretations64. @@ -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.GF2213_32Reflective.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' : GF2213_32.fe2213_32 -> GF2213_32.fe2213_32 -> GF2213_32.fe2213_32) (x' y' : GF2213_32.fe2213_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2213_32 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_fe2213_32 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_fe2213_32 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_fe2213_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2213_32 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 diff --git a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v index 3b95ae5c4..4dd4b8e9e 100644 --- a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2213_32. Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF2213_32BoundedCommon.fe2 -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF2519_32Reflective.v b/src/SpecificGen/GF2519_32Reflective.v index 5ebb35b5e..f3c1d7c08 100644 --- a/src/SpecificGen/GF2519_32Reflective.v +++ b/src/SpecificGen/GF2519_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF2519_32BoundedCommon.wire_digitsW -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v index dd7be148a..6f6f607fb 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common.v +++ b/src/SpecificGen/GF2519_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. 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.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.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_fe2519_32 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_fe2519_32 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_fe2519_32 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_fe2519_32 + => invert_Return (Apply length_fe2519_32 (Apply length_fe2519_32 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_fe2519_32 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_fe2519_32 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_fe2519_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe2519_32 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 rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize 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/GF2519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v index 1cedb55ac..6a07ae3cf 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF2519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v index 095c7a8c6..e20ab88d1 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF2519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v index f2e091570..505a9a9ce 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe2519_32WToZ 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/GF2519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v index cf8a85d6f..e84df9be2 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe2519_32WToZ 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/GF2519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v index 7d70c1234..054155d1f 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe2519_32WToZ 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/GF2519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v index 22e68fcf5..b22e73f6e 100644 --- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF2519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v index 332178361..1e74a8cf5 100644 --- a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. 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.Interpretations64. @@ -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.GF2519_32Reflective.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' : GF2519_32.fe2519_32 -> GF2519_32.fe2519_32 -> GF2519_32.fe2519_32) (x' y' : GF2519_32.fe2519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2519_32 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_fe2519_32 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_fe2519_32 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_fe2519_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 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/GF2519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v index e5ea0e52b..3a069c45c 100644 --- a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Export Crypto.SpecificGen.GF2519_32BoundedCommon. 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.Interpretations64. @@ -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.GF2519_32Reflective.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' : GF2519_32.fe2519_32 -> GF2519_32.fe2519_32 -> GF2519_32.fe2519_32) (x' y' : GF2519_32.fe2519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe2519_32 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_fe2519_32 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_fe2519_32 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_fe2519_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe2519_32 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 diff --git a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v index a400a893a..e1f691607 100644 --- a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF2519_32. Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF2519_32BoundedCommon.fe2 -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF25519_32Reflective.v b/src/SpecificGen/GF25519_32Reflective.v index 92a1bdbf8..d3e45d36d 100644 --- a/src/SpecificGen/GF25519_32Reflective.v +++ b/src/SpecificGen/GF25519_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF25519_32BoundedCommon.wire_digitsW -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index 644ed7c92..bd01c31a2 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. 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.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.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_32 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_32 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_32 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_32 + => invert_Return (Apply length_fe25519_32 (Apply length_fe25519_32 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_32 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_32 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_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe25519_32 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 rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize 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_32Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v index c163fa18a..fc0bf3d0b 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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_32Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v index f254a2d3a..3053b6d51 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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_32Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v index 246dcbf70..dd7c392b1 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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_32WToZ 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_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v index a940a0c8b..f05bfdba4 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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_32WToZ 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_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v index b7ec2c6a5..ea8f01446 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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_32WToZ 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_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v index 34e0896f1..2a19f9eb1 100644 --- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v index 567ed1a01..c276df344 100644 --- a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. 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.Interpretations64. @@ -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_32Reflective.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_32.fe25519_32 -> GF25519_32.fe25519_32 -> GF25519_32.fe25519_32) (x' y' : GF25519_32.fe25519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_32 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_32 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_32 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_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 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_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v index 9fc865d98..33b232dc2 100644 --- a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Export Crypto.SpecificGen.GF25519_32BoundedCommon. 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.Interpretations64. @@ -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_32Reflective.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_32.fe25519_32 -> GF25519_32.fe25519_32 -> GF25519_32.fe25519_32) (x' y' : GF25519_32.fe25519_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe25519_32 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_32 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_32 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_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519_32 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 diff --git a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v index b13c07f44..b4840a4d2 100644 --- a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_32. Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF25519_32BoundedCommon.fe -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF25519_64Reflective.v b/src/SpecificGen/GF25519_64Reflective.v index 86b8735d6..620c96713 100644 --- a/src/SpecificGen/GF25519_64Reflective.v +++ b/src/SpecificGen/GF25519_64Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_bexpr (rword128ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr (rword128ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr (rword128ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.word128 - := Eval asm_interp in interp_uexpr_FEToZ (rword128ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword128ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF25519_64BoundedCommon.wire_digitsW -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - := Eval asm_interp in interp_uexpr_WireToFE (rword128ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. 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 diff --git a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v index e9067cee8..9050ee849 100644 --- a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF25519_64. Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations128. Require Crypto.Reflection.Z.Interpretations128.Relations. Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + mapf_interp_flat_type WordW.interp_base_type word128ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF25519_64BoundedCommon.fe -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword128ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF41417_32Reflective.v b/src/SpecificGen/GF41417_32Reflective.v index 5f37c51fa..efc54565e 100644 --- a/src/SpecificGen/GF41417_32Reflective.v +++ b/src/SpecificGen/GF41417_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF41417_32BoundedCommon.wire_digitsW -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v index b9f98cfba..9ab04a78f 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common.v +++ b/src/SpecificGen/GF41417_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. 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.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.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_fe41417_32 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_fe41417_32 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_fe41417_32 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_fe41417_32 + => invert_Return (Apply length_fe41417_32 (Apply length_fe41417_32 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_fe41417_32 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_fe41417_32 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_fe41417_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe41417_32 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 rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize 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/GF41417_32Reflective/Common9_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v index d7916c957..f1230b04e 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF41417_32Reflective/CommonBinOp.v b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v index 3542dc9cf..438110cb8 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF41417_32Reflective/CommonUnOp.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v index 7d86a5e95..b3d00f8c9 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe41417_32WToZ 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/GF41417_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v index a008c50bb..8a8075739 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe41417_32WToZ 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/GF41417_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v index 700581bad..19664d936 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe41417_32WToZ 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/GF41417_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v index d04d44d32..7c23f3be8 100644 --- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF41417_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v index 8288d10e0..4c658f227 100644 --- a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. 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.Interpretations64. @@ -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.GF41417_32Reflective.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' : GF41417_32.fe41417_32 -> GF41417_32.fe41417_32 -> GF41417_32.fe41417_32) (x' y' : GF41417_32.fe41417_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe41417_32 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_fe41417_32 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_fe41417_32 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_fe41417_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 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/GF41417_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v index 7384553a5..1f3516551 100644 --- a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Export Crypto.SpecificGen.GF41417_32BoundedCommon. 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.Interpretations64. @@ -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.GF41417_32Reflective.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' : GF41417_32.fe41417_32 -> GF41417_32.fe41417_32 -> GF41417_32.fe41417_32) (x' y' : GF41417_32.fe41417_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe41417_32 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_fe41417_32 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_fe41417_32 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_fe41417_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe41417_32 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 diff --git a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v index 6d4dd60bb..82f159e25 100644 --- a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF41417_32. Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF41417_32BoundedCommon.fe -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. diff --git a/src/SpecificGen/GF5211_32Reflective.v b/src/SpecificGen/GF5211_32Reflective.v index faf61f8c2..8c80562de 100644 --- a/src/SpecificGen/GF5211_32Reflective.v +++ b/src/SpecificGen/GF5211_32Reflective.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -50,7 +49,7 @@ Declare Reduction asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta @@ -61,41 +60,41 @@ Ltac asm_interp WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. Definition interp_radd : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_bexpr (rword64ize radd). + := Eval asm_interp in interp_bexpr radd. (*Print interp_radd.*) Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. Definition interp_rsub : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_bexpr (rword64ize rsub). + := Eval asm_interp in interp_bexpr rsub. (*Print interp_rsub.*) Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. Definition interp_rmul : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_bexpr (rword64ize rmul). + := Eval asm_interp in interp_bexpr rmul. (*Print interp_rmul.*) Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. Definition interp_ropp : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_uexpr (rword64ize ropp). + := Eval asm_interp in interp_uexpr ropp. (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. Definition interp_rprefreeze : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). + := Eval asm_interp in interp_uexpr rprefreeze. (*Print interp_rprefreeze.*) Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.word64 - := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). + := Eval asm_interp in interp_uexpr_FEToZ rge_modulus. Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl. Definition interp_rpack : SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.wire_digitsW - := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack). + := Eval asm_interp in interp_uexpr_FEToWire rpack. Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl. Definition interp_runpack : SpecificGen.GF5211_32BoundedCommon.wire_digitsW -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack). + := Eval asm_interp in interp_uexpr_WireToFE runpack. Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl. Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v index 396d2cd35..670234315 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common.v +++ b/src/SpecificGen/GF5211_32Reflective/Common.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. 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.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.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_fe5211_32 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_fe5211_32 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_fe5211_32 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_fe5211_32 + => invert_Return (Apply length_fe5211_32 (Apply length_fe5211_32 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_fe5211_32 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_fe5211_32 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_fe5211_32 f k)). + => LetIn (invert_Return (unop_make_args x)) + (fun k => invert_Return (Apply length_fe5211_32 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 rword64ize {t} (x : Expr t) : Expr t - := MapInterp (fun t => match t with TZ => word64ize 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/GF5211_32Reflective/Common9_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v index 627b8849d..b1da3f12f 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v +++ b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF5211_32Reflective/CommonBinOp.v b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v index ccaefeb38..2395d7c74 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF5211_32Reflective/CommonUnOp.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v index 4c8c024ef..29652a1e8 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe5211_32WToZ 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/GF5211_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v index 4abf5e85f..9d37b910f 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe5211_32WToZ 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/GF5211_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v index 821f6529c..9dde1f276 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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 (fe5211_32WToZ 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/GF5211_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v index 9284bf40f..e20146853 100644 --- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v +++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v @@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Z.Interpretations64. 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/GF5211_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v index 26fb59a04..85da73838 100644 --- a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v +++ b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. 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.Interpretations64. @@ -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.GF5211_32Reflective.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' : GF5211_32.fe5211_32 -> GF5211_32.fe5211_32 -> GF5211_32.fe5211_32) (x' y' : GF5211_32.fe5211_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe5211_32 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_fe5211_32 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_fe5211_32 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_fe5211_32 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 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/GF5211_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v index 71cb965a9..b05fc64a6 100644 --- a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v +++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v @@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Export Crypto.SpecificGen.GF5211_32BoundedCommon. 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.Interpretations64. @@ -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.GF5211_32Reflective.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' : GF5211_32.fe5211_32 -> GF5211_32.fe5211_32 -> GF5211_32.fe5211_32) (x' y' : GF5211_32.fe5211_32) (H : interp_type_gen_rel_pointwise (fun _ => Logic.eq) (Interp interp_op f) (uncurry_binop_fe5211_32 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_fe5211_32 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_fe5211_32 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_fe5211_32 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe5211_32 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 diff --git a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v index ddba2a199..5284ffbcd 100644 --- a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v +++ b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v @@ -9,7 +9,6 @@ Require Export Crypto.SpecificGen.GF5211_32. Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. Require Import Crypto.Reflection.Z.Interpretations64. Require Crypto.Reflection.Z.Interpretations64.Relations. Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. @@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp_add_coordinates := cbv beta iota delta @@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates WordW.interp_op WordW.interp_base_type Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type - mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type WordW.interp_base_type word64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. @@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : SpecificGen.GF5211_32BoundedCommon.fe5 -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4 - := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). + := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates. (*Print interp_radd_coordinates.*) Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. |