diff options
32 files changed, 63 insertions, 1843 deletions
diff --git a/_CoqProject b/_CoqProject index 3617b5890..f6d2f69f0 100644 --- a/_CoqProject +++ b/_CoqProject @@ -164,7 +164,6 @@ src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v src/Specific/GF25519Reflective/Common.v -src/Specific/GF25519Reflective/Common10_4Op.v src/Specific/GF25519Reflective/Common9_4Op.v src/Specific/GF25519Reflective/CommonBinOp.v src/Specific/GF25519Reflective/CommonUnOp.v diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index fea289d78..361cc83a7 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -197,26 +197,6 @@ Proof. repeat (etransitivity; [ apply app_10_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519) := - app_10 x0 (fun x0' => - app_10 x1 (fun x1' => - app_10 x2 (fun x2' => - app_10 x3 (fun x3' => - app_10 x4 (fun x4' => - app_10 x5 (fun x5' => - app_10 x6 (fun x6' => - app_10 x7 (fun x7' => - app_10 x8 (fun x8' => - app_10 x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_10_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe25519 {T} (op : fe25519 -> T) := Eval compute in Tuple.uncurry (n:=length_fe25519) op. Definition curry_unop_fe25519 {T} op : fe25519 -> T @@ -250,13 +230,6 @@ Definition curry_9op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 - appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe25519 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T) - := Eval compute in uncurry_n_op_fe25519 10 op. -Definition curry_10op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe25519) : { fg : fe25519 | fg = add_opt f g}. Proof. diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index f50304073..683f5f47f 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe25519W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519W) := - app_fe25519W x0 (fun x0' => - app_fe25519W x1 (fun x1' => - app_fe25519W x2 (fun x2' => - app_fe25519W x3 (fun x3' => - app_fe25519W x4 (fun x4' => - app_fe25519W x5 (fun x5' => - app_fe25519W x6 (fun x6' => - app_fe25519W x7 (fun x7' => - app_fe25519W x8 (fun x8' => - app_fe25519W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe25519W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe25519W_sig (x : fe25519W) : { v : fe25519W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe25519W {T} op : fe25519W -> fe25519W -> fe25519W -> fe255 appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe25519W {T} (op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe25519W (fun x0 => - uncurry_unop_fe25519W (fun x1 => - uncurry_unop_fe25519W (fun x2 => - uncurry_unop_fe25519W (fun x3 => - uncurry_unop_fe25519W (fun x4 => - uncurry_unop_fe25519W (fun x5 => - uncurry_unop_fe25519W (fun x6 => - uncurry_unop_fe25519W (fun x7 => - uncurry_unop_fe25519W (fun x8 => - uncurry_unop_fe25519W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe25519W {T} op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T - := Eval cbv (*-[word64]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe25519W (x : fe25519) : fe25519W := Eval app_tuple_map in app_fe25519 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe25519WToZ x0) (fe25519WToZ x1) (fe25519WToZ x2) (fe25519WToZ x3) (fe25519WToZ x4) (fe25519WToZ x5) (fe25519WToZ x6) (fe25519WToZ x7) (fe25519WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe25519WToZ x0) = true - -> is_bounded (fe25519WToZ x1) = true - -> is_bounded (fe25519WToZ x2) = true - -> is_bounded (fe25519WToZ x3) = true - -> is_bounded (fe25519WToZ x4) = true - -> is_bounded (fe25519WToZ x5) = true - -> is_bounded (fe25519WToZ x6) = true - -> is_bounded (fe25519WToZ x7) = true - -> is_bounded (fe25519WToZ x8) = true - -> is_bounded (fe25519WToZ x9) = true - -> (Tuple.map (n:=k) fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe25519WToZ x0) (fe25519WToZ x1) (fe25519WToZ x2) (fe25519WToZ x3) (fe25519WToZ x4) (fe25519WToZ x5) (fe25519WToZ x6) (fe25519WToZ x7) (fe25519WToZ x8) (fe25519WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF25519.prefreeze. diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 431e38c8c..d59da1d93 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe25519 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> Specific.GF25519BoundedCommon.fe25519W -> Tuple.tuple Specific.GF25519BoundedCommon.fe25519W 4 := fun e => curry_9op_fe25519W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Specific.GF25519BoundedCommon.fe25519W - -> Tuple.tuple Specific.GF25519BoundedCommon.fe25519W 4 - := fun e => curry_10op_fe25519W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe25519 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W * fe25519W) - (H0 : is_bounded (fe25519WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe25519WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe25519WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe25519WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe25519WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe25519WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W curry_10op_fe25519W - curry_binop_fe25519 curry_unop_fe25519 curry_unop_wire_digits curry_9op_fe25519 curry_10op_fe25519 - uncurry_binop_fe25519W uncurry_unop_fe25519W uncurry_unop_wire_digitsW uncurry_9op_fe25519W uncurry_10op_fe25519W - uncurry_binop_fe25519 uncurry_unop_fe25519 uncurry_unop_wire_digits uncurry_9op_fe25519 uncurry_10op_fe25519 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W + curry_binop_fe25519 curry_unop_fe25519 curry_unop_wire_digits curry_9op_fe25519 + uncurry_binop_fe25519W uncurry_unop_fe25519W uncurry_unop_wire_digitsW uncurry_9op_fe25519W + uncurry_binop_fe25519 uncurry_unop_fe25519 uncurry_unop_wire_digits uncurry_9op_fe25519 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe25519WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe25519WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe25519WToZ; simpl @wire_digitsWToZ; diff --git a/src/Specific/GF25519Reflective/Common10_4Op.v b/src/Specific/GF25519Reflective/Common10_4Op.v deleted file mode 100644 index 0110637e4..000000000 --- a/src/Specific/GF25519Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.Specific.GF25519Reflective.Common. -Require Import Crypto.Specific.GF25519BoundedCommon. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe25519W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe25519W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe25519W (snd (fst (fst (fst x0123456789)))), - eta_fe25519W (snd (fst (fst x0123456789))), - eta_fe25519W (snd (fst x0123456789)), - eta_fe25519W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe25519WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe25519WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe25519WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe25519W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe25519W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe25519W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe25519W (snd (fst (fst (fst x0123456789)))), - eta_fe25519W (snd (fst (fst x0123456789))), - eta_fe25519W (snd (fst x0123456789)), - eta_fe25519W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe25519WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe25519WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe25519WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe25519WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*) diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v index 71e51ccac..9b8f0d74e 100644 --- a/src/SpecificGen/GF2213_32.v +++ b/src/SpecificGen/GF2213_32.v @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2213_32) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe2213_32 {T} (op : fe2213_32 -> T) := Eval compute in Tuple.uncurry (n:=length_fe2213_32) op. Definition curry_unop_fe2213_32 {T} op : fe2213_32 -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> fe2213_32 -> f appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe2213_32 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T) - := Eval compute in uncurry_n_op_fe2213_32 10 op. -Definition curry_10op_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe2213_32) : { fg : fe2213_32 | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v index 2451f5f1d..f9b215ac9 100644 --- a/src/SpecificGen/GF2213_32BoundedCommon.v +++ b/src/SpecificGen/GF2213_32BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe2213_32W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2213_32W) := - app_fe2213_32W x0 (fun x0' => - app_fe2213_32W x1 (fun x1' => - app_fe2213_32W x2 (fun x2' => - app_fe2213_32W x3 (fun x3' => - app_fe2213_32W x4 (fun x4' => - app_fe2213_32W x5 (fun x5' => - app_fe2213_32W x6 (fun x6' => - app_fe2213_32W x7 (fun x7' => - app_fe2213_32W x8 (fun x8' => - app_fe2213_32W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe2213_32W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe2213_32W_sig (x : fe2213_32W) : { v : fe2213_32W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe2213_32W {T} op : fe2213_32W -> fe2213_32W -> fe2213_32W appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe2213_32W {T} (op : fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe2213_32W (fun x0 => - uncurry_unop_fe2213_32W (fun x1 => - uncurry_unop_fe2213_32W (fun x2 => - uncurry_unop_fe2213_32W (fun x3 => - uncurry_unop_fe2213_32W (fun x4 => - uncurry_unop_fe2213_32W (fun x5 => - uncurry_unop_fe2213_32W (fun x6 => - uncurry_unop_fe2213_32W (fun x7 => - uncurry_unop_fe2213_32W (fun x8 => - uncurry_unop_fe2213_32W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe2213_32W {T} op : fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> T - := Eval cbv (*-[word64]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe2213_32W (x : fe2213_32) : fe2213_32W := Eval app_tuple_map in app_fe2213_32 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe2213_32WToZ x0) (fe2213_32WToZ x1) (fe2213_32WToZ x2) (fe2213_32WToZ x3) (fe2213_32WToZ x4) (fe2213_32WToZ x5) (fe2213_32WToZ x6) (fe2213_32WToZ x7) (fe2213_32WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe2213_32WToZ x0) = true - -> is_bounded (fe2213_32WToZ x1) = true - -> is_bounded (fe2213_32WToZ x2) = true - -> is_bounded (fe2213_32WToZ x3) = true - -> is_bounded (fe2213_32WToZ x4) = true - -> is_bounded (fe2213_32WToZ x5) = true - -> is_bounded (fe2213_32WToZ x6) = true - -> is_bounded (fe2213_32WToZ x7) = true - -> is_bounded (fe2213_32WToZ x8) = true - -> is_bounded (fe2213_32WToZ x9) = true - -> (Tuple.map (n:=k) fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe2213_32WToZ x0) (fe2213_32WToZ x1) (fe2213_32WToZ x2) (fe2213_32WToZ x3) (fe2213_32WToZ x4) (fe2213_32WToZ x5) (fe2213_32WToZ x6) (fe2213_32WToZ x7) (fe2213_32WToZ x8) (fe2213_32WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2213_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF2213_32.prefreeze. diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v index 884ae0fc3..e5fab2a8d 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common.v +++ b/src/SpecificGen/GF2213_32Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe2213_32 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4 := fun e => curry_9op_fe2213_32W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W - -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4 - := fun e => curry_10op_fe2213_32W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe22 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe2213_32 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2213_32 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe2213_32 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W * fe2213_32W) - (H0 : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe2213_32WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe2213_32WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe2213_32WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe2213_32WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W curry_10op_fe2213_32W - curry_binop_fe2213_32 curry_unop_fe2213_32 curry_unop_wire_digits curry_9op_fe2213_32 curry_10op_fe2213_32 - uncurry_binop_fe2213_32W uncurry_unop_fe2213_32W uncurry_unop_wire_digitsW uncurry_9op_fe2213_32W uncurry_10op_fe2213_32W - uncurry_binop_fe2213_32 uncurry_unop_fe2213_32 uncurry_unop_wire_digits uncurry_9op_fe2213_32 uncurry_10op_fe2213_32 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W + curry_binop_fe2213_32 curry_unop_fe2213_32 curry_unop_wire_digits curry_9op_fe2213_32 + uncurry_binop_fe2213_32W uncurry_unop_fe2213_32W uncurry_unop_wire_digitsW uncurry_9op_fe2213_32W + uncurry_binop_fe2213_32 uncurry_unop_fe2213_32 uncurry_unop_wire_digits uncurry_9op_fe2213_32 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe2213_32WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe2213_32WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe2213_32WToZ; simpl @wire_digitsWToZ; diff --git a/src/SpecificGen/GF2213_32Reflective/Common10_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common10_4Op.v deleted file mode 100644 index 26f1edaef..000000000 --- a/src/SpecificGen/GF2213_32Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.SpecificGen.GF2213_32Reflective.Common. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe2213_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe2213_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe2213_32W (snd (fst (fst (fst x0123456789)))), - eta_fe2213_32W (snd (fst (fst x0123456789))), - eta_fe2213_32W (snd (fst x0123456789)), - eta_fe2213_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe2213_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe2213_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe2213_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe2213_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe2213_32W (snd (fst (fst (fst x0123456789)))), - eta_fe2213_32W (snd (fst (fst x0123456789))), - eta_fe2213_32W (snd (fst x0123456789)), - eta_fe2213_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe2213_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe2213_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*) diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v index a9cba3ce0..72c686596 100644 --- a/src/SpecificGen/GF2519_32.v +++ b/src/SpecificGen/GF2519_32.v @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2519_32) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe2519_32 {T} (op : fe2519_32 -> T) := Eval compute in Tuple.uncurry (n:=length_fe2519_32) op. Definition curry_unop_fe2519_32 {T} op : fe2519_32 -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> fe2519_32 -> f appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe2519_32 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T) - := Eval compute in uncurry_n_op_fe2519_32 10 op. -Definition curry_10op_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe2519_32) : { fg : fe2519_32 | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v index f8538a6fb..f6bf77cb0 100644 --- a/src/SpecificGen/GF2519_32BoundedCommon.v +++ b/src/SpecificGen/GF2519_32BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe2519_32W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2519_32W) := - app_fe2519_32W x0 (fun x0' => - app_fe2519_32W x1 (fun x1' => - app_fe2519_32W x2 (fun x2' => - app_fe2519_32W x3 (fun x3' => - app_fe2519_32W x4 (fun x4' => - app_fe2519_32W x5 (fun x5' => - app_fe2519_32W x6 (fun x6' => - app_fe2519_32W x7 (fun x7' => - app_fe2519_32W x8 (fun x8' => - app_fe2519_32W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe2519_32W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe2519_32W_sig (x : fe2519_32W) : { v : fe2519_32W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe2519_32W {T} op : fe2519_32W -> fe2519_32W -> fe2519_32W appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe2519_32W {T} (op : fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe2519_32W (fun x0 => - uncurry_unop_fe2519_32W (fun x1 => - uncurry_unop_fe2519_32W (fun x2 => - uncurry_unop_fe2519_32W (fun x3 => - uncurry_unop_fe2519_32W (fun x4 => - uncurry_unop_fe2519_32W (fun x5 => - uncurry_unop_fe2519_32W (fun x6 => - uncurry_unop_fe2519_32W (fun x7 => - uncurry_unop_fe2519_32W (fun x8 => - uncurry_unop_fe2519_32W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe2519_32W {T} op : fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> T - := Eval cbv (*-[word64]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe2519_32W (x : fe2519_32) : fe2519_32W := Eval app_tuple_map in app_fe2519_32 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe2519_32WToZ x0) (fe2519_32WToZ x1) (fe2519_32WToZ x2) (fe2519_32WToZ x3) (fe2519_32WToZ x4) (fe2519_32WToZ x5) (fe2519_32WToZ x6) (fe2519_32WToZ x7) (fe2519_32WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe2519_32WToZ x0) = true - -> is_bounded (fe2519_32WToZ x1) = true - -> is_bounded (fe2519_32WToZ x2) = true - -> is_bounded (fe2519_32WToZ x3) = true - -> is_bounded (fe2519_32WToZ x4) = true - -> is_bounded (fe2519_32WToZ x5) = true - -> is_bounded (fe2519_32WToZ x6) = true - -> is_bounded (fe2519_32WToZ x7) = true - -> is_bounded (fe2519_32WToZ x8) = true - -> is_bounded (fe2519_32WToZ x9) = true - -> (Tuple.map (n:=k) fe2519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe2519_32WToZ x0) (fe2519_32WToZ x1) (fe2519_32WToZ x2) (fe2519_32WToZ x3) (fe2519_32WToZ x4) (fe2519_32WToZ x5) (fe2519_32WToZ x6) (fe2519_32WToZ x7) (fe2519_32WToZ x8) (fe2519_32WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF2519_32.prefreeze. diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v index bf4be644f..729c79995 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common.v +++ b/src/SpecificGen/GF2519_32Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe2519_32 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4 := fun e => curry_9op_fe2519_32W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W - -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4 - := fun e => curry_10op_fe2519_32W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe2519_32 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe2519_32 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe2519_32 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W * fe2519_32W) - (H0 : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe2519_32WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe2519_32WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe2519_32WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe2519_32WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W curry_10op_fe2519_32W - curry_binop_fe2519_32 curry_unop_fe2519_32 curry_unop_wire_digits curry_9op_fe2519_32 curry_10op_fe2519_32 - uncurry_binop_fe2519_32W uncurry_unop_fe2519_32W uncurry_unop_wire_digitsW uncurry_9op_fe2519_32W uncurry_10op_fe2519_32W - uncurry_binop_fe2519_32 uncurry_unop_fe2519_32 uncurry_unop_wire_digits uncurry_9op_fe2519_32 uncurry_10op_fe2519_32 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W + curry_binop_fe2519_32 curry_unop_fe2519_32 curry_unop_wire_digits curry_9op_fe2519_32 + uncurry_binop_fe2519_32W uncurry_unop_fe2519_32W uncurry_unop_wire_digitsW uncurry_9op_fe2519_32W + uncurry_binop_fe2519_32 uncurry_unop_fe2519_32 uncurry_unop_wire_digits uncurry_9op_fe2519_32 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe2519_32WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe2519_32WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe2519_32WToZ; simpl @wire_digitsWToZ; diff --git a/src/SpecificGen/GF2519_32Reflective/Common10_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common10_4Op.v deleted file mode 100644 index cb762e1cb..000000000 --- a/src/SpecificGen/GF2519_32Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.SpecificGen.GF2519_32Reflective.Common. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe2519_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe2519_32W (snd (fst (fst (fst x0123456789)))), - eta_fe2519_32W (snd (fst (fst x0123456789))), - eta_fe2519_32W (snd (fst x0123456789)), - eta_fe2519_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe2519_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe2519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe2519_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe2519_32W (snd (fst (fst (fst x0123456789)))), - eta_fe2519_32W (snd (fst (fst x0123456789))), - eta_fe2519_32W (snd (fst x0123456789)), - eta_fe2519_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe2519_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe2519_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*) diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v index c57fd6786..2221c9860 100644 --- a/src/SpecificGen/GF25519_32.v +++ b/src/SpecificGen/GF25519_32.v @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_32) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe25519_32 {T} (op : fe25519_32 -> T) := Eval compute in Tuple.uncurry (n:=length_fe25519_32) op. Definition curry_unop_fe25519_32 {T} op : fe25519_32 -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> fe25519_32 appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe25519_32 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T) - := Eval compute in uncurry_n_op_fe25519_32 10 op. -Definition curry_10op_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe25519_32) : { fg : fe25519_32 | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v index 43fc1be36..bf76e028b 100644 --- a/src/SpecificGen/GF25519_32BoundedCommon.v +++ b/src/SpecificGen/GF25519_32BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe25519_32W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_32W) := - app_fe25519_32W x0 (fun x0' => - app_fe25519_32W x1 (fun x1' => - app_fe25519_32W x2 (fun x2' => - app_fe25519_32W x3 (fun x3' => - app_fe25519_32W x4 (fun x4' => - app_fe25519_32W x5 (fun x5' => - app_fe25519_32W x6 (fun x6' => - app_fe25519_32W x7 (fun x7' => - app_fe25519_32W x8 (fun x8' => - app_fe25519_32W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe25519_32W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe25519_32W_sig (x : fe25519_32W) : { v : fe25519_32W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe25519_32W {T} op : fe25519_32W -> fe25519_32W -> fe25519_ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe25519_32W {T} (op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe25519_32W (fun x0 => - uncurry_unop_fe25519_32W (fun x1 => - uncurry_unop_fe25519_32W (fun x2 => - uncurry_unop_fe25519_32W (fun x3 => - uncurry_unop_fe25519_32W (fun x4 => - uncurry_unop_fe25519_32W (fun x5 => - uncurry_unop_fe25519_32W (fun x6 => - uncurry_unop_fe25519_32W (fun x7 => - uncurry_unop_fe25519_32W (fun x8 => - uncurry_unop_fe25519_32W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe25519_32W {T} op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T - := Eval cbv (*-[word64]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe25519_32W (x : fe25519_32) : fe25519_32W := Eval app_tuple_map in app_fe25519_32 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe25519_32WToZ x0) = true - -> is_bounded (fe25519_32WToZ x1) = true - -> is_bounded (fe25519_32WToZ x2) = true - -> is_bounded (fe25519_32WToZ x3) = true - -> is_bounded (fe25519_32WToZ x4) = true - -> is_bounded (fe25519_32WToZ x5) = true - -> is_bounded (fe25519_32WToZ x6) = true - -> is_bounded (fe25519_32WToZ x7) = true - -> is_bounded (fe25519_32WToZ x8) = true - -> is_bounded (fe25519_32WToZ x9) = true - -> (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8) (fe25519_32WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF25519_32.prefreeze. diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index b1dbbd976..aad67f032 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe25519_32 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4 := fun e => curry_9op_fe25519_32W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W - -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4 - := fun e => curry_10op_fe25519_32W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519_32 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_32 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe25519_32 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W * fe25519_32W) - (H0 : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe25519_32WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe25519_32WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe25519_32WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe25519_32WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W curry_10op_fe25519_32W - curry_binop_fe25519_32 curry_unop_fe25519_32 curry_unop_wire_digits curry_9op_fe25519_32 curry_10op_fe25519_32 - uncurry_binop_fe25519_32W uncurry_unop_fe25519_32W uncurry_unop_wire_digitsW uncurry_9op_fe25519_32W uncurry_10op_fe25519_32W - uncurry_binop_fe25519_32 uncurry_unop_fe25519_32 uncurry_unop_wire_digits uncurry_9op_fe25519_32 uncurry_10op_fe25519_32 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W + curry_binop_fe25519_32 curry_unop_fe25519_32 curry_unop_wire_digits curry_9op_fe25519_32 + uncurry_binop_fe25519_32W uncurry_unop_fe25519_32W uncurry_unop_wire_digitsW uncurry_9op_fe25519_32W + uncurry_binop_fe25519_32 uncurry_unop_fe25519_32 uncurry_unop_wire_digits uncurry_9op_fe25519_32 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe25519_32WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe25519_32WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe25519_32WToZ; simpl @wire_digitsWToZ; diff --git a/src/SpecificGen/GF25519_32Reflective/Common10_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common10_4Op.v deleted file mode 100644 index f94ed3446..000000000 --- a/src/SpecificGen/GF25519_32Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.SpecificGen.GF25519_32Reflective.Common. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe25519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe25519_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe25519_32W (snd (fst (fst (fst x0123456789)))), - eta_fe25519_32W (snd (fst (fst x0123456789))), - eta_fe25519_32W (snd (fst x0123456789)), - eta_fe25519_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe25519_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe25519_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe25519_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe25519_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe25519_32W (snd (fst (fst (fst x0123456789)))), - eta_fe25519_32W (snd (fst (fst x0123456789))), - eta_fe25519_32W (snd (fst x0123456789)), - eta_fe25519_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe25519_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe25519_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*) diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v index 80d679b73..6aa576fa4 100644 --- a/src/SpecificGen/GF25519_64.v +++ b/src/SpecificGen/GF25519_64.v @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_64) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe25519_64 {T} (op : fe25519_64 -> T) := Eval compute in Tuple.uncurry (n:=length_fe25519_64) op. Definition curry_unop_fe25519_64 {T} op : fe25519_64 -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> fe25519_64 appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe25519_64 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T) - := Eval compute in uncurry_n_op_fe25519_64 10 op. -Definition curry_10op_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe25519_64) : { fg : fe25519_64 | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v index 90a107f9c..b4c8e47ca 100644 --- a/src/SpecificGen/GF25519_64BoundedCommon.v +++ b/src/SpecificGen/GF25519_64BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe25519_64W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_64W) := - app_fe25519_64W x0 (fun x0' => - app_fe25519_64W x1 (fun x1' => - app_fe25519_64W x2 (fun x2' => - app_fe25519_64W x3 (fun x3' => - app_fe25519_64W x4 (fun x4' => - app_fe25519_64W x5 (fun x5' => - app_fe25519_64W x6 (fun x6' => - app_fe25519_64W x7 (fun x7' => - app_fe25519_64W x8 (fun x8' => - app_fe25519_64W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe25519_64W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe25519_64W_sig (x : fe25519_64W) : { v : fe25519_64W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> fe25519_ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe25519_64W {T} (op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T) - := Eval cbv (*-[word128]*) in - uncurry_unop_fe25519_64W (fun x0 => - uncurry_unop_fe25519_64W (fun x1 => - uncurry_unop_fe25519_64W (fun x2 => - uncurry_unop_fe25519_64W (fun x3 => - uncurry_unop_fe25519_64W (fun x4 => - uncurry_unop_fe25519_64W (fun x5 => - uncurry_unop_fe25519_64W (fun x6 => - uncurry_unop_fe25519_64W (fun x7 => - uncurry_unop_fe25519_64W (fun x8 => - uncurry_unop_fe25519_64W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T - := Eval cbv (*-[word128]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe25519_64W (x : fe25519_64) : fe25519_64W := Eval app_tuple_map in app_fe25519_64 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe25519_64WToZ x0) (fe25519_64WToZ x1) (fe25519_64WToZ x2) (fe25519_64WToZ x3) (fe25519_64WToZ x4) (fe25519_64WToZ x5) (fe25519_64WToZ x6) (fe25519_64WToZ x7) (fe25519_64WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_64WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe25519_64WToZ x0) = true - -> is_bounded (fe25519_64WToZ x1) = true - -> is_bounded (fe25519_64WToZ x2) = true - -> is_bounded (fe25519_64WToZ x3) = true - -> is_bounded (fe25519_64WToZ x4) = true - -> is_bounded (fe25519_64WToZ x5) = true - -> is_bounded (fe25519_64WToZ x6) = true - -> is_bounded (fe25519_64WToZ x7) = true - -> is_bounded (fe25519_64WToZ x8) = true - -> is_bounded (fe25519_64WToZ x9) = true - -> (Tuple.map (n:=k) fe25519_64WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe25519_64WToZ x0) (fe25519_64WToZ x1) (fe25519_64WToZ x2) (fe25519_64WToZ x3) (fe25519_64WToZ x4) (fe25519_64WToZ x5) (fe25519_64WToZ x6) (fe25519_64WToZ x7) (fe25519_64WToZ x8) (fe25519_64WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_64WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF25519_64.prefreeze. diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index eb90b67e5..f639aa0b6 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe25519_64 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4 := fun e => curry_9op_fe25519_64W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4 - := fun e => curry_10op_fe25519_64W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe25 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe25519_64 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519_64 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe25519_64 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W * fe25519_64W) - (H0 : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe25519_64WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe25519_64WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe25519_64WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe25519_64WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W curry_10op_fe25519_64W - curry_binop_fe25519_64 curry_unop_fe25519_64 curry_unop_wire_digits curry_9op_fe25519_64 curry_10op_fe25519_64 - uncurry_binop_fe25519_64W uncurry_unop_fe25519_64W uncurry_unop_wire_digitsW uncurry_9op_fe25519_64W uncurry_10op_fe25519_64W - uncurry_binop_fe25519_64 uncurry_unop_fe25519_64 uncurry_unop_wire_digits uncurry_9op_fe25519_64 uncurry_10op_fe25519_64 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W + curry_binop_fe25519_64 curry_unop_fe25519_64 curry_unop_wire_digits curry_9op_fe25519_64 + uncurry_binop_fe25519_64W uncurry_unop_fe25519_64W uncurry_unop_wire_digitsW uncurry_9op_fe25519_64W + uncurry_binop_fe25519_64 uncurry_unop_fe25519_64 uncurry_unop_wire_digits uncurry_9op_fe25519_64 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe25519_64WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe25519_64WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe25519_64WToZ; simpl @wire_digitsWToZ; diff --git a/src/SpecificGen/GF25519_64Reflective/Common10_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common10_4Op.v deleted file mode 100644 index 6c4fde676..000000000 --- a/src/SpecificGen/GF25519_64Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.SpecificGen.GF25519_64Reflective.Common. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe25519_64W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe25519_64W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe25519_64W (snd (fst (fst (fst x0123456789)))), - eta_fe25519_64W (snd (fst (fst x0123456789))), - eta_fe25519_64W (snd (fst x0123456789)), - eta_fe25519_64W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe25519_64WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe25519_64W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe25519_64W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe25519_64W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe25519_64W (snd (fst (fst (fst x0123456789)))), - eta_fe25519_64W (snd (fst (fst x0123456789))), - eta_fe25519_64W (snd (fst x0123456789)), - eta_fe25519_64W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe25519_64WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe25519_64WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.128s) (successful) *)*) diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v index d9d2a871c..6899f940e 100644 --- a/src/SpecificGen/GF41417_32.v +++ b/src/SpecificGen/GF41417_32.v @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe41417_32) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe41417_32 {T} (op : fe41417_32 -> T) := Eval compute in Tuple.uncurry (n:=length_fe41417_32) op. Definition curry_unop_fe41417_32 {T} op : fe41417_32 -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> fe41417_32 appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe41417_32 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T) - := Eval compute in uncurry_n_op_fe41417_32 10 op. -Definition curry_10op_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe41417_32) : { fg : fe41417_32 | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v index 15416433e..2bf69d425 100644 --- a/src/SpecificGen/GF41417_32BoundedCommon.v +++ b/src/SpecificGen/GF41417_32BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe41417_32W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe41417_32W) := - app_fe41417_32W x0 (fun x0' => - app_fe41417_32W x1 (fun x1' => - app_fe41417_32W x2 (fun x2' => - app_fe41417_32W x3 (fun x3' => - app_fe41417_32W x4 (fun x4' => - app_fe41417_32W x5 (fun x5' => - app_fe41417_32W x6 (fun x6' => - app_fe41417_32W x7 (fun x7' => - app_fe41417_32W x8 (fun x8' => - app_fe41417_32W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe41417_32W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe41417_32W_sig (x : fe41417_32W) : { v : fe41417_32W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe41417_32W {T} op : fe41417_32W -> fe41417_32W -> fe41417_ appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe41417_32W {T} (op : fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe41417_32W (fun x0 => - uncurry_unop_fe41417_32W (fun x1 => - uncurry_unop_fe41417_32W (fun x2 => - uncurry_unop_fe41417_32W (fun x3 => - uncurry_unop_fe41417_32W (fun x4 => - uncurry_unop_fe41417_32W (fun x5 => - uncurry_unop_fe41417_32W (fun x6 => - uncurry_unop_fe41417_32W (fun x7 => - uncurry_unop_fe41417_32W (fun x8 => - uncurry_unop_fe41417_32W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe41417_32W {T} op : fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> T - := Eval cbv (*-[word64]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe41417_32W (x : fe41417_32) : fe41417_32W := Eval app_tuple_map in app_fe41417_32 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe41417_32WToZ x0) (fe41417_32WToZ x1) (fe41417_32WToZ x2) (fe41417_32WToZ x3) (fe41417_32WToZ x4) (fe41417_32WToZ x5) (fe41417_32WToZ x6) (fe41417_32WToZ x7) (fe41417_32WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe41417_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe41417_32WToZ x0) = true - -> is_bounded (fe41417_32WToZ x1) = true - -> is_bounded (fe41417_32WToZ x2) = true - -> is_bounded (fe41417_32WToZ x3) = true - -> is_bounded (fe41417_32WToZ x4) = true - -> is_bounded (fe41417_32WToZ x5) = true - -> is_bounded (fe41417_32WToZ x6) = true - -> is_bounded (fe41417_32WToZ x7) = true - -> is_bounded (fe41417_32WToZ x8) = true - -> is_bounded (fe41417_32WToZ x9) = true - -> (Tuple.map (n:=k) fe41417_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe41417_32WToZ x0) (fe41417_32WToZ x1) (fe41417_32WToZ x2) (fe41417_32WToZ x3) (fe41417_32WToZ x4) (fe41417_32WToZ x5) (fe41417_32WToZ x6) (fe41417_32WToZ x7) (fe41417_32WToZ x8) (fe41417_32WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe41417_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF41417_32.prefreeze. diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v index e63c29ce3..62d55b463 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common.v +++ b/src/SpecificGen/GF41417_32Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe41417_32 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4 := fun e => curry_9op_fe41417_32W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W - -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4 - := fun e => curry_10op_fe41417_32W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe41 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe41417_32 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe41417_32 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe41417_32 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W * fe41417_32W) - (H0 : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe41417_32WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe41417_32WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe41417_32WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe41417_32WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W curry_10op_fe41417_32W - curry_binop_fe41417_32 curry_unop_fe41417_32 curry_unop_wire_digits curry_9op_fe41417_32 curry_10op_fe41417_32 - uncurry_binop_fe41417_32W uncurry_unop_fe41417_32W uncurry_unop_wire_digitsW uncurry_9op_fe41417_32W uncurry_10op_fe41417_32W - uncurry_binop_fe41417_32 uncurry_unop_fe41417_32 uncurry_unop_wire_digits uncurry_9op_fe41417_32 uncurry_10op_fe41417_32 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W + curry_binop_fe41417_32 curry_unop_fe41417_32 curry_unop_wire_digits curry_9op_fe41417_32 + uncurry_binop_fe41417_32W uncurry_unop_fe41417_32W uncurry_unop_wire_digitsW uncurry_9op_fe41417_32W + uncurry_binop_fe41417_32 uncurry_unop_fe41417_32 uncurry_unop_wire_digits uncurry_9op_fe41417_32 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe41417_32WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe41417_32WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe41417_32WToZ; simpl @wire_digitsWToZ; diff --git a/src/SpecificGen/GF41417_32Reflective/Common10_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common10_4Op.v deleted file mode 100644 index 46bb1211d..000000000 --- a/src/SpecificGen/GF41417_32Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.SpecificGen.GF41417_32Reflective.Common. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe41417_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe41417_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe41417_32W (snd (fst (fst (fst x0123456789)))), - eta_fe41417_32W (snd (fst (fst x0123456789))), - eta_fe41417_32W (snd (fst x0123456789)), - eta_fe41417_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe41417_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe41417_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe41417_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe41417_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe41417_32W (snd (fst (fst (fst x0123456789)))), - eta_fe41417_32W (snd (fst (fst x0123456789))), - eta_fe41417_32W (snd (fst x0123456789)), - eta_fe41417_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe41417_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe41417_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*) diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v index edc1bc979..6b9f360c8 100644 --- a/src/SpecificGen/GF5211_32.v +++ b/src/SpecificGen/GF5211_32.v @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe5211_32) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe5211_32 {T} (op : fe5211_32 -> T) := Eval compute in Tuple.uncurry (n:=length_fe5211_32) op. Definition curry_unop_fe5211_32 {T} op : fe5211_32 -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> fe5211_32 -> f appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe5211_32 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T) - := Eval compute in uncurry_n_op_fe5211_32 10 op. -Definition curry_10op_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe5211_32) : { fg : fe5211_32 | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v index 82c577dfa..20e8c84fd 100644 --- a/src/SpecificGen/GF5211_32BoundedCommon.v +++ b/src/SpecificGen/GF5211_32BoundedCommon.v @@ -206,26 +206,6 @@ Section generic_destructuring. intros. cbv [appify9]. repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity. Qed. - - Definition appify10 {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe5211_32W) := - app_fe5211_32W x0 (fun x0' => - app_fe5211_32W x1 (fun x1' => - app_fe5211_32W x2 (fun x2' => - app_fe5211_32W x3 (fun x3' => - app_fe5211_32W x4 (fun x4' => - app_fe5211_32W x5 (fun x5' => - app_fe5211_32W x6 (fun x6' => - app_fe5211_32W x7 (fun x7' => - app_fe5211_32W x8 (fun x8' => - app_fe5211_32W x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - - Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity. - Qed. End generic_destructuring. Definition eta_fe5211_32W_sig (x : fe5211_32W) : { v : fe5211_32W | v = x }. @@ -426,24 +406,6 @@ Definition curry_9op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe5211_32W {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T) - := Eval cbv (*-[word64]*) in - uncurry_unop_fe5211_32W (fun x0 => - uncurry_unop_fe5211_32W (fun x1 => - uncurry_unop_fe5211_32W (fun x2 => - uncurry_unop_fe5211_32W (fun x3 => - uncurry_unop_fe5211_32W (fun x4 => - uncurry_unop_fe5211_32W (fun x5 => - uncurry_unop_fe5211_32W (fun x6 => - uncurry_unop_fe5211_32W (fun x7 => - uncurry_unop_fe5211_32W (fun x8 => - uncurry_unop_fe5211_32W (fun x9 => - op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))). -Definition curry_10op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T - := Eval cbv (*-[word64]*) in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition proj1_fe5211_32W (x : fe5211_32) : fe5211_32W := Eval app_tuple_map in app_fe5211_32 x (HList.mapt (fun _ => (@proj_word _ _))). @@ -871,21 +833,5 @@ Notation i9top_correct_and_bounded k irop op = op (fe5211_32WToZ x0) (fe5211_32WToZ x1) (fe5211_32WToZ x2) (fe5211_32WToZ x3) (fe5211_32WToZ x4) (fe5211_32WToZ x5) (fe5211_32WToZ x6) (fe5211_32WToZ x7) (fe5211_32WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). -Notation i10top_correct_and_bounded k irop op - := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - is_bounded (fe5211_32WToZ x0) = true - -> is_bounded (fe5211_32WToZ x1) = true - -> is_bounded (fe5211_32WToZ x2) = true - -> is_bounded (fe5211_32WToZ x3) = true - -> is_bounded (fe5211_32WToZ x4) = true - -> is_bounded (fe5211_32WToZ x5) = true - -> is_bounded (fe5211_32WToZ x6) = true - -> is_bounded (fe5211_32WToZ x7) = true - -> is_bounded (fe5211_32WToZ x8) = true - -> is_bounded (fe5211_32WToZ x9) = true - -> (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) - = op (fe5211_32WToZ x0) (fe5211_32WToZ x1) (fe5211_32WToZ x2) (fe5211_32WToZ x3) (fe5211_32WToZ x4) (fe5211_32WToZ x5) (fe5211_32WToZ x6) (fe5211_32WToZ x7) (fe5211_32WToZ x8) (fe5211_32WToZ x9)) - * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) - (only parsing). Definition prefreeze := GF5211_32.prefreeze. diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v index 6ef9d3c9f..977710173 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common.v +++ b/src/SpecificGen/GF5211_32Reflective/Common.v @@ -55,7 +55,6 @@ Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe5211_32 pack). Defined. Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. -Definition Expr10_4OpT : type base_type := Eval compute in Expr_nm_OpT 10 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -73,7 +72,6 @@ Definition ExprBinOp : Type := Expr ExprBinOpT. Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. -Definition Expr10_4Op : Type := Expr Expr10_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. @@ -84,7 +82,6 @@ Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_t 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 expr10_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr10_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. @@ -140,8 +137,6 @@ Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_ := Eval compute in Expr_nm_Op_bounds 4 1. Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type := Eval compute in Expr_nm_Op_bounds 9 4. -Definition Expr10Op_bounds : interp_all_binders_for Expr10_4OpT ZBounds.interp_base_type - := Eval compute in Expr_nm_Op_bounds 10 4. Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. @@ -167,19 +162,6 @@ Definition interp_9_4expr : Expr9_4Op -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4 := fun e => curry_9op_fe5211_32W (Interp (@WordW.interp_op) e). -Definition interp_10_4expr : Expr10_4Op - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W - -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4 - := fun e => curry_10op_fe5211_32W (Interp (@WordW.interp_op) e). Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). @@ -193,8 +175,6 @@ Notation unop_WireToFE_correct_and_bounded rop op := (iunop_WireToFE_correct_and_bounded (interp_uexpr_WireToFE rop) op) (only parsing). Notation op9_4_correct_and_bounded rop op := (i9top_correct_and_bounded 4 (interp_9_4expr rop) op) (only parsing). -Notation op10_4_correct_and_bounded rop op - := (i10top_correct_and_bounded 4 (interp_10_4expr rop) op) (only parsing). Ltac rexpr_cbv := lazymatch goal with @@ -220,7 +200,6 @@ Notation rexpr_unop_FEToZ_sig op := (rexpr_sig ExprUnOpFEToZT (uncurry_unop_fe52 Notation rexpr_unop_FEToWire_sig op := (rexpr_sig ExprUnOpFEToWireT (uncurry_unop_fe5211_32 op)) (only parsing). Notation rexpr_unop_WireToFE_sig op := (rexpr_sig ExprUnOpWireToFET (uncurry_unop_wire_digits op)) (only parsing). Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe5211_32 op)) (only parsing). -Notation rexpr_10_4op_sig op := (rexpr_sig Expr10_4OpT (uncurry_10op_fe5211_32 op)) (only parsing). Notation correct_and_bounded_genT ropW'v ropZ_sigv := (let ropW' := ropW'v in @@ -415,31 +394,6 @@ Proof. let v := app_tuples (unop_args_to_bounded _ H0) v in exact v. Defined. -Definition op10_args_to_bounded (x : fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W * fe5211_32W) - (H0 : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H1 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x)))))))))) = true) - (H2 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x))))))))) = true) - (H3 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x)))))))) = true) - (H4 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x))))))) = true) - (H5 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x)))))) = true) - (H6 : is_bounded (fe5211_32WToZ (snd (fst (fst (fst x))))) = true) - (H7 : is_bounded (fe5211_32WToZ (snd (fst (fst x)))) = true) - (H8 : is_bounded (fe5211_32WToZ (snd (fst x))) = true) - (H9 : is_bounded (fe5211_32WToZ (snd x)) = true) - : interp_flat_type (fun _ => BoundedWordW.BoundedWord) (all_binders_for Expr10_4OpT). -Proof. - let v := constr:(unop_args_to_bounded _ H9) in - let v := app_tuples (unop_args_to_bounded _ H8) v in - let v := app_tuples (unop_args_to_bounded _ H7) v in - let v := app_tuples (unop_args_to_bounded _ H6) v in - let v := app_tuples (unop_args_to_bounded _ H5) v in - let v := app_tuples (unop_args_to_bounded _ H4) v in - let v := app_tuples (unop_args_to_bounded _ H3) v in - let v := app_tuples (unop_args_to_bounded _ H2) v in - let v := app_tuples (unop_args_to_bounded _ H1) v in - let v := app_tuples (unop_args_to_bounded _ H0) v in - exact v. -Defined. Local Ltac make_bounds_prop bounds orig_bounds := let bounds' := fresh "bounds'" in @@ -477,8 +431,6 @@ Proof. 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 op10_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr10_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 := fun x @@ -517,12 +469,12 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Hbounds1 := fresh "Hbounds1" in let Hbounds2 := fresh "Hbounds2" in pose proof (proj2_sig ropZ_sig) as Heq; - cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr interp_10_4expr - curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W curry_10op_fe5211_32W - curry_binop_fe5211_32 curry_unop_fe5211_32 curry_unop_wire_digits curry_9op_fe5211_32 curry_10op_fe5211_32 - uncurry_binop_fe5211_32W uncurry_unop_fe5211_32W uncurry_unop_wire_digitsW uncurry_9op_fe5211_32W uncurry_10op_fe5211_32W - uncurry_binop_fe5211_32 uncurry_unop_fe5211_32 uncurry_unop_wire_digits uncurry_9op_fe5211_32 uncurry_10op_fe5211_32 - ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr10_4OpT Expr4OpT + cbv [interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W + curry_binop_fe5211_32 curry_unop_fe5211_32 curry_unop_wire_digits curry_9op_fe5211_32 + uncurry_binop_fe5211_32W uncurry_unop_fe5211_32W uncurry_unop_wire_digitsW uncurry_9op_fe5211_32W + uncurry_binop_fe5211_32 uncurry_unop_fe5211_32 uncurry_unop_wire_digits uncurry_9op_fe5211_32 + ExprBinOpT ExprUnOpFEToWireT ExprUnOpT ExprUnOpFEToZT ExprUnOpWireToFET Expr9_4OpT Expr4OpT interp_type_gen_rel_pointwise interp_type_gen_rel_pointwise] in *; cbv zeta in *; simpl @fe5211_32WToZ; simpl @wire_digitsWToZ; @@ -553,7 +505,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := end; repeat match goal with x := _ |- _ => subst x end; cbv [id - binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded op10_args_to_bounded + binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right; lazymatch goal with | [ |- fe5211_32WToZ ?x = _ /\ _ ] @@ -571,8 +523,8 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good op10_4_bounds_good - ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr10Op_bounds Expr4Op_bounds] in H1; + binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good + ExprUnOp_bounds ExprBinOp_bounds ExprUnOpFEToWire_bounds ExprUnOpFEToZ_bounds ExprUnOpWireToFE_bounds Expr9Op_bounds Expr4Op_bounds] in H1; destruct_head' ZBounds.bounds; unfold_is_bounded_in H1; simpl @fe5211_32WToZ; simpl @wire_digitsWToZ; diff --git a/src/SpecificGen/GF5211_32Reflective/Common10_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common10_4Op.v deleted file mode 100644 index c595470e9..000000000 --- a/src/SpecificGen/GF5211_32Reflective/Common10_4Op.v +++ /dev/null @@ -1,115 +0,0 @@ -Require Export Crypto.SpecificGen.GF5211_32Reflective.Common. -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. -Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing). -Lemma Expr10_4Op_correct_and_bounded - ropW op (ropZ_sig : rexpr_10_4op_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x0123456789 - (x0123456789 - := (eta_fe5211_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe5211_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe5211_32W (snd (fst (fst (fst x0123456789)))), - eta_fe5211_32W (snd (fst (fst x0123456789))), - eta_fe5211_32W (snd (fst x0123456789)), - eta_fe5211_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe5211_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x0123456789 - (x0123456789 - := (eta_fe5211_32W (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst x0123456789))))))), - eta_fe5211_32W (snd (fst (fst (fst (fst (fst x0123456789)))))), - eta_fe5211_32W (snd (fst (fst (fst (fst x0123456789))))), - eta_fe5211_32W (snd (fst (fst (fst x0123456789)))), - eta_fe5211_32W (snd (fst (fst x0123456789))), - eta_fe5211_32W (snd (fst x0123456789)), - eta_fe5211_32W (snd x0123456789))) - (Hx0123456789 - : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst (fst x0123456789)))))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x0123456789))))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x0123456789)))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x0123456789))))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x0123456789)))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst x0123456789))))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst (fst x0123456789)))) = true - /\ is_bounded (fe5211_32WToZ (snd (fst x0123456789))) = true - /\ is_bounded (fe5211_32WToZ (snd x0123456789)) = true), - let (Hx0, Hx123456789) := (eta_and Hx0123456789) in - let (Hx1, Hx23456789) := (eta_and Hx123456789) in - let (Hx2, Hx3456789) := (eta_and Hx23456789) in - let (Hx3, Hx456789) := (eta_and Hx3456789) in - let (Hx4, Hx56789) := (eta_and Hx456789) in - let (Hx5, Hx6789) := (eta_and Hx56789) in - let (Hx6, Hx789) := (eta_and Hx6789) in - let (Hx7, Hx89) := (eta_and Hx789) in - let (Hx8, Hx9) := (eta_and Hx89) in - let args := op10_args_to_bounded x0123456789 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9 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'))) - with - | Some bounds => op10_4_bounds_good bounds = true - | None => False - end) - : op10_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. - intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9. - pose x0 as x0'. - pose x1 as x1'. - pose x2 as x2'. - pose x3 as x3'. - pose x4 as x4'. - pose x5 as x5'. - pose x6 as x6'. - pose x7 as x7'. - pose x8 as x8'. - pose x9 as x9'. - hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8, x9; destruct_head' prod. - specialize (H0 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') - (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 (conj Hx8 Hx9)))))))))). - Time let args := constr:(op10_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8', x9') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 Hx9) in - admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *) -Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*) diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4 index 5d3b9c263..a9d6c574f 100644 --- a/src/SpecificGen/GFtemplate3mod4 +++ b/src/SpecificGen/GFtemplate3mod4 @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe{{{k}}}{{{c}}}_{{{w}}}) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T) := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op. Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 10 op. -Definition curry_10op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}. Proof. diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8 index 579be07bf..c0ad5a630 100644 --- a/src/SpecificGen/GFtemplate5mod8 +++ b/src/SpecificGen/GFtemplate5mod8 @@ -196,26 +196,6 @@ Proof. repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. Qed. -Definition appify10 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe{{{k}}}{{{c}}}_{{{w}}}) := - app_n x0 (fun x0' => - app_n x1 (fun x1' => - app_n x2 (fun x2' => - app_n x3 (fun x3' => - app_n x4 (fun x4' => - app_n x5 (fun x5' => - app_n x6 (fun x6' => - app_n x7 (fun x7' => - app_n x8 (fun x8' => - app_n x9 (fun x9' => - op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))). - -Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, - @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9. -Proof. - intros. cbv [appify10]. - repeat (etransitivity; [ apply app_n_correct | ]); reflexivity. -Qed. - Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T) := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op. Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T @@ -249,13 +229,6 @@ Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8). -Definition uncurry_10op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) - := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 10 op. -Definition curry_10op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T - := Eval compute in - appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 - => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9). - Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}. Proof. diff --git a/src/Util/Tower.v b/src/Util/Tower.v index f2709ef75..7f6bca59d 100644 --- a/src/Util/Tower.v +++ b/src/Util/Tower.v @@ -55,20 +55,3 @@ Definition apply9_nd {BK PA PB ARR} : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B))))))))) := @apply9 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) tt tt tt tt tt tt tt tt tt B f. - -Definition apply10 {AK BK PA PB ARR} - (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B)) - {A0 A1 A2 A3 A4 A5 A6 A7 A8 A9 : AK} {B : BK} - (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PA A4 -> PA A5 -> PA A6 -> PA A7 -> PA A8 -> PA A9 -> PB B) - : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 (ARR A4 (ARR A5 (ARR A6 (ARR A7 (ARR A8 (ARR A9 B)))))))))). -Proof. - repeat (apply F; intro); apply f; assumption. -Defined. - -Definition apply10_nd {BK PA PB ARR} - (F : forall (B : BK), (PA -> PB B) -> PB (ARR B)) - {B : BK} - (f : tower_nd PA (PB B) 10) - : PB (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR (ARR B)))))))))) - := @apply10 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F) - tt tt tt tt tt tt tt tt tt tt B f. |