Runtime.MemoryCopyRoutine

1module Runtime.MemoryCopyRoutine
2
3import Data.Bytes
4
5-- Forward byte copy between caller-owned live ranges. Length zero performs no
6-- memory access; overlapping ranges are not a memmove contract. The target's
7-- step loads and stores one byte, advances both pointers and decrements the
8-- 64-bit count. The shared loop tests the full count and returns status zero.
9-- No allocation, IO or implicit extent admission occurs in this primitive.
10def nativeMemoryRoutineLabelEntry : Bytes =
11  b"mem-entry"
12
13def nativeMemoryRoutineLabelLoop : Bytes =
14  b"mem-loop"
15
16def nativeMemoryRoutineLabelDone : Bytes =
17  b"mem-done"
18
19def memoryCopyAssemblyFor =
20  (lambda erased A : Type 0 .
21    (lambda unrestricted step : (pi unrestricted tail : A . A) .
22      (lambda unrestricted testCount : (pi unrestricted tail : A . A) .
23        (lambda unrestricted jumpZero : (pi unrestricted label : Bytes . (pi unrestricted tail : A . A)) .
24          (lambda unrestricted jumpNotZero : (pi unrestricted label : Bytes . (pi unrestricted tail : A . A)) .
25            (lambda unrestricted label : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A)) .
26              (lambda unrestricted returnZero : (pi unrestricted tail : A . A) .
27                (lambda unrestricted end : A .
28                  (label
29                    nativeMemoryRoutineLabelEntry
30                    (testCount
31                      (jumpZero
32                        nativeMemoryRoutineLabelDone
33                        (label
34                          nativeMemoryRoutineLabelLoop
35                          (step
36                            (testCount
37                              (jumpNotZero
38                                nativeMemoryRoutineLabelLoop
39                                (label nativeMemoryRoutineLabelDone (returnZero end)))))))))))))))))