@@ -3,6 +3,7 @@ module ResourceMachine;
3
3
import Encode open;
4
4
import ByteArray open;
5
5
import Stdlib.Prelude open;
6
+ import Stdlib.Debug.Fail open;
6
7
7
8
type Tag :=
8
9
| Created Commitment
31
32
32
33
--- The nullifier key type describing a secret required to compute the ;Nullifier; of a resource
33
34
builtin anoma-nullifier-key
34
- type NullifierKey :=
35
- privateMk@{
36
- unNullifierKey : ByteArray;
37
- }
35
+ type NullifierKey := privateMk ByteArray
38
36
with
37
+ size : Nat := 64;
38
+
39
39
fromByteArray : ByteArray -> NullifierKey := privateMk;
40
40
41
41
toByteArray : NullifierKey -> ByteArray
42
42
| (privateMk b) := b;
43
43
44
44
module Transparent;
45
- mk : NullifierKey := privateMk (ByteArray.zero 64 );
45
+ mk : NullifierKey := privateMk (ByteArray.zero size );
46
46
end;
47
47
48
48
deriving instance
@@ -94,15 +94,15 @@ type ConsumedItem :=
94
94
mk@{
95
95
nullifier : Nullifier;
96
96
root : CommitmentRoot;
97
- logic : Nat ;
97
+ logic : Encoded Logic ;
98
98
};
99
99
100
100
type DeltaHash := privateMk Nat;
101
101
102
102
type CreatedItem :=
103
103
mk@{
104
104
commitment : Commitment;
105
- logic : Nat ;
105
+ logic : Encoded Logic ;
106
106
};
107
107
108
108
type Instance :=
@@ -134,6 +134,7 @@ type Logic : Type :=
134
134
compute : Logic.Arg -> Bool;
135
135
}
136
136
with
137
+ -- called RLPS.Instance
137
138
positive
138
139
type Arg :=
139
140
mk@{
@@ -161,18 +162,18 @@ end;
161
162
162
163
--- A fixed-size data type encoding a number to be used once ensuring that the resource commitment is unique.
163
164
--- NOTE: This should be a number having an at most negligible chance of repeating is sufficient, e.g., a pseudo-random number.
164
- type Nonce := internalMk ByteArray
165
+ type Nonce := privateMk ByteArray
165
166
with
166
167
size : Nat := 32;
167
168
168
- fromNat : Nat -> Nonce := fromAnomaContents size >> internalMk ;
169
+ fromNat : Nat -> Nonce := fromAnomaContents size >> privateMk ;
169
170
170
- from32SizedByteArray : ByteArray -> Nonce := internalMk ;
171
+ from32SizedByteArray : ByteArray -> Nonce := privateMk ;
171
172
172
173
toAnomaAtom : Nonce -> AnomaAtom := toNat >> AnomaAtom.fromNat;
173
174
174
175
toNat : Nonce -> Nat
175
- | (internalMk nonce) := toAnomaContents nonce;
176
+ | (privateMk nonce) := toAnomaContents nonce;
176
177
177
178
deriving instance
178
179
Nonce-Ord : Ord Nonce;
@@ -210,8 +211,8 @@ type Resource :=
210
211
value : AnomaAtom;
211
212
quantity : Nat;
212
213
ephemeral : Bool;
213
- nonce : AnomaAtom ;
214
- nullifierKeyCommitment : AnomaAtom ;
214
+ nonce : Nonce ;
215
+ nullifierKeyCommitment : NullifierKeyCommitment ;
215
216
unusedRandSeed : Nat;
216
217
}
217
218
with
@@ -377,6 +378,36 @@ with
377
378
end;
378
379
end;
379
380
381
+ type RootedNullifiableResource :=
382
+ mk@{
383
+ key : NullifierKey;
384
+ resource : Resource;
385
+ root : CommitmentRoot;
386
+ }
387
+ with
388
+ module Transparent;
389
+ mkEphemeral (resource : Resource) : RootedNullifiableResource :=
390
+ if
391
+ | Resource.ephemeral resource :=
392
+ mk@{
393
+ resource;
394
+ root := CommitmentRoot.fromNat 0;
395
+ }
396
+ | else :=
397
+ failwith "mkEphemeral requires an ephemeral resource as an argument";
398
+
399
+ mk
400
+ (resource : Resource)
401
+ (root : CommitmentRoot)
402
+ : RootedNullifiableResource :=
403
+ RootedNullifiableResource.mk@{
404
+ resource;
405
+ root;
406
+ key := NullifierKey.Transparent.mk;
407
+ };
408
+ end;
409
+ end;
410
+
380
411
type NullifiableResource :=
381
412
mk@{
382
413
key : NullifierKey;
@@ -416,21 +447,19 @@ with
416
447
axiom listDelta : List Action -> Delta;
417
448
418
449
create
419
- (consumed : List NullifiableResource )
450
+ (consumed : List RootedNullifiableResource )
420
451
(created : List Resource)
421
452
(appData : AppData)
422
453
: Action :=
423
454
builtinCreate@{
424
- -- consumed := AnomaSet.fromList consumed;
425
- -- created := AnomaSet.fromList created;
426
455
consumed;
427
456
created;
428
457
appData;
429
458
};
430
459
431
460
builtin anoma-action-create
432
461
axiom builtinCreate
433
- (consumed : List NullifiableResource )
462
+ (consumed : List RootedNullifiableResource )
434
463
(created : List Resource)
435
464
(appData : AppData)
436
465
: Action;
0 commit comments