Add the dettman square operation

[OwenConoly]

Turns out that the squaring algorithm is essentially identical to the multiplication algorithm. To transform the mul function into the square function, I just had to replace Associational.mul with Associational.square.

[OwenConoly]

I benchmarked the generated C implementation for square using the tools in https://github.com/bitcoin-core/secp256k1/. It's significantly faster than the mul operation, which is reassuring. I wasn't able to discern a significant difference between the performance of the generated C implementation vs. that of the handwritten assembly version.

[JasonGross]

Looks good! Here are a couple suggestions that I think will make the organization slightly cleaner

[JasonGross]

What's up with the

fatal: detected dubious ownership in repository at '/github/workspace/rewriter'
To add an exception for this directory, call:

	git config --global --add safe.directory /github/workspace/rewriter

errors? (Does the branch just need to be rebased, or is something bigger going on?)

[OwenConoly]

I don't know what could've caused that.

[JasonGross]

Seems to be failing on master now? https://github.com/mit-plv/fiat-crypto/actions/workflows/docker-coq.yml?query=branch%3Amaster

[JasonGross]

I've asked about this at https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/docker.20dev.2Fmaster.20change.3F