Remove strictly positive size of blocks in free semantics

Open josuemoreau opened this issue 1 year ago • 1 comments

The condition Ptrofs.unsigned sz > 0 in the semantics of free makes it difficult to prove that a program cannot block when calling free. So, this commit removes it, at the expense of a slightly more complicated proof that free is a proper external function.

Jan 29 '24 16:01 josuemoreau

Thanks for this proposal. It will take a while before I can review it in depth, but it sounds interesting.

Jan 31 '24 17:01 xavierleroy

I could finally review, and I like the idea very much. Thanks! I just manually merged this PR, with a slightly simpler proof of the injection diagram in Events.v (commit e1ea590).

Mar 18 '24 15:03 xavierleroy