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

Factor out reusable libraries from simulator backends #651

Open brianhuffman opened 4 years ago

brianhuffman commented 4 years ago

This ticket is based on #37. Instead of trying to use the same symbolic simulator for cryptol and saw-core, we should try to share code for some pieces of each. In particular, we should consider making a library for the implementation of the cryptol sequence type. The goal of this refactoring would be to have the saw-core symbolic simulator be able to reuse some of the same libraries.

brianhuffman commented 3 years ago

Maybe it would be nice for the saw-core simulator to use Cryptol's Backend class. We should have a close look at how Backend is defined to see if this would work.

robdockins commented 3 years ago

After taking a quick look a this, I think there wouldn't be too much work to do so we could align the set of primitives in SAWCore with those in Cryptol. As a bonus, SAWCore would automatically get the benefit of the safety predicate and definitional equation features we added to the Cryptol evaluator, as well as immediately usable definitions of all the integer, Z n and rational operations.