Shielded Kudos Pt. 3: KL constraints

Applications
1

This post aims to describe the KL logic constraints of the Kudos Application Design from this post. It doesn’t include Receive constraints, Intent constraints, or DL examples.

Kudos resource structure
logic KL logic VK
label DL logic VK
value Owner PK
  • DL might require additional fields in the label and value. For that reason, we assume label and value openings being maps, but from the KL perspective, so far, only one sub-field is needed for each (I might have missed something).

Constraints

Depending on the sort of the self resource’s tag type and ephemerality, it can only be a part of certain functions. For example, ephemeral resources are created only in Burn.

image
image812×780 15 KB

Persistent resources can be a part of different functions. The diagram below describes how to differentiate between them.

image
image2844×977 176 KB

1. Issue (required resources in the action: 3, kudo resources: 2)

  1. The DL is triggered[1]:
    1. There is a resource R_{DL} in the same action s.t. R_DL.logic = self.label.dl_vk
  2. If self is consumed:
    1. self.is_ephemeral = True
    2. There is another created resource R_K in the transaction s.t.:
      1. R_K.logic = self.logic
      2. R_K.label.dl_vk = self.label.dl_vk[2]
      3. R_K.is_ephemeral = False
  3. If self is created:
    1. self.is_ephemeral = False
    2. There is another consumed resource R_K in the transaction s.t.:
      1. R_K.logic = self.logic
      2. R_K.label.dl_vk = self.label.dl_vk
      3. R_K.is_ephemeral = True

2. Burn (required resources in the action: 3, kudo resources: 2)

  1. DL is checked

    1. there is a resource R_{DL} in the same action s.t. R_DL.logic = self.label.dl_vk

  2. If self is created:

    1. self.is_ephemeral = True
    2. There is another consumed resource R_K in the transaction s.t.:
      1. R_K.logic = self.logic
      2. R_K.label.dl_vk = self.label.dl_vk
      3. R_K.is_ephemeral = False

  3. If self is consumed:

    1. self.is_ephemeral = False
    2. There is another created resource R_K in the transaction s.t.:
      1. R_K.logic = self.logic
      2. R_K.label.dl_vk = self.label.dl_vk
      3. R_K.is_ephemeral = True

3. Transfer (required resources in the action: 4, kudo resources: 2)

  1. DL is checked
    1. there is a resource R_{DL} in the same action s.t. R.logic = self.label.dl_vk
  2. If self is created:

    1. self.is_ephemeral = False

    2. There is another consumed resource R_K in the transaction s.t.:

      1. R_K.logic = self.logic
      2. R_K.label.dl_vk = self.label.dl_vk
      3. R_K.is_ephemeral = False

    3. Receive logic is triggered:

      1. There is another created resource R_{receive} in the transaction s.t.:
        1. Signature.Verify(Sig,R_receive.logic, self.value.owner) = True
  3. If self is consumed:
    1. self.is_ephemeral = False
    2. There is another created resource R_{K} in the transaction s.t.:
      1. R_K.logic = self.logic
      2. R_K.label.dl_vk = self.label.dl_vk
      3. R_K.is_ephemeral = False

4. Swap (required resources in the action: 3, kudo resources: 1)

  1. DL is checked

    1. there is a resource R_{DL} in the same action s.t.:
      1. R_DL.logic = self.label.dl_vk

  2. self.is_ephemeral = False

  3. isConsumed = True

  4. Intent logic is triggered:

    1. There is another created resource R_I in the transaction s.t.:
      1. Signature.Verify(Sig, R_I.logic, self.value.owner) = True

Instances and Witnesses

  • Instance:
    • as specified in the specs
    • action.applicationData[tag] contains:
      • For Transfer: the signature over the receive logic (1.4)
      • For Swap: the signature over the intent logic (1.2)[3]
  • Witness:
    • We only need the resource objects

Action sizes

We often like to think of actions as data structures of arbitrary size, but in the shielded case the circuit can take only a limited amount of resources in the action since the circuit is fixed. One approach would be to fix the expected amount of resources in the action to the minimal necessary, another - to set an upper bound. The first option makes verification a bit easier: there are not a lot of resources to go through. One thing we need to keep in mind is that the same logic governs different functions (Issue, Burn, Transfer, Swap), and some of them require less resources. We need to make sure this cannot be exploited. The upper bound approach gives us a bit more programmability, but makes the verification a bit more difficult: more resources - more processing + more opportunities to exploit the structure (if flawed).

In the post I specified the minimal amount of resources required, but didn’t make an explicit decision about the approach to take.

Redundancy

It is possible that the constraints can be simplified. I didn’t try to optimise for that.

  1. this is a check that must be present in all transaction functions ↩︎

  2. since right now label only contains DL VK, this comparison is equivalent to comparing labels. I’m not sure if there is a case when we want to allow different labels with the same DL VK to interoperate, but I decided to be specific just in case. Note that in that case the balance would have to be taken care of explicitly in the logic since the delta check wouldn’t work for resources of different kinds. ↩︎

  3. We might want to move the signatures to the resources, as described here, which would be convenient, but I didn’t think much about it yet. ↩︎