使用Lean进行形式验证入门（第一部分）

# 教程：使用 Lean 进行形式化验证入门（第一部分）- HashCloak 来源：https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1) 形式化验证是一种验证数学陈述正确性的工具。我们通常用纸笔书写数学证明，但也可以使用形式化验证工具将证明写成代码，并由机器检查，从而确保证明的正确性。这类工具的例子有 **Rocq** (https://rocq-prover.org/)（原名 Coq）、**Isabelle** (https://isabelle.in.tum.de/)，以及本教程的主题 **Lean** (https://lean-lang.org/)。 在本教程中，我们将用 Lean 编写一些简单的密码学陈述及其证明。这旨在让刚接触形式化验证或想重温基础知识的密码学工程师感到有趣。具体来说，我们将从头学习 Lean 的基础知识，然后形式化验证一次一密（OTP）协议，该协议最早由 **Claude Shannon** (https://en.wikipedia.org/wiki/Claude_Shannon) 推广，但更早由 **Frank Miller** (https://www.cs.columbia.edu/~CS4HS/talks/FrankMillerOneTimePad.pdf) 和 **Gilbert Vernam** (https://en.wikipedia.org/wiki/Gilbert_Vernam) 描述。 本教程的目标是将关于简单密码学协议（如一次一密）的形式化定义和证明移植到 Lean。我们使用 Dan Boneh 和 Victor Shoup 的《A Graduate Course in Applied Cryptography》(https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf) 作为定义和证明的主要来源。学完本教程后，你应该能够理解其他形式化的密码学 Lean 证明，例如来自 **VCV-io** (https://github.com/Verified-zkEVM/VCV-io) 的证明。 > 免责声明：本文绝非意在提供 Lean 的最佳实践，而只是希望为密码学人士带来有趣且易懂的入门介绍。 ## Lean 编程语言与证明助手 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#the-lean-programming-language-proof-assistant) **Lean** (https://lean-lang.org/) 由 **Leonardo de Moura** (https://leodemoura.github.io/) 于 2013 年创建，当时他在微软研究院工作。它是一种函数式编程语言和定理证明器。数学家可以用它来写下公理、引理和定理，并在需要时添加证明。如果证明被 Lean 编译器编译通过，就意味着它是正确的（假设我们信任 Lean 编译器）。除了可检查的证明之外，其优点还在于可以更容易地将证明分解为子证明并进行协作。此外，Lean 可以通过自动搜索和应用缺失的部分来帮助你完成证明。 然而，Lean 也“只是”一种编程语言。具体来说，它是一种纯函数式编程语言，这意味着它的程序没有副作用，函数被视为一等公民。我们将在教程中进一步了解后者。 有许多优秀的资源可以帮助你入门 Lean。这里列举几个： - 面向初学者的书籍与练习：《The Hitchhiker’s Guide to Logical Verification》(https://github.com/lean-forward/logical_verification_2025) - Lean 官网的入门书籍： - 《Functional Programming in Lean》(https://lean-lang.org/functional_programming_in_lean/)：如果你已经了解函数式编程，这本书非常合适。 - 《Theorem Proving in Lean 4》(https://lean-lang.org/theorem_proving_in_lean4/)：更偏数学方向。 - 《Natural Numbers Game》(https://adam.math.hhu.de/#/g/leanprover-community/nng4)：一个交互式游戏，可以直接在浏览器中学习在 Lean 中证明。 （我之所以在已有如此多优秀资源的情况下创建这个特定练习，是因为它特别与密码学相关；VCV-io 拥有出色的密码学证明，但对初学者来说太高级了，而且没有教程。） ## 教程 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#tutorial) 让我们开始吧。本教程在快速完成“Hello World!” 之后分为 4 个部分（第二部分最长）。所有内容都基于 Lean 4，建议你跟着编码。所有带行号的代码都是最终结果所需的代码。没有行号的代码尚未完成或仅用于检查，可以安全删除。最后，每个子节开头都有一个简短注释，介绍该节涉及的新概念。 ## Hello World in Lean (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#hello-world-in-lean) > - Lean InfoView > - `#eval` 你可以在本地安装 Lean，或使用在线编辑器，例如 https://live.lean-lang.org/，它看起来像下图这样。左侧是编写 Lean 代码的区域，右侧是 Lean InfoView，显示有用的信息和提示。 要确保一切正常，可以写类似这样的内容，并验证右侧 InfoView 中是否显示了结果。对于传统的“Hello World!”，我们可以选择以下任一方式： ```lean #eval "Hello World!" #eval String.append "Hello " "World!" #eval String.append "Hello " (if 1 > 2 then "Lean!" else "World!") ``` Lean 的一些特性： - 遵循标准的数学约定：例如 `#eval 4 + 5 * 6` 计算为 4+(5*6)=34 - 函数参数不需要括号，即 Lean 中写 `f x` 而不是 `f(x)` - 函数是 Lean 中的一等公民，它们与数字或字符串等任何值一样被对待 但我们别操之过急；我们将边学边掌握每个必要的 Lean 主题。 ## 书上怎么说？即我们想移植什么到 Lean？ (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#what-does-the-book-say-i.e.-what-do-we-want-to-port-to-lean) 我们大致知道要定义什么，但关键在于使用 Lean 需要清晰和精确。我们到底想定义什么？如何精确定义它？这就是为什么我们使用 **Boneh & Shoup** 的书 (https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf)，所需的数学已经写好，我们只需操心如何将其翻译成 Lean。 首先，香农密码的定义 (第 2.1.1 节 (https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf)) 具有 3 个属性。前两个告诉我们加密和解密函数是什么，最后一个属性是正确性，即解密加密后的结果应返回原始消息。 我们感兴趣的具体例子是一次一密，其中加密和解密只是 XOR 操作： 本教程的很大一部分将致力于证明按位异或 (XOR) 的性质： 最后，我们可以通过证明一次一密符合正确性属性来表明它是一个香农密码： 对于本教程的第一部分，我们将完成以下简单步骤： 1. 定义位串和 XOR 函数 2. 证明 XOR 的必要性质 - 交换律 - 结合律 - 单位元 - 自逆性 3. 定义香农密码，包含 - 加密函数 - 解密函数 - 解密“逆转”加密的属性（正确性） 4. 证明一次一密（其中加密和解密都是 XOR）是一个香农密码 准备好开始了吗？让我们开始吧。 ## 教程第一部分：定义 BitString 和 XOR (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#tutorial-part-1-define-a-bitstring-and-xor) 一次一密将定义在密钥 K、消息 M 和密文 C 上，它们都是相同长度 L 的位串：K := M := C := {0,1}^L。在 XOR 的定义中，我们需要模 2 加法。因此将 {0,1}^L 视为 Z2^L 并在 Lean 中使用 Z2 上的算术会很有帮助。 ### 有限域 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#finite-fields) > - 导入库 > - `ZMod n` 首先，从 Lean 的数学库中导入有限域库 `ZMod`： ```lean import Mathlib.Data.ZMod.Basic ``` 在这个预定义库中，`ZMod n` 定义了整数模 n，它已经预先实现了模算术。（你可以按住 Cmd/Ctrl 并点击来查看更多已实现类型的信息，例如查看 `ZMod n` (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/ZMod/Defs.html)。） 尝试一些简单的模算术来熟悉 `ZMod`，例如 5 + 6 mod 7： ```lean #eval (5: ZMod 7) + (6: ZMod 7) ``` 现在我们可以通过创建一个新的类型来定义 K、M、L 的定义域，该类型是 `ZMod 2` 元素的向量。 ### BitString 定义 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#bitstring-definition) > - `Vector` > - 依赖类型 > - `#check` Lean 的一个优点是我们可以不固定位串长度 `L`；只需说 `L` 属于 N，就像在数学中一样（输入 `\N` 在 Lean 中写 N）。预定义类型 `Vector α n` 创建了一个长度为 `n`、元素类型为 `α` 的向量。因此我们可以使用 `Vector (ZMod 2) L` 来定义我们的自定义类型 Z2^L： ```lean def BitString (L: N): Type := Vector (ZMod 2) L ``` 这是一个依赖类型，对于 N 中不同的 `L` 值会给出不同的实例化。我们可以检查它（在 Lean 中用 `--` 前缀注释）： ```lean #check BitString 5 --BitString 5 : Type ``` 注意 `#eval` 不起作用，因为没有要计算的内容，但 `#check` 会显示表达式的类型，在这里效果很好。 ### XOR 定义 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#xor-definition) > - 隐式参数 > - 柯里化 > - Lambda 函数 现在定义函数 `xor`，输入位串 x = [x_1, ..., x_L] 和 y = [y_1, ..., y_L]，输出为 [x_1 +2 y_1, ..., x_L +2 y_L]，其中 +2 是模 2 加法。如何在 Lean 中定义它？想一想数学中的函数签名：Z2^L × Z2^L → Z2^L。有几种方法可以实现（在 Lean 中总是有多种方法达到相同目的），我们将采用： ```lean def xor {L: N} (x y: BitString L): (BitString L) ``` 这里，参数 `L` 是**隐式的** (https://lean-lang.org/functional_programming_in_lean/Getting-to-Know-Lean/Polymorphism/#implicit-parameters)。现在我们需要“函数体”。为了简便地遍历两个输入向量并逐分量相加，我们可以使用预定义的函数 `zipWith`，它适用于向量。让我们理解 `zipWith` 的类型： ```lean def zipWith (f : α → β → φ) (as : Vector α n) (bs : Vector β n) : Vector φ n ``` 它接受一个函数 `f` 和两个向量 `as` 和 `bs`，返回一个与 `as` 和 `bs` 长度相同的向量。注意向量元素的类型可以不同（虽然 `xor` 并非如此）。函数类型 `f : α → β → φ` 意味着：它接受一个 `α` 类型的元素和一个 `β` 类型的元素，并返回一个 `φ` 类型的元素。在数学中我们会写成 α × β → φ。Lean 采用的方法称为**柯里化** (https://en.wikipedia.org/wiki/Currying)；一个多参数函数被表示为一串函数，每个函数只接受一个参数。这意味着你可以部分应用，使得代码非常灵活。因此我们可以将 `f : α → β → φ` 解读为 `f : α → (β → φ)`，这表明当你给它第一个类型为 `α` 的元素时，你得到一个函数 `β → φ`，然后你再给它一个类型为 `β` 的元素，最终得到类型为 `φ` 的输出。 所以 `zipWith` 的作用是并行遍历两个向量，并对当前的两个元素执行操作 `f`。对于 `xor`，我们希望它遍历 `x` 和 `y` 并将它们模 2 相加。 ```lean def xor {L: N} (x y: BitString L): (BitString L) := -- TODO 定义 f Vector.zipWith f x y ``` 最后的难题是如何定义我们想要传递给 `zipWith` 的函数 `f`，我们知道它需要对元素进行加法运算。我们可以使用 **lambda 函数** (https://lean-lang.org/functional_programming_in_lean/Getting-to-Know-Lean/Additional-Conveniences/#anonymous-functions)，它可以这样紧凑地写：`fun x => x + 1`（例如，返回自然数的后继）。合在一起： ```lean def xor {L: N} (x y: BitString L): (BitString L) := Vector.zipWith (fun a b => a + b) x y ``` 注意这将正确工作，因为 `BitString` 的类型元素属于 Z2，因此加法将自动是模 2 加法。 ## 教程第二部分：证明 XOR 的性质 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#tutorial-part-2-prove-properties-of-xor) 好的，真正的乐趣开始了！为了清晰起见，你现在至少应该有以下内容： ```lean import Mathlib.Data.ZMod.Basic def BitString (L: N): Type := Vector (ZMod 2) L def xor {L: N} (x y: BitString L): (BitString L) := Vector.zipWith (fun a b => a + b) x y ``` 或者任何其他对你有效的等价版本！我们将再添加一行，**在** `xor` **定义之前**： ```lean open scoped hiding xor ``` 这将确保在开始证明时，Lean 不会与另一个已有的 `xor` 定义混淆。😅 继续跟随 Boneh & Shoup 的书，我们现在将证明 XOR 定义（例 2.1 (https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf)）中提到的性质，从交换律开始： ### 证明 XOR 的交换律：`x ⊕ y = y ⊕ x` (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#prove-commutativity-of-xor-x-%E2%8A%95-y-y-%E2%8A%95-x) 我们先证明 XOR 的交换律，即 `x ⊕ y = y ⊕ x`。这个第一个性质将花费最多时间，因为它包含本教程的第一个 Lean 证明。它分为 3 个步骤。 #### 定义交换律引理 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#define-lemma-for-commutativity) > - Lean 中的目标 > - 引理定义 > - `sorry` 我们将交换律性质定义为一个引理然后证明它。一旦写下了引理，Lean 就会称它为“目标”，即有待证明的东西。你的任务是将当前目标归约为一个或多个更小的子目标，这些子目标更接近你已经知道为真的事实。证明你的陈述就变成了一个归约链，类似于将编程问题分解为更小的子问题。 Lean 中引理（或定理）的组成： ```lean lemma <名字> <参数> : <陈述> := <证明> ``` 在本例中，`<参数>` 包含两个 BitString：`x` 和 `y`。`<陈述>` 应表达我们想要证明的 `x` 和 `y` 的交换律性质：`xor x y = xor y x`。引理的名字取决于个人偏好；我选了简洁的 `xor_comm_property`。注意对于 BitString，我们需要隐式参数 `L`： ```lean lemma xor_comm_property {L: N} (x y : BitString L) : xor x y = xor y x := sorry -- 在添加证明之前，这是占位符 ``` `sorry` 占位符并非我的独创，这确实是 Lean 的占位符，可以理解为“抱歉，我还没证明它”。 #### 证明交换律引理：第一步 (https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)#prove-lemma-commutativity-step-1) > - 策略，`by` > - `⊢` > - `Vector.ext` 我们将使用**策略** (https://lean-lang.org/theorem_proving_in_lean4/Tactics/#Theorem-Proving-in-Lean-4--Tactics) 来构建证明：这些指令有助于归约当前目标。你可以应用许多不同的步骤，例如： - 将目标重写为等价形式 - 将目标拆分为多个子目标 - 当目标匹配某个已知事实时关闭它 我们首先移除 `sorry` 并用 `by` 替换，这表明我们将使用策略来证明。这很有用，因为 Lean 会