def dec_go_rt

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
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

1307# Reading the decimal digits of n before acc gives n and acc.
1308def 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}:
1309  match f last:
1310    case 0n _:
1311      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))
1312    case 1n+ +g True{}:
1313      %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}
1314      {==}
1315    case 1n+ +g False{}:
1316      +q = Nat.div(n, 10n)
1317      +r = Nat.mod(n, 10n)
1318      +ay = String.append(acc, Y)
1319      +hr = NR.dm_lt(9n, n)
1320      +hq = N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf))
1321      -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
1322      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,
1323        dec_go_rt(g, q, SCon{PH.dchar(r), acc}, Y, Nat.is_lt(q, 10n), {==}, hq),
1324        dec_step(n, ay, hr))