Dual of "make invalid states unrepresentable"

[Pierre Thierry]

When I wrote the "Revocation" section of the capability-URI RFC, I described a design principle, where you avoid having code make a decision to enforce a policy, and instead have the graph of capabilities enforce the policy by construction.

The example is with a caretaker that removes its capability when revoked. After revocation, the caretaker couldn't decide wrongly to proxy an invocation, because its internal variable points to NULL or something similar.

I realize that it's not how the caretaker is described in many documents, including Robust Composition, where the caretaker has a boolean flag inside. I wonder if it is how Redel implemented it, though, because its thesis says "Whenever A's level of trust in B decreases, a weaker capability can be given to C."

Has this principle been formally described somewhere? Does it have a name?

It reminded me a lot of "make invalid states unrepresentable", which is now pretty widely known. I wondered about calling it "make wrong decisions unreachable" but it doesn't fit exactly…

Curiously,
Pierre Thierry
--

pie...@nothos.net
0xD9D50D8A

[Alan Karp]

I believe the E in a Walnut describes the "set to null" version of the caretaker.

I want to point out that you have more options for revocation in other capability systems.  With both opaque bearer tokens and certificate capabilities you have the option of telling the resource to stop honoring the token.  The advantage is that you don't have to plan ahead by creating a caretaker.  The downside is that you need enough information to also revoke downstream delegations.

--------------
Alan Karp

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/friam/8849f876-63df-4823-9dc7-9e1a273982c6%40nothos.net.

[Matt Rice]

On Fri, Aug 28, 2026 at 3:23 PM Pierre Thierry <pie...@nothos.net> wrote:
>

There is also a long history of the pattern of "correct by
construction" where program states are constructed as a part of its
proof of correctness.
I don't know if dijkstra coined it, but you can see the term used in a
description of his process
https://www.computer.org/profiles/edsger-dijkstra

> Curiously,
> Pierre Thierry
> --
>
> pie...@nothos.net
> 0xD9D50D8A
>

[Mark S. Miller]

I usually use the set-to-null pattern. In Robust Composition, I did not, to give Alice the option to re-enable it

In context, "Alice's gate" refers to a gate in Carol's vat created by Alice, to which Alice remotely holds the `gate`.

On Fri, Aug 28, 2026 at 3:23 PM Pierre Thierry <pie...@nothos.net> wrote:

--

You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/friam/8849f876-63df-4823-9dc7-9e1a273982c6%40nothos.net.

--

  Cheers,
  --MarkM

[Pierre Thierry]

Le 02/09/2026 à 23:32, Mark S. Miller a écrit :

I usually use the set-to-null pattern. In Robust Composition, I did not, to give Alice the option to re-enable it

Wouldn't it have been better to use the set-to-null caretaker? Such a caretaker, once revoked, shows in topology-only bounds of authority that Bob cannot be reached anymore. Or was the goal to have a version where it doesn't, to discuss the behvioral analysis?

[Pierre Thierry]

Le 29/08/2026 à 00:34, Matt Rice a écrit :

It reminded me a lot of "make invalid states unrepresentable", which is now pretty widely known. I wondered about calling it "make wrong decisions unreachable" but it doesn't fit exactly…

There is also a long history of the pattern of "correct by construction" where program states are constructed as a part of its proof of correctness.

But "correct by construction" mandates a program construction method, while "make invalid states unrepresentable" and the one I'm trying to name are design principles you can incorporate in any method.

[Matt Rice]

On Sun, Sep 6, 2026 at 4:21 PM Pierre Thierry <pie...@nothos.net> wrote:
>
> Le 02/09/2026 à 23:32, Mark S. Miller a écrit :
>
> I usually use the set-to-null pattern. In Robust Composition, I did not, to give Alice the option to re-enable it
>
> Wouldn't it have been better to use the set-to-null caretaker? Such a caretaker, once revoked, shows in topology-only bounds of authority that Bob cannot be reached anymore. Or was the goal to have a version where it doesn't, to discuss the behvioral analysis?

