Unimplemented bitvector operations in saw-core-coq

GaloisInc / saw-script

The SAW scripting language.

BSD 3-Clause "New" or "Revised" License

438 stars 63 forks source link

Unimplemented bitvector operations in saw-core-coq #1235

Open brianhuffman opened 4 years ago

brianhuffman commented 4 years ago

There are many bitvector primitive operations that do not yet have proper definitions in Coq.

https://github.com/GaloisInc/saw-core-coq/blob/691120b7811236518591396c2d03e6d377277812/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

brianhuffman commented 4 years ago

It might be useful to use the BITS library for some of these operations. The BITS library is already used for some operations like bitvector multiplication.