proofs/crypto/argon2/phc.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc

8 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ./words.bend as LW
import ../../math/hash/hash.bend as HH
import ../../math/natural/arith.bend as NR
import ../../../src/crypto/argon2/phc.bend as PH

Definitions

def ok source · line 16 · raw

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

Every byte is below 256.

def ok_head source · line 23 · raw

@+x:U32 -> @+r:List<&2, U32> -> @+h:{ok(x <> r) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}

def ok_tail source · line 26 · raw

@+x:U32 -> @+r:List<&2, U32> -> @+h:{ok(x <> r) == True{} : Bool} -> {ok(r) == True{} : Bool}

def u source · line 29 · raw

@+n:Nat -> U32

def dv_n source · line 34 · raw

@+n:Nat -> @+h:{Nat.is_lt(n, 64n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.digit(u(n))) == Some{u(n)} : Maybe<&2, U32>}

def digit_value source · line 167 · raw

@+x:U32 -> @+h:{Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.digit(x)) == Some{x} : Maybe<&2, U32>}

def nd_n source · line 171 · raw

@+n:Nat -> @+h:{Nat.is_lt(n, 64n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dollar(SCon{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.digit(u(n)), ""}) == False{} : Bool}

def no_dollar source · line 304 · raw

@+x:U32 -> @+h:{Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dollar(SCon{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.digit(x), ""}) == False{} : Bool}

def tn source · line 311 · raw

@+i:Nat -> @+h:{Nat.is_lt(i, 4n) == True{} : Bool} -> {U32.to_nat(U32.from_nat(i)) == i : Nat}

A value below 4 round-trips through U32.

def div4_lt source · line 315 · raw

@+m:Nat -> @+k:Nat -> @+h:{Nat.is_lt(m, Nat.mul(k, 4n)) == True{} : Bool} -> {Nat.is_lt(Nat.div(m, 4n), k) == True{} : Bool}

m < K * 4 gives m / 4 < K.

def c0_lt source · line 318 · raw

@+x:U32 -> {Nat.is_lt(U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c0(x)), 4n) == True{} : Bool}

def c1_lt source · line 322 · raw

@+x:U32 -> {Nat.is_lt(U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c1(x)), 4n) == True{} : Bool}

def c2_lt source · line 326 · raw

@+x:U32 -> {Nat.is_lt(U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c2(x)), 4n) == True{} : Bool}

def t3_lt source · line 330 · raw

@+x:U32 -> @+h:{Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool} -> {Nat.is_lt(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n) == True{} : Bool}

def c3_lt source · line 333 · raw

@+x:U32 -> @+h:{Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c3(x)), 4n) == True{} : Bool}

def byte_rt source · line 338 · raw

@+x:U32 -> @+h:{Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.byte_of(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c3(x), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c2(x), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c1(x), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.c0(x)) == x : U32}

A byte is the byte of its crumbs.

def su_eq_n source · line 350 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha:{Nat.is_lt(a, 4n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 4n) == True{} : Bool} -> @+hc:{Nat.is_lt(c, 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.su(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(u(a), u(b), u(c))) == u(a) : U32}

def su_eq source · line 523 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> @+hx:{Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool} -> @+hy:{Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool} -> @+hz:{Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.su(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(x, y, z)) == x : U32}

def sv_eq_n source · line 529 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha:{Nat.is_lt(a, 4n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 4n) == True{} : Bool} -> @+hc:{Nat.is_lt(c, 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(u(a), u(b), u(c))) == u(b) : U32}

def sv_eq source · line 702 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> @+hx:{Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool} -> @+hy:{Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool} -> @+hz:{Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(x, y, z)) == y : U32}

def sw_eq_n source · line 708 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha:{Nat.is_lt(a, 4n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 4n) == True{} : Bool} -> @+hc:{Nat.is_lt(c, 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sw(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(u(a), u(b), u(c))) == u(c) : U32}

def sw_eq source · line 881 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> @+hx:{Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool} -> @+hy:{Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool} -> @+hz:{Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sw(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(x, y, z)) == z : U32}

def sx_lt_n source · line 887 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha:{Nat.is_lt(a, 4n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 4n) == True{} : Bool} -> @+hc:{Nat.is_lt(c, 4n) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(u(a), u(b), u(c))), 64n) == True{} : Bool}

def sx_lt source · line 1060 · raw

@+x:U32 -> @+y:U32 -> @+z:U32 -> @+hx:{Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool} -> @+hy:{Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool} -> @+hz:{Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.sext(x, y, z)), 64n) == True{} : Bool}

def b64_rt source · line 1068 · raw

@+bs:List<&2, U32> -> @+h:{ok(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.unb64(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.b64(bs)) == Some{bs} : Maybe<&2, List<&2, U32>>}

def nd source · line 1137 · raw

@s:String -> Bool

No character is '$'.

def dollar_cons source · line 1144 · raw

@+c:Char -> @+r:String -> @+r2:String -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dollar(SCon{c, r}) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dollar(SCon{c, r2}) : Bool}

