As pointed out on #911 the outcome of having an ArchAcc_R.thy with very little in it (~100 lines), and an ArchArchAcc_R.thy having a silly name.
@corlewis observed:
"I think in my perfect world the generic ArchAcc_R would be removed and its contents moved to an earlier file. The lemmas that are currently in the interface would also need to move earlier, possibly to ArchKHeap_R like they were on X64. That would make it so that the arch-specific files can go back to being called ArchAcc_R, and they would stay focused on the arch get/set object lemmas like the comment suggests."
The silly name issue already happens in AInvs with ArchArch_AI and will likely happen again with ArchArch_R. No one really likes the alternative name options, e.g. GenArchAcc_R, ArchAccPre_R (sounds like it's arch-specific too)
As pointed out on #911 the outcome of having an
ArchAcc_R.thywith very little in it (~100 lines), and anArchArchAcc_R.thyhaving a silly name.@corlewis observed:
"I think in my perfect world the generic ArchAcc_R would be removed and its contents moved to an earlier file. The lemmas that are currently in the interface would also need to move earlier, possibly to ArchKHeap_R like they were on X64. That would make it so that the arch-specific files can go back to being called ArchAcc_R, and they would stay focused on the arch get/set object lemmas like the comment suggests."
The silly name issue already happens in AInvs with
ArchArch_AIand will likely happen again withArchArch_R. No one really likes the alternative name options, e.g.GenArchAcc_R,ArchAccPre_R(sounds like it's arch-specific too)