search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Reconsider the usefulness of the translation of vectors as lists in saw-core-coq #1233

Open Ptival opened 4 years ago

Ptival commented 4 years ago

We had initially added an option for translating Cryptol vectors as Coq lists, ignoring indices.

This might not be useful in practice: almost no proof can be done on the output code, as we lose the information that the lists will have the given size.

An alternative solution would be translating vectors as an existential package of the raw list, and a proof that its length is the index. For vectors, we currently insert a "tactic term", ltac:(solveUnsafeAssert), whenever a proof that relates two judgmentally different but propositionally equal indices should be inserted (say, when a vector of size n + 0 is used in a context where a vector of size n is needed).

sauclovian-g commented 1 week ago

It might also be reasonable to use Coq's vector library.