triton_vm/
example_programs.rs

1use isa::program::Program;
2use isa::triton_program;
3use lazy_static::lazy_static;
4
5lazy_static! {
6    pub static ref FIBONACCI_SEQUENCE: Program = fibonacci_sequence();
7    pub static ref GREATEST_COMMON_DIVISOR: Program = greatest_common_divisor();
8    pub static ref PROGRAM_WITH_MANY_U32_INSTRUCTIONS: Program =
9        program_with_many_u32_instructions();
10    pub static ref VERIFY_SUDOKU: Program = verify_sudoku();
11    pub static ref CALCULATE_NEW_MMR_PEAKS_FROM_APPEND_WITH_SAFE_LISTS: Program =
12        calculate_new_mmr_peaks_from_append_with_safe_lists();
13    pub static ref MERKLE_TREE_AUTHENTICATION_PATH_VERIFY: Program =
14        merkle_tree_authentication_path_verify();
15    pub static ref MERKLE_TREE_UPDATE: Program = merkle_tree_update();
16}
17
18fn fibonacci_sequence() -> Program {
19    triton_program!(
20        // initialize stack: ⊥ 0 1 i
21        push 0
22        push 1
23        read_io 1
24
25        // is any looping necessary?
26        dup 0
27        skiz
28        call fib_loop
29
30        // pop zero, write result
31        pop 1
32        write_io 1
33        halt
34
35        // before: ⊥ 0 1 i
36        // after:  ⊥ fib(i-1) fib(i) 0
37        fib_loop:
38            push -1   // ⊥ a b j -1
39            add       // ⊥ a b (j-1)
40            swap 2    // ⊥ (j-1) b a
41            dup 1     // ⊥ (j-1) b a b
42            add       // ⊥ (j-1) b (a+b)
43            swap 1    // ⊥ (j-1) (a+b) b
44            swap 2    // ⊥ b (a+b) (j-1)
45            dup 0     // ⊥ b (a+b) (j-1) (j-1)
46            skiz      // ⊥ b (a+b) (j-1)
47            recurse
48            return
49    )
50}
51
52fn greatest_common_divisor() -> Program {
53    triton_program!(
54        read_io 2    // _ a b
55        dup 1        // _ a b a
56        dup 1        // _ a b a b
57        lt           // _ a b b<a
58        skiz         // _ a b
59            swap 1   // _ d n where n > d
60
61        loop_cond:
62        dup 1
63        push 0
64        eq
65        skiz
66            call terminate  // _ d n where d != 0
67        dup 1               // _ d n d
68        dup 1               // _ d n d n
69        div_mod             // _ d n q r
70        swap 2              // _ d r q n
71        pop 2               // _ d r
72        swap 1              // _ r d
73        call loop_cond
74
75        terminate:
76            // _ d n where d == 0
77            write_io 1      // _ d
78            halt
79    )
80}
81
82fn program_with_many_u32_instructions() -> Program {
83    triton_program!(
84        push 1311768464867721216 split
85        push 13387 push 78810 lt
86        push     5 push     7 pow
87        push 69584 push  6796 xor
88        push 64972 push  3915 and
89        push 98668 push 15787 div_mod
90        push 15787 push 98668 div_mod
91        push 98141 push  7397 and
92        push 67749 push 60797 lt
93        push 49528 split
94        push 53483 call lsb
95        push 79655 call is_u32
96        push 60615 log_2_floor
97        push    13 push     5 pow
98        push 86323 push 37607 xor
99        push 32374 push 20636 pow
100        push 97416 log_2_floor
101        push 14392 push 31589 div_mod
102        halt
103        lsb:
104            push 2 swap 1 div_mod return
105        is_u32:
106            split pop 1 push 0 eq return
107    )
108}
109
110/// Triton program to verify Merkle authentication paths.
111/// - input: merkle root, number of leafs, leaf values, APs
112/// - output: Result<(), VMFail>
113fn merkle_tree_authentication_path_verify() -> Program {
114    triton_program!(
115        read_io 1                                   // number of authentication paths to test
116                                                    // stack: [num]
117        mt_ap_verify:                               // proper program starts here
118        push 0 write_mem 1 pop 1                    // store number of APs at RAM address 0
119                                                    // stack: []
120        read_io 5                                   // read Merkle root
121                                                    // stack: [r4 r3 r2 r1 r0]
122        call check_aps
123        pop 5                                       // leave clean stack: Merkle root
124                                                    // stack: []
125        halt                                        // done – should be “return”
126
127        // subroutine: check AP one at a time
128        // stack before: [* r4 r3 r2 r1 r0]
129        // stack after:  [* r4 r3 r2 r1 r0]
130        check_aps:
131        push 0 read_mem 1 pop 1 dup 0   // get number of APs left to check
132                                        // stack: [* r4 r3 r2 r1 r0 num_left num_left]
133        push 0 eq                       // see if there are authentication paths left
134                                        // stack: [* r4 r3 r2 r1 r0 0 num_left num_left==0]
135        skiz return                     // return if no authentication paths left
136        push -1 add                     // decrease number of authentication paths left to check
137                                        // stack: [* r4 r3 r2 r1 r0 num_left-1]
138        push 0 write_mem 1 pop 1        // write decreased number to address 0
139                                        // stack: [* r4 r3 r2 r1 r0]
140        call get_idx_and_leaf
141                                        // stack: [* r4 r3 r2 r1 r0 idx l4 l3 l2 l1 l0]
142        call traverse_tree
143                                        // stack: [* r4 r3 r2 r1 r0   1 d4 d3 d2 d1 d0]
144        call assert_tree_top
145                                        // stack: [* r4 r3 r2 r1 r0]
146        recurse                         // check next AP
147
148        // subroutine: read index & hash leaf
149        // stack before: [*]
150        // stack after:  [* idx l4 l3 l2 l1 l0]
151        get_idx_and_leaf:
152        read_io 1                                   // read node index
153        read_io 5                                   // read leaf's value
154        return
155
156        // subroutine: go up tree
157        // stack before: [* r4 r3 r2 r1 r0 idx l4 l3 l2 l1 l0]
158        // stack after:  [* r4 r3 r2 r1 r0   1 d4 d3 d2 d1 d0]
159        traverse_tree:
160        dup 5 push 1 eq skiz return                 // break loop if node index is 1
161        merkle_step recurse                         // move up one level in the Merkle tree
162
163        // subroutine: compare digests
164        // stack before: [* r4 r3 r2 r1 r0   1 d4 d3 d2 d1 d0]
165        // stack after:  [* r4 r3 r2 r1 r0]
166        assert_tree_top:
167                                                    // stack: [* r4 r3 r2 r1 r0   1 d4 d3 d2 d1 d0]
168        swap 1 swap 2 swap 3 swap 4 swap 5
169                                                    // stack: [* r4 r3 r2 r1 r0 d4 d3 d2 d1 d0   1]
170        assert                                      // ensure the entire path was traversed
171                                                    // stack: [* r4 r3 r2 r1 r0 d4 d3 d2 d1 d0]
172        assert_vector                               // actually compare to root of tree
173        return
174    )
175}
176
177/// Triton program to verifiably change a Merkle tree's leaf. That is:
178/// 1. verify that the supplied `old_leaf` is indeed a leaf in the Merkle tree
179///    defined by the `merkle_root` and the `tree_height`,
180/// 2. update the leaf at the specified `leaf_index` with the `new_leaf`, and
181/// 3. return the new Merkle root.
182///
183/// The authentication path for the leaf to update has to be supplied via RAM.
184///
185/// - input:
186///     - RAM address of leaf's authentication path
187///     - leaf index to update
188///     - Merkle tree's height
189///     - old leaf
190///     - (current) merkle root
191///     - new leaf
192/// - output:
193///     - new root
194fn merkle_tree_update() -> Program {
195    triton_program! {
196        read_io 3           // _ *ap leaf_index tree_height
197        push 2 pow add      // _ *ap node_index
198        dup 1 push 1 dup 2  // _ *ap node_index *ap 1 node_index
199        read_io 5           // _ *ap node_index *ap 1 node_index [old_leaf; 5]
200        call compute_root   // _ *ap node_index *ap' 1 1 [root; 5]
201        read_io 5           // _ *ap node_index *ap' 1 1 [root; 5] [presumed_root; 5]
202        assert_vector       // _ *ap node_index *ap' 1 1 [root; 5]
203        pop 5 pop 3         // _ *ap node_index
204        push 1 swap 1       // _ *ap 1 node_index
205        read_io 5           // _ *ap 1 node_index [new_leaf; 5]
206        call compute_root   // _ *ap' 1 1 [new_root; 5]
207        write_io 5          // _ *ap' 1 1
208        pop 3 halt          // _
209
210        // BEFORE: _ *ap                     1 node_index [leaf; 5]
211        // AFTER:  _ (*ap + 5 * tree_height) 1          1 [root; 5]
212        compute_root:
213            merkle_step_mem
214            recurse_or_return
215    }
216}
217
218fn verify_sudoku() -> Program {
219    // RAM layout:
220    // 0..=8: primes for mapping digits 1..=9
221    // 9: flag for whether the Sudoku is valid
222    // 10..=90: the Sudoku grid
223    //
224    // 10 11 12  13 14 15  16 17 18
225    // 19 20 21  22 23 24  25 26 27
226    // 28 29 30  31 32 33  34 35 36
227    //
228    // 37 38 39  40 41 42  43 44 45
229    // 46 47 48  49 50 51  52 53 54
230    // 55 56 57  58 59 60  61 62 63
231    //
232    // 64 65 66  67 68 69  70 71 72
233    // 73 74 75  76 77 78  79 80 81
234    // 82 83 84  85 86 87  88 89 90
235
236    triton_program!(
237        call initialize_flag
238        call initialize_primes
239        call read_sudoku
240        call write_sudoku_and_check_rows
241        call check_columns
242        call check_squares
243        call assert_flag
244
245        // For checking whether the Sudoku is valid. Initially `true`, set to
246        // `false` if any inconsistency is found.
247        initialize_flag:
248            push 1                        // _ 1
249            push 0                        // _ 1 0
250            write_mem 1                   // _ 1
251            pop 1                         // _
252            return
253
254        invalidate_flag:
255            push 0                        // _ 0
256            push 0                        // _ 0 0
257            write_mem 1                   // _ 1
258            pop 1                         // _
259            return
260
261        assert_flag:
262            push 0                        // _ 0
263            read_mem 1                    // _ flag -1
264            pop 1                         // _ flag
265            assert                        // _
266            halt
267
268        // For mapping legal Sudoku digits to distinct primes. Helps with
269        // checking consistency of rows, columns, and boxes.
270        initialize_primes:
271            push 23 push 19 push 17
272            push 13 push 11 push  7
273            push  5 push  3 push  2
274            push 1 write_mem 5 write_mem 4
275            pop 1
276            return
277
278        read_sudoku:
279            call read9 call read9 call read9
280            call read9 call read9 call read9
281            call read9 call read9 call read9
282            return
283
284        read9:
285            call read1 call read1 call read1
286            call read1 call read1 call read1
287            call read1 call read1 call read1
288            return
289
290        // Applies the mapping from legal Sudoku digits to distinct primes.
291        read1:                            // _
292            read_io 1                     // _ d
293            read_mem 1                    // _ p d-1
294            pop 1                         // _ p
295            return
296
297        write_sudoku_and_check_rows:      // row0 row1 row2 row3 row4 row5 row6 row7 row8
298            push 10                       // row0 row1 row2 row3 row4 row5 row6 row7 row8 10
299            call write_and_check_one_row  // row0 row1 row2 row3 row4 row5 row6 row7 19
300            call write_and_check_one_row  // row0 row1 row2 row3 row4 row5 row6 27
301            call write_and_check_one_row  // row0 row1 row2 row3 row4 row5 36
302            call write_and_check_one_row  // row0 row1 row2 row3 row4 45
303            call write_and_check_one_row  // row0 row1 row2 row3 54
304            call write_and_check_one_row  // row0 row1 row2 63
305            call write_and_check_one_row  // row0 row1 72
306            call write_and_check_one_row  // row0 81
307            call write_and_check_one_row  // 90
308            pop 1                         // ⊥
309            return
310
311        write_and_check_one_row:          // row addr
312            dup 9 dup 9 dup 9
313            dup 9 dup 9 dup 9
314            dup 9 dup 9 dup 9             // row addr row
315            call check_9_numbers          // row addr
316            write_mem 5 write_mem 4       // addr+9
317            return
318
319        check_columns:
320            push 82 call check_one_column
321            push 83 call check_one_column
322            push 84 call check_one_column
323            push 85 call check_one_column
324            push 86 call check_one_column
325            push 87 call check_one_column
326            push 88 call check_one_column
327            push 89 call check_one_column
328            push 90 call check_one_column
329            return
330
331        check_one_column:
332            read_mem 1 push -8 add read_mem 1 push -8 add read_mem 1 push -8 add
333            read_mem 1 push -8 add read_mem 1 push -8 add read_mem 1 push -8 add
334            read_mem 1 push -8 add read_mem 1 push -8 add read_mem 1 pop 1
335            call check_9_numbers
336            return
337
338        check_squares:
339            push 30 call check_one_square
340            push 33 call check_one_square
341            push 36 call check_one_square
342            push 57 call check_one_square
343            push 60 call check_one_square
344            push 63 call check_one_square
345            push 84 call check_one_square
346            push 87 call check_one_square
347            push 90 call check_one_square
348            return
349
350        check_one_square:
351            read_mem 3 push -6 add
352            read_mem 3 push -6 add
353            read_mem 3 pop 1
354            call check_9_numbers
355            return
356
357        check_9_numbers:
358            mul mul mul
359            mul mul mul
360            mul mul
361            // 223092870 = 2·3·5·7·11·13·17·19·23
362            push 223092870 eq
363            skiz return
364            call invalidate_flag
365            return
366    )
367}
368
369pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program {
370    triton_program!(
371        // Stack and memory setup
372        push 0                          // _ 0
373        push 3                          // _ 0 3
374        push 1                          // _ 0 3 1
375
376        push 00457470286889025784
377        push 04071246825597671119
378        push 17834064596403781463
379        push 17484910066710486708
380        push 06700794775299091393       // _ 0 3 1 [digest]
381
382        push 06595477061838874830
383        push 10897391716490043893
384        push 01807330184488272967
385        push 05415221245149797169
386        push 05057320540678713304       // _ 0 3 1 [digest] [digest]
387
388        push 01838589939278841373
389        push 02628975953172153832
390        push 06845409670928290394
391        push 00880730500905369322
392        push 04594396536654736100       // _ 0 3 1 [digest] [digest] [digest]
393
394        push 64                         // _ 0 3 1 [digest] [digest] [digest] 64
395        push 2                          // _ 0 3 1 [digest] [digest] [digest] 64 2
396        push 323                        // _ 0 3 1 [digest] [digest] [digest] 64 2 323
397
398        push 0                          // _ 0 3 1 [digest] [digest] [digest] 64 2 323 0
399        write_mem 3                     // _ 0 3 1 [digest] [digest] [digest] 3
400        write_mem 5                     // _ 0 3 1 [digest] [digest] 8
401        write_mem 5                     // _ 0 3 1 [digest] 13
402        pop 1                           // _ 0 3 1 [digest]
403
404        call tasm_mmr_calculate_new_peaks_from_append_safe
405        halt
406
407        // Main function
408        // BEFORE: _ [old_leaf_count: u64] *peaks [digest]
409        // AFTER:  _ *new_peaks *auth_path
410        tasm_mmr_calculate_new_peaks_from_append_safe:
411            dup 5 dup 5 dup 5 dup 5 dup 5 dup 5
412            call tasm_list_safe_u32_push_digest
413            pop 5                       // _ [old_leaf_count: u64] *peaks
414
415            // Create auth_path return value (vector living in RAM)
416            // All MMR auth paths have capacity for 64 digests
417            push 64                     // _ [old_leaf_count: u64] *peaks 64
418            call tasm_list_safe_u32_new_digest
419
420            swap 1
421            // _ [old_leaf_count: u64] *auth_path *peaks
422
423            dup 3 dup 3
424            // _ [old_leaf_count: u64] *auth_path *peaks [old_leaf_count: u64]
425
426            call tasm_arithmetic_u64_incr
427            call tasm_arithmetic_u64_index_of_last_nonzero_bit
428
429            call tasm_mmr_calculate_new_peaks_from_append_safe_while
430            // _ [old_leaf_count: u64] *auth_path *peaks (rll = 0)
431
432            pop 1
433            swap 3 pop 1 swap 1 pop 1
434            // _ *peaks *auth_path
435
436            return
437
438        // Stack start and end: _ *auth_path *peaks rll
439        tasm_mmr_calculate_new_peaks_from_append_safe_while:
440            dup 0
441            push 0
442            eq
443            skiz
444                return
445            // _ *auth_path *peaks rll
446
447            swap 2 swap 1
448            // _ rll *auth_path *peaks
449
450            dup 0
451            dup 0
452            call tasm_list_safe_u32_pop_digest
453            // _ rll *auth_path *peaks *peaks [new: Digest]
454
455            dup 5
456            // _ rll *auth_path *peaks *peaks [new: Digest] *peaks
457
458            call tasm_list_safe_u32_pop_digest
459            // _ rll *auth_path *peaks *peaks [new: Digest] [old_peak: Digest]
460
461            // Update authentication path with latest previous_peak
462            dup 12
463            // _ rll *auth_path *peaks *peaks [new: Digest] [old_peak: Digest] *auth_path
464
465            dup 5 dup 5 dup 5 dup 5 dup 5
466            call tasm_list_safe_u32_push_digest
467            // _ rll *auth_path *peaks *peaks [new: Digest] [old_peak: Digest]
468
469            hash
470            // _ rll *auth_path *peaks *peaks [new_peak: Digest]
471
472            call tasm_list_safe_u32_push_digest
473            // _ rll *auth_path *peaks
474
475            swap 1 swap 2
476            // _ *auth_path *peaks rll
477
478            push -1
479            add
480            // _ *auth_path *peaks (rll - 1)
481
482            recurse
483
484
485        // Before: _ value_hi value_lo
486        // After: _ (value + 1)_hi (value + 1)_lo
487        tasm_arithmetic_u64_incr_carry:
488            pop 1
489            push 1
490            add
491            dup 0
492            push 4294967296
493            eq
494            push 0
495            eq
496            assert
497            push 0
498            return
499
500        tasm_arithmetic_u64_incr:
501            push 1
502            add
503            dup 0
504            push 4294967296
505            eq
506            skiz
507                call tasm_arithmetic_u64_incr_carry
508            return
509
510        // Before: _ *list, elem[4], elem[3], elem[2], elem[1], elem[0]
511        // After:  _
512        tasm_list_safe_u32_push_digest:
513            dup 5       // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list
514            push 1 add  // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+1
515            read_mem 2  // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] capacity len *list-1
516
517            // Verify that length < capacity
518            swap 2      // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len capacity
519            dup 1       // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len capacity len
520            lt          // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len capacity>len
521            assert      // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len
522
523            // Adjust ram pointer
524            push 5      // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len 5
525            mul         // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 5·len
526            add         // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len-1
527            push 3      // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len 3
528            add         // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len+2
529
530            // Write all elements
531            write_mem 5 // _ *list *list+5·len+7
532
533            // Remove ram pointer
534            pop 1       // _ *list
535
536            // Increase length indicator by one
537            read_mem 1  // _ len *list-1
538            push 1 add  // _ len *list
539            swap 1      // _ *list len
540            push 1      // _ *list len 1
541            add         // _ *list len+1
542            swap 1      // _ len+1 *list
543            write_mem 1 // _ *list+1
544            pop 1       // _
545            return
546
547        // BEFORE: _ capacity
548        // AFTER:
549        tasm_list_safe_u32_new_digest:
550            // Convert capacity in number of elements to number of VM words
551            // required for that list
552            dup 0       // _ capacity capacity
553            push 5      // _ capacity capacity 5
554            mul         // _ capacity 5·capacity
555                        // _ capacity capacity_in_bfes
556            push 2      // _ capacity capacity_in_bfes 2
557            add         // _ capacity capacity_in_bfes+2
558                        // _ capacity words_to_allocate
559
560            call tasm_memory_dyn_malloc     // _ capacity *list
561
562            // Write initial length = 0 to `*list`, and capacity to `*list + 1`
563            push 0                          // _ capacity *list 0
564            swap 1                          // _ capacity 0 *list
565            write_mem 2                     // _ (*list+2)
566            push -2                         // _ (*list+2) -2
567            add                             // _ *list
568            return
569
570        tasm_arithmetic_u64_decr:
571            push -1
572            add
573            dup 0
574            push -1
575            eq
576            skiz
577                call tasm_arithmetic_u64_decr_carry
578            return
579
580        tasm_arithmetic_u64_decr_carry:
581            pop 1
582            push -1
583            add
584            dup 0
585            push -1
586            eq
587            push 0
588            eq
589            assert
590            push 4294967295
591            return
592
593        // BEFORE: _ value_hi value_lo
594        // AFTER: _ log2_floor(value)
595        tasm_arithmetic_u64_log_2_floor:
596            swap 1
597            push 1
598            dup 1
599            // _ value_lo value_hi 1 value_hi
600
601            skiz call tasm_arithmetic_u64_log_2_floor_then
602            skiz call tasm_arithmetic_u64_log_2_floor_else
603            // _ log2_floor(value)
604
605            return
606
607        tasm_arithmetic_u64_log_2_floor_then:
608            // value_hi != 0
609            // _ value_lo value_hi 1
610            swap 1
611            swap 2
612            pop 2
613            // _ value_hi
614
615            log_2_floor
616            push 32
617            add
618            // _ (log2_floor(value_hi) + 32)
619
620            push 0
621            // _ (log2_floor(value_hi) + 32) 0
622
623            return
624
625        tasm_arithmetic_u64_log_2_floor_else:
626            // value_hi == 0
627            // _ value_lo value_hi
628            pop 1
629            log_2_floor
630            return
631
632        // Before: _ *list
633        // After:  _ elem{N - 1}, elem{N - 2}, ..., elem{0}
634        tasm_list_safe_u32_pop_digest:
635            read_mem 1      // _ len *list-1
636            push 1 add      // _ len *list
637
638            // Assert that length is not 0
639            dup 1           // _ len *list len
640            push 0          // _ len *list len 0
641            eq              // _ len *list len==0
642            push 0          // _ len *list len==0 0
643            eq              // _ len *list len!=0
644            assert          // _ len *list
645
646            // Decrease length value by one and write back to memory
647            dup 1           // _ len *list len
648            push -1         // _ len *list len -1
649            add             // _ len *list len-1
650            swap 1          // _ len len-1 *list
651            write_mem 1     // _ len *list+1
652            push -1 add     // _ len *list
653
654            // Read elements
655            swap 1          // _ *list len
656            push 5          // _ *list len 5
657            mul             // _ *list 5·len
658                            // _ *list offset_for_last_element
659            add             // _ *list+offset_for_last_element
660                            // _ address_for_last_element
661            read_mem 5      // _ [elements] address_for_last_element-5
662            pop 1           // _ [elements]
663            return
664
665        // BEFORE: rhs_hi rhs_lo lhs_hi lhs_lo
666        // AFTER:  (rhs & lhs)_hi (rhs & lhs)_lo
667        tasm_arithmetic_u64_and:
668            swap 3
669            and
670            // _ lhs_lo rhs_lo (lhs_hi & rhs_hi)
671
672            swap 2
673            and
674            // _ (lhs_hi & rhs_hi) (rhs_lo & lhs_lo)
675
676            return
677
678        // BEFORE: _ value_hi value_lo
679        // AFTER: _ index_of_last_non-zero_bit
680        tasm_arithmetic_u64_index_of_last_nonzero_bit:
681            dup 1
682            dup 1
683            // _ value_hi value_lo value_hi value_lo
684
685            call tasm_arithmetic_u64_decr
686            // _ value_hi value_lo (value - 1)_hi (value - 1)_lo
687
688            push 4294967295
689            push 4294967295
690            // _ value_hi value_lo (value - 1)_hi (value - 1)_lo 0xFFFFFFFF 0xFFFFFFFF
691
692            call tasm_arithmetic_u64_xor
693            // _ value_hi value_lo ~(value - 1)_hi ~(value - 1)_lo
694
695            call tasm_arithmetic_u64_and
696            // _ (value & ~(value - 1))_hi (value & ~(value - 1))_lo
697
698            // The above value is now a power of two in u64. Calling log2_floor
699            // on this value gives us the index we are looking for.
700            call tasm_arithmetic_u64_log_2_floor
701
702            return
703
704
705        // Return a pointer to a free address and allocate `size` words for this
706        // pointer
707
708        // Before: _ size
709        // After:  _ *next_addr
710        tasm_memory_dyn_malloc:
711            push 0                     // _ size *free_pointer
712            read_mem 1                 // _ size *next_addr' *free_pointer-1
713            pop 1                      // _ size *next_addr'
714
715            // add 1 iff `next_addr` was 0, i.e. uninitialized.
716            dup 0                      // _ size *next_addr' *next_addr'
717            push 0                     // _ size *next_addr' *next_addr' 0
718            eq                         // _ size *next_addr' (*next_addr' == 0)
719            add                        // _ size *next_addr
720
721            dup 0                      // _ size *next_addr *next_addr
722            dup 2                      // _ size *next_addr *next_addr size
723
724            // Ensure that `size` does not exceed 2^32
725            split
726            swap 1
727            push 0
728            eq
729            assert
730
731            add                        // _ size *free_pointer *next_addr *(next_addr + size)
732
733            // Ensure that no more than 2^32 words are allocated, because I
734            // don't want a wrap-around in the address space
735            split
736            swap 1
737            push 0
738            eq
739            assert
740
741            swap 1                     // _ size *(next_addr + size) *next_addr
742            swap 2                     // _ *next_addr *(next_addr + size) size
743            pop 1                      // _ *next_addr *(next_addr + size)
744            push 0                     // _ *next_addr *(next_addr + size) *free_pointer
745            write_mem 1                // _ *next_addr *free_pointer+1
746            pop 1                      // _ *next_addr
747            return
748
749        // BEFORE: rhs_hi rhs_lo lhs_hi lhs_lo
750        // AFTER: (rhs ^ lhs)_hi (rhs ^ lhs)_lo
751        tasm_arithmetic_u64_xor:
752            swap 3
753            xor
754            // _ lhs_lo rhs_lo (lhs_hi ^ rhs_hi)
755
756            swap 2
757            xor
758            // _ (lhs_hi ^ rhs_hi) (rhs_lo ^ lhs_lo)
759
760            return
761    )
762}