How to quantify nested property on smart contract?

[syuhei176]

The topic I wanna clarify in this issue is about predicate design. And I believe PG know the same difficulty. In short, how quantifier quantify inner properties.

Simple example.

I describe the problem using simple example below.

claim(b) :=
For All blockNumber Such That blockNumber < b:
  FooPredicate(blockNumber)

In this formulation, when FooPredicate(1) and FooPredicate(2) are True, claim(3) is True.

The property for client.

{
  decider: ForAllSuchThatDecider,
  input: {
    quantifier: LessThanQuantifier,
    quantifierParameters: b,
    propertyFactory: (blockNumber) => {
      return  FooDecider(blockNumber)
    }
  }
}

The claim for Universal Adjudicator contract.

Claim = {
    predicate: FOR_ALL_SUCH_THAT,
    input: {
        quantifier: LESS_THAN_QUANTIFIER,
        quantifierParameters: b,
        innerProperty: {
          predicate: FooPredicate,
          input: bb // blockNumber
        }
    }
}

let's say, now Alice called claimProperty with b=5.
Anyone can prove contradiction showing "FooPredicate(1) is False". Let's say Bob prove contradiction.
Bob should send the claim like below. It means bb must be less than 5, but isn't constant value.

{
  predicate: FooPredicate,
  input: 1
}

Problem

bb in claim is not constant value but variable. So we should express variable inside innerProperty.
And LessThanQuantifier should verify bb which is used in "innerProperty" is less than upperBound.

note: quantify was called from FOR_ALL_SUCH_THAT.quantify, and FOR_ALL_SUCH_THAT.quantify was called from verifyImplication.

If we implement LessThanQuantifier, quantify should check

• _toQuantify should be same as _parameters.innerProperty applied bb
• bb should be less than parameter.upperBound.

contract LessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
        // `bb` inside _parameters.innerProperty should be less than _parameters.upperBound
      let bb = _implicationProofElement
      assert(bb < _parameters.upperBound)
      // should check that _parameters.innerProperty(bb) and _toQuantify are same property
    }
}

Solutions?

I'm looking for appropriate solution for this. these are my very rough ideas but I have no concrete solutions yet.

Are there any ways to make innerProperty the function returning property?

Can we use create2?

contract LessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
      let bb = _implicationProofElement.bb
      assert(bb < _parameters.upperBound)
      check_equality(_parameters.innerProperty(bb), _toQuantify)
    }
}

innerProperty is reducer?

contract LessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
      let bb = _parameters.innerProperty.reduce(_toQuantify)
      assert(bb < _parameters.upperBound)
    }
}

Specific quantifier?

contract SpecificLessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
      assert(_toQuantify.input[0].predicate == FooPredicate)
      assert(_toQuantify.input[0].input.bb < _parameters.upperBound)
    }
}

[ben-chain]

Great question!! This definitely needs to be addressed somehow, and I'm not sure of the best approach either.

Create2 is an interesting idea--but I'm not sure if it changes the underlying problem--even if create2 allows us to not deploy the contract up front, we still need to know the underlying bytecode.

I think the second two approaches both work, but clearly they are a little annoying to do. In fact "specific quantifier" is how we did it in some examples in the original contract spec attempt, but the propertyFactory was easier to do in the client.

Speaking of propertyFactory, what do you think of literally recreating the propertyFactory on the contract side? That is, something like:

type ForAllSuchThatInput = {
   quantifier: address,
   propertyFactory: address
}
contract ForAllSuchThat {
   function verifyImplication(_input: ForAllSuchThatInput, _implication: ImplicationProofElement) {
       require(_input.quantifier.quantify(_implication.witness))
       require(_input.propertyFactory.constructProperty(_implication.witness) == _implication.property)
   }
}

I'd be curious how you think this approach compares! :) It would probably be the closest way to match how it's done on the client. However, I'm not sure that it solves the main issue here, which is: is it possible to do this functionality without writing new solidity? The problem with all of these is that it requires new developers to potentially audit new code. Do you agree this is the biggest issue?

[syuhei176]

Thank you for replying!

However, I'm not sure that it solves the main issue here, which is: is it possible to do this functionality without writing new solidity? The problem with all of these is that it requires new developers to potentially audit new code. Do you agree this is the biggest issue?