We need to take into account the context of this revocation, In this
section the object which was granted, and the grantor of the object
are a part of a network partitioning event.
So out of an abundance of caution, the object revokes itself, since
assuming symmetry of the network failure it assumes that the grantor
would be unable to revoke the object.

Assuming the network failure is resolved, it could be that the grantor
did not want to revoke. Or if the automatic revocation was overzealous
we may want to restore the grant upon reconnection. So in that case it
isn't actually an explicit decision by the grantor to revoke access.

[Matt Rice]

Sure, I should probably have stated that that appears to me to be the
history of "correct by construction", these days I hear it mostly in a
looser sense
of "only valid states are representable"

[Matt Rice]

I guess I should make it clear that the context being section 11.5.3
Implications for revocation of Robust Composition
from which that screenshot from Mark's was taken.

[Pierre Thierry]

Le 07/09/2026 à 01:33, Matt Rice a écrit :

It reminded me a lot of "make invalid states unrepresentable", which is now pretty widely known. I wondered about calling it "make wrong decisions unreachable" but it doesn't fit exactly…
There is also a long history of the pattern of "correct by construction" where program states are constructed as a part of its proof of correctness.
But "correct by construction" mandates a program construction method, while "make invalid states unrepresentable" and the one I'm trying to name are design principles you can incorporate in any method.
Sure, I should probably have stated that that appears to me to be the history of "correct by construction", these days I hear it mostly in a looser sense of "only valid states are representable"

Well, on second read, I don't agree with my earlier comment. It so happens that I just saw Dijkstra's description of "correct by construction" again, and both "make invalid states unrepresentable" and making the graph of authority such that wrong choices cannot be made both completely fit into his method: in each step, you identify an invariant, and you modify the code to enforce that invariant.

Thanks for pointing it out. Referring to Dijkstra's more general principle makes it less pressing to me to find a name for the graph case.

Gratefully,
Pierre Thierry
--

pie...@nothos.net
0xD9D50D8A

[Matt Rice]

One thing I think might be worth mentioning is that you can actually do a hybrid pattern here,

which combines the gate approach, with the set-to-null pattern.

Interestingly you can do it all with a single non-null pointer by storing a gate disable bit in the unused extra

space of the pointer alignment. This allows for the "enabled" version of the pointer to just be the pointer itself.

You can pretty easily make a rust typed version of this using the `enum-ptr` crate, 

```

#[derive(EnumPtr)]
#[repr(C, usize)]

enum Gate<T> {

   Enabled(Box<T>),

   Disabled(Box<T>)

}

assert_eq!(std::mem::size_of::<Option<Compact<Gate<u8>>>>(), std::mem::size_of::<Box<u8>>())

```

The `Compact` type here is a pointer sized reference to a `Gate`, but since `Box` references are also `NonNull`

It has a `NonNull` niche so the sizes of `Option<T>` and `Box<T>` are the same. That is to say, `Option::None` is

the null pointer.

I just figured it might be worth mentioning because it is both a hybrid pattern between the discussed patterns, but also space

efficient with an equivalent type safe conversion, but kind of a random thought...

To view this discussion visit https://groups.google.com/d/msgid/friam/CAK5yZYjUvy15YcLLr1tG%2BfZZ6aP_iOT_DDYcPz0ykPTib5SzTw%40mail.gmail.com.

[Pierre Thierry]

Le 08/09/2026 à 23:58, Matt Rice a écrit :

Interestingly you can do it all with a single non-null pointer by storing a gate disable bit in the unused extra

space of the pointer alignment. This allows for the "enabled" version of the pointer to just be the pointer itself.

You can pretty easily make a rust typed version of this using the `enum-ptr` crate, 

But then the authority is still there, dormant, just a flip away. It doesn't give you the guarantee that the caretaker won't give access to the target capability in the future, does it?

