Tobias' comments/questions/remarks/...

docs/arch/system/state/resource_machine/data_structures/action.md

@@ -8,6 +8,9 @@ search:
 # Action
 
 An action is a composite structure of type `Action` that contains the following components:
+<!--ᚦ
+    «@"composite structure" can it be a juvix record?»
+-->
 
 |Component|Type|Description|
 |-|-|-|
@@ -17,46 +20,164 @@ An action is a composite structure of type `Action` that contains the following
 |`complianceUnits`|`Set ComplianceUnit`|The set of transaction's [compliance units](./compliance_unit.md)|
 |`applicationData`|`Map AppDataValueHash (BitString, DeletionCriterion)`|contains a map of hashes and [openings](./../primitive_interfaces/fixed_size_type/hash.md#hash) of various data needed to verify resource logic proofs. The deletion criterion field is described [here](./../notes/storage.md#data-blob-storage). The openings are expected to be ordered.|
 
+<!--ᚦ
+    «The lists should be repetition free, right?»
+--><!--ᚦ
+    «@resourceLogicProofs I think,
+    a description similar to the [forums](https://research.anoma.net/t/clarifying-proof-structures/856) could be preferable: ¶
+    1. `resourceLogicProofs: Map Tag (PS.VerifyingKey, PS.Proof)` as the type in the table
+    2. a (foot)note on `VerifyingKey=:LogicRefHash.T` for convenient implementation
+    »
+--><!--ᚦ
+    «more @resourceLogicProofs :
+        this deserves some more space, it is maximally compact,
+        but that makes it really hard to read
+    »
+--><!--ᚦ
+    «"|contains"
+    →"|consisting of"?»
+--><!--ᚦ
+    «can we have a description of an example for a resourceLogicProof ?»
+--><!--ᚦ
+    «What is the `self` resource? It seems only used here w/o definition.
+    This need to be fixed as sth.
+    along the lines of _the_ resource associated with the proof.
+»--><!--ᚦ
+    «We would like to have the type parameters of the Map in juvix, probably»
+--><!--ᚦ
+    «@"of transaction's [compliance units]..."
+    should it be "action's [compliance units]"?»
+--><!--ᚦ
+    «How are the openings expected to be ordered?
+    In what sense are they ordered?»
+-->
 
 !!! note
+
     `resourceLogicProofs` type: For function privacy, we assume that the produced logic proof is recursive, and the verifying key used to verify the proof is either universal and publicly known (in case we have a recursion) - then the verifying key for the inner proof is committed to in the `LogicRefHash` parameter - or it is contained directly in the `LogicRefHash` parameter. This part isn't properly generalised yet.
+    <!--ᚦ
+    «link to function privacy is desirable»
+    --><!--ᚦ
+    «@"recursive proofs": link(s) please, internal / external »
+    -->
 
 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.
 
+<!--ᚦ
+    «Can we move this paragraph to the top of the page?»
+--><!--ᚦ
+    «how is 'proof access' defined?»
+--><!--ᚦ
+    «"A resource is associated with exactly one action."
+    _at most_ one in general,
+    but exactly one for which resources ?
+    (probably the ones relevant to the enveloping transaction)»
+--><!--ᚦ
+    «the opposite of "consume" is "produce";
+    if we were to change this,
+    the term _resource creation_
+    would describe the action of addting to the commitment accumulator (merkle tree)»
+-->
+
 !!! note
+
     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.
+    <!--ᚦ
+        «in general, transactions may be unbalanced,
+        but then they are not executable, right?
+        [Btw, the definition of executable seems off.]»
+    -->
 
 ## Interface
 
-1. `create(Set (NullifierKey, Resource), Set Resource, ApplicationData) -> Action` - creates an action
-2. `delta(Action) -> DeltaHash`
+1. `create(Set (NullifierKey, Resource), Set Resource, ApplicationData) -> Action` - creates an action<!--ᚦ
+   «@'Set (NullifierKey, Resource)':
+   that's a set of elements in the Cartesian product NullifierKey×Resource,
+   right? »
+--><!--ᚦ
+    «The signature of `create` here seems to be inconsistent with
+    the description given below in `## create`»
+-->
+2. `delta(Action) -> DeltaHash`<!--ᚦ
+   «do we accidentally identify the type parameter T with the interface name here?
+   In transaction.md we have `DeltaHash.T`.
+   In other words "DeltaHash"→"DeltaHash.T".»
+-->
 3. `verify(Action) -> Bool`
 
 ## Proofs
-Each action refers to a set of resources to be consumed and a set of resources to be created. Creation and consumption of a resource requires a set of proofs that attest to the correctness of the proposed action. There are two proof types associated with each action:
 
-1. *Resource logic proofs* are created by `ResourceLogicProvingSystem`. 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 [here](./proof/logic.md).
+Each action refers to a set of resources to be consumed and a set of resources to be created. Creation and consumption of a resource requires a set of proofs that attest to the correctness of the proposed action. There are two proof types associated with each action:
+<!--ᚦ
+    «@"two proof types"→"two collections of proofs"
+    with an optional "(of two different kinds)"»
+--><!--ᚦ
+    «what is the referring mode—by which means do we refer—in
+    "Each action refers to"? via their tag, right?
+    »
+--><!--ᚦ
+    «what are the conditions for an action to be _correct_?»
+-->
+
+1. *Resource logic proofs* are created by `ResourceLogicProvingSystem`. 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 [here](./proof/logic.md).<!--ᚦ
+   «"the amount of resources"
+   →"the number/count of resources"
+   (because amount is synonym to quantity in other contexts)»
+--><!--ᚦ
+    «wikilinks preferred»
+-->
 2. *Resource machine [compliance proofs](./action.md#compliance-proofs-and-compliance-units)* are created by `ComplianceProvingSystem`. Compliance proofs ensure that the provided action complies with the resource machine definitions. Actions are partitioned into *compliance units*, and there is one compliance proof created for each compliance unit. Compliance proofs and compliance units are further described [here](./proof/compliance.md).
+<!--ᚦ
+    «wikilinks preferred»
+--><!--ᚦ
+    «@"resource machine definitions"
+    could we mention here the whole story in a (foot)note
+    about why we cannot (or do not want to) have arbitrary partitions?»
+-->
 
 ## `create`
 
 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:
-
-1. Partition action into compliance units and compute a compliance proof for each unit. Put the information about the units in `action.complianceUnits`
+<!--ᚦ
+    «step zero:
+    compute the corresponding lists of commitments and nullifiers
+    »
+-->
+
+1. Partition action into compliance units and compute a compliance proof for each unit. Put the information about the units in `action.complianceUnits`<!--ᚦ
+   «How do I (as a prover)
+   "[p]artition action into compliance units and compute a compliance proof for each unit."»
+--><!--ᚦ
+    «the concept of action seems only partially defined above;
+    are we rather looking into a partition of (relevant) resources / resource kinds
+    (as opposed to the action itself)?»
+-->
 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`
 3. `action.consumed = r.nullifier(nullifierKey) for r in consumedResources`
 4. `action.created = r.commitment() for r in createdResources`
 5. `action.applicationData = applicationData`
 
+<!--ᚦ
+    «How do I obtain the relevant applicationData?»
+-->
+
 ## `verify`
 
 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:
+<!--ᚦ
+    «@"Validity of an action can only be determined for actions that are associated with a transaction" why?»
+-->
 
 1. action input resources have valid resource logic proofs associated with them: `verify(RLVerifyingKey, RLInstance, RLproof) = True`
 2. action output resources have valid resource logic proofs associated with them: `verify(RLVerifyingKey, RLInstance, RLproof) = True`
 3. all compliance proofs are valid: `complianceUnit.verify() = True`
 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](./action.md#input-existence-check) in the compliance proofs.
+<!--ᚦ
+    «transaction are only defined further down in the TOC»
+-->
 
 ## `delta`
 
-`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)`.
+`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)`.
+
+<!--ᚦtags:annotated,non-trivial,improvable-->

docs/arch/system/state/resource_machine/data_structures/compliance_unit.md

@@ -1,28 +1,66 @@
 # Compliance proofs and compliance units
 
 `ComplianceUnit` is a data structure that partitions the [action](./action.md), meaning that there might be multiple compliance units for a single action, the sets of resources covered by any two compliance units cover don't intersect, and together the compliance proofs cover all of the resources in the action. This partition corresponds to the format expected by the compliance proving system used to produce compliance proofs. The table below describes the components of a compliance unit:
+<!--ᚦ
+    «I wonder: is it rather about tags than resources?»
+--><!--ᚦ
+    «"partitions the [action]"
+    →"partitions the _set of_ SOMETHING (??? resource tags ??? ???) of an [action]"
+    this is probably related to the union of created and consumend
+»--><!--ᚦ
+    «Can we repeat that
+        a consumed resource cannot be produced by an action in the same tx?»
+-->
 
 |Component|Type|Description|
 |-|-|-|
 |`proof`| `PS.Proof`||
 |`refInstance`|`ReferencedInstance`|The instance required to verify the compliance proof. Includes the references to the tags of the checked resources, compliance unit delta, `CMtree` roots references|
 |`vk`|`PS.VerifyingKey`|
+<!--ᚦ
+    «@"|The instance" where is this defined (internal/external link please)?»
+--><!--ᚦ
+    «@"|The instance" where can read up on this (external link please)?»
+--><!--ᚦ
+    «@"compliance unit delta" this should link
+    "compliance unit [[Compliance unit#Delta|delta]]"»
+-->
 
 !!! warning
+
     `ReferenceInstance` is a modified `PS.Instance` structure in which some elements are replaced by their references. To get `PS.Instance` from `ReferencedInstance` the referenced structures must be dereferenced. The structures we assume to be referenced here are:
-        - CMtree roots (stored in transaction)
-        - commitments and nullifiers (stored in action)
+
+    - CMtree roots (stored in transaction)
+    - commitments and nullifiers (stored in action)
+
     All other instance elements are assumed to be as the instance requires.
 
 !!! note
+
     Referencing Merkle tree roots: the Merkle tree roots required to verify the compliance proofs are stored in the transaction (not in action or a compliance unit), and are referenced by a short hash in `refInstance`. To find the right roots corresponding to the proof, the verifier has to compute the hashes of the roots in the transaction, match them with the short hashes in the `refInstance` structure, and use the ones that match for verification. A similar approach is used to reference the tags of the checked in the compliance unit resources.
 
 
 The size of a compliance unit - the number of created and consumed resources in each unit - is determined by the resource machine *instantiation*. The total number of compliance proofs required for an action is determined by the number of compliance units that comprise the action. For example, if the instantiation defines a single compliance proof to include 1 input and 1 output resource, and an action contains 3 input and 2 output resources, the total number of compliance units will be 3 (with a placeholder output resource in the third compliance unit).
 
+<!--ᚦ
+    «@"the number of created and consumed resources in each unit"
+    → "the number of resources in the unit, either created or consumed (never both)"
+    or similar.
+-->
+
 ## Delta
 
 Compliance unit delta is used to compute action and transaction deltas and is itself computed from resource deltas: `delta = sum(r.delta() for r in outputResources - sum(r.delta() for r in inputResources))`. Note that the delta is computed by the prover (who knows the resource objects of resources associated with the unit) and is a part of the instance. The compliance proof must ensure the correct computation of delta from the resource deltas available at the proving time.
+<!--ᚦ
+    «@outputResources
+    this is not defined;
+    it is probably `created(ComplianceUnit)`.
+    I actually would prefere "output" or "produced" over created.»
+--><!--ᚦ
+    «@inputResources
+    same issue, but with input for output»
+    [mutatis mutandis](https://en.wikipedia.org/wiki/Mutatis_mutandis)
+-->
 
 #### Delta for computing balance
 
@@ -32,10 +70,33 @@ The kind-distinctness property of $h_\Delta$ allows computing $\Delta = \sum_j{\
 
 As a result, the properties of `DeltaHash` allow computing the total balance for a compliance unit, action, or transaction, without having direct access to quantities and kinds of the resources that comprise the data structure.
 
+<!--ᚦ
+    «This is a good explanation, but in an unexpected place»
+-->
+
 ## Interface
 
-1. `delta(ComplianceUnit) -> DeltaHash` - returns the compliance unit delta, which is stored in `complianceData`: `unit.delta() = unit.complianceData.delta`
+<!--ᚦ
+    «This `## Interface` almost has to go higher up in the page
+    to improve readability.»
+-->
+
+1. `delta(ComplianceUnit) -> DeltaHash` - returns the compliance unit delta, which is stored in `complianceData`: `unit.delta() = unit.complianceData.delta`<!--ᚦ
+   « This is probably computed in the "obvious way", which needs spelling out though»
+--><!--ᚦ
+    «Where is `complianceData`»
+--><!--ᚦ
+    «"DeltaHash"
+    →"DeltaHash.T"
+--><!--ᚦ
+    «So, apparently, we are making reference to some (private and/or implicit???)
+    [[Compliance inputs]];
+    this file further down in the TOC, so I was not even aware of it.
+    »
+-->
 2. `created(ComplianceUnit) -> Set Commimtent` - returns the commitments of the created resources checked in the unit
 3. `consumed(ComplianceUnit) -> Set Nullifier` - returns the nullifiers of the consumed resources checked in the unit
 4. `create(PS.ProvingKey, PS.Instance, PS.Proof) -> ComplianceUnit` - computes the compliance proof and stores the data (or references to it, if stored elsewhere) required to verify it in the compliance unit
-4. `verify(ComplianceUnit) -> Bool` - returns `ComplianceProvingSystem.Verify(vk, instance, proof)`, where `instance` is computed from `refInstance` by dereferencing
+4. `verify(ComplianceUnit) -> Bool` - returns `ComplianceProvingSystem.Verify(vk, instance, proof)`, where `instance` is computed from `refInstance` by dereferencing
+
+<!--ᚦtags:nits,reviewed,improvable-->

docs/arch/system/state/resource_machine/data_structures/index.md

@@ -1,3 +1,5 @@
 # Data structures
 
-This section describes the resource machine data structures
+This section describes the resource machine data structures
+
+<!--ᚦ«should we include subsections here or put an itemized list with links?»-->