Architecture independent P256 functions

[miriampolzer]

The P256 code we wrote so far is hardcoded 64 bits. The C code itself is already free of any dependencies on the architecture, but the specs and proofs are not. We should wrap them in contexts for word.

[miriampolzer]

While working on this I ended up refactoring the word instances a bit, I will link the respective chain of PRs here.

Coqutil: mit-plv/coqutil#179
riscv-coq: mit-plv/riscv-coq#52
Bedrock2: mit-plv/bedrock2#551
Rupicola: mit-plv/rupicola#219
Fiat-Crypto: #2382

After those are merged through, I will update the P256 proofs to be architecture independent where necessary.

[miriampolzer]

All except fiat-crypto are in, and when I tried the bump + merge today I noticed some proof failures. I will investigate and resolve this. Until then, an automatic rupicola bump that would come in on Monday would fail.