Refactor receipt part of the invocation

[Gozala]

📽️ Preview

Attempt at factoring out receipts from the invocation spec. It describes receipts in terms of /ucan/assert invocation. This is an early draft and could use substantial lifting, however I thought it was still good idea to capture what we've been discussing in side channels so we could align on exact format.

[expede]

I've been thinking about this a bit recently. It's possible that /assert is too broad, since you can assert all kinds of things including content claims, computation receipts, and (oracle) facts about the world. In this current setup, you need to duck type the args field.

How do you feel about making receipt a subtype of assert? It would have all of the same fields, but you'd also know more about the inner structure. Following the new cmd format, this would look like /ucan/assert/receipt or /ucan/assert/ran or similar.

[Gozala]

I've been thinking about this a bit recently. It's possible that /assert is too broad, since you can assert all kinds of things including content claims, computation receipts, and (oracle) facts about the world. In this current setup, you need to duck type the args field.

I have not called that out explicitly but that was kind of the intention behind making facts into a map. The way I was thinking about it is that receipt is just an assertion that specifies two expected {out, run} facts, but it should be possible to assert arbitrary that about entity in the about field they just aren't required by receipt specification.

How do you feel about making receipt a subtype of assert? It would have all of the same fields, but you'd also know more about the inner structure. Following the new cmd format, this would look like /ucan/assert/receipt or /ucan/assert/ran or similar.

I suppose ☝️ in comparison might be useful if you want to say allow asserting {out, run} but nothing else 🤔 On the other hand if someone adds additional field even if cmd was /ucan/assert/receipt it probably still should be considered as a valid receipt.

Either way I don't mind changing cmd to /ucan/assert/receipt although I do not know if I buy into the argument.

[expede]

in comparison might be useful if you want to say allow asserting {out, run} but nothing else

I think that we're thinking about the design space here very differently. I see the cmd field as filling two roles:

1. Define the semantics of the invocation
2. Establish a common language / "which fields are available to that function call"

Receipts have a particular mechanical function with promises. They're more than an assertion of fact — while you can look at it through that lens, these are very different in functionality.

This is the same distinction as shows up in the age old arguments about structural vs nominal typing. Just because the same structural information exists doesn't necessarily mean that it has the same meaning. The analogy breaks down a but here since with a type system you can move that extra bit of information to compile time, which we can't do due to the distributed nature of the problem.

What I liked about the idea of subtyping is that we could nominally tag with the cmd field that "the payload is just some assertion, not something to run", and leave the fields blank. You can then subtype for more specific uses.

[Gozala]

I don't think we're thinking that differently it's just you're hoisting all the types all they way to the invocation and use cmd as a discriminant, which I generally agree with. In this instance however I feel like not hoisting the type is a better idea and treating it as somewhat constrained generic makes more sense to me. Here is illustration in typescript syntax

What I'm proposing is something like

type Assert<Facts extends {[key:string]: unknown}> = {
  cmd: "ucan/assert"
  with: DID
  args: { about: Link, facts: Facts }
}

type Receipt = Assert<{ out: Result, run: Link[] }>

// I could also have something like
type LocationCommitment = Assert<{ site: URL }>

Where's what you're suggesting is not to make Assert generic but rather hoist to the cmd discriminant

type Receipt = {
   cmd: "/ucan/assert/receipt"
   with: DID
   args: { about: Link, out: Result, run Link[] } 
}

type LocationCommitment = {
  cmd: "/ucan/assert/commitment"
  with: DID
  args: { about: Link, site: Link[] }
}

I prefer generic route as opposed to hoisted, because I have a neutral component in the system that does not need to worry about the Facts parameter and can index things regardless of the concrete type. Doing this with hoisted variant is possible, but requires maintaining list of cmds or adopting some name-spacing like ucan/assert/, even then I loose one invariant which is all variants should have about field.

On the flip side I do recognize that generic variant above no longer features discriminant which certainly can be a drawback. It does not affect my use case because indexer does not care, and receipts are to be queried from the index so things that don't match will not be returned by query.

That said I understand that in other systems having discriminant may be important which is why I proposed something like this as a compromise (where key is a discriminant)

type Assert<Facts extends {[key:string]: unknown}> = {
  cmd: "ucan/assert"
  with: DID
  args: { about: Link, facts: Facts }
}

type Receipt = Assert<{ receipt: { out: Result, run: Link[] } }>
type Commitment = Assert<{ commitment: { site: URL } }>

It also could be sugared more to your liking as follows (although level of advanced typing makes me uncomfortable)

type Assert<Key extends string, Facts extends {[key: string]: unknown}> = {
   cmd: `/ucan/assert/${Key}`
   with: DID
   args: { about: Link } & Facts
}

