def split256

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:26

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/src/crypto/secp256k1/limbs.bend as L
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B

26# x = lo + hi 2^256 for lo, hi the first 16 limbs and the rest
27def split256(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>) -> {LV.ev(xs) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat}:
28  %Equal.sym(Nat, LV.ev(xs), Nat.add(LV.ev(L.take(16n, xs)), LV.pos(16n, LV.ev(L.drop(16n, xs)))), LV.take_drop_v(16n, xs)) : {_ == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat}
29  %Equal.sym(Nat, LV.pos(16n, LV.ev(L.drop(16n, xs))), C.shift(256n, LV.ev(L.drop(16n, xs))), B.pos16(LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat}
30  %Equal.sym(Nat, C.shift(256n, LV.ev(L.drop(16n, xs))), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one)), WW.shift_mul_one(256n, one, h1, LV.ev(L.drop(16n, xs)))) : {Nat.add(LV.ev(L.take(16n, xs)), _) == Nat.add(LV.ev(L.take(16n, xs)), Nat.mul(LV.ev(L.drop(16n, xs)), C.shift(256n, one))) : Nat}
31  {==}