合成密码原语的按构造校正代码

此存储库需要Coq 8.9或更高版本。请注意，如果从Ubuntu aptitude软件包安装Coq，则除了coq外还需要libcoq-ocaml-dev。注意在某些情况下（例如在Mac上通过自制软件安装Coq）需要安装ocaml-findlib（用于ocamlfind）和ocaml-num。如果要构建bedrock2代码，则需要Coq 8.10或更高版本（否则可以传递SKIP_BEDROCK2 = 1进行制作）。建议下载最新版本的Coq 。

Git子模块用于某些依赖项。如果未使用--recursive克隆，请运行

您可以查看我们的配置项以查看构建需要多长时间；截至README中此行的最后更新，在Coq 8.11.1上运行make -j2大约需要1h10m。

如果您只想构建用于生成代码的命令行二进制文件，则可以通过仅将standalone-ocaml目标设置为来节省一些时间。

Coq开发建立了使用某种实现策略生成代码的二进制编译器，在编译器的命令行上指定了参数（模数，硬件乘法输入位宽等），并将生成的C代码写入标准输出。

或将Haskell生成的编译器二进制文件制作为独立haskell，或将Haskell和OCaml编译器二进制文件制作为独立文件。这些二进制文件分别位于src / ExtractionOcaml /和src / ExtractionHaskell中。

不传递任何参数，或传递-h或--help（或任何其他无效参数）将导致打印用法消息。这些二进制文件在stdout上输出C代码。

以下是一些从二进制文件所在的目录中调用二进制文件的方法示例：

＃生成2 ^ 255-19的代码。/unsaturated_solinas＆＃39; 25519＆＃39; ＆＃39; 64＆＃39; ＆＃39; 5＆＃39; ＆＃39; 2 ^ 255-19＆＃39;进位添加子opp selectznz to_bytes from_bytes＆gt; curve25519_64.c./unsaturated_solinas＆＃39; 25519＆＃39; ＆＃39; 32＆＃39; ＆＃39; 10＆＃39; ＆＃39; 2 ^ 255-19＆＃39;进位添加子opp selectznz to_bytes from_bytes＆gt; curve25519_32.c＃为NIST-P256生成代码（2 ^ 256-2 ^ 224 + 2 ^ 192 + 2 ^ 96-1）。/word_by_word_montgomery＆＃39; p256＆＃39; ＆＃39; 32＆＃39; ＆＃39; 2 ^ 256-2 ^ 224 + 2 ^ 192 + 2 ^ 96-1＆＃39; ＆gt; p256_32.c./word_by_word_montgomery＆＃39; p256＆＃39; ＆＃39; 64＆＃39; ＆＃39; 2 ^ 256-2 ^ 224 + 2 ^ 192 + 2 ^ 96-1＆＃39; ＆gt; p256_64.c

请注意，对于大素数，您可能需要增加堆栈大小以避免堆栈溢出。例如：

这会在运行命令之前将堆栈大小设置为1 GB（= 1024 MB = 1024 * 1024 KB = 1048576 KB）。从此行的最后编辑开始，此命令需要大约一个小时才能运行，但实际上已成功完成如果没有足够大的堆栈大小，则会堆栈溢出。

研究语言bedrock2支持输出.Coq开发构建使用某种实现策略生成代码的二进制编译器。在编译器的命令行上指定参数（模数，硬件乘法输入位宽等）。生成的bedrock2代码然后使用bedrock2 C后端将其写入标准输出。

或将Haskell生成的二进制文件制作为独立haskell，或将Haskell和OCaml二进制文件制作为独立。这些二进制文件分别位于src / ExtractionOcaml /和src / ExtractionHaskell中。

不传递任何参数，或传递-h或--help（或任何其他无效参数）将导致打印用法消息。这些二进制文件在stdout上输出bedrock2 / C代码。

以下是一些从二进制文件所在的目录中调用二进制文件的方法示例：

