宣布SAW对Isabelle的支持

# 宣布 SAW 支持 Isabelle 来源: https://www.galois.com/articles/announcing-isabelle-support-for-saw 我们很高兴地宣布，SAW (https://tools.galois.com/saw) 现在支持从 Cryptol (https://tools.galois.com/cryptol) 规范生成 Isabelle (https://isabelle.in.tum.de/) 理论——这是 Galois 与 Apple 合作开发的新功能。 Cryptol 和 SAW 提供了一条简单、可用、半自动化路径，用于创建、分析和验证密码协议，但在可自动证明的内容上存在限制。像 Isabelle 这样的交互式定理证明器 (ITP) 表达力强得多，但复杂且学习曲线陡峭。SAW 从 Cryptol 生成 Isabelle 理论的新能力兼具两者优势：将 SAW 和 Cryptol 的易用性与 Isabelle 的表达力相结合 [1]。 - 一个新的 SAW 命令：write_isabelle_cryptol_modules（需要 enable_experimental） - 一个新的 SAW 策略：offline_isabelle（需要 enable_experimental） - 一个独立的 cryptol-to-isabelle 可执行文件，用于独立地将 Cryptol 模块翻译为 Isabelle - 一个前奏 Isabelle 理论，实现了 Cryptol 原语 - 对 Cryptol 原语的代码生成器和 quickcheck 支持 - 一个用于推理 Cryptol 规范的 Isabelle 支持理论库 ## 支持的内容： - 所有 Cryptol 内置操作、类型和类，不包括无限流 - 类型签名约束，将复杂约束推迟为证明义务 - Cryptol 记录，表示为 Isabelle 记录 - 通过用户提供的终止证明实现互递归 Cryptol 函数 - 类型级算术，逻辑等价类型的值之间的隐式强制转换 ## 尚未支持的内容： - 任意 SAWCore 项——源必须是 Cryptol 模块或包含已定义 Cryptol 函数和原语的简单 SAWCore 项 - inf 类型——所有位向量必须具有具体长度，或约束为有限 - newtype 被翻译为类型别名，而不是不同的类型 - 子模块 - 外部函数调用 ## 示例输出 `` cryptol_definition toInt :: "{'n} ((fin 'n) =?> ((['n]) ⇒ Integer))" where "toInt x ≡ foldr`{'n,Bit,Integer} (λ(y :: Bit) (b :: Integer). ((if y then 1 else 0 :: Integer) +`{Integer} ((2 :: Integer) *`{Integer} b))) (0 :: Integer) (reverse`{'n,Bit} x)" `` ## 背景 ### Cryptol Cryptol (https://tools.galois.com/cryptol) 是由 Galois 开发的一种编程语言，用于创建、分析和验证复杂的密码算法。它提供简单的接口，使用户能够轻松地用数学语言描述算法，并指定和证明关于算法的性质。Cryptol 的证明是自动化的，基于 SMT 求解器（如 Z3），这提供了简单性和易用性，但以可证明内容受限为代价。 #### 示例 `` module toInt where toInt : {n} (fin n) => [n] -> Int toInt x = foldr (\y b -> (if y then 1 else 0) + 2 * b) 0 (reverse x) toInt_valid : {n} (fin n) => [n] -> Bit property toInt_valid x = toInt x == toInteger x `` 在此示例中，toInt 是一个将任意长度的固定宽度位向量转换为等价整数的函数。性质 toInt_valid 表明 toInt 应始终与 Cryptol 原语 toInteger 给出相同的结果。 我们可以直接从 Cryptol REPL 轻松证明该性质对任何具体位向量宽度成立： `` cryptol> :l toInt.cry toInt> :prove toInt_valid`{16} Q.E.D. `` ### SAW SAW 同样由 Galois 开发，是一个用于证明软件性质的多工具，支持多种输入语言并整合了多种指定和证明性质的解决方案。SAW 的一个关键组件是与 Cryptol 的深度集成，Cryptol 充当 SAW 的主要规范语言。与 Cryptol 类似，SAW 主要侧重于使用 SMT 求解器自动化证明，但通过其脚本语言 SAWScript 支持用户引导的证明策略。 #### 示例 我们可以将 toInt Cryptol 模块导入 SAW，并类似地证明它对具体位向量宽度成立： `` sawscript> import "toInt.cry" sawscript> prove z3 {{ toInt_valid`{16} }} Valid `` ### 交互式定理证明器（ITP） 与 SAW 和 Cryptol 相比，交互式定理证明器（如 Isabelle 或 Rocq）是用于任何形式推理的通用工具。ITP 的核心重点（通常）是提供一个混合自动推理和手动证明的框架，同时确保无论采用何种方法，只有合理的证明才被接受。这使得它们既适用于形式化数学，也适用于软件验证。 ITP 的灵活性以陡峭的学习曲线为代价，用户必须先掌握编写形式证明的一般技能，然后才能尝试任何软件验证。ITP 中的证明可能变得极其庞大，难以更新和维护。然而，ITP 常常是唯一能够处理某个验证问题的表达力足够的工具。 #### 示例 在我们的示例中，Cryptol 和 SAW 都能够证明 toInt_valid 针对特定位向量宽度成立，但两者都不支持自动证明它对*所有*位向量长度成立： `` cryptol> :l toInt.cry toInt> :prove toInt_valid Not a monomorphic type: {n} (fin n) => [n] -> Bi sawscript> prove z3 {{ toInt_valid }} ... sequentToSATQuery: expected first order type or assertion: Num `` 证明这个一般性质根本超出了 SMT 求解器的位向量理论范围。这种抽象推理通常需要 ITP。 ### 从 Cryptol 到 Isabelle 通过本次更新，SAWScript 现在包含两个新命令：write_isabelle_cryptol_modules 和 offline_isabelle，两者都需要先执行 enable_experimental 才能访问。第一个命令接受一个 CryptolModule 值列表作为输入，以及一个目标目录。它将提供的模块（以及任何依赖项）翻译为 Isabelle，并以一组 Isabelle 理论的形式输出。 #### 示例 `` sawscript> toInt_m <- cryptol_load "toInt.cry" sawscript> write_isabelle_cryptol_modules [toInt_m] "./" Successfully wrote './toInt.thy' `` 生成的 toInt.thy 文件包含了对应 Cryptol 模块中所有函数和性质的定义： `` theory "toInt" imports "Cryptol.Cryptol" begin context includes cryptol_translation_syntax begin cryptol_definition toInt :: "{'n} ((fin 'n) =?> ((['n]) ⇒ Integer))" where "toInt x ≡ foldr`{'n,Bit,Integer} (λ(y :: Bit) (b :: Integer). ((if y then 1 else 0 :: Integer) +`{Integer} ((2 :: Integer) *`{Integer} b))) (0 :: Integer) (reverse`{'n,Bit} x)" cryptol_definition toInt_valid :: "{'n} ((fin 'n) =?> ((['n]) ⇒ Bit))" where "toInt_valid x ≡ (toInt`{'n} x) ==`{Integer} (toInteger`{['n]} x)" end end `` 然后我们可以将其导入到一个单独的 Isabelle 理论中，以证明我们想要的性质： `` theory toInt_valid imports "toInt" ... lemma "toInt_valid`{'n} x" sorry (* TODO *) ... `` 第二个命令 offline_isabelle 是一个证明脚本命令（或称策略），只能作为 "prove" 调用的一部分被调用。在 SAW 中，离线策略将当前证明状态翻译为另一个验证工具的输入。与基于 SMT 的策略不同，SAW 实际上并不执行此外部工具来验证证明，而是信任用户自己将执行此验证。 #### 示例 `` sawscript> import "toInt.cry" sawscript> prove (offline_isabelle "toInt") {{ toInt_valid }} Successfully wrote './toInt.thy' Successfully wrote './toInt_prove0.thy' Valid `` 与之前一样，toInt Cryptol 模块被翻译为 Isabelle 理论，但此外还从证明目标生成了一个额外的理论 toInt_prove0： `` theory "toInt_prove0" ... cryptol_definition goal :: "{'n} ((fin 'n) =?> Bit)" where "goal ≡ (∀(i_U :: ['n]). (toInt.toInt_valid`{'n} (i_U :: ['n])))" ... `` 尽管 SAW 已经将证明接受为 "Valid"，但它假定用户将独立证明这个生成的目标为真。要做到这一点，我们需要证明谓词 "goal" 对于 'n 的任何实例化都是 "True"。借助支持的 Cryptol 理论和 Isabelle 的有限机器字库，这个证明是直接的： `` lemma "goal`{'n}" unfolding goal_def toInt_valid_def toInt_def by (simp add: horner_sum_foldr seq_to_list bl_to_bin_eq of_bool_def) `` ## 设计目标 该项目的目标是提供自动将 Cryptol 规范（即一组 Cryptol 模块）翻译为相应 Isabelle 理论集的能力，保留原始含义（语义）和尽可能多的原始结构。 在 Cryptol 中可证明的性质应保持可在 Isabelle 中证明。特别是，给定相同的具体输入，函数应始终产生相同的具体结果。 在 Cryptol 将行为保留为未定义的情况下（如越界索引），翻译后的 Isabelle 定义可能定义也可能未定义，但将保持内部一致。 翻译旨在尽可能保留 Cryptol 源码的原始“形状”，Cryptol 概念尽可能映射到等价的 Isabelle 概念。Cryptol 模块转换为 Isabelle 理论，函数转换为 Isabelle 函数，类型转换为 Isabelle 类型，类转换为 Isabelle 类。这并非总是可能：例如，类型 [n + m] 和 [m + n] 在 Cryptol 中被视为等价，但在 Isabelle 中则不然。为了避免使翻译本身复杂化，这些问题通过自定义 Isabelle 工具（如 cryptol_definition 命令）来处理。 #### **前奏** 虽然翻译本身相对直接，但大部分复杂性存在于提供的前奏中，它允许生成的被 Isabelle 处理的理论。这个库（以 Cryptol.thy 形式提供）定义了 Cryptol 概念的语法（例如，类型应用、序列类型语法等），实现了一个自定义的 seq 类型作为 Cryptol 序列的翻译目标，提供了一个用于推理这些结构的引理库，并为 Cryptol 对应的类型级函数和类定义了类型构造器和类。 ## 为什么选择 Isabelle？ Isabelle 带来了一个成熟的证明策略和理论生态系统。最显著的是，有限机器字库（最初作为 l4.verified 证明的一部分开发）拥有关于字操作的丰富结果集合，包括用于在不同表示之间转换的引理、算术和位移的定义和引理，以及代码生成器支持。这些可以适应关于 Cryptol 函数的证明，通过使用包含的前奏理论。 Isabelle 还包含一个强大且可扩展的证明策略库，如 simp、auto 和 induct，以及像 Sledgehammer 这样的工具，它使用 SMT 求解器来生成交互式证明和高度可扩展的项语法。它的标准库涵盖了各种常见结构，包括列表、集合、整数和用于抽象代数的类型类。 关键的是，Cryptol 规范（相当）自然地映射到 Isabelle 的高阶逻辑和类型系统。一阶类型（如位向量和列表）、高阶函数以及类型类（如 Ring 或 Integral）在 Isabelle 中都有密切的类似物。这使得以保留原始结构和含义的方式将 Cryptol 程序翻译为 Isabelle 成为可能，而无需引入来自中间表示的繁琐翻译伪影。 #### **局限与未来工作** 与任何系统间的翻译一样，存在局限。最值得注意的是，Cryptol 和 Isabelle 之间的语义等价性尚未得到形式化证明。Cryptol 本身没有完全形式化的语义；其行为取决于表达式求值、SMT 翻译和底层求解器理论的组合实现。因此，测试规范在具体输入上是否一致仍然是一个重要步骤。未来，我们可能会开发更标准化的测试框架来验证语义等价性。 目前也不支持无限序列，因为提供的 "seq" 类型仅定义为有限长度。此外，参数化模块结构在翻译过程中被展平，这意味着每个实例化都成为自己独立的理论。 尽管存在这些局限，从 Cryptol 到 Isabelle 在 SAW 内部的翻译能力代表了显著的飞跃——极大地扩展了软件验证的可能性范围。形式化方法中经典的可用性与效能权衡长期以来被视为理所当然。这一假设正在开始瓦解。敬请关注我们帮助缩小这一差距。 [1] 这是对 SAW 现有的 Cryptol 到 Rocq 翻译能力的补充。