def ud.step2

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

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

1770def ud.step2(+p: Nat, +a0: Bool, +bw: Word(32n), +q: Word(p), +rw: Word(32n), +x: Nat, +x2: Nat, +ex: {Nat.add(U.U32Nat.bit(a0), Nat.double(x)) == x2 : Nat}, +i1: {Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)) == x : Nat}, +i2: {Nat.is_lt(Word.to_nat(32n, rw), Word.to_nat(32n, bw)) == True{} : Bool}) -> {Nat.add(Nat.mul(ud.q(1n+p, U32.divmod.go.shl(p, q, U32{bw}, Word.shl.out(32n, a0, rw))), U32.to_nat(U32{bw})), ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, Word.shl.out(32n, a0, rw)))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, Word.shl.out(32n, a0, rw))), U32.to_nat(U32{bw})) == True{} : Bool}:
1771  %Equal.sym(Bool & Word(32n), Word.shl.out(32n, a0, rw), (un.topc(32n, a0, rw), Word.shl.put(32n, a0, rw)), un.so(32n, a0, rw)) : {Nat.add(Nat.mul(ud.q(1n+p, U32.divmod.go.shl(p, q, U32{bw}, _)), U32.to_nat(U32{bw})), ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, _))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.shl(p, q, U32{bw}, _)), U32.to_nat(U32{bw})) == True{} : Bool}
1772  ud.fin(p, q, Word.shl.put(32n, a0, rw), bw, un.topc(32n, a0, rw), Bool.or(un.topc(32n, a0, rw), U32.is_ge(U32{Word.shl.put(32n, a0, rw)}, U32{bw})), a0, rw, x, x2, {==}, un.putv(32n, a0, rw), ex, i1, i2)