def byte_rt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:337

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as LW
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

337# A byte is the byte of its crumbs.
338def 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}:
339  %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}
340  %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}
341  %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}
342  %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}
343  %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}
344  %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}
345  %NR.dm_eq(3n, U32.to_nat(x)) : {U32.from_nat(_) == x : U32}
346  LW.rt(x)