＃生成2 ^ 255-19的代码。/bedrock2_unsaturated_solinas--no-wide-int --widen-carry --widen-bytes --split-multiret --no-select＆＃39; 25519＆＃39; ＆＃39; 64＆＃39; ＆＃39; 5＆＃39; ＆＃39; 2 ^ 255-19＆＃39;进位添加子opp selectznz to_bytes from_bytes＆gt; curve25519_64.c./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select＆＃39; 25519＆＃39; ＆＃39; 32＆＃39; ＆＃39; 10＆＃39; ＆＃39; 2 ^ 255-19＆＃39;进位添加子opp selectznz to_bytes from_bytes＆gt; curve25519_32.c＃为NIST-P256生成代码（2 ^ 256-2 ^ 224 + 2 ^ 192 + 2 ^ 96-1）./ bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes- split-multiret-不选择＆＃39; p256＆＃39; ＆＃39; 32＆＃39; ＆＃39; 2 ^ 256-2 ^ 224 + 2 ^ 192 + 2 ^ 96-1＆＃39; ＆gt; p256_32.c./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select＆＃39; p256＆＃39; ＆＃39; 64＆＃39; ＆＃39; 2 ^ 256-2 ^ 224 + 2 ^ 192 + 2 ^ 96-1＆＃39; ＆gt; p256_64.c＃生成2 ^ 130-5的代码。/bedrock2_unsaturated_solinas--no-wide-int --widen-carry --widen-bytes --split-multiret --no-select＆＃39; poly1305＆＃39; ＆＃39; 64＆＃39; ＆＃39; 3＆＃39; ＆＃39; 2 ^ 130-5＆＃39; ＆gt; poly1305_64.c./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select＆＃39; poly1305＆＃39; ＆＃39; 32＆＃39; ＆＃39; 5＆＃39; ＆＃39; 2 ^ 130-5＆＃39; ＆gt; poly1305_32.c

Fiat-Crypto是根据MIT许可，Apache许可（2.0版）和BSD 1-Clause许可的条款发行的；用户可以选择要申请的许可证。

Andres Erbsen，Jade Philipoom，Jason Gross，Robert Sloan，Adam Chlipala。加密算法的简单高级代码-带有证明，不妥协。出现在IEEE安全与安全研讨会论文集中隐私权2019（S＆amp; P＆＃39; 19）。 2019年5月。本文描述了多个字段算术实现，以及旧版本的编译管道（在此处保留）。它受到空间的限制，因此最好在下面的文章中阅读一些详细信息。

翡翠（Jade Philipoom）。 Coq中的按结构校正有限域算法。麻省理工学院硕士论文。 2018年2月。第3章和第4章详细介绍了现场算术实现（再次针对先前的编译管道）。

安德列斯·埃尔布森在Coq中制作认证的椭圆曲线密码学实施方案。麻省理工学院硕士论文。 2017年6月。第3节简要介绍了使用coq合成字段算术代码的过程，没有假设Coq的技能，但只覆盖了整个库的一小部分。第5节和第6节仅包含此存储库中椭圆曲线库上的内容。

最新的编译管道还没有单独的文档，但是此自述文件确实对其进行了详细介绍。

合成过程的想法已在src / Demo.v中进行了演示。我们强烈建议您在研究全面系统之前先阅读此内容。

我们使用的PHOAS表达式的客户端入口点是Language / API.v。有关该接口的说明，请参见该文件中的注释。下面的文字描述了表达式的生成方式，而不是如何与之交互。

