def high8

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

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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
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/limbs.bend as LV

225def high8(+n: Nat) -> {C.high(8n, n) == Nat.div(n, 256n) : Nat}:
226  +lo = C.low(8n, n)
227  +hi = C.high(8n, n)
228  +e = Equal.trans(Nat, n, Nat.add(lo, C.shift(8n, hi)), Nat.add(Nat.mul(hi, 256n), lo), WW.low_high(8n, n), Equal.trans(Nat, Nat.add(lo, C.shift(8n, hi)), Nat.add(C.shift(8n, hi), lo), Nat.add(Nat.mul(hi, 256n), lo), NA.add_comm(lo, C.shift(8n, hi)), Equal.cong(Nat, Nat, z => Nat.add(z, lo), C.shift(8n, hi), Nat.mul(hi, 256n), Equal.sym(Nat, Nat.mul(hi, 256n), C.shift(8n, hi), LV.m256(hi)))))
229  %Equal.sym(Nat, n, Nat.add(Nat.mul(C.high(8n, n), 256n), C.low(8n, n)), e) : {C.high(8n, n) == Nat.div(_, 256n) : Nat}
230  Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(hi, 256n), lo), 256n), hi, NR.div_of(hi, 255n, lo, WW.low_lt(8n, n)))