0 | module Data.String.Base64.Decode
  1 |
  2 | import Data.String.Base64.Internal
  3 |
  4 | import Data.Array
  5 | import Data.Array.Indexed
  6 | import Data.Bits
  7 | import Data.Buffer
  8 | import Data.Buffer.Core
  9 | import Data.Buffer.Indexed
 10 | import Data.Linear.Token
 11 | import Data.List
 12 | import Syntax.T1
 13 |
 14 | --------------------------------------------------------------------------------
 15 | --          Length calculations
 16 | --------------------------------------------------------------------------------
 17 |
 18 | ||| Given the length of Base64 encoded data, calculate the maximum possible
 19 | ||| length of the decoded data.
 20 | |||
 21 | ||| The result is an upper bound and does not account for padding characters.
 22 | |||
 23 | ||| The actual decoded length may therefore be smaller.
 24 | |||
 25 | export
 26 | base64DecodeLength : Int -> Int
 27 | base64DecodeLength len =
 28 |   (len `div` 4) * 3 + 2
 29 |
 30 | ||| Calculate the maximum number of bytes that can be produced by decoding
 31 | ||| a Base64 input of the given length.
 32 | |||
 33 | ||| This is the natural-number counterpart of `base64DecodeLength` and is used
 34 | ||| internally when allocating statically sized mutable output buffers.
 35 | |||
 36 | base64DecodeLengthNat : Nat -> Nat
 37 | base64DecodeLengthNat len =
 38 |   (len `div` 4) * 3 + 2
 39 |
 40 | --------------------------------------------------------------------------------
 41 | --          Internal constants
 42 | --------------------------------------------------------------------------------
 43 |
 44 | ||| The ASCII value of the Base64 padding character.
 45 | |||
 46 | charpadBits8 : Bits8
 47 | charpadBits8 = 61
 48 |
 49 | ||| The sentinel value stored in the decoder lookup tables for an invalid
 50 | ||| Base64 input byte.
 51 | |||
 52 | ||| The decoder lookup tables use a 24-bit packed representation.
 53 | |||
 54 | ||| The high-order bit is set in this value so that invalid table entries can
 55 | ||| be detected efficiently after lookup.
 56 | |||
 57 | base64DecodeInvalid : Bits32
 58 | base64DecodeInvalid = 0x01ffffff
 59 |
 60 | --------------------------------------------------------------------------------
 61 | --          Internal table access
 62 | --------------------------------------------------------------------------------
 63 |
 64 | ||| Look up a decoder contribution for an ASCII input byte.
 65 | |||
 66 | ||| The decoder tables contain 256 entries, one for every possible byte value.
 67 | |||
 68 | ||| The input is therefore used directly as an array index.
 69 | |||
 70 | lookupDecodeTable : Array Bits32 -> Bits8 -> Bits32
 71 | lookupDecodeTable table byte =
 72 |   case tryNatToFin (cast {to=Nat} byte) of
 73 |     Nothing =>
 74 |       assert_total $
 75 |         idris_crash
 76 |           "Data.String.Base64.Decode.lookupDecodeTable: invalid byte index"
 77 |     Just index =>
 78 |       at table.arr index
 79 |
 80 | ||| Look up the first packed decoder contribution for a Base64 input byte.
 81 | |||
 82 | lookupD0 : Bits8 -> Bits32
 83 | lookupD0 =
 84 |   lookupDecodeTable d0a
 85 |
 86 | ||| Look up the second packed decoder contribution for a Base64 input byte.
 87 | |||
 88 | lookupD1 : Bits8 -> Bits32
 89 | lookupD1 =
 90 |   lookupDecodeTable d1a
 91 |
 92 | ||| Look up the third packed decoder contribution for a Base64 input byte.
 93 | |||
 94 | lookupD2 : Bits8 -> Bits32
 95 | lookupD2 =
 96 |   lookupDecodeTable d2a
 97 |
 98 | ||| Look up the fourth packed decoder contribution for a Base64 input byte.
 99 | |||
