Further proof optimization

[JoaoDiogoDuarte]

This PR optimizes the runtime of the proof in the following ways:

1. Removed unused lemmas and dependencies.
2. Improved invert op proof in Curve25519_Operations.ec
3. Symlinked the ref4 correctness proof to the mulx repository and use transitivity for the mulx proofs whose related procedures contain the exact same code as they originate from the common subfolder in src.

As an example of point 3 conditional swapping is done exactly the same in mulx and ref4, so instead of proving the lemma directly in both the mulx and ref4 proofs, we prove it for ref4 and use transitivity for the mulx proof.

This last point also allows for better management of code shared between repositories.

This is a draft as I resolve merge issues.

[tfaoliveira-sb]

Cool!

Can you take a look into:

$ cat formosa-25519/proof/crypto_scalarmult/curve25519/amd64/mulx/.ci/CorrectnessProof.ec.out.error
1
[critical] [: line 1 (0) to line 3 (112)] In external theory CorrectnessProofRef4 [: line 1 (0) to line 3 (73)]:

cannot locate theory `Ref4_scalarmult_s

Maybe files/links/extraction names need to be arranged differently.

[JoaoDiogoDuarte]

Should be fixed! I did this by removing symlinks and added -R crypto_scalarmult/ to the Easycrypt command in the proof Makefile along with some little tweaks.