第2章数学基础

数学基础：命题逻辑、谓词逻辑、集合论基础、归纳法原理

各位同学，咱们今天聊点硬核的。形式化验证说白了，就是把「数学」请来给智能合约当裁判。你想想看，代码跑起来之前，先用数学逻辑推一遍，是不是比上线后等着被黑客打脸强多了？

我个人习惯，每次写合约前都会在脑子里过一遍逻辑框架。这就像盖房子先画图纸，数学基础就是你的「逻辑图纸」。咱们今天把这四块内容啃下来，后面讲形式化验证工具时，你就能理解它们为什么那么设计了。

命题逻辑，说白了就是「是」与「非」的游戏。一个命题要么真，要么假，没有中间态。比如「余额大于0」就是一个命题，它要么成立，要么不成立。

我在项目中遇到过一个问题：一个简单的转账函数，逻辑上看起来没问题，但形式化验证工具却报错了。后来发现，是命题逻辑的「蕴含关系」没处理好。嗯，这里要注意，P → Q 在逻辑上等价于 ¬P ∨ Q，这个转换在形式化验证中非常常用。

  核心运算符：
  ¬（非）：取反，真变假，假变真
∧（与）：两个都真才真
∨（或）：一个真就真
→（蕴含）：前件真则后件必须真
↔（等价）：前后真假一致

举个例子，你写一个 require 语句：

require(balance > 0 && msg.sender == owner);

这其实就是命题逻辑的「与」运算。形式化验证时，工具会把这个条件拆成两个命题，分别验证。我曾经因为少写了一个括号，导致逻辑优先级出错，被工具狠狠教育了一顿。

避坑指南： 我曾经在复杂条件判断中，把「与」和「或」混用，结果逻辑完全反了。建议你写合约时，多用括号明确优先级，别依赖默认规则。

命题逻辑只能处理「单个」事实，但合约里经常要表达「所有用户」或「存在某个地址」这样的概念。这时候就需要谓词逻辑了。

谓词逻辑引入了两个量词：

你想想看，在验证一个白名单合约时，我们需要证明「所有在白名单中的地址都可以调用某个函数」。这就是典型的全称量词应用。形式化验证工具会遍历所有可能的地址，检查条件是否成立。

我记得有一次，我在验证一个拍卖合约时，需要证明「存在一个出价最高的竞拍者」。用存在量词表达就是 ∃x: ∀y (bid(x) > bid(y))。这个看似简单的逻辑，在形式化验证中却需要仔细处理边界条件。

注意： 谓词逻辑的「量词顺序」非常重要。∀x ∃y 和 ∃y ∀x 是完全不同的含义。前者是「每个人都有一个朋友」，后者是「存在一个所有人的共同朋友」。写合约时，这种细微差别可能导致严重的逻辑漏洞。

集合论，说白了就是研究「一堆东西」的数学。在智能合约里，地址集合、余额映射、权限列表，本质上都是集合。

核心概念就几个：

我在项目中遇到过一个问题：一个合约用 mapping 来存储白名单，但验证时发现，某些地址既在白名单又在黑名单中。这就是集合的「交集」不为空，逻辑上产生了矛盾。用集合论的语言说，就是两个集合没有做到「互斥」。

实用技巧： 我个人习惯在写合约前，先用集合论画出所有状态变量的「关系图」。哪些集合互斥？哪些集合包含？画清楚了，代码逻辑自然就清晰了。

归纳法，是形式化验证中最常用的证明方法。为什么？因为合约里的循环、递归调用、状态转移，本质上都是「无限步」的操作。你不可能手动验证每一步，但归纳法可以帮你「一步到位」。

归纳法的核心思想很简单：

举个例子，验证一个累加器合约：

uint256 public total;
function add(uint256 x) public {
    total += x;
}

用归纳法证明「total 始终等于所有输入 x 之和」：

你看，就这么简单。但实际合约往往复杂得多，比如涉及多个状态变量、条件分支、外部调用。这时候归纳法的「归纳假设」就需要精心设计。

  关键点： 归纳法在形式化验证中，通常用于证明「不变式」。所谓不变式，就是合约执行过程中始终为真的条件。比如「总供应量不变」、「余额总和守恒」等。

我记得有一次，我在验证一个借贷合约时，需要证明「用户的抵押品价值始终大于借款金额」。这个不变式涉及多个变量的联动，归纳假设需要同时考虑价格波动、利息累积等因素。嗯，那一次我花了整整两天才把归纳假设写对。

常见陷阱： 归纳法最怕「循环依赖」。比如证明 A 时需要用到 B，证明 B 时又需要用到 A。这时候需要引入「强归纳法」或「嵌套归纳法」。我曾经在这个坑里爬了三天，最后发现是归纳假设的「强度」不够。

这四块数学基础，是形式化验证的「四根柱子」。命题逻辑帮你处理条件判断，谓词逻辑帮你表达「所有」和「存在」，集合论帮你理清状态关系，归纳法帮你证明无限步操作的正确性。

我个人建议，你可以在写合约时，有意识地把逻辑「翻译」成数学语言。比如看到 require 条件，就想想它对应哪个命题逻辑公式；看到 mapping，就想想它对应哪个集合运算。久而久之，你的合约逻辑会越来越严谨，形式化验证工具用起来也会得心应手。

下一章，咱们会把这些数学工具应用到实际的形式化验证工具中，比如如何用命题逻辑描述合约规范，如何用归纳法证明合约的不变式。准备好了吗？