[Alan Karp]

On Tue, Sep 8, 2026 at 3:17 PM Pierre Thierry <pie...@nothos.net> wrote:

 

But then the authority is still there, dormant, just a flip away. It doesn't give you the guarantee that the caretaker won't give access to the target capability in the future, does it?

It does if the caretaker has no method that resets the forwarding object.  In MarkM's example, the caretaker has a revoke method that sets the forwarding target to null.  The caretaker does not remember the old value, and there's no method for changing it other than setting it to null.

 

--------------
Alan Karp

[Matt Rice]

By wrapping the gate in an Option type it achieves the same result as the set-to-null

I.e Option::none == null

Option::Some(Gate::Enabled(foo)) or Some(Gate::Disabled(foo))

It can be either fully revoked, or disabled in a way that can be re-enabled. Only the full revocation satisfies your invariant though.

So, hybrid between the two approaches, with irreversible and temporary revocation

--

You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/friam/c7b9fc29-f165-4582-858c-01c847337863%40nothos.net.

[Matt Rice]

On Tue, Sep 8, 2026 at 3:48 PM Matt Rice <rat...@gmail.com> wrote:
>
> By wrapping the gate in an Option type it achieves the same result as the set-to-null
> I.e Option::none == null
>
> Option::Some(Gate::Enabled(foo)) or Some(Gate::Disabled(foo))
>
> It can be either fully revoked, or disabled in a way that can be re-enabled. Only the full revocation satisfies your invariant though.
>
> So, hybrid between the two approaches, with irreversible and temporary revocation
>
>
> On Tue, Sep 8, 2026, 3:17 PM Pierre Thierry <pie...@nothos.net> wrote:
>>
>> Le 08/09/2026 à 23:58, Matt Rice a écrit :
>>
>> Interestingly you can do it all with a single non-null pointer by storing a gate disable bit in the unused extra
>> space of the pointer alignment. This allows for the "enabled" version of the pointer to just be the pointer itself.
>> You can pretty easily make a rust typed version of this using the `enum-ptr` crate,
>>
>> But then the authority is still there, dormant, just a flip away. It doesn't give you the guarantee that the caretaker won't give access to the target capability in the future, does it?
>>

Just to maybe (hopefully) make it easily understandable, at the
expense of being a bit less idiomatic we could "inline" the `Option`
type directly into the `Gate` type.
Also giving comments explaining the pointer representation.

```
// We can convert between `Gate<T>` and a compact tagged pointer type,
assuming the pointer is both non-null and has unused extra bits for
alignment.

#[repr(C, usize)]
enum Gate<T> {

Enabled(Box<T>), // repr = addr(T), relying on the fact that Box<T>
is NonNull.
Disabled(Box<T>) // repr = addr(T) | 0x1, relying on the fact that
Box<T> is NonNull.
Revoked, // repr = 0x0,
}
```

[Alan Karp]

Here's an example from E in a Walnut by Marc Stiegler.

# E sample
def revocableCapabilityMaker(baseCapableObject)  {
    var capableObject := baseCapableObject
    def forwarder {
        to revoke() {capableObject := null}
        match [verb, args] {E.call(capableObject, verb, args)}
    }
    return forwarder
}

As you can see, there's no way to unrevoke.

--------------
Alan Karp

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/friam/CACTLOFrJHFruBGkVp5TVMpxoa7LxBUSCLfHJOxScX_oJMfeFow%40mail.gmail.com.

[Matt Rice]

Yes, this is the set-to-null pattern Pierre was referring to. The one I posted the type signature for can be made into hybrid with the features of both this one by MarcS and the one which can be disabled/then re-enabled that MarkM posted a screenshot of. It can have both revoke and enable/disable.

To view this discussion visit https://groups.google.com/d/msgid/friam/CANpA1Z3pxGKhr5-8NViS7Mf%2BkoKupr1G%3DxDwqAynsO6Tt0S9sw%40mail.gmail.com.