michaelmcinerney

Missed a few bits of cleanup, but should be all good now

> The actual content looks good to me. However, I can't be sure without opening it up myself, but do you need all of the fake constants. I would have...

> @michaelmcinerney : any reason this wasn't merged? No good reason. I've been meaning to ask whether it's fine to merge. I'll try today

I didn't put much thought into the names of the new lemmas. Maybe `valid_cross` or `hoare_cross` might be slightly better than `hoare_from_abs`. But I imagine that someone would have to...

I have responded to the comments, and also added a type signature for `ex_abs_underlying`

> It does look like it's a left-over, yes. @michaelmcinerney and @mktnk3 do you remember why `mcsPreemptionPoint` has an `irq` parameter? It seems to be unused inside. I can't remember...

> @michaelmcinerney did I summarise this correctly? Yes, thanks Gerwin

An infinite budget for the idle sc is an interesting idea, but we'd still need to special case it so that it's not charged the same as other threads. If...

Actually, if the idle sc had just the one refill, starting at time 0, and with rAmount equal to the max word, then, along with the special casing in #697...

> @michaelmcinerney do you think would need any spec/ainvs/refine changes? I assume we haven't reached this function yet in CRefine. The `irq` bit has already been removed from the aspec....