From 55a5bd4872f1f53740b9ae5650b5d591ce1df530 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 20 Oct 2016 18:20:14 -0400 Subject: A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstantiation --- src/Assembly/GF25519BoundedInstantiation.v | 46 ++++++++++++++++++++++++++---- 1 file changed, 41 insertions(+), 5 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v index e17e20386..b3c38fd69 100644 --- a/src/Assembly/GF25519BoundedInstantiation.v +++ b/src/Assembly/GF25519BoundedInstantiation.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Assembly.GF25519. Require Import Crypto.Specific.GF25519. Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Tuple. (* Totally fine to edit these definitions; DO NOT change the type signatures at all *) @@ -24,8 +25,43 @@ Local Notation binop_correct_and_bounded rop op Local Notation unop_correct_and_bounded rop op := (iunop_correct_and_bounded (interp_uexpr rop) op) (only parsing). -Axiom radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. -Axiom rsub_correct_and_bounded : binop_correct_and_bounded rsub carry_sub. -Axiom rmul_correct_and_bounded : binop_correct_and_bounded rmul mul. -Axiom ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp. -Axiom rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze. +Local Ltac start_correct_and_bounded_t op op_expr lem := + intros; hnf in *; destruct_head' prod; simpl in * |- ; + repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end; + change op with op_expr; + rewrite <- lem. + +Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. +Proof. + start_correct_and_bounded_t + carry_add GF25519.AddExpr.ge25519_add_expr + (fun x y => proj2_sig (GF25519.AddExpr.ge25519_add' x y)). + simpl @fe25519WToZ. +Admitted. +Lemma rsub_correct_and_bounded : binop_correct_and_bounded rsub carry_sub. +Proof. + start_correct_and_bounded_t + carry_sub GF25519.SubExpr.ge25519_sub_expr + (fun x y => proj2_sig (GF25519.SubExpr.ge25519_sub' x y)). + simpl @fe25519WToZ. +Admitted. +Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul. +Proof. + start_correct_and_bounded_t + Specific.GF25519.mul GF25519.MulExpr.ge25519_mul_expr + (fun x y => proj2_sig (GF25519.MulExpr.ge25519_mul' x y)). + simpl @fe25519WToZ. +Admitted. +Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp. +Proof. + start_correct_and_bounded_t + carry_opp GF25519.OppExpr.ge25519_opp_expr + (fun x => proj2_sig (GF25519.OppExpr.ge25519_opp' x)). + simpl @fe25519WToZ. +Admitted. +Lemma rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze. +Proof. + intros; hnf in *; destruct_head' prod; simpl in * |- ; + repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end. + simpl @fe25519WToZ. +Admitted. -- cgit v1.2.3