From 75132de934cad936b68158ca1b49b066ff3f75c4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 18:56:31 -0500 Subject: Start work on a faster version of GF*Reflective/Common* --- src/Specific/GF25519Reflective/Common.v | 78 +++++++++++++++++++++------------ 1 file changed, 51 insertions(+), 27 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index daf036bc2..c00223c96 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe25519 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe25519 carry_opp). Defined. +Definition fe25519T : flat_type base_type. +Proof. + let T := (eval compute in GF25519.fe25519) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe25519T] in + Syntax.tuple fe25519T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe25519T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe25519 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe25519 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF25519.fe25519) - (@uncurry_unop_fe25519)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF25519.fe25519 4) - (@uncurry_unop_fe25519)) with - | _ -> ?T => T - end in - make_type_from' T. -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 ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition 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 exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. @@ -584,3 +607,4 @@ Module Export PrettyPrinting. Notation sanity_check opW bounds := (eq_refl (sanity_compute opW bounds) <: no = no) (only parsing). End PrettyPrinting. +G -- cgit v1.2.3