From cc2f215830b36568168b32466622143a6cfa39f8 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:02:53 -0500 Subject: [PATCH 01/39] Add state type documentation in Juvix Markdown format This commit introduces a new documentation file for the `State` type in the Juvix programming language. The file includes detailed descriptions of the type's structure, its components, and their respective arguments. Additionally, it provides auxiliary Juvix code for deriving equality and order instances for the `State` type. This enhancement improves the clarity and accessibility of the documentation for developers working with state management in Juvix. --- docs/arch/system/types/state.juvix.md | 67 +++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 docs/arch/system/types/state.juvix.md diff --git a/docs/arch/system/types/state.juvix.md b/docs/arch/system/types/state.juvix.md new file mode 100644 index 00000000000..4ae30674cd6 --- /dev/null +++ b/docs/arch/system/types/state.juvix.md @@ -0,0 +1,67 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.state; + import prelude open; + import arch.system.types.nullifier open; + ``` + +# State + +```juvix +type State := mkState { + -- commitmentAccumulator : CommitmentAccumulator; + -- secondCommitmentAccumulator : CommitmentAccumulator; + nullifierSet : Set Nullifier; + -- hierarchicalIndex : HierarchicalIndex; + -- dataBlobStorage : DataBlobStorage; +}; +``` + +??? quote "Arguments" + + `commitmentAccumulator` + : a commitment accumulator that maps timestamps (part of CMtree) onto finite + field elements + + `secondCommitmentAccumulator` + : a second commitment accumulator that maps finite field x timestamp pairs + onto finite field elements + + `nullifierSet` + : a nullifier set that is a map from a finite field element to a finite + field element + + `hierarchicalIndex` + : a hierarchical index that is a chained hash set that maps tree paths to + finite field elements + + `dataBlobStorage` + : a data blob storage that is a key-value store mapping finite field + elements to (variable length byte array, deletion criterion) pairs + + `deletionCriteria` + : a deletion criterion. + +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + stateEq : Eq State; + ``` + + ```juvix + deriving + instance + stateOrd : Ord State; + ``` + From 7e292c537424474d2b98c9a5a029e00ccc3664a6 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:03:11 -0500 Subject: [PATCH 02/39] Add documentation for Resource type in Juvix Markdown format --- docs/arch/system/types/resource.juvix.md | 86 ++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 docs/arch/system/types/resource.juvix.md diff --git a/docs/arch/system/types/resource.juvix.md b/docs/arch/system/types/resource.juvix.md new file mode 100644 index 00000000000..526c2a7b39b --- /dev/null +++ b/docs/arch/system/types/resource.juvix.md @@ -0,0 +1,86 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.resource; + import prelude open; + import arch.node.types.crypto open; + ``` + +# Resource + +A **resource** is a composite structure `Resource` that contains the following components: + +## `Resource` + +```juvix +type Resource := mkResource { + -- logicRef : LogicHash; + -- labelRef : LabelHash; + valueRef : Digest; + -- quantity : Quantity; + isEphemeral : Bool; + -- nonce : Nonce; +}; +``` + +??? quote "Arguments" + + `logicRef` + : [[Hash]] of the predicate associated with the resource (resource logic). + + `labelRef` + : [[Hash]] of the resource label. Resource label specifies the fungibility + domain for the resource. Resources within the same fungibility domain are + seen as equivalent kinds of different quantities. Resources from different + fungibility domains are seen and treated as non-equivalent kinds. This + distinction comes into play in the balance check described later + + `valueRef` + : [[Hash]] of the resource value. Resource value is the fungible data + associated with the resource. It contains extra information but does not + affect the resource's fungibility + + `quantity` + : is a number representing the quantity of the resource + + `isEphemeral` + : is a flag that reflects the resource's ephemerality. Ephemeral resources + do not get checked for existence when being consumed + + `nonce` + : guarantees the uniqueness of the resource computable components + + `nullifierKeyCommitment` + : is a nullifier key commitment. Corresponds to the nullifier key $nk$ used to + the resource nullifier (nullifiers are further described [[Nullifier|here]]) + + `randSeed` + : randomness seed used to derive whatever randomness needed + +To distinguish between the resource data structure consisting of the resource +components and a resource as a unit of state identified by just one (or some) of +the resource computed fields, we sometimes refer to the former as a *resource +object*. Data which is referenced by the resource object - such as the preimage +of `valueRef` - we refer to as *resource-linked data*. + + +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + ResourceEq : Eq Resource; + ``` + + ```juvix + deriving + instance + ResourceOrd : Ord Resource; + ``` From 5577216a98bf42c55c162f8eb903d6fc47c6c151 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:08:31 -0500 Subject: [PATCH 03/39] Add documentation for Resource Machine type in Juvix Markdown format --- .../system/types/resource_machine.juvix.md | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 docs/arch/system/types/resource_machine.juvix.md diff --git a/docs/arch/system/types/resource_machine.juvix.md b/docs/arch/system/types/resource_machine.juvix.md new file mode 100644 index 00000000000..d62d423e290 --- /dev/null +++ b/docs/arch/system/types/resource_machine.juvix.md @@ -0,0 +1,52 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - resource-machine + - protocol + - commitment + - nullifier + - accumulator + - resource logic +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.resource_machine; + import prelude open; + import + arch.system.state.resource_machine.data_structures.transaction.transaction open; + ``` + +# Resource Machines + +A **resource machine** is a term of type `ResourceMachine`. + +## `ResourceMachine` + +```juvix +type ResourceMachine := mkResourceMachine { + createTransaction : + -- CMTreeRoots : Set CMtree.Value; + -- actions : Set Action; + -- deltaProof : DeltaProvingSystem.Proof; + Unit -> Transaction; -- which is the mkTransaction function + composeTransactions : Transaction -> Transaction -> Transaction; + verifyTransaction : Transaction -> Bool; + -- read nullifier set? + -- append to nullifier set? + -- read commitment tree? + -- add data to commitment tree? +}; +``` + +## Purpose + +The purpose of the `ResourceMachine` is to allow us to: + +- create a transaction, +- compose transactions, and +- verify transactions according to the rules of the protocol. From 8a117b8624eed787fbd146f53881fc8d9fd7d5d6 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:11:48 -0500 Subject: [PATCH 04/39] Add documentation for Resource Logic Proof in Juvix Markdown format --- .../types/resource_logic_proof.juvix.md | 91 +++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 docs/arch/system/types/resource_logic_proof.juvix.md diff --git a/docs/arch/system/types/resource_logic_proof.juvix.md b/docs/arch/system/types/resource_logic_proof.juvix.md new file mode 100644 index 00000000000..61baef941b5 --- /dev/null +++ b/docs/arch/system/types/resource_logic_proof.juvix.md @@ -0,0 +1,91 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.resource_logic_proof; + import prelude open; + ``` + +# Resource logic proofs + +A **resource logic proof** is a term of type `ResourceLogicProof`. Resource +logic proofs attest to validity of [[Resource logic|resource_logics]]. + +## `ResourceLogicProof` + +```juvix +type ResourceLogicProof := mkResourceLogicProof { + -- instance : ResourceLogicProofInstance; + -- witness : ResourceLogicProofWitness; + -- constraints : ResourceLogicProofConstraints; +}; +``` + +??? quote "Arguments" + + `instance` + : the instance of the resource logic proof + + `witness` + : the witness of the resource logic proof + + `constraints` + : the constraints of the resource logic proof + +## Purpose + +!!! todo + + Explain the purpose of resource logic proofs. + +## Properties + +!!! todo + + Explain the properties of resource logic proofs. + + From 9974c4c206d8c3e17b4fba7673c9717c3d3856a1 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:15:43 -0500 Subject: [PATCH 05/39] Add documentation for Action type in Juvix Markdown format. --- docs/arch/system/types/action.juvix.md | 139 +++++++++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 docs/arch/system/types/action.juvix.md diff --git a/docs/arch/system/types/action.juvix.md b/docs/arch/system/types/action.juvix.md new file mode 100644 index 00000000000..4089065e267 --- /dev/null +++ b/docs/arch/system/types/action.juvix.md @@ -0,0 +1,139 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.action; + import prelude open; + import arch.system.types.nullifier open; + ``` + +# Actions + +An **action** is a term of type `Action`. + +## `Action` + +```juvix +type Action := mkAction { + -- created : List Commitment; + consumed : List Nullifier; + -- resourceLogicProofs : Map Tag (LogicRefHash, PS.Proof); + -- complianceUnits : Set ComplianceUnit; + -- applicationData : Map Tag (BitString, DeletionCriterion); +}; +``` + +??? quaote "Arguments" + + `created` + : contains commitments of resources created in this action + + `consumed` + : contains nullifiers of resources consumed in this action + + `resourceLogicProofs` + : 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 + + `complianceUnits` + : The set of transaction's [[Compliance unit | compliance units]] + + `applicationData` + : 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. + +## Purpose + +!!! todo + + Explain the purpose of actions. + +## Properties + +!!! todo + + Explain the properties of actions. + + \ No newline at end of file From 213308b0bae8fbd3136662932579ffee2ea189ea Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:16:30 -0500 Subject: [PATCH 06/39] Refactor Juvix documentation for cryptographic types This commit updates the documentation for the `PublicKey`, `PrivateKey`, `SecretKey`, and `Digest` types in Juvix. It introduces auxiliary code snippets for deriving equality and order instances for each type. --- docs/arch/node/types/crypto.juvix.md | 68 +++++++++++++++++++++++----- 1 file changed, 56 insertions(+), 12 deletions(-) diff --git a/docs/arch/node/types/crypto.juvix.md b/docs/arch/node/types/crypto.juvix.md index 4139a997fbd..7532f1680ab 100644 --- a/docs/arch/node/types/crypto.juvix.md +++ b/docs/arch/node/types/crypto.juvix.md @@ -27,14 +27,24 @@ Public key for public-key cryptography. type PublicKey := | Curve25519PubKey ByteString ; - -instance -PublicKeyOrd : Ord PublicKey := - mkOrd@{ - cmp := \{_ _ := Equal}; - }; ``` +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + PublicKeyEq : Eq PublicKey; + ``` + + ```juvix + instance + PublicKeyOrd : Ord PublicKey := + mkOrd@{ + cmp := \{_ _ := Equal}; + }; + ``` + ### Private key Private key for public-key cryptography. @@ -43,14 +53,22 @@ Private key for public-key cryptography. type PrivateKey := | Curve25519PrivKey ByteString ; - -instance -PrivateKeyOrd : Ord PrivateKey := - mkOrd@{ - cmp := \{_ _ := Equal}; - }; ``` +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + PrivateKeyEq : Eq PrivateKey; + + instance + PrivateKeyOrd : Ord PrivateKey := + mkOrd@{ + cmp := \{_ _ := Equal}; + }; + ``` + ### Secret key Secret key for secret-key cryptography. @@ -61,6 +79,18 @@ type SecretKey := ; ``` +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + SecretKeyEq : Eq SecretKey; + + deriving + instance + SecretKeyOrd : Ord SecretKey; + ``` + ### Signature Cryptographic signature. @@ -80,3 +110,17 @@ type Digest := | Blake3Digest ByteString ; ``` + +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + DigestEq : Eq Digest; + + instance + DigestOrd : Ord Digest := + mkOrd@{ + cmp := \{(Blake3Digest a) (Blake3Digest b) := Equal}; + }; + ``` From dbdee2fb9c9757ab928b06074baeb6ea6acdcf70 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:16:51 -0500 Subject: [PATCH 07/39] Update Juvix documentation: refine equality import in prelude.juvix.md This commit modifies the import statement for the equality trait in the `prelude.juvix.md` file, changing it to include both `Eq` and `mkEq`. --- docs/prelude.juvix.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prelude.juvix.md b/docs/prelude.juvix.md index f9024bf4f75..8c78a0372fd 100644 --- a/docs/prelude.juvix.md +++ b/docs/prelude.juvix.md @@ -13,7 +13,7 @@ tags: module prelude; import Stdlib.Trait open public; import Stdlib.Trait.Ord open using {Ordering; mkOrd; Equal; isEqual} public; - import Stdlib.Trait.Eq open using {==} public; + import Stdlib.Trait.Eq open using {Eq; mkEq; ==} public; import Stdlib.Debug.Fail open using {failwith}; ``` From 2164c13885d7705bb1fc1b3bcb713deef77e19d5 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:18:34 -0500 Subject: [PATCH 08/39] Remove nullifier documentation and add new nullifier and nullifier key documentation This commit introduces new documentation for nullifiers and nullifier keys in Juvix. The new files provide detailed descriptions of nullifier properties, their purpose in preventing double-spending, and the structure of nullifier keys. --- .../computable_components/nullifier.juvix.md | 23 ------ docs/arch/system/types/nullifier.juvix.md | 75 +++++++++++++++++++ .../types/nullifier_properties.juvix.md | 63 ++++++++++++++++ docs/arch/system/types/nullifierkey.juvix.md | 53 +++++++++++++ 4 files changed, 191 insertions(+), 23 deletions(-) delete mode 100644 docs/arch/system/state/resource_machine/data_structures/resource/computable_components/nullifier.juvix.md create mode 100644 docs/arch/system/types/nullifier.juvix.md create mode 100644 docs/arch/system/types/nullifier_properties.juvix.md create mode 100644 docs/arch/system/types/nullifierkey.juvix.md diff --git a/docs/arch/system/state/resource_machine/data_structures/resource/computable_components/nullifier.juvix.md b/docs/arch/system/state/resource_machine/data_structures/resource/computable_components/nullifier.juvix.md deleted file mode 100644 index b1c0b183aac..00000000000 --- a/docs/arch/system/state/resource_machine/data_structures/resource/computable_components/nullifier.juvix.md +++ /dev/null @@ -1,23 +0,0 @@ ---- -icon: material/file-document-outline -search: - exclude: false - boost: 2 ---- - -```juvix -module arch.system.state.resource_machine.data_structures.resource.computable_components.nullifier; -``` - -# Nullifier - -A resource nullifier is a computed field, the publishing of which marks the resource associated with the nullifier as consumed. - -For a resource `r`, `r.nullifier(nullifierKey) = nullifierHash(nullifierKey, r)`, where `nullifierKey` is a key provided externally. - -A resource can be consumed only once. Nullifiers of consumed resources are stored in a public append-only structure called the resource *nullifier set*. This structure is external to the resource machine, but the resource machine can read from it and append to it. - -!!! note - Every time a resource is consumed, it has to be checked that the resource existed before (the resource's commitment is in the commitment tree) and has not been consumed yet (the resource's nullifier is not in the nullifier set). - - diff --git a/docs/arch/system/types/nullifier.juvix.md b/docs/arch/system/types/nullifier.juvix.md new file mode 100644 index 00000000000..ee61bd644ca --- /dev/null +++ b/docs/arch/system/types/nullifier.juvix.md @@ -0,0 +1,75 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - nullifier + - resource-machine + - state +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.nullifier; + import prelude open; + import arch.system.types.resource open; + import arch.system.types.nullifierkey open; + import arch.node.types.crypto open; + ``` + +# Nullifiers + +A *resource nullifier* or *nullifier* for short is a term of type `Nullifier`. +Each nullifier is data consisting of a `key` and the `resource` it is +associated with. + +## `Nullifier` + +```juvix +type Nullifier := mkNullifier { + key : NullifierKey; + resource : Resource; +}; +``` + +???+ quote "Arguments" + + `key` + : identifier of the nullifier + + `resource` + : the resource that is presumed to be consumed + +??? quote "Auxiliary Juvix code: Instances" + + ```juvix + deriving + instance + nullifierEq : Eq Nullifier; + ``` + + ```juvix + deriving + instance + nullifierOrd : Ord Nullifier; + ``` + +## Purpose + +Nullifiers prevent double-spending by: + +1. Uniquely identifying *consumed resources* when stored in **the** nullifier +set part of the [[State|state]]. + +2. Requiring two factors to consume a resource, that is: + + - A nullifier key matching the resource's nullifier key commitment. + + - The resource nullifier must not exist in the [[Nullifier Set|nullifier set]]. + + +## Properties + +--8<-- "./nullifier_properties.juvix.md:properties" diff --git a/docs/arch/system/types/nullifier_properties.juvix.md b/docs/arch/system/types/nullifier_properties.juvix.md new file mode 100644 index 00000000000..5785b463d5d --- /dev/null +++ b/docs/arch/system/types/nullifier_properties.juvix.md @@ -0,0 +1,63 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - nullifier + - resource-machine + - state +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.nullifier_properties; + import prelude open; + import arch.system.types.resource open; + import arch.system.types.nullifierkey open; + import arch.system.types.state open; + import arch.system.types.nullifier open; + import arch.node.types.crypto open; + ``` + +# Nullifier Properties + + + +??? quote "Auxiliary Juvix code: Axioms" + + ```juvix + axiom computeNullifier : Resource -> NullifierKey -> Digest; + axiom nullifierHash : Nullifier -> Digest; + ``` + +The following properties must hold true to consider a nullifier valid: + +### Nullifier key must match the resource's nullifier key commitment + +```juvix +match-nullifier-key + (r : Resource) (nk : NullifierKey) : Bool := + let n := mkNullifier@{key := nk; resource := r} in + (computeNullifier r nk) == (nullifierHash n) +``` + +### Nullifier must not exist in the [[Nullifier Set|nullifier set]] + +``` +unique-nullifier-property + (s : State) (r : Resource) (nk : NullifierKey) : Bool := + let nullifier := mkNullifier@{key := nk; resource := r}; + nullifierSet : Set Nullifier := State.nullifierSet s; + cond (other : Nullifier) : Bool := (Set.isMember other nullifierSet) && (other == nullifier) + in not (all cond (n in nullifierSet)); +``` + +!!! todo + + Typecheck the `unique-nullifier-property` produces an error message stating that + `nullifierSet` is of type `Set Nullifier` and not `Set NullifierKey`. + Apparently, it is an alias issue. + + diff --git a/docs/arch/system/types/nullifierkey.juvix.md b/docs/arch/system/types/nullifierkey.juvix.md new file mode 100644 index 00000000000..766e74ffa8d --- /dev/null +++ b/docs/arch/system/types/nullifierkey.juvix.md @@ -0,0 +1,53 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.nullifierkey; + import prelude open; + import arch.node.types.crypto open; + ``` + +# Nullifier Key + +A *resource nullifier key* is of type `NullifierKey`. A nullifier key is data +used to compute the nullifier of a resource and expected to be unique for each +resource. + +## `NullifierKey` + +```juvix +type NullifierKey := mkNullifierKey { + key : SecretKey; +}; +``` + +???+ quote "Arguments" + + `key` + : an external secret key. + + +??? quote "Auxiliary Juvix code: Instances" + + ```juvix + deriving + instance + nullifierKeyEq : Eq NullifierKey; + ``` + + ```juvix + deriving + instance + nullifierKeyOrd : Ord NullifierKey; + ``` + +## Purpose + +The publishing of a resource nullifier key marks the resource associated with +the nullifier as consumed. From fd7d8d9ff464ae27d7b0d9a11627cf3364caa15d Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:23:24 -0500 Subject: [PATCH 09/39] Add documentation for Transaction type and update Action type in Juvix Markdown format This commit introduces a new documentation file for the `Transaction` type in Juvix, detailing its structure, arguments, and auxiliary code for deriving equality and order instances. Additionally, it updates the existing documentation for the `Action` type by correcting a typo and enhancing the auxiliary code section. --- docs/arch/system/types/action.juvix.md | 16 ++- .../system/types/resource_machine.juvix.md | 3 +- docs/arch/system/types/transaction.juvix.md | 128 ++++++++++++++++++ 3 files changed, 144 insertions(+), 3 deletions(-) create mode 100644 docs/arch/system/types/transaction.juvix.md diff --git a/docs/arch/system/types/action.juvix.md b/docs/arch/system/types/action.juvix.md index 4089065e267..8aa25a0cf0c 100644 --- a/docs/arch/system/types/action.juvix.md +++ b/docs/arch/system/types/action.juvix.md @@ -30,7 +30,7 @@ type Action := mkAction { }; ``` -??? quaote "Arguments" +???+ quote "Arguments" `created` : contains commitments of resources created in this action @@ -52,6 +52,20 @@ type Action := mkAction { proofs. The deletion criterion field is described [[Stored data format |here]]. The openings are expected to be ordered. +??? quote "Auxiliary Juvix code: Instances" + + ```juvix + deriving + instance + eqAction : Eq Action; + ``` + + ```juvix + deriving + instance + ordAction : Ord Action; + ``` + ## Purpose !!! todo diff --git a/docs/arch/system/types/resource_machine.juvix.md b/docs/arch/system/types/resource_machine.juvix.md index d62d423e290..dc471fdde33 100644 --- a/docs/arch/system/types/resource_machine.juvix.md +++ b/docs/arch/system/types/resource_machine.juvix.md @@ -17,8 +17,7 @@ tags: ```juvix module arch.system.types.resource_machine; import prelude open; - import - arch.system.state.resource_machine.data_structures.transaction.transaction open; + import arch.system.types.transaction open; ``` # Resource Machines diff --git a/docs/arch/system/types/transaction.juvix.md b/docs/arch/system/types/transaction.juvix.md new file mode 100644 index 00000000000..02f8b0c8c2c --- /dev/null +++ b/docs/arch/system/types/transaction.juvix.md @@ -0,0 +1,128 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.transaction; + import prelude open; + import arch.system.types.action open; + ``` + +# Transactions + +A **transaction** is a term of type `Transaction`. + +## `Transaction` + +```juvix +type Transaction := mkTransaction { + actions : Set Action; + -- CMTreeRoots : Set CMtree.Value; + -- deltaProof : DeltaProvingSystem.Proof; +}; +``` + +???+ quote "Arguments" + + `CMTreeRoots` + : a set of valid commitment tree roots used to prove the existence of the + resources being consumed in the transaction. This set is not a part of + actions to avoid duplication of data + + `actions` + : a set of actions that comprise the transaction + + `deltaProof` + : balance proof. It makes sure that `transactionDelta` is correctly derived + from the actions' deltas and commits to the expected publicly known value, + called a _balancing value_. There is just one delta proof per transaction + +???+ quote "Auxiliary Juvix code: Instances" + + ```juvix + deriving + instance + eqTrans : Eq Transaction; + ``` + + ```juvix + deriving + instance + ordTrans : Ord Transaction; + ``` + +## Purpose + +!!! todo + + Explain the purpose of transactions. + +## Properties + +!!! todo + + Explain the properties of transactions. + + \ No newline at end of file From 5b5665d71a65aaad5e5db5c435b334d36754d811 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:26:10 -0500 Subject: [PATCH 10/39] Remove obsolete documentation for Action, Resource Logic Proof, Resource, and Transaction types in Juvix Markdown format. --- .../data_structures/action/index.juvix.md | 64 ----------------- .../action/resource_logic_proof.juvix.md | 44 ------------ .../data_structures/resource/index.juvix.md | 27 ------- .../transaction/transaction.juvix.md | 72 ------------------- 4 files changed, 207 deletions(-) delete mode 100644 docs/arch/system/state/resource_machine/data_structures/action/index.juvix.md delete mode 100644 docs/arch/system/state/resource_machine/data_structures/action/resource_logic_proof.juvix.md delete mode 100644 docs/arch/system/state/resource_machine/data_structures/resource/index.juvix.md delete mode 100644 docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md diff --git a/docs/arch/system/state/resource_machine/data_structures/action/index.juvix.md b/docs/arch/system/state/resource_machine/data_structures/action/index.juvix.md deleted file mode 100644 index 9ef27ac72d5..00000000000 --- a/docs/arch/system/state/resource_machine/data_structures/action/index.juvix.md +++ /dev/null @@ -1,64 +0,0 @@ - ---- -icon: material/file-document-outline -search: - exclude: false - boost: 2 ---- - -```juvix -module arch.system.state.resource_machine.data_structures.action.index; -``` - -# Action - -An action is a composite structure of type `Action` that contains the following components: - -|Component|Type|Description| -|-|-|-| -|`created`|`List Commitment`|contains commitments of resources created in this action| -|`consumed`|`List Nullifier`|contains nullifiers of resources consumed in this action| -|`resourceLogicProofs`|`Map Tag (LogicRefHash, 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| -|`complianceUnits`|`Set ComplianceUnit`|The set of transaction's [[Compliance unit | compliance units]]| -|`applicationData`|`Map Tag (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.| - - -!!! 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. - -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. - -!!! 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. - -## Interface - -1. `create(Set (NullifierKey, Resource), Set Resource, ApplicationData) -> Action` - creates an action -2. `delta(Action) -> DeltaHash` -3. `verify(Action) -> Bool` - -## Proofs -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]]. - -## `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` -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` - -## `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: - -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 in the compliance proofs. - -## `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)`. \ No newline at end of file diff --git a/docs/arch/system/state/resource_machine/data_structures/action/resource_logic_proof.juvix.md b/docs/arch/system/state/resource_machine/data_structures/action/resource_logic_proof.juvix.md deleted file mode 100644 index 77068455eb8..00000000000 --- a/docs/arch/system/state/resource_machine/data_structures/action/resource_logic_proof.juvix.md +++ /dev/null @@ -1,44 +0,0 @@ - ---- -icon: material/file-document-outline -search: - exclude: false - boost: 2 ---- - -```juvix -module arch.system.state.resource_machine.data_structures.action.resource_logic_proof; -``` - -# Resource logic proof - -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. - -## Proving - -When proving, resource logics take as input resources created and consumed in the action: - -#### Instance - -1. [[Computable components#Tag | Resource tag]] — identifies the current resource being checked -2. `isConsumed` - a flag that tells the logic if the resource is consumed or created -3. `action.consumed` (possibly excluding the tagged resource, if it is consumed) -4. `action.created` (possibly excluding the tagged resource, if it is created) -5. `action.applicationData[tag]` - -#### Witness - -1. for consumed resources: `OrderedSet (Resource, NullifierKey)` - -2. for created resources: `OrderedSet Resource` - -3. Application inputs - -!!! note - 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) - -#### Constraints - -1. Created commitment integrity: `r.commitment() = cm` -2. Consumed nullifier integrity: `r.nullifier(nullifierKey) = nf` -3. Application constraints \ No newline at end of file diff --git a/docs/arch/system/state/resource_machine/data_structures/resource/index.juvix.md b/docs/arch/system/state/resource_machine/data_structures/resource/index.juvix.md deleted file mode 100644 index e1700f8abef..00000000000 --- a/docs/arch/system/state/resource_machine/data_structures/resource/index.juvix.md +++ /dev/null @@ -1,27 +0,0 @@ ---- -icon: material/file-document-outline -search: - exclude: false - boost: 2 ---- - -```juvix -module arch.system.state.resource_machine.data_structures.resource.index; -``` - -# Resource - -A **resource** is a composite structure `Resource` that contains the following components: - -|Component|Type|Description| -|-|-|-| -|`logicRef`|`LogicHash`|[[Hash]] of the predicate associated with the resource (resource logic)| -|`labelRef`|`LabelHash`|[[Hash]] of the resource label. Resource label specifies the fungibility domain for the resource. Resources within the same fungibility domain are seen as equivalent kinds of different quantities. Resources from different fungibility domains are seen and treated as non-equivalent kinds. This distinction comes into play in the balance check described later| -|`valueRef`|`ValueHash`|[[Hash]] of the resource value. Resource value is the fungible data associated with the resource. It contains extra information but does not affect the resource's fungibility| -|`quantity`|`Quantity`|is a number representing the quantity of the resource| -|`isEphemeral`|`Bool`|is a flag that reflects the resource's ephemerality. Ephemeral resources do not get checked for existence when being consumed| -|`nonce`|`Nonce`|guarantees the uniqueness of the resource computable components| -|`nullifierKeyCommitment`|`NullifierKeyCommitment`|is a nullifier key commitment. Corresponds to the nullifier key $nk$ used to derive the resource nullifier (nullifiers are further described [[Nullifier|here]])| -|`randSeed`|`RandSeed`|randomness seed used to derive whatever randomness needed| - -To distinguish between the resource data structure consisting of the resource components and a resource as a unit of state identified by just one (or some) of the resource computed fields, we sometimes refer to the former as a *resource object*. Data which is referenced by the resource object - such as the preimage of `valueRef` - we refer to as *resource-linked data*. \ No newline at end of file diff --git a/docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md b/docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md deleted file mode 100644 index 3e69ab5e189..00000000000 --- a/docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md +++ /dev/null @@ -1,72 +0,0 @@ ---- -icon: material/file-document-outline -search: - exclude: false - boost: 2 ---- - -```juvix -module arch.system.state.resource_machine.data_structures.transaction.transaction; -``` - -# Transaction - -A transaction is a necessary and sufficient collection of fields required to validate and apply a state update to the state. -It is a composite structure that contains the following components: - -|Component|Type|Description| -|-|-|-| -|`CMTreeRoots`|`Set CMtree.Value`|A set of valid commitment tree roots used to prove the existence of the resources being consumed in the transaction. This set is not a part of actions to avoid duplication of data| -|`actions`|`Set Action`|A set of actions that comprise the transaction| -|`deltaProof`|`DeltaProvingSystem.Proof`|Balance proof. It makes sure that `transactionDelta` is correctly derived from the actions' deltas and commits to the expected publicly known value, called a _balancing value_. There is just one delta proof per transaction| - -## Interface - -1. `create(Set CMtree.Value, Set Actions) -> Transaction` -2. `compose(Transaction, Transaction) -> Transaction` -3. `verify(Transaction) -> Bool` -4. `delta(Transaction) -> DeltaHash` - -## `create` -Given a set of roots and a set of actions, a transaction is formed as follows: - -1. `tx.CMTreeRoots = CMTreeRoots` -2. `tx.actions = actions` -3. `tx.transactionDelta = sum(action.Delta() for action in actions)` -4. `tx.deltaProof = DeltaProvingSystem(deltaProvingKey, deltaInstance, deltaWitness)` - - -## `compose` - -Having two transactions `tx1` and `tx2`, their composition `compose(tx1, tx2)` is defined as a transaction `tx`, where: - -1. `tx.CMTreeRoots = Set.union(tx1.CMTreeRoots, tx2.CMTreeRoots)` -2. `tx.actions = Set.union(tx1.actions, tx2.actions)` -3. `tx.deltaProof = DeltaProvingSystem.aggregate(tx1.deltaProof, tx2.deltaProof)` -4. `tx.transactionDelta = tx1.transactionDelta + tx2.transactionDelta` - -!!! note - When composing transactions, action sets are simply united without composing the actions themselves. For example, composing a transaction with two actions and another transaction with three actions will result in a transaction with five actions. - -## `verify` - -A transaction is considered _valid_ if the following statements hold: - -Checks that do not require access to global structures: - -1. all actions in the transaction are valid, as defined per [[Action#`verify` | action validity rules]] -1. actions partition the state change induced by the transaction: - 1. there is no resource created more than once across actions - 2. there is no resource consumed more than once across actions -3. `deltaProof` is valid - -Checks that require access to global `CMTree` and `NullifierSet`: - -1. each created resource wasn't created in prior transactions -2. each consumed resource wasn't consumed in prior transactions - -A transaction is *executable* if it is valid and `transactionDelta` commits to the expected balancing value. - -## `delta` - -Transaction delta is a hash of _transaction balance_ - the total quantity change per resource kind induced by the transaction. It isn't computed from the transaction balance directly by applying a hash function to it, but rather by using the homomoprhic properties of `deltaHash`: adding action deltas together results in transaction delta. \ No newline at end of file From d9d62069a76740d4bff7c61635a752f04e896438 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Tue, 31 Dec 2024 13:28:07 -0500 Subject: [PATCH 11/39] Update nav and, update everything.juvix.md and indexes. --- docs/arch/system/types.juvix.md | 27 +++++++++++ docs/everything.juvix.md | 80 +++++++++++++++++++-------------- mkdocs.yml | 12 ++++- 3 files changed, 85 insertions(+), 34 deletions(-) create mode 100644 docs/arch/system/types.juvix.md diff --git a/docs/arch/system/types.juvix.md b/docs/arch/system/types.juvix.md new file mode 100644 index 00000000000..514781489fa --- /dev/null +++ b/docs/arch/system/types.juvix.md @@ -0,0 +1,27 @@ +--- +icon: material/pillar +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types; + ``` + +# Basic types in the system + + +```juvix +import arch.system.types.nullifier; +import arch.system.types.nullifierkey; +import arch.system.types.nullifier_properties; +import arch.system.types.resource; +import arch.system.types.resource_machine; +import arch.system.types.state; +import arch.system.types.resource_logic_proof; +import arch.system.types.action; +import arch.system.types.transaction; +``` diff --git a/docs/everything.juvix.md b/docs/everything.juvix.md index d57ca785185..6152b4c75c1 100644 --- a/docs/everything.juvix.md +++ b/docs/everything.juvix.md @@ -24,39 +24,53 @@ import arch.system.identity.identity; {- Resource Machine -} -import arch.system.state.resource_machine.data_structures.transaction.transaction_with_payment; -import arch.system.state.resource_machine.data_structures.transaction.transaction; -import arch.system.state.resource_machine.data_structures.transaction.transaction_function; -import arch.system.state.resource_machine.data_structures.transaction.delta_proof; -import arch.system.state.resource_machine.data_structures.compliance_unit.compliance_proof; -import arch.system.state.resource_machine.data_structures.compliance_unit.compliance_unit; -import arch.system.state.resource_machine.data_structures.action.resource_logic_proof; -import arch.system.state.resource_machine.data_structures.action.index; -import arch.system.state.resource_machine.data_structures.resource.computable_components.resource_commitment; -import arch.system.state.resource_machine.data_structures.resource.computable_components.kind; -import arch.system.state.resource_machine.data_structures.resource.computable_components.nullifier; -import arch.system.state.resource_machine.data_structures.resource.computable_components.delta; -import arch.system.state.resource_machine.data_structures.resource.computable_components.introduction; -import arch.system.state.resource_machine.data_structures.resource.index; -import arch.system.state.resource_machine.primitive_interfaces.transaction_function_vm; -import arch.system.state.resource_machine.primitive_interfaces.set; -import arch.system.state.resource_machine.primitive_interfaces.nullifier_set; -import arch.system.state.resource_machine.primitive_interfaces.map; -import arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_types; -import arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_delta; -import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.fixed_size_type; -import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.hash; -import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.delta_hash; -import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.arithmetic; -import arch.system.state.resource_machine.primitive_interfaces.index; -import arch.system.state.resource_machine.primitive_interfaces.ordered_set; -import arch.system.state.resource_machine.primitive_interfaces.commitment_accumulator; -import arch.system.state.resource_machine.notes.storage; -import arch.system.state.resource_machine.notes.function_formats.transaction_function_format; -import arch.system.state.resource_machine.notes.applications; -import arch.system.state.resource_machine.notes.roles_and_requirements; -import arch.system.state.resource_machine.index; -import arch.system.state.resource_machine.execution_flow.flow; +{- Types -} + +import arch.system.types.nullifier; +import arch.system.types.nullifierkey; +import arch.system.types.nullifier_properties; + +import arch.system.types.resource; +import arch.system.types.resource_machine; +import arch.system.types.resource_logic_proof; +import arch.system.types.action; +import arch.system.types.transaction; +import arch.system.types.state; + +import arch.system.types; + +-- import arch.system.state.resource_machine.data_structures.transaction.transaction_with_payment; +-- import arch.system.state.resource_machine.data_structures.transaction.transaction; +-- import arch.system.state.resource_machine.data_structures.transaction.transaction_function; +-- import arch.system.state.resource_machine.data_structures.transaction.delta_proof; +-- import arch.system.state.resource_machine.data_structures.compliance_unit.compliance_proof; +-- import arch.system.state.resource_machine.data_structures.compliance_unit.compliance_unit; +-- import arch.system.state.resource_machine.data_structures.action.resource_logic_proof; +-- import arch.system.state.resource_machine.data_structures.action.index; +-- import arch.system.state.resource_machine.data_structures.resource.computable_components.resource_commitment; +-- import arch.system.state.resource_machine.data_structures.resource.computable_components.kind; +-- import arch.system.state.resource_machine.data_structures.resource.computable_components.delta; +-- import arch.system.state.resource_machine.data_structures.resource.computable_components.introduction; +-- import arch.system.state.resource_machine.data_structures.resource.index; +-- import arch.system.state.resource_machine.primitive_interfaces.transaction_function_vm; +-- import arch.system.state.resource_machine.primitive_interfaces.set; +-- import arch.system.state.resource_machine.primitive_interfaces.nullifier_set; +-- import arch.system.state.resource_machine.primitive_interfaces.map; +-- import arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_types; +-- import arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_delta; +-- import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.fixed_size_type; +-- import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.hash; +-- import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.delta_hash; +-- import arch.system.state.resource_machine.primitive_interfaces.fixed_size_type.arithmetic; +-- import arch.system.state.resource_machine.primitive_interfaces.index; +-- import arch.system.state.resource_machine.primitive_interfaces.ordered_set; +-- import arch.system.state.resource_machine.primitive_interfaces.commitment_accumulator; +-- import arch.system.state.resource_machine.notes.storage; +-- import arch.system.state.resource_machine.notes.function_formats.transaction_function_format; +-- import arch.system.state.resource_machine.notes.applications; +-- import arch.system.state.resource_machine.notes.roles_and_requirements; +-- import arch.system.state.resource_machine.index; +-- import arch.system.state.resource_machine.execution_flow.flow; {- Types -} diff --git a/mkdocs.yml b/mkdocs.yml index e2a3bf7681c..bf6a64a94a3 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -18,6 +18,16 @@ nav: - ./arch/system/index.md - Identity Architecture: ./arch/system/identity/identity.juvix.md - State Architecture: + - Types: + - Resource: ./arch/system/types/resource.juvix.md + - Nullifier: ./arch/system/types/nullifier.juvix.md + - Nullifier key: ./arch/system/types/nullifierkey.juvix.md + - Nullifier properties: ./arch/system/types/nullifier_properties.juvix.md + - Resource machine: ./arch/system/types/resource_machine.juvix.md + - Transaction : ./arch/system/types/transaction.juvix.md + - Action: ./arch/system/types/action.juvix.md + - Resource logic proof: ./arch/system/types/resource_logic_proof.juvix.md + - State: ./arch/system/types/state.juvix.md - Resource Machine: - ./arch/system/state/resource_machine/index.juvix.md - Primitive interfaces: @@ -44,7 +54,7 @@ nav: - Computable components: - ./arch/system/state/resource_machine/data_structures/resource/computable_components/introduction.juvix.md - Commitment: ./arch/system/state/resource_machine/data_structures/resource/computable_components/resource_commitment.juvix.md - - Nullifier: ./arch/system/state/resource_machine/data_structures/resource/computable_components/nullifier.juvix.md + - Nullifier: ./arch/system/types/nullifier.juvix.md - Kind: ./arch/system/state/resource_machine/data_structures/resource/computable_components/kind.juvix.md - Delta: ./arch/system/state/resource_machine/data_structures/resource/computable_components/delta.juvix.md - Compliance unit: From a46dc3def10377610c0d8b0e77e5e0ad7c5498ee Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:47:20 -0500 Subject: [PATCH 12/39] Add documentation for Commitment type --- docs/arch/system/types/commitment.juvix.md | 67 ++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 docs/arch/system/types/commitment.juvix.md diff --git a/docs/arch/system/types/commitment.juvix.md b/docs/arch/system/types/commitment.juvix.md new file mode 100644 index 00000000000..446ada49274 --- /dev/null +++ b/docs/arch/system/types/commitment.juvix.md @@ -0,0 +1,67 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - commitment + - resource-machine +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.commitment; + import prelude open; + import arch.node.types.crypto open; + ``` + +# Commitment + +## `Commitment` + +```juvix +type Commitment A := mkCommitment@{ + value : A; + hash : Digest; +}; +``` + +!!! todo + + Determine if the type parameter is necessary, or it should be just + String/Bytestring or something else. + +???+ quote "Arguments" + + `value` + : The value that is committed to. + + `hash` + : The hash of the value. + +## Purpose + +Commitments are used to prove the existence of a value without revealing the +value itself. In the context of the resource machine, they are used to prove the +existence of resources. Precisely, commitments are meant to be stored in the +state of the resource machine in a [[CommitmentTree|commitment tree]] to be +queried by the resource machine. + +## Properties + +!!! todo + + Add properties of the commitment. + +??? quote "Auxiliary Juvix code" + + ```juvix + instance + Commitment-Eq {A} {{Eq A}} : Eq (Commitment A) + := mkEq@{ + eq := \{c1 c2 := + Commitment.hash c1 == Commitment.hash c2 + } + }; + ``` From b31444193d15764ce73018ebef38143de7f15933 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:47:39 -0500 Subject: [PATCH 13/39] Enhance Action documentation and add tags for better categorization --- docs/arch/system/types/action.juvix.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/docs/arch/system/types/action.juvix.md b/docs/arch/system/types/action.juvix.md index 8aa25a0cf0c..2d5841364d0 100644 --- a/docs/arch/system/types/action.juvix.md +++ b/docs/arch/system/types/action.juvix.md @@ -4,6 +4,10 @@ icon: material/file-document-outline search: exclude: false boost: 2 +tags: + - action + - transaction + - resource-machine --- ??? quote "Juvix imports" @@ -12,6 +16,7 @@ search: module arch.system.types.action; import prelude open; import arch.system.types.nullifier open; + import arch.system.types.commitment open; ``` # Actions From efd921144ff9887a1ec6629514d8ee4f2a898fff Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:48:19 -0500 Subject: [PATCH 14/39] Add documentation for Commitment Trees in Juvix This commit introduces a new documentation file detailing the `CommitmentTree` and its associated types, including `MTree`, `CTree`, and `Path`. --- .../arch/system/types/commitmenttree.juvix.md | 144 ++++++++++++++++++ 1 file changed, 144 insertions(+) create mode 100644 docs/arch/system/types/commitmenttree.juvix.md diff --git a/docs/arch/system/types/commitmenttree.juvix.md b/docs/arch/system/types/commitmenttree.juvix.md new file mode 100644 index 00000000000..c13fe1e3f95 --- /dev/null +++ b/docs/arch/system/types/commitmenttree.juvix.md @@ -0,0 +1,144 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - commitment-tree + - state +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.commitmenttree; + import prelude open; + import arch.node.types.crypto open; + import arch.system.types.commitment open; + ``` + +# Commitment Trees + +## `MTree` + +A `MTree` is a data structure that accumulates the output related to the values +of its children in the node `merge`. In the leaves, we store the some particular +data. + +```juvix +type MTree A B := + | mkMTreeLeaf@{ value : A } + | mkMTreeNode@{ + merge : B; + left : MTree A B; + right : MTree A B } + ; +``` + +???+ quote "`MTree` constructors" + + `mkMTreeLeaf` + : A leaf node in the tree which stores some particular data. + + `mkMTreeNode` + : An internal node in the tree which stores the merge of the two sub-trees, + and the two sub-trees themselves. +## `CTree` + +The `CTree` type is formally defined as a specialised `MTree` where the leaf +nodes store [[Commitment|`Commitment` values]] and the internal nodes store +[[hashes]], precisely. These hashes, `Digest` values, in the internal nodes +represent the combined hash of their child nodes. See *merkle trees* for more +information. + +```juvix +CTree (A : Type) : Type := MTree (Commitment A) Digest; +``` + +## `Path` + +A *path* is a sequence of `PathDir` values used to navigate through a `CTree` by +specifying the direction to take at each node. + +### `PathDir` + +```juvix +type PathDir := + | PathDirLeft + | PathDirRight + | PathDirHere; +``` + +```juvix +Path : Type := List PathDir; +``` + +## `CommitmentTree` + +A *commitment tree* is a read-append-only structure that allows you to store +commitments, and to verify that a commitment is in the tree. + +```juvix +trait +type CommitmentTree A := + mkCommitmentTree@{ + add : Commitment A -> CTree A -> Path; + path : Commitment A -> CTree A -> Option Path; + hashRoot : CTree A -> Digest; + verify : Path -> Commitment A -> Bool; + }; +``` + +???+ quote "`CommitmentTree` constructors" + + `add` + : Adds a `Commitment` to the `CommitmentTree`. + + `path` + : Returns the `Path` to a `Commitment` in the `CommitmentTree`. + + `hashRoot` + : Returns the `Digest` of the root of the `CommitmentTree`. + + `verify` + : Verifies a `Path` of a `Commitment` in the `CommitmentTree`. + +### `CommitmentTree` instance + +In particular, a `CTree` is an instance of the `CommitmentTree` trait. + +!!! todo + + Update the definitions below for CTree. + +#### `addToMTree` + +``` +terminating +addToMTree {A} (tree : MTree A) (a : A) : MTree A := + case tree of { + | MTreeLeaf rval := MTreeNode (MTreeLeaf a) (MTreeLeaf rval) + | MTreeNode lTree rTree := MTreeNode (addToMTree lTree a) rTree + } +``` + +#### `getMTreePath` + +``` +terminating -- TODO: it's failing to see that the function is terminating +getMTreePath {A} {{Eq A}} (tree : MTree A) (a : A) : Option Path := + case tree of { + | (MTreeLeaf rval) := + if | a == rval := some [PathDirHere] + | else := none + | (MTreeNode lTree rTree) := + case getMTreePath lTree a of { + | some lPath := some (PathDirLeft :: lPath) + | none := + case getMTreePath rTree a of { + | some rPath := some (PathDirRight :: rPath) + | none := none + } + } + } +``` \ No newline at end of file From 797272d501197d239f2cbedf9583530a21cb8e92 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:48:46 -0500 Subject: [PATCH 15/39] Update nullifier and nullifier key documentation with clarifications and Markdown tags --- docs/arch/system/types/nullifier_properties.juvix.md | 5 +++++ docs/arch/system/types/nullifierkey.juvix.md | 11 ++++++++--- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/docs/arch/system/types/nullifier_properties.juvix.md b/docs/arch/system/types/nullifier_properties.juvix.md index 5785b463d5d..0e99ea5a21b 100644 --- a/docs/arch/system/types/nullifier_properties.juvix.md +++ b/docs/arch/system/types/nullifier_properties.juvix.md @@ -32,6 +32,11 @@ tags: axiom nullifierHash : Nullifier -> Digest; ``` +!!! todo + + How are we supposed to define the `computeNullifier` and `nullifierHash` + functions? + The following properties must hold true to consider a nullifier valid: ### Nullifier key must match the resource's nullifier key commitment diff --git a/docs/arch/system/types/nullifierkey.juvix.md b/docs/arch/system/types/nullifierkey.juvix.md index 766e74ffa8d..4bead55ac5b 100644 --- a/docs/arch/system/types/nullifierkey.juvix.md +++ b/docs/arch/system/types/nullifierkey.juvix.md @@ -3,6 +3,10 @@ icon: material/file-document-outline search: exclude: false boost: 2 +tags: + - nullifier + - resource-machine + - crypto --- ??? quote "Juvix imports" @@ -15,9 +19,10 @@ search: # Nullifier Key -A *resource nullifier key* is of type `NullifierKey`. A nullifier key is data -used to compute the nullifier of a resource and expected to be unique for each -resource. +A *resource nullifier key* is of type `NullifierKey`, sometimes called +*nullifier key commitment*. A nullifier key is data `NullifierKey`. A nullifier +key is data used to compute the nullifier of a resource and expected to be +unique for each resource. ## `NullifierKey` From 7ecbf0a9e71a16e6f055cfdbbdc408d2fc80c783 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:49:18 -0500 Subject: [PATCH 16/39] Enhance resource documentation with new type synonyms and properties - Added type synonyms for `LogicHash`, `LabelHash`, `ValueHash`, `Nonce`. - Updated `Resource` type definition to include `nullifierKey` and `randSeed`. - Clarified the purpose and properties of resources, emphasizing uniqueness, fungibility, nullification, and ephemerality. - Introduced tags for better categorization: resource-logic-proof, resource-machine, security, proof. --- docs/arch/system/types/resource.juvix.md | 67 +++++++++++++++---- .../types/resource_logic_proof.juvix.md | 5 ++ 2 files changed, 58 insertions(+), 14 deletions(-) diff --git a/docs/arch/system/types/resource.juvix.md b/docs/arch/system/types/resource.juvix.md index 526c2a7b39b..d0797dbd59d 100644 --- a/docs/arch/system/types/resource.juvix.md +++ b/docs/arch/system/types/resource.juvix.md @@ -11,22 +11,53 @@ search: module arch.system.types.resource; import prelude open; import arch.node.types.crypto open; + import arch.system.types.nullifierkey open; ``` # Resource -A **resource** is a composite structure `Resource` that contains the following components: +A **resource** is of type `Resource`. ## `Resource` +??? quote "Auxiliary Juvix code: Type synonyms" + + For the time being, the following type synonyms are used: + + ### `LogicHash` + + ```juvix + syntax alias LogicHash := Digest; + ``` + + ### `LabelHash` + + ```juvix + syntax alias LabelHash := Digest; + ``` + + ### `ValueHash` + + ```juvix + syntax alias ValueHash := Digest; + ``` + + ### `Nonce` + + ```juvix + syntax alias Nonce := Nat; + ``` + ```juvix type Resource := mkResource { - -- logicRef : LogicHash; - -- labelRef : LabelHash; - valueRef : Digest; - -- quantity : Quantity; + logicRef : LogicHash; + labelRef : LabelHash; + valueRef : ValueHash; + quantity : Nat; isEphemeral : Bool; - -- nonce : Nonce; + nonce : Nonce; + nullifierKey : NullifierKey; + randSeed : Nat; }; ``` @@ -58,18 +89,12 @@ type Resource := mkResource { : guarantees the uniqueness of the resource computable components `nullifierKeyCommitment` - : is a nullifier key commitment. Corresponds to the nullifier key $nk$ used to - the resource nullifier (nullifiers are further described [[Nullifier|here]]) + : is a nullifier key commitment. Corresponds to the nullifier key $nk$ used to + derive the resource nullifier (nullifiers are further described [[Nullifier|here]]) `randSeed` : randomness seed used to derive whatever randomness needed -To distinguish between the resource data structure consisting of the resource -components and a resource as a unit of state identified by just one (or some) of -the resource computed fields, we sometimes refer to the former as a *resource -object*. Data which is referenced by the resource object - such as the preimage -of `valueRef` - we refer to as *resource-linked data*. - ??? quote "Auxiliary Juvix code" @@ -84,3 +109,17 @@ of `valueRef` - we refer to as *resource-linked data*. instance ResourceOrd : Ord Resource; ``` + +## Purpose + +A resource represents a uniquely identifiable asset in the system. Resources can +be created, consumed, and transformed according to predefined logic rules. + +## Properties + +Resources have the following key properties: + +- Uniqueness: Each resource instance is uniquely identified by its components +- Fungibility: Resources sharing the same label are considered fungible +- Nullification: Resources can be consumed only once using their [[Nullifier|nullifier key]] +- Ephemerality: Ephemeral resources bypass existence checks when consumed diff --git a/docs/arch/system/types/resource_logic_proof.juvix.md b/docs/arch/system/types/resource_logic_proof.juvix.md index 61baef941b5..530c7ff4641 100644 --- a/docs/arch/system/types/resource_logic_proof.juvix.md +++ b/docs/arch/system/types/resource_logic_proof.juvix.md @@ -4,6 +4,11 @@ icon: material/file-document-outline search: exclude: false boost: 2 +tags: + - resource-logic-proof + - resource-machine + - security + - proof --- ??? quote "Juvix imports" From ed4ea45741f32f22e16400a06e0ffa3a045a3397 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:49:30 -0500 Subject: [PATCH 17/39] Add documentation for Tag type in Juvix --- docs/arch/system/types/tag.juvix.md | 31 +++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 docs/arch/system/types/tag.juvix.md diff --git a/docs/arch/system/types/tag.juvix.md b/docs/arch/system/types/tag.juvix.md new file mode 100644 index 00000000000..31dcec0c867 --- /dev/null +++ b/docs/arch/system/types/tag.juvix.md @@ -0,0 +1,31 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - resource-machine +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.tag; + import arch.system.types.commitment; + import arch.system.types.nullifier; + ``` + +# Tags + +A **tag** is a term of type `Tag`. + +## `Tag` + +```juvix +type Tag A := + | TagCommitment (Commitment A) + | TagNullifier Nullifier + ; +``` + From 44f71be65b181d89b8ebe420e80585c53023983e Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 1 Jan 2025 23:49:37 -0500 Subject: [PATCH 18/39] Add tags for better categorization in state documentation --- docs/arch/system/types/state.juvix.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/arch/system/types/state.juvix.md b/docs/arch/system/types/state.juvix.md index 4ae30674cd6..0cc18bb5a59 100644 --- a/docs/arch/system/types/state.juvix.md +++ b/docs/arch/system/types/state.juvix.md @@ -4,6 +4,8 @@ icon: material/file-document-outline search: exclude: false boost: 2 +tags: + - state --- ??? quote "Juvix imports" From aacadb38837bf24e5b85818fe46d791163d24b2a Mon Sep 17 00:00:00 2001 From: Anoma Research Date: Thu, 2 Jan 2025 05:00:19 +0000 Subject: [PATCH 19/39] Fix issues detected by pre-commit --- docs/arch/system/types/action.juvix.md | 14 +++++++------- docs/arch/system/types/commitmenttree.juvix.md | 10 +++++----- docs/arch/system/types/nullifier.juvix.md | 2 +- .../system/types/nullifier_properties.juvix.md | 2 +- docs/arch/system/types/resource.juvix.md | 4 ++-- docs/arch/system/types/resource_machine.juvix.md | 2 +- docs/arch/system/types/state.juvix.md | 2 +- docs/arch/system/types/transaction.juvix.md | 8 ++++---- mkdocs.yml | 4 ++-- 9 files changed, 24 insertions(+), 24 deletions(-) diff --git a/docs/arch/system/types/action.juvix.md b/docs/arch/system/types/action.juvix.md index 2d5841364d0..c46614c7be1 100644 --- a/docs/arch/system/types/action.juvix.md +++ b/docs/arch/system/types/action.juvix.md @@ -21,7 +21,7 @@ tags: # Actions -An **action** is a term of type `Action`. +An **action** is a term of type `Action`. ## `Action` @@ -60,14 +60,14 @@ type Action := mkAction { ??? quote "Auxiliary Juvix code: Instances" ```juvix - deriving - instance + deriving + instance eqAction : Eq Action; ``` ```juvix - deriving - instance + deriving + instance ordAction : Ord Action; ``` @@ -85,7 +85,7 @@ type Action := mkAction { \ No newline at end of file diff --git a/docs/arch/system/types/nullifier.juvix.md b/docs/arch/system/types/nullifier.juvix.md index 53d93855115..2bdbbc9ed1f 100644 --- a/docs/arch/system/types/nullifier.juvix.md +++ b/docs/arch/system/types/nullifier.juvix.md @@ -69,7 +69,6 @@ set part of the [[State|state]]. - The resource nullifier must not exist in the [[Nullifier Set|nullifier set]]. - ## Properties --8<-- "./nullifier_properties.juvix.md:properties" diff --git a/docs/arch/system/types/nullifier_properties.juvix.md b/docs/arch/system/types/nullifier_properties.juvix.md index e6817656a56..24889195cb8 100644 --- a/docs/arch/system/types/nullifier_properties.juvix.md +++ b/docs/arch/system/types/nullifier_properties.juvix.md @@ -43,7 +43,8 @@ The following properties must hold true to consider a nullifier valid: ```juvix match-nullifier-key - (r : Resource) (nk : NullifierKey) : Bool := + (r : Resource) + (nk : NullifierKey) : Bool := let n := mkNullifier@{key := nk; resource := r} in (computeNullifier r nk) == (nullifierHash n) ``` @@ -52,7 +53,9 @@ match-nullifier-key ``` unique-nullifier-property - (s : State) (r : Resource) (nk : NullifierKey) : Bool := + (s : State) + (r : Resource) + (nk : NullifierKey) : Bool := let nullifier := mkNullifier@{key := nk; resource := r}; nullifierSet : Set Nullifier := State.nullifierSet s; cond (other : Nullifier) : Bool := (Set.isMember other nullifierSet) && (other == nullifier) diff --git a/docs/arch/system/types/nullifierkey.juvix.md b/docs/arch/system/types/nullifierkey.juvix.md index 4bead55ac5b..8e179acb41b 100644 --- a/docs/arch/system/types/nullifierkey.juvix.md +++ b/docs/arch/system/types/nullifierkey.juvix.md @@ -28,7 +28,7 @@ unique for each resource. ```juvix type NullifierKey := mkNullifierKey { - key : SecretKey; + key : Digest; --TODO: What type I need to put here. Hash? }; ``` diff --git a/docs/arch/system/types/resource_machine.juvix.md b/docs/arch/system/types/resource_machine.juvix.md index 420f02fc0a6..494019ea846 100644 --- a/docs/arch/system/types/resource_machine.juvix.md +++ b/docs/arch/system/types/resource_machine.juvix.md @@ -27,6 +27,7 @@ A **resource machine** is a term of type `ResourceMachine`. ## `ResourceMachine` ```juvix +trait type ResourceMachine := mkResourceMachine { createTransaction : -- CMTreeRoots : Set CMtree.Value; diff --git a/docs/arch/system/types/state.juvix.md b/docs/arch/system/types/state.juvix.md index b1d51ebbd9d..b4a42a40bc4 100644 --- a/docs/arch/system/types/state.juvix.md +++ b/docs/arch/system/types/state.juvix.md @@ -19,14 +19,23 @@ tags: # State +???+ quote "Auxiliary Juvix code" + + ```juvix + axiom CommitmentAccumulator : Type; + ``` + + ```juvix + axiom DataBlobStorage : Type; + ``` ```juvix type State := mkState { - -- commitmentAccumulator : CommitmentAccumulator; + commitmentAccumulator {A : Type} {{CommitmentTreeOps A CTree}} : A ; -- secondCommitmentAccumulator : CommitmentAccumulator; nullifierSet : Set Nullifier; + dataBlobStorage : DataBlobStorage; -- hierarchicalIndex : HierarchicalIndex; - -- dataBlobStorage : DataBlobStorage; }; ``` From 3ffcfdd4266f3cb273dada5726a293d0d78da232 Mon Sep 17 00:00:00 2001 From: Anoma Research Date: Wed, 8 Jan 2025 20:57:57 +0000 Subject: [PATCH 32/39] Fix issues detected by pre-commit --- docs/arch/system/types/nullifier_properties.juvix.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/arch/system/types/nullifier_properties.juvix.md b/docs/arch/system/types/nullifier_properties.juvix.md index 24889195cb8..f44dd51a73a 100644 --- a/docs/arch/system/types/nullifier_properties.juvix.md +++ b/docs/arch/system/types/nullifier_properties.juvix.md @@ -43,7 +43,7 @@ The following properties must hold true to consider a nullifier valid: ```juvix match-nullifier-key - (r : Resource) + (r : Resource) (nk : NullifierKey) : Bool := let n := mkNullifier@{key := nk; resource := r} in (computeNullifier r nk) == (nullifierHash n) @@ -53,8 +53,8 @@ match-nullifier-key ``` unique-nullifier-property - (s : State) - (r : Resource) + (s : State) + (r : Resource) (nk : NullifierKey) : Bool := let nullifier := mkNullifier@{key := nk; resource := r}; nullifierSet : Set Nullifier := State.nullifierSet s; From 89843f34836358a59a05249b11a7be90839027b8 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Wed, 15 Jan 2025 11:51:40 -0500 Subject: [PATCH 33/39] Jan. Last code block. typecheck the file arch/system/../commitmenttree.juvix.md --- docs/arch/system/types/commitmenttree.juvix.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/arch/system/types/commitmenttree.juvix.md b/docs/arch/system/types/commitmenttree.juvix.md index 37319a6a9c8..c073d5e560d 100644 --- a/docs/arch/system/types/commitmenttree.juvix.md +++ b/docs/arch/system/types/commitmenttree.juvix.md @@ -131,7 +131,6 @@ as a `CTree` by specifying the direction to take at each node. type PathDir := | PathDirLeft | PathDirRight - | PathDirHere; ``` ### `CTreePath` @@ -149,7 +148,7 @@ CommitmentTree (A : Type) : Type := CommitmentTreeOps A CTree PathDir; ```