def step64

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbytes.bend:278

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as P32

278def step64(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool}, +z: WU.U64, +hz: {C.fits(k, SG.u64_val(z)) == True{} : Bool}, +b: U32, +hb: {C.fits(8n, v(b)) == True{} : Bool}) -> {SG.u64_val(X.add(WU.U64{b, 0}, X.mul(z, WU.U64{256, 0}))) == Nat.add(v(b), C.shift(8n, SG.u64_val(z))) : Nat}:
279  +vz = SG.u64_val(z)
280  +sz = C.shift(8n, vz)
281  +mz = X.mul(z, WU.U64{256, 0})
282  +bz = {WU.U64{b, 0} : WU.U64}
283  +f0 = Equal.trans(Bool, C.fits(64n, sz), C.fits(64n, Nat.add(0n, sz)), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), sz, Nat.add(0n, sz), Equal.sym(Nat, Nat.add(0n, sz), sz, P32.zero_add(sz))), to64(k, hk, Nat.add(0n, sz), step_fits(k, 0n, vz, {==}, hz)))
284  +em = Equal.trans(Nat, SG.u64_val(mz), C.low(64n, Nat.mul(vz, 256n)), sz, WA.mul_value(z, WU.U64{256, 0}), Equal.trans(Nat, C.low(64n, Nat.mul(vz, 256n)), C.low(64n, sz), sz, Equal.cong(Nat, Nat, t => C.low(64n, t), Nat.mul(vz, 256n), sz, Equal.sym(Nat, sz, Nat.mul(vz, 256n), WW.shift_mul(8n, vz))), WW.low_fit(64n, sz, f0)))
285  +eb2 = Equal.trans(Nat, SG.u64_val(bz), Nat.add(v(b), 0n), v(b), {==}, N.add_zero(v(b)))
286  +ea = Equal.trans(Nat, SG.u64_val(X.add(bz, mz)), C.low(64n, Nat.add(SG.u64_val(bz), SG.u64_val(mz))), C.low(64n, Nat.add(v(b), sz)), WA.add_value(bz, mz), Equal.trans(Nat, C.low(64n, Nat.add(SG.u64_val(bz), SG.u64_val(mz))), C.low(64n, Nat.add(v(b), SG.u64_val(mz))), C.low(64n, Nat.add(v(b), sz)), Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, SG.u64_val(mz))), SG.u64_val(bz), v(b), eb2), Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(v(b), t)), SG.u64_val(mz), sz, em)))
287  Equal.trans(Nat, SG.u64_val(X.add(bz, mz)), C.low(64n, Nat.add(v(b), sz)), Nat.add(v(b), sz), ea, WW.low_fit(64n, Nat.add(v(b), sz), to64(k, hk, Nat.add(v(b), sz), step_fits(k, v(b), vz, hb, hz))))