形式化驗證零知識證明系統編譯器

Abstract

本論文提出一個依值型別的可驗證計算編譯器，並證明其可靠性。此編譯器將一個淺層嵌入於 Agda 當中，具有依值型別的領域特定語言轉換成一階限制條件。可靠性是轉換正確性的一個部份，表示如果產生出來的限制條件是可被滿足的，那產生出來的限制條件會是正確的。藉由利用柯里-霍華德對應，我們在互動式定理證明器 Agda 當中建構此編譯器的形式規格以及證明其可靠性。

In this thesis, we will construct and prove the soundness of a dependently typed verifiable computation compiler. The compiler described in this thesis compiles a user program written in a dependently typed shallowly embedded domain specific language in Agda into a set of rank 1 constraints. Soundness is a part of translational correctness that says that if the generated constraints are satisfiable, then the generated constraints are correct. By utilizing the Curry-Howard correspondence, the compiler is formally specified and proved in the interactive theorem prover Agda.