Yes, I think this is big issue. and I feel trade-off between extensibility and security ;;)
And for "propertyFactory on the contract side" way, I think we need only a few propertyFactories for Plasma. However, we should write new solidity for any other claims except Plasma. I believe it's application specific.

After a little thought, I think we need a more limited expression than propertyFactory.
I think the straight way is that "Propagating parameters without property Factory.", similar to flow based programming. credit @nakajo2011 and @tkmct

This is just example.

OVM claims without propertyFactory

An example claim

claim([A, B]) :=
(params = [A, B]) => {
  ForAllSuchThat(
    LessThanQuantifier(params.0),
    (params = [a, B]) => {
      ForAllSuchThat(
        LessThanQuantifier(params.1),
        (params = [a, b]) => {
           And(
             FooPredicate(params.0),
             BarPredicate(params.1)
           )
        }
      )
    }
  )
}

In this claim, any property don't use parameters across property.(property don't use ancestor's parameter, but use parent's parameter).
So, can serialize this claim without propertyFactory.

Claim as JSON

"parameters" defines initial parameters for Property.
ForAllSuchThat predicate add new parameter in right.
we can get quantified a by [2] and b by [3].

{
  "parameters": [A, B],
  "predicate": ForAllSuchThat,
  "quantifier": [LessThanQuantifier, 0],
  "innerProperty": {
    "predicate": ForAllSuchThat,
    "quantifier": [LessThanQuantifier, 1],
    "innerProperty": {
      "predicate": And,
      "input": [
        { "predicate": FooPredicate, "input": [2] },
        { "predicate": BarPredicate, "input": [3] }
      ]
    }
  }
}

Predicate Implementation

type ForAllSuchThatInput = {
   quantifier: address,
   quantifierParameters: uint[],
   innerProperty: bytes
}
contract ForAllSuchThat {
   function verifyImplication(_property: Property, _implication: ImplicationProofElement) {
       let _input: ForAllSuchThatInput = _property.input;
       require(_input.quantifier.quantify(
           _input.quantifierParameters,
           _property.parameters,
           _implication.parameters[_property.parameters.length])) // output is most right side
       require(_input.innerProperty == _implication.property)
   }
}
contract LessThanQuantifier {
    quantify(_parameterIndex: uint[], _inputParams: bytes[], _outputParam: bytes) {
        let upperBound = _inputParams[_parameterIndex[0]];
        return _outputParam < upperBound;
    }
}

And should modify 1 line of UDC contract and data structure of Property.

Property = {
    parameters: bytes[], // concrete parameters for property
    predicate: address,
    input: bytes,
}

verifyImplicationProof(_rootPremise: Property, _implicationProof: ImplicationProof): bool {
    // ...
    for (const i = 0; i < _implicationProof.length - 1; i++;) {
        premise: ImplicationProofElement = _implicationProof[i]
        implication: ImplicationProofElement = _implicationProof[i+1]
        // check white list
        require(premise.implication.parameters == implication.implication.parameters)
        require(premise.predicate.verifyImplication(premise.implication.input, implication))
    }
}

I think there are more good expression, but what do you think intuitively? @ben-chain

[ben-chain]

I think this could be a good direction, however I am a little confused by the code.

For example in the last section, the line require(premise.implication.parameters == implication.parameters) is confusing--what is the type of ImplicationProofElement in this scheme? What is implication.parameters?

[syuhei176]

Sorry! My fault. That is

require(premise.implication.parameters == implication.implication.parameters)

[ben-chain]

This is starting to make more sense, it definitely feels like the start of a reasonable solution. 😃

More questions--is the parameters array meant to be increasing as more verifyDependency checks are made? Or is it meant to be initialized with the full [A, B, a, b]? It seems like

           _implication.parameters[_property.parameters.length])) // output is most right side

suggests that it is growing, but wouldn't

require(premise.implication.parameters == implication.implication.parameters)

prevent it from growing?

Also considering other naming choices here--we are probably overusing "parameters" . Perhaps something relating to free or bound variables?

Second point--in the JSON example we have:

"innerProperty": {
      "predicate": And,
      "input": [
        { "predicate": FooPredicate, "input": [2] },
        { "predicate": BarPredicate, "input": [3] }
      ]
    }

