"Unexpected Fin constraint violation!"

[weaversa]

$ cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.7.1 (1e11ff6)

Loading module Cryptol
Cryptol> transpose (zero : [inf][1][1])
[[0x0, 0x0, 0x0, 0x0, 0x0, ...]]

$ saw
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.3 (58e71d5)

sawscript> print {{ transpose (zero : [inf][1][1]) }}
saw: Unexpected Fin constraint violation!

[brianhuffman]

It appears that when we implemented transpose in saw-core, we omitted the cases for infinite sizes. (https://github.com/GaloisInc/cryptol-verifier/blob/master/saw/Cryptol.sawcore#L1066) This should be pretty easy to fix.

[weaversa]

Thank you!