Enigma example in "Programming Cryptol" needs to be updated

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

Enigma example in "Programming Cryptol" needs to be updated #1745

Open smithdtyler opened 2 weeks ago

smithdtyler commented 2 weeks ago

In section 3.2, the call to elem in mkRotor is incorrect, as elem does not take a tuple.

mkRotor : {n} (fin n) => (Permutation, String n) -> Rotor
mkRotor (perm, notchLocations) = [ (p, elem (p, notchLocations))
| p <- perm
]

Should be

mkRotor (perm, notchLocations) = [ (p, elem p notchLocations)
                                | p <- perm
                                ]

sauclovian-g commented 2 weeks ago

It's more complicated than that since this elem is a private definition (see line 762 of Enigma.tex for the copy that's used here) so one should change not just this usage, but also that definition and also the real one elsewhere in the book that the comment about an exercise refers to. And there are other references scattered around the book, some of which use one signature and some the other, and they should probably all be updated as well.

Is there any reason that one would deliberately use a different type signature for the exercise version? Or is it all just Olde?