def wb.or_bit

bend-osdev-word64@0.1.1.0 · PROOF_bits.bend:193

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 UL
import bend-osdev-word64@0.1.1.0/word64.bend as W

193def wb.or_bit(+x: W.W64, +c: U32, +hc: {Nat.is_lt(U32.to_nat(c), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {W.W64.to_nat(W.W64.or(W.W64.shl(x, 1n), W.W64.from_u32(c))) == Nat.add(W.W64.to_nat(W.W64.shl(x, 1n)), U32.to_nat(c)) : Nat}:
194  match x:
195    case W.W64{+h, +l}:
196      Equal.trans(Nat, Nat.add(U32.to_nat(U32.or(U32.shln(l, 1n), c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))))), U32.to_nat(c)), Equal.trans(Nat, Nat.add(U32.to_nat(U32.or(U32.shln(l, 1n), c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)))), U32.to_nat(U32.or(U32.shln(l, 1n), c)), Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), UL.u32_or_split(U32.shln(l, 1n), c, 1n, U.U32Nat.low(31n, U32.to_nat(l)), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), Nat.double(U.U32Nat.low(31n, U32.to_nat(l))), U.U32Nat.dbl(1n, U.U32Nat.low(31n, U32.to_nat(l))), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), Nat.double(U.U32Nat.low(31n, U32.to_nat(l))), Equal.trans(Nat, U32.to_nat(U32.shln(l, 1n)), U.U32Nat.low(32n, U.U32Nat.dbl(1n, U32.to_nat(l))), U.U32Nat.low(32n, Nat.double(U32.to_nat(l))), UL.u32_shln_low(l, 1n), {==}), UL.low_double(31n, U32.to_nat(l))), {==}), hc)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c)), U.U32Nat.dbl(32n, zz)), U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n), Equal.trans(Nat, U32.to_nat(U32.or(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), U32.to_nat(0)), Nat.add(U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), 0n), UL.u32_or_split(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)), 0, 0n, U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n))), {==}, {==}), {==}))), wr.b5(U32.to_nat(U32.shln(l, 1n)), U32.to_nat(c), U32.to_nat(U32.or(U32.shln(h, 1n), U32.shrn(l, 31n)))))