Dhvani Patel

PODs Explained

Background

When you write a regular program, you can run it and get an output. There is a special type of program called a zero-knowledge program, where running it not only produces the program output but an associated proof. The proof output can be given to others to convince them that the program output came as a result of running the program, without them having to see the inputs or re-run the program.

Introduction

0xPARC has built the POD framework to make it easy to write and use these special provable programs, or “proven computation”. The output of these provable programs can be thought of as provable object data (POD). The user can choose which parts of the input data to make public or keep private.

The framework comes with a simple way to produce PODs via signed data and also allows developers to write custom programs. Once you have a POD, the framework has a language, PODLang, which allows users to make claims about those PODs and produce new ones. In this way, PODLang is another way to create PODs.

Supported Data Types

The following data types are currently supported:

  • Integer (64 bit signed)
  • Bool
  • String
  • “Raw” 256-bit value
  • Dictionary
  • Array
  • Set

Signed Data

If you have a signed piece of data that is in JSON format (constrained to the above types), then you can produce PODs which hold claims about the data.

For example, if you have an event ticket JSON which has been signed by the ticket issuer’s public key, you can prove to someone that you went to this event without revealing your ticket id or how much you paid for it.

Custom Programs

To write a custom program that produces a POD, you have to write your program as a Plonky2 circuit that follows the interface required by the framework.

An example is this proof of work program which outputs a POD claiming how much proof of work was done and the resulting proof of work hash.

PODLang

PODLang allows you to create PODs which are claims about the values of some data (this data could be another POD!).

The language supports a number of logical operations, which produce a statement.

An example is the EqualFromEntries operation which allows you to produce an Equal statement. For example, you could claim that you have two tickets that were both held in the same venue by making a statement that their venue_id data field is equal (eg Equal(ticket1.venue_id, ticket2.venue_id)).

You can see the other supported operations here.

Another primitive in the framework is a predicate, which allows for more complex logical relations. A predicate is a collection of statements grouped together, and defined as either a conjunction (AND) or disjunction (OR).

The framework currently supports up to five statements, but a predicate can also be made up of other predicates to define more complex relations.

Example

Here is an example of a predicate definition:

ItemDef(item, ingredients, inputs, key, work) = AND(
    DictContains(ingredients, "inputs", inputs)
    DictContains(ingredients, "key", key)
    HashOf(item, ingredients, work)
)

DictContains is a native statement (ie produced by a native operation in the framework) that takes a dictionary, a key, and a value, and verifies that the dictionary contains the key-value pair.

HashOf is a native statement that takes a hash, and two inputs, and verifies that the hash is a hash of the inputs.

This ItemDef definition is defined as a conjunction of two DictContains statements and one HashOf statement. A user can thus produce an ItemDef POD by providing the 5 required inputs.

The proof will state:

  • The ingredients input has a key inputs which matches the inputs input
  • The ingredients input has a key key which matches the key input
  • The item input is a hash of the ingredients input and the work input.

Another way to see this is that you can prove to someone that you have the following:

ingredients = {
  key: key,
  inputs: inputs,
  ... (there may be other key-values)
}
work = "" (some bits of data)
item = hash(ingredients, work)

Now let’s look at another predicate that requires the ItemDef predicate we just saw as an input. Note that an application can give semantic meaning to these PODs by naming them as we will see here.

An application defines a stone predicate as follows:

use intro Pow(count, input, output) from 0x3493488bc23af15ac5fabe38c3cb6c4b66adb57e3898adf201ae50cc57183f65 // powpod vd hash

IsStone(item, private: ingredients, inputs, key, work) = AND(
    ItemDef(item, ingredients, inputs, key, work)
    Equal(inputs, {})
    DictContains(ingredients, "blueprint", "stone")
    Pow(3, ingredients, work)
)

The only new statement here is the Pow statement. This is an example of how you can write a custom program and require it as a statement in the predicate definition.

We see a new keyword here “private”. Remember the framework allows the user to choose which parts of the data to make public or private. Here the user is making only the item input public and the rest private. Previously, in ItemDef all the inputs were public.

Here the proof will state:

All the statements from ItemDef we saw before:

  • The ingredients input has a key inputs which matches the inputs input
  • The ingredients input has a key key which matches the key input
  • The item input is a hash of the ingredients input and the work input.

Plus:

  • The inputs input is an empty dictionary
  • The ingredients input has a key blueprint with a value of stone
  • Running proof of work 3 times using ingredients as a seed produces the work output

So now, you can see that a user can produce a stone POD and give this to a user who will learn that the user has a stone item identified with a particular hash.

item = 0x1234 = hash(ingredients, work)
ingredients = {
  key: key,
  inputs: {},
  blueprint: "stone",
  ... (there may be other key-values)
}
work = "" (a proof of work hash with '3' amount of work)

You can see that the key, work, and potentially other fields on ingredients data is kept private. While the item hash, the inputs field, and blueprint field is public.

Conclusion

An application can define its own predicate definitions and publish them for users. Users can then locally produce these PODs and interact with other users. The recursive nature allows for an interesting tree of PODs to be produced (eg IsAxe POD that requires an IsStone as an input).

How to coordinate user interactions and prevent “double spending” of PODs is not discussed here. For example, an application might want to require that an IsStone POD be consumed and not usable again after it’s used once to create an IsAxe POD. An implemented proof of concept can be seen here.

Another way to think of these PODs is as digital objects.