Make 'a signed word have a different name than 'a word

[simonjwinwood]

   "typ_name (typ_uinfo_t TYPE(8 word))  = ''word00010''"

and

   "typ_name (typ_uinfo_t TYPE(8 sword))  = ''sword00010''"

[lsf37]

Can you please provide motivation for the change in the description so the we can figure out in the future why we did this?

The C proofs all seem to be fine, which is a good sign, the errors are all in AsmRefine. @mbrcknl might know more about these.

[simonjwinwood]

So this is no longer true:

l4v/tools/asmrefine/ProveGraphRefine.thy

Line 192 in dcf271a

lemma typ_uinfo_t_signed_word:

    192 lemma typ_uinfo_t_signed_word:
    193   "typ_uinfo_t TYPE (('a :: len8) signed word) = typ_uinfo_t TYPE ('a word)"

[lsf37]

This might actually not be needed. It's used to prove the align_td lemma underneath, which should still be true, and then the ptr_inverse_safe lemma which I have no idea what it is. The definition talks about footprints, though, which should also still be the same. So both should hold.