proofs/crypto/argon2/phc.bend source
proofs/crypto/argon2/phc.bend on the hub · documented module
import Baseimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/u32.bend as Uimport ./words.bend as LWimport ../../math/hash/hash.bend as HHimport ../../math/natural/arith.bend as NRimport ../../../src/crypto/argon2/phc.bend as PH# Generated by tools/generators/argon2_phc_gen.py; do not edit by hand.# The PHC string of an Argon2id hash parses back to its fields: base64 and# decimal round trips, and the '$'-separated fields. Every finite fact# (a crumb, a base64 digit, a decimal digit) is checked value by value.# Every byte is below 256.def ok(bs: List<&2, U32>) -> Bool: match bs: case Nil{}: True{} case x <> r: Bool.and(Nat.is_lt(U32.to_nat(x), 256n), ok(r))def ok_head(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}: L.and_left(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)def ok_tail(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {ok(r) == True{} : Bool}: L.and_right(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)def u(+n: Nat) -> U32: U32.from_nat(n)# ---------------------------------------------------------------- base64 digitsdef dv_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.value(PH.digit(u(n))) == Some{u(n)} : Maybe<&2, U32>}: match n: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n: {==} case 5n: {==} case 6n: {==} case 7n: {==} case 8n: {==} case 9n: {==} case 10n: {==} case 11n: {==} case 12n: {==} case 13n: {==} case 14n: {==} case 15n: {==} case 16n: {==} case 17n: {==} case 18n: {==} case 19n: {==} case 20n: {==} case 21n: {==} case 22n: {==} case 23n: {==} case 24n: {==} case 25n: {==} case 26n: {==} case 27n: {==} case 28n: {==} case 29n: {==} case 30n: {==} case 31n: {==} case 32n: {==} case 33n: {==} case 34n: {==} case 35n: {==} case 36n: {==} case 37n: {==} case 38n: {==} case 39n: {==} case 40n: {==} case 41n: {==} case 42n: {==} case 43n: {==} case 44n: {==} case 45n: {==} case 46n: {==} case 47n: {==} case 48n: {==} case 49n: {==} case 50n: {==} case 51n: {==} case 52n: {==} case 53n: {==} case 54n: {==} case 55n: {==} case 56n: {==} case 57n: {==} case 58n: {==} case 59n: {==} case 60n: {==} case 61n: {==} case 62n: {==} case 63n: {==} case 64n+r: Empty.absurd({PH.value(PH.digit(u(64n+r))) == Some{u(64n+r)} : Maybe<&2, U32>}, N.lt_zero_absurd(r, h))def digit_value(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.value(PH.digit(x)) == Some{x} : Maybe<&2, U32>}: %LW.rt(x) : {PH.value(PH.digit(_)) == Some{_} : Maybe<&2, U32>} dv_n(U32.to_nat(x), h)def nd_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(u(n)), SNil{}}) == False{} : Bool}: match n: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n: {==} case 5n: {==} case 6n: {==} case 7n: {==} case 8n: {==} case 9n: {==} case 10n: {==} case 11n: {==} case 12n: {==} case 13n: {==} case 14n: {==} case 15n: {==} case 16n: {==} case 17n: {==} case 18n: {==} case 19n: {==} case 20n: {==} case 21n: {==} case 22n: {==} case 23n: {==} case 24n: {==} case 25n: {==} case 26n: {==} case 27n: {==} case 28n: {==} case 29n: {==} case 30n: {==} case 31n: {==} case 32n: {==} case 33n: {==} case 34n: {==} case 35n: {==} case 36n: {==} case 37n: {==} case 38n: {==} case 39n: {==} case 40n: {==} case 41n: {==} case 42n: {==} case 43n: {==} case 44n: {==} case 45n: {==} case 46n: {==} case 47n: {==} case 48n: {==} case 49n: {==} case 50n: {==} case 51n: {==} case 52n: {==} case 53n: {==} case 54n: {==} case 55n: {==} case 56n: {==} case 57n: {==} case 58n: {==} case 59n: {==} case 60n: {==} case 61n: {==} case 62n: {==} case 63n: {==} case 64n+r: Empty.absurd({PH.dollar(SCon{PH.digit(u(64n+r)), SNil{}}) == False{} : Bool}, N.lt_zero_absurd(r, h))def no_dollar(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(x), SNil{}}) == False{} : Bool}: %LW.rt(x) : {PH.dollar(SCon{PH.digit(_), SNil{}}) == False{} : Bool} nd_n(U32.to_nat(x), h)# ---------------------------------------------------------------- crumbs# A value below 4 round-trips through U32.def tn(+i: Nat, +h: {Nat.is_lt(i, 4n) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}: U.to_nat_from_nat(i, 2n, {==}, h)# m < K * 4 gives m / 4 < K.def div4_lt(+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}: N.not_le_lt(k, Nat.div(m, 4n), Equal.trans(Bool, Nat.is_le(k, Nat.div(m, 4n)), Nat.is_le(Nat.mul(k, 4n), m), False{}, NR.le_div(3n, k, m), N.lt_not_le(m, Nat.mul(k, 4n), h)))def c0_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c0(x)), 4n) == True{} : Bool}: %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {Nat.is_lt(_, 4n) == True{} : Bool} NR.dm_lt(3n, U32.to_nat(x))def c1_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c1(x)), 4n) == True{} : Bool}: %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool} NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n))def c2_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c2(x)), 4n) == True{} : Bool}: %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool} NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n))def t3_lt(+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}: div4_lt(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n, div4_lt(Nat.div(U32.to_nat(x), 4n), 16n, div4_lt(U32.to_nat(x), 64n, h)))def c3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.c3(x)), 4n) == True{} : Bool}: %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {Nat.is_lt(_, 4n) == True{} : Bool} t3_lt(x, h)# A byte is the byte of its crumbs.def byte_rt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {PH.byte_of(PH.c3(x), PH.c2(x), PH.c1(x), PH.c0(x)) == x : U32}: %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), U32.to_nat(PH.c2(x))), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32} %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), _), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32} %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), _), 4n), U32.to_nat(PH.c0(x)))) == x : U32} %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), _)) == x : U32} %NR.dm_eq(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32} %NR.dm_eq(3n, Nat.div(U32.to_nat(x), 4n)) : {U32.from_nat(Nat.add(Nat.mul(_, 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32} %NR.dm_eq(3n, U32.to_nat(x)) : {U32.from_nat(_) == x : U32} LW.rt(x)# ---------------------------------------------------------------- digit values of crumbsdef su_eq_n(+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}) -> {PH.su(PH.sext(u(a), u(b), u(c))) == u(a) : U32}: match a b c: case 0n 0n 0n: {==} case 0n 0n 1n: {==} case 0n 0n 2n: {==} case 0n 0n 3n: {==} case 0n 1n 0n: {==} case 0n 1n 1n: {==} case 0n 1n 2n: {==} case 0n 1n 3n: {==} case 0n 2n 0n: {==} case 0n 2n 1n: {==} case 0n 2n 2n: {==} case 0n 2n 3n: {==} case 0n 3n 0n: {==} case 0n 3n 1n: {==} case 0n 3n 2n: {==} case 0n 3n 3n: {==} case 1n 0n 0n: {==} case 1n 0n 1n: {==} case 1n 0n 2n: {==} case 1n 0n 3n: {==} case 1n 1n 0n: {==} case 1n 1n 1n: {==} case 1n 1n 2n: {==} case 1n 1n 3n: {==} case 1n 2n 0n: {==} case 1n 2n 1n: {==} case 1n 2n 2n: {==} case 1n 2n 3n: {==} case 1n 3n 0n: {==} case 1n 3n 1n: {==} case 1n 3n 2n: {==} case 1n 3n 3n: {==} case 2n 0n 0n: {==} case 2n 0n 1n: {==} case 2n 0n 2n: {==} case 2n 0n 3n: {==} case 2n 1n 0n: {==} case 2n 1n 1n: {==} case 2n 1n 2n: {==} case 2n 1n 3n: {==} case 2n 2n 0n: {==} case 2n 2n 1n: {==} case 2n 2n 2n: {==} case 2n 2n 3n: {==} case 2n 3n 0n: {==} case 2n 3n 1n: {==} case 2n 3n 2n: {==} case 2n 3n 3n: {==} case 3n 0n 0n: {==} case 3n 0n 1n: {==} case 3n 0n 2n: {==} case 3n 0n 3n: {==} case 3n 1n 0n: {==} case 3n 1n 1n: {==} case 3n 1n 2n: {==} case 3n 1n 3n: {==} case 3n 2n 0n: {==} case 3n 2n 1n: {==} case 3n 2n 2n: {==} case 3n 2n 3n: {==} case 3n 3n 0n: {==} case 3n 3n 1n: {==} case 3n 3n 2n: {==} case 3n 3n 3n: {==} case 4n+r _ _: Empty.absurd({PH.su(PH.sext(u(4n+r), u(b), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, ha)) case 0n 4n+r _: Empty.absurd({PH.su(PH.sext(u(0n), u(4n+r), u(c))) == u(0n) : U32}, N.lt_zero_absurd(r, hb)) case 0n 0n 4n+r: Empty.absurd({PH.su(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 0n 1n 4n+r: Empty.absurd({PH.su(PH.sext(u(0n), u(1n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 0n 2n 4n+r: Empty.absurd({PH.su(PH.sext(u(0n), u(2n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 0n 3n 4n+r: Empty.absurd({PH.su(PH.sext(u(0n), u(3n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 4n+r _: Empty.absurd({PH.su(PH.sext(u(1n), u(4n+r), u(c))) == u(1n) : U32}, N.lt_zero_absurd(r, hb)) case 1n 0n 4n+r: Empty.absurd({PH.su(PH.sext(u(1n), u(0n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 1n 4n+r: Empty.absurd({PH.su(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 2n 4n+r: Empty.absurd({PH.su(PH.sext(u(1n), u(2n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 3n 4n+r: Empty.absurd({PH.su(PH.sext(u(1n), u(3n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 4n+r _: Empty.absurd({PH.su(PH.sext(u(2n), u(4n+r), u(c))) == u(2n) : U32}, N.lt_zero_absurd(r, hb)) case 2n 0n 4n+r: Empty.absurd({PH.su(PH.sext(u(2n), u(0n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 1n 4n+r: Empty.absurd({PH.su(PH.sext(u(2n), u(1n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 2n 4n+r: Empty.absurd({PH.su(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 3n 4n+r: Empty.absurd({PH.su(PH.sext(u(2n), u(3n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 4n+r _: Empty.absurd({PH.su(PH.sext(u(3n), u(4n+r), u(c))) == u(3n) : U32}, N.lt_zero_absurd(r, hb)) case 3n 0n 4n+r: Empty.absurd({PH.su(PH.sext(u(3n), u(0n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 1n 4n+r: Empty.absurd({PH.su(PH.sext(u(3n), u(1n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 2n 4n+r: Empty.absurd({PH.su(PH.sext(u(3n), u(2n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 3n 4n+r: Empty.absurd({PH.su(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))def su_eq(+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}) -> {PH.su(PH.sext(x, y, z)) == x : U32}: %LW.rt(x) : {PH.su(PH.sext(_, y, z)) == _ : U32} %LW.rt(y) : {PH.su(PH.sext(u(U32.to_nat(x)), _, z)) == u(U32.to_nat(x)) : U32} %LW.rt(z) : {PH.su(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(x)) : U32} su_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)def sv_eq_n(+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}) -> {PH.sv(PH.sext(u(a), u(b), u(c))) == u(b) : U32}: match a b c: case 0n 0n 0n: {==} case 0n 0n 1n: {==} case 0n 0n 2n: {==} case 0n 0n 3n: {==} case 0n 1n 0n: {==} case 0n 1n 1n: {==} case 0n 1n 2n: {==} case 0n 1n 3n: {==} case 0n 2n 0n: {==} case 0n 2n 1n: {==} case 0n 2n 2n: {==} case 0n 2n 3n: {==} case 0n 3n 0n: {==} case 0n 3n 1n: {==} case 0n 3n 2n: {==} case 0n 3n 3n: {==} case 1n 0n 0n: {==} case 1n 0n 1n: {==} case 1n 0n 2n: {==} case 1n 0n 3n: {==} case 1n 1n 0n: {==} case 1n 1n 1n: {==} case 1n 1n 2n: {==} case 1n 1n 3n: {==} case 1n 2n 0n: {==} case 1n 2n 1n: {==} case 1n 2n 2n: {==} case 1n 2n 3n: {==} case 1n 3n 0n: {==} case 1n 3n 1n: {==} case 1n 3n 2n: {==} case 1n 3n 3n: {==} case 2n 0n 0n: {==} case 2n 0n 1n: {==} case 2n 0n 2n: {==} case 2n 0n 3n: {==} case 2n 1n 0n: {==} case 2n 1n 1n: {==} case 2n 1n 2n: {==} case 2n 1n 3n: {==} case 2n 2n 0n: {==} case 2n 2n 1n: {==} case 2n 2n 2n: {==} case 2n 2n 3n: {==} case 2n 3n 0n: {==} case 2n 3n 1n: {==} case 2n 3n 2n: {==} case 2n 3n 3n: {==} case 3n 0n 0n: {==} case 3n 0n 1n: {==} case 3n 0n 2n: {==} case 3n 0n 3n: {==} case 3n 1n 0n: {==} case 3n 1n 1n: {==} case 3n 1n 2n: {==} case 3n 1n 3n: {==} case 3n 2n 0n: {==} case 3n 2n 1n: {==} case 3n 2n 2n: {==} case 3n 2n 3n: {==} case 3n 3n 0n: {==} case 3n 3n 1n: {==} case 3n 3n 2n: {==} case 3n 3n 3n: {==} case 4n+r _ _: Empty.absurd({PH.sv(PH.sext(u(4n+r), u(b), u(c))) == u(b) : U32}, N.lt_zero_absurd(r, ha)) case 0n 4n+r _: Empty.absurd({PH.sv(PH.sext(u(0n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb)) case 0n 0n 4n+r: Empty.absurd({PH.sv(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 0n 1n 4n+r: Empty.absurd({PH.sv(PH.sext(u(0n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 0n 2n 4n+r: Empty.absurd({PH.sv(PH.sext(u(0n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 0n 3n 4n+r: Empty.absurd({PH.sv(PH.sext(u(0n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 4n+r _: Empty.absurd({PH.sv(PH.sext(u(1n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb)) case 1n 0n 4n+r: Empty.absurd({PH.sv(PH.sext(u(1n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 1n 4n+r: Empty.absurd({PH.sv(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 2n 4n+r: Empty.absurd({PH.sv(PH.sext(u(1n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 1n 3n 4n+r: Empty.absurd({PH.sv(PH.sext(u(1n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 4n+r _: Empty.absurd({PH.sv(PH.sext(u(2n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb)) case 2n 0n 4n+r: Empty.absurd({PH.sv(PH.sext(u(2n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 1n 4n+r: Empty.absurd({PH.sv(PH.sext(u(2n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 2n 4n+r: Empty.absurd({PH.sv(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 2n 3n 4n+r: Empty.absurd({PH.sv(PH.sext(u(2n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 4n+r _: Empty.absurd({PH.sv(PH.sext(u(3n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb)) case 3n 0n 4n+r: Empty.absurd({PH.sv(PH.sext(u(3n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 1n 4n+r: Empty.absurd({PH.sv(PH.sext(u(3n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 2n 4n+r: Empty.absurd({PH.sv(PH.sext(u(3n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc)) case 3n 3n 4n+r: Empty.absurd({PH.sv(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))def sv_eq(+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}) -> {PH.sv(PH.sext(x, y, z)) == y : U32}: %LW.rt(x) : {PH.sv(PH.sext(_, y, z)) == y : U32} %LW.rt(y) : {PH.sv(PH.sext(u(U32.to_nat(x)), _, z)) == _ : U32} %LW.rt(z) : {PH.sv(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(y)) : U32} sv_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)def sw_eq_n(+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}) -> {PH.sw(PH.sext(u(a), u(b), u(c))) == u(c) : U32}: match a b c: case 0n 0n 0n: {==} case 0n 0n 1n: {==} case 0n 0n 2n: {==} case 0n 0n 3n: {==} case 0n 1n 0n: {==} case 0n 1n 1n: {==} case 0n 1n 2n: {==} case 0n 1n 3n: {==} case 0n 2n 0n: {==} case 0n 2n 1n: {==} case 0n 2n 2n: {==} case 0n 2n 3n: {==} case 0n 3n 0n: {==} case 0n 3n 1n: {==} case 0n 3n 2n: {==} case 0n 3n 3n: {==} case 1n 0n 0n: {==} case 1n 0n 1n: {==} case 1n 0n 2n: {==} case 1n 0n 3n: {==} case 1n 1n 0n: {==} case 1n 1n 1n: {==} case 1n 1n 2n: {==} case 1n 1n 3n: {==} case 1n 2n 0n: {==} case 1n 2n 1n: {==} case 1n 2n 2n: {==} case 1n 2n 3n: {==} case 1n 3n 0n: {==} case 1n 3n 1n: {==} case 1n 3n 2n: {==} case 1n 3n 3n: {==} case 2n 0n 0n: {==} case 2n 0n 1n: {==} case 2n 0n 2n: {==} case 2n 0n 3n: {==} case 2n 1n 0n: {==} case 2n 1n 1n: {==} case 2n 1n 2n: {==} case 2n 1n 3n: {==} case 2n 2n 0n: {==} case 2n 2n 1n: {==} case 2n 2n 2n: {==} case 2n 2n 3n: {==} case 2n 3n 0n: {==} case 2n 3n 1n: {==} case 2n 3n 2n: {==} case 2n 3n 3n: {==} case 3n 0n 0n: {==} case 3n 0n 1n: {==} case 3n 0n 2n: {==} case 3n 0n 3n: {==} case 3n 1n 0n: {==} case 3n 1n 1n: {==} case 3n 1n 2n: {==} case 3n 1n 3n: {==} case 3n 2n 0n: {==} case 3n 2n 1n: {==} case 3n 2n 2n: {==} case 3n 2n 3n: {==} case 3n 3n 0n: {==} case 3n 3n 1n: {==} case 3n 3n 2n: {==} case 3n 3n 3n: {==} case 4n+r _ _: Empty.absurd({PH.sw(PH.sext(u(4n+r), u(b), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, ha)) case 0n 4n+r _: Empty.absurd({PH.sw(PH.sext(u(0n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb)) case 0n 0n 4n+r: Empty.absurd({PH.sw(PH.sext(u(0n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 0n 1n 4n+r: Empty.absurd({PH.sw(PH.sext(u(0n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 0n 2n 4n+r: Empty.absurd({PH.sw(PH.sext(u(0n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 0n 3n 4n+r: Empty.absurd({PH.sw(PH.sext(u(0n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 1n 4n+r _: Empty.absurd({PH.sw(PH.sext(u(1n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb)) case 1n 0n 4n+r: Empty.absurd({PH.sw(PH.sext(u(1n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 1n 1n 4n+r: Empty.absurd({PH.sw(PH.sext(u(1n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 1n 2n 4n+r: Empty.absurd({PH.sw(PH.sext(u(1n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 1n 3n 4n+r: Empty.absurd({PH.sw(PH.sext(u(1n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 2n 4n+r _: Empty.absurd({PH.sw(PH.sext(u(2n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb)) case 2n 0n 4n+r: Empty.absurd({PH.sw(PH.sext(u(2n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 2n 1n 4n+r: Empty.absurd({PH.sw(PH.sext(u(2n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 2n 2n 4n+r: Empty.absurd({PH.sw(PH.sext(u(2n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 2n 3n 4n+r: Empty.absurd({PH.sw(PH.sext(u(2n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 3n 4n+r _: Empty.absurd({PH.sw(PH.sext(u(3n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb)) case 3n 0n 4n+r: Empty.absurd({PH.sw(PH.sext(u(3n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 3n 1n 4n+r: Empty.absurd({PH.sw(PH.sext(u(3n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 3n 2n 4n+r: Empty.absurd({PH.sw(PH.sext(u(3n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc)) case 3n 3n 4n+r: Empty.absurd({PH.sw(PH.sext(u(3n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))def sw_eq(+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}) -> {PH.sw(PH.sext(x, y, z)) == z : U32}: %LW.rt(x) : {PH.sw(PH.sext(_, y, z)) == z : U32} %LW.rt(y) : {PH.sw(PH.sext(u(U32.to_nat(x)), _, z)) == z : U32} %LW.rt(z) : {PH.sw(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == _ : U32} sw_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)def sx_lt_n(+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(PH.sext(u(a), u(b), u(c))), 64n) == True{} : Bool}: match a b c: case 0n 0n 0n: {==} case 0n 0n 1n: {==} case 0n 0n 2n: {==} case 0n 0n 3n: {==} case 0n 1n 0n: {==} case 0n 1n 1n: {==} case 0n 1n 2n: {==} case 0n 1n 3n: {==} case 0n 2n 0n: {==} case 0n 2n 1n: {==} case 0n 2n 2n: {==} case 0n 2n 3n: {==} case 0n 3n 0n: {==} case 0n 3n 1n: {==} case 0n 3n 2n: {==} case 0n 3n 3n: {==} case 1n 0n 0n: {==} case 1n 0n 1n: {==} case 1n 0n 2n: {==} case 1n 0n 3n: {==} case 1n 1n 0n: {==} case 1n 1n 1n: {==} case 1n 1n 2n: {==} case 1n 1n 3n: {==} case 1n 2n 0n: {==} case 1n 2n 1n: {==} case 1n 2n 2n: {==} case 1n 2n 3n: {==} case 1n 3n 0n: {==} case 1n 3n 1n: {==} case 1n 3n 2n: {==} case 1n 3n 3n: {==} case 2n 0n 0n: {==} case 2n 0n 1n: {==} case 2n 0n 2n: {==} case 2n 0n 3n: {==} case 2n 1n 0n: {==} case 2n 1n 1n: {==} case 2n 1n 2n: {==} case 2n 1n 3n: {==} case 2n 2n 0n: {==} case 2n 2n 1n: {==} case 2n 2n 2n: {==} case 2n 2n 3n: {==} case 2n 3n 0n: {==} case 2n 3n 1n: {==} case 2n 3n 2n: {==} case 2n 3n 3n: {==} case 3n 0n 0n: {==} case 3n 0n 1n: {==} case 3n 0n 2n: {==} case 3n 0n 3n: {==} case 3n 1n 0n: {==} case 3n 1n 1n: {==} case 3n 1n 2n: {==} case 3n 1n 3n: {==} case 3n 2n 0n: {==} case 3n 2n 1n: {==} case 3n 2n 2n: {==} case 3n 2n 3n: {==} case 3n 3n 0n: {==} case 3n 3n 1n: {==} case 3n 3n 2n: {==} case 3n 3n 3n: {==} case 4n+r _ _: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(4n+r), u(b), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, ha)) case 0n 4n+r _: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb)) case 0n 0n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 0n 1n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 0n 2n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 0n 3n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 1n 4n+r _: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb)) case 1n 0n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 1n 1n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 1n 2n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 1n 3n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 2n 4n+r _: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb)) case 2n 0n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 2n 1n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 2n 2n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 2n 3n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 3n 4n+r _: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb)) case 3n 0n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 3n 1n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 3n 2n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc)) case 3n 3n 4n+r: Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))def sx_lt(+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(PH.sext(x, y, z)), 64n) == True{} : Bool}: %LW.rt(x) : {Nat.is_lt(U32.to_nat(PH.sext(_, y, z)), 64n) == True{} : Bool} %LW.rt(y) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), _, z)), 64n) == True{} : Bool} %LW.rt(z) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)), 64n) == True{} : Bool} sx_lt_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)# ---------------------------------------------------------------- base64def b64_rt(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {PH.unb64(PH.b64(bs)) == Some{bs} : Maybe<&2, List<&2, U32>>}: match bs: case Nil{}: {==} case +a <> Nil{}: +ha = ok_head(a, Nil{}, h) +ta = ok_tail(a, Nil{}, h) %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec2(_, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0)))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0))), Some{PH.sext(PH.c0(a), 0, 0)}, digit_value(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {PH.dec2(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), 0, 0)), PH.c0(a), su_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), 0, 0)), 0, sv_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(_, 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), 0, 0)), 0, sw_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(0, 0), U32.is_eq(_, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec2_fin(_, Bool.and(U32.is_eq(0, 0), U32.is_eq(0, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>} {==} case +a <> +b <> Nil{}: +ha = ok_head(a, b <> Nil{}, h) +ta = ok_tail(a, b <> Nil{}, h) +hb = ok_head(b, Nil{}, ta) +tb = ok_tail(b, Nil{}, ta) %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec3(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0))), Some{PH.sext(PH.c1(b), PH.c0(b), 0)}, digit_value(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0, sw_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(_, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec3_fin(_, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {PH.dec3_fin(a, _, U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>} {==} case +a <> +b <> +c <> +rest: +ha = ok_head(a, b <> c <> rest, h) +ta = ok_tail(a, b <> c <> rest, h) +hb = ok_head(b, c <> rest, ta) +tb = ok_tail(b, c <> rest, ta) +hc = ok_head(c, rest, tb) +tc = ok_tail(c, rest, tb) %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec4(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, digit_value(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, digit_value(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, _, PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(rest)), Some{rest}, b64_rt(rest, tc)) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, _) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c3(c), sw_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(_, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c2(c), su_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), _, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c1(c), sv_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), _, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c0(c), sw_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), _) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {Some{_ <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {Some{a <> _ <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} %Equal.sym(U32, PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)), c, byte_rt(c, hc)) : {Some{a <> b <> _ <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>} {==}# ---------------------------------------------------------------- the '$' separator# No character is '$'.def nd(s: String) -> Bool: match s: case SNil{}: True{} case SCon{c, r}: Bool.and(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r))def dollar_cons(+c: Char, +r: String, +r2: String) -> {PH.dollar(SCon{c, r}) == PH.dollar(SCon{c, r2}) : Bool}: match c: case Chr{x}: {==}def nd_head(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {PH.dollar(SCon{c, SNil{}}) == False{} : Bool}: +e = L.and_left(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h) L.not_true(PH.dollar(SCon{c, SNil{}}), e)def nd_tail(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {nd(r) == True{} : Bool}: L.and_right(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)# A string without '$', then '$': the field before it and the rest.def field_nd(+cs: String, +r: String, +h: {nd(cs) == True{} : Bool}) -> {PH.field_go(String.append(cs, SCon{Chr{36}, r}), PH.dollar(String.append(cs, SCon{Chr{36}, r}))) == Some{PH.Cut{cs, r}} : Maybe<&2, PH.Cut>}: match cs: case SNil{}: {==} case SCon{Chr{+x}, +t}: +hd = Equal.trans(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), PH.dollar(SCon{Chr{x}, SNil{}}), False{}, dollar_cons(Chr{x}, String.append(t, SCon{Chr{36}, r}), SNil{}), nd_head(Chr{x}, t, h)) %Equal.sym(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), False{}, hd) : {PH.field_go(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>} %Equal.sym(Maybe<&2, PH.Cut>, PH.field_go(String.append(t, SCon{Chr{36}, r}), PH.dollar(String.append(t, SCon{Chr{36}, r}))), Some{PH.Cut{t, r}}, field_nd(t, r, nd_tail(Chr{x}, t, h))) : {PH.field_cons(x, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>} {==}def b64_nd(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {nd(PH.b64(bs)) == True{} : Bool}: match bs: case Nil{}: {==} case +a <> Nil{}: +ha = ok_head(a, Nil{}, h) +ta = ok_tail(a, Nil{}, h) %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}})), True{})) == True{} : Bool} %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{})) == True{} : Bool} {==} case +a <> +b <> Nil{}: +ha = ok_head(a, b <> Nil{}, h) +ta = ok_tail(a, b <> Nil{}, h) +hb = ok_head(b, Nil{}, ta) +tb = ok_tail(b, Nil{}, ta) %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool} %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool} %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{}))) == True{} : Bool} {==} case +a <> +b <> +c <> +rest: +ha = ok_head(a, b <> c <> rest, h) +ta = ok_tail(a, b <> c <> rest, h) +hb = ok_head(b, c <> rest, ta) +tb = ok_tail(b, c <> rest, ta) +hc = ok_head(c, rest, tb) +tc = ok_tail(c, rest, tb) %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool} %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool} %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool} %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}}), False{}, no_dollar(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), nd(PH.b64(rest)))))) == True{} : Bool} %Equal.sym(Bool, nd(PH.b64(rest)), True{}, b64_nd(rest, tc)) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), _)))) == True{} : Bool} {==}def field_b64(+bs: List<&2, U32>, +r: String, +h: {ok(bs) == True{} : Bool}) -> {PH.field(String.append(PH.b64(bs), SCon{Chr{36}, r})) == Some{PH.Cut{PH.b64(bs), r}} : Maybe<&2, PH.Cut>}: field_nd(PH.b64(bs), r, b64_nd(bs, h))# ---------------------------------------------------------------- decimaldef dd_n(+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}: match n: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n: {==} case 5n: {==} case 6n: {==} case 7n: {==} case 8n: {==} case 9n: {==} case 10n+r: Empty.absurd({U32.to_nat(U32.sub(U32.add(48, U32.from_nat(10n+r)), 48)) == 10n+r : Nat}, N.lt_zero_absurd(r, h))def di_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {PH.is_digit(U32.add(48, U32.from_nat(n))) == True{} : Bool}: match n: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n: {==} case 5n: {==} case 6n: {==} case 7n: {==} case 8n: {==} case 9n: {==} case 10n+r: Empty.absurd({PH.is_digit(U32.add(48, U32.from_nat(10n+r))) == True{} : Bool}, N.lt_zero_absurd(r, h))def mul10_ge(+k: Nat) -> {Nat.is_le(k, Nat.mul(k, 10n)) == True{} : Bool}: match k: case 0n: {==} case 1n+ +j: +x = Nat.mul(j, 10n) +h1 = N.le_trans(j, x, Nat.add(x, 9n), mul10_ge(j), N.le_add_right(x, 9n)) L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)# m < 9 + 10 mdef lt9(+m: Nat) -> {Nat.is_lt(m, Nat.add(9n, Nat.mul(m, 10n))) == True{} : Bool}: +x = Nat.mul(m, 10n) +h0 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, 9n)) == True{} : Bool}, Nat.add(x, 0n), x, N.add_zero(x), N.lt_add_left(0n, 9n, x, {==})) +h1 = N.le_lt_trans(m, x, Nat.add(x, 9n), mul10_ge(m), h0) L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)# n / 10 < n for n >= 1.def div10_lt(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(n, 10n), n) == True{} : Bool}: match n: case 0n: Empty.absurd({Nat.is_lt(Nat.div(0n, 10n), 0n) == True{} : Bool}, L.false_true(h)) case 1n+ +m: +e = NR.le_div(9n, 1n+m, 1n+m) +f = N.lt_not_le(m, Nat.add(9n, Nat.mul(m, 10n)), lt9(m)) N.not_le_lt(1n+m, Nat.div(1n+m, 10n), Equal.trans(Bool, Nat.is_le(1n+m, Nat.div(1n+m, 10n)), Nat.is_le(Nat.mul(1n+m, 10n), 1n+m), False{}, e, f))def ge10_pos(+n: Nat, +h: {Nat.is_lt(n, 10n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}: match n: case 0n: Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_false(h)) case 1n+ +m: N.zero_le(m)def sd_dec(+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}) -> {PH.starts_digit(String.append(PH.dec_go(f, n, acc, last), Y)) == True{} : Bool}: match f last: case 0n _: Empty.absurd({PH.starts_digit(String.append(acc, Y)) == True{} : Bool}, N.lt_zero_absurd(n, hf)) case 1n+ +g True{}: di_n(n, el) case 1n+ +g False{}: +q = Nat.div(n, 10n) sd_dec(g, q, SCon{PH.dchar(Nat.mod(n, 10n)), acc}, Y, Nat.is_lt(q, 10n), {==}, N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf)))def dec_step(+n: Nat, +ay: String, +hr: {Nat.is_lt(Nat.mod(n, 10n), 10n) == True{} : Bool}) -> {PH.read_go(SCon{PH.dchar(Nat.mod(n, 10n)), ay}, Nat.div(n, 10n), PH.starts_digit(SCon{PH.dchar(Nat.mod(n, 10n)), ay})) == PH.read_go(ay, n, PH.starts_digit(ay)) : PH.Got}: +q = Nat.div(n, 10n) +r = Nat.mod(n, 10n) -rhs = PH.read_go(ay, n, PH.starts_digit(ay)) %Equal.sym(Bool, PH.is_digit(U32.add(48, U32.from_nat(r))), True{}, di_n(r, hr)) : {PH.read_go(SCon{PH.dchar(r), ay}, q, _) == rhs : PH.Got} %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(r)), 48)), r, dd_n(r, hr)) : {PH.read_go(ay, Nat.add(Nat.mul(q, 10n), _), PH.starts_digit(ay)) == rhs : PH.Got} %NR.dm_eq(9n, n) : {PH.read_go(ay, _, PH.starts_digit(ay)) == rhs : PH.Got} {==}# Reading the decimal digits of n before acc gives n and acc.def dec_go_rt(+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}) -> {PH.read_go(String.append(PH.dec_go(f, n, acc, last), Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}: match f last: case 0n _: Empty.absurd({PH.read_go(String.append(acc, Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}, N.lt_zero_absurd(n, hf)) case 1n+ +g True{}: %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)), n, dd_n(n, el)) : {PH.read_go(String.append(acc, Y), _, PH.starts_digit(String.append(acc, Y))) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got} {==} case 1n+ +g False{}: +q = Nat.div(n, 10n) +r = Nat.mod(n, 10n) +ay = String.append(acc, Y) +hr = NR.dm_lt(9n, n) +hq = N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf)) -rhs = PH.read_go(ay, n, PH.starts_digit(ay)) Equal.trans(PH.Got, PH.read_go(String.append(PH.dec_go(g, q, SCon{PH.dchar(r), acc}, Nat.is_lt(q, 10n)), Y), 0n, True{}), PH.read_go(SCon{PH.dchar(r), ay}, q, PH.starts_digit(SCon{PH.dchar(r), ay})), rhs, dec_go_rt(g, q, SCon{PH.dchar(r), acc}, Y, Nat.is_lt(q, 10n), {==}, hq), dec_step(n, ay, hr))def got_nd(+n: Nat, +c: Char, +Y: String) -> {Some{PH.read_go(SCon{c, Y}, n, False{})} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}: match c: case Chr{x}: {==}# A decimal number followed by a non-digit is read back.def dec_rt(+n: Nat, +c: Char, +Y: String, +hc: {PH.starts_digit(SCon{c, Y}) == False{} : Bool}) -> {PH.read(String.append(PH.decimal(n), SCon{c, Y})) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}: +s = String.append(PH.dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n)), SCon{c, Y}) %Equal.sym(Bool, PH.starts_digit(s), True{}, sd_dec(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {PH.read_check(s, _) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>} %Equal.sym(PH.Got, PH.read_go(s, 0n, True{}), PH.read_go(SCon{c, Y}, n, PH.starts_digit(SCon{c, Y})), dec_go_rt(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {Some{_} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>} %Equal.sym(Bool, PH.starts_digit(SCon{c, Y}), False{}, hc) : {Some{PH.read_go(SCon{c, Y}, n, _)} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>} got_nd(n, c, Y)# ---------------------------------------------------------------- the PHC stringdef append_nil(+x: String) -> {String.append(x, SNil{}) == x : String}: match x: case SNil{}: {==} case SCon{+h, +t}: Equal.cong(String, String, z => SCon{h, z}, String.append(t, SNil{}), t, append_nil(t))# parse(format(x)) == Some{x}, for byte lists of bytes below 256.def parse_format(+m: Nat, +t: Nat, +p: Nat, +salt: List<&2, U32>, +hash: List<&2, U32>, +hs: {ok(salt) == True{} : Bool}, +hh: {ok(hash) == True{} : Bool}) -> {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}: %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(m), SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{m, SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(m, Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_m(_) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(t), SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{t, SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(t, Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_t(m, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(p), SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])})), Some{PH.Got{p, SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])}}}, dec_rt(p, Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)]), {==})) : {PH.parse_p(m, t, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} %Equal.sym(Maybe<&2, PH.Cut>, PH.field(String.append(PH.b64(salt), SCon{Chr{36}, String.concat([PH.b64(hash)])})), Some{PH.Cut{PH.b64(salt), String.concat([PH.b64(hash)])}}, field_b64(salt, String.concat([PH.b64(hash)]), hs)) : {PH.parse_salt(m, t, p, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} %Equal.sym(String, String.append(PH.b64(hash), SNil{}), PH.b64(hash), append_nil(PH.b64(hash))) : {PH.parse_hash(m, t, p, PH.unb64(PH.b64(salt)), PH.unb64(_)) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(salt)), Some{salt}, b64_rt(salt, hs)) : {PH.parse_hash(m, t, p, _, PH.unb64(PH.b64(hash))) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(hash)), Some{hash}, b64_rt(hash, hh)) : {PH.parse_hash(m, t, p, Some{salt}, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>} {==}