Intent Languages: CSP Formulation

Protocol Design
22

Multi Agent, Multi Resource Swaps with Intents

Condensing the above discussion, I propose the following, mostly written out examples of a generalized swap Intents.

Preliminary: Authentication

Here we introduce a simple two party, two resource swap with consumption authentication via signatures in ephemeral resources. The authentication is not relevant at solving time, as it is validated before and/or after search has produced candidate matches. We introduce it here, because it might be relevant context for some readers, as it defines required pre- and post-conditions, but you can skip it if you’re not interested in these mechanics.

fn can_be_consumed(self, tx: TX) -> bool {
    if tx.input_resoruces.contains("an ephemeral resource with a valid signature of the owner") {
        true
    } else {
        false
    }
}

fn auth_eph_can_be_created(self, tx: TX) -> bool {
    if TX.outputs.contains("a resource of the type which consumption this auth resource authenticated") and TX.persistent_resources.is_balanced() { // TODO: is the first statement implied in the second?
        true
    } else {
        false
    }
}

let have1 = Resource {
    res_type: A,
    quantity: 1,
    owner: agent1,
    predicate: can_be_consumed(),
    ephemeral: no,
    value: "", // The values of persistent Resources are not relevant for this example, but in general they will contain the actual state represented.
}


let auth_eph_in1 = Resource {
    res_type: consume auth for A,
    quantity: 1,
    owner: agent1,
    predicate: auth_eph_can_be_created(), // Always evaluates to true at consumption.
    ephemeral: yes,
    value: "signature over have1 by agent1"
}

let want1 = Resource {
    res_type: B,
    quantity: 1,
    owner: agent1,
    predicate: can_be_consumed()
    ephemeral: no,
    value: "",
}   // can_be_consumed() will always evaluate to true on creation. Balance checking, which always happens, ensures that only the same amount of resources per type get created as were consumed.


let have2 = Resource {
    res_type: B,
    quantity: 1,
    owner: agent2,
    predicate: can_be_consumed(),
    ephemeral: no,
    value: "",
}

let auth_eph_in2 = Resource {
    res_type: consume auth for B,
    quantity: 1,
    owner: agent2,
    predicate: auth_eph_can_be_created(),
    ephemeral: yes,
    value: "signature over have2 by agent2"
}

let want2 = Resource {
    res_type: A,
    quantity: 1,
    owner: agent2,
    predicate: can_be_consumed(), 
    ephemeral: no,
    value: "",
}


// Now the following two PTXs get, amongst others, submitted to a solver.

let ptx1 = PTX {
    input_resources: [have1, auth_eph_in1],
    output_resources: [want1],
    term: "create auth_eph_out1 in this ptx after solving"
}
let ptx1 = PTX {
    input_resources: [have2, auth_eph_in2],
    output_resources: [want2],
    term: "create auth_eph_out2 in this ptx after solving"
}

// All predicates (here can_be_consumed()) of all Resources in a PTX are evaluated before solving. A PTX is only accepted into a batch if all of its Resource Predicates evaluate to 'true'.

// In this example, the solver matches up ptx1 and ptx2, since want1 + have2, and have1 + want2 produce a satisfying assignment. The only information relevant for search by the solver in this batch are these persistent Resources.

// Once a TX has been bundled from PTXs, the solver creates auth_eph_out1 and auth_eph_out2 as indicated by the terms.

let auth_eph_out1 = Resource {
    res_type: consume auth for A,
    quantity: 1,
    owner: agent1,
    predicate: auth_eph_can_be_created(),
    ephemeral: yes,
    value: "",
}

let auth_eph_out2 = Resource {
    res_type: consume auth for B,
    quantity: 1,
    owner: agent2,
    predicate: auth_eph_can_be_created(),
    ephemeral: yes,
    value: "",
}

// Once this is done, all Predicates (here auth_eph_can_be_created()) of all Resources in the TX get evaluated again, on the context of the TX and balance is checked. If all these evaluate to 'true' the TX is handed on to consensus for validation.

Example: Multi Agent, Multi Resource swap with fixed Resources and one Linear Preference

Let us now move to a Multi Agent, Multi Resource swap. We leave out the details of the consumption authentication introduced above and focus only on the machinery relevant to intents and solving for them. We also omit data fields of Resources and PTXs when not required for explanation. The following example will be one, where all Input and Output resources are uniquely specified and persistent, with one party expressing a preference over the amounts they give up for consumption.

// agent1
let have1 = Resource {
    res_type: A,
    quantity: 4,
    owner: agent1,
}
let want1 = Resource {
    res_type: B,
    quantity: 1,
    owner: agent1,
}

