diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 23:01:53 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 23:02:19 -0400 |
| commit | d7670f26f566a94e989a10fda2c45ff6c369aae9 (patch) | |
| tree | 04e763b91ca5b1b4d058bc27506acc9d4f98ebd3 /src/Specific/GF25519Reflective/Reified/Sub.v | |
| parent | 80d0cf475af29fc011da4415967a460a32cafb73 (diff) | |
Also construct relatedness proofs in reified
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified/Sub.v')
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Sub.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v index 2695da171..7a498179e 100644 --- a/src/Specific/GF25519Reflective/Reified/Sub.v +++ b/src/Specific/GF25519Reflective/Reified/Sub.v @@ -1,3 +1,6 @@ Require Import Crypto.Specific.GF25519Reflective.Common. Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined. +Definition rsubW := Eval vm_compute in rword_of_Z rsubZ_sig. +Lemma rsubW_correct_and_bounded_gen : correct_and_bounded_genT rsubW rsubZ_sig. +Proof. rexpr_correct. Qed. |