diff --git a/docs/arch/node/concepts/subsystem.md b/docs/arch/node/concepts/subsystem.md index 83764dadb50..e3d20fb0ed0 100644 --- a/docs/arch/node/concepts/subsystem.md +++ b/docs/arch/node/concepts/subsystem.md @@ -16,8 +16,9 @@ tags: specific goal. The purpose of a subsystem is to provide a high-level interface for the components that make up the node. -## Examples +## Subsystems - [[Hardware subsystem overview|Hardware subsystem]] - [[Identity subsystem overview|Identity subsystem]] - [[Ordering subsystem overview|Ordering subsystem]] +- [[Network subsystem overview|Network subsystem]] diff --git a/docs/arch/node/engines/mempool_worker_behaviour.juvix.md b/docs/arch/node/engines/mempool_worker_behaviour.juvix.md index befa1d014fd..55d16b82c8d 100644 --- a/docs/arch/node/engines/mempool_worker_behaviour.juvix.md +++ b/docs/arch/node/engines/mempool_worker_behaviour.juvix.md @@ -443,7 +443,7 @@ transactionRequestAction mailbox := some 0; msg := Anoma.MsgMempoolWorker (MempoolWorkerMsgTransactionAck (mkTransactionAck@{ - tx_hash := hash fingerprint candidate; + tx_hash := TChash fingerprint candidate; batch_number := MempoolWorkerLocalState.batch_number local; batch_start := 0; worker_id := worker_id; diff --git a/docs/arch/node/types/crypto.juvix.md b/docs/arch/node/types/crypto.juvix.md index 2e91c72ea68..e2c966e7e6d 100644 --- a/docs/arch/node/types/crypto.juvix.md +++ b/docs/arch/node/types/crypto.juvix.md @@ -8,6 +8,10 @@ tags: - types - crypto - prelude + - node-architecture + - types + - crypto + - prelude --- ??? code "Juvix imports" @@ -27,14 +31,25 @@ 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}; + }; + ``` + +### `PrivateKey` ### `PrivateKey` Private key for public-key cryptography. @@ -43,14 +58,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}; + }; + ``` + ### `SecretKey` Secret key for secret-key cryptography. @@ -61,7 +84,19 @@ type SecretKey := ; ``` -### `Signature` +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + SecretKeyEq : Eq SecretKey; + + deriving + instance + SecretKeyOrd : Ord SecretKey; + ``` + +### ``Signature`` Cryptographic signature. @@ -80,3 +115,23 @@ type Digest := | Blake3Digest ByteString ; ``` + +### `hash` + +```juvix +axiom hash {A} : A -> Digest; +``` + +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + DigestEq : Eq Digest; + + instance + DigestOrd : Ord Digest := + mkOrd@{ + cmp := \{(Blake3Digest a) (Blake3Digest b) := Equal}; + }; + ``` 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 2109345919d..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`|`OrderedSet Commitment`|contains commitments of resources created in this action| -|`consumed`|`OrderedSet Nullifier`|contains nullifiers of resources consumed in this action| -|`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| -|`complianceUnits`|`Set ComplianceUnit`|The set of transaction's [[Compliance unit | compliance units]]| -|`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.| - - -!!! note - 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. - -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/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/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/notes/function_formats/nockma.juvix.md b/docs/arch/system/state/resource_machine/notes/function_formats/nockma.juvix.md new file mode 100644 index 00000000000..f0eda6c8245 --- /dev/null +++ b/docs/arch/system/state/resource_machine/notes/function_formats/nockma.juvix.md @@ -0,0 +1,470 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.state.resource_machine.notes.function_formats.nockma; + import prelude open; + import Stdlib.Data.Nat open; + import Stdlib.Data.List open; + import arch.system.state.resource_machine.notes.function_formats.transactionfunction open; + ``` + +# Nockma Implementation + +```juvix +-- Operation codes for Nockma: +-- 0: Slash (/) +-- 1: Constant: Returns operand unchanged +-- 2: Apply/Ap/S: +-- 3: Cell test (?): Tests if noun is cell +-- 4: Increment (+): Add 1 to atom +-- 5: Equality test (=): Compare nouns +-- 6: If-then-else +-- 7: Compose +-- 8: Extend subject +-- 9: Invoke (call function by arm name) +-- 10: Pound (#) +-- 11: Match: Case split on Cells vs Atoms +-- 12: Scry (read storage) + +-- Basic Nock types +type Noun := + | Atom : Nat -> Noun + | Cell : Noun -> Noun -> Noun; + +terminating +nounEq (n1 n2 : Noun) : Bool := + case mkPair n1 n2 of { + | mkPair (Atom x) (Atom y) := x == y + | mkPair (Cell a b) (Cell c d) := nounEq a c && nounEq b d + | _ := false + }; + +instance EqNoun : Eq Noun := mkEq@{ eq := nounEq }; + +-- Helper to convert storage values to Nouns +axiom convertToNoun : {val : Type} -> val -> Noun; +-- Helper to convert Nouns to storage values +axiom convertFromNoun : {val : Type} -> Noun -> Option val; + +type ScryOp := + | Direct + | Index; + +type Storage addr val := mkStorage { + readDirect : addr -> Option val; + readIndex : val -> Option val +}; + +axiom externalStorage : {addr val : Type} -> Storage addr val; + +type NockOp := + | Slash -- / + | Constant -- Returns operand unchanged + | Apply + | CellTest -- ? + | Increment -- + + | EqualOp -- = + | IfThenElse -- 6 + | Compose -- 7 + | Extend -- 8 + | Invoke -- 9 + | Pound -- # + | Match -- 11 + | Scry; -- 12 + +opOr {A : Type} (n m : Option A) : Option A := + case n of { + | none := m + | (some n) := some n + }; + +parseOp (n : Nat) : Option NockOp := + let test := \{m op := + case (n == m) of { + | true := some op + | false := none + }} in + foldr opOr none + (zipWith test + [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12] + [Slash; Constant; Apply; CellTest; Increment; + EqualOp; IfThenElse; Compose; Extend; Invoke; + Pound; Match; Scry]); + +-- Monad to encompass gas consumption and error handling. +type GasState A := mkGasState { + runGasState : Nat -> Result String (Pair A Nat) +}; + +instance +GasStateMonad : Monad GasState := mkMonad@{ + applicative := mkApplicative@{ + functor := mkFunctor@{ + map := \{f s := mkGasState \{gas := + case GasState.runGasState s gas of { + | ok (mkPair x remaining) := ok (mkPair (f x) remaining) + | error e := error e + }} + }}; + pure := \{x := mkGasState \{gas := ok (mkPair x gas)}}; + ap := \{sf sa := mkGasState \{gas := + case GasState.runGasState sf gas of { + | ok (mkPair f remaining) := + case GasState.runGasState sa remaining of { + | ok (mkPair x final) := ok (mkPair (f x) final) + | error e := error e + } + | error e := error e + }} + } + }; + bind := \{ma f := mkGasState \{gas := + case GasState.runGasState ma gas of { + | ok (mkPair a remaining) := GasState.runGasState (f a) remaining + | error e := error e + }} + } +}; + +err {A : Type} (str : String) : GasState A := mkGasState \{_ := error str}; + +-- Gas cost values for each operation type +-- These are made up for demo purposes +getGasCost (cost : NockOp) : Nat := + case cost of { + | Slash := 1 + | CellTest := 1 + | Increment := 1 + | EqualOp := 2 + | IfThenElse := 3 + | Compose := 2 + | Extend := 2 + | Invoke := 3 + | Pound := 1 + | Scry := 10 + | _ := 0 + }; + +consume (op : NockOp) : GasState Unit := + mkGasState \{gas := + let cost := getGasCost op in + case cost > gas of { + | true := error "Out of gas" + | false := ok (mkPair unit (sub gas cost)) + }}; + +-- Implementation of storage read operations (scrying) +scry {val : Type} (stor : Storage Nat val) (op : ScryOp) (addr : Nat) : Result String Noun := + case op of { + | Direct := case Storage.readDirect stor addr of { + | some val := ok (convertToNoun val) + | none := error "Direct storage read failed" + } + | Index := case Storage.readDirect stor addr of { + | some indexFn := case Storage.readIndex stor indexFn of { + | some val := ok (convertToNoun val) + | none := error "Index computation failed" + } + | none := error "Index function not found" + } + }; + +-- Helper for slash (/) operations +terminating +slash {val : Type} (stor : Storage Nat val) (n : Noun) (subject : Noun) : GasState Noun := + case n of { + | Atom x := case x == 1 of { + | true := pure subject -- Rule: /[1 a] -> a + | false := case x == 2 of { + | true := case subject of { -- Rule: /[2 a b] -> a + | Cell a _ := pure a + | _ := err "Cannot take slash of atom" + } + | false := case x == 3 of { + | true := case subject of { -- Rule: /[3 a b] -> b + | Cell _ b := pure b + | _ := err "Cannot take slash of atom" + } + | false := case (mod x 2) == 0 of { + | true := -- Rule: /[(a + a) b] -> /[2 /[a b]] + consume Slash >>= \{_ := + slash stor (Atom (div x 2)) subject >>= \{res := + consume Slash >>= \{_ := + slash stor (Atom 2) res + }}} + | false := -- Rule: /[(a + a + 1) b] -> /[3 /[a b]] + consume Slash >>= \{_ := + slash stor (Atom (div x 2)) subject >>= \{res := + consume Slash >>= \{_ := + slash stor (Atom 3) res + }}} + } + } + } + } + | _ := err "Slash must be atom" + }; + +-- Helper for pound (#) operations +terminating +pound {val : Type} (stor : Storage Nat val) (n : Noun) (b : Noun) (c : Noun) : GasState Noun := + case n of { + | Atom x := case x == 1 of { + | true := pure b -- Rule: #[1 a b] -> a + | false := case mod x 2 == 0 of { + | true := case c of { -- Rule: #[(a + a) b c] -> #[a [b /[(a + a + 1) c]] c] + | Cell _ _ := + consume Slash >>= \{_ := + slash stor (Atom ((2 * div x 2) + 1)) c >>= \{slashResult := + consume Pound >>= \{_ := + pound stor (Atom (div x 2)) (Cell b slashResult) c + }}} + | _ := err "Invalid pound target" + } + | false := case c of { -- Rule: #[(a + a + 1) b c] -> #[a [/[(a + a) c] b] c] + | Cell _ _ := + consume Slash >>= \{_ := + slash stor (Atom (2 * div x 2)) c >>= \{slashResult := + consume Pound >>= \{_ := + pound stor (Atom (div x 2)) (Cell slashResult b) c + }}} + | _ := err "Invalid pound target" + } + } + } + | _ := err "Pound must be atom" + }; + +terminating +evalOp {val : Type} (stor : Storage Nat val) (op : NockOp) (a : Noun) (args : Noun) : GasState Noun := + case op of { + -- *[a 0 b] -> /[b a] + | Slash := slash stor args a + + -- *[a 1 b] -> b + | Constant := pure args + + -- *[a 2 b c] -> *[*[a b] *[a c]] + | Apply := case args of { + | Cell b c := + nock stor (Cell a b) >>= \{r1 := + nock stor (Cell a c) >>= \{r2 := + nock stor (Cell r1 r2) + }} + | _ := err "Invalid apply args" + } + + -- *[a 3 b] -> ?*[a b] + -- ?[a b] -> 0 + -- ?a -> 1 + | CellTest := case args of { + | Cell b _ := + nock stor (Cell a b) >>= \{res := + case res of { + | Cell _ _ := pure (Atom 0) + | _ := pure (Atom 1) + } + } + | _ := err "Invalid cell test args" + } + + -- *[a 4 b] -> +*[a b] + -- +[a b] -> +[a b] + -- +a -> 1 + a + | Increment := case args of { + | Cell b _ := + nock stor (Cell a b) >>= \{res := + case res of { + | (Atom n) := pure (Atom (suc n)) + | x := pure x -- +[a b] -> +[a b] case + } + } + | _ := err "Invalid increment args" + } + + -- *[a 5 b c] -> =*[a b] *[a c] + -- =[a a] -> 0 + -- =[a b] -> 1 + | EqualOp := case args of { + | Cell b c := + nock stor (Cell a b) >>= \{r1 := + nock stor (Cell a c) >>= \{r2 := + pure (Atom (case nounEq r1 r2 of { + | true := 0 + | false := 1 + })) + }} + | _ := err "Invalid equality args" + } + + -- *[a 6 b c d] -> *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]] + | IfThenElse := case args of { + | Cell b (Cell c d) := + nock stor (Cell a (Cell (Atom 4) (Cell (Atom 4) b))) >>= \{r1 := + nock stor (Cell (Cell (Atom 2) (Atom 3)) (Cell (Atom 0) r1)) >>= \{r2 := + nock stor (Cell (Cell c d) (Cell (Atom 0) r2)) >>= \{r3 := + nock stor (Cell a r3) + }}} + | _ := err "Invalid if-then-else args" + } + + -- *[a 7 b c] -> *[*[a b] c] + | Compose := case args of { + | Cell b c := + nock stor (Cell a b) >>= \{r := + nock stor (Cell r c) + } + | _ := err "Invalid compose args" + } + + -- *[a 8 b c] -> *[[*[a b] a] c] + | Extend := case args of { + | Cell b c := + nock stor (Cell a b) >>= \{r := + nock stor (Cell (Cell r a) c) + } + | _ := err "Invalid extend args" + } + + -- *[a 9 b c] -> *[*[a c] 2 [0 1] 0 b] + | Invoke := case args of { + | Cell b c := + nock stor (Cell a c) >>= \{core := + let formula := Cell (Atom 2) (Cell (Cell (Atom 0) (Atom 1)) (Cell (Atom 0) b)) in + nock stor (Cell core formula) + } + | _ := err "Invalid invoke args" + } + + -- *[a 10 [b c] d] -> #[b *[a c] *[a d]] + | Pound := case args of { + | Cell (Cell b c) d := + nock stor (Cell a c) >>= \{r1 := + nock stor (Cell a d) >>= \{r2 := + pound stor b r1 r2 + }} + | _ := err "Invalid pound args" + } + + -- *[a 11 [b c] d] -> *[[*[a c] *[a d]] 0 3] + -- *[a 11 b c] -> *[a c] + | Match := case args of { + | Cell (Cell b c) d := + nock stor (Cell a c) >>= \{r1 := + nock stor (Cell a d) >>= \{r2 := + nock stor (Cell (Cell r1 r2) (Cell (Atom 0) (Atom 3))) + }} + | Cell _ c := nock stor (Cell a c) + | _ := err "Invalid pure pound args" + } + + -- *[a 12 b c d] -> result <- SCRY b c; *[a result d] + | Scry := case args of { + | Cell b (Cell c d) := + -- First evaluate b to get the opcode + nock stor b >>= \{opcode := + case opcode of { + | Atom opval := + -- Then evaluate c to get the address + nock stor c >>= \{addr := + case addr of { + | Atom addrVal := + -- Convert opcode to ScryOp + let scryType := case opval == 0 of { + | true := Direct + | false := Index + } in + -- Perform the scry operation and wrap result in GasState + mkGasState \{gas := + scry stor scryType addrVal >>= \{scryResult := + -- Continue evaluation with the scry result + GasState.runGasState (nock stor (Cell a (Cell scryResult d))) gas + } + } + | _ := err "Scry address must be atom" + } + } + | _ := err "Scry type must be atom" + } + } + | _ := err "Invalid scry args" + } + }; + +-- Core Nockma evaluator +terminating +nock {val : Type} (stor : Storage Nat val) (input : Noun) : GasState Noun := + case input of { + -- Rule: *a -> *a + | Atom _ := pure input + + | Cell a b := case b of { + + | Cell first rest := case first of { + -- Rule: *[a [b c] d] -> [*[a b c] *[a d]] + | Cell b c := + nock stor (Cell a (Cell b c)) >>= \{r1 := + nock stor (Cell a rest) >>= \{r2 := + pure (Cell r1 r2) + }} + + | Atom n := case parseOp n of { + | some opcode := consume opcode >>= \{_ := + evalOp stor opcode a rest + } + | none := err "Invalid operation" + } + } + | _ := err "Invalid Nock expression" + } + }; +``` + +Nockma instances for transaction function functionality; + +```juvix +instance +NockmaTransactionFunction : TransactionFunction Noun Nat (Option Noun) Nat Noun Noun := + mkTransactionFunction@{ + readStorage := \{addr := + Cell (Atom 12) (Cell (Atom 0) (Cell (Atom addr) (Atom 1))) + }; + readByIndex := \{prog := + Cell (Atom 12) (Cell (Atom 1) (Cell prog (Atom 1))) + }; + cost := \{prog := + -- Simple cost model: sums gas cost of all appearing operations + let + terminating + countNodes (n : Noun) : Nat := + case n of { + | Atom a := + case parseOp a of { + | some op := getGasCost op + | none := 0 + } + | Cell a b := countNodes a + countNodes b + }; + in countNodes prog + }; + }; + +instance +NockmaVM : TransactionVM Noun Nat (Option Noun) Nat Noun Noun := + mkTransactionVM@{ + txFunc := NockmaTransactionFunction; + eval := \{prog gas := + case GasState.runGasState (nock (externalStorage {Nat} {Nat}) prog) gas of { + | ok result := ok (fst result) + | error msg := error msg + } + }; + }; +``` \ No newline at end of file diff --git a/docs/arch/system/state/resource_machine/notes/function_formats/transactionfunction.juvix.md b/docs/arch/system/state/resource_machine/notes/function_formats/transactionfunction.juvix.md new file mode 100644 index 00000000000..7779f64d2fc --- /dev/null +++ b/docs/arch/system/state/resource_machine/notes/function_formats/transactionfunction.juvix.md @@ -0,0 +1,38 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.state.resource_machine.notes.function_formats.transactionfunction; + import prelude open; + ``` + +# Transaction Function types + +## `TransactionFunction` + +```juvix +trait +type TransactionFunction (prog addr val gas idx tx : Type) := + mkTransactionFunction@{ + readStorage : addr -> prog; + readByIndex : prog -> prog; + cost : prog -> gas; + }; +``` + +## `TransactionVM` + +```juvix +trait +type TransactionVM (prog addr val gas idx tx : Type) := + mkTransactionVM@{ + {{txFunc}} : TransactionFunction prog addr val gas idx tx; + eval : prog -> gas -> Result String tx; + }; +``` diff --git a/docs/arch/system/state/resource_machine/prelude.juvix.md b/docs/arch/system/state/resource_machine/prelude.juvix.md new file mode 100644 index 00000000000..a4654aec536 --- /dev/null +++ b/docs/arch/system/state/resource_machine/prelude.juvix.md @@ -0,0 +1,460 @@ +--- +icon: material/database +search: + exclude: false +categories: +- resource-machine +tags: +- data-structures +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.state.resource_machine.prelude; + import prelude open; + import arch.node.types.crypto open using {Digest}; + ``` + +## Overview + +This file defines the core data structures and traits (interfaces) used by the Resource Machine (RM). + +The RM uses three main container types: + +- `Set`: Stores unique items like resource commitments and nullifiers. +- `Map`: Holds key-value pairs, such as environment references or application data. +- `List`: Keeps ordered sequences, like proofs or resources. + +Additionally, the RM requires several traits for its data structures listed +below. + +- `FixedSize`: Ensures that certain types have a fixed bit length. +- `Arithmetic`: Provides basic arithmetic operations, inheriting from `FixedSize`. +- `Hash`: Defines hashing functionality, inheriting from `FixedSize`. +- `ISet`: An interface defining standard set operations. +- `IOrderedSet`: Extends `ISet` to maintain elements in a specific order. +- `IMap`: An interface defining standard map operations. + +### Aliases + +The RM frequently uses hashes for commitments and nullifiers. + +There are a variety of hashes of unspecified character appearing in the RM which +we declare here as aliases of `Digest`. + +#### `ValueHash` + +```juvix +syntax alias ValueHash := Digest; +``` + +#### `DeltaHash` + +```juvix +syntax alias DeltaHash := Digest; +``` + +#### `LabelHash` + +```juvix +syntax alias LabelHash := Digest; +``` + +#### `LogicHash` + +```juvix +syntax alias LogicHash := Digest; +``` + +#### `Quantity` + +There are two numeric types of unspecified character mentioned in the RM, which +we declare here as aliases to `Nat`. + +```juvix +syntax alias Quantity := Nat; +``` + +#### `Balance` + +```juvix +syntax alias Balance := Nat; +``` + +#### `Nonce` + +The RM specs reference a `Nonce` type which is left undefined. +Let's define it as a some kind of `Nat` for now, as we later need to have a +`Eq` instance for it. + +```juvix +type Nonce := mkNonce@{ + nonce : Nat; +}; +``` + +```juvix +deriving +instance +eqNonce : Eq Nonce; + +deriving +instance +ordNonce : Ord Nonce; +``` + +#### `RandSeed` + +The RM specs reference a `RandSeed` type which is left undefined. + +```juvix +axiom RandSeed : Type; +``` + +### `FixedSize` Trait + +The `FixedSize` trait ensures that certain types have a fixed bit +length, which is essential for resource integrity and security. + +```juvix +trait +type FixedSize A := + mkFixedSize@{ + bitSize : Nat; + }; +``` + +#### `FixedSize` instance for `Nat` + +An instance of `FixedSize` for natural numbers with a bit size of 256. + +```juvix +instance +fixedSizeNat256 : FixedSize Nat := + mkFixedSize@{ + bitSize := 256 + }; +``` + +#### `FixedSize` instance for `ByteString` + +An instance of `FixedSize` for bytestrings with a bit size of 256. + +```juvix +instance +fixedSizeByteString256 : FixedSize ByteString := + mkFixedSize@{ + bitSize := 256 + }; +``` + +#### `FixedSize` instance for `Nonce` + +An instance of `FixedSize` for nonces with a bit size of 256. + +```juvix +instance +fixedSizeNonce256 : FixedSize Nonce := + mkFixedSize@{ + bitSize := 256 + }; +``` + +#### `FixedSize` instance for `RandSeed` + +An instance of `FixedSize` for random seeds with a bit size of 256. + +```juvix +instance +fixedSizeRandSeed256 : FixedSize RandSeed := + mkFixedSize@{ + bitSize := 256 + }; +``` + +### `Arithmetic` Trait + +The `Arithmetic` trait defines addition and subtraction operations. It requires +a `FixedSize` instance. + +```juvix +trait +type Arithmetic A := + mkArithmetic@{ + {{fixedSize}} : FixedSize A; + add : A -> A -> A; + sub : A -> A -> A; + }; +``` + +#### `Arithmetic` instance for `Nat` + +An instance of `Arithmetic` for natural numbers. + +```juvix +instance +arithmeticNat : Arithmetic Nat := + mkArithmetic@{ + add := \{x y := x + y}; + sub := sub + }; +``` + +### `Hash` Trait + +The `Hash` trait provides a standardized interface for hashing +operations within the RM. It implies `FixedSize` as we will always +assume that's present when using a `Hash` instance. + +```juvix +trait +type Hash H := + mkHash@{ + {{fixedSize}} : FixedSize H; + hash : H -> Digest; + }; +``` + +#### `Hash` instance for `Nat` + +Assuming `Nat` can be directly hashed, we provide an instance of `Hash` for it. + +```juvix +axiom computeNatHash : Nat -> Digest; +``` + +```juvix +instance +hashNat : Hash Nat := + mkHash@{ + fixedSize := fixedSizeNat256; + hash := computeNatHash + }; +``` + +#### `Hash` instance for `ByteString` + +Assuming `ByteString` can be directly hashed, we provide an instance of `Hash` for it. + +```juvix +axiom computeByteStringHash : ByteString -> Digest; +``` + +```juvix +instance +hashByteString : Hash ByteString := + mkHash@{ + fixedSize := fixedSizeByteString256; + hash := computeByteStringHash + }; +``` + +### `ISet` Trait + +The `ISet` trait defines the essential operations for set manipulation, +defining a standard interface for any `Set` implementation used by the RM. +The type parameter `S` is the set type, and `A` is the element type. + +```juvix +trait +type ISet S A := + mkISet@{ + newSet : S; + size : S -> Nat; + insert : A -> S -> S; + union : S -> S -> S; + intersection : S -> S -> S; + difference : S -> S -> S; + contains : A -> S -> Bool; + }; +``` + +#### `ISet` instance for Prelude's `Set` + +An instance of `ISet` for the standard `Set` type. + +```juvix +instance +iSetForStdSet + {A} {{Ord A}} : ISet (Set A) A := + mkISet@{ + newSet := Set.empty; + size := Set.size; + insert := Set.insert; + union := Set.union; + intersection := Set.intersection; + difference := Set.difference; + contains := Set.isMember + }; +``` + +### `IOrderedSet` Trait + +`IOrderedSet` is intended to represent a list without repeated elements; +that is, a set equipped with a permutation. The interface is left mostly +unspecified. Details are not given in the original RM specs, so this is +a speculative interface. + +```juvix +trait +type IOrderedSet S A := + mkIOrderedSet@{ + {{iset}} : ISet S A; + -- Returns elements in order as a list + toList : S -> List A; + -- Creates from a list, preserving order of first occurrence + fromList : List A -> S; + }; +``` + +### `OrderedSet` + +An ordered set as a regular set plus a list of indices defining the permutation. + +```juvix +type OrderedSet A := mkOrderedSet { + elements : Set A; + permutation : List Nat -- List of indices +}; +``` + +#### `setToListWithPerm` + +```juvix +setToListWithPerm + {A} {{Ord A}} + (indices : List Nat) + (elements : Set.Set A) : List A := + let + -- First convert set to sorted list + sorted : List A := Set.toList elements; + -- Then map each index to the element at that position + access (index : Nat) : Option A := + case splitAt index sorted of { + | (mkPair _ (x :: _)) := some x + | (mkPair _ _) := none + } + in catOptions (map access indices); +``` + +#### `orderedSetToList` + +```juvix +orderedSetToList + {A} {{Ord A}} + (s : OrderedSet A) : List A := + setToListWithPerm (OrderedSet.permutation s) (OrderedSet.elements s); +``` + +#### `findPosition` + +Find position where `x` would go in sorted order + +```juvix +findPosition + {A} {{Ord A}} + (x : A) (elements : Set.Set A) : Nat := + let + sorted : List A := Set.toList elements; + go : List A -> Nat + | [] := 0 + | (y :: ys) := + if | (x <= y) := 0 + | else := suc (go ys); + in go sorted; +``` + +#### `orderedSetFromList` + +```juvix +orderedSetFromList + {A} {{Ord A}} : List A -> OrderedSet A := + foldl + (\{acc x := + if | (Set.isMember x (OrderedSet.elements acc)) := acc + | else := let pos := findPosition x (OrderedSet.elements acc) + in mkOrderedSet + (Set.insert x (OrderedSet.elements acc)) + ((OrderedSet.permutation acc) ++ [pos])}) + (mkOrderedSet Set.empty []); +``` + +#### `IOrderedSet` instance for `OrderedSet` + +```juvix +instance +orderedSetInstance + {A} {{Ord A}} : IOrderedSet (OrderedSet A) A := + mkIOrderedSet@{ + -- ISet instance + iset := mkISet@{ + newSet := mkOrderedSet Set.empty []; + size := \{s := Set.size (OrderedSet.elements s)}; + insert := \{x s := + if | (Set.isMember x (OrderedSet.elements s)) := s + | else := mkOrderedSet + (Set.insert x (OrderedSet.elements s)) + ((OrderedSet.permutation s) ++ [Set.size (OrderedSet.elements s)]) + }; + -- Union + union := \{s1 s2 := orderedSetFromList (orderedSetToList s1 ++ + orderedSetToList s2)}; + + -- Intersection + intersection := \{s1 s2 := + orderedSetFromList (filter (\{x := Set.isMember x (OrderedSet.elements s2)}) (orderedSetToList s1)) + }; + + -- Difference + difference := \{s1 s2 := + orderedSetFromList (filter (\{x := not (Set.isMember x (OrderedSet.elements s2))}) (orderedSetToList s1)) + }; + + -- Contains + contains := \{x s := Set.isMember x (OrderedSet.elements s)} + }; + + -- toList + toList := orderedSetToList; + + -- fromList + fromList := orderedSetFromList; + }; +``` + +### `IMap` Trait + +The `IMap` trait defines the standard operations for map manipulation, +defining a standard interface for any Map implementation used by the RM. + +```juvix +trait +type IMap M K V := + mkIMap@{ + emptyMap : M; + insert : K -> V -> M -> M; + lookup : K -> M -> Option V; + delete : K -> M -> M; + keys : M -> List K; + values : M -> List V; + }; +``` + +#### `IMap` instance for Prelude's `Map` + +An instance of `IMap` for the standard `Map` type. + +```juvix +instance +iMapForStdMap + {K} {{Ord K}} {V : Type} : IMap (Map K V) K V := + mkIMap@{ + emptyMap := Map.empty; + insert := \{k v m := Map.insert k v m}; + lookup := \{k m := Map.lookup k m}; + delete := \{k m := Map.delete k m}; + keys := \{m := Map.keys m}; + values := \{m := Map.values m} + }; +``` diff --git a/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_delta.juvix.md b/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_delta.juvix.md index 559f519ab70..5969bb8da9e 100644 --- a/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_delta.juvix.md +++ b/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_delta.juvix.md @@ -7,6 +7,8 @@ search: ```juvix module arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_delta; +import prelude open; +import arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_types open; ``` # Delta Proving System @@ -21,6 +23,21 @@ Delta proving system is used to prove that the transaction delta is equal to a c The aggregation function allows to aggregate proofs in a way that if $\pi_1$ proves that the first transaction's balance is $b_1$ and the second proof $\pi_2$ proves the second transaction's balance is $b_2$, then the proof $Aggregate(\pi_1, \pi_2)$ proves that the composed transaction's balance is $b_1 + b_2$. +```juvix +trait +type DeltaProvingSystem (Statement Proof Instance Witness ProvingKey VerifyingKey : Type) := mkDeltaProvingSystem@{ + provingSystem : ProvingSystem Statement Proof Instance Witness ProvingKey VerifyingKey; + aggregate : Proof -> Proof; + }; +``` + +??? note "Coercion to parent `provingSystemOf`" + + ```juvix + coercion instance + provingSystemOf {S P I W PK VK} {{dps : DeltaProvingSystem S P I W PK VK}} : ProvingSystem S P I W PK VK := + DeltaProvingSystem.provingSystem {{dps}}; + ``` ```mermaid --- @@ -43,4 +60,4 @@ classDiagram class DeltaProvingSystem -``` \ No newline at end of file +``` diff --git a/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_types.juvix.md b/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_types.juvix.md index 52ac42f0844..ea57fb8b900 100644 --- a/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_types.juvix.md +++ b/docs/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_types.juvix.md @@ -7,6 +7,7 @@ search: ```juvix module arch.system.state.resource_machine.primitive_interfaces.proving_system.proving_system_types; +import prelude open; ``` # Proving system definition @@ -14,21 +15,114 @@ module arch.system.state.resource_machine.primitive_interfaces.proving_system.pr We define a set of structures required to define a proving system $PS$ as follows: -- Proof $\pi: PS.Proof$ - proves that a specific statement `f` with the inputs `x` and `w` evaluates to `True`. +- Proof $\pi: PS.Proof$ - $\pi$ is a proof that a specific statement `f` with the inputs `x` and `w` evaluates to `True`. - Instance $x: PS.Instance$ is the ordered input data structure used to produce and verify a proof. - Witness $w: PS.Witness$ is the ordered input data structure used to produce (but not verify) a proof. - Proving key $pk: PS.ProvingKey$ contains the data required to produce a proof for a pair $(x, w)$. Specific to a particular statement (different statements `f` and `f'` imply different proving keys) being proven, but doesn't depend on the inputs. - Verifying key $vk: PS.VerifyingKey$ contains the data required, along with the instance $x$, to verify a proof $\pi$. Specific to a particular statement being proven (different statements `f` and `f'` imply different verifying keys), but doesn't depend on the inputs. +Besides a paramter `Statement` +(that is left underspecified for the time being), +we have a trait with the required structures for each of the "sorts". + -A proving system $PS$ consists of a pair of algorithms, $(Prove, Verify)$: +```juvix +trait +type ProvingSystemStructure + (Statement Proof Instance Witness ProvingKey VerifyingKey : Type) := + mkProvingSystemStructure@{ + proofEq : Eq Proof; + instanceOrd : Ord Instance; + witnessOrd : Ord Witness; + pkEq : Eq ProvingKey; + vkEq : Eq VerifyingKey; + encode : Statement -> ProvingKey; + functionalize : Statement -> Instance -> Witness -> Bool; + } +; +``` + +??? info "Coercions to the enclosed traits" + + ```juvix + coercion instance + proofEqOf {S P I W PK VK} {{ p : ProvingSystemStructure S P I W PK VK}} : Eq P := + ProvingSystemStructure.proofEq {{p}}; + + coercion instance + instanceOrdOf {S P I W PK VK} {{ p : ProvingSystemStructure S P I W PK VK}} : Ord I := + ProvingSystemStructure.instanceOrd {{p}}; + + coercion instance + witnessOrdOf {S P I W PK VK} {{ p : ProvingSystemStructure S P I W PK VK}} : Ord W := + ProvingSystemStructure.witnessOrd {{p}}; + + coercion instance + pkEqOf {S P I W PK VK} {{ p : ProvingSystemStructure S P I W PK VK}} : Eq PK := + ProvingSystemStructure.pkEq {{p}}; + + coercion instance + vkEqOf {S P I W PK VK} {{ p : ProvingSystemStructure S P I W PK VK}} : Eq VK := + ProvingSystemStructure.vkEq {{p}}; + ``` + +!!! todo "injectivity" + + `encode` should be injective + +!!! todo "instances : ordered input data structure" + + What does it mean for (the type of) instances to be ordered? + Is it really just the ordering on terms of the type as per `Ord`? + +!!! todo "witnesses : ordered input data structure" + + What does it mean for (the type of) witnesses to be ordered? + Is it really just the ordering on terms of the type as per `Ord`? + +A _proving system $PS$_ consists of a pair of algorithms, $(Prove, Verify)$: - $Prove(pk, x, w): PS.ProvingKey \times PS.Instance \times PS.Witness \rightarrow PS.Proof$ - $Verify(vk, x, \pi): PS.VerifyingKey \times PS.Instance \times PS.Proof \rightarrow Bool$. +Thus, the trait of a proving system has two methods besides +the relevant proving system structure. + +```juvix +trait +type ProvingSystem + (Statement Proof Instance Witness ProvingKey VerifyingKey : Type) := + mkProvingSystem@{ + structure : ProvingSystemStructure Statement Proof Instance Witness ProvingKey VerifyingKey; + prove : ProvingKey -> Instance -> Witness -> Proof; + verify : VerifyingKey -> Instance -> Proof -> Bool; + } +; +``` + +??? info "Coercion to the parent trait" + + ```juvix + coercion instance + structureOf {S P I W PK VK} {{ps : ProvingSystem S P I W PK VK}} : ProvingSystemStructure S P I W PK VK := + ProvingSystem.structure {{ps}}; + ``` + !!! note To verify a proof created for instance `x`, the same instance `x` must be used. For instances that contain elements of the same type, the order of the elements must be preserved. +!!! todo "clarify the note" + + What does the sentence + "For instances that contain elements of the same type, + the order of the elements must be preserved." + mean? + +!!! todo "add «axioms» to the signature" + + Ideally, we want to add the "axiom" + $verify(vk, y, prove(pk, x, w)) = true \Rightarrow x = y$. + ### Properties A proving system must have the following properties: @@ -38,9 +132,23 @@ A proving system must have the following properties: For a statement `f`, `Verify(vk, x, proof) = True` implies that `f x w = True` and `Verify(vk, x, proof) = False` implies that `f x w = False`. +!!! todo "completeness" + + How to express that for all terms $f$ of type Statement such that $f x w = True$, + there exists a witness $w$, an instance $x$ (...) + such that $Verify(vk, x, prove(pk, x, w))$⁈ + So, + the type `Statement` is + a (very special) subtype of $Instance \to Witness \to Bool$. + +!!! todo "soundness" + + So, if we encode a statement `f: Statement`, + and a proof for its encoding as , using + Certain proving systems may also be **zero-knowledge**, meaning that the produced proofs reveal no information other than their own validity. -A proof $\pi$ for which $Verify(pr) = True$ is considered valid. +A proof $\pi$ for which $Verify(pi) = True$ is considered _valid_. ### Common proving scheme types @@ -71,4 +179,4 @@ Assuming the proving system is used to verify that a predicate evaluated on its In practice, the predicate and its arguments can be represented as a hash or commitment to the actual value. In the trivial scheme, they would have to be opened in order to verify them. In the trusted delegation case, they *don't have to* be opened if the signature is produced over the hashed values. !!! note - For application developers: writing applications that can work with all types of systems can be challenging since different proof types require different argument split between instance and witness (e.g., trivial scheme, unlike succinct PoK, expects no witness). The current solution is to write applications with succinct PoK types of proving systems in mind, which then can be translated to other proving systems by moving witness arguments to instance. \ No newline at end of file + For application developers: writing applications that can work with all types of systems can be challenging since different proof types require different argument split between instance and witness (e.g., trivial scheme, unlike succinct PoK, expects no witness). The current solution is to write applications with succinct PoK types of proving systems in mind, which then can be translated to other proving systems by moving witness arguments to instance. diff --git a/docs/arch/system/types.juvix.md b/docs/arch/system/types.juvix.md new file mode 100644 index 00000000000..7aa3f8302ed --- /dev/null +++ b/docs/arch/system/types.juvix.md @@ -0,0 +1,34 @@ +--- +icon: material/pillar +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types; + ``` + +# Basic types in the system + +## Specific prelude for the RM + +```juvix +import arch.system.state.resource_machine.prelude; +``` + +## Types in the RM + +```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/arch/system/types/action.juvix.md b/docs/arch/system/types/action.juvix.md new file mode 100644 index 00000000000..6e61f3d1783 --- /dev/null +++ b/docs/arch/system/types/action.juvix.md @@ -0,0 +1,209 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - action + - transaction + - resource-machine +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.action; + import prelude open; + import arch.system.types.nullifier open; + import arch.system.types.commitment open; + ``` + +# Actions + +An *action* is a term of type `Action` that represent *atomic transactions* or +*state changes*. + +## Purpose + +Actions are atomic units of [[State|state]] change within a +[[Transaction|transaction]]. They serve the following main purposes. + +1. **State Change Organization**: Actions partition a transaction's overall +state change into smaller, focused units. Each action clearly specifies which +resources are being created and consumed by the associated [[Transaction|transaction]]. + +2. **Proof Context Isolation**: Actions provide an isolated context for +[[Resource logic proof|resource logic proofs]]. When evaluating proofs for a +resource, only the resources associated with that action are accessible. This +isolation helps manage complexity and ensures proper resource handling. + +### Resource Association + +We also need to discuss how resources are associated with actions. + +A resource can be associated with an action in two ways: + +- Through its corresponding [[Commitment|commitment]] in the action's `created` +field, indicating it is being created + +- Through its corresponding [[Nullifier|nullifier]] in the action's `consumed` +field, indicating it is being consumed + +Important properties of this resource association: + +- Resources listed in `consumed` are considered "consumed in the action". +- Resources listed in `created` are considered "created in the action". +- Each resource is associated with exactly one action in case it is created or +consumed in the action. + +Now we can define the `Action` type. + +## `Action` + +A *transaction action* or simply *action* is a term of type `Action`. + +```juvix +type Action A := mkAction { + created : Set (Commitment A); + consumed : Set Nullifier; + -- resourceLogicProofs : Map Tag (LogicRefHash, PS.Proof); + -- complianceUnits : Set ComplianceUnit; + -- applicationData : Map Tag (BitString, DeletionCriterion); +}; +``` + +???+ quote "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. + +??? quote "Auxiliary Juvix code: Instances" + + ```juvix + deriving + instance + eqAction {A} {{Eq A}}: Eq (Action A); + ``` + + ```juvix + deriving + instance + ordAction {A} {{Ord A}}: Ord (Action A); + ``` + + +## Properties + +### A resource can only be associated with one action when being consumed or +created + +### Actions must provide proofs for all *resource transitions* + + \ No newline at end of file diff --git a/docs/arch/system/types/commitment.juvix.md b/docs/arch/system/types/commitment.juvix.md new file mode 100644 index 00000000000..479e76ee193 --- /dev/null +++ b/docs/arch/system/types/commitment.juvix.md @@ -0,0 +1,75 @@ +--- +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 + +## Purpose + +Commitments prove the existence of a value without revealing it. In the resource +machine, they prove the existence of resources. Commitments are stored in the +resource machine's state within a [[CommitmentTree|commitment tree]] for +querying. + +## `Commitment` + +```juvix +type Commitment A := mkCommitment@{ + committed : A; + commitment : Digest; +}; +``` + +???+ quote "Arguments" + + `committed` + : The value that is committed to. + + `commitment` + : The hash of the value. + +???+ quote "Auxiliary Juvix code: Instances" + + ```juvix + deriving + instance + CommitmentEq {A} {{Eq A}} : Eq (Commitment A); + ``` + + ```juvix + deriving + instance + CommitmentOrd {A} {{Ord A}} : Ord (Commitment A); + ``` + +### `makeCommitment` + +```juvix +makeCommitment {A} (a : A) : Commitment A := + mkCommitment@{ + committed := a; + commitment := hash a; + }; +``` + + +## Properties + +!!! todo + + Add properties of the commitment. + diff --git a/docs/arch/system/types/commitmenttree.juvix.md b/docs/arch/system/types/commitmenttree.juvix.md new file mode 100644 index 00000000000..e1427ee3859 --- /dev/null +++ b/docs/arch/system/types/commitmenttree.juvix.md @@ -0,0 +1,166 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - commitment-tree + - merkle-tree + - cryptographic-accumulator + - 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 + +## Purpose + +Commitment trees are a tree-like data structure that stores [[Commitment|commitments]] and +provide a way to efficiently store, retrieve those commitments, and verify +their inclusion in the tree. + +Commitment trees are part of the [[State|state]] in the system. + +## `CommitmentTreeOps` + +The `CommitmentTreeOps` trait defines the stateless operations that a tree that +stores commitments must implement. + +The `CommitmentTreeOps` type has the following type parameters: + +- `A` : The type of the data that is being committed. +- `Tree` : The type of the tree that stores the commitments. +- `P` : The type of the path that is used to navigate through the tree. + +```juvix +trait +type CommitmentTreeOps A (Tree : Type -> Type) P := + mkCommitmentTreeOps@{ + hashRoot : Tree A -> Digest; + add : A -> Tree A -> Pair (Tree A) P; + read : P -> Tree A -> Option (Commitment A); + verify : P -> Commitment A -> Tree A -> Bool; + }; +``` + +???+ quote "`CommitmentTreeOps` operations" + + `hashRoot` + : Returns the hash of the root of the given commitment tree. + + `add` : Adds a commitment to the commitment tree. Returns the new + commitment tree and the path to the commitment. + + `read` + : Returns the commitment at a `Path` in the commitment tree. + + `verify` + : Verifies if a commitment is at a `Path` in the commitment tree. + +## An instance of `CommitmentTreeOps` + +We now define an instance of a `CommitmentTreeOps` for the `CTree` type. +Trees of this type can be used as *default* cryptographic accumulators. + +The `CTree` type is defined as a specialised `MTree`, a general type of tree +that can be used as a cryptographic accumulator. + +### `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` + +Trees of type `CTree` are 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. + +```juvix +CTree (A : Type) : Type := MTree (Commitment A) Digest; +``` + +Let us now define the `treeHash` function which computes the hash of a `CTree`. + +```juvix +treeHash {A} (tree : CTree A) : Digest := + case tree of { + | (mkMTreeLeaf@{ value := c }) := TODO -- Commitment.commitment c + | (mkMTreeNode@{ merge := digest}) := digest + } +``` + +To retrieve commitments from a `CTree`, we need to define a *path* which is a +sequence of directions used to navigate through the tree. + +### `PathDir` + +A *path* is a sequence of `PathDir` values used to navigate through a tree such +as a `CTree` by specifying the direction to take at each node. + +```juvix +type PathDir := + | PathDirLeft + | PathDirRight +``` + +### `CTreePath` + +A `CTreePath` is a sequence of `PathDir` values used to navigate through a `CTree`. + +```juvix +CTreePath : Type := List PathDir; +``` + +### `CommitmentTree` + +```juvix +CommitmentTree (A : Type) : Type := CommitmentTreeOps A CTree PathDir; +``` + + \ No newline at end of file diff --git a/docs/arch/system/types/nullifier.juvix.md b/docs/arch/system/types/nullifier.juvix.md new file mode 100644 index 00000000000..2bdbbc9ed1f --- /dev/null +++ b/docs/arch/system/types/nullifier.juvix.md @@ -0,0 +1,74 @@ +--- +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..f44dd51a73a --- /dev/null +++ b/docs/arch/system/types/nullifier_properties.juvix.md @@ -0,0 +1,71 @@ +--- +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; + ``` + +!!! 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 + +```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..8e179acb41b --- /dev/null +++ b/docs/arch/system/types/nullifierkey.juvix.md @@ -0,0 +1,58 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - nullifier + - resource-machine + - crypto +--- + +??? 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`, 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` + +```juvix +type NullifierKey := mkNullifierKey { + key : Digest; --TODO: What type I need to put here. Hash? +}; +``` + +???+ 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. diff --git a/docs/arch/system/types/resource.juvix.md b/docs/arch/system/types/resource.juvix.md new file mode 100644 index 00000000000..8721381a776 --- /dev/null +++ b/docs/arch/system/types/resource.juvix.md @@ -0,0 +1,97 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.resource; + import prelude open; + import arch.system.types.nullifierkey open; + import arch.system.state.resource_machine.prelude open; + ``` + +# Resource + +A **resource** is of type `Resource`. + +## `Resource` + +```juvix +type Resource := mkResource { + logicRef : LogicHash; + labelRef : LabelHash; + valueRef : ValueHash; + quantity : Nat; + isEphemeral : Bool; + nonce : Nonce; + nullifierKey : NullifierKey; + randSeed : Nat; +}; +``` + +??? 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 + derive the resource nullifier (nullifiers are further described [[Nullifier|here]]) + + `randSeed` + : randomness seed used to derive whatever randomness needed + + +??? quote "Auxiliary Juvix code" + + ```juvix + deriving + instance + ResourceEq : Eq Resource; + ``` + + ```juvix + deriving + 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 new file mode 100644 index 00000000000..530c7ff4641 --- /dev/null +++ b/docs/arch/system/types/resource_logic_proof.juvix.md @@ -0,0 +1,96 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - resource-logic-proof + - resource-machine + - security + - proof +--- + +??? 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. + + 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..4fca667fe22 --- /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.types.transaction open; + ``` + +# Resource Machines + +A **resource machine** is a term of type `ResourceMachine`. + +## `ResourceMachine` + +```juvix +trait +type ResourceMachine A := mkResourceMachine { + createTransaction : + -- CMTreeRoots : Set CMtree.Value; + -- actions : Set Action; + -- deltaProof : DeltaProvingSystem.Proof; + Unit -> Transaction A; -- which is the mkTransaction function + composeTransactions : Transaction A -> Transaction A -> Transaction A; + verifyTransaction : Transaction A -> 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. diff --git a/docs/arch/system/types/state.juvix.md b/docs/arch/system/types/state.juvix.md new file mode 100644 index 00000000000..d381b586c61 --- /dev/null +++ b/docs/arch/system/types/state.juvix.md @@ -0,0 +1,86 @@ + +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - state +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.state; + import prelude open; + import arch.system.types.nullifier open; + import arch.system.types.commitmenttree open; + ``` + +# State + +???+ quote "Auxiliary Juvix code" + + ```juvix + axiom CommitmentAccumulator : Type; + ``` + + ```juvix + axiom DataBlobStorage : Type; + + axiom EqDataBlobStoragea : Eq DataBlobStorage; + instance EqDataBlobStorage : Eq DataBlobStorage := EqDataBlobStoragea; + + axiom OrdDataBlobStoragea : Ord DataBlobStorage; + instance OrdDataBlobStorage : Ord DataBlobStorage := OrdDataBlobStoragea; + ``` + +```juvix +type State := mkState { + -- commitmentAccumulator {A : Type} {{CommitmentTreeOps A CTree CTreePath}} : A ; + -- secondCommitmentAccumulator : CommitmentAccumulator; + nullifierSet : Set Nullifier; + dataBlobStorage : DataBlobStorage; + -- hierarchicalIndex : HierarchicalIndex; +}; +``` + +??? 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; + ``` + diff --git a/docs/arch/system/types/tag.juvix.md b/docs/arch/system/types/tag.juvix.md new file mode 100644 index 00000000000..d3ba963df59 --- /dev/null +++ b/docs/arch/system/types/tag.juvix.md @@ -0,0 +1,32 @@ + +--- +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 open; + import arch.system.types.nullifier open; + ``` + +# Tags + +A **tag** is a term of type `Tag`. + +## `Tag` + +```juvix +type Tag A := + | TagCommitment (Commitment A) + | TagNullifier Nullifier + ; +``` + diff --git a/docs/arch/system/types/test.agda b/docs/arch/system/types/test.agda new file mode 100644 index 00000000000..ddfc6c816ee --- /dev/null +++ b/docs/arch/system/types/test.agda @@ -0,0 +1,44 @@ +module Test where + +postulate + Digest : Set + hash : {A : Set} -> A -> Digest + Option : Set -> Set + Path : Set + Pair : Set -> Set -> Set + Bool : Set + undef : {A : Set} -> A + + +record Commitment (A : Set) : Set where + field + committed : A + commitment : Digest + + +record CommitmentTree (A : Set) (Tree : Set -> Set) : Set where + field + hashRoot : Tree A -> Digest + add : A -> Tree A -> Pair (Tree A) Path + read : Path -> Tree A -> Option (Commitment A) + verify : Path -> Commitment A -> Tree A -> Bool + +data MTree (A B : Set) : Set where + mkMTreeLeaf : (value : A) -> MTree A B + mkMTreeNode : (merge : B) -> (left : MTree A B) -> (right : MTree A B) -> MTree A B + +CTree : Set -> Set +CTree A = MTree (Commitment A) Digest + + +thisShouldWork : {A : Set} -> CommitmentTree A CTree +CommitmentTree.hashRoot (thisShouldWork {A}) = treeHash + where + treeHash : {A : Set} -> CTree A -> Digest + treeHash (mkMTreeLeaf + record { committed = committed ; commitment = commitment }) = commitment + treeHash (mkMTreeNode merge left right) = merge +CommitmentTree.add (thisShouldWork {A}) = undef +CommitmentTree.read (thisShouldWork {A}) = undef +CommitmentTree.verify (thisShouldWork {A}) = undef + diff --git a/docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md b/docs/arch/system/types/transaction.juvix.md similarity index 54% rename from docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md rename to docs/arch/system/types/transaction.juvix.md index 3e69ab5e189..af0d0e63fe8 100644 --- a/docs/arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md +++ b/docs/arch/system/types/transaction.juvix.md @@ -5,24 +5,73 @@ search: 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 -module arch.system.state.resource_machine.data_structures.transaction.transaction; +type Transaction A := mkTransaction { + actions : Set (Action A); + -- CMTreeRoots : Set CMtree.Value; + -- deltaProof : DeltaProvingSystem.Proof; +}; ``` -# Transaction +???+ 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" -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: + ```juvix + deriving + instance + eqTrans {A} {{Eq A}} : Eq (Transaction A); + ``` -|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| + ```juvix + deriving + instance + ordTrans {A} {{Ord A}} : Ord (Transaction A); + ``` + +## Purpose + +!!! todo + + Explain the purpose of transactions. + +## Properties + +!!! todo + + Explain the properties of transactions. + + \ No newline at end of file diff --git a/docs/everything.juvix.md b/docs/everything.juvix.md index 4138ce68bf4..8402bcb191f 100644 --- a/docs/everything.juvix.md +++ b/docs/everything.juvix.md @@ -5,7 +5,6 @@ search: boost: 2 tags: - index - - juvix --- @@ -13,24 +12,23 @@ tags: ```juvix module everything; -``` -## Prelude +{- Prelude -} -```juvix import prelude; +import anomian; ``` -## Anomian +## System ```juvix -import anomian; +import arch.system.identity.identity; ``` -## System +### Resource Machine ```juvix -import arch.system.identity.identity; +{- Types -} ``` ### Resource Machine @@ -73,6 +71,58 @@ 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.state.resource_machine.prelude; + +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.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 + ```juvix import arch.node.types; @@ -97,31 +147,19 @@ import arch.node.types.router; ## Engines -### Identity - -### Commitment - ```juvix import arch.node.engines.commitment_messages; import arch.node.engines.commitment_config; import arch.node.engines.commitment_environment; import arch.node.engines.commitment_behaviour; import arch.node.engines.commitment; -``` -### Decryption - -```juvix import arch.node.engines.decryption_messages; import arch.node.engines.decryption_config; import arch.node.engines.decryption_environment; import arch.node.engines.decryption_behaviour; import arch.node.engines.decryption; -``` -### Encryption - -```juvix import arch.node.engines.encryption_messages; import arch.node.engines.encryption_config; import arch.node.engines.encryption_environment; diff --git a/docs/prelude.juvix.md b/docs/prelude.juvix.md index cc71f82ab7f..4b4670b36a6 100644 --- a/docs/prelude.juvix.md +++ b/docs/prelude.juvix.md @@ -14,7 +14,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}; import Stdlib.Data.Fixity open public; ``` @@ -884,6 +884,8 @@ import Stdlib.Data.List as List any; all; zip; + splitAt; + filter; } public; ``` @@ -1079,7 +1081,11 @@ Traversable instance for lists instance traversableListI : Traversable List := mkTraversable@{ - sequence {F : Type -> Type} {A} {{appF : Applicative F}} (xs : List (F A)) : F (List A) := + sequence + {F : Type -> Type} + {A} + {{appF : Applicative F}} + (xs : List (F A)) : F (List A) := let cons : F A -> F (List A) -> F (List A) | x acc := liftA2 (::) x acc; @@ -1089,7 +1095,11 @@ traversableListI : Traversable List := | (x :: xs) := cons x (go xs); in go xs; - traverse {F : Type -> Type} {A B} {{appF : Applicative F}} (f : A -> F B) (xs : List A) : F (List B) := + traverse + {F : Type -> Type} + {A B} + {{appF : Applicative F}} + (f : A -> F B) (xs : List A) : F (List B) := let cons : A -> F (List B) -> F (List B) | x acc := liftA2 (::) (f x) acc; diff --git a/mkdocs.yml b/mkdocs.yml index ae1d6d6a8e1..a3a15128a9e 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -1,9 +1,12 @@ site_name: !ENV [SITE_NAME, "Anoma specs"] +site_name: !ENV [SITE_NAME, "Anoma specs"] site_author: !ENV [SITE_AUTHOR, "Anoma Foundation"] site_description: !ENV [SITE_DESCRIPTION, "The Anoma specs is a collection of documents that describe the architecture, design, and implementation of the Anoma Network."] +site_description: !ENV [SITE_DESCRIPTION, "The Anoma specs is a collection of documents that describe the architecture, design, and implementation of the Anoma Network."] site_dir: !ENV [SITE_DIR, site] site_url: !ENV [SITE_URL, 'https://specs.anoma.net/latest/'] site_version: !ENV [SITE_VERSION, "v0.1.4"] +site_version: !ENV [SITE_VERSION, "v0.1.4"] copyright: !ENV [COPYRIGHT, "© 2025 Anoma Foundation"] repo_url: https://github.com/anoma/nspec repo_name: anoma/nspec @@ -258,6 +261,253 @@ nav: - Run pre commit checks: ./tutorial/commit_checks.md - Updating the changelog: ./tutorial/changelog.md - Versioning: ./tutorial/versioning.md + - Indexes: + - List of tags: ./indexes/tags.md + - List of modules: ./indexes/modules.md + - List of basic types: ./prelude.juvix.md + # - List of engines: ./indexes/engines.md + - Introduction: + - Anomian: ./anomian.juvix.md + - Anoma architecture: ./arch/overview.md + - Node architecture: + - Concepts: + - Engine: ./arch/node/concepts/engine.md + - Subsystem: ./arch/node/concepts/subsystem.md + - Node: ./arch/node/concepts/node.md + - Types: + - Anoma Message: ./arch/node/types/anoma_message.juvix.md + - Anoma Configuration: ./arch/node/types/anoma_config.juvix.md + - Anoma Environment: ./arch/node/types/anoma_environment.juvix.md + - Engine: ./arch/node/types/engine.juvix.md + - Engine Configuration: ./arch/node/types/engine_config.juvix.md + - Engine Environment: ./arch/node/types/engine_environment.juvix.md + - Engine Behaviour: ./arch/node/types/engine_behaviour.juvix.md + - Messages & Mailboxes: ./arch/node/types/messages.juvix.md + - Subsystems: + - Hardware subsystem: + - Hardware subsystem overview: ./arch/node/subsystems/hardware.juvix.md + - Hardware subsystem engines: + - Local Key Value Storage Engine: + - Local Key Value Storage Engine: ./arch/node/engines/local_key_value_storage.juvix.md + - Local Key Value Storage Messages: ./arch/node/engines/local_key_value_storage_messages.juvix.md + - Local Key Value Storage Configuration: ./arch/node/engines/local_key_value_storage_config.juvix.md + - Local Key Value Storage Environment: ./arch/node/engines/local_key_value_storage_environment.juvix.md + - Local Key Value Storage Behaviour: ./arch/node/engines/local_key_value_storage_behaviour.juvix.md + - Local Time Series Storage Engine: + - Local Time Series Storage Engine: ./arch/node/engines/local_time_series_storage.juvix.md + - Local Time Series Storage Messages: ./arch/node/engines/local_time_series_storage_messages.juvix.md + - Local Time Series Storage Configuration: ./arch/node/engines/local_time_series_storage_config.juvix.md + - Local Time Series Storage Environment: ./arch/node/engines/local_time_series_storage_environment.juvix.md + - Local Time Series Storage Behaviour: ./arch/node/engines/local_time_series_storage_behaviour.juvix.md + - Logging Engine: + - Logging Engine: ./arch/node/engines/logging.juvix.md + - Logging Messages: ./arch/node/engines/logging_messages.juvix.md + - Logging Configuration: ./arch/node/engines/logging_config.juvix.md + - Logging Environment: ./arch/node/engines/logging_environment.juvix.md + - Logging Behaviour: ./arch/node/engines/logging_behaviour.juvix.md + - Wall Clock Engine: + - Wall Clock Engine: ./arch/node/engines/wall_clock.juvix.md + - Wall Clock Messages: ./arch/node/engines/wall_clock_messages.juvix.md + - Wall Clock Configuration: ./arch/node/engines/wall_clock_config.juvix.md + - Wall Clock Environment: ./arch/node/engines/wall_clock_environment.juvix.md + - Wall Clock Behaviour: ./arch/node/engines/wall_clock_behaviour.juvix.md + - Identity subsystem: + - Identity subsystem overview: ./arch/node/subsystems/identity.juvix.md + - Identity subsystem engines: + - Identity Management Engine: + - Identity Management Engine: ./arch/node/engines/identity_management.juvix.md + - Identity Management Messages: ./arch/node/engines/identity_management_messages.juvix.md + - Identity Management Configuration: ./arch/node/engines/identity_management_config.juvix.md + - Identity Management Environment: ./arch/node/engines/identity_management_environment.juvix.md + - Identity Management Behaviour: ./arch/node/engines/identity_management_behaviour.juvix.md + - Encryption Engine: + - Encryption Engine: ./arch/node/engines/encryption.juvix.md + - Encryption Messages: ./arch/node/engines/encryption_messages.juvix.md + - Encryption Configuration: ./arch/node/engines/encryption_config.juvix.md + - Encryption Environment: ./arch/node/engines/encryption_environment.juvix.md + - Encryption Behaviour: ./arch/node/engines/encryption_behaviour.juvix.md + - Decryption Engine: + - Decryption Engine: ./arch/node/engines/decryption.juvix.md + - Decryption Messages: ./arch/node/engines/decryption_messages.juvix.md + - Decryption Configuration: ./arch/node/engines/decryption_config.juvix.md + - Decryption Environment: ./arch/node/engines/decryption_environment.juvix.md + - Decryption Behaviour: ./arch/node/engines/decryption_behaviour.juvix.md + - Commitment Engine: + - Commitment Engine: ./arch/node/engines/commitment.juvix.md + - Commitment Messages: ./arch/node/engines/commitment_messages.juvix.md + - Commitment Configuration: ./arch/node/engines/commitment_config.juvix.md + - Commitment Environment: ./arch/node/engines/commitment_environment.juvix.md + - Commitment Behaviour: ./arch/node/engines/commitment_behaviour.juvix.md + - Verification Engine: + - Verification Engine: ./arch/node/engines/verification.juvix.md + - Verification Messages: ./arch/node/engines/verification_messages.juvix.md + - Verification Configuration: ./arch/node/engines/verification_config.juvix.md + - Verification Environment: ./arch/node/engines/verification_environment.juvix.md + - Verification Behaviour: ./arch/node/engines/verification_behaviour.juvix.md + - ReadsFor Engine: + - ReadsFor Engine: ./arch/node/engines/reads_for.juvix.md + - ReadsFor Messages: ./arch/node/engines/reads_for_messages.juvix.md + - ReadsFor Configuration: ./arch/node/engines/reads_for_config.juvix.md + - ReadsFor Environment: ./arch/node/engines/reads_for_environment.juvix.md + - ReadsFor Behaviour: ./arch/node/engines/reads_for_behaviour.juvix.md + - SignsFor Engine: + - SignsFor Engine: ./arch/node/engines/signs_for.juvix.md + - SignsFor Messages: ./arch/node/engines/signs_for_messages.juvix.md + - SignsFor Configuration: ./arch/node/engines/signs_for_config.juvix.md + - SignsFor Environment: ./arch/node/engines/signs_for_environment.juvix.md + - SignsFor Behaviour: ./arch/node/engines/signs_for_behaviour.juvix.md + - Naming Engine: + - Naming Engine: ./arch/node/engines/naming.juvix.md + - Naming Messages: ./arch/node/engines/naming_messages.juvix.md + - Naming Configuration: ./arch/node/engines/naming_config.juvix.md + - Naming Environment: ./arch/node/engines/naming_environment.juvix.md + - Naming Behaviour: ./arch/node/engines/naming_behaviour.juvix.md + - Ordering subsystem: + - Ordering subsystem overview: ./arch/node/subsystems/ordering.juvix.md + - Ordering subsystem engines: + - Mempool layer: + - Mempool Worker Engine: + - Mempool Worker Engine: ./arch/node/engines/mempool_worker.juvix.md + - Mempool Worker Messages: ./arch/node/engines/mempool_worker_messages.juvix.md + - Mempool Worker Configuration: ./arch/node/engines/mempool_worker_config.juvix.md + - Mempool Worker Environment: ./arch/node/engines/mempool_worker_environment.juvix.md + - Mempool Worker Behaviour: ./arch/node/engines/mempool_worker_behaviour.juvix.md + - Execution layer: + - Shard Engine: + - Shard Engine: ./arch/node/engines/shard.juvix.md + - Shard Messages: ./arch/node/engines/shard_messages.juvix.md + - Shard Configuration: ./arch/node/engines/shard_config.juvix.md + - Shard Environment: ./arch/node/engines/shard_environment.juvix.md + - Shard Behaviour: ./arch/node/engines/shard_behaviour.juvix.md + - Executor Engine: + - Executor Engine: ./arch/node/engines/executor.juvix.md + - Executor Messages: ./arch/node/engines/executor_messages.juvix.md + - Executor Configuration: ./arch/node/engines/executor_config.juvix.md + - Executor Environment: ./arch/node/engines/executor_environment.juvix.md + - Executor Behaviour: ./arch/node/engines/executor_behaviour.juvix.md + - Network subsystem: + - Network subsystem overview: ./arch/node/subsystems/net.juvix.md + - Network subsystem engines: + - Network Registry: + - Network Registry Engine: ./arch/node/engines/net_registry.juvix.md + - Network Registry Messages: ./arch/node/engines/net_registry_messages.juvix.md + - Network Registry Configuration: ./arch/node/engines/net_registry_config.juvix.md + - Network Registry Environment: ./arch/node/engines/net_registry_environment.juvix.md + - Network Registry Behaviour: ./arch/node/engines/net_registry_behaviour.juvix.md + - Router: + - Router Engine: ./arch/node/engines/router.juvix.md + - Router Messages: ./arch/node/engines/router_messages.juvix.md + - Router Configuration: ./arch/node/engines/router_config.juvix.md + - Router Environment: ./arch/node/engines/router_environment.juvix.md + - Router Behaviour: ./arch/node/engines/router_behaviour.juvix.md + - Transport Protocol: + - Transport Protocol Engine: ./arch/node/engines/transport_protocol.juvix.md + - Transport Protocol Messages: ./arch/node/engines/transport_protocol_messages.juvix.md + - Transport Protocol Configuration: ./arch/node/engines/transport_protocol_config.juvix.md + - Transport Protocol Environment: ./arch/node/engines/transport_protocol_environment.juvix.md + - Transport Protocol Behaviour: ./arch/node/engines/transport_protocol_behaviour.juvix.md + - Transport Connection: + - Transport Connection Engine: ./arch/node/engines/transport_connection.juvix.md + - Transport Connection Messages: ./arch/node/engines/transport_connection_messages.juvix.md + - Transport Connection Configuration: ./arch/node/engines/transport_connection_config.juvix.md + - Transport Connection Environment: ./arch/node/engines/transport_connection_environment.juvix.md + - Transport Connection Behaviour: ./arch/node/engines/transport_connection_behaviour.juvix.md + - Pub/Sub Topic: + - Pub/Sub Topic Engine: ./arch/node/engines/pub_sub_topic.juvix.md + - Pub/Sub Topic Messages: ./arch/node/engines/pub_sub_topic_messages.juvix.md + - Pub/Sub Topic Configuration: ./arch/node/engines/pub_sub_topic_config.juvix.md + - Pub/Sub Topic Environment: ./arch/node/engines/pub_sub_topic_environment.juvix.md + - Pub/Sub Topic Behaviour: ./arch/node/engines/pub_sub_topic_behaviour.juvix.md + - Storage: + - Storage Engine: ./arch/node/engines/storage.juvix.md + - Storage Messages: ./arch/node/engines/storage_messages.juvix.md + - Storage Configuration: ./arch/node/engines/storage_config.juvix.md + - Storage Environment: ./arch/node/engines/storage_environment.juvix.md + - Storage Behaviour: ./arch/node/engines/storage_behaviour.juvix.md + - System architecture: + - Identity Architecture: + - Identity Architecture Types: ./arch/system/identity/identity.juvix.md + - State Architecture: + - Resource Machine: + - ./arch/system/state/resource_machine/index.juvix.md + - Primitive interfaces: + - ./arch/system/state/resource_machine/primitive_interfaces/index.juvix.md + - Set: + - Set interface: ./arch/system/state/resource_machine/primitive_interfaces/set.juvix.md + - Ordered set: ./arch/system/state/resource_machine/primitive_interfaces/ordered_set.juvix.md + - Map: ./arch/system/state/resource_machine/primitive_interfaces/map.juvix.md + - Fixed size type: + - Interface: ./arch/system/state/resource_machine/primitive_interfaces/fixed_size_type/fixed_size_type.juvix.md + - Arithmetic: ./arch/system/state/resource_machine/primitive_interfaces/fixed_size_type/arithmetic.juvix.md + - Hash: ./arch/system/state/resource_machine/primitive_interfaces/fixed_size_type/hash.juvix.md + - Delta hash: ./arch/system/state/resource_machine/primitive_interfaces/fixed_size_type/delta_hash.juvix.md + - Proving system: + - ./arch/system/state/resource_machine/primitive_interfaces/proving_system/index.md + - Definitions: ./arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_types.juvix.md + - Delta proving system: ./arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_delta.juvix.md + - Commitment accumulator: ./arch/system/state/resource_machine/primitive_interfaces/commitment_accumulator.juvix.md + - Nullifier set: ./arch/system/state/resource_machine/primitive_interfaces/nullifier_set.juvix.md + - Data structures: + - ./arch/system/state/resource_machine/data_structures/index.juvix.md + - Resource: + - ./arch/system/state/resource_machine/data_structures/resource/index.juvix.md + - 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 + - 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: + - Compliance unit: ./arch/system/state/resource_machine/data_structures/compliance_unit/compliance_unit.juvix.md + - Compliance proof: ./arch/system/state/resource_machine/data_structures/compliance_unit/compliance_proof.juvix.md + - Action: + - Action: ./arch/system/state/resource_machine/data_structures/action/index.juvix.md + - Resource logic proof: ./arch/system/state/resource_machine/data_structures/action/resource_logic_proof.juvix.md + - Transaction: + - Transaction: ./arch/system/state/resource_machine/data_structures/transaction/transaction.juvix.md + - Delta proof: ./arch/system/state/resource_machine/data_structures/transaction/delta_proof.juvix.md + - Transaction Function: ./arch/system/state/resource_machine/data_structures/transaction/transaction_function.juvix.md + - Transaction With Payment: ./arch/system/state/resource_machine/data_structures/transaction/transaction_with_payment.juvix.md + - Execution flow: ./arch/system/state/resource_machine/execution_flow/flow.juvix.md + - Notes: + - Roles and requirements: ./arch/system/state/resource_machine/notes/roles_and_requirements.juvix.md + - Stored data format: ./arch/system/state/resource_machine/notes/storage.juvix.md + - Function formats: + - Transaction function format: ./arch/system/state/resource_machine/notes/function_formats/transaction_function_format.juvix.md + - Applications: ./arch/system/state/resource_machine/notes/applications.juvix.md + - Tutorials: + - Contributor guidelines: + - Global principles and guidelines: ./tutorial/principles_and_guidelines.md + - Prepare working environment: ./tutorial/install/index.md + - Engines in Anoma: + - ./tutorial/engines/index.md + - Engine writing conventions: ./tutorial/engines/writing_conventions.md + - Examples: + - Template Engine: + - Template Engine: ./tutorial/engines/template.juvix.md + - Template Messages: ./tutorial/engines/template_messages.juvix.md + - Template Configuration: ./tutorial/engines/template_config.juvix.md + - Template Environment: ./tutorial/engines/template_environment.juvix.md + - Template Behaviour: ./tutorial/engines/template_behaviour.juvix.md + - Ticker Engine: + - Ticker Engine: ./arch/node/engines/ticker.juvix.md + - Ticker Messages: ./arch/node/engines/ticker_messages.juvix.md + - Ticker Configuration: ./arch/node/engines/ticker_config.juvix.md + - Ticker Environment: ./arch/node/engines/ticker_environment.juvix.md + - Ticker Behaviour: ./arch/node/engines/ticker_behaviour.juvix.md + - Add Juvix code for specification: ./tutorial/juvix.md + - Write Markdown: ./tutorial/md/index.md + - Headers and other Markdown formatting conventions: ./tutorial/md/headers_and_other_conventions.md + - Use Wiki style links: ./tutorial/md/links.md + - Include images in Markdown: ./tutorial/md/images.md + - Include code snippets: ./tutorial/md/snippets.md + - Add pending tasks with Todos admonition: ./tutorial/md/todos.md + - Add literature references: ./tutorial/md/citations.md + - Use Git and GitHub: ./tutorial/branch.md + - File naming conventions: ./tutorial/file_naming.md + - Run pre commit checks: ./tutorial/commit_checks.md + - Updating the changelog: ./tutorial/changelog.md + - Versioning: ./tutorial/versioning.md extra: social: - icon: fontawesome/brands/x-twitter @@ -326,16 +576,25 @@ theme: # - navigation.instant.prefetch # - navigation.instant.progress - navigation.instant.preview + - navigation.instant.preview - navigation.tracking # - navigation.expand - navigation.prune + - navigation.prune - navigation.indexes - navigation.sections + - navigation.sections - navigation.footer - navigation.path - toc.follow # - toc.integrate plugins: + - search: + lang: en + pipeline: + - stemmer + - stopWordFilter + - trimmer - search: lang: en pipeline: