验证特点：引理，自定义谓词，逻辑函数，量化断言，逻辑宏定义，幽灵语句，多重循环

标注说明：函数前条件：对于矩阵乘 Z = X • Y，给出矩阵 X、Y 的行数和分块大小 b 的限制。宏定义给出了矩阵 X、Y 各元素的取值范围；
　　　　　函数后条件：Z = X • Y。矩阵 X、Y 的行数未变。