miden-protocol 0.14.5

Core components of the Miden protocol
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
use miden::core::word
use $kernel::memory

# A link map is a map data structure based on a sorted linked list.
#
# # Basics & Terminology
#
# The entries in the list are sorted by their keys. The order is defined by comparing the
# individual felts of the word from most significant (the top element on a word laid out on the
# stack) to least significant.
#
# A link map is identified by a pointer called the map_ptr. The map_ptr points to a single field
# element which is the head of the map, i.e. the first element in the map with the smallest key.
# The value at the map_ptr is an entry_ptr, which points to a concrete entry of the map.
#
# The map_ptr is a double pointer, i.e. it takes two dereference operations to end up at the head
# entry of the map. This has the following properties:
# - A link map does not need any initialization. If a map_ptr is uninitialized mem_load returns 0,
#   which is interpreted as an empty map.
# - It is simple to update the head of the map simply by setting *map_ptr = entry_ptr, where
#   entry_ptr is the new head entry of the map.
#
# # Layout
#
# The layout of a link map _conceptually_ looks like this:
#
# [
#   (map_ptr, prev_entry_ptr, next_entry_ptr, 0, KEY, VALUE0, VALUE1),
#   (map_ptr, prev_entry_ptr, next_entry_ptr, 0, KEY, VALUE0, VALUE1),
#   ...
# ]
#
# where:
# - KEY and VALUE{0,1} are the user-provided data and all are of size word.
# - the first word is the METADATA of the entry.
# - the map_ptr is the pointer of the map to which this entry belongs. See the security section
#   for the rationale.
# - the prev_entry_ptr is an entry pointer that points to the previous item in the list whose key
#   is smaller than the entry's KEY.
# - the next_entry_ptr is an entry pointer that points to the next item in the list whose key is
#   greater than the entry's KEY.
# - the fourth element in the entry metadata is currently unused.
#
# Each entry takes up 4 words or 16 field elements of memory. Note that the above layout is not
# how the map is laid out in memory, since entries are not guaranteed to be contiguous in memory.
#
# # Memory Allocation
#
# A link map can be grown dynamically without the need to specify the number of entries upfront.
# This works by statically allocating a large chunk of dedicated link map memory in the kernel and
# then allocating entry by entry on demand.
#
# Multiple link map's entries can be allocated from that same region of memory, which avoids
# having to split up this chunk into smaller chunks per map, which would impose more limitations
# on the overall system.
#
# # Security
#
# The in-VM link map works closely together with a link map part of the VM host. For set
# operations this means the host does the expensive iteration to find the place where a key-value
# pair must be inserted or updated. Similarly for get operations. The host will either find the
# requested key-value pair or provide the entry at which the pair would reside if it was present
# in the map to prove its absence. The link map in the VM will assert that what the host
# provided is correct.
#
# Because the host cannot be trusted, the link map in the VM must assert a couple of things.
#
# ## Entry Pointer Validity
#
# The first of these is basic entry pointer validity. Both in set and get operations, the host
# provides entry pointers. It is important that the host cannot provide a pointer to an arbitrary
# memory location, otherwise the VM might read or write to those locations and produce incorrect
# results.
#
# Each map entry is allocated from a dedicated range of memory. That way, it is simple to assert
# that a host-provided entry_ptr lies within that range. That ensures that no other piece of
# memory can be abused as an entry. Moreover, each entry takes up exactly four words, so each
# entry pointer can be checked for entry-alignment. Finally, because entries from _different_ link
# maps are allocated from the same memory region means it would still be possible for a host to
# provide an entry pointer from map 1 to an operation in map 2. To avoid this, each entry is
# tagged using the map_ptr. Every operation on a map_ptr asserts that the entry's map_ptr tag
# matches it.
#
# ## Set Operation
#
# During a set operation, the host is asked where the provided key-value pair should be inserted
# or updated. The host can respond with three different values:
# - Update = 0
#   - Means the key already exists in the map and requires validating that the host-provided entry
#     pointer's key matches the one that is being set.
# - InsertAtHead = 1
#   - Means the key should be inserted at the head of the list. This requires validating that the
#     key that is being inserted is less than current head entry's key.
# - InsertAfterEntry = 2
#   - Means the key should be inserted after the entry that the host provided. This requires
#     validating that the key that is being inserted is greater than the host-provided entry's
#     key. If the host-provided entry has a next entry, then the key that is being inserted must
#     be less than the next entry's key.
#
# ## Get Operation
#
# During a get operation, the host is asked where the requested key-value pair is located, or if
# it does not exist, where its absence can be asserted. Similarly to the set operation, the host
# can respond with three different values:
# - Found = 0
#   - Means the key was found and requires validating that the host-provided entry pointer's key
#     matches the requested one.
# - AbsentAtHead = 1
#   - Means the key would be at the head of the map, if it was present in the map. This requires
#     validating that the requested key is smaller than the current head's key to validate the
#     absence claim.
# - AbsentAfterEntry = 2
#   - Means the key would be after the entry that the host provided, if it was present in the map.
#     This requires validating that the requested key is greater than the host-provided entry's
#     key. If the host-provided entry has a next entry, then the requested key must also be less
#     than the next entry's key to validate the absence claim.

