diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-21 16:29:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-21 16:29:29 -0400 |
| commit | 448e38eac815b0dce1b59d11011a65d1898deeaa (patch) | |
| tree | 563089ce3ce10702fdbab20e88a52e0fe6b05109 /src/Specific/GF25519.v | |
| parent | 1422c9d382d2e37ef7f7f5cb7e92212a887db92c (diff) | |
Sane fieldwiseb
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 446e7fba2..42797c1a1 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -528,11 +528,19 @@ Proof. Defined. Definition fieldwiseb (f g : fe25519) : bool - := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in proj1_sig (fieldwiseb_sig f g). + := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in + proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) + (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Definition fieldwiseb_correct (f g : fe25519) - : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g - := Eval cbv beta iota delta [proj2_sig fieldwiseb_sig] in proj2_sig (fieldwiseb_sig f g). +Lemma fieldwiseb_correct (f g : fe25519) + : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g. +Proof. + set (f' := f); set (g' := g). + hnf in f, g; destruct_head' prod. + exact (proj2_sig (fieldwiseb_sig f' g')). +Qed. Definition eqb_sig (f g : fe25519) : { b | b = eqb f g }. |