diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-28 14:18:08 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-28 14:18:08 -0400 |
| commit | 238301431d29005f010466c48c330777a897cb3f (patch) | |
| tree | c6a33dafc8d165147ec36a49cd11800212b9efab /src | |
| parent | c27dbaa5bfb8346e7484e07e551cf13ed745740b (diff) | |
EdDSARefinement: work around rewrite_strat for 8.4
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/EdDSARefinement.v | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v index c8de64895..79c9b05dd 100644 --- a/src/Experiments/EdDSARefinement.v +++ b/src/Experiments/EdDSARefinement.v @@ -108,24 +108,21 @@ Section EdDSA. {SdecS} {SdecS_correct : forall w, (decS w) = (SdecS w)} (* FIXME: equivalence relation *) {natToS_modl : forall n, Seq (natToS (n mod l)) (natToS n)}. - Create HintDb hintsEtoA discriminated. - Hint Rewrite - Aenc_correct - homomorphism - homomorphism_id - homomorphism_inv - SAmul_correct - SdecS_correct - natToS_modl - : hintsEtoA. - Definition verify_using_representation {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : { answer | answer = verify message pk sig }. Proof. eexists. cbv [verify]. - (rewrite_strat topdown hints hintsEtoA). + repeat ( + setoid_rewrite Aenc_correct + || setoid_rewrite homomorphism + || setoid_rewrite homomorphism_id + || setoid_rewrite (homomorphism_inv(INV:=Eopp)(inv:=Aopp)(eq:=Aeq)(phi:=EtoA)) + || setoid_rewrite SAmul_correct + || setoid_rewrite SdecS_correct + || setoid_rewrite natToS_modl + ). reflexivity. Defined. End ChangeRep. |