def ud.fin

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

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

1763def ud.fin(+p: Nat, +q: Word(p), +s: Word(32n), +bw: Word(32n), +T: Bool, +g: Bool, +a0: Bool, +rw: Word(32n), +x: Nat, +x2: Nat, +eg: {Bool.or(T, U32.is_ge(U32{s}, U32{bw})) == g : Bool}, +eput: {Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, U.U32Nat.bit(T))) == Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))) : 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.fin(p, q, U32{s}, U32{bw}, g)), U32.to_nat(U32{bw})), ud.r(1n+p, U32.divmod.go.fin(p, q, U32{s}, U32{bw}, g))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.fin(p, q, U32{s}, U32{bw}, g)), U32.to_nat(U32{bw})) == True{} : Bool}:
1764  match g:
1765    case True{}:
1766      ud.fin.t(p, q, bw, a0, rw, x, x2, U32.to_nat(U32.sub(U32{s}, U32{bw})), ex, i1, ud.k(32n, Word.to_nat(32n, s), Word.to_nat(32n, bw), Word.to_nat(32n, rw), U.U32Nat.bit(a0), U32.to_nat(U32.sub(U32{s}, U32{bw})), T, U32.is_lt(U32{s}, U32{bw}), True{}, eput, Equal.sym(Bool, U32.is_lt(U32{s}, U32{bw}), Nat.is_lt(Word.to_nat(32n, s), Word.to_nat(32n, bw)), Laws.u32_lt_value(U32{s}, U32{bw})), Equal.trans(Bool, Bool.or(T, Bool.not(U32.is_lt(U32{s}, U32{bw}))), Bool.or(T, U32.is_ge(U32{s}, U32{bw})), True{}, Equal.cong(Bool, Bool, zz => Bool.or(T, zz), Bool.not(U32.is_lt(U32{s}, U32{bw})), U32.is_ge(U32{s}, U32{bw}), Equal.sym(Bool, U32.is_ge(U32{s}, U32{bw}), Bool.not(U32.is_lt(U32{s}, U32{bw})), un.ge_lt(U32.cmp(U32{s}, U32{bw})))), eg), Equal.trans(Nat, Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), Nat.mul(1n, Word.to_nat(32n, bw))), Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw})))), Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, Nat.mul(1n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))))), Equal.trans(Nat, Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), Nat.mul(1n, Word.to_nat(32n, bw))), Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), Word.to_nat(32n, bw)), Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw})))), Equal.cong(Nat, Nat, zz => Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), zz), Nat.mul(1n, Word.to_nat(32n, bw)), Word.to_nat(32n, bw), ur.r32(Word.to_nat(32n, bw))), Laws.u32_sub_wrap(U32{s}, U32{bw})), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, zz)), U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw})), Nat.mul(1n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))), ur.r33(U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))))), un.bit_le(a0), i2, Laws.word_value_lt(32n, bw)))
1767    case False{}:
1768      ud.fin.f(p, q, bw, a0, rw, x, x2, Word.to_nat(32n, s), ex, i1, ud.k(32n, Word.to_nat(32n, s), Word.to_nat(32n, bw), Word.to_nat(32n, rw), U.U32Nat.bit(a0), Word.to_nat(32n, s), T, U32.is_lt(U32{s}, U32{bw}), False{}, eput, Equal.sym(Bool, U32.is_lt(U32{s}, U32{bw}), Nat.is_lt(Word.to_nat(32n, s), Word.to_nat(32n, bw)), Laws.u32_lt_value(U32{s}, U32{bw})), Equal.trans(Bool, Bool.or(T, Bool.not(U32.is_lt(U32{s}, U32{bw}))), Bool.or(T, U32.is_ge(U32{s}, U32{bw})), False{}, Equal.cong(Bool, Bool, zz => Bool.or(T, zz), Bool.not(U32.is_lt(U32{s}, U32{bw})), U32.is_ge(U32{s}, U32{bw}), Equal.sym(Bool, U32.is_ge(U32{s}, U32{bw}), Bool.not(U32.is_lt(U32{s}, U32{bw})), un.ge_lt(U32.cmp(U32{s}, U32{bw})))), eg), ur.r34(Word.to_nat(32n, s), Word.to_nat(32n, bw), U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))), un.bit_le(a0), i2, Laws.word_value_lt(32n, bw)))