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

Fix `splitV` when splitting empty sequence to type `[inf][0]` #1750

Closed RyanGlScott closed 2 weeks ago

RyanGlScott commented 3 weeks ago

Previously, splitV would assume that if you were splitting a value val into something of type [inf][each], then val must be a stream of type of [inf * each] (i.e., of type [inf]). This is not true in the corner case where each equals 0, however. In that case, val is of type [0], which is a word, not a stream. As such, we need to ensure that we do not call fromSeq on val, which crashes if val is not a stream or sequence.

Fixes https://github.com/GaloisInc/cryptol/issues/1749.