Does this mean that FooPredicate and BarPredicate are built to understand their input is the index of a value in parameters? If so, it would be good to try to avoid this--so that predicates can be built independent from variable substitution. In general, I would be interested to see how you would write out the contract for AND for the Foo and Bar example above.

[syuhei176]

Answer 1

Sorry! A line below would be more like forward_match rather than check_equality.

require(premise.implication.parameters == implication.implication.parameters)

require(check_forward_match(premise.implication.parameters, implication.implication.parameters))

function check_forward_match(a: bytes[], b: bytes[]) {
  for(let i = 0; i < a.length;i++) {
    if(a[i] != b[i]) return false;
  }
  return true;
}

So, parameter array is growing.

Also considering other naming choices here--we are probably overusing "parameters" . Perhaps something relating to free or bound variables?

Agree! "the parameters" seems to be bound variables for a property. boundVariables is better?

Answer 2

Does this mean that FooPredicate and BarPredicate are built to understand their input is the index of a value in parameters?

Yes, actually I was thinking to build like that(predicate understand their inputs is the index). But finally claim was decided as Property without index of boundedVariables.
Let's say FooPredicate is PreimageExistsPredicate.
I wrote code for verifying PreimageExistsPredicate(preimage) from boundedVariables=(_, ... , preimage), (boundedVariables)=> PreimageExistsPredicate(boundedVariables) as verifyImplication method of PreimageExistsPredicate.

Codes

ANDPredicateInput = [Property, Property]
ANDImplicationWitness = 0 | 1

verifyImplication(_andProperty: Property, _implicationProofElement: ImplicationProofElement): bool {
    implication =  _implicationProofElement.implication
    indexInAND: ANDImplicationWitness = _implicationProofElement.witness
    if (_andProperty.predicate == implication.predicate) {
      // check "vals=[p0, p1], (vals) => and(vals.0, vals.1)" -> "and(p0, p1)"
      require(_andProperty.input[0].evaluate(_andProperty.boundedVariables) == implication.input[0])
      require(_andProperty.input[1].evaluate(_andProperty.boundedVariables) == implication.input[1])
    } else {
      // parameters don't grow in AndPredicate
      require(_andProperty.parameters.length == implication.parameters.length)
      return (_andProperty.input[indexInAND] == Property({predicate: implication.predicate, input: implication.input}))
    }
}

decideTrue(_leftDecidedRootProperty: Property, _leftImplicationProof: ImplicationProof, _rightDecidedRootProperty: Property, _rightImplicationProof: ImplicationProof) {
    require(_leftDecidedRootProperty.boundedVariables == _rightDecidedRootProperty.boundedVariables)
    decidedExistsProperty: Property = {
            _property.boundedVariables: _leftDecidedRootProperty.boundedVariables,
            predicate: this.address,
            input: [Property({
              predicate: _leftDecidedRootProperty.predicate,
              input: _leftDecidedRootProperty.input
            }), Property({
              predicate: _rightDecidedRootProperty.predicate,
              input: _rightDecidedRootProperty.input
            })]
    }
    MANAGER.decideProperty(decidedExistsProperty, true)
}

PreimageExistsPredicateInput = {
    verifier: address,
    hash: bytes
}

contract PreimageExistsPredicate {
    decidePreimageExistsTrue(_input: PreimageExistsPredicateInput, 
    _witness: bytes) {
        require(_input.verifier.verify(_input.hash, _witness))
        decidedExistsProperty: Property = {
            predicate: this.address,
            input: [_input.hash]
        }
        MANAGER.decideProperty(decidedExistsProperty, true)
    }
    // verify "vals=[..., preimage], (vals) => PreimageExists(vals[self.input])" -> "PreimageExists(preimage)"
    verifyImplication(
      _property: Property,
      _implicationProofElement: ImplicationProofElement
    ): bool {
      require(_property.predicate == implication.implication.predicate)
      require(_property.boundedVariables[_property.input[0]] == implication.implication.input[0])
    }
}

[ben-chain]

Sorry for slow response here--yes, I like boundVariables! 😃

A few questions about this code:

