1  import credits.alpha;
  2  
  3  program large_functions.alpha;
  4  
  5  function join_3:
  6      input r0 as credits.alpha/credits.record;
  7      input r1 as credits.alpha/credits.record;
  8      input r2 as credits.alpha/credits.record;
  9      assert.eq r0.owner r1.owner;
 10      assert.eq r1.owner r2.owner;
 11      call credits.alpha/join r0 r1 into r3;
 12      call credits.alpha/join r3 r2 into r4;
 13      output r4 as credits.alpha/credits.record;
 14  
 15  function join_5:
 16      input r0 as credits.alpha/credits.record;
 17      input r1 as credits.alpha/credits.record;
 18      input r2 as credits.alpha/credits.record;
 19      input r3 as credits.alpha/credits.record;
 20      input r4 as credits.alpha/credits.record;
 21      assert.eq r0.owner r1.owner;
 22      assert.eq r1.owner r2.owner;
 23      assert.eq r2.owner r3.owner;
 24      assert.eq r3.owner r4.owner;
 25      call credits.alpha/join r0 r1 into r5;
 26      call credits.alpha/join r2 r3 into r6;
 27      call credits.alpha/join r5 r6 into r7;
 28      call credits.alpha/join r7 r4 into r8;
 29      output r8 as credits.alpha/credits.record;
 30  
 31  function join6:
 32      input r0 as credits.alpha/credits.record;
 33      input r1 as credits.alpha/credits.record;
 34      input r2 as credits.alpha/credits.record;
 35      input r3 as credits.alpha/credits.record;
 36      input r4 as credits.alpha/credits.record;
 37      input r5 as credits.alpha/credits.record;
 38      assert.eq r0.owner r1.owner;
 39      assert.eq r1.owner r2.owner;
 40      assert.eq r2.owner r3.owner;
 41      assert.eq r3.owner r4.owner;
 42      assert.eq r4.owner r5.owner;
 43      call credits.alpha/join r0 r1 into r6;
 44      call credits.alpha/join r2 r3 into r7;
 45      call credits.alpha/join r4 r5 into r8;
 46      call credits.alpha/join r6 r7 into r9;
 47      call credits.alpha/join r9 r8 into r10;
 48      output r10 as credits.alpha/credits.record;
 49  
 50  function join7:
 51      input r0 as credits.alpha/credits.record;
 52      input r1 as credits.alpha/credits.record;
 53      input r2 as credits.alpha/credits.record;
 54      input r3 as credits.alpha/credits.record;
 55      input r4 as credits.alpha/credits.record;
 56      input r5 as credits.alpha/credits.record;
 57      input r6 as credits.alpha/credits.record;
 58      assert.eq r0.owner r1.owner;
 59      assert.eq r1.owner r2.owner;
 60      assert.eq r2.owner r3.owner;
 61      assert.eq r3.owner r4.owner;
 62      assert.eq r4.owner r5.owner;
 63      assert.eq r5.owner r6.owner;
 64      call credits.alpha/join r0 r1 into r7;
 65      call credits.alpha/join r2 r3 into r8;
 66      call credits.alpha/join r4 r5 into r9;
 67      call credits.alpha/join r7 r8 into r10;
 68      call credits.alpha/join r10 r9 into r11;
 69      call credits.alpha/join r11 r6 into r12;
 70      output r12 as credits.alpha/credits.record;
 71  
 72  function join8:
 73      input r0 as credits.alpha/credits.record;
 74      input r1 as credits.alpha/credits.record;
 75      input r2 as credits.alpha/credits.record;
 76      input r3 as credits.alpha/credits.record;
 77      input r4 as credits.alpha/credits.record;
 78      input r5 as credits.alpha/credits.record;
 79      input r6 as credits.alpha/credits.record;
 80      input r7 as credits.alpha/credits.record;
 81      assert.eq r0.owner r1.owner;
 82      assert.eq r1.owner r2.owner;
 83      assert.eq r2.owner r3.owner;
 84      assert.eq r3.owner r4.owner;
 85      assert.eq r4.owner r5.owner;
 86      assert.eq r5.owner r6.owner;
 87      assert.eq r6.owner r7.owner;
 88      call credits.alpha/join r0 r1 into r8;
 89      call credits.alpha/join r2 r3 into r9;
 90      call credits.alpha/join r4 r5 into r10;
 91      call credits.alpha/join r6 r7 into r11;
 92      call credits.alpha/join r8 r9 into r12;
 93      call credits.alpha/join r11 r10 into r13;
 94      call credits.alpha/join r12 r13 into r14;
 95      output r14 as credits.alpha/credits.record;
 96  
 97  function join9:
 98      input r0 as credits.alpha/credits.record;
 99      input r1 as credits.alpha/credits.record;
