LEB128, the variable-length encoding the interface cache uses: seven bits
per byte, low group first, the high bit meaning "more follows". Five groups
cover every value a 32-bit quantity can hold, and the encoding is canonical
because groups stop as soon as the remainder is zero.
59def stdCodecEncodeVarint =
60 (lambda unrestricted value : Nat .
61 (let unrestricted group0 =
62 (naturalModuloUnchecked value stdCodecVarintBase)
63 in
64 (let unrestricted rest0 =
65 (naturalDivideUnchecked value stdCodecVarintBase)
66 in
67 (eliminate
68 StdBool
69 (lambda unrestricted current : (family StdBool) . Bytes)
70 (stdBoolFromNatural rest0)
71 -- more groups follow: set the continuation bit on this one
72 (branch
73 StdTrue
74 .
75 (bytes-cons
76 (nat-to-byte (naturalAdd group0 stdCodecVarintBase))
77 (let unrestricted group1 =
78 (naturalModuloUnchecked rest0 stdCodecVarintBase)
79 in
80 (let unrestricted rest1 =
81 (naturalDivideUnchecked rest0 stdCodecVarintBase)
82 in
83 (eliminate
84 StdBool
85 (lambda unrestricted current : (family StdBool) . Bytes)
86 (stdBoolFromNatural rest1)
87 (branch
88 StdTrue
89 .
90 (bytes-cons
91 (nat-to-byte (naturalAdd group1 stdCodecVarintBase))
92 (let unrestricted group2 =
93 (naturalModuloUnchecked rest1 stdCodecVarintBase)
94 in
95 (let unrestricted rest2 =
96 (naturalDivideUnchecked rest1 stdCodecVarintBase)
97 in
98 (eliminate
99 StdBool
100 (lambda unrestricted current : (family StdBool) . Bytes)
101 (stdBoolFromNatural rest2)
102 (branch
103 StdTrue
104 .
105 (bytes-cons
106 (nat-to-byte (naturalAdd group2 stdCodecVarintBase))
107 (bytes-cons
108 (nat-to-byte (naturalModuloUnchecked rest2 stdCodecVarintBase))
109 b"")))
110 (branch StdFalse . (bytes-cons (nat-to-byte group2) b"")))))))
111 (branch StdFalse . (bytes-cons (nat-to-byte group1) b"")))))))
112 (branch StdFalse . (bytes-cons (nat-to-byte group0) b""))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.