100 | lookupD3 : Bits8 -> Bits32
101 | lookupD3 =
102 |   lookupDecodeTable d3a
103 |
104 | --------------------------------------------------------------------------------
105 | --          Decoder table validation
106 | --------------------------------------------------------------------------------
107 |
108 | ||| Determine whether a decoder table contribution represents invalid input.
109 | |||
110 | isInvalidDecodeValue : Bits32 -> Bool
111 | isInvalidDecodeValue value =
112 |   value == base64DecodeInvalid
113 |
114 | ||| Determine whether a Base64 input byte is the padding character.
115 | |||
116 | isPadding : Bits8 -> Bool
117 | isPadding byte =
118 |   byte == charpadBits8
119 |
120 | ||| Determine whether a byte is a valid Base64 alphabet character.
121 | |||
122 | ||| This checks the optimized lookup tables directly.
123 | |||
124 | ||| Padding is handled separately because it is valid only in the final
125 | ||| quartet.
126 | |||
127 | isValidBase64Byte : Bits8 -> Bool
128 | isValidBase64Byte byte =
129 |   not (isInvalidDecodeValue (lookupD0 byte))
130 |     || not (isInvalidDecodeValue (lookupD1 byte))
131 |     || not (isInvalidDecodeValue (lookupD2 byte))
132 |     || not (isInvalidDecodeValue (lookupD3 byte))
133 |
134 | --------------------------------------------------------------------------------
135 | --          Immutable buffer access
136 | --------------------------------------------------------------------------------
137 |
138 | ||| Read a byte from an immutable input buffer at a natural-number offset.
139 | |||
140 | ||| The decoder's traversal guarantees that all requested offsets are within
141 | ||| the bounds of the source buffer. Failure therefore indicates an internal
142 | ||| decoder invariant violation.
143 | |||
144 | readByte : {n : Nat} -> IBuffer n -> Nat -> Bits8
145 | readByte src offset =
146 |   case tryNatToFin offset of
147 |     Nothing =>
148 |       assert_total $
149 |         idris_crash
150 |           "Data.String.Base64.Decode.readByte: input offset out of bounds"
151 |     Just i =>
152 |       at src i
153 |
154 | --------------------------------------------------------------------------------
155 | --          Mutable buffer access
156 | --------------------------------------------------------------------------------
157 |
158 | ||| Write a decoded byte to a mutable output buffer at a natural-number offset.
159 | |||
160 | ||| The destination buffer is scoped to the current `F1` region.
161 | |||
162 | ||| The decoder preallocates an output buffer large enough for the maximum
163 | ||| possible decoded result, so failure indicates an internal decoder
164 | ||| invariant violation.
165 | |||
166 | writeByte : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> F1' s
167 | writeByte dest offset value =
168 |   case tryNatToFin offset of
169 |     Nothing =>
170 |       assert_total $
171 |         idris_crash
172 |           "Data.String.Base64.Decode.writeByte: output offset out of bounds"
173 |     Just i =>
174 |       set dest i value
175 |
176 | --------------------------------------------------------------------------------
177 | --          Four-byte hot path
178 | --------------------------------------------------------------------------------
179 |
180 | ||| Decode four Base64 alphabet bytes into a packed 24-bit output value.
181 | |||
182 | ||| The four input bytes are translated through the optimized `d0a`, `d1a`,
183 | ||| `d2a`, and `d3a` lookup tables.
184 | |||
185 | ||| Each table contains a pre-shifted contribution to the final 24-bit value.
186 | ||| Combining those contributions with bitwise OR reconstructs the original
187 | ||| three bytes.
188 | |||
189 | ||| Returns `Nothing` if any input byte is not a valid Base64 alphabet
190 | ||| character.
191 | |||
192 | decodeFourValue : Bits8 -> Bits8 -> Bits8 -> Bits8 -> Maybe Bits32
193 | decodeFourValue c0 c1 c2 c3 =
194 |   let v0 : Bits32
195 |       v0 = lookupD0 c0
196 |       v1 : Bits32
197 |       v1 = lookupD1 c1
198 |       v2 : Bits32
199 |       v2 = lookupD2 c2
200 |       v3 : Bits32
201 |       v3 = lookupD3 c3
202 |   in
203 |     case isInvalidDecodeValue v0
204 |       || isInvalidDecodeValue v1
205 |       || isInvalidDecodeValue v2
206 |       || isInvalidDecodeValue v3 of
207 |       True =>
208 |         Nothing
209 |       False =>
210 |         Just (v0 .|. v1 .|. v2 .|. v3)
211 |
212 | ||| Decode four complete, non-padded Base64 characters and write the resulting
213 | ||| three bytes to a mutable output buffer.
214 | |||
215 | ||| The optimized decoder tables reconstruct the original three bytes in
216 | ||| little-endian byte order within the packed 24-bit value:
217 | |||
218 | |||   bits  0..7  = first decoded byte
219 | |||   bits  8..15 = second decoded byte
220 | |||   bits 16..23 = third decoded byte
221 | |||
222 | ||| The destination buffer must contain at least three writable bytes beginning
223 | ||| at `destOffset`.
224 | |||
225 | decodeFour : {n : Nat} -> MBuffer s n -> Nat -> Bits32 -> F1' s
226 | decodeFour dest destOffset value = T1.do
227 |   let b0 : Bits8
228 |       b0 =
229 |         cast value
230 |       b1 : Bits8
231 |       b1 =
232 |         cast (value `shiftR` 8)
233 |       b2 : Bits8
234 |       b2 =
235 |         cast (value `shiftR` 16)
236 |   writeByte dest destOffset       b0
237 |   writeByte dest (destOffset + 1) b1
238 |   writeByte dest (destOffset + 2) b2
239 |
240 | --------------------------------------------------------------------------------
241 | --          Final padded groups
242 | --------------------------------------------------------------------------------
243 |
244 | ||| Decode a final Base64 quartet containing `==` padding.
245 | |||
246 | ||| A quartet of the form:
247 | |||
248 | |||     xx==
249 | |||
250 | ||| represents exactly one decoded byte.
251 | |||
252 | ||| The first two characters must be valid Base64 alphabet characters.
253 | |||
254 | ||| The optimized decoder tables place the decoded byte in the least
255 | ||| significant eight bits of the packed value.
256 | |||
257 | ||| The returned `Maybe Nat` contains the number of bytes written.
258 | |||
259 | decodeOne : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> Bits8 -> F1 s (Maybe Nat)
260 | decodeOne dest destOffset c0 c1 =
261 |   if isPadding c0 || isPadding c1
262 |      then
263 |        pure Nothing
264 |      else
265 |        let v0 : Bits32
266 |            v0 = lookupD0 c0
267 |            v1 : Bits32
268 |            v1 = lookupD1 c1
269 |        in
270 |          if isInvalidDecodeValue v0
271 |             || isInvalidDecodeValue v1
272 |          then
273 |            pure Nothing
274 |          else T1.do
275 |            let value : Bits32
276 |                value =
277 |                  v0 .|. v1
278 |                b0 : Bits8
279 |                b0 =
280 |                  cast value
281 |            writeByte dest destOffset b0
282 |            pure (Just 1)
283 |
284 | ||| Decode a final Base64 quartet containing `=` padding.
285 | |||
286 | ||| A quartet of the form:
287 | |||
288 | |||     xxx=
289 | |||
290 | ||| represents exactly two decoded bytes.
291 | |||
292 | ||| The first three characters must be valid Base64 alphabet characters.
293 | |||
294 | ||| The optimized decoder tables place the first decoded byte in bits 0..7
295 | ||| and the second decoded byte in bits 8..15 of the packed value.
296 | |||
297 | ||| The returned `Maybe Nat` contains the number of bytes written.
298 | |||
299 | decodeTwo : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> Bits8 -> Bits8 -> F1 s (Maybe Nat)
300 | decodeTwo dest destOffset c0 c1 c2 =
301 |   if isPadding c0 || isPadding c1 || isPadding c2
302 |      then
303 |        pure Nothing
304 |      else
305 |        let v0 : Bits32
306 |            v0 = lookupD0 c0
307 |            v1 : Bits32
308 |            v1 = lookupD1 c1
309 |            v2 : Bits32
310 |            v2 = lookupD2 c2
311 |        in
312 |          if isInvalidDecodeValue v0
313 |             || isInvalidDecodeValue v1
314 |             || isInvalidDecodeValue v2
315 |          then
316 |            pure Nothing
317 |          else T1.do
318 |            let value : Bits32
319 |                value =
320 |                  v0 .|. v1 .|. v2
321 |                b0 : Bits8
322 |                b0 =
323 |                  cast value
324 |                b1 : Bits8
325 |                b1 =
326 |                  cast (value `shiftR` 8)
327 |            writeByte dest destOffset       b0
328 |            writeByte dest (destOffset + 1) b1
329 |            pure (Just 2)
330 |
331 | --------------------------------------------------------------------------------
332 | --          Native decoder
333 | --------------------------------------------------------------------------------
334 |
335 | ||| Decode an immutable Base64 input buffer into a preallocated mutable output
336 | ||| buffer.
337 | |||
338 | ||| Complete four-character Base64 groups are decoded through the optimized
339 | ||| `d0a`, `d1a`, `d2a`, and `d3a` lookup tables.
340 | |||
341 | ||| Padding is permitted only in the final quartet.
342 | |||
343 | ||| A final `==` quartet produces one byte, while a final `=` quartet produces
344 | ||| two bytes.
345 | |||
346 | ||| Mutation remains entirely inside the `F1` region associated with the
347 | ||| supplied destination buffer.
348 | |||
349 | ||| The returned `Maybe Nat` contains the number of decoded bytes written to
350 | ||| the destination buffer.
351 | |||
352 | decodeBuffer : {destLen : Nat} -> {srcLen : Nat} -> IBuffer srcLen -> MBuffer s destLen -> Nat -> F1 s (Maybe Nat)
353 | decodeBuffer src dest destOffset =
354 |   go 0 destOffset
355 |   where
356 |     go : Nat -> Nat -> F1 s (Maybe Nat)
357 |     go srcOffset outOffset =
358 |       let remaining : Nat
359 |           remaining =
360 |             srcLen `minus` srcOffset
361 |       in
362 |         if remaining == 0
363 |         then
364 |           pure (Just (outOffset `minus` destOffset))
365 |         else if remaining < 4
366 |         then
367 |           -- Base64 input must consist entirely of complete four-character
368 |           -- quartets.
369 |           pure Nothing
370 |         else
371 |           let c0 : Bits8
372 |               c0 =
373 |                 readByte src srcOffset
374 |               c1 : Bits8
375 |               c1 =
376 |                 readByte src (srcOffset + 1)
377 |               c2 : Bits8
378 |               c2 =
379 |                 readByte src (srcOffset + 2)
380 |               c3 : Bits8
381 |               c3 =
382 |                 readByte src (srcOffset + 3)
383 |           in
384 |             if isPadding c0
385 |             then
386 |               -- Padding cannot appear as the first character of a quartet.
387 |               pure Nothing
388 |             else if isPadding c1
389 |             then
390 |               -- Padding cannot appear as the second character of a quartet.
391 |               pure Nothing
392 |             else if isPadding c2
393 |             then
394 |               -- The only valid padded form here is:
395 |               --
396 |               --     xx==
397 |               --
398 |               if isPadding c3
399 |               then
400 |                 -- Padding must terminate the entire input.
401 |                 if srcOffset + 4 == srcLen
402 |                 then T1.do
403 |                   result <- decodeOne dest outOffset c0 c1
404 |                   case result of
405 |                     Nothing =>
406 |                       pure Nothing
407 |                     Just written =>
408 |                       pure $
409 |                         Just
410 |                           ((outOffset + written) `minus` destOffset)
411 |                 else
412 |                   pure Nothing
413 |               else
414 |                 pure Nothing
415 |             else if isPadding c3
416 |             then
417 |               -- The only valid padded form here is:
418 |               --
419 |               --     xxx=
420 |               --
421 |               -- Padding must terminate the entire input.
422 |               if srcOffset + 4 == srcLen
423 |               then T1.do
424 |                 result <- decodeTwo dest outOffset c0 c1 c2
425 |                 case result of
426 |                   Nothing =>
427 |                     pure Nothing
428 |                   Just written =>
429 |                     pure $
430 |                       Just
431 |                         ((outOffset + written) `minus` destOffset)
432 |               else
433 |                 pure Nothing
434 |             else
435 |               -- Complete, non-padded quartet.
436 |               case decodeFourValue c0 c1 c2 c3 of
437 |                 Nothing =>
438 |                   pure Nothing
439 |                 Just value => T1.do
440 |                   decodeFour dest outOffset value
441 |                   go
442 |                     (srcOffset + 4)
443 |                     (outOffset + 3)
444 |
445 | --------------------------------------------------------------------------------
446 | --          Immutable buffer decoding
447 | --------------------------------------------------------------------------------
448 |
449 | ||| Decode an immutable Base64 byte buffer.
450 | |||
451 | ||| A mutable destination buffer large enough for the maximum decoded result
452 | ||| is allocated inside an `F1` region.
453 | |||
454 | ||| After successful decoding, only the prefix actually written is frozen.
455 | ||| `unsafeFreezeLTE` performs this operation without copying the backing
456 | ||| buffer.
457 | |||
458 | ||| The resulting immutable byte buffer is then materialized as a
459 | ||| `List Bits8`.
460 | |||
461 | decodeIBuffer : {n : Nat} -> IBuffer n -> Maybe (List Bits8)
462 | decodeIBuffer src =
463 |   let outputLen : Nat
464 |       outputLen =
465 |         base64DecodeLengthNat n
466 |   in
467 |     run1 $ T1.do
468 |       dest <- mbuffer1 outputLen
469 |       result <- decodeBuffer src dest 0
470 |       case result of
471 |         Nothing =>
472 |           pure Nothing
473 |         Just written =>
474 |           case isLTE written outputLen of
475 |             No _ =>
476 |               -- The decoder must never be able to write more than the
477 |               -- precomputed maximum decoded size.
478 |               pure Nothing
479 |             Yes prf => T1.do
480 |               decoded <- unsafeFreezeLTE dest written @{prf}
481 |               pure $
482 |                 Just (toList decoded)
483 |
484 | --------------------------------------------------------------------------------
485 | --          Public decoding API
486 | --------------------------------------------------------------------------------
487 |
488 | ||| Decode a list of Base64 bytes into its original bytes.
489 | |||
490 | ||| Returns `Nothing` if the input is not valid Base64.
491 | |||
492 | ||| The source list is copied once into an immutable `IBuffer`, after which
493 | ||| decoding operates entirely on the array library's indexed buffer types.
494 | |||
495 | ||| The decoder allocates a mutable output buffer inside an `F1` region,
496 | ||| processes complete quartets using the optimized `d0a` through `d3a`
497 | ||| lookup tables, freezes only the successfully written output prefix, and
498 | ||| finally converts that prefix to `List Bits8`.
499 | |||
500 | export
501 | base64DecodeBits8 : List Bits8 -> Maybe (List Bits8)
502 | base64DecodeBits8 input =
503 |   decodeIBuffer (bufferL input)
504 |
505 | ||| Decode a Base64 String into its original bytes.
506 | |||
507 | ||| The String is converted directly to an immutable UTF-8 byte buffer using
508 | ||| the array library's `fromString` operation.
509 | |||
510 | ||| Since Base64 is ASCII-only, valid Base64 text has the same byte
511 | ||| representation in UTF-8. Any non-Base64 UTF-8 byte is rejected by the
512 | ||| optimized decoder tables.
513 | |||
514 | ||| Returns `Nothing` when the input is not valid Base64.
515 | |||
516 | export
517 | base64DecodeString : String -> Maybe (List Bits8)
518 | base64DecodeString str =
519 |   decodeIBuffer (fromString str)
520 |