diff options
| -rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 4 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 19 |
2 files changed, 22 insertions, 1 deletions
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index 6e2213ee7..931e67ede 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -25,6 +25,10 @@ Definition word64 := Word.word 64. Coercion word64ToZ (x : word64) : Z := Z.of_N (wordToN x). Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x). +Definition w64eqb (x y : word64) := weqb x y. + +Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y. +Proof. apply wordeqb_Zeqb. Qed. (* END aliases for word extraction *) diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index a89d02364..f2ceb047f 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -140,4 +140,21 @@ Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) Admitted. Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a). -Admitted.
\ No newline at end of file +Admitted. + +Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y. +Proof. + match goal with |- ?LHS = ?RHS => destruct LHS eqn:HL, RHS eqn:HR end; + repeat match goal with + | _ => reflexivity + | _ => progress unfold not in * + | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H + | [ |- Z.eqb _ _ = true ] => apply Z.eqb_eq + | [ H : context[Z.of_N _ = Z.of_N _] |- _ ] => rewrite N2Z.inj_iff in H + | [ H : wordToN _ = wordToN _ |- _ ] => apply wordToN_inj in H + | [ H : x = y :> word _ |- _ ] => apply weqb_true_iff in H + | [ H : ?x = false |- _ ] => progress rewrite <- H; clear H + | _ => congruence + | [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst + end. +Qed. |