You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A protocol adapter provides [[Executor Engine|executor engine]] and [[Shard Engine|shard engine]] functionality on a foreign blockchain protocol (adaptee) being independent of the Anoma protocol (target). In other words, it processes [[Resource Machine|resource machine (RM)]] transactions and updates the RM state in correspondence with the adaptee's state changes.
15
+
16
+
In order to support a protocol adapter, the adaptee protocol has to be programmable (i.e., support smart contracts).
Copy file name to clipboardExpand all lines: docs/arch/system/state/resource_machine/data_structures/action/index.juvix.md
+28-23Lines changed: 28 additions & 23 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -16,49 +16,54 @@ An action is a composite structure of type `Action` that contains the following
16
16
17
17
|Component|Type|Description|
18
18
|-|-|-|
19
-
|`created`|`OrderedSet Commitment`|contains commitments of resources created in this action|
20
-
|`consumed`|`OrderedSet Nullifier`|contains nullifiers of resources consumed in this action|
21
-
|`resourceLogicProofs`|`Map Tag (LogicRef, PS.Proof)`|contains a map of resource logic proofs associated with this action. The key is the `self` resource for which the proof is computed, the first parameter of the value opens to the required verifying key, the second one is the corresponding proof|
22
-
|`complianceUnits`|`Set ComplianceUnit`|The set of transaction's [[Compliance unit | compliance units]]|
23
-
|`applicationData`|`Map Tag OrderedSet (BitString, DeletionCriterion)`|maps tags to relevant application data needed to verify resource logic proofs. The deletion criterion field is described [[Stored data format |here]]. The openings are expected to be ordered.|
24
-
19
+
|`resourceLogicProofs`|`Map Tag (isConsumed: Bool, logicVKOuter: LogicVKOuterHash, applicationData: List (BitString, DeletionCriterion), proof: ResourceLogicProvingSystem.Proof)`|Resource logic proofs for resources associated with the action. The key of each map entry is the tag of the resource for which a RL proof is provided. The deletion criterion field is described [[Stored data format |here]].|
20
+
|`complianceUnits`|`List ComplianceUnit`|The set of transaction's [[Compliance unit | compliance units]]|
25
21
26
22
!!! note
27
-
For function privacy in the shielded contenxt, instead of a logic proof we verify a proof of a logic proof validity - a recursive proof. `LogicRefHash` type corresponds to the RL VK commitment while verifying key in `resourceLogicProofs` refers to the key to be used for verification (i.e., verifier circuit verifying key as opposed to a resource logic verifying key). RL VK commitment should be included somewhere else, e.g., `applicationData[tag]`, and the compliance instance must reference it in `refInstance` as it is also a compliance proof instance.
23
+
For function privacy in the shielded context, instead of a logic proof we verify a proof of a logic proof validity - a recursive proof. `LogicVKOuterHash` type corresponds to the RL VK commitment while verifying key in `resourceLogicProofs` refers to the key to be used for verification (i.e., verifier circuit verifying key as opposed to a resource logic verifying key). RL VK commitment should be included somewhere else, e.g., `applicationData`.
28
24
29
-
Actions partition the state change induced by a transaction and limit the resource logics evaluation context: proofs created in the context of an action have access only to the resources associated with the action. A resource is said to be *associated with an action* if its commitment or nullifier is present in the action's `created` or `consumed` correspondingly. A resource is associated with exactly one action. A resource is said to be *consumed in the action* for a valid action if its nullifier is present in the action's `consumed` list. A resource is said to be *created in the action* for a valid action if its commitment is in the action's `created` list.
25
+
Actions partition the state change induced by a transaction and limit the resource logics evaluation context: proofs created in the context of an action have access only to the resources associated with the action. A resource is said to be *associated with an action* if its tag is present in the set of `resourceLogicProofs` keys . A resource is associated with at most two actions: resource creation is associated with exactly one action and resource consumption is associated with exactly one action. A resource is said to be *consumed in the action* for a valid action if its *nullifier* is present in the set of `resourceLogicProofs` keys. A resource is said to be *created in the action* for a valid action if its *commitment* is in the set of `resourceLogicProofs` keys.
30
26
31
27
!!! note
32
28
Unlike transactions, actions don't need to be balanced, but if an action is valid and balanced, it is sufficient to create a balanced transaction.
33
29
34
30
## Interface
35
31
36
-
1.`create(Set (NullifierKey, Resource), Set Resource, ApplicationData) -> Action` - creates an action
37
-
2.`delta(Action) -> DeltaHash`
38
-
3.`verify(Action) -> Bool`
32
+
1.`create(List (NullifierKey, Resource, deltaExtraInput, CMtreePath, CMTreeRoot, List (BitString, DeletionCriterion)), List (Resource, deltaExtraInput, List (BitString, DeletionCriterion)), appWitness: BitString) -> Action`
For each resource consumed or created in the action, it is required to provide a proof that the logic associated with that resource evaluates to `True` given the input parameters that describe the state transition induced by the action. The number of such proofs in an action equals to the amount of resources (both created and consumed) in that action, even if some resources have the same logics. Resource logic proofs are further described [[Resource logic proof | here]].
42
39
43
40
## `create`
44
41
45
-
Given a set of input resource objects `consumedResources: Set (NullifierKey, Resource, CMtreePath)`, a set of output resource plaintexts `createdResources: Set Resource`, and `applicationData`, including a set of application inputs required by resource logics, an action is computed the following way:
46
-
47
-
1. Partition action into compliance units and compute a compliance proof for each unit. Put the information about the units in `action.complianceUnits`
48
-
2. For each resource, compute a resource logic proof. Associate each proof with the tag of the resource and the logic hash reference. Put the resulting map in `action.resourceLogicProofs`
49
-
3.`action.consumed = r.nullifier(nullifierKey) for r in consumedResources`
50
-
4.`action.created = r.commitment() for r in createdResources`
51
-
5.`action.applicationData = applicationData`
42
+
1.`complianceUnits`: Partition the resources into compliance units and compute a compliance proof for each unit
43
+
2.`resourceLogicProofs`: For each resource, compute a resource logic proof. Associate each proof (and other components needed to verify it) with the tag of the resource
52
44
53
45
## `verify`
54
46
55
47
Validity of an action can only be determined for actions that are associated with a transaction. Assuming that an action is associated with a transaction, an action is considered valid if all of the following conditions hold:
56
48
57
-
1. action input resources have valid resource logic proofs associated with them: `verify(RLVerifyingKey, RLInstance, RLproof) = True`
58
-
2. action output resources have valid resource logic proofs associated with them: `verify(RLVerifyingKey, RLInstance, RLproof) = True`
59
-
3. all compliance proofs are valid: `complianceUnit.verify() = True`
60
-
4. transaction's $rts$ field contains correct `CMtree` roots (that were actual `CMtree` roots at some epochs) used to prove the existence of consumed resources in the compliance proofs.
49
+
1. All resource logic proofs associated with the action are valid
50
+
2. All compliance proofs associated with the action are valid: `cu.verify() = True for cu in complianceUnits`
51
+
3.`resourceLogicProofs` keys = the list of tags associated with `complianceUnits` (ignoring the order)
61
52
62
53
## `delta`
63
54
64
-
`action.delta() -> DeltaHash` is a computable component used to compute `transactionDelta`. It is computed from `r.delta()` of the resources that comprise the action and defined as `action.delta() = sum(cu.delta() for cu in action.complianceUnits)`.
55
+
`action.delta()` computes the action delta. Action delta is computed from `r.delta()` of the resources that comprise the action and defined as `action.delta() = sum(cu.delta() for cu in action.complianceUnits)`.
56
+
57
+
## `to_instance`
58
+
59
+
This function assembles the instance required to verify a resource logic proof from the data in the action.
60
+
61
+
The main task is to assemble the `consumed` and `created` lists of resources. The proposed mechanism works as follows:
62
+
1. Iterate over all compliance units and accumulate the lists of created and consumed resources. The resulting list of consumed resources contains all consumed resources in the action. The resulting list of created resources contains all created resources in the action.
63
+
2. Erase the `self` resource from the relevant list. If the resource is consumed and its nullifier is stored under index `n` in the list of consumed resources, the resulting list is `l[0], l[1], ..., l[n - 1], l[n + 1], ...`. Keep the list of created resources the same.
64
+
3. If `self` is created, erase the resource from the list of created resources as in step 2. Keep the list of consumed resources the same. For each resource we assemble an instance for, we erase only one resource - itself - from one list.
65
+
66
+
!!! note
67
+
When verifying multiple logic proofs from the same action, it might make sense to create the 'full' lists once and erase resources one at a time to create a particular instance. Note that the next instance must be created from the original `full` list, not the list with previously erased resources.
68
+
69
+
All other fields of the instance (resource tag, `isConsumed`, `applicationData`) are taken from the relevant entry of `resourceLogicProofs`.
Resource logic proofs attest to validity of resource logics. A resource logic is a computable predicate associated with a resource that constrains the creation and consumption of a resource. Each time a resource is created or consumed, the corresponding resource logic proof is required in order for the action (and thus the transaction) to be valid.
15
+
Resource logic proofs attest to validity of resource logics. A resource logic is a computable predicate associated with a resource (this resource is referred to as `self` in this context) that constrains the creation and consumption of a resource. Each time a resource is created or consumed, the corresponding resource logic proof is required in order for the action (and thus the transaction) to be valid.
16
16
17
17
## Proving
18
18
19
-
When proving, resource logics take as input resources created and consumed in the action:
19
+
When proving, resource logics take as input resources created and consumed in that action.
20
20
21
21
#### Instance
22
22
23
-
1.[[Computable components#Tag | Resource tag]] — identifies the current resource being checked
23
+
1. Resource's commitment/nullifier
24
24
2.`isConsumed` - a flag that tells the logic if the resource is consumed or created
25
-
3.`action.consumed` (possibly excluding the tagged resource, if it is consumed)
26
-
4.`action.created` (possibly excluding the tagged resource, if it is created)
27
-
5.`action.applicationData[tag]`
25
+
3.`consumed` (excluding the tagged resource, if it is consumed)
26
+
4.`created` (excluding the tagged resource, if it is created)
27
+
5.`applicationData`
28
28
29
-
#### Witness
30
-
31
-
1. for consumed resources: `OrderedSet (Resource, NullifierKey)`
32
29
33
-
2. for created resources: `OrderedSet Resource`
30
+
#### Witness
34
31
35
-
3. Application inputs
32
+
1.`self` resource object
33
+
2. If `isConsumed = True`: nullifier key of `self`
34
+
3. Resource objects of consumed resources: `List (Resource, NullifierKey)`
35
+
4. Resource objects of created resources: `List Resource`
36
+
5. Application-specific inputs
36
37
37
38
!!! note
38
-
The instance and witness values are expected to correspond to each other: the first tag in the instance corresponds to the first resource object in the witness (and corresponds to the resource being checked), and so on. Note that the tag has to be recomputed from the object to verify that it indeed corresponds to the tag (this condition is included in the constraints)
39
+
Instance and witness elements are expected to go in the same order: the first element of the instance corresponds to the first elements of the witness and so on.
39
40
40
41
#### Constraints
41
42
42
-
1. Created commitment integrity: `r.commitment() = cm`
1. For created resources: created commitment integrity: `r.commitment() = cm`
44
+
2. For consumed resources: `r.nullifier(nullifierKey) = nf`
45
+
3. Application-specific constraints
46
+
47
+
Checks that require access to global `CMTree` and `NullifierSet`:
48
+
49
+
1. each created resource wasn't created in prior transactions
50
+
2. each consumed resource wasn't consumed in prior transactions
51
+
52
+
!!! note
53
+
Actions can be verified as parts of supposedly valid transactions and individually, when building a valid transaction (e.g., in the partial solving case). In case the actions are verified _not_ individually, all global checks can be aggregated and verified at once to reduce the amount of global communication.
Copy file name to clipboardExpand all lines: docs/arch/system/state/resource_machine/data_structures/compliance_unit/compliance_proof.juvix.md
+22-24Lines changed: 22 additions & 24 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -19,9 +19,9 @@ Compliance proofs are created by `ComplianceProvingSystem` and computed over com
19
19
20
20
|Name|Type|Description|
21
21
|-|-|-|
22
-
|`consumed`|`OrderedSet (NullifierRef, RootRef, LogicRef)`|Includes nullifiers' references of all consumed resources in the compliance unit, root references, and commitments to [[Resource |`logicRef`resource components]] (used for referencing the `logicRef` without explicitly using the component value) for consumed resources|
23
-
|`created`|`OrderedSet (CommitmentRef, LogicRef)`|Commitments' references of all created resources in the compliance unit|
24
-
|`unitDelta`|`DeltaHash`|Unit delta|
22
+
|`consumed`|`List (nf: Nullifier, root: CMTree.Value, logicVKOuter: LogicVKOuterHash)`|Each entry corresponds to a consumed resource and includes a hash of the resource's [[Resource |`logicRef`component]]|
23
+
|`created`|`List (cm: Commitment, logicVKOuter: LogicVKOuterHash)`|Each entry corresponds to a created resource|
24
+
|`unitDelta`|`DeltaHash`||
25
25
26
26
#### Witness
27
27
@@ -31,48 +31,46 @@ Compliance proofs are created by `ComplianceProvingSystem` and computed over com
31
31
32
32
2.`nullifierKey`
33
33
34
-
3.`CMtree` path
34
+
3.`CMtree` path to the consumed resource commitment
35
35
36
-
4.resource commitment `cm`
36
+
4.pre-image of `logicVKOuter`
37
37
38
-
5.opening of `logicRefHash` (implicitly includes `logicRef`, which is already part of the resource object, and other data used to derive `logicRefHash`, such as randomness)
38
+
5.`deltaExtraInput`used to compute resource delta
39
39
40
40
2. for created resources:
41
41
42
42
1. resource object `r`
43
43
44
-
2. opening of `logicRefHash`
44
+
2. pre-image of `logicVKOuter`
45
+
46
+
3.`deltaExtraInput` used to compute resource delta
45
47
46
48
!!! note
47
49
48
-
The instance and witness values are expected to correspond to each other: the first tag in the instance corresponds to the first resource object in the witness, and so on. Note that in the compliance proof, the tag is recomputed from the object to verify that the tag is correct
50
+
Instance and witness elements are expected to go in the same order: the first element of the instance corresponds to the first (4 for consumed and 2 for created) elements of the witness and so on.
49
51
50
52
## Compliance constraints
51
53
Each resource machine compliance proof must check the following:
52
54
53
-
1. Merkle path validity (for *non-ephemeral* resources only): `CMTree::Verify(cm, path, root) = True` for each resource associated with a nullifier from the `consumedResourceTagSet`
54
-
2. for each consumed resource `r`:
55
+
1. Merkle path validity: `CMTree::Verify(r.commitment(), path, root) = True` for each resource associated with a nullifier from the `consumed`. For ephemeral resources a "fake" relation is checked.
55
56
56
-
1. Nullifier integrity: `r.nullifier(nullifierKey) is in consumedResourceTagSet`
[2.3, 3.2]: Combined with checking the logic proofs, logic integrity checks allow to ensure that the logics associated with the resources are satisfied
67
+
4. Delta integrity: `unitDelta = sum(r.delta(deltaExtraInput(r)) for r in consumed) - sum(r.delta(deltaExtraInput(r)) for r in created)` where `deltaExtraInput(r)` returns `deltaExtraInput` associated with resource `r`
71
68
72
69
!!! note
73
-
[2.1, 3.1]: To ensure correct computation of a commitment/nullifier, they have to be recomputed from the raw parameters (resource object and possibly `nullifierKey`) and compared to what is provided in the public tag set.
70
+
Kind integrity is checked implicitly in delta integrity
74
71
75
72
!!! note
76
-
To support function privacy, the compliance proof must also verify the logic verifying key integrity: given `logicRefHash` as public input and `logicRef` as private input, verify that `logicRefHash = hash(logicRef)`
73
+
[2.3, 3.2]: Combined with checking the logic proofs, logic integrity checks allow to ensure that the logics associated with the resources are satisfied
77
74
78
-
Compliance proofs must be composition-independent: composing two actions, the compliance proof sets can be simply united to provide a valid composed action compliance proof set.
75
+
!!! note
76
+
[2.1, 3.1]: To ensure correct binding between the instance and the witness, resource tags have to be recomputed from the witness and compared to what is provided in the instance.
0 commit comments