def sd_dec

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

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/src/crypto/argon2/phc.bend as PH

1288def 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}:
1289  match f last:
1290    case 0n _:
1291      Empty.absurd({PH.starts_digit(String.append(acc, Y)) == True{} : Bool}, N.lt_zero_absurd(n, hf))
1292    case 1n+ +g True{}:
1293      di_n(n, el)
1294    case 1n+ +g False{}:
1295      +q = Nat.div(n, 10n)
1296      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)))