• I do not understand the if...else in AND.verifyImplication. Is the idea that we use verifyImplication twice, first to replace bound vars, and second to select left or right side?
• What is the function evaluate? Is this what replaces indices with bound variables? If so, why not always do this (if no bound vars to replace, evaluate does nothing) and then remove the if...else discussed in the line above?
• In this line:
  require(_andProperty.parameters.length == implication.parameters.length)
  Do you mean boundVariables when you say parameters?
• I see near the bottom ... _property.input[0] ... But the input type is not an array. Do you think we need to make all inputs be arrays? I have definitely thought before that making all inputs arrays would help with propertyFactory.

[syuhei176]

Sorry for slow response here--yes, I like boundVariables! 😃

OK! I'll use boundVariables!

• I do not understand the if...else in AND.verifyImplication. Is the idea that we use verifyImplication twice, first to replace bound vars, and second to select left or right side?

Yes, right. Your understanding is correct.

• What is the function evaluate? Is this what replaces indices with bound variables? If so, why not always do this (if no bound vars to replace, evaluate does nothing) and then remove the if...else discussed in the line above?

Sorry, mistake. I should use verifyImplication instead of evaluate.
Yes, at first I was using evaluate to replace indices, but I think verifyImplication can realize same thing.

verifyImplication(_andProperty: Property, _implicationProofElement: ImplicationProofElement): bool {
    implication =  _implicationProofElement.implication
    indexInAND: ANDImplicationWitness = _implicationProofElement.witness
    if (_andProperty.predicate == implication.predicate) {
      let left: Property = {predicate: _andProperty.input[0].predicate, input: _andProperty.input[0].input, boundVariables: _andProperty.boundVariables}
      let right: Property = {predicate: _andProperty.input[1].predicate, input: _andProperty.input[1].input, boundVariables: _andProperty.boundVariables}
      require(left.verifyImplication({implication: implication.input[0]}))
      require(right.verifyImplication({implication: implication.input[1]}))
    } else {
      // parameters don't grow in AndPredicate
      require(_andProperty.parameters.length == implication.parameters.length)
      return (_andProperty.input[indexInAND] == Property({predicate: implication.predicate, input: implication.input}))
    }
}

• In this line:
  require(_andProperty.parameters.length == implication.parameters.length)
  Do you mean boundVariables when you say parameters?

Yes, I mean boundVariables. I forgot to replace all ;;)

• I see near the bottom ... _property.input[0] ... But the input type is not an array. Do you think we need to make all inputs be arrays? I have definitely thought before that making all inputs arrays would help with propertyFactory.

Sorry that was also mistake. _property.input[0] would be _property.input.hash.
I think it's not necessary to make all inputs arrays, but the code may be easy to reuse by array.

for example

for(i in 0..5) {
    require(_property.boundedVariables[_property.input[i]] == implication.input[i])
}

[ben-chain]

Cool, makes sense!

I'm curious, what's the motivation for embedding inside verifyImplication? I actually feel like it might be easier to understand as an evaluation--is the intermediate step really a "dependency"?

This is feeling like a good direction, though--I think you are right and arrays just help reuse code. As long as the boundVariables interpretation is standardized, the predicate can have different code for replacing each part of the struct. 😃

[willmeister]

Sorry that it's taken me this long to catch up! I like what you describe with boundVariables, evaluate, and the general representation. I wonder if we can tweak it so that boundVariables is global for all descendants instead of relative in a growing array?

Would something like this work?

JSON Claim:

{
  "decider": ForAllSuchThatDecider,
  "input": {
    "quantifier": BlockLessThanQuantifier,
    "quantifierParameters": {
      "blockNumber": 10
    },
    "transformer": undefined,    // Can just omit in this case
    "quantifiedPlaceholder": "$$block$$"
    "property": {
      "decider": AndDecider,
      "input": {
        "properties": [
          {
            "decider": ForAllSuchThatDecider,
            "input": {
              "quantifier": SignedByQuantifier,
              "quantifierParameters": {
                "publicKey": "0x0a",
                "channelID": "1234567890" 
              },
              "transformer": SignedToStateChannelMsg,
              "quantifiedPlaceholder": "$$message$$"
              "property": {
                "decider": MessageNotInBlockDecider,
                "input": {
                  "message": "$$message$$"
                  "block": "$$block$$"
                }
              }
            }  
          },
          {
            "decider": BlockFinalizedDecider,
            "input": {
              "block": "$$block$$"
            }
          }
        ]
      }
    },
  }
}

