1 import Base 2 3 # The PHC string format of an Argon2id hash: 4 # 5 # $argon2id$v=19$m=,t=,p=

$$ 6 # 7 # with m, t, p in decimal and the salt and hash in standard base64 (RFC 4648 8 # section 4 alphabet) without padding, as the reference implementation and 9 # argon2-cffi write it. parse accepts exactly the strings format writes, up to 10 # leading zeros in the numbers; base64 must be canonical (unused low bits zero). 11 # 12 # Bytes are U32 values below 256. Base64 is computed through 2-bit crumbs: a 13 # byte is four crumbs (high first), a base64 digit three, so encoding and 14 # decoding only regroup crumbs. 15 16 type Phc is Data: 17 Phc{m: Nat, t: Nat, p: Nat, salt: List<&2, U32>, hash: List<&2, U32>} 18 19 # A number read and the rest of the string. 20 type Got is Data: 21 Got{value: Nat, rest: String} 22 23 # A string cut at a '$': before and after it. 24 type Cut is Data: 25 Cut{before: String, after: String} 26 27 # ---------------------------------------------------------------- crumbs 28 29 # The crumbs of a byte n, high first: n = ((c3 * 4 + c2) * 4 + c1) * 4 + c0. 30 def c0(+b: U32) -> U32: 31 U32.from_nat(Nat.mod(U32.to_nat(b), 4n)) 32 33 def c1(+b: U32) -> U32: 34 U32.from_nat(Nat.mod(Nat.div(U32.to_nat(b), 4n), 4n)) 35 36 def c2(+b: U32) -> U32: 37 U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(b), 4n), 4n), 4n)) 38 39 def c3(+b: U32) -> U32: 40 U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(b), 4n), 4n), 4n)) 41 42 # The byte of four crumbs, high first. 43 def byte_of(+w: U32, +x: U32, +y: U32, +z: U32) -> U32: 44 U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(U32.to_nat(w), 4n), U32.to_nat(x)), 4n), U32.to_nat(y)), 4n), U32.to_nat(z))) 45 46 # The base64 digit value of three crumbs, high first, and back. 47 def sext(+x: U32, +y: U32, +z: U32) -> U32: 48 U32.or(U32.shln(x, 4n), U32.or(U32.shln(y, 2n), z)) 49 50 def su(+s: U32) -> U32: 51 U32.shrn(s, 4n) 52 53 def sv(+s: U32) -> U32: 54 U32.and(U32.shrn(s, 2n), 3) 55 56 def sw(+s: U32) -> U32: 57 U32.and(s, 3) 58 59 def digit_last(+s: U32, is62: Bool) -> U32: 60 match is62: 61 case True{}: 62 43 63 case False{}: 64 47 65 66 # ---------------------------------------------------------------- base64 digits 67 68 def digit_hi(+s: U32, lt62: Bool) -> U32: 69 match lt62: 70 case True{}: 71 U32.sub(s, 4) 72 case False{}: 73 digit_last(s, U32.is_eq(s, 62)) 74 75 def digit_mid(+s: U32, lt52: Bool) -> U32: 76 match lt52: 77 case True{}: 78 U32.add(s, 71) 79 case False{}: 80 digit_hi(s, U32.is_lt(s, 62)) 81 82 def digit_code(+s: U32, lt26: Bool) -> U32: 83 match lt26: 84 case True{}: 85 U32.add(s, 65) 86 case False{}: 87 digit_mid(s, U32.is_lt(s, 52)) 88 89 # The character of digit value s < 64: A-Z, a-z, 0-9, +, /. 90 def digit(+s: U32) -> Char: 91 Chr{digit_code(s, U32.is_lt(s, 26))} 92 93 def in_range(+x: U32, +lo: U32, +hi: U32) -> Bool: 94 Bool.and(U32.is_le(lo, x), U32.is_le(x, hi)) 95 96 def value_slash(slash: Bool) -> Maybe<&2, U32>: 97 match slash: 98 case True{}: 99 Some{63} 100 case False{}: 101 None{} 102 103 def value_sym(+x: U32, plus: Bool) -> Maybe<&2, U32>: 104 match plus: 105 case True{}: 106 Some{62} 107 case False{}: 108 value_slash(U32.is_eq(x, 47)) 109 110 def value_num(+x: U32, num: Bool) -> Maybe<&2, U32>: 111 match num: 112 case True{}: 113 Some{U32.add(x, 4)} 114 case False{}: 115 value_sym(x, U32.is_eq(x, 43)) 116 117 def value_low(+x: U32, low: Bool) -> Maybe<&2, U32>: 118 match low: 119 case True{}: 120 Some{U32.sub(x, 71)} 121 case False{}: 122 value_num(x, in_range(x, 48, 57)) 123 124 def value_code(+x: U32, up: Bool) -> Maybe<&2, U32>: 125 match up: 126 case True{}: 127 Some{U32.sub(x, 65)} 128 case False{}: 129 value_low(x, in_range(x, 97, 122)) 130 131 # The value of a base64 character, or None. 132 def value(c: Char) -> Maybe<&2, U32>: 133 match c: 134 case Chr{+x}: 135 value_code(x, in_range(x, 65, 90)) 136 137 # ---------------------------------------------------------------- base64 138 139 def enc1(+a: U32) -> String: 140 SCon{digit(sext(c3(a), c2(a), c1(a))), SCon{digit(sext(c0(a), 0, 0)), SNil{}}} 141 142 def enc2(+a: U32, +b: U32) -> String: 143 SCon{digit(sext(c3(a), c2(a), c1(a))), SCon{digit(sext(c0(a), c3(b), c2(b))), SCon{digit(sext(c1(b), c0(b), 0)), SNil{}}}} 144 145 def enc3(+a: U32, +b: U32, +c: U32, rest: String) -> String: 146 SCon{digit(sext(c3(a), c2(a), c1(a))), SCon{digit(sext(c0(a), c3(b), c2(b))), SCon{digit(sext(c1(b), c0(b), c3(c))), SCon{digit(sext(c2(c), c1(c), c0(c))), rest}}}} 147 148 # Standard base64 without padding. 149 def b64(bs: List<&2, U32>) -> String: 150 match bs: 151 case Nil{}: 152 SNil{} 153 case a <> Nil{}: 154 enc1(a) 155 case a <> b <> Nil{}: 156 enc2(a, b) 157 case a <> b <> c <> rest: 158 enc3(a, b, c, b64(rest)) 159 160 def dec2_fin(+x: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>: 161 match ok: 162 case True{}: 163 Some{[x]} 164 case False{}: 165 None{} 166 167 def dec2(ma: Maybe<&2, U32>, mb: Maybe<&2, U32>) -> Maybe<&2, List<&2, U32>>: 168 match ma mb: 169 case Some{+a} Some{+b}: 170 dec2_fin(byte_of(su(a), sv(a), sw(a), su(b)), Bool.and(U32.is_eq(sv(b), 0), U32.is_eq(sw(b), 0))) 171 case _ _: 172 None{} 173 174 def dec3_fin(+x: U32, +y: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>: 175 match ok: 176 case True{}: 177 Some{[x, y]} 178 case False{}: 179 None{} 180 181 def dec3(ma: Maybe<&2, U32>, mb: Maybe<&2, U32>, mc: Maybe<&2, U32>) -> Maybe<&2, List<&2, U32>>: 182 match ma mb mc: 183 case Some{+a} Some{+b} Some{+c}: 184 dec3_fin(byte_of(su(a), sv(a), sw(a), su(b)), byte_of(sv(b), sw(b), su(c), sv(c)), U32.is_eq(sw(c), 0)) 185 case _ _ _: 186 None{} 187 188 def dec4(ma: Maybe<&2, U32>, mb: Maybe<&2, U32>, mc: Maybe<&2, U32>, md: Maybe<&2, U32>, mr: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>: 189 match ma mb mc md mr: 190 case Some{+a} Some{+b} Some{+c} Some{+d} Some{rest}: 191 Some{byte_of(su(a), sv(a), sw(a), su(b)) <> byte_of(sv(b), sw(b), su(c), sv(c)) <> byte_of(sw(c), su(d), sv(d), sw(d)) <> rest} 192 case _ _ _ _ _: 193 None{} 194 195 # The bytes of canonical unpadded base64, or None. 196 def unb64(s: String) -> Maybe<&2, List<&2, U32>>: 197 match s: 198 case SNil{}: 199 Some{Nil{}} 200 case SCon{a, SNil{}}: 201 None{} 202 case SCon{a, SCon{b, SNil{}}}: 203 dec2(value(a), value(b)) 204 case SCon{a, SCon{b, SCon{c, SNil{}}}}: 205 dec3(value(a), value(b), value(c)) 206 case SCon{a, SCon{b, SCon{c, SCon{d, rest}}}}: 207 dec4(value(a), value(b), value(c), value(d), unb64(rest)) 208 209 # ---------------------------------------------------------------- decimal 210 211 def dchar(+d: Nat) -> Char: 212 Chr{U32.add(48, U32.from_nat(d))} 213 214 # The decimal digits of n before acc; fuel bounds the number of digits and 215 # last says n < 10. 216 def dec_go(fuel: Nat, +n: Nat, acc: String, last: Bool) -> String: 217 match fuel last: 218 case 0n _: 219 acc 220 case 1n+f True{}: 221 SCon{dchar(n), acc} 222 case 1n+f False{}: 223 +q = Nat.div(n, 10n) 224 dec_go(f, q, SCon{dchar(Nat.mod(n, 10n)), acc}, Nat.is_lt(q, 10n)) 225 226 # n in decimal, without leading zeros. 227 def decimal(+n: Nat) -> String: 228 dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n)) 229 230 def is_digit(+x: U32) -> Bool: 231 in_range(x, 48, 57) 232 233 def starts_digit(s: String) -> Bool: 234 match s: 235 case SNil{}: 236 False{} 237 case SCon{Chr{+x}, rest}: 238 is_digit(x) 239 240 # Digits from s on top of v (d says s starts with a digit); the value and the rest. 241 def read_go(s: String, +v: Nat, d: Bool) -> Got: 242 match s d: 243 case SNil{} _: 244 Got{v, SNil{}} 245 case SCon{Chr{+x}, +rest} True{}: 246 read_go(rest, Nat.add(Nat.mul(v, 10n), U32.to_nat(U32.sub(x, 48))), starts_digit(rest)) 247 case SCon{c, rest} False{}: 248 Got{v, SCon{c, rest}} 249 250 def read_check(s: String, first: Bool) -> Maybe<&2, Got>: 251 match first: 252 case True{}: 253 Some{read_go(s, 0n, True{})} 254 case False{}: 255 None{} 256 257 # A decimal number (at least one digit) and the rest. 258 def read(+s: String) -> Maybe<&2, Got>: 259 read_check(s, starts_digit(s)) 260 261 # ---------------------------------------------------------------- the string 262 263 def same_char(a: Char, b: Char) -> Bool: 264 match a b: 265 case Chr{x} Chr{y}: 266 U32.is_eq(x, y) 267 268 def heads(+lit: String, +s: String) -> Bool: 269 match lit s: 270 case SCon{a, lt} SCon{b, st}: 271 same_char(a, b) 272 case _ _: 273 False{} 274 275 # s without the prefix lit, or None (same says the first characters agree). 276 def strip_go(lit: String, s: String, same: Bool) -> Maybe<&2, String>: 277 match lit s same: 278 case SNil{} _ _: 279 Some{s} 280 case SCon{a, lt} SNil{} _: 281 None{} 282 case SCon{a, +lt} SCon{b, +st} True{}: 283 strip_go(lt, st, heads(lt, st)) 284 case SCon{a, lt} SCon{b, st} False{}: 285 None{} 286 287 def strip(+lit: String, +s: String) -> Maybe<&2, String>: 288 strip_go(lit, s, heads(lit, s)) 289 290 def dollar(s: String) -> Bool: 291 match s: 292 case SCon{Chr{+x}, rest}: 293 U32.is_eq(x, 36) 294 case SNil{}: 295 False{} 296 297 def field_cons(+x: U32, r: Maybe<&2, Cut>) -> Maybe<&2, Cut>: 298 match r: 299 case None{}: 300 None{} 301 case Some{Cut{a, b}}: 302 Some{Cut{SCon{Chr{x}, a}, b}} 303 304 # The characters before the first '$' and what follows it, or None (d says s starts with '$'). 305 def field_go(s: String, d: Bool) -> Maybe<&2, Cut>: 306 match s d: 307 case SNil{} _: 308 None{} 309 case SCon{c, rest} True{}: 310 Some{Cut{SNil{}, rest}} 311 case SCon{Chr{+x}, +rest} False{}: 312 field_cons(x, field_go(rest, dollar(rest))) 313 314 def field(+s: String) -> Maybe<&2, Cut>: 315 field_go(s, dollar(s)) 316 317 def format(x: Phc) -> String: 318 match x: 319 case Phc{m, t, p, salt, hash}: 320 String.concat(["$argon2id$v=19$m=", decimal(m), ",t=", decimal(t), ",p=", decimal(p), "$", b64(salt), "$", b64(hash)]) 321 322 def parse_hash(+m: Nat, +t: Nat, +p: Nat, salt: Maybe<&2, List<&2, U32>>, hash: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Phc>: 323 match salt hash: 324 case Some{s} Some{h}: 325 Some{Phc{m, t, p, s, h}} 326 case _ _: 327 None{} 328 329 def parse_salt(+m: Nat, +t: Nat, +p: Nat, r: Maybe<&2, Cut>) -> Maybe<&2, Phc>: 330 match r: 331 case None{}: 332 None{} 333 case Some{Cut{s, h}}: 334 parse_hash(m, t, p, unb64(s), unb64(h)) 335 336 def parse_p2(+m: Nat, +t: Nat, +p: Nat, r: Maybe<&2, String>) -> Maybe<&2, Phc>: 337 match r: 338 case None{}: 339 None{} 340 case Some{rest}: 341 parse_salt(m, t, p, field(rest)) 342 343 def parse_p(+m: Nat, +t: Nat, r: Maybe<&2, Got>) -> Maybe<&2, Phc>: 344 match r: 345 case None{}: 346 None{} 347 case Some{Got{+p, rest}}: 348 parse_p2(m, t, p, strip("$", rest)) 349 350 def parse_t2(+m: Nat, +t: Nat, r: Maybe<&2, String>) -> Maybe<&2, Phc>: 351 match r: 352 case None{}: 353 None{} 354 case Some{rest}: 355 parse_p(m, t, read(rest)) 356 357 def parse_t(+m: Nat, r: Maybe<&2, Got>) -> Maybe<&2, Phc>: 358 match r: 359 case None{}: 360 None{} 361 case Some{Got{+t, rest}}: 362 parse_t2(m, t, strip(",p=", rest)) 363 364 def parse_m2(+m: Nat, r: Maybe<&2, String>) -> Maybe<&2, Phc>: 365 match r: 366 case None{}: 367 None{} 368 case Some{rest}: 369 parse_t(m, read(rest)) 370 371 def parse_m(r: Maybe<&2, Got>) -> Maybe<&2, Phc>: 372 match r: 373 case None{}: 374 None{} 375 case Some{Got{+m, rest}}: 376 parse_m2(m, strip(",t=", rest)) 377 378 def parse_head(r: Maybe<&2, String>) -> Maybe<&2, Phc>: 379 match r: 380 case None{}: 381 None{} 382 case Some{rest}: 383 parse_m(read(rest)) 384 385 # The fields of an Argon2id version 19 PHC string, or None. 386 def parse(s: String) -> Maybe<&2, Phc>: 387 parse_head(strip("$argon2id$v=19$m=", s))