def mid_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:254

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

254# the next 8 bits: x div 256 (x < 2^16)
255def mid_v(+x: Nat, +r: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {C.low(8n, C.high(8n, Nat.add(x, C.shift(16n, r)))) == Nat.div(x, 256n) : Nat}:
256  %Equal.sym(Nat, C.shift(16n, r), C.shift(8n, C.shift(8n, r)), Equal.sym(Nat, C.shift(8n, C.shift(8n, r)), C.shift(16n, r), SR.shift_shift(8n, 8n, r))) : {C.low(8n, C.high(8n, Nat.add(x, _))) == Nat.div(x, 256n) : Nat}
257  %Equal.sym(Nat, C.high(8n, Nat.add(x, C.shift(8n, C.shift(8n, r)))), Nat.add(C.high(8n, x), C.shift(8n, r)), WW.high_add_shift(8n, x, C.shift(8n, r))) : {C.low(8n, _) == Nat.div(x, 256n) : Nat}
258  %Equal.sym(Nat, C.low(8n, Nat.add(C.high(8n, x), C.shift(8n, r))), C.low(8n, C.high(8n, x)), WW.low_add_shift(8n, C.high(8n, x), r)) : {_ == Nat.div(x, 256n) : Nat}
259  %Equal.sym(Nat, C.low(8n, C.high(8n, x)), C.high(8n, x), WW.low_fit(8n, C.high(8n, x), fh8(x, f16))) : {_ == Nat.div(x, 256n) : Nat}
260  high8(x)