Comments on FC00 paper

Mark S. Miller
Tue, 02 Nov 1999 15:47:17 -0800

At 03:12 PM 11/2/99 , Chip Morningstar wrote:
>-- To match the sealer/unsealer semantics, it needs to be impossible to get
>        the sealer given the sealed box alone.

It must also be impossible to get the sealer given the box and the unsealer,
and it must be impossible to get the unsealer given the box and a sealer.

>-- You must be able to seal multiple messages with the same sealer and be
>        able to unseal them all later with the same unsealer.


>-- It must be impossible to change the contents of the box after it has been
>        sealed (and it must be similarly impossible to create an 
> "unsealed" box
>        that is uncommited as to what is in it until you decide later what to
>        put in it).

Whoa!  This one's tricky. Depending on how you interpret it, E either does
this perfectly or not at all.  For deferred commitment, consider:

     ? define BrandMaker := import:org.erights.e.elang.sealing.Brand
     # value: <statics of org.erights.e.elang.sealing.Brand>

     ? define [sealer,unsealer] := BrandMaker pair("Chip")
     # value: [<Chip sealer>, <Chip unsealer>]

     ? define [promise,resolver] := PromiseMaker()
     # value: [<Deferred ref>, <Unresolved Resolver>]

     ? define sealedPromise := sealer seal(promise)
     # value: <sealed by Chip>

     ? define contents := unsealer unseal(sealedPromise)
     # value: <Deferred ref>

     ? contents
     # value: <Deferred ref>

     ? resolver resolve("I finally made up my mind")

     ? contents
     # value: I finally made up my mind

On the one hand, the invoker of seal() committed to which object was being
sealed -- this particular promise.  OTOH, because it was a promise, and a
resolved promise is equivalent to its resolution, the invoker of seal
successfully deferred the decision about what was sealed until later.
Similar games can be played with apparently mutating the contents of the box
after sealing it: the seal() invoker can immutably seal a mutable forwarder
that he retains the right to mutate.  I don't find either of these a
problem, so I would drop that part of Chip's specification.  If you want an
assurance of various kinds of immutability, E provides (or will provide)
other mechanisms for doing so.