// agent2
let have2 = Resource {
    res_type: C,
    quantity: 2,
    owner: agent2,
}
let want2 = Resource {
    res_type: A,
    quantity: 4,
    owner: agent2,
}

// agent3
let have3 = Resource {
    res_type: B,
    quantity: 4,
    owner: agent3,
}
let want3 = Resource {
    res_type: C,
    quantity: 2,
    owner: agent3,
}
fn linear_preference3(tx: TX) -> scalar {
    "prefer minimizing C given away, with linear utility, by splitting up want3 and sending the remainder back"
}

let ptx1 = PTX { 
    input_resources: [have1],
    output_resources: [want1],
}

let ptx2 = PTX { 
    input_resources: [have2],
    output_resources: [want2],
}

let ptx3 = PTX { 
    input_resources: [have3],
    output_resources: [want3],
    welfare_function: linear_preference3(),
}


// The above PTXs get submitted to the solver and it produces the following TX fulfilling their intents, after updating the PTXs as follows. 
// Since ptx3 contains a linear preference, which is not in conflict with other constraints or preferences, it enables the solver to locally optimize the assignment to lead to a better outcome for agent3.
// Should conflicts arise, they can be resolved by weighting whole PTXs, either by querying a trust database or offering rewards to the solver, by which the clauses of the CSP instantiated by any given PTX can be weighted. 

let have3' = Resource {
    res_type: B,
    quantity: 3,
    owner: agent3,
}
let ptx3' = Resource {
    input_resources: [have3],
    output_resoruces [have3', want3],
    term: term3,
}

let tx = TX {
    ptxs: [ptx1, ptx2, ptx3']
}

Example: Multi Agent, Multi Resource Swap with non-fixed Resources and Linear Preferences

To further generalize the above, we introduce a preference over a partially determined resource collection.

// agent1
let have1A = Resource {
    res_type: A,
    quantity: 4,
    owner: agent1,
}
let have1B = Resource {
    res_type: B,
    quantity: 2,
    owner: agent1,
}
fn linear_preference1(tx: TX) -> bool {
    "prefer giving away 2.5A over 1B and send the remainder back"  
}
let want1 = Resource {
    res_type: E,
    quantity: 2,
    owner: agent1,
}
let ptx1 = PTX { 
    input_resources: [have1A, have1B],
    output_resources: [want1],
    term: term1,
    welfare_function: linear_preference1()
}

// agent2
let have2 = Resource {
    res_type: C,
    quantity: 4,
    owner: agent1,
}
let want2 = Resource {
    res_type: E,
    quantity: 2,
    owner: agent1,
}
let ptx2 = PTX { 
    input_resources: [have2],
    output_resources: [want2],
}

// agent3
let have3 = Resource {
    res_type: E,
    quantity: 4,
    owner: agent2,
}
fn resource_preference3(tx: TX) -> bool {
    if tx.output_resources.contain("(2A || 1B) && (1C || 1D) each with owner == agent2") {
        true
    } else {
        false
    }
}
let want_pref_eph_out3 = Resource {
    res_type: "preference for resource",
    quantity: 1,
    owner: agent3,
    predicate: resource_preference3()
    ephemeral: yes,
}
let term3 = Term {
    term: "create want_pref_eph_in3 for balance check after matching",
}
let ptx3 = PTX { 
    input_resources: [have3],
    output_resources: [want_pref_eph3],
    term: term3,
}


// The solver searches according to the PTX structure, with additional constraints given by lin_pref_eph_in1 and res_pref_eph_in3 updates ptx1 as follows:
let have1A' = Resource {
    res_type: A,
    quantity: 2,
    owner: agent1,
}
let ptx1' = PTX {
    input_resources: [have1A], // TODO: When do the ephemeral resources for preferences get consumed? 
    output_resources: [want1, have1B, have1A'], // have1B technically is a different resource after consumption and creation, but it is of the same type and amount
    term: term1,
}

// And ptx3 as follows, as indicated by the preference predicate and the term:
let want3A = Resource {
    res_type: A,
    quantity: 2,
    owner: agent3,
}
let want3C = Resource {
    res_type: C,
    quantity: 1,
    owner: agent3,
}
let ptx3' = PTX {
    input_resources: [have3, want_pref_eph_in3],
    output_resources: [want3A, want3C, want_pref_eph_out3],
    term = term3,
}

let tx = TX {
    ptxs: [ptx1', ptx2, ptx3']
}

Distinguishing between Predicates for Validation and Solving

As we have seen, some predicates will be only relevant for validation, which happens before and after solving time, and some predicates will be relevant during solving time, as they encode constraints. We probably want to implement them with different recognizable (at parsing time) subsets of the predicate language.