diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-05 23:43:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-05 23:43:18 -0400 |
| commit | a002e5043eed1dcf4203386262f69d03334e80e6 (patch) | |
| tree | ab8bca912e93026e90e2e1b466e1854da2b6478f /src/Specific/GF25519Reflective/Reified/CarrySub.v | |
| parent | 44f75506d2155e3e08d0cb7f81214dd6d5e5ee34 (diff) | |
Add better bounded lemmas to reified things
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified/CarrySub.v')
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarrySub.v | 5 |
1 files changed, 5 insertions, 0 deletions
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). |