l4v icon indicating copy to clipboard operation
l4v copied to clipboard

Published 20 hours ago • verified publisher icon seL4

Style for `ccorres` statements

Open michaelmcinerney opened this issue 2 years ago • 1 comments

michaelmcinerney avatar Jul 29 '22 05:07 michaelmcinerney

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 thought you would just need ccorres, UNIV, c_guard, ptr_select, and maybe ptr and cond. Couldn't the ccorres arguments be bound variables?

Also, you shouldn't need the axiomatizations unless you explicitly refer to the definition lemma.

Very good point. None of the constants is needed. I've removed them, and adjusted things in the fake lemmas to make the schematic variable names nicer

michaelmcinerney avatar Jul 29 '22 06:07 michaelmcinerney

@michaelmcinerney : any reason this wasn't merged?

Xaphiosis avatar Oct 05 '22 16:10 Xaphiosis

@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

michaelmcinerney avatar Oct 06 '22 00:10 michaelmcinerney