def dec_step

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

import Base
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

1298def 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}:
1299  +q = Nat.div(n, 10n)
1300  +r = Nat.mod(n, 10n)
1301  -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
1302  %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}
1303  %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}
1304  %NR.dm_eq(9n, n) : {PH.read_go(ay, _, PH.starts_digit(ay)) == rhs : PH.Got}
1305  {==}