# ERRORS
# =================================================================================================

const ERR_LINK_MAP_EMPTY_MAP_REQUIRES_AT_HEAD_OPERATION="empty map requires operation InsertAtHead for set or AbsentAtHead for get"

const ERR_LINK_MAP_PROVIDED_KEY_NOT_EQUAL_TO_ENTRY_KEY="provided key does not match key in map entry"

const ERR_LINK_MAP_PROVIDED_KEY_NOT_GREATER_THAN_ENTRY_KEY="provided key is not greater than the entry key"

const ERR_LINK_MAP_PROVIDED_KEY_NOT_LESS_THAN_ENTRY_KEY="provided key is not less than the entry key"

const ERR_LINK_MAP_ENTRY_PTR_IS_OUTSIDE_VALID_MEMORY_REGION="host-provided entry ptr is outside the valid memory region"

const ERR_LINK_MAP_ENTRY_PTR_IS_NOT_ENTRY_ALIGNED="host-provided entry ptr is not 'link map entry'-aligned"

const ERR_LINK_MAP_MAP_PTR_IN_ENTRY_DOES_NOT_MATCH_EXPECTED_MAP_PTR="map ptr stored in host-provided entry does not match actual pointer of the map"

# CONSTANTS
# =================================================================================================

# The offset of the prev_entry_ptr in an entry's metadata.
const PREV_ENTRY_PTR_OFFSET=1

# The offset of the next_entry_ptr in an entry's metadata.
const NEXT_ENTRY_PTR_OFFSET=2

# The offset of the KEY in an entry.
const KEY_OFFSET=4

# The offset of the VALUE0 in an entry.
const VALUE0_OFFSET=8

# The offset of the VALUE1 in an entry.
const VALUE1_OFFSET=12

# The value of the Update operation for a set event.
const INSERT_OPERATION_UPDATE=0

# The value of the InsertAtHead operation for a set event.
const INSERT_OPERATION_AT_HEAD=1

# The value of the Found operation for a get event.
const GET_OPERATION_FOUND=0

# The value of the AbsentAtHead operation for a get event.
const GET_OPERATION_ABSENT_AT_HEAD=1

# EVENTS
# =================================================================================================

# Event emitted when an entry is set.
const LINK_MAP_SET_EVENT=event("miden::protocol::link_map::set")

# Event emitted when an entry is fetched.
const LINK_MAP_GET_EVENT=event("miden::protocol::link_map::get")

# LINK MAP PROCEDURES
# =================================================================================================

# PUBLIC API
# -------------------------------------------------------------------------------------------------