100      input r2 as credits.alpha/credits.record;
101      input r3 as credits.alpha/credits.record;
102      input r4 as credits.alpha/credits.record;
103      input r5 as credits.alpha/credits.record;
104      input r6 as credits.alpha/credits.record;
105      input r7 as credits.alpha/credits.record;
106      input r8 as credits.alpha/credits.record;
107      assert.eq r0.owner r1.owner;
108      assert.eq r1.owner r2.owner;
109      assert.eq r2.owner r3.owner;
110      assert.eq r3.owner r4.owner;
111      assert.eq r4.owner r5.owner;
112      assert.eq r5.owner r6.owner;
113      assert.eq r6.owner r7.owner;
114      assert.eq r7.owner r8.owner;
115      call credits.alpha/join r0 r1 into r9;
116      call credits.alpha/join r2 r3 into r10;
117      call credits.alpha/join r4 r5 into r11;
118      call credits.alpha/join r6 r7 into r12;
119      call credits.alpha/join r9 r10 into r13;
120      call credits.alpha/join r12 r11 into r14;
121      call credits.alpha/join r13 r14 into r15;
122      call credits.alpha/join r15 r8 into r16;
123      output r16 as credits.alpha/credits.record;
124  
125  function join10:
126      input r0 as credits.alpha/credits.record;
127      input r1 as credits.alpha/credits.record;
128      input r2 as credits.alpha/credits.record;
129      input r3 as credits.alpha/credits.record;
130      input r4 as credits.alpha/credits.record;
131      input r5 as credits.alpha/credits.record;
132      input r6 as credits.alpha/credits.record;
133      input r7 as credits.alpha/credits.record;
134      input r8 as credits.alpha/credits.record;
135      input r9 as credits.alpha/credits.record;
136      assert.eq r0.owner r1.owner;
137      assert.eq r1.owner r2.owner;
138      assert.eq r2.owner r3.owner;
139      assert.eq r3.owner r4.owner;
140      assert.eq r4.owner r5.owner;
141      assert.eq r5.owner r6.owner;
142      assert.eq r6.owner r7.owner;
143      assert.eq r7.owner r8.owner;
144      assert.eq r8.owner r9.owner;
145      call credits.alpha/join r0 r1 into r10;
146      call credits.alpha/join r2 r3 into r11;
147      call credits.alpha/join r4 r5 into r12;
148      call credits.alpha/join r6 r7 into r13;
149      call credits.alpha/join r8 r9 into r14;
150      call credits.alpha/join r10 r11 into r15;
151      call credits.alpha/join r13 r12 into r16;
152      call credits.alpha/join r15 r16 into r17;
153      call credits.alpha/join r17 r14 into r18;
154      output r18 as credits.alpha/credits.record;
155  
156  function transfer_3:
157      input r0 as address.private;
158      input r1 as credits.alpha/credits.record;
159      input r2 as credits.alpha/credits.record;
160      input r3 as credits.alpha/credits.record;
161      assert.eq r1.owner r2.owner;
162      assert.eq r2.owner r3.owner;
163      call credits.alpha/transfer_private r1 r0 r1.microcredits into r4 r5;
164      call credits.alpha/transfer_private r2 r0 r2.microcredits into r6 r7;
165      call credits.alpha/transfer_private r3 r0 r3.microcredits into r8 r9;
166      output r4 as credits.alpha/credits.record;
167      output r5 as credits.alpha/credits.record;
168      output r6 as credits.alpha/credits.record;
169      output r7 as credits.alpha/credits.record;
170      output r8 as credits.alpha/credits.record;
171      output r9 as credits.alpha/credits.record;
172  
173  function transfer_5:
174      input r0 as address.private;
175      input r1 as credits.alpha/credits.record;
176      input r2 as credits.alpha/credits.record;
177      input r3 as credits.alpha/credits.record;
178      input r4 as credits.alpha/credits.record;
179      input r5 as credits.alpha/credits.record;
180      assert.eq r1.owner r2.owner;
181      assert.eq r2.owner r3.owner;
182      assert.eq r3.owner r4.owner;
183      assert.eq r4.owner r5.owner;
184      call credits.alpha/transfer_private r1 r0 r1.microcredits into r6 r7;
185      call credits.alpha/transfer_private r2 r0 r2.microcredits into r8 r9;
186      call credits.alpha/transfer_private r3 r0 r3.microcredits into r10 r11;
187      call credits.alpha/transfer_private r4 r0 r4.microcredits into r12 r13;
188      call credits.alpha/transfer_private r5 r0 r5.microcredits into r14 r15;
189      output r6 as credits.alpha/credits.record;
190      output r7 as credits.alpha/credits.record;
191      output r8 as credits.alpha/credits.record;
192      output r9 as credits.alpha/credits.record;
193      output r10 as credits.alpha/credits.record;
194      output r11 as credits.alpha/credits.record;
195      output r12 as credits.alpha/credits.record;
196      output r13 as credits.alpha/credits.record;
197      output r14 as credits.alpha/credits.record;
198      output r15 as credits.alpha/credits.record;
199  
200  function split_3:
201      input r0 as u64.private;
202      input r1 as credits.alpha/credits.record;
203      input r2 as credits.alpha/credits.record;
204      input r3 as credits.alpha/credits.record;
205      assert.eq r1.owner r2.owner;
206      assert.eq r2.owner r3.owner;
207      call credits.alpha/split r1 r0 into r4 r5;
208      call credits.alpha/split r2 r0 into r6 r7;
209      call credits.alpha/split r3 r0 into r8 r9;
210      output r4 as credits.alpha/credits.record;
211      output r5 as credits.alpha/credits.record;
212      output r6 as credits.alpha/credits.record;
213      output r7 as credits.alpha/credits.record;
214      output r8 as credits.alpha/credits.record;
215      output r9 as credits.alpha/credits.record;
216  
217  function split_5:
218      input r0 as u64.private;
219      input r1 as credits.alpha/credits.record;
220      input r2 as credits.alpha/credits.record;
221      input r3 as credits.alpha/credits.record;
222      input r4 as credits.alpha/credits.record;
223      input r5 as credits.alpha/credits.record;
224      assert.eq r1.owner r2.owner;
225      assert.eq r2.owner r3.owner;
226      assert.eq r3.owner r4.owner;
227      assert.eq r4.owner r5.owner;
228      call credits.alpha/split r1 r0 into r6 r7;
229      call credits.alpha/split r2 r0 into r8 r9;
230      call credits.alpha/split r3 r0 into r10 r11;
231      call credits.alpha/split r4 r0 into r12 r13;
232      call credits.alpha/split r5 r0 into r14 r15;
233      output r6 as credits.alpha/credits.record;
234      output r7 as credits.alpha/credits.record;
235      output r8 as credits.alpha/credits.record;
236      output r9 as credits.alpha/credits.record;
237      output r10 as credits.alpha/credits.record;
238      output r11 as credits.alpha/credits.record;
239      output r12 as credits.alpha/credits.record;
240      output r13 as credits.alpha/credits.record;
241      output r14 as credits.alpha/credits.record;
242      output r15 as credits.alpha/credits.record;