test format

Author: subfish-zhou

src/SUMMARY.md

@@ -1,12 +1,12 @@
 # Lean 4 类型检查
 
-[Type Checking in Lean 4](./title_page.md)
-[Foreword](./foreword.md)
+[Lean 4 类型检查](./title_page.md)
+[前言](./foreword.md)
 
-- [What's a kernel?](./whats_a_kernel.md)
-- [Trust](./trust/trust.md)
-    - [Unsafe declarations](./trust/unsafe_declarations.md)
-    - [Adversarial inputs](./trust/adversarial_inputs.md)
+- [什么是内核](./whats_a_kernel.md)
+- [信任](./trust/trust.md)
+    - [非安全声明](./trust/unsafe_declarations.md)
+    - [对抗性输入](./trust/adversarial_inputs.md)
 - [Export format](./export_format.md)
 - [Kernel concepts](./kernel_concepts/kernel_concepts.md)
     - [The big picture](./kernel_concepts/the_big_picture.md)

src/foreword.md

@@ -1,6 +1,6 @@
-# Foreword
+# 前言
 
-The author would like to thank:
+鸣谢：
 
 Mario Carneiro
 
@@ -12,10 +12,10 @@ Gabriel Ebner
 
 Jonathan Protzenko
 
-The [Lean Zulip](https://leanprover.zulipchat.com/) community.
+[Lean Zulip](https://leanprover.zulipchat.com/) 社区。
 
-Each and every contributor to Lean4, Mathlib, and the broader Lean ecosystem.
+每一位 Lean4、Mathlib 和 Lean 生态贡献者。
 
 ---
 
-This book is dedicated to the memory of Philip Elliot Bailey _(31 January, 1987 - 9 December, 2023)_.
+致 Philip Elliot Bailey _(1987.1.31 - 2023.12.9)_.

src/trust/adversarial_inputs.md

@@ -1,3 +1,18 @@
+# 对抗性输入
+
+在讨论“可信度”这一更宏观的问题时，人们常会提到 Lean 在面对**对抗性输入**时的稳健性。
+
+一个正确实现的类型检查器，会把它接收到的输入严格限制在 Lean 类型系统的规则之内，并尊重操作者允许使用的公理。如果操作者只准许 Lean 的三条“官方”公理（`propext`、`Quot.sound`、`Classical.choice`），那么无论在何种情况下，输入文件都不应能向类型检查器提供 Prelude 中 `False` 的证明。
+
+然而，一个**最小化**的类型检查器并不会主动防御那些“在逻辑上正确，却意在欺骗人工审阅者”的输入。举例来说，攻击者可能**重新定义**他们确信审稿人不会查看的深层依赖，或插入“Unicode 同形异义字符”，使得美化打印器的输出隐藏了对关键定义的微妙篡改。
+
+“用户以为某定理已被形式化证明，实际上却被系统的行为误导”这一风险，被称为 **Pollack 不一致性（Pollack-inconsistency）**，Freek Wiedijk 在其论文中对此进行了探讨 [^pollack]。
+
+从原理上讲，开发者完全可以编写软件，或扩展类型检查器，以抵御这类攻击——只是这些防护并不属于“内核所需的最小功能”。然而，Lean 用户对其强大的自定义语法与宏系统的广泛使用，的确给改进此方面的防护带来了一定挑战。对此，读者可将其视为一种[未来工作的开放议题](../future_work.md#improving-pollack-consistency)。
+
+[^pollack]: Freek Wiedijk, “Pollack-inconsistency”, *Electronic Notes in Theoretical Computer Science* 285 (2012): 85-100.
+
+
 # Adversarial inputs
 
 A topic that often accompanies the more general trust question is Lean's robustness against adversarial inputs.

src/trust/trust.md

@@ -1,3 +1,18 @@
+# 信任
+
+Lean 的核心价值之一在于它能够构建数学证明，包括关于程序正确性的证明。用户经常提出的一个问题是：信任 Lean 究竟需要多大程度的信任，以及具体需要信任哪些部分。
+
+这个问题的答案包含两个方面：用户需要信任哪些部分才能相信Lean中的证明，以及用户需要信任哪些部分才能相信通过编译Lean程序获得的可执行程序。
+
+具体来说，区别在于：证明（包括关于程序的陈述）和未编译的程序可以直接用Lean的内核语言表达，并由内核对实现进行检查。它们不需要被编译成可执行文件，因此信任仅限于检查它们的内核实现，而Lean编译器不属于可信代码库的一部分。
+
+信任已编译Lean程序的正确性需要信任Lean的编译器，而编译器与内核是分离的，不属于Lean的核心逻辑。信任Lean中_关于程序的陈述_与信任_Lean编译器生成的程序_是两回事。关于Lean程序的陈述是证明，属于仅需信任内核的范畴。而信任关于程序的证明_能推广到已编译程序的行为_则会将编译器纳入可信代码库。
+
+**注意**：策略（tactics）和其他元程序（metaprograms），即使是已编译的策略，也_完全不需要_被信任；它们是非可信代码，仅用于生成供其他部分使用的内核项。命题`P`可以通过任意复杂的已编译元程序在Lean中证明，而无需将可信代码库扩展到内核之外，因为元程序必须生成用Lean内核语言表达的证明。
+
++ 这些陈述适用于[导出](../export_format.md)的证明。为了让更~~挑剔~~谨慎的读者满意，这确实需要在某种程度上信任其他部分，例如运行导出器和验证器的计算机操作系统、硬件等。
+
++ 对于未导出的证明，用户还需要额外信任内核之外的Lean组件（如 elaborator、解析器等）。
 
 # Trust
 
@@ -60,3 +75,49 @@ The advantages of using external checkers are:
 + For kernel extensions, users can cross-check the results of multiple bignum/string implementations.
 
 + Using the export feature is the only way to get out of trusting the parts of Lean outside the kernel, so there's a benefit to doing this even if the export file is checked by something like [lean4lean](https://github.com/digama0/lean4lean/tree/master). Users worried about fallout from misuse of Lean's metaprogramming features are therefore encouraged to use the export feature.
+
+## 更详细的清单
+
+关于Lean 4中信任问题的更详细说明来自Mario Carneiro在Lean Zulip上的帖子。
+
+> 一般来说：
+> 
+> 1. 你需要信任Lean的逻辑是可靠的（作者注：这包括任何内核扩展，例如Nat和String的扩展）
+> 
+> 2. 如果你没有证明程序的正确性，你需要信任elaborator已将你的输入转换为符合预期的Lean表达式
+> 
+> 3. 如果你确实证明了程序的正确性，你需要信任关于程序的证明已被检查（可通过外部检查器消除此需求）
+> 
+> 4. 你需要信任运行这些程序的硬件/固件/操作系统软件没有出错或欺骗你
+> 
+> 5. （运行程序时）你需要信任硬件/固件/操作系统软件能按照规范忠实地执行程序，并且没有调试器、硬盘上的磁铁或宇宙射线干扰输出
+>
+> 对于已编译的可执行文件：
+>
+> 6. 你需要信任任何编译器覆盖（extern / implemented_by）没有违反Lean逻辑（即模型与实现匹配）
+>
+> 7. 你需要信任Lean编译器（将Lean代码降级为C代码）能保持程序的语义
+>
+> 8. 你需要信任clang/LLVM能将C程序转换为具有相同语义的可执行文件
+
+第一组要点适用于证明和已编译的可执行文件，而第二组专门针对已编译的可执行程序。
+
+## 对外部检查器的信任
+
+1. 你仍然需要信任Lean的逻辑是可靠的。
+
+2. 你需要信任外部检查器的开发者正确实现了该程序。
+
+3. 你需要信任实现语言的编译器或解释器。如果运行多个外部检查器，你可以将它们视为维恩图中的圆圈；你需要信任这些圆圈重叠的部分没有可靠性问题。
+
+4. 对于Nat和String的内核扩展，你可能需要信任一个大数库和实现语言的UTF-8字符串类型。
+
+使用外部检查器的优势包括：
+
++ 用户可以用完全独立于Lean生态系统的工具检查结果，不依赖于Lean代码库的任何部分。
+
++ 外部检查器可以利用成熟的编译器或解释器实现。
+
++ 对于内核扩展，用户可以交叉检查多个大数/字符串实现的结果。
+
++ 使用导出功能是摆脱对Lean内核之外部分信任的唯一方法，因此即使导出文件是通过[lean4lean](https://github.com/digama0/lean4lean/tree/master)等工具检查的，这样做也有好处。因此，担心滥用Lean元编程功能可能带来影响的用户被鼓励使用导出功能。

src/trust/unsafe_declarations.md

@@ -1,3 +1,20 @@
+# 非安全（unsafe）声明
+
+Lean 的表层语言允许用户编写带有 `unsafe` 标记的声明，这类声明能执行通常被禁止的操作。例如，Lean 接受下面的定义：
+
+```lean
+unsafe def y : Nat := y
+```
+
+非安全声明不会被导出 [^note1]，因此也无需被信任；并且，即便在表层语言里，它们也不能出现在正式证明中。之所以仍允许写 `unsafe` 声明，是为了让用户在编写**生成证明的辅助代码**（本身不一定是证明）时拥有更大的自由度。
+
+`aesop` 库提供了一个现实范例。[Aesop](https://github.com/leanprover-community/aesop) 是一个自动化框架，用来帮助用户生成证明。开发过程中，作者发现用**互递归归纳类型**表达系统的某部分最合适，[代码见此](https://github.com/leanprover-community/aesop/blob/69404390bdc1de946bf0a2e51b1a69f308e56d7a/Aesop/Tree/Data.lean#L375)。但这一组归纳类型在 Lean 理论里存在不合法的自引用，不会被内核接受，因此必须标记为 `unsafe`。
+
+允许将该定义作 `unsafe` 声明是一种双赢：Aesop 开发者得以继续在 Lean 中用熟悉的语法实现库，而无需另学一套元编程 DSL，也不必为取悦内核大费周章；而 Aesop 的使用者仍能导出并验证 **Aesop 生成的** 证明，而无需验证 Aesop 自身。
+
+[^note1]: 从技术上说，无法绝对阻止把 `unsafe` 声明写进导出文件（导出器本身并非可信组件），但内核在加载时会检查这些声明，若它们确实不安全，就不会把它们加入环境。若类型检查器收到含上述 Aesop 代码的导出文件，应当报错并拒绝加载。
+
+
 # Unsafe declarations
 
 Lean's vernacular allows users to write declarations marked as `unsafe`, which are permitted to do things that are normally forbidden. For example, Lean permits the following definition:

src/whats_a_kernel.md

@@ -1,3 +1,30 @@
+# 什么是 **内核**？
+
+内核是一段在软件中实现的 Lean 逻辑——也就是一段**最小化机制**的计算机程序，能够构造 Lean 逻辑语言中的对象，并验证这些对象的正确性。它的主要组成部分包括：
+
+* **名字（name）的种类**，用于寻址。
+* **宇宙层级（universe level）的种类**。
+* **表达式（expression）的种类**（λ-抽象、变量等）。
+* **声明（declaration）的种类**（公理、定义、定理、归纳类型等）。
+* **环境（environment）**：名字到声明的映射。
+* **表达式操作功能**，例如束缚变量替换、宇宙参数替换。
+* **类型检查核心操作**：类型推断、化简、判定定义等价。
+* **归纳类型相关的操作与检验**：生成类型的递归器（消除规则），以及检查构造子的定义是否与类型规范一致。
+* **可选的内核扩展**，使上述操作能够直接处理 `nat` 与 `string` 字面量。
+
+之所以要隔离一个小型内核，并要求 Lean 中的定义被翻译成一种**最简内核语言**，目的在于提高证明系统的可信度。Lean 的设计允许使用者在功能完备的证明助理中工作，享受强大的元编程、丰富的编辑器支持和可扩展语法；同时又能把构造出的证明项导出为一种形式，使人们**无需信任那些实现高级特性的代码**，也能独立验证其正确性——这些高级特性正是 Lean（作为证明助理）高效且易用的原因。
+
+在 [*Certified Programming with Dependent Types*](http://adam.chlipala.net/cpdt/) 一书第 1.2.3 节中，Adam Chlipala 提出了通常称为 \*\*de Bruijn 准则（de Bruijn criterion）\*\*或 **de Bruijn 原则**的概念：
+
+> 当证明助理即便采用复杂且可扩展的策略来搜索证明，也会输出可在小型内核语言中表达的证明项时，就满足了 “de Bruijn 准则”。这些核心语言的特性复杂度大致与形式化数学基础（如 ZF 集合论）的提案相当。要相信一个证明，我们可以无视搜索过程中的潜在错误，只依赖一个（相对较小的）**证明检查内核**来验证搜索结果。
+
+Lean 的内核足够小，小到开发者可以自行实现，并借助 **导出器（exporter）**[^1] 独立检查 Lean 中的证明。Lean 的导出格式为每个声明提供了充分信息，使得用户可以选择只实现完整内核的一部分。例如，若只对类型推断、化简和定义等价的核心功能感兴趣，就可以省略归纳类型规范检查的实现。
+
+除了上面列出的项目，外部类型检查器还需要一个针对 [Lean 导出格式](./export_format.md) 的**解析器**以及一个**美化打印器**，分别用于输入和输出。解析器与打印器并不属于内核，但若想与内核进行有意义的交互，它们就不可或缺。
+
+[^1]: 编写自己的类型检查器并非“下午茶”级别的小项目，但对于热爱探索的技术爱好者而言，绝对在可实现的范围内。
+
+
 # What is the kernel?
 
 The kernel is an implementation of Lean's logic in software; a computer program with the minimum amount of machinery required to construct elements of Lean's logical language and check those elements for correctness. The major components are: