Add most of the types for RM specs

docs/arch/node/engines/mempool_worker_behaviour.juvix.md

@@ -43,7 +43,7 @@ A mempool worker acts as a transaction coordinator, receiving transaction reques
 
     ```juvix
     axiom sign : TxFingerprint -> TransactionCandidate -> Signature;
-    axiom hash : TxFingerprint -> TransactionCandidate -> Hash;
+    axiom TChash : TxFingerprint -> TransactionCandidate -> Hash;
     ```
 
 ## Action arguments
@@ -204,7 +204,7 @@ handleTransactionRequest
                 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;

docs/arch/node/types/crypto.juvix.md

@@ -27,14 +27,24 @@ Public key for public-key cryptography.
 type PublicKey :=
   | Curve25519PubKey ByteString
   ;
-
-instance
-PublicKeyOrd : Ord PublicKey :=
-  mkOrd@{
-    cmp := \{_ _ := Equal};
-  };
 ```
 
+??? quote "Auxiliary Juvix code"
+
+    ```juvix
+    deriving
+    instance
+    PublicKeyEq : Eq PublicKey;
+    ```
+
+    ```juvix
+    instance
+    PublicKeyOrd : Ord PublicKey :=
+      mkOrd@{
+        cmp := \{_ _ := Equal};
+      };
+    ```
+
 ### Private key
 
 Private key for public-key cryptography.
@@ -43,14 +53,22 @@ Private key for public-key cryptography.
 type PrivateKey :=
   | Curve25519PrivKey ByteString
   ;
-
-instance
-PrivateKeyOrd : Ord PrivateKey :=
-  mkOrd@{
-    cmp := \{_ _ := Equal};
-  };
 ```
 
+??? quote "Auxiliary Juvix code"
+
+    ```juvix
+    deriving
+    instance
+    PrivateKeyEq : Eq PrivateKey;
+
+    instance
+    PrivateKeyOrd : Ord PrivateKey :=
+      mkOrd@{
+        cmp := \{_ _ := Equal};
+      };
+    ```
+
 ### Secret key
 
 Secret key for secret-key cryptography.
@@ -61,6 +79,18 @@ type SecretKey :=
   ;
 ```
 
+??? quote "Auxiliary Juvix code"
+
+    ```juvix
+    deriving
+    instance
+    SecretKeyEq : Eq SecretKey;
+
+    deriving
+    instance
+    SecretKeyOrd : Ord SecretKey;
+    ```
+
 ### Signature
 
 Cryptographic signature.
@@ -80,3 +110,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};
+      };
+    ```

docs/arch/system/state/resource_machine/prelude.juvix.md

@@ -85,9 +85,23 @@ 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
-axiom Nonce : Type;
+type Nonce := mkNonce@{
+  nonce : Nat;
+};
+```
+
+```juvix
+deriving
+instance
+eqNonce : Eq Nonce;
+
+deriving
+instance
+ordNonce : Ord Nonce;
 ```
 
 #### `RandSeed`

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;
+```