def pos_shift

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bounds.bend:28

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/crypto/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

28# 2^(16 n) y
29def pos_shift(n: Nat, +y: Nat) -> {LV.pos(n, y) == C.shift(Nat.mul(n, 16n), y) : Nat}:
30  match n:
31    case 0n:
32      {==}
33    case 1n+ +k:
34      %Equal.sym(Nat, LV.pos(k, y), C.shift(Nat.mul(k, 16n), y), pos_shift(k, y)) : {C.shift(16n, _) == C.shift(Nat.add(16n, Nat.mul(k, 16n)), y) : Nat}
35      %Equal.sym(Nat, C.shift(Nat.add(16n, Nat.mul(k, 16n)), y), C.shift(16n, C.shift(Nat.mul(k, 16n), y)), Equal.sym(Nat, C.shift(16n, C.shift(Nat.mul(k, 16n), y)), C.shift(Nat.add(16n, Nat.mul(k, 16n)), y), SR.shift_shift(16n, Nat.mul(k, 16n), y))) : {C.shift(16n, C.shift(Nat.mul(k, 16n), y)) == _ : Nat}
36      {==}