type Receipt = Assert<"receipt", { out: Result, run: Link[] }>
type Commitment = Assert<"commitment", { site: URL }>

I find last two pretty much identical except later seems to reduce nesting and require more powerful type system and one before is less demanding on type system at the expense of bit more nesting

[expede]

Given how receipts interact with promises, is the idea here to make more granular repos? Basically:

flowchart TB
    Invocation
    Delegation -->|depends on| Invocation
    Revocation -->|depends on| Invocation
    Assertion -.->|kind of| Invocation
    Receipt -.->|kind of| Assertion
    Promise -->|depends on| Receipt

Loading

[Gozala]

Given how receipts interact with promises, is the idea here to make more granular repos? Basically:

flowchart TB
    Invocation
    Delegation -->|depends on| Invocation
    Revocation -->|depends on| Invocation
    Assertion -.->|kind of| Invocation
    Receipt -.->|kind of| Assertion
    Promise -->|depends on| Receipt

Loading

We don't have to break it out necessarily it's just we did talk not too long ago that perhaps receipts are still something we're iterating and others might want to use invocations without receipts so I thought I'd just move it into own thing so people could adopt invocations without necessarily adopting receipts.

[Gozala]

@expede your comment about asserts been very generic and my sentiment that receipt is just an assertion of {out, run} got me wondering that perhaps run could be made optional and implicitly []. That way this is even more minimal requirement space.

Or alternatively we could make make the whole thing as

{
   cmd: '/ucan/assert'
   args: {
       about: { '/': 'bafy...thing' },
       facts: {
          receipt: {
              out: { ok: {} },
              run: [] 
          }
      }
   }
}

That way /ucan/assert/receipt could be typed as follows and be equivalent of the above

{
   cmd: '/ucan/assert/receipt'
   args: {
       about: { '/': 'bafy...thing' },
       facts: {
         out: { ok: {} },
         run: [] 
      }
   }
}

[expede]

Hmm I'm not sure about adding facts as a wrapper around out and run. Does it add something that I'm missing? This is such a common case, it makes me wonder if we should just put receipts at the same level as assertions ("receipts don't need to be assertions"). Assertions in this style almost feel so generic as to be meaningless, which is something I've been warned against that was a mistake in OAuth 2

[Gozala]

Hmm I'm not sure about adding facts as a wrapper around out and run. Does it add something that I'm missing?

It only makes sense if there are generic assertions and receipt is just a variant of it, kind of like what sturct with known fields is to a map. If we say there is no generic assertions then it no longer matters.

In other words I was treating about as entity, and facts as set of attribute → value pairs for that entity. Trough this lens "receipt" is just a well defined relation akin of schema you can define (e.g. in datomic). My sentiment there is we could define other schemas for other relations over time. In fact someone could also extend receipts to add some extra attributes. e.g. I have contemplated idea of using this similar to session cookies.

Now non of that matters if we decide that generic assertions aren't a think we care in which case wrapper does become a more of redundancy.

[Gozala]

I think one other option to kind of do what I want in terms of generic assertions without having to burden anyone else is to change about to something that is clearly distinct from all other fields of the args in which case same goal could be accomplished. I have in fact considered following variant, but hesitated because of special relation IPLD has with /.

{
   cmd: '/ucan/assert/receipt'
   args: {
       '/': 'bafy...thing',
       out: { ok: {} },
       run: []
   }
}

Some other distinct symbol could be utilized of course, but I don't know it never feels right, so I suggested {about, facts} instead.

[expede]

We don't have to break it out necessarily it's just we did talk not too long ago that perhaps receipts are still something we're iterating and others might want to use invocations without receipts so I thought I'd just move it into own thing so people could adopt invocations without necessarily adopting receipts.

Yeah that's true. I've also thought it through more since writing the above and it's probably the right thing. There's no drawback AFAICT, and we can always merge them later if need be. It also lets us ship delegation, invocation, and revocation immediately. Promises and receipts have often been a slow burn for it to click, so let's just remove the problem by separating them 👍

[Peeja]

Receipt Audience

The aud field of the ReceiptPayload MUST be the DID of the Invoaction Executor and be equal to sub field. This creates an authorization loop that is rooted and terminated with an Executor, which in turn can be used by anyone to prove that described state has been asserted by the Executor.

Could we have a bit more explanation here? How does this loop carry meaning? What does it mean that the Issuer (either the Executor or their deputy) has addressed the Executor here? Anyone may address anyone, so it doesn't provide any further evidence that the Executor has stated something; that comes entirely from the Issuer being the Executor, or from the Executor's trust in some deputy issuing assertions on its behalf via delegation.

I would have assumed that the audience would be either some Principal who particularly needs to know about the facts of the assertion (such as the Issuer of the original Invocation), or null, since that's a valid iss as well.