def d32_sbnd

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

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

96def d32_sbnd(+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}) -> {bnd(Nat.add(8n, k), SF.mval(~U32, ~SG.u32_val, F.dig32(Some{z}, c, b))) == True{} : Bool}:
97  match c:
98    case True{}:
99      +hb = Equal.trans(Bool, C.fits(8n, v(b)), F.is_byte(b), True{}, fb(b), hc)
100      %Equal.sym(Nat, v(U32.add(b, U32.mul(z, 256))), Nat.add(v(b), C.shift(8n, v(z))), step32(k, hk, z, hz, b, hb)) : {C.fits(Nat.add(8n, k), _) == True{} : Bool}
101      step_fits(k, v(b), v(z), hb, hz)
102    case False{}:
103      {==}