src/crypto/argon2/phc.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/argon2/phc.bend as Phc

1 import

import Base

Types

type Phc source · line 16 · raw

Data

Phc

@m:Nat -> @t:Nat -> @p:Nat -> @salt:List<&2, U32> -> @hash:List<&2, U32> -> Phc

type Got source · line 20 · raw

Data

A number read and the rest of the string.

Got
```
@value:Nat -> @rest:String -> Got
```

type Cut source · line 24 · raw

Data

A string cut at a '$': before and after it.

Cut
```
@before:String -> @after:String -> Cut
```

Definitions

def c0 source · line 30 · raw

@+b:U32 -> U32

The crumbs of a byte n, high first: n = ((c3 * 4 + c2) * 4 + c1) * 4 + c0.

def c1 source · line 33 · raw

@+b:U32 -> U32

def c2 source · line 36 · raw

@+b:U32 -> U32

def c3 source · line 39 · raw

@+b:U32 -> U32

def byte_of source · line 43 · raw

@+w:U32 -> @+x:U32 -> @+y:U32 -> @+z:U32 -> U32

The byte of four crumbs, high first.

def sext source · line 47 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> U32

The base64 digit value of three crumbs, high first, and back.

def su source · line 50 · raw

@+s:U32 -> U32

def sv source · line 53 · raw

@+s:U32 -> U32

def sw source · line 56 · raw

@+s:U32 -> U32

def digit_last source · line 59 · raw

@+s:U32 -> @is62:Bool -> U32

def digit_hi source · line 68 · raw

@+s:U32 -> @lt62:Bool -> U32

def digit_mid source · line 75 · raw

@+s:U32 -> @lt52:Bool -> U32

def digit_code source · line 82 · raw

@+s:U32 -> @lt26:Bool -> U32

def digit source · line 90 · raw

@+s:U32 -> Char

The character of digit value s < 64: A-Z, a-z, 0-9, +, /.

def in_range source · line 93 · raw

@+x:U32 -> @+lo:U32 -> @+hi:U32 -> Bool

def value_slash source · line 96 · raw

@slash:Bool -> Maybe<&2, U32>

def value_sym source · line 103 · raw

@+x:U32 -> @plus:Bool -> Maybe<&2, U32>

def value_num source · line 110 · raw

@+x:U32 -> @num:Bool -> Maybe<&2, U32>

def value_low source · line 117 · raw

@+x:U32 -> @low:Bool -> Maybe<&2, U32>

def value_code source · line 124 · raw

@+x:U32 -> @up:Bool -> Maybe<&2, U32>

def value source · line 132 · raw

@c:Char -> Maybe<&2, U32>

The value of a base64 character, or None.

def enc1 source · line 139 · raw

@+a:U32 -> String

def enc2 source · line 142 · raw

@+a:U32 -> @+b:U32 -> String

def enc3 source · line 145 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @rest:String -> String

def b64 source · line 149 · raw

@bs:List<&2, U32> -> String

Standard base64 without padding.

def dec2_fin source · line 160 · raw

@+x:U32 -> @ok:Bool -> Maybe<&2, List<&2, U32>>

def dec2 source · line 167 · raw

@ma:Maybe<&2, U32> -> @mb:Maybe<&2, U32> -> Maybe<&2, List<&2, U32>>

def dec3_fin source · line 174 · raw

@+x:U32 -> @+y:U32 -> @ok:Bool -> Maybe<&2, List<&2, U32>>

def dec3 source · line 181 · raw

@ma:Maybe<&2, U32> -> @mb:Maybe<&2, U32> -> @mc:Maybe<&2, U32> -> Maybe<&2, List<&2, U32>>

def dec4 source · line 188 · raw

@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>>

def unb64 source · line 196 · raw

@s:String -> Maybe<&2, List<&2, U32>>

The bytes of canonical unpadded base64, or None.

def dchar source · line 211 · raw

@+d:Nat -> Char

def dec_go source · line 216 · raw

@fuel:Nat -> @+n:Nat -> @acc:String -> @last:Bool -> String

The decimal digits of n before acc; fuel bounds the number of digits and last says n < 10.

def decimal source · line 227 · raw

@+n:Nat -> String

n in decimal, without leading zeros.

def is_digit source · line 230 · raw

@+x:U32 -> Bool

def starts_digit source · line 233 · raw

@s:String -> Bool

def read_go source · line 241 · raw

@s:String -> @+v:Nat -> @d:Bool -> Got

Digits from s on top of v (d says s starts with a digit); the value and the rest.

def read_check source · line 250 · raw

@s:String -> @first:Bool -> Maybe<&2, Got>

def read source · line 258 · raw

@+s:String -> Maybe<&2, Got>

A decimal number (at least one digit) and the rest.

def same_char source · line 263 · raw

@a:Char -> @b:Char -> Bool

def heads source · line 268 · raw

@+lit:String -> @+s:String -> Bool

def strip_go source · line 276 · raw

@lit:String -> @s:String -> @same:Bool -> Maybe<&2, String>

s without the prefix lit, or None (same says the first characters agree).

def strip source · line 287 · raw

@+lit:String -> @+s:String -> Maybe<&2, String>

def dollar source · line 290 · raw

@s:String -> Bool

def field_cons source · line 297 · raw

@+x:U32 -> @r:Maybe<&2, Cut> -> Maybe<&2, Cut>

def field_go source · line 305 · raw

@s:String -> @d:Bool -> Maybe<&2, Cut>

The characters before the first '$' and what follows it, or None (d says s starts with '$').

def field source · line 314 · raw

@+s:String -> Maybe<&2, Cut>

def format source · line 317 · raw

@x:Phc -> String

def parse_hash source · line 322 · raw

@+m:Nat -> @+t:Nat -> @+p:Nat -> @salt:Maybe<&2, List<&2, U32>> -> @hash:Maybe<&2, List<&2, U32>> -> Maybe<&2, Phc>

def parse_salt source · line 329 · raw

@+m:Nat -> @+t:Nat -> @+p:Nat -> @r:Maybe<&2, Cut> -> Maybe<&2, Phc>

def parse_p2 source · line 336 · raw

@+m:Nat -> @+t:Nat -> @+p:Nat -> @r:Maybe<&2, String> -> Maybe<&2, Phc>

def parse_p source · line 343 · raw

@+m:Nat -> @+t:Nat -> @r:Maybe<&2, Got> -> Maybe<&2, Phc>

def parse_t2 source · line 350 · raw

@+m:Nat -> @+t:Nat -> @r:Maybe<&2, String> -> Maybe<&2, Phc>

def parse_t source · line 357 · raw

@+m:Nat -> @r:Maybe<&2, Got> -> Maybe<&2, Phc>

def parse_m2 source · line 364 · raw

@+m:Nat -> @r:Maybe<&2, String> -> Maybe<&2, Phc>

def parse_m source · line 371 · raw

@r:Maybe<&2, Got> -> Maybe<&2, Phc>

def parse_head source · line 378 · raw

@r:Maybe<&2, String> -> Maybe<&2, Phc>

def parse source · line 386 · raw

@s:String -> Maybe<&2, Phc>

The fields of an Argon2id version 19 PHC string, or None.