While it's already known that word_size and word_bits_def are available outside of Arch during arch-split (which also leads to things such as tcbSizeBits ending up outside Arch), we can be generally careful about not unfolding these to try get a generic proof.
Unfortunately, the Word library adds rules to the simpset (and maybe intro/elim/dest) which talk about LENGTH('a). For example, when trying to write a generic proof, we'd want length (to_bl x) to simplify to word_bits with the same word length. Currently, if x is a 32 word, we'll get a simplification to LENGTH(32) which simplifies to 32. When 32 or 64 starts flying around the proof, we can't really say it's generic.
Ad-hoc workarounds such as:
lemmas word_bl_word_bits = word_bl_Rep'[where 'a=machine_word_len, simplified word_bits_def[symmetric]]
and then also removing word_bl_Rep' from the simpset are adequate for now, but there are quite a few more lemmas which expose LENGTH and may trigger in surprising ways (e.g. on only one architecture).
To be able to find all of these, it would be useful to augment find_theorems somehow to be able to look at sets of theorems (either simp for the global/context simpset, or named_theorems).
While it's already known that
word_sizeandword_bits_defare available outside of Arch during arch-split (which also leads to things such as tcbSizeBits ending up outside Arch), we can be generally careful about not unfolding these to try get a generic proof.Unfortunately, the Word library adds rules to the simpset (and maybe intro/elim/dest) which talk about
LENGTH('a). For example, when trying to write a generic proof, we'd wantlength (to_bl x)to simplify toword_bitswith the same word length. Currently, ifxis a32 word, we'll get a simplification toLENGTH(32)which simplifies to32. When 32 or 64 starts flying around the proof, we can't really say it's generic.Ad-hoc workarounds such as:
and then also removing
word_bl_Rep'from the simpset are adequate for now, but there are quite a few more lemmas which exposeLENGTHand may trigger in surprising ways (e.g. on only one architecture).To be able to find all of these, it would be useful to augment
find_theoremssomehow to be able to look at sets of theorems (eithersimpfor the global/context simpset, or named_theorems).