def step32

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

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/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as P32

78def step32(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, +z: U32, +hz: {C.fits(k, v(z)) == True{} : Bool}, +b: U32, +hb: {C.fits(8n, v(b)) == True{} : Bool}) -> {v(U32.add(b, U32.mul(z, 256))) == Nat.add(v(b), C.shift(8n, v(z))) : Nat}:
79  +sz = C.shift(8n, v(z))
80  +f0 = Equal.trans(Bool, C.fits(32n, sz), C.fits(32n, Nat.add(0n, sz)), True{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), sz, Nat.add(0n, sz), Equal.sym(Nat, Nat.add(0n, sz), sz, P32.zero_add(sz))), to32(k, hk, Nat.add(0n, sz), step_fits(k, 0n, v(z), {==}, hz)))
81  +em = Equal.trans(Nat, v(U32.mul(z, 256)), C.low(32n, Nat.mul(v(z), 256n)), sz, P32.mul_low(z, 256), Equal.trans(Nat, C.low(32n, Nat.mul(v(z), 256n)), C.low(32n, sz), sz, Equal.cong(Nat, Nat, t => C.low(32n, t), Nat.mul(v(z), 256n), sz, Equal.sym(Nat, sz, Nat.mul(v(z), 256n), WW.shift_mul(8n, v(z)))), WW.low_fit(32n, sz, f0)))
82  +ea = Equal.trans(Nat, v(U32.add(b, U32.mul(z, 256))), C.low(32n, Nat.add(v(b), v(U32.mul(z, 256)))), C.low(32n, Nat.add(v(b), sz)), P32.add_low(b, U32.mul(z, 256)), Equal.cong(Nat, Nat, t => C.low(32n, Nat.add(v(b), t)), v(U32.mul(z, 256)), sz, em))
83  Equal.trans(Nat, v(U32.add(b, U32.mul(z, 256))), C.low(32n, Nat.add(v(b), sz)), Nat.add(v(b), sz), ea, WW.low_fit(32n, Nat.add(v(b), sz), to32(k, hk, Nat.add(v(b), sz), step_fits(k, v(b), v(z), hb, hz))))