def ud.step

bend-osdev-u32@0.1.0.0 · PROOF.bend:1774

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

1774def ud.step(+p: Nat, +a0: Bool, +b: U32, qr: Word(p) & U32, +x: Nat, +x2: Nat, +ex: {Nat.add(U.U32Nat.bit(a0), Nat.double(x)) == x2 : Nat}, ih: {Nat.add(Nat.mul(ud.q(p, qr), U32.to_nat(b)), ud.r(p, qr)) == x : Nat} & {Nat.is_lt(ud.r(p, qr), U32.to_nat(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(ud.q(1n+p, U32.divmod.go.rec(p, a0, b, qr)), U32.to_nat(b)), ud.r(1n+p, U32.divmod.go.rec(p, a0, b, qr))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.rec(p, a0, b, qr)), U32.to_nat(b)) == True{} : Bool}:
1775  match b:
1776    case U32{+bw}:
1777      match qr:
1778        case (+q, +r):
1779          match r:
1780            case U32{+rw}:
1781              (+i1, +i2) = ih
1782              ud.step2(p, a0, bw, q, rw, x, x2, ex, i1, i2)