Refactor simuliris ghost state

Change ghost state to use the lamba-rust ghost state.

Could you give a short summary for what happens here? :)

This MR replaces the ghost state of simplang with the ghost state from lambda rust so that we get the load rule for fractional points to and it is also doing some refactoring ;)

changed the description

added 2 commits

• 22702798 - 1 commit from branch master
• ed940df4 - refactor ghost state

Compare with previous version

I guess I am most wondering why something is taking option loc here -- that seems odd?

==>t is heap_freeable and takes option nat where Some n means that the block starting at l is still allocated and has n bytes while None means that the block starting at l has been deallocated.

Oh, that's a 1, not an l... makes sense, thanks :)

Could we maybe also have some notation that does not require the Some? It seems quite uncommon to explicitly state the None (though it seems to be very convenient to have this notation with options for the setup of the ghost state). Maybe ~~>t and ~~>s?

Yes, it might be nice to have some better notations. But using different kinds of arrows for all ghost state seems a bit weird to me. How about something closer to what RustBelt uses? E.g. something like the following?

† l … n  := freeable l (Some n)
† l …? n := freeable l n
† l … -  := freeable l None

Yes, that might be better than the arrows

changed this line in version 4 of the diff

I've changed the notation. Any other comment?

Thanks! No, I don't have any other objections :)

Great, thanks. I will merge the MR then.

Wow, the proofs are so much nicer now! :)

added 1 commit

• 0e9c8bdd - refactor ghost state

Compare with previous version

added 1 commit

• d3d0a6a0 - refactor ghost state

Compare with previous version

merged

mentioned in commit be46711f