def pk.mod_pad

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:161

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

161# a + (1 + q - (a mod (1 + q))) is a multiple of 1 + q
162def pk.mod_pad(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.add(a, Nat.sub(1n+q, Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)))), m, d, r)) == 0n : Nat}:
163  match a:
164    case 0n:
165      inv => %inv : {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.sub(1n+_, r), m, d, r)) == 0n : Nat}
166        %Equal.sym(Nat, Nat.sub(1n+Nat.add(m, r), r), 1n+m, pk.sub_add_r(m, r)) : {Pair.snd(Nat, Nat, Nat.divmod.go(_, m, d, r)) == 0n : Nat}
167        %UL.nat_add_zero(m) : {Pair.snd(Nat, Nat, Nat.divmod.go(1n+_, m, d, r)) == 0n : Nat}
168        %Equal.sym(Nat & Nat, Nat.divmod.go(1n+Nat.add(m, 0n), m, d, r), Nat.divmod.go(0n, Nat.add(m, r), 1n+d, 0n), pk.go_skip(m, 0n, d, r)) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
169        {==}
170    case 1n+ap:
171      match m:
172        case 0n:
173          inv => pk.mod_pad(ap, r, 1n+d, 0n, q)(Equal.trans(Nat, Nat.add(r, 0n), r, q, UL.nat_add_zero(r), inv))
174        case 1n+mp:
175          inv => pk.mod_pad(ap, mp, d, 1n+r, q)(Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), q, UL.nat_add_succ(mp, r), inv))