search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
442 stars 93 forks source link

Why progs64/ is different from progs/ ? #583

Closed lengyijun closed 2 years ago

lengyijun commented 2 years ago

For example, verif_insertion_sort.v only exists in progs/ , not progs64/ .

QinshiWang commented 2 years ago

I think it's because that proof is not maintained for 64-bit. I don't know why it's not. There are some files only in one version of 32/64-bit but not the other.

andrew-appel commented 2 years ago

Just as a C program may or not be portable between 32-bit and 64-bit, even when the program is portable the VST proof script may or may not be portable between 32-bit and 64-bit. All the proof scripts in progs64 are portable (i.e., they are automatically copied from the progs/*.v files). The programs that are in progs/ but not in progs64 are those that are either not (yet) made portable, or not (yet) checked for portability. In the long run, since most users are likely to use 64-bit mode, it would be good to increase the number of verifications in progs64.