search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
439 stars 63 forks source link

Unimplemented `IntMod` SAWCore operators #1912

Open WeeknightMVP opened 1 year ago

WeeknightMVP commented 1 year ago

While attempting to use SAW to verify the correctness of a Cryptol property that uses prime modular integer fields (prime p => Z p), SAW's translation of the property to SAWCore included the assignment x@... = error x@... "Unimplemented: recip IntMod", indicating that IntMod operator recip is currently unimplemented.

RyanGlScott commented 1 year ago

Indeed, this would be nice to have. Currently, all of the IntMod operations are implemented as SAWCore primitives, such as the ones here:

https://github.com/GaloisInc/saw-script/blob/e0604caf6bf10f4aab4f21578e1fe2fa43e4d60a/saw-core/prelude/Prelude.sawcore#L1629-L1633

At first blush, adding recip support for IntMod would mean adding a new intModRecip primitive and giving it appropriate semantics in each of the SAW simulator backends. This might not be entirely as straightforward to do for recip as the other IntMod primitives, since some of the backends (e.g., What4) lack direct counterparts to Cryptol's recip function.

There is also the question about how to translate recip over IntMods in the Coq translation. I image that ZModulo in the Coq standard library would give us the tools we need to implement a version of recip in Coq, but I haven't looked deeply at it.