From a002e5043eed1dcf4203386262f69d03334e80e6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 5 Nov 2016 23:43:18 -0400 Subject: Add better bounded lemmas to reified things --- src/Specific/GF25519Reflective/Reified/CarrySub.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Specific/GF25519Reflective/Reified/CarrySub.v') diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v index b09960a18..3acfb1f45 100644 --- a/src/Specific/GF25519Reflective/Reified/CarrySub.v +++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v @@ -5,6 +5,11 @@ Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig. Lemma rcarry_subW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_subW rcarry_subZ_sig. Proof. rexpr_correct. Qed. Definition rcarry_sub_output_bounds := Eval vm_compute in compute_bounds rcarry_subW ExprBinOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rcarry_subW_correct_and_bounded + := ExprBinOp_correct_and_bounded + rcarry_subW carry_sub rcarry_subZ_sig rcarry_subW_correct_and_bounded_gen + _ _. Local Open Scope string_scope. Compute ("Carry_Sub", compute_bounds_for_display rcarry_subW ExprBinOp_bounds). -- cgit v1.2.3