search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

Mechanism for primitives with reference implementations (starting with pmod) #922

Open atomb opened 3 years ago

atomb commented 3 years ago

The pmod operation is one of many examples that can easily be defined in Cryptol but could benefit from being a special case (especially for performance during concrete execution).

It would be useful to add support for such functions. They'd include Cryptol definitions that could be used in any case where special treatment isn't useful (such as in symbolic reasoning backends) but could be treated as if they were primitives when useful (such as for concrete execution).

This would also be beneficial for some of the new crypto primitives.

robdockins commented 3 years ago

This is now down for polynomial arithmetic.

robdockins commented 3 years ago

There are still some questions to be answered about how to handle the SuiteB and PrimeEC primitives, but I don't think we will get to answering those in time for 2.10.