[cap-talk] Is EQ necessary for PetName systems?

[David Hopwood]

Toby Murray wrote:
> Essentially, as demonstrated by Dean Tribble on numerous occasions, one
> can express a lot without EQ. I believe we're still yet to see an
> example of a pattern that cannot be expressed without EQ.
>
> I'd like to reignite the discussion with the suggestion the
> implementation of a petname system in an object-capability language
> might not be achievable without an EQ primitive -- or at least without
> the facilities to build an EQ primitive.
> 
> At minimum, I believe one needs a reliable map from caps to PetNames
> that will reliably map capabilities that are EQ to the same PetName.

That only needs to work for a subset of capabilities -- the ones that
represent targets for petnames. That's important because it allows a
system to have objects that can be declared as incomparable for identity
(e.g. Selfless objects in Joe-E).

Also, the mapping needs to be reliable in the sense of mapping a given
petname always to the same logical abstraction, but not necessarily always
to the same object.

> I'll stick my neck out and say that without such a thing, it appears the
> implementation of a PetName system would be impossible.
> 
> However, given such a map, one can implement one's own reliable EQ. I
> maintain a collection of these maps, m_1, m_2, ..., m_N . Each m_i is a
> map of size 1 -- it maps only a single capability, c, to itself and
> throws an exception if given any other cap that isn't EQ to c.  Each cap
> I receive, I simply test to see whether it is mapped by any of the m_i.
> If not, I create a new map m_N+1 and have it map the new capability to
> itself.
> 
> Two caps are then EQ if and only if they are mapped by the same m_i.

If we do have a general-purpose map that works for any two capabilities,
I think you're correct that this implies EQ.

EQ has the following properties:

a) equivalence relation between any two capabilities (in the system
   under discussion)
b) EQ(a, b) = true implies that a and b are observationally
   indistinguishable
c) universally available
d) is a prompt operation (preferably O(1); at the least, completes
   without relying on the compared objects)
e) does not expose the fact that a comparison has been performed to
   either object
f) does not make either object accessible to the other.

The EQ constructed from a map satisfies all these criteria except the
O(1) part of d). I think that not being O(1) is a minor nit, that doesn't
materially affect your conclusion -- with the caveat above about not
all objects needing to be comparable for identity.

> Hence, my argument is that one can implement a PetName system if and
> only if one can implement (or already has available) EQ.

-- 
David Hopwood <david.hopwood at industrial-designers.co.uk>