def from8_ok

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

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/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F

327def from8_ok(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +b4: U32, +b5: U32, +b6: U32, +b7: U32) -> {SF.mval(~WU.U64, ~SG.u64_val, F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(F.dig64(Some{WU.U64{0, 0}}, F.is_byte(b7), b7), F.is_byte(b6), b6), F.is_byte(b5), b5), F.is_byte(b4), b4), F.is_byte(b3), b3), F.is_byte(b2), b2), F.is_byte(b1), b1), F.is_byte(b0), b0)) == SF.from_le(8n, [v(b0), v(b1), v(b2), v(b3), v(b4), v(b5), v(b6), v(b7)]) : Maybe<&2, Nat>}:
328  +r0 = {Some{WU.U64{0, 0}} : Maybe<&2, WU.U64>}
329  +r1 = F.dig64(r0, F.is_byte(b7), b7)
330  +r2 = F.dig64(r1, F.is_byte(b6), b6)
331  +r3 = F.dig64(r2, F.is_byte(b5), b5)
332  +r4 = F.dig64(r3, F.is_byte(b4), b4)
333  +r5 = F.dig64(r4, F.is_byte(b3), b3)
334  +r6 = F.dig64(r5, F.is_byte(b2), b2)
335  +r7 = F.dig64(r6, F.is_byte(b1), b1)
336  +S0 = {Some{0n} : Maybe<&2, Nat>}
337  +S1 = SF.digit_on(S0, C.fits(8n, v(b7)), v(b7))
338  +S2 = SF.digit_on(S1, C.fits(8n, v(b6)), v(b6))
339  +S3 = SF.digit_on(S2, C.fits(8n, v(b5)), v(b5))
340  +S4 = SF.digit_on(S3, C.fits(8n, v(b4)), v(b4))
341  +S5 = SF.digit_on(S4, C.fits(8n, v(b3)), v(b3))
342  +S6 = SF.digit_on(S5, C.fits(8n, v(b2)), v(b2))
343  +S7 = SF.digit_on(S6, C.fits(8n, v(b1)), v(b1))
344  +c1 = d64_bnd(0n, {==}, r0, {==}, b7)
345  +c2 = d64_bnd(8n, {==}, r1, c1, b6)
346  +c3 = d64_bnd(16n, {==}, r2, c2, b5)
347  +c4 = d64_bnd(24n, {==}, r3, c3, b4)
348  +c5 = d64_bnd(32n, {==}, r4, c4, b3)
349  +c6 = d64_bnd(40n, {==}, r5, c5, b2)
350  +c7 = d64_bnd(48n, {==}, r6, c6, b1)
351  +e1 = hstep(0n, {==}, r0, S0, {==}, {==}, b7)
352  +e2 = hstep(8n, {==}, r1, S1, e1, c1, b6)
353  +e3 = hstep(16n, {==}, r2, S2, e2, c2, b5)
354  +e4 = hstep(24n, {==}, r3, S3, e3, c3, b4)
355  +e5 = hstep(32n, {==}, r4, S4, e4, c4, b3)
356  +e6 = hstep(40n, {==}, r5, S5, e5, c5, b2)
357  +e7 = hstep(48n, {==}, r6, S6, e6, c6, b1)
358  hstep(56n, {==}, r7, S7, e7, c7, b0)