Std.Codec

1module Std.Codec
2
3import Std.Foundation
4import Std.List
5import Std.Natural
6
7-- Codecs (Language Platform PRD §28.2 Hash/codec, LP-804).
8--
9-- Fixed-width and variable-length encodings with BOUNDED decoders: every
10-- decoder here answers with what it read and what is left, and a decoder that
11-- runs out of input answers that it did, rather than failing or reading past
12-- the end. Encodings are little-endian and canonical: one value has exactly
13-- one encoding, so equal values have equal bytes and a digest over them means
14-- something.
15-- What a decoder answers: the value and the remaining input, or the fact that
16-- the input ended too soon.
17family StdDecoded : Type 0
18parameter erased stdDecodedValueType : Type 0
19constructor StdDecodedValue
20field unrestricted stdDecodedItem : stdDecodedValueType
21field unrestricted stdDecodedRest : Bytes
22constructor StdDecodedTruncated
23
24end-family
25
26-- 256, the base of a byte, written once.
27def stdCodecByteBase =
28  (succ (byte-to-nat (byte 255)))
29
30-- 128, the base of a LEB128 group.
31def stdCodecVarintBase =
32  (byte-to-nat (byte 128))
33
34-- The low byte of a natural.
35def stdCodecLowByte =
36  (lambda unrestricted value : Nat . (nat-to-byte (naturalModuloUnchecked value stdCodecByteBase)))
37
38-- One byte, encoded.
39def stdCodecEncodeByte =
40  (lambda unrestricted value : Byte . (bytes-cons value b""))
41
42-- One byte, decoded, with the rest of the input.
43def stdCodecDecodeByte =
44  (lambda unrestricted input : Bytes .
45    (eliminate
46      StdBool
47      (lambda unrestricted current : (family StdBool) . (family StdDecoded Byte))
48      (stdBoolFromNatural (bytes-length input))
49      (branch
50        StdTrue
51        .
52        (constructor StdDecoded StdDecodedValue Byte (bytes-head input) (bytes-tail input)))
53      (branch StdFalse . (constructor StdDecoded StdDecodedTruncated Byte))))
54
55-- LEB128, the variable-length encoding the interface cache uses: seven bits
56-- per byte, low group first, the high bit meaning "more follows". Five groups
57-- cover every value a 32-bit quantity can hold, and the encoding is canonical
58-- 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""))))))
113
114-- A natural as four little-endian bytes. Values wider than the field are
115-- reduced modulo the width, which is stated here rather than discovered: a
116-- caller who needs a checked conversion uses `Data.CheckedWord64`.
117def stdCodecEncodeWord32 =
118  (lambda unrestricted value : Nat .
119    (let unrestricted byte0 =
120      (naturalModuloUnchecked value stdCodecByteBase)
121      in
122      (let unrestricted rest1 =
123        (naturalDivideUnchecked value stdCodecByteBase)
124        in
125        (let unrestricted byte1 =
126          (naturalModuloUnchecked rest1 stdCodecByteBase)
127          in
128          (let unrestricted rest2 =
129            (naturalDivideUnchecked rest1 stdCodecByteBase)
130            in
131            (let unrestricted byte2 =
132              (naturalModuloUnchecked rest2 stdCodecByteBase)
133              in
134              (let unrestricted rest3 =
135                (naturalDivideUnchecked rest2 stdCodecByteBase)
136                in
137                (bytes-cons
138                  (nat-to-byte byte0)
139                  (bytes-cons
140                    (nat-to-byte byte1)
141                    (bytes-cons
142                      (nat-to-byte byte2)
143                      (bytes-cons
144                        (nat-to-byte (naturalModuloUnchecked rest3 stdCodecByteBase))
145                        b"")))))))))))
146
147-- Four little-endian bytes as a natural, with the remaining input. A shorter
148-- input is reported as truncated, never padded.
149def stdCodecDecodeWord32 =
150  (lambda unrestricted input : Bytes .
151    (eliminate
152      StdBool
153      (lambda unrestricted current : (family StdBool) . (family StdDecoded Nat))
154      (stdBoolFromNatural (nat-less-than (bytes-length input) (byte-to-nat (byte 4))))
155      (branch StdTrue . (constructor StdDecoded StdDecodedTruncated Nat))
156      (branch
157        StdFalse
158        .
159        (let unrestricted byte0 =
160          (byte-to-nat (bytes-head input))
161          in
162          (let unrestricted after0 =
163            (bytes-tail input)
164            in
165            (let unrestricted byte1 =
166              (byte-to-nat (bytes-head after0))
167              in
168              (let unrestricted after1 =
169                (bytes-tail after0)
170                in
171                (let unrestricted byte2 =
172                  (byte-to-nat (bytes-head after1))
173                  in
174                  (let unrestricted after2 =
175                    (bytes-tail after1)
176                    in
177                    (let unrestricted byte3 =
178                      (byte-to-nat (bytes-head after2))
179                      in
180                      (constructor
181                        StdDecoded
182                        StdDecodedValue
183                        Nat
184                        (naturalAdd
185                          byte0
186                          (naturalMultiply
187                            stdCodecByteBase
188                            (naturalAdd
189                              byte1
190                              (naturalMultiply
191                                stdCodecByteBase
192                                (naturalAdd byte2 (naturalMultiply stdCodecByteBase byte3))))))
193                        (bytes-tail after2))))))))))))
194
195-- The checksum of a byte string: the same one the source snapshot uses, so a
196-- library caller and the compiler agree on what a content digest is.
197def stdCodecChecksum =
198  (lambda unrestricted input : Bytes . (bytes-checksum input))
199
200-- Did this decoder run out of input?
201def stdDecodedIsTruncated =
202  (lambda erased valueType : Type 0 .
203    (lambda unrestricted decoded : (family StdDecoded valueType) .
204      (eliminate
205        StdDecoded
206        (lambda unrestricted current : (family StdDecoded valueType) . (family StdBool))
207        decoded
208        (branch StdDecodedValue item rest . (constructor StdBool StdFalse))
209        (branch StdDecodedTruncated . (constructor StdBool StdTrue)))))
210
211-- The decoded value, or a default when the input ended too soon.
212def stdDecodedValueOr =
213  (lambda erased valueType : Type 0 .
214    (lambda unrestricted fallback : valueType .
215      (lambda unrestricted decoded : (family StdDecoded valueType) .
216        (eliminate
217          StdDecoded
218          (lambda unrestricted current : (family StdDecoded valueType) . valueType)
219          decoded
220          (branch StdDecodedValue item rest . item)
221          (branch StdDecodedTruncated . fallback)))))