Create byteTheory and move it to HOL

CakeML / cakeml

CakeML: A Verified Implementation of ML

https://cakeml.org

Other

954 stars 84 forks source link

Create byteTheory and move it to HOL #521

Closed myreen closed 1 week ago

myreen commented 6 years ago

This issue is about:

collecting all byte-access functions and theorems about them into a new byteScript.sml;
tidying up that file;
moving it to HOL.

By "byte-access functions" I mean functions such as set_byte and get_byte in wordSem, and also conversions between words and lists of bytes.

xrchz commented 5 years ago

This is pretty related to #549

xrchz commented 5 years ago

Many properties of these functions that appear across the CakeML proofs have good_dimindex(:'a) as an assumption. However, I don't think good_dimindex should appear in this byteTheory. What do you think @myreen?

myreen commented 5 years ago

@xrchz I agree that good_dimindex shouldn't feature in byteTheory. However, one might still have theorems for 32 and 64 cases in byteTheory.

xrchz commented 5 years ago

It's probable that these theorems could/should be generalised. E.g., maybe they work for any word size above 8, or any multiple of 8. I guess this issue should include attempting to generalise theorems if possible, so that more can be put in byteTheory.

xrchz commented 1 week ago

This is done right? I see byteTheory in HOL now.