From 2541a1d606b9ee93beedb964f6b2c0968b15e926 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 22 Nov 2016 17:00:02 -0500 Subject: More GF25519ReflectiveCommon generalization --- src/Specific/GF25519Reflective/Common.v | 46 ++++++++++++++------------------- 1 file changed, 20 insertions(+), 26 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index f47b9f298..e8ad44494 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls := constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) end. -Local Ltac make_bounds_cps ls := +Local Ltac make_bounds_cps ls extra := let v := bounds_from_list_cps (List.rev ls) in let v := (eval compute in v) in - pose v. + exact (v _ extra). Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with @@ -116,36 +116,30 @@ 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. +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 - _ + | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in + interp_all_binders_for_of' _ 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. -Proof. make_bounds (Tuple.to_list _ bounds). Defined. -Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type. -Proof. make_bounds (Tuple.to_list _ bounds). Defined. -Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type. -Proof. make_bounds (Tuple.to_list _ bounds). Defined. + make_bounds_cps (Tuple.to_list _ bounds) v. +Defined. +Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type + := Eval compute in Expr_nm_Op_bounds 2 1. +Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type + := Eval compute in Expr_nm_Op_bounds 1 1. +Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type + := Eval compute in Expr_nm_Op_bounds 1 1. +Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type + := Eval compute in Expr_nm_Op_bounds 1 1. +Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type + := 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 ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. -Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type. -Proof. - make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)). -Defined. -Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type. -Proof. - make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)). -Defined. + Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W := fun e => curry_binop_fe25519W (Interp (@WordW.interp_op) e). Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -- cgit v1.2.3