jadephilipoom
jadephilipoom
The code in `Bedrock/Tests/` is maturing into less of a one-off sanity check and more of a suite of examples. For that purpose, it should be a lot less sloppy...
Now that the `Language` API exists, `Fancy/Compiler.v` should use `API.expr` instead of defining its own `cexpr` notation.
This PR allows the bedrock2 backend for fiat-crypto to interpret add-carry and sub-borrow instructions by calling external bedrock2 functions. I changed the arguments to the fiat-crypto pipeline so that it...
This backwards-incompatible change is part of the changes between the round 3 SPHINCS+ submission to the NIST PQC competition and the SLH-DSA draft standard. Part of https://github.com/lowRISC/opentitan/issues/21944 Corresponds to this...
Currently it's represented by `nat`, which is the theoretical-mathematics version of a natural number, but it would be better to use `N`, the binary version, since we're never doing mathematical...
As per discussion in #36 In several Coq lemmas I use `a` as the name for function arguments that have address types. I should go through, find these places, and...
This RFC recommends a general strategy for accelerating post-quantum cryptography (PQC) on OTBN, namely: - Increase OTBN’s instruction and data memory. - We will likely need at least 12kB each,...
See https://github.com/lowRISC/opentitan/pull/9811#discussion_r778171126 for context. In order to have a default set of test vectors for RSA that can be run without any additional steps, there's an autogenerated test vector file...
### Description Right now, the cryptolib API headers under `sw/device/lib/crypto/include` contain a bunch of copy-pasted comments like this: https://github.com/lowRISC/opentitan/blob/a47262e648ba973f6e0b2d8ce33f59bf57b4ae04/sw/device/lib/crypto/include/ecc.h#L89-L96 However, this advice is outdated; hardware-backed keys now do need to...
### Description Within the OTBN code for attestation certificate endorsements, run `verify` right after `sign` as an FI mitigation. If the verify doesn't pass, lock OTBN so the attacker can't...