Evaluate HACL-rs bignums

[tarcieri]

From #577 (comment):

HACL* extracted as pure safe Rust (dubbed "HACL-rs") lives here: https://github.com/hacl-star/hacl-star/tree/afromher_rs/dist/rs

In there, you'll find bignums in src/hacl:

• bignum.rs, bignum64.rs: variable-length, 32 and 64-bit versions (scattered across these two files, this needs to be done better)
• bignum{4096,256}.rs: fixed-length, 32-bit limbs
• bignum{4096,256}_64.rs: fixed-length, 64-bit limbs

cc @protz @spitters