def nd_head source · line 1149 · raw

@+c:Char -> @+r:String -> @+h:{nd(SCon{c, r}) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dollar(SCon{c, ""}) == False{} : Bool}

def nd_tail source · line 1153 · raw

@+c:Char -> @+r:String -> @+h:{nd(SCon{c, r}) == True{} : Bool} -> {nd(r) == True{} : Bool}

def field_nd source · line 1157 · raw

@+cs:String -> @+r:String -> @+h:{nd(cs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.field_go(String.append(cs, SCon{'$', r}), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dollar(String.append(cs, SCon{'$', r}))) == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Cut{cs, r}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Cut>}

A string without '$', then '$': the field before it and the rest.

def b64_nd source · line 1167 · raw

@+bs:List<&2, U32> -> @+h:{ok(bs) == True{} : Bool} -> {nd(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.b64(bs)) == True{} : Bool}

def field_b64 source · line 1200 · raw

@+bs:List<&2, U32> -> @+r:String -> @+h:{ok(bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.field(String.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.b64(bs), SCon{'$', r})) == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Cut{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.b64(bs), r}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Cut>}

def dd_n source · line 1205 · raw

@+n:Nat -> @+h:{Nat.is_lt(n, 10n) == True{} : Bool} -> {U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)) == n : Nat}

def di_n source · line 1230 · raw

@+n:Nat -> @+h:{Nat.is_lt(n, 10n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.is_digit(U32.add(48, U32.from_nat(n))) == True{} : Bool}

def mul10_ge source · line 1255 · raw

@+k:Nat -> {Nat.is_le(k, Nat.mul(k, 10n)) == True{} : Bool}

def lt9 source · line 1265 · raw

@+m:Nat -> {Nat.is_lt(m, Nat.add(9n, Nat.mul(m, 10n))) == True{} : Bool}

m < 9 + 10 m

def div10_lt source · line 1272 · raw

@+n:Nat -> @+h:{Nat.is_le(1n, n) == True{} : Bool} -> {Nat.is_lt(Nat.div(n, 10n), n) == True{} : Bool}

n / 10 < n for n >= 1.

def ge10_pos source · line 1281 · raw

@+n:Nat -> @+h:{Nat.is_lt(n, 10n) == False{} : Bool} -> {Nat.is_le(1n, n) == True{} : Bool}

def sd_dec source · line 1288 · raw

@+f:Nat -> @+n:Nat -> @+acc:String -> @+Y:String -> @+last:Bool -> @+el:{Nat.is_lt(n, 10n) == last : Bool} -> @+hf:{Nat.is_lt(n, f) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.starts_digit(String.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dec_go(f, n, acc, last), Y)) == True{} : Bool}

def dec_step source · line 1298 · raw

@+n:Nat -> @+ay:String -> @+hr:{Nat.is_lt(Nat.mod(n, 10n), 10n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.read_go(SCon{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dchar(Nat.mod(n, 10n)), ay}, Nat.div(n, 10n), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.starts_digit(SCon{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dchar(Nat.mod(n, 10n)), ay})) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.read_go(ay, n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.starts_digit(ay)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Got}

def dec_go_rt source · line 1308 · raw

@+f:Nat -> @+n:Nat -> @+acc:String -> @+Y:String -> @+last:Bool -> @+el:{Nat.is_lt(n, 10n) == last : Bool} -> @+hf:{Nat.is_lt(n, f) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.read_go(String.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.dec_go(f, n, acc, last), Y), 0n, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.read_go(String.append(acc, Y), n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.starts_digit(String.append(acc, Y))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Got}

Reading the decimal digits of n before acc gives n and acc.

def got_nd source · line 1326 · raw

@+n:Nat -> @+c:Char -> @+Y:String -> {Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.read_go(SCon{c, Y}, n, False{})} == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Got{n, SCon{c, Y}}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Got>}

def dec_rt source · line 1332 · raw

@+n:Nat -> @+c:Char -> @+Y:String -> @+hc:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.starts_digit(SCon{c, Y}) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.read(String.append(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.decimal(n), SCon{c, Y})) == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Got{n, SCon{c, Y}}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Got>}

A decimal number followed by a non-digit is read back.

def append_nil source · line 1342 · raw

@+x:String -> {String.append(x, "") == x : String}

def parse_format source · line 1350 · raw

@+m:Nat -> @+t:Nat -> @+p:Nat -> @+salt:List<&2, U32> -> @+hash:List<&2, U32> -> @+hs:{ok(salt) == True{} : Bool} -> @+hh:{ok(hash) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.parse(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.format(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Phc{m, t, p, salt, hash})) == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Phc{m, t, p, salt, hash}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Phc>}

parse(format(x)) == Some{x}, for byte lists of bytes below 256.