def d32_some

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

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

85def d32_some(+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, +c: Bool, +hc: {F.is_byte(b) == c : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, c, b)) == SF.digit_on(Some{v(z)}, C.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}:
86  match c:
87    case True{}:
88      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), True{}, fb(b), hc)
89      %Equal.sym(Bool, C.fits(8n, v(b)), True{}, hb) : {SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, True{}, b)) == SF.digit_on(Some{v(z)}, _, v(b)) : Maybe<&2, Nat>}
90      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, v(U32.add(b, U32.mul(z, 256))), Nat.add(v(b), C.shift(8n, v(z))), step32(k, hk, z, hz, b, hb))
91    case False{}:
92      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), False{}, fb(b), hc)
93      %Equal.sym(Bool, C.fits(8n, v(b)), False{}, hb) : {SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, False{}, b)) == SF.digit_on(Some{v(z)}, _, v(b)) : Maybe<&2, Nat>}
94      {==}