语言/*.v↑├────────────────────┬ ──────────────┬───────────┐摘要解释/*.v MiscCompilerPasses.v重写者/ *。 v PushButtonSynthesis / ReificationCache.v算术.v↑↑↑↑Stringification / *。v│││COperationSpecifications.v↑││││└────────────┬──── ────────────┴───────────┴ ────────────┘│BoundsPipeline.v CompilersTestCases.v│↑│└──────────┬──────── ────────────────────────────────────────────────── ──────────────────────┘PushButtonSynthesis / *。v↑┌──────────┴──── .──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐CLI.v SlowPrimeSynthesisExamples.v↑┌──────────┴──────── v StandaloneOCamlMain.v↑提取ExtractHaskell.v ExtractionOCaml.v

上一个←────────────────────────────── ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── ──标识符BasicGENERATED.v←─────────────────────────────API.v↑↑↑├─────── ────────┐└──────────┐││UnderLets.vIdentifiersLibrary.v←──── ────────IdentifiersGenerate.v←───────IdentifiersGENERATED.v↑↑↑IdentifiersLibraryProofs.v←───IdentifiersGenerateProofs.v←─IdentifersGENERATEDProofs.v

Language.v↑IR.v↑┌──┴────────┐C.v Rust.v

COperationSpecifications.v：要综合的各种操作的规范。TODO：此文件可能应该重命名。

AbstractInterpretation / *。v：基于类型代码的ZRange定义，标识符的抽象解释（出于历史原因，它允许放行，并且应该删除对UnderLets的依赖），它定义了以下内容：

上一个：写出重写器和PHOAS标识符解释时使用的一些定义，例如ident.cast，ident.eagerly，Thunked.list_rect等

Language.v：定义了PHOAS基本基础结构的部分，这些部分根据基本类型和标识符进行了参数化，包括：菲亚斯化。表示/解释。反转PHOAS exprs的实用程序。 PHOAS exprs的默认值/虚拟值。通用PHOAS类型的默认实例化。 Gallina修改地面术语。平面/索引语法树，以及往返PHOAS的转换

API.v：将PHOAS表达式的类型专用于我们正在使用的特定标识符，并为某些特殊版本定义了便利性注释，策略和定义。

IdentifierParameters.v：定义了两个定义，以确定该语言使用的标识符和类型。这些用作生成标识符定义的输入。

IdentifiersBasicGenerate.v：除了定义基于生成的包进行验证的策略之外，还定义生成PHOASmachinery使用的所有特定于标识符列表的定义的策略。

IdentifiersBasicGENERATED.v：基本上是自动生成的文件，用于定义基本类型代码和标识符代码的归纳（第一个是手写的，因为它很短；后者是从打印归纳法的策略中复制粘贴的），并调用程序包生成IdentifiersBasicGenerate.v。中的-tactic。

UnderLets.v：UnderLets monad，该过程可以替代var样的东西，该过程将let-binders插入随后的代码的最后一行，以替代var样的东西（这用于确保在我们输出时C代码，对输入和输出数组进行别名不会造成问题）。定义passs ：。 SubstVar。 SubstVarLike。替代者

IdentifiersLibrary.v：有关标识符，模式标识符和原始标识符的一些定义。其中一些定义将生成的定义作为参数。还定义一个包记录以保存所有生成的定义。

IdentifiersGenerate.v：生成用于重写器的标识符的无类型和模式版本的定义的策略。最终形成一种策略，该策略占用了IdentifiersLibrary.v中定义的包类型。

IdentifiersLibraryProofs.v：有关IdentifiersLibrary中定义的证明。还定义了一个包来保存生成的证明，该证明需要破坏此文件中尚未定义的归纳法。

Language.v：为PHOAS语言定义打印机（显示实例），定义一些与语言无关的通用实用程序，以转换为输出代码，并定义从PHOAS到语言的字符串转换的规范/ API。 （取决于ZRange实用程序的AbstractInterpretation.v。）定义通过：。 ToString.LinesToString。 ToString.ToFunctionLines

IR.v：为C和Rust（以及最终可能的其他语言）定义通用的IR，并为实例化具有指针和函数调用的语言的LanguageSpecification API建立必要的大多数基础结构

BoundsPipeline.v：将各种编译器通道组装在一起，组成一个组合管道。它是编译器的最终接口。还包含一些应用BoundsPipelinecorrectity引理的策略。

PushButtonSynthesis / ReificationCache.v：定义用于保存操作版本的缓存，以及用于定义和应用缓存中内容的策略。

PushButtonSynthesis / *：从Arithmetic.v中修改各种操作，使用这些操作定义BoundsPipeline的组成，证明其解释满足COperationSpecifications.v中的规范，将经过精化的边界后操作组装为综合目标。这些是CLI.v依赖的文件：

ReificationCache.v：定义预定义术语的缓存。从管道的使用中分离出升职要求，使我们不必在每次更改管道或管道的中间阶段时就重新定义大术语。

InvertHighLow.v：为Barrett和FancyMontgomeryReduction定义一些通用的定义，围绕事物的高低位分开。

SmallExamples.v：使用管道的一些小示例。没有什么依赖于此文件；它仅用于演示目的。

BarrettReduction.v，FancyMontgomeryReduction.v，SaturatedSolinas.v，UnsaturatedSolinas.v，WordByWordMontgomery.v：将管线实例化为相应的实现选择，以及所有相关的正确性证明（例如，事物组装成一个环）。

SlowPrimeSynthesisExamples.v：流水线的其他用途是用于一些很慢的素数，我不想提取阻塞。还包含一些调试示例。

CLI.v：设置提取的所有与语言无关的部分；依赖于每个管道的字符串或错误消息列表以及该管道的参数，并为此建立命令行参数解析器。

Rewriter /中定义的文件分为以下依赖关系图（包括顶部Language /中的一些文件）：

IdentifiersLibrary.v←──────────────────────────────────────────────────────────────────────────────────────────────────────────── ────IdentifiersGENERATED.v↑──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── ↑│││││││││││││Rewriter.v←────────────────────ProofsCommon.v←─────── ──────────────ProofsCommonTactics.v│↑↗↖↑│Reify.v←────────────┐Wf.v InterpProofs.v││││ │││Rules.v└────────────AllTactics.v────────────────────── ────┘│↑↑┌──────────────────────────────── ──────┘RulesProofs.vAllTacticsExtra.v↑↑├────────┬───────────┬ ────┴────────┬────────────────────────────────────────────────────────────────────────────── /Arith.v Passs / ArithWithCasts.v Passes / StripLiteralCasts.v│↑↑↑↑│└───────────┴ ──────────┴──────────────┴ ────┐││└──────┬┬──────────────── /ToFancyWithCasts.v│↑↑│└───────┬────────────┴ ──────────────── ──────────────────┘│All.v

Rules.v：定义将被修改的重写规则的类型列表。在很大程度上独立于表达语言。

Rewriter.v：定义重写器机制。特别是，在此文件中找到所有具有非重写规则特定证明的重写器定义。

RewrierReify.v：定义重写规则的形式化，从Rewriter.v开始，并以策略RewriteRules.Tactic.Build_RewriterT和策略符号make_Rewriter达到顶点，后者定义了RewriteRules.GoalType.RewriterT类型的包。 Build_ *策略返回一个constr，而make_ *策略符号则对该目标进行细化。两种策略都采用两个参数：首先是一个布尔值include_interp，它指定（true）与否（false）为重写规则列表加归约文字重写规则；第二个是bool * Prop列表，它是要修改的重写规则类型的列表，每一个都与布尔值配对，无论是否尝试在该规则的位置输出中再次重写。

ProofsCommon.v：定义了插补规则的interp-goodness和wf-goodness概念，定义了证明这些概念的策略，并包含了在wf证明和interp证明之间共享的半任意的证明和定义集合。文件定义了陈述和证明特定重写规则正确所需的所有内容。另外定义一个包RewriteRules.GoalType.VerifiedRewriter，该包描述总体专业重写器的类型及其Wf和Interp证明。 （此软件包也许应该移到另一个文件？）

ProofsCommonTactics.v：定义用于证明特定重写规则正确并居住在ProofsCommon.v中定义的程序包的实际策略。

Wf.v：证明通用重写器的wf保留，以重写规则的wf优点为假设。

AllTactics.v：定义策略RewriteRules.Tactic.make_rewriter（以及类似的策略表示法），该策略将构建整个VerifiedRewriter。它们采用Rewriter.v策略中的include_interp，以及在重写规则类型列表（bool * Prop）上建立索引的一系列重写规则证明。这是用于从重写规则列表中定义arewriter的主要接口。

{NBE，Arith，ArithWithCasts，StripLiteralCasts，ToFancy，ToFancyWithCasts} .v：将AllTactics.v中的策略与RulesProofs.v中可靠的重写规则列表一起使用，以减少和减少相应的密码并生成重写器。

type.invert_one e，它以保留关于e类型的信息的方式，对通过类型代码索引的任何归纳类型进行案例分析，即使目标是根据e和/或其类型独立键入的，通常也可以工作

ident.invert_match，对作为目标或任何假设中的比赛的判别式出现的身份进行案例分析

expr.invert_match，对作为目标或任何假设中的匹配判别式的exprs进行案例分析

expr.invert_subst，它对显示形式为expr.invert_ * _的假设的exprs进行案例分析。

expr.wf_t（以及变体wf_unsafe_t和wf_safe_t）使wf目标取得进展； wf_safe_t绝不应将可证明的目标变成不可证明的目标，而wf_unsafe_t则可能。 expr.interp_t（和变体），它应该使进展等同于interp的假设和目标，但使用不多（主要是因为我忘记了定义） verify_Wf，它比重复构造函数以更优化的方式证明具体语法树上的wf目标。