{"action":"created","issue":{"url":"https://api.github.com/repos/mir-core/mips/issues/7","repository_url":"https://api.github.com/repos/mir-core/mips","labels_url":"https://api.github.com/repos/mir-core/mips/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/mir-core/mips/issues/7/comments","events_url":"https://api.github.com/repos/mir-core/mips/issues/7/events","html_url":"https://github.com/mir-core/mips/issues/7","id":387060301,"node_id":"MDU6SXNzdWUzODcwNjAzMDE=","number":7,"title":"Composite predicates","user":{"login":"dlubarov","id":828366,"node_id":"MDQ6VXNlcjgyODM2Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/828366?v=4","gravatar_id":"","url":"https://api.github.com/users/dlubarov","html_url":"https://github.com/dlubarov","followers_url":"https://api.github.com/users/dlubarov/followers","following_url":"https://api.github.com/users/dlubarov/following{/other_user}","gists_url":"https://api.github.com/users/dlubarov/gists{/gist_id}","starred_url":"https://api.github.com/users/dlubarov/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dlubarov/subscriptions","organizations_url":"https://api.github.com/users/dlubarov/orgs","repos_url":"https://api.github.com/users/dlubarov/repos","events_url":"https://api.github.com/users/dlubarov/events{/privacy}","received_events_url":"https://api.github.com/users/dlubarov/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-12-04T00:04:26Z","updated_at":"2018-12-06T05:02:23Z","closed_at":null,"author_association":"MEMBER","body":"In Zexe, it seems natural for applications to require that records have a certain standardized birth predicate, while not imposing any requirement on death predicates. An example is the token scheme described in the Zexe paper, where each token record is required to have a particular birth predicate `Φ_b` which enforces balance conservation. A token record can have any death predicate, so custom death predicates can be written to verify arbitrary signatures, enforce time locks, and so forth.\r\n\r\nHowever, a problem arises when an application needs to standardize death predicates. For example, suppose we were implementing a DEX. The natural approach would be to write a death predicate `Φ_d`, declaring \"any transaction may consume this record if it also creates X units of token Y, spendable by Z\". To submit an order, a user would move some tokens into a record with `Φ_d`, then register it in some decentralized order book.\r\n\r\nBut now that we've mandated that every token order record use both `Φ_b` and `Φ_d`, there is no room left for customization. `Φ_d` could support some standardized signature scheme, but users would lose the flexibility to use arbitrary schemes. If there were two competing DEXs using different death predicates, users would need to pick one or the other; it wouldn't be possible to offer the same tokens on two different DEXs.\r\n\r\nMaybe these limitation wouldn't be a big deal in practice, but let's explore some possible solutions.\r\n\r\n\r\n## Composite predicates\r\n\r\nIn the example above, what we want is multiple death predicates with a disjunctive relationship. Then the user could create a record with a death predicate for DEX A, another for DEX B, and another for an owner-authenticated transfer (in case the order doesn't get filled).\r\n\r\nHowever, disjunction alone does not seem sufficient. Suppose that a DEX was being overloaded with short-lived orders from market makers. To address the problem, they might want to require that orders remain in the order book for a certain time period before the funds can be transferred out. To meet this requirement, order records would need to have a death predicate structure like\r\n\r\n    order is filled OR (owner authorizes a transfer AND time lock has expired)\r\n\r\n\r\n## Composition via circuits\r\n\r\nA straightforward way to support this sort of composition would be to give each record two small logical circuits, one for birth and one for death. Each wire would be either a constant or a predicate. These circuits would be private by default; users could prove their satisfiability in zero knowledge after first proving certain predicates to be satisfiable.\r\n\r\n\r\n## Composition via plugins\r\n\r\nAnother approach would be a plugin model, where a predicate can designate certain wires in its circuit as hooks, and arbitrary subpredicates can be attached to those hooks.\r\n\r\nThis model would be more powerful in a sense, since the top-level predicate would be a full-fledged Zexe predicate with access to all the transaction data. It could require certain subpredicates only in certain contexts, depending on what the transaction was doing. For example, imagine an application where users can decide whether or not to publicly log each operation. The top-level predicate could check if there was a data command (see #3) writing to the log structure, and if so, require a subpredicate which validates the content of the log.\r\n\r\nI don't think this extra power is really necessary. In our example, the log validation subpredicate itself could check the list of data commands, and output 1 for a transaction with no logging. However, having this logic in the top-level predicate could be more performant, as users would not need to generate an argument for the log validation subpredicate if they knew that the top-level predicate would not require it.\r\n\r\nFurthermore, this approach would make it possible to replace birth and death predicates with a single predicate per record. The top-level predicate could check whether the record it cares about was being created or consumed, and potentially require different subpredicates accordingly. That said, there are some tradeoffs here and I'm not sure whether it would be a good idea overall; need to give this more thought.\r\n\r\nGoing back to our token example, a token record with a single predicate could look something like this. This is for a record holding 100 DAI, whose owner was offering it on a DEX in exchange for 10 MKR.\r\n\r\n    StandardToken(\r\n        token = \"DAI\",\r\n        units = 100,\r\n        transfer_authorization = DexOrderFilled(\r\n            ask_token = \"MKR\",\r\n            ask_units = 10,\r\n            submitted_at = \"2018-12-03\",\r\n            owner_authorization = Sha3Signature(\r\n                pk = <owner's public key>)))\r\n\r\nHere `DexOrderFilled` would allow another DEX user to claim the 100 DAI if they simultaneously transferred 10 MKR to the owner. `owner_authorization` would also be used to let the owner cancel their order, perhaps after a time lock expired.\r\n\r\n\r\n## Open questions\r\n\r\nIs the Zexe limitation significant enough to warrant nontrivial solutions like these? If so, which model would work best, circuits or plugins? If we go with the plugin model, should be keep separate birth and death predicates, or combine them?\r\n\r\nShould we generate a separate argument for each subpredicate, then compose them with recursive arguments? Or should we generate one big composite circuit, then generate a single argument for the whole thing? The answer might depend on which argument system we use."},"comment":{"url":"https://api.github.com/repos/mir-core/mips/issues/comments/444749223","html_url":"https://github.com/mir-core/mips/issues/7#issuecomment-444749223","issue_url":"https://api.github.com/repos/mir-core/mips/issues/7","id":444749223,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0NDc0OTIyMw==","user":{"login":"dlubarov","id":828366,"node_id":"MDQ6VXNlcjgyODM2Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/828366?v=4","gravatar_id":"","url":"https://api.github.com/users/dlubarov","html_url":"https://github.com/dlubarov","followers_url":"https://api.github.com/users/dlubarov/followers","following_url":"https://api.github.com/users/dlubarov/following{/other_user}","gists_url":"https://api.github.com/users/dlubarov/gists{/gist_id}","starred_url":"https://api.github.com/users/dlubarov/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dlubarov/subscriptions","organizations_url":"https://api.github.com/users/dlubarov/orgs","repos_url":"https://api.github.com/users/dlubarov/repos","events_url":"https://api.github.com/users/dlubarov/events{/privacy}","received_events_url":"https://api.github.com/users/dlubarov/received_events","type":"User","site_admin":false},"created_at":"2018-12-06T05:02:23Z","updated_at":"2018-12-06T05:02:23Z","author_association":"MEMBER","body":"> I think that this could get a bit messy, since records would need to inspect the contents of a predicate to ensure that it was a valid StandardToken predicate with plugins, rather than just comparing the hash of a predicate verification key as in Zexe.\r\n\r\nYeah I see what you mean. I think it should be possible to inspect subpredicates (and ideally our tooling should make it easy), but with the birth/death paradigm, it should rarely be necessary.\r\n\r\n> leaf nodes are hashed verification keys for each condition\r\n\r\nHm, would conditions correspond to predicates, or do you mean conditions in a different sense, like wire values? I don't quite understand. Taking your example of `p_1 AND (p_2 OR p_3)`, I was thinking the user would generate arguments for `p_1` and `p_2`, then an outer argument which recursively verifies all three (even though one will fail), then applies the two logic gates. Is your idea a way to improve upon that with an outer circuit which only verifies two arguments? That would be neat!\r\n\r\nAs an aside, I think the recursive approach could definitely speed up proof times in some cases. An extreme case would be a 1-of-100 multisig, where a merged circuit would be huge. With recursion we could generate just one signature verification argument, and then if we're clever, the outer argument could verify a single argument.\r\n\r\nHowever, using predicate boundaries as our recursion boundaries might be far from optimal in some cases. For instance if we wrote a time lock predicate, that just involves an integer comparison, so the circuit would probably be much smaller than a recursive verification circuit. Plus if the time lock is required (i.e. not part of an OR), then every valid transaction will need to show that it's satisfied, so we wouldn't gain anything from recursion.\r\n\r\nSo I think if we want to really optimize proving times, we should let predicate authors (or compilers) decide where to set the recursion boundaries. Or if we wanted to keep it simple, we could just merge all predicates into one circuit, and that might be good enough in practice."}}
{"actor":{"display_login":"dlubarov"}}