0 | module Data.String.Base64.Encode
  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.Core
  8 | import Data.Buffer.Indexed
  9 | import Data.Linear.Token
 10 | import Data.List
 11 | import Syntax.T1
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Length calculations
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| Given a length of input data, calculate the length of its Base64 encoding.
 18 | |||
 19 | ||| Base64 encodes every three input bytes as four output bytes.
 20 | |||
 21 | ||| A final partial group of one or two bytes is padded to a complete
 22 | ||| four-byte group.
 23 | |||
 24 | ||| The returned length does not include a trailing NUL byte.
 25 | |||
 26 | export
 27 | base64EncodeLength : Int -> Int
 28 | base64EncodeLength len =
 29 |   ((len + 2) `div` 3) * 4
 30 |
 31 | ||| Calculate the number of Base64 bytes required to encode a given number
 32 | ||| of input bytes.
 33 | |||
 34 | ||| This is the natural-number counterpart of `base64EncodeLength` and is
 35 | ||| used internally when allocating statically sized mutable buffers.
 36 | |||
 37 | base64EncodeLengthNat : Nat -> Nat
 38 | base64EncodeLengthNat len =
 39 |   ((len + 2) `div` 3) * 4
 40 |
 41 | --------------------------------------------------------------------------------
 42 | --          Internal constants
 43 | --------------------------------------------------------------------------------
 44 |
 45 | ||| The ASCII representation of the Base64 padding character.
 46 | |||
 47 | charpadBits8 : Bits8
 48 | charpadBits8 = 61
 49 |
 50 | --------------------------------------------------------------------------------
 51 | --          Internal Base64 table access
 52 | --------------------------------------------------------------------------------
 53 |
 54 | ||| Look up the first Base64 character generated from an input byte.
 55 | |||
 56 | ||| The `e0a` table maps each possible input byte directly to the Base64
 57 | ||| character represented by its upper six bits.
 58 | |||
 59 | indexBase64First : Bits8 -> Char
 60 | indexBase64First byte =
 61 |   case tryNatToFin (cast {to=Nat} byte) of
 62 |     Nothing =>
 63 |       assert_total $
 64 |         idris_crash
 65 |           "Data.String.Base64.Encode.indexBase64First: invalid input byte"
 66 |     Just i =>
 67 |       at e0a.arr i
 68 |
 69 | ||| Look up a Base64 character using the second optimized encoding table.
 70 | |||
 71 | ||| The input is a six-bit Base64 alphabet index represented as `Bits8`.
 72 | |||
 73 | indexBase64Second : Bits8 -> Char
 74 | indexBase64Second index =
 75 |   case tryNatToFin (cast {to=Nat} index) of
 76 |     Nothing =>
 77 |       assert_total $
 78 |         idris_crash
 79 |           "Data.String.Base64.Encode.indexBase64Second: invalid Base64 index"
 80 |     Just i =>
 81 |       at e1a.arr i
 82 |
 83 | ||| Look up a Base64 character using the third optimized encoding table.
 84 | |||
 85 | ||| The input is a six-bit Base64 alphabet index represented as `Bits8`.
 86 | |||
 87 | indexBase64Third : Bits8 -> Char
 88 | indexBase64Third index =
 89 |   case tryNatToFin (cast {to=Nat} index) of
 90 |     Nothing =>
 91 |       assert_total $
 92 |         idris_crash
 93 |           "Data.String.Base64.Encode.indexBase64Third: invalid Base64 index"
 94 |     Just i =>
 95 |       at e2a.arr i
 96 |
 97 | --------------------------------------------------------------------------------
 98 | --          Mutable buffer access
 99 | --------------------------------------------------------------------------------
