Lemmas for simplifying masking and thread states #817
Conversation
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
proof/crefine/X64/Wellformed_C.thy
Outdated
| (* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *) | ||
| lemma | ||
| shows ThreadState_Restart_mask[simp]: | ||
| "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart" |
There was a problem hiding this comment.
nitpick: I'd much prefer scast ThreadState_Restart :: machine_word to the version with no spaces; the no-space version visually indicates a cast of ThreadState_Restart as if it were an 'a, but I assume that what's intended is that machine_word is the target of the scast
There was a problem hiding this comment.
by the way: is ThreadSTate_Restart coming from the C or the Haskell? I'm trying to think if there's a nice way to generate these lemmas in one go.
There was a problem hiding this comment.
These are all from the C, in include/object/structures.h. The Haskell has similar things, but doesn't use the ThreadState prefix in the names.
And due to an ifdef in the C, I forgot to include IdleThreadState. I'll add a fixup commit for that
There was a problem hiding this comment.
Right, then there's probably no nice way to generate these lemmas. There might be some hack where we go from x : set [ThreadState_Restart, ...] ==> (scast x :: machine_word) && mask 4 = scast x and explode it, but I'm not sure how much nicer that is.
|
This is causing tests to fail. I'll check this out tonight and hopefully push a fixup commit tonight or tomorrow |
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
No description provided.