Contract:

struct Property {
    address decider;
    mapping(string => bytes) input;
}

struct ForAllSuchThatInput {
    address quantifier; 
    mapping(string => bytes) quantifierParameters;
    address transformer;
    string quantifiedPlaceholder;
    Property property;
}

contract Decider {
    function getInputKeys() public view returns (string[]);
    function decide(mapping(string => bytes) _input) public returns (boolean);
}

contract ForAllSuchThatDecider is Decider {

    string[5] private inputKeys = [
        'quantifier', 
        'quantifierParameters', 
        'transformer',
        'quantifiedPlaceholder',
        'property'
    ];

    function getInputKeys() public view returns(string[]) {
        return inputKeys;
    }

    function decide(mapping(string => bytes) _input) public returns (boolean) {
        return decide(getInputFromMap(_input));
    }

    function decide(ForAllSuchThatInput _input) public returns (boolean) {
        bytes[] memory quantified = Quantifier(_input.quantifier).quantify(_input.quantifierParameters);
        bytes[] memory transformed = (_input.transformer != address(0)) 
            ? Transformer(_input.transformer).transform(quantified) 
            : quantified;
      
        for(uint i = 0; i < transformed.length i++) {
            Property memory prop = createProperty(_input.property, _input.quantifiedPlaceholder, transformed[i]);

            Decision memory decision = Decider(prop.decider).decide(prop.input);
            // TODO: process decisions in a for-all-such-that manner.
        }
    }
    
    function getInputFromMap(mapping(string => bytes) _map) public returns (ForAllSuchThatInput memory) {
        // TODO: parse and populate (part of decider interface)
        // Note: any sub-properties' input will remain as mapping(string => bytes)
    }
   
    function createProperty(Property _template, string _placeholder, bytes _replacement) private returns (Property prop memory) {
        prop = cloneProperty(_template);   // Assume this function exists.
        for (uint i = 0; i < prop.getInputKeys().length; i++) {
            string key = prop.getInputKeys()[i];
            if (key == 'property') {
                prop.input['property'] = createProperty(prop.input['property'], _placeholder, _replacement);
                continue;
            }
            
            if (key == 'properties') {
                for (int j = 0; j < prop.input['properties'].length; j++) {
                    prop.input['properties'][j] = createProperty(prop.input['properties'][j], _placeholder, _replacement);
                }
                continue;
            }
        
            if (prop.input[key] == _placeholder) {
                prop.input[key] = _replacement;
            }
        }
    }
}

[ben-chain]

Nice, I think this is a promising direction @willmeister ! @syuhei176 Curious how you would compare to an "external" boundVariables 😃

As a separate note, I just thought of another example of a related use we may want:
When we define ExampleProperty(x,y,z) := A(x) AND B(y) AND C(z) we might prefer to submit the claim ExampleClaim(x,y,z) without immediately converting to save on gas cost.

[syuhei176]

I like what you describe with boundVariables, evaluate, and the general representation. I wonder if we can tweak it so that boundVariables is global for all descendants instead of relative in a growing array?

@willmeister Thank you for replying! I don't have idea but I believe some optimizations are possible to prevent growing array.
And the way to create property using template literal is great! I think this needs less call-data than the way to use boundVariables.

@ben-chain I think the difference between 2 approaches are call-data size to propagate variables and number of function calls to create property. And I feel the template literal for property approach is good and simpler as the first approach. 😃

I'm also interested in the componentization of the predicate! But I'm still not sure how can challengers prove contradiction of ExampleProperty(x, y, z) showing Not(A(x)).
Can ExampleProperty(x, y, z) verify the implication(or dependency) to A(x)?

ExampleProperty(x,y,z) := A(x) AND B(y) AND C(z)

[ben-chain]

I'm also interested in the componentization of the predicate! But I'm still not sure how can challengers prove contradiction of ExampleProperty(x, y, z) showing Not(A(x)).
Can ExampleProperty(x, y, z) verify the implication(or dependency) to A(x)?

I think that this "transformer"/"evaluator" must be run before we verifyImplication. So for example, select specific X0, Y0, Z0 and then convert to A(X0) AND B(Y0) AND C(Z0). Then from there, we allow AND.verifyImplication and so on. Does this make sense or was the question something else?