This can be classified as a concurrency bug as there were two processes at once in the unsealer routine; there were two stack frames within the same lexical scope coordinating the state of the same instance of HasPayload. This code is not needed in Keykos because Keykos has the primitive domain tool which provides efficient synergy. Also domains are not accidentally ‘reentrant’ as they are in most modern languages. Keykos also prevents domains from being called while they ‘are already on the stack’.
One red flag is a call to a suspicious function, such as box. But what is a ‘suspicious function’? The plan was that box was an object whose behavior we had defined, but there was no way to enforce that plan. Reasoning about the behavior failed when a call to a suspicious function resulted in running code, that we had written, which used its authority to modify the variable which we were reasoning about. For any sort of correctness we must assume that the function car is in fact the real primitive described in the manual. Here box is a parameter passed from the netherworld. We think:
Another bad mental pattern is while thinking about sealer logic, we try to guard only the uniqueness of our access to innards of sealed objects. We did not fail in that regard but we may neglect our obligation to keep separate the abstract values of our clients. Now the question is just whose obligation is that? This is a serious question. The Keykos factory was invented to absolve the definer of the behavior of objects from a factory from issues of keeping secrets defined by the abstracted state of those objects.
If a purveyor of an abstraction wants to guarantee that abstractions from one client are never mixed from those of another, it will suffice to instantiate a whole new purveyor with its own sealer-unsealer pair. Factory like logic can assure clients that this has been done. This would preclude clients from even sharing those abstract value should they decide to.
With factory logic in Keykos two users of the same factory will not have their secrets mixed even if the behavior of the objects from the factory are incompetent. They can share such objects should they decide to. This is because the object from the factory retains the domain creator that all of the siblings from that factory use. The creator and recognize and open domains that it created, much as the unsealer unseals.