100 |
101 | ||| Write a byte to a mutable buffer at a natural-number offset.
102 | |||
103 | ||| The mutable buffer is scoped to the current `F1` region. The offset is
104 | ||| dynamically converted to a valid `Fin n`; failure indicates an internal
105 | ||| encoder invariant violation.
106 | |||
107 | ||| All offsets passed by the encoder are derived from the precomputed Base64
108 | ||| output length and are therefore expected to be in bounds.
109 | |||
110 | writeByte : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> F1' s
111 | writeByte buf offset value =
112 |   case tryNatToFin offset of
113 |     Nothing =>
114 |       assert_total $
115 |         idris_crash
116 |           "Data.String.Base64.Encode.writeByte: output offset out of bounds"
117 |     Just i =>
118 |       set buf i value
119 |
120 | --------------------------------------------------------------------------------
121 | --          Three-byte hot path
122 | --------------------------------------------------------------------------------
123 |
124 | ||| Encode three input bytes into four Base64 bytes.
125 | |||
126 | ||| This is the hot path of the native encoder.
127 | |||
128 | ||| Three input bytes contain 24 bits, which are divided into four six-bit
129 | ||| Base64 indices:
130 | |||
131 | |||   76543210 76543210 76543210
132 | |||   aaaaaabb bbbbcccc ccdddddd
133 | |||
134 | ||| The optimized encoding tables from `Data.String.Base64.Internal` are used
135 | ||| to translate the resulting indices into their ASCII Base64 bytes.
136 | |||
137 | ||| The destination buffer must contain at least four writable bytes beginning
138 | ||| at `destOffset`.
139 | |||
140 | encodeThree : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> Bits8 -> Bits8 -> F1' s
141 | encodeThree dest destOffset b0 b1 b2 = T1.do
142 |   let i1 : Bits8
143 |       i1 =
144 |         ((b0 .&. 0x03) `shiftL` 4)
145 |           .|. (b1 `shiftR` 4)
146 |       i2 : Bits8
147 |       i2 =
148 |         ((b1 .&. 0x0F) `shiftL` 2)
149 |           .|. (b2 `shiftR` 6)
150 |       i3 : Bits8
151 |       i3 =
152 |         b2 .&. 0x3F
153 |       c0 : Bits8
154 |       c0 =
155 |         cast $ ord (indexBase64First b0)
156 |       c1 : Bits8
157 |       c1 =
158 |         cast $ ord (indexBase64Second i1)
159 |       c2 : Bits8
160 |       c2 =
161 |         cast $ ord (indexBase64Third i2)
162 |       c3 : Bits8
163 |       c3 =
164 |         cast $ ord (indexBase64Second i3)
165 |   writeByte dest destOffset       c0
166 |   writeByte dest (destOffset + 1) c1
167 |   writeByte dest (destOffset + 2) c2
168 |   writeByte dest (destOffset + 3) c3
169 |
170 | --------------------------------------------------------------------------------
171 | --          Final partial groups
172 | --------------------------------------------------------------------------------
173 |
174 | ||| Encode a final one-byte Base64 group.
175 | |||
176 | ||| One input byte produces two Base64 characters followed by two padding
177 | ||| characters:
178 | |||
179 | |||     xx==
180 | |||
181 | ||| The destination buffer must contain at least four writable bytes beginning
182 | ||| at `destOffset`.
183 | |||
184 | encodeOne : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> F1' s
185 | encodeOne dest destOffset b0 = T1.do
186 |   let i1 : Bits8
187 |       i1 =
188 |         (b0 .&. 0x03) `shiftL` 4
189 |       c0 : Bits8
190 |       c0 =
191 |         cast $ ord (indexBase64First b0)
192 |       c1 : Bits8
193 |       c1 =
194 |         cast $ ord (indexBase64Second i1)
195 |   writeByte dest destOffset       c0
196 |   writeByte dest (destOffset + 1) c1
197 |   writeByte dest (destOffset + 2) charpadBits8
198 |   writeByte dest (destOffset + 3) charpadBits8
199 |
200 | ||| Encode a final two-byte Base64 group.
201 | |||
202 | ||| Two input bytes produce three Base64 characters followed by one padding
203 | ||| character:
204 | |||
205 | |||     xxx=
206 | |||
207 | ||| The destination buffer must contain at least four writable bytes beginning
208 | ||| at `destOffset`.
209 | |||
210 | encodeTwo : {n : Nat} -> MBuffer s n -> Nat -> Bits8 -> Bits8 -> F1' s
211 | encodeTwo dest destOffset b0 b1 = T1.do
212 |   let i1 : Bits8
213 |       i1 =
214 |         ((b0 .&. 0x03) `shiftL` 4)
215 |           .|. (b1 `shiftR` 4)
216 |       i2 : Bits8
217 |       i2 =
218 |         (b1 .&. 0x0F) `shiftL` 2
219 |       c0 : Bits8
220 |       c0 =
221 |         cast $ ord (indexBase64First b0)
222 |       c1 : Bits8
223 |       c1 =
224 |         cast $ ord (indexBase64Second i1)
225 |       c2 : Bits8
226 |       c2 =
227 |         cast $ ord (indexBase64Third i2)
228 |   writeByte dest destOffset       c0
229 |   writeByte dest (destOffset + 1) c1
230 |   writeByte dest (destOffset + 2) c2
231 |   writeByte dest (destOffset + 3) charpadBits8
232 |
233 | --------------------------------------------------------------------------------
234 | --          Native encoder
235 | --------------------------------------------------------------------------------
236 |
237 | ||| Encode a list of bytes into a preallocated mutable Base64 buffer.
238 | |||
239 | ||| The destination buffer must be large enough to hold
240 | ||| `base64EncodeLengthNat (length input)` bytes.
241 | |||
242 | ||| Complete three-byte groups are processed using the optimized Base64
243 | ||| encoding lookup tables. Only the final one- or two-byte group uses the
244 | ||| padding-specific paths.
245 | |||
246 | ||| Mutation remains entirely inside the `F1` region associated with the
247 | ||| supplied `MBuffer`.
248 | |||
249 | ||| The returned natural number is the number of bytes written.
250 | |||
251 | encodeBuffer : {n : Nat} -> MBuffer s n -> List Bits8 -> Nat -> F1 s Nat
252 | encodeBuffer dest input destOffset =
253 |   go input destOffset
254 |   where
255 |     go : List Bits8 -> Nat -> F1 s Nat
256 |     go [] offset =
257 |       pure offset
258 |     go [b0] offset = T1.do
259 |       encodeOne dest offset b0
260 |       pure (offset + 4)
261 |     go [b0, b1] offset = T1.do
262 |       encodeTwo dest offset b0 b1
263 |       pure (offset + 4)
264 |     go (b0 :: b1 :: b2 :: rest) offset = T1.do
265 |       encodeThree dest offset b0 b1 b2
266 |       go rest (offset + 4)
267 |
268 | --------------------------------------------------------------------------------
269 | --          List encoding
270 | --------------------------------------------------------------------------------
271 |
272 | ||| Encode a list of bytes into Base64.
273 | |||
274 | ||| The implementation is entirely native Idris2 and has no dependency on an
275 | ||| external C Base64 implementation.
276 | |||
277 | ||| A mutable byte buffer of exactly the required output size is allocated
278 | ||| inside an `F1` region. The encoder writes directly into this buffer using
279 | ||| the optimized lookup tables from `Data.String.Base64.Internal`.
280 | |||
281 | ||| Once encoding is complete, the mutable buffer is frozen without copying
282 | ||| and converted to the requested `List Bits8` result.
283 | |||
284 | ||| The returned list contains ASCII Base64 bytes.
285 | |||
286 | export
287 | base64Encode : List Bits8 -> List Bits8
288 | base64Encode input =
289 |   let inputLen : Nat
290 |       inputLen = length input
291 |       outputLen : Nat
292 |       outputLen = base64EncodeLengthNat inputLen
293 |   in
294 |     run1 $ T1.do
295 |       dest <- mbuffer1 outputLen
296 |       _    <- encodeBuffer dest input 0
297 |       buf  <- unsafeFreeze dest
298 |       pure (toList buf)
299 |
300 | --------------------------------------------------------------------------------
301 | --          String encoding
302 | --------------------------------------------------------------------------------
303 |
304 | ||| Encode a list of bytes into a Base64 String.
305 | |||
306 | ||| Base64 output consists entirely of ASCII characters.
307 | |||
308 | ||| The encoder writes directly into a mutable byte buffer inside an `F1`
309 | ||| region and converts the completed buffer directly to a `String`.
310 | |||
311 | ||| This avoids first materializing the Base64 output as a `List Bits8` and
312 | ||| then allocating another buffer solely for UTF-8 decoding.
313 | |||
314 | export
315 | base64EncodeString : List Bits8 -> String
316 | base64EncodeString input =
317 |   let inputLen : Nat
318 |       inputLen = length input
319 |       outputLen : Nat
320 |       outputLen = base64EncodeLengthNat inputLen
321 |   in
322 |     run1 $ T1.do
323 |       dest <- mbuffer1 outputLen
324 |       _    <- encodeBuffer dest input 0
325 |       bufString dest outputLen
326 |