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 126 forks source link

Don't store widths of words twice #1740

Closed yav closed 2 months ago

yav commented 2 months ago

The cryptol value for words stored the length of the word and a WordValue:

https://github.com/GaloisInc/cryptol/blob/09853251186d4590f3b093dbdf2b324c9a7e6ca0/src/Cryptol/Eval/Value.hs#L127

But the WordValue also stored the length of the word:

https://github.com/GaloisInc/cryptol/blob/09853251186d4590f3b093dbdf2b324c9a7e6ca0/src/Cryptol/Backend/WordValue.hs#L91

The only case that does not have an explicit value is the WordVal which uses the type family SWord to pick a type based on representation.

In the Concrete backend this value is BV https://github.com/GaloisInc/cryptol/blob/09853251186d4590f3b093dbdf2b324c9a7e6ca0/src/Cryptol/Backend/Concrete.hs#L135

which also has a length:

https://github.com/GaloisInc/cryptol/blob/09853251186d4590f3b093dbdf2b324c9a7e6ca0/src/Cryptol/Backend/Concrete.hs#L57

In fact, any instance of SWord must store its length, because the backend contains this method:

https://github.com/GaloisInc/cryptol/blob/09853251186d4590f3b093dbdf2b324c9a7e6ca0/src/Cryptol/Backend.hs#L298

I think we can remove the length from VWord and just get it from teh WordValue.