def from4_ok

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

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/fixed.bend as F

119def from4_ok(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> {SF.mval(~U32, ~SG.u32_val, F.from4(b0, b1, b2, b3)) == SF.from_le(4n, [v(b0), v(b1), v(b2), v(b3)]) : Maybe<&2, Nat>}:
120  +r0 = {Some{0} : Maybe<&2, U32>}
121  +r1 = F.dig32(r0, F.is_byte(b3), b3)
122  +r2 = F.dig32(r1, F.is_byte(b2), b2)
123  +r3 = F.dig32(r2, F.is_byte(b1), b1)
124  +M0 = SF.mval(~U32, ~SG.u32_val, r0)
125  +M1 = SF.mval(~U32, ~SG.u32_val, r1)
126  +M2 = SF.mval(~U32, ~SG.u32_val, r2)
127  +M3 = SF.mval(~U32, ~SG.u32_val, r3)
128  +f0 = C.fits(8n, v(b0))
129  +f1 = C.fits(8n, v(b1))
130  +f2 = C.fits(8n, v(b2))
131  +f3 = C.fits(8n, v(b3))
132  +bd1 = d32_bnd(0n, {==}, r0, {==}, b3)
133  +bd2 = d32_bnd(8n, {==}, r1, bd1, b2)
134  +bd3 = d32_bnd(16n, {==}, r2, bd2, b1)
135  +S1 = SF.digit_on(M0, f3, v(b3))
136  +S2 = SF.digit_on(S1, f2, v(b2))
137  +S3 = SF.digit_on(S2, f1, v(b1))
138  +e1 = d32_val(0n, {==}, r0, {==}, b3)
139  +e2 = Equal.trans(Maybe<&2, Nat>, M2, SF.digit_on(M1, f2, v(b2)), S2, d32_val(8n, {==}, r1, bd1, b2), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, f2, v(b2)), M1, S1, e1))
140  +e3 = Equal.trans(Maybe<&2, Nat>, M3, SF.digit_on(M2, f1, v(b1)), S3, d32_val(16n, {==}, r2, bd2, b1), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, f1, v(b1)), M2, S2, e2))
141  Equal.trans(Maybe<&2, Nat>, SF.mval(~U32, ~SG.u32_val, F.dig32(r3, F.is_byte(b0), b0)), SF.digit_on(M3, f0, v(b0)), SF.digit_on(S3, f0, v(b0)), d32_val(24n, {==}, r3, bd3, b0), Equal.cong(Maybe<&2, Nat>, Maybe<&2, Nat>, t => SF.digit_on(t, f0, v(b0)), M3, S3, e3))