diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-16 13:31:40 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-16 19:00:06 -0400 |
| commit | 1ea69cd53ff8472bb23c338d0e3fcac0a1f9ada5 (patch) | |
| tree | 14379b1df13a789daf454f29324661ebb85c9f0c /src/Util/WordUtil.v | |
| parent | 7d139ded819549c587b169e6ef54d411bc543cd4 (diff) | |
Derive EdDSA.verify from equational specification
Experiments/SpecEd25519 will come back soon
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 6a8831b14..9e88c1731 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -59,3 +59,7 @@ Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with | eq_refl => w end)); abstract omega. Defined. + +Lemma combine_eq_iff {a b} (A:word a) (B:word b) C : + combine A B = C <-> A = split1 a b C /\ B = split2 a b C. +Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed. |