Skip to content

Commit b0c1888

Browse files
lukaszczlukaszcz
authored
Shielded resource machine support (#89)
* shielded resource machine * json * wrapper * rename resources * minor naming change * Json in Applib * ToJson ByteArray * defaultCairoRoot * BaseLayer.Cairo * bug workaround * mkDefaultWitness * bug workaround * fix type-checking
1 parent 8807343 commit b0c1888

File tree

8 files changed

+266
-0
lines changed

8 files changed

+266
-0
lines changed

‎Anoma/Builtin/ByteArray.juvix

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ module Anoma.Builtin.ByteArray;
33
import Stdlib.Prelude open;
44
import BaseLayer.AnomaAtom open;
55
import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
6+
import Anoma.Data.Json open;
67

78
module ByteArray;
89
builtin bytearray
@@ -31,6 +32,12 @@ module ByteArray;
3132
size;
3233
contents := AnomaAtom.toNat contents;
3334
};
35+
36+
instance
37+
ByteArray-ToJson : ToJson ByteArray :=
38+
ToJson.mk@{
39+
toJson (b : ByteArray) : Json := Json.number (rawToAnomaContents b);
40+
};
3441
end;
3542

3643
open ByteArray using {ByteArray; fromAnomaContents; toAnomaContents} public;

‎Anoma/Data.juvix

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
module Anoma.Data;
22

33
import Anoma.Data.RandSeed open public;
4+
import Anoma.Data.Json open public;

‎Anoma/Data/Json.juvix

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
module Anoma.Data.Json;
2+
3+
import Stdlib.Prelude open;
4+
5+
builtin json
6+
type Json :=
7+
| array (List Json)
8+
| bool Bool
9+
| object (List (Pair String Json))
10+
| number Nat
11+
| string String;
12+
13+
trait
14+
type ToJson A :=
15+
mk@{
16+
toJson : A -> Json;
17+
};
18+
19+
trait
20+
type FromJson A :=
21+
mk@{
22+
fromJson : Json -> Maybe A;
23+
};

‎BaseLayer.juvix

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,6 @@ module BaseLayer;
22

33
import BaseLayer.ResourceMachine open public;
44
import BaseLayer.TransactionRequest open public;
5+
6+
import BaseLayer.ShieldedResourceMachine as Shielded public;
7+
import BaseLayer.Cairo as Cairo public;

‎BaseLayer/AnomaAtom.juvix

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
module BaseLayer.AnomaAtom;
22

33
import Stdlib.Prelude open;
4+
import Anoma.Data.Json open;
45

56
type AnomaAtom := mk Nat
67
with
@@ -20,4 +21,11 @@ with
2021

2122
deriving instance
2223
AnomaAtomOrdI : Ord AnomaAtom;
24+
25+
instance
26+
AnomaAtom-ToJson : ToJson AnomaAtom :=
27+
ToJson.mk@{
28+
toJson : AnomaAtom -> Json
29+
| (mk n) := Json.number n;
30+
};
2331
end;

‎BaseLayer/Cairo.juvix

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
module BaseLayer.Cairo;
2+
3+
import Anoma.Builtin.ByteArray open;
4+
5+
defaultCairoRoot : ByteArray :=
6+
ByteArray.mk
7+
[
8+
4;
9+
159;
10+
35;
11+
51;
12+
235;
13+
49;
14+
48;
15+
244;
16+
131;
17+
34;
18+
79;
19+
109;
20+
240;
21+
252;
22+
193;
23+
45;
24+
153;
25+
168;
26+
38;
27+
144;
28+
4;
29+
120;
30+
15;
31+
77;
32+
11;
33+
26;
34+
82;
35+
221;
36+
66;
37+
229;
38+
253;
39+
122;
40+
];

‎BaseLayer/ResourceMachine.juvix

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Anoma.Builtin.ByteArray open;
88
import Stdlib.Prelude open;
99
import Stdlib.Data.Map as Map open;
1010
import Anoma.Primitives.FixedSize open;
11+
import Anoma.Data.Json open;
1112

1213
type Tag :=
1314
| Created Commitment
@@ -69,6 +70,13 @@ with
6970

7071
deriving instance
7172
NullifierKey-Eq : Eq NullifierKey;
73+
74+
instance
75+
NullifierKey-ToJson : ToJson NullifierKey :=
76+
ToJson.mk@{
77+
toJson : NullifierKey -> Json
78+
| (privateMk b) := ToJson.toJson b;
79+
};
7280
end;
7381

7482
type Commitment := privateMk Nat
@@ -188,6 +196,13 @@ with
188196

189197
deriving instance
190198
Label-Eq : Eq Label;
199+
200+
instance
201+
Label-ToJson : ToJson Label :=
202+
ToJson.mk@{
203+
toJson : Label -> Json
204+
| (mk l) := Json.number l;
205+
};
191206
end;
192207

193208
--- A fixed-size data type encoding a number to be used once ensuring that the resource commitment is unique.
@@ -220,6 +235,13 @@ with
220235

221236
deriving instance
222237
Nonce-Eq : Eq Nonce;
238+
239+
instance
240+
Nonce-ToJson : ToJson Nonce :=
241+
ToJson.mk@{
242+
toJson : Nonce -> Json
243+
| (privateMk b) := ToJson.toJson b;
244+
};
223245
end;
224246

225247
--- The nullifier key type describing a secret required to compute the ;Nullifier; of a resource
@@ -249,6 +271,13 @@ with
249271

250272
deriving instance
251273
NullifierKeyCommitment-Eq : Eq NullifierKeyCommitment;
274+
275+
instance
276+
NullifierKeyCommitment-ToJson : ToJson NullifierKeyCommitment :=
277+
ToJson.mk@{
278+
toJson : NullifierKeyCommitment -> Json
279+
| (mk b) := ToJson.toJson b;
280+
};
252281
end;
253282

