resource: add ResourceAlgebra trait

[bsdinis]

This is done by partitioning the previous PCM trait (while keeping that axiomatization of the pcm::Resource API intact and unchanged).

Then the algebra::Resouce API is verified against the pcm::Resource API, using an Option combinator (which lifts any RA into a PCM).

The interfaces are morally equivalent, with some minor details.
One of the more annoying details is that the axiomatized interface can "create" tracked shared refs to a resource, whereas we are forced to add a algebra::ResourceRef to hold the shared ref.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[bsdinis]

Importantly, the only changes to PCM relate to excising out the ResourceAlgebra part. Functionally, the PCM interface remains the same because now PCM extends ResourceAlgebra

[tjhance]

This looks good!

I assume you added ResourceRef because there otherwise wasn't a way to go from &'a pcm::Resource<Option<RA>> to &'a Resource<RA>? If you want, you can axiomatize a &'a pcm::Resource<Option<RA>> --> &'a Resource<RA> law, it's kind of a missing piece in our theory of shared ghost state, I just don't think it's come up before.

[bsdinis]

I assume you added ResourceRef because there otherwise wasn't a way to go from &'a pcm::Resource<Option> to 'a Resource? If you want, you can axiomatize a &'a pcm::Resource<Option> --> &'a Resource law, it's kind of missing piece in our theory of shared ghost state, I just don't think it's come up before.

Yes exactly, it's quite annoying because even converting is not trivial (i.e., it is not really doable via impl AsRef<Resource> since we'd need both a tracked alternative and a way to get the write postconditions in)

[bsdinis]

I'll take a look into adding the axiom