Fixbytes.step64: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as Fixbytes
Lines 278-287 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&start_line=278&end_line=287

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

def 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}:
  +vz = SG.u64_val(z)
  +sz = C.shift(8n, vz)
  +mz = X.mul(z, WU.U64{256, 0})
  +bz = {WU.U64{b, 0} : WU.U64}
  +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)))
  +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)))
  +eb2 = Equal.trans(Nat, SG.u64_val(bz), Nat.add(v(b), 0n), v(b), {==}, N.add_zero(v(b)))
  +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)))
  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))))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend&name=zero_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=step_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=to64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=add_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=mul_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/generic.bend&name=u64_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=mul