254283
builtin anoma-resource
@@ -536,6 +565,7 @@ with
536565
mk : DeltaProof := privateMk 0;
537566
end;
538567

568+
builtin anoma-transaction
539569
type Transaction :=
540570
privateMk@{
541571
roots : AnomaSet CommitmentRoot;

‎BaseLayer/ShieldedResourceMachine.juvix

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
module BaseLayer.ShieldedResourceMachine;
2+
3+
import Stdlib.Prelude open;
4+
import Anoma.Builtin.ByteArray open;
5+
import Anoma.Data.Json open;
6+
import BaseLayer.ResourceMachine open;
7+
8+
type ConsumedResource :=
9+
mk@{
10+
label : Label;
11+
quantity : Nat;
12+
value : AnomaAtom;
13+
ephemeral : Bool;
14+
nonce : Nonce;
15+
randSeed : Nat;
16+
};
17+
18+
instance
19+
ConsumedResource-ToJson : ToJson ConsumedResource :=
20+
ToJson.mk@{
21+
toJson : ConsumedResource -> Json
22+
| ConsumedResource.mk@{
23+
label;
24+
quantity;
25+
value;
26+
ephemeral;
27+
nonce;
28+
randSeed;
29+
} :=
30+
Json.object
31+
[
32+
"label_ref", ToJson.toJson label;
33+
"quantity", Json.number quantity;
34+
"value_ref", ToJson.toJson value;
35+
"is_ephemeral", Json.bool ephemeral;
36+
"nonce", ToJson.toJson nonce;
37+
"rand_seed", Json.number randSeed;
38+
];
39+
};
40+
41+
type CreatedResource :=
42+
mk@{
43+
label : Label;
44+
quantity : Nat;
45+
value : AnomaAtom;
46+
ephemeral : Bool;
47+
nonce : Nonce;
48+
nullifierKeyCommitment : NullifierKeyCommitment;
49+
randSeed : Nat;
50+
};
51+
52+
instance
53+
CreatedResource-ToJson : ToJson CreatedResource :=
54+
ToJson.mk@{
55+
toJson : CreatedResource -> Json
56+
| CreatedResource.mk@{
57+
label;
58+
quantity;
59+
value;
60+
ephemeral;
61+
nonce;
62+
nullifierKeyCommitment;
63+
randSeed;
64+
} :=
65+
Json.object
66+
[
67+
"label_ref", ToJson.toJson label;
68+
"quantity", Json.number quantity;
69+
"value_ref", ToJson.toJson value;
70+
"is_ephemeral", Json.bool ephemeral;
71+
"nonce", ToJson.toJson nonce;
72+
"nk_commitment", ToJson.toJson nullifierKeyCommitment;
73+
"rand_seed", Json.number randSeed;
74+
];
75+
};
76+
77+
type MerklePath :=
78+
mk@{
79+
path : List (Pair Nat Bool);
80+
};
81+
82+
instance
83+
MerklePath-ToJson : ToJson MerklePath :=
84+
ToJson.mk@{
85+
toJson : MerklePath -> Json
86+
| MerklePath.mk@{path} :=
87+
Json.array
88+
(map
89+
\{x :=
90+
Json.object
91+
["fst", Json.number (fst x); "snd", Json.bool (snd x)]}
92+
path);
93+
};
94+
95+
builtin anoma-compliance-inputs
96+
type ComplianceInputs :=
97+
mk@{
98+
consumedResource : ConsumedResource;
99+
createdResource : CreatedResource;
100+
inputNullifierKey : NullifierKey;
101+
merklePath : MerklePath;
102+
rcv : Nat;
103+
ephRoot : ByteArray;
104+
};
105+
106+
instance
107+
ComplianceInputs-ToJson : ToJson ComplianceInputs :=
108+
ToJson.mk@{
109+
toJson : ComplianceInputs -> Json
110+
| ComplianceInputs.mk@{
111+
consumedResource;
112+
createdResource;
113+
inputNullifierKey;
114+
merklePath;
115+
rcv;
116+
ephRoot;
117+
} :=
118+
Json.object
119+
[
120+
"input", ToJson.toJson consumedResource;
121+
"output", ToJson.toJson createdResource;
122+
"input_nf_key", ToJson.toJson inputNullifierKey;
123+
"merkle_path", ToJson.toJson merklePath;
124+
"rcv", Json.number rcv;
125+
"eph_root", ToJson.toJson ephRoot;
126+
];
127+
};
128+
129+
builtin anoma-create-from-compliance-inputs
130+
axiom createFromJsonComplianceInputs
131+
: (complianceInputs : List Json)
132+
-> (inputLogics : List ByteArray)
133+
-> (inputWitnesses : List Json)
134+
-> (outputLogics : List ByteArray)
135+
-> (outputWitnesses : List Json)
136+
-> Transaction;
137+
138+
createFromComplianceInputs
139+
(complianceInputs : List ComplianceInputs)
140+
: (inputLogics : List ByteArray)
141+
-> (inputWitnesses : List Json)
142+
-> (outputLogics : List ByteArray)
143+
-> (outputWitnesses : List Json)
144+
-> Transaction :=
145+
createFromJsonComplianceInputs (map ToJson.toJson complianceInputs);
146+
147+
mkDefaultWitness (isConsumed : Bool) : Json :=
148+
Json.object
149+
[
150+
"self_resource", Json.string "";
151+
"is_consumed", Json.bool isConsumed;
152+
"resource_nf_key", Json.string "";
153+
"merkle_path", Json.string "";
154+
];

0 commit comments

Comments
 (0)