#! Inserts the specified key-value pair into the map, or updates the existing key if the pair
#! already exists.
#!
#! Note that unlike smt::set, passing VALUE{0,1} = EMPTY_WORD does not mean removal of the entry.
#!
#! Inputs:  [map_ptr, KEY, VALUE0, VALUE1]
#! Outputs: [is_new_key]
#!
#! Where:
#! - map_ptr is the pointer to the map.
#! - KEY is the key that will be set in the map.
#! - VALUE0 and VALUE1 are the values that will be set under KEY.
#! - is_new_key is a boolean indicating whether the KEY and its values were newly inserted into the
#!   map or not. That is:
#!   - If the map did not previously contain the KEY, 1 is returned.
#!   - If the map already contained the KEY, 0 is returned.
#!
#! Panics if:
#! - the host provides faulty advice. See panic sections of assert_entry_ptr_is_valid,
#!   update_entry, insert_at_head, insert_after_entry and assert_empty_map_op_is_at_head.
pub proc set
    emit.LINK_MAP_SET_EVENT
    adv_push.2
    # => [operation, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

    dup eq.INSERT_OPERATION_UPDATE swap eq.INSERT_OPERATION_AT_HEAD
    # => [is_insert_at_head_op, is_insert_update_op, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

    dup dup.4
    # => [map_ptr, is_insert_at_head_op, is_insert_at_head_op, is_insert_update_op, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

    exec.assert_empty_map_op_is_at_head
    # => [is_insert_at_head_op, is_insert_update_op, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

    if.true
        # drop is_insert_update_op and the unvalidated entry ptr since we can load the entry ptr
        # at the head of the map securely from map_ptr
        drop drop
        # => [map_ptr, KEY, VALUE0, VALUE1]

        exec.insert_at_head
        # => []

        push.1
        # => [is_new_key]
    else
        # => [is_insert_update_op, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

        dup.2 dup.2
        # => [entry_ptr, map_ptr, is_insert_update_op, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

        # validate the entry pointer
        # this can be skipped for insert_at_head because the entry_ptr is not used in that branch
        exec.assert_entry_ptr_is_valid
        # => [is_insert_update_op, entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

        # note: the is_new_key flag logic is duplicated rather than appended after the if-else branch
        # to avoid introducing an extra MAST node
        if.true
            # update existing entry
            # drop unused map_ptr
            swap drop
            # => [entry_ptr, KEY, VALUE0, VALUE1]

            exec.update_entry
            # => []

            push.0
            # => [is_new_key]
        else
            # insert after existing entry
            exec.insert_after_entry
            # => []

            push.1
            # => [is_new_key]
        end
    end
end

#! Returns the VALUE located at KEY in the given map.
#!
#! Inputs:  [map_ptr, KEY]
#! Outputs: [contains_key, VALUE0, VALUE1]
#!
#! Where:
#! - map_ptr is the pointer to the map.
#! - KEY is the key that will be fetched from the map.
#! - contains_key is a boolean indicating whether the map contained the KEY or not.
#! - VALUE0 and VALUE1 are the values fetched from the map. Both values are guaranteed to be an
#!   EMPTY_WORD if the map did not contain the key.
#!
#! Panics if:
#! - the host provides faulty advice. See panic sections of assert_entry_ptr_is_valid,
#!   get_existing_value, assert_absent_at_head, assert_absent_after_entry and
#!   assert_empty_map_op_is_at_head.
pub proc get
    emit.LINK_MAP_GET_EVENT
    adv_push.2
    # => [get_operation, entry_ptr, map_ptr, KEY]

    dup eq.GET_OPERATION_FOUND swap eq.GET_OPERATION_ABSENT_AT_HEAD
    # => [is_absent_at_head, is_found, entry_ptr, map_ptr, KEY]

    dup dup.4
    # => [map_ptr, is_absent_at_head, is_absent_at_head, is_found, entry_ptr, map_ptr, KEY]

    exec.assert_empty_map_op_is_at_head
    # => [is_absent_at_head, is_found, entry_ptr, map_ptr, KEY]

    if.true
        # drop is_found and the unvalidated entry ptr since we can load the entry ptr
        # at the head of the map securely from map_ptr
        drop drop
        # => [map_ptr, KEY]

        exec.assert_absent_at_head
        # => []

        padw padw push.0
        # => [contains_key, EMPTY_WORD, EMPTY_WORD]
    else
        # => [is_found, entry_ptr, map_ptr, KEY]

        dup.2 dup.2
        # => [entry_ptr, map_ptr, is_found, entry_ptr, map_ptr, KEY]

        # validate the entry pointer
        # this can be skipped for assert_absent_at_head because the entry_ptr is not used in that
        # branch
        exec.assert_entry_ptr_is_valid
        # => [is_found, entry_ptr, map_ptr, KEY]

        # drop unused map_ptr
        movup.2 drop
        # => [is_found, entry_ptr, KEY]

        # note: the flag and empty word logic is duplicated rather than appended after the if-else
        # branch to avoid introducing an extra MAST node
        if.true
            # => [entry_ptr, KEY]

            exec.get_existing_value
            # => [VALUE0, VALUE1]

            push.1
            # => [contains_key, VALUE0, VALUE1]
        else
            # => [entry_ptr, KEY]

            exec.assert_absent_after_entry
            # => []

            padw padw push.0
            # => [contains_key, EMPTY_WORD, EMPTY_WORD]
        end
    end
end

#! Returns true if the list is empty, i.e. map ptr points to a 0 entry_ptr, false otherwise.
#!
#! Inputs:  [map_ptr]
#! Outputs: [is_empty]
pub proc is_empty
    mem_load eq.0
end

#! Initializes an iterator over the provided link map.
#!
#! The returned iter can be passed to the link_map::next_key_* procedures to advance the iterator.
#!
#! Inputs:  [map_ptr]
#! Outputs: [has_next, iter]
pub proc iter
    exec.get_head
    # => [entry_ptr]

    # a next item exists if the entry_ptr does not point to 0
    dup neq.0
    # => [has_next, entry_ptr]
end

#! Returns the item at the current iterator entry and advances the iterator to the next entry.
#!
#! The iter can be obtained by link_map::iter.
#!
#! The returned next_iter can be passed to the next call to a link_map::next_key_* procedure if
#! has_next = true.
#!
#! Once has_next = false has been returned, the next_key_* procedures should not be called again.
#! The behavior of calling it again with the returned next_iter is undefined.
#!
#! Inputs:  [iter]
#! Outputs: [KEY, VALUE0, VALUE1, has_next, next_iter]
pub proc next_key_double_value
    dup exec.next_key
    # => [KEY, has_next, next_entry_ptr, entry_ptr = iter]

    movup.6 exec.get_values
    # => [VALUE0, VALUE1, KEY, has_next, next_entry_ptr]

    movupw.2
    # => [KEY, VALUE0, VALUE1, has_next, next_iter = next_entry_ptr]
end

#! Returns the key at the current iterator entry and advances the iterator to the next entry.
#!
#! This is the same as link_map::next_key_double_value but does not return VALUE1. See its docs
#! for important details.
#!
#! Inputs:  [iter]
#! Outputs: [KEY, VALUE0, has_next, next_iter]
pub proc next_key_value
    dup exec.next_key
    # => [KEY, has_next, next_entry_ptr, entry_ptr = iter]

    movup.6 exec.get_value0
    # => [VALUE0, KEY, has_next, next_entry_ptr]

    swapw
    # => [KEY, VALUE0, has_next, next_entry_ptr]
end

#! Returns the key at the current iterator entry and advances the iterator to the next entry.
#!
#! This is the same as link_map::next_key_double_value but does not return the values. See its docs
#! for important details.
#!
#! Inputs:  [iter]
#! Outputs: [KEY, has_next, next_iter]
pub proc next_key
    dup exec.get_next_entry_ptr
    # => [next_entry_ptr, entry_ptr = iter]

    dup neq.0
    # => [has_next, next_entry_ptr, entry_ptr]

    movup.2 exec.get_key
    # => [KEY, has_next, next_iter = next_entry_ptr]
end

# SET HELPERS
# -------------------------------------------------------------------------------------------------

#! Inserts the key-value pair at the head of the map.
#!
#! Inputs:  [map_ptr, KEY, VALUE0, VALUE1]
#! Outputs: []
#!
#! Panics if:
#! - the KEY is not less than the key in the head of the map, unless the map is empty.
proc insert_at_head
    exec.memory::link_map_malloc
    # => [entry_ptr, map_ptr, KEY, VALUE0, VALUE1]

    dup movdn.14
    # => [entry_ptr, map_ptr, KEY, VALUE0, VALUE1, entry_ptr]

    dup.1 movdn.14
    # => [entry_ptr, map_ptr, KEY, VALUE0, VALUE1, map_ptr, entry_ptr]

    exec.insert_pair
    # => [map_ptr, entry_ptr]

    dup exec.is_empty not
    # => [is_non_empty, map_ptr, entry_ptr]

    # if the link map was not previously empty, then the previous head must be updated to point back
    # to the newly inserted entry
    if.true
        dup.1
        # => [entry_ptr, map_ptr, entry_ptr]

        dup.1 exec.get_head
        # => [current_head_entry_ptr, entry_ptr, map_ptr, entry_ptr]

        # assert that entry_ptr.key < current_head_entry_ptr.key
        dup.1 exec.get_key
        # => [ENTRY_KEY, current_head_entry_ptr, entry_ptr, map_ptr, entry_ptr]

        dup.4
        # => [current_head_entry_ptr, ENTRY_KEY, current_head_entry_ptr, entry_ptr, map_ptr, entry_ptr]

        exec.assert_key_is_less
        # => [current_head_entry_ptr, entry_ptr, map_ptr, entry_ptr]

        dup movdn.2
        # => [current_head_entry_ptr, entry_ptr, current_head_entry_ptr, map_ptr, entry_ptr]

        # set current_head_entry_ptr.prev_entry_ptr = entry_ptr
        exec.set_prev_entry_ptr
        # => [current_head_entry_ptr, map_ptr, entry_ptr]

        # set entry_ptr.next_entry_ptr = current_head_entry_ptr
        dup.2 exec.set_next_entry_ptr
        # => [map_ptr, entry_ptr]
    end

    # update the current head of the map to the newly inserted entry
    exec.set_head
    # => []
end

#! Updates the VALUE0 in the given entry.
#!
#! Inputs:  [entry_ptr, KEY, VALUE0, VALUE1]
#! Outputs: []
#!
#! Panics if:
#! - the key in the entry does not match the provided KEY.
proc update_entry
    dup movdn.5
    # => [entry_ptr, KEY, entry_ptr, VALUE0, VALUE1]

    exec.assert_key_is_equal
    # => [entry_ptr, VALUE0, VALUE1]

    exec.set_value
    # => []
end

#! Inserts the key value pair as the next entry after the prev_entry_ptr.
#!
#! Inputs:  [prev_entry_ptr, map_ptr, KEY, VALUE0, VALUE1]
#! Outputs: []
#!
#! Panics if:
#! - the KEY is not greater than the key in the prev entry.
#! - the KEY is not less than the key in prev_entry.next_entry, unless the prev entry is the last
#!   one in the map.
proc insert_after_entry
    movdn.5
    # => [map_ptr, KEY, prev_entry_ptr, VALUE0, VALUE1]

    movdn.5
    # => [KEY, prev_entry_ptr, map_ptr, VALUE0, VALUE1]

    dupw dup.8
    # => [prev_entry_ptr, KEY, KEY, prev_entry_ptr, map_ptr, VALUE0]

    exec.assert_key_is_greater
    # => [KEY, prev_entry_ptr, map_ptr, VALUE0, VALUE1]

    movup.4 movdn.13
    # => [KEY, map_ptr, VALUE0, VALUE1, prev_entry_ptr]

    movup.4
    # => [map_ptr, KEY, VALUE0, VALUE1, prev_entry_ptr]

    exec.memory::link_map_malloc
    # => [entry_ptr, map_ptr, KEY, VALUE0, VALUE1, prev_entry_ptr]

    dup movdn.14
    # => [entry_ptr, map_ptr, KEY, VALUE0, VALUE1, entry_ptr, prev_entry_ptr]

    exec.insert_pair
    # => [entry_ptr, prev_entry_ptr]

    dup.1 exec.get_next_entry_ptr movdn.2
    # => [entry_ptr, prev_entry_ptr, next_entry_ptr]

    dup dup.2
    # => [prev_entry_ptr, entry_ptr, entry_ptr, prev_entry_ptr, next_entry_ptr]

    # set prev_entry_ptr.next_entry_ptr = entry_ptr
    exec.set_next_entry_ptr
    # => [entry_ptr, prev_entry_ptr, next_entry_ptr]

    dup movdn.3
    # => [entry_ptr, prev_entry_ptr, next_entry_ptr, entry_ptr]

    # set entry_ptr.prev_entry = prev_entry_ptr
    exec.set_prev_entry_ptr
    # => [entry_ptr, next_entry_ptr, entry_ptr]

    dup eq.0 not
    # => [has_next_entry, next_entry_ptr, entry_ptr]

    if.true
        dup.1 exec.get_key
        # => [KEY, next_entry_ptr, entry_ptr]

        dup.4
        # => [next_entry_ptr, KEY, next_entry_ptr, entry_ptr]

        # assert KEY < next_entry.key
        exec.assert_key_is_less
        # => [next_entry_ptr, entry_ptr]

        dup dup.2
        # => [entry_ptr, next_entry_ptr, next_entry_ptr, entry_ptr]

        # set entry_ptr.next_entry_ptr = next_entry
        exec.set_next_entry_ptr
        # => [next_entry_ptr, entry_ptr]

        # set next_entry.prev_entry_ptr = entry_ptr
        exec.set_prev_entry_ptr
        # => []

    else
        # remove unneeded stack elements
        drop drop
        # => []
    end
    # => []
end

#! Inserts the key, value into the entry pointer and sets the map ptr to the provided value.
#!
#! Inputs:  [entry_ptr, map_ptr, KEY, VALUE0, VALUE1]
#! Outputs: []
proc insert_pair
    swap dup.1
    # => [entry_ptr, map_ptr, entry_ptr, KEY, VALUE0, VALUE1]

    exec.set_map_ptr
    # => [entry_ptr, KEY, VALUE0, VALUE1]

    dup movdn.5
    # => [entry_ptr, KEY, entry_ptr, VALUE0, VALUE1]

    exec.set_key
    # => [entry_ptr, VALUE0, VALUE1]

    exec.set_value
    # => []
end

# GET HELPERS
# -------------------------------------------------------------------------------------------------

#! Asserts that the provided KEY is absent at the head of the link map.
#!
#! An invariant of the link map is that its entries are sorted and since there is no previous
#! entry for the head, this proves that the KEY is absent from the map.
#!
#! Inputs:  [map_ptr, KEY]
#! Outputs: []
#!
#! Panics if:
#! - the KEY is not less than the key in the head of the map, unless the map is empty.
proc assert_absent_at_head
    dup exec.is_empty
    # => [is_empty, map_ptr, KEY]

    if.true
        # in an empty list, any KEY is absent at the head, so there's nothing further to assert
        drop dropw
        # => []
    else
        exec.get_head
        # => [entry_ptr, KEY]

        # assert that KEY is less than the current head's key
        exec.assert_key_is_less
        # => []
    end
end

#! Asserts that the provided KEY is absent after the provided entry.
#!
#! If KEY is greater than the key in the entry and less than the key in entry's next entry, then
#! that proves the absence of the key.
#!
#! Inputs:  [entry_ptr, KEY]
#! Outputs: []
#!
#! Panics if:
#! - the KEY is not greater than the key in the entry.
#! - the KEY is not less than the key in entry.next_entry, unless the entry is the last one in the map.
proc assert_absent_after_entry
    movdn.4 dupw
    # => [KEY, KEY, entry_ptr]

    dup.8
    # => [entry_ptr, KEY, KEY, entry_ptr]

    # assert that KEY is greater than the entry's key
    exec.assert_key_is_greater
    # => [KEY, entry_ptr]

    movup.4 exec.get_next_entry_ptr
    # => [next_entry_ptr, KEY]

    dup eq.0
    # => [is_last_entry, next_entry_ptr, KEY]

    if.true
        # nothing further to assert
        drop dropw
        # => []
    else
        # if there is a next entry, then the KEY must be less than next entry's key
        exec.assert_key_is_less
        # => []
    end
    # => []
end

#! Fetches VALUE0 and VALUE1 at the provided KEY from the provided entry.
#!
#! Inputs:  [entry_ptr, KEY]
#! Outputs: [VALUE0, VALUE1]
#!
#! Panics if:
#! - the key in the entry does not match KEY.
proc get_existing_value
    movdn.4 dup.4
    # => [entry_ptr, KEY, entry_ptr]

    exec.assert_key_is_equal
    # => [entry_ptr]

    exec.get_values
    # => [VALUE0, VALUE1]
end

# HELPERS
# -------------------------------------------------------------------------------------------------

#! Returns true if the entry at the given ptr has a non-null ptr to a next entry.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [has_next]
proc has_next
    exec.get_next_entry_ptr eq.0 not
end

#! Sets the next_entry ptr of the entry to the provided value.
#!
#! Inputs:  [entry_ptr, next_entry_ptr]
#! Outputs: []
proc set_next_entry_ptr
    add.NEXT_ENTRY_PTR_OFFSET mem_store
    # => []
end

#! Returns the value of the next_entry pointer in the provided entry pointer.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [next_entry_ptr]
proc get_next_entry_ptr
    add.NEXT_ENTRY_PTR_OFFSET mem_load
    # => [next_entry_ptr]
end

#! Sets the prev_entry ptr of the entry to the provided value.
#!
#! Inputs:  [entry_ptr, prev_entry_ptr]
#! Outputs: []
proc set_prev_entry_ptr
    add.PREV_ENTRY_PTR_OFFSET mem_store
    # => []
end

#! Sets the value of the entry pointer.
#!
#! Inputs:  [entry_ptr, VALUE0, VALUE1]
#! Outputs: []
proc set_value
    dup movdn.5
    # => [entry_ptr, VALUE0, entry_ptr, VALUE1]

    add.VALUE0_OFFSET mem_storew_le dropw
    # => [entry_ptr, VALUE1]

    add.VALUE1_OFFSET mem_storew_le dropw
    # => []
end

#! Returns the values of the entry pointer.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [VALUE0, VALUE1]
proc get_values
    dup exec.get_value1
    # => [VALUE1, entry_ptr]

    movup.4 exec.get_value0
    # => [VALUE0, VALUE1]
end

#! Returns VALUE0 of the entry pointer.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [VALUE0]
proc get_value0
    padw movup.4
    # => [entry_ptr, pad(4)]

    add.VALUE0_OFFSET mem_loadw_le
    # => [VALUE0]
end

#! Returns VALUE1 of the entry pointer.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [VALUE1]
proc get_value1
    padw movup.4
    # => [entry_ptr, pad(4)]

    add.VALUE1_OFFSET mem_loadw_le
    # => [VALUE1]
end

#! Sets the key of the entry pointer.
#!
#! Inputs:  [entry_ptr, KEY]
#! Outputs: []
proc set_key
    add.KEY_OFFSET mem_storew_le dropw
end

#! Returns the key of the entry pointer.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [KEY]
proc get_key
    padw movup.4
    # => [entry_ptr, pad(4)]

    add.KEY_OFFSET mem_loadw_le
    # => [KEY]
end

#! Sets the entry ptr as the head of the linked list.
#!
#! Inputs:  [map_ptr, entry_ptr]
#! Outputs: []
proc set_head
    mem_store
end

#! Returns the entry ptr at the head of the linked list.
#!
#! Inputs:  [map_ptr]
#! Outputs: [entry_ptr]
proc get_head
    mem_load
end

#! Sets the map ptr of the entry pointer.
#!
#! Inputs:  [entry_ptr, map_ptr]
#! Outputs: []
proc set_map_ptr
    mem_store
end

#! Returns the map ptr of the entry pointer.
#!
#! Inputs:  [entry_ptr]
#! Outputs: [map_ptr]
proc get_map_ptr
    mem_load
end

# ASSERTIONS
# -------------------------------------------------------------------------------------------------

#! Asserts that the KEY is equal to the key in the entry.
#!
#! Inputs:  [entry_ptr, KEY]
#! Outputs: []
proc assert_key_is_equal
    exec.get_key swapw
    # => [KEY, ENTRY_KEY]

    assert_eqw.err=ERR_LINK_MAP_PROVIDED_KEY_NOT_EQUAL_TO_ENTRY_KEY
    # => []
end

#! Asserts that the KEY is greater than the key in the entry pointer.
#!
#! Inputs:  [entry_ptr, KEY]
#! Outputs: []
proc assert_key_is_greater
    exec.get_key
    # => [ENTRY_KEY, KEY]

    exec.word::gt assert.err=ERR_LINK_MAP_PROVIDED_KEY_NOT_GREATER_THAN_ENTRY_KEY
end

#! Asserts that the KEY is less than the key in the entry pointer.
#!
#! Inputs:  [entry_ptr, KEY]
#! Outputs: []
proc assert_key_is_less
    exec.get_key
    # => [ENTRY_KEY, KEY]

    exec.word::lt assert.err=ERR_LINK_MAP_PROVIDED_KEY_NOT_LESS_THAN_ENTRY_KEY
    # => []
end

#! Asserts that if the map is empty, the host-provided operation is the `*AT_HEAD` variant:
#! - INSERT_OPERATION_AT_HEAD for link_map::set
#! - GET_OPERATION_ABSENT_AT_HEAD for link_map::get
#!
#! This ensures the other operations never have to consider the empty map case to reduce
#! complexity.
#!
#! What we want is:
#! is_empty_map | !is_at_head_op | outcome
#! true         | true           | panic
#! true         | false          | ok
#! false        | true           | ok
#! false        | false          | ok
#!
#! Inputs:  [map_ptr, is_at_head_op]
#! Outputs: []
#!
#! Panics if:
#! - the map is empty and the provided operation is not the *AT_HEAD variant.
proc assert_empty_map_op_is_at_head
    exec.is_empty
    # => [is_empty_map, is_at_head_op]

    swap not
    # => [!is_at_head_op, is_empty_map]

    and assertz.err=ERR_LINK_MAP_EMPTY_MAP_REQUIRES_AT_HEAD_OPERATION
    # => []
end

#! Asserts that the given entry ptr is a valid entry in the map identified by map_ptr.
#!
#! Inputs:  [entry_ptr, map_ptr]
#! Outputs: []
#!
#! Panics if:
#! - any of the following conditions is false:
#!   - LINK_MAP_MEMORY_START_PTR <= entry_ptr < LINK_MAP_MEMORY_END_PTR.
#!   - entry ptr is "link map entry"-aligned, i.e. entry_ptr % LINK_MAP_ENTRY_SIZE == 0. This
#!     works because every entry ptr is a multiple of LINK_MAP_ENTRY_SIZE.
#!   - entry's map ptr is equal to the given map_ptr.
proc assert_entry_ptr_is_valid
    # Check entry pointer is in valid memory range.
    # -------------------------------------------------------------------------------------------------

    # memory pointers must fit into a u32
    # this enables us to use the more efficient u32lt(e) instructions.
    u32assert.err=ERR_LINK_MAP_ENTRY_PTR_IS_OUTSIDE_VALID_MEMORY_REGION
    # => [entry_ptr, map_ptr]

    exec.memory::get_link_map_region_start_ptr dup.1
    # => [entry_ptr, region_start_ptr, entry_ptr, map_ptr]

    # compute region_start_ptr <= entry_ptr
    # region_start_ptr is guaranteed to be a u32
    u32lte
    # => [is_entry_ptr_gt_start, entry_ptr, map_ptr]

    dup.1 exec.memory::get_link_map_region_end_ptr
    # => [region_end_ptr, entry_ptr, is_entry_ptr_gt_start, entry_ptr, map_ptr]

    # compute entry_ptr < region_end_ptr
    # region_end_ptr is guaranteed to be a u32
    u32lt and
    # => [is_entry_ptr_in_valid_range, entry_ptr, map_ptr]

    assert.err=ERR_LINK_MAP_ENTRY_PTR_IS_OUTSIDE_VALID_MEMORY_REGION
    # => [entry_ptr, map_ptr]

    # Check that the entry pointer is aligned to link map entries.
    # -------------------------------------------------------------------------------------------------

    # Because LINK_MAP_MEMORY_START_PTR is chosen as a multiple of LINK_MAP_ENTRY_SIZE
    # any valid entry pointer is a multiple of LINK_MAP_ENTRY_SIZE. So to check validity,
    # we assert that entry_ptr % LINK_MAP_ENTRY_SIZE == 0.
    # note: we previously asserted that entry_ptr fits in a u32
    dup exec.memory::get_link_map_entry_size u32mod eq.0
    # => [is_entry_ptr_aligned, entry_ptr, map_ptr]

    assert.err=ERR_LINK_MAP_ENTRY_PTR_IS_NOT_ENTRY_ALIGNED
    # => [entry_ptr, map_ptr]

    # Check entry pointer's map ptr is equal to map_ptr.
    # -------------------------------------------------------------------------------------------------

    # check if entry_ptr.map_ptr == map_ptr
    exec.get_map_ptr eq
    # => [entry_contains_map_ptr]

    assert.err=ERR_LINK_MAP_MAP_PTR_IN_ENTRY_DOES_NOT_MATCH_EXPECTED_MAP_PTR
    # => []
end