search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
944 stars 81 forks source link

update verification of compiler from closLang to bvp #45

Closed xrchz closed 9 years ago

xrchz commented 9 years ago

at present I think that just means finishing compiler1/proofs/bvi_to_bvpProof

myreen commented 9 years ago

There is also a bit of work to be done in bvl_to_bvi, namely this transition should compile away the globals. It currently doesn't, but the proof should be set up to enable removal of globals. What does it mean to compile away the globals? Answer: instead of having an arbitrary number of globals, there should only be one global and this global holds an array pointer (bc_value) to an array that holds all the globals. Note that, as new globals are allocated, this array will eventually run out of space. There should be a library function (in the stubs) in bvi that allocates a new globals array (which is double the size of the previous one) and copies the content from the old globals array into the new bigger globals array.

xrchz commented 9 years ago

49f4c42dd065b799a2caefb61f38af34a6d43b5e does what I intended, I'll open a new issue for compilation of globals