Math Proof Generation
Math Proof Generation is the process that takes as input the math theory of the programming language, the computing result, and the math proof hint, and using the Proof Calculus to generate the math proof for a given computing task conducted by K. The math proof is complete, rigorous, and machine-checkable by a math proof checker, and can serve as the verifiable certificate of the original computing task.
The generation of the math proof eliminates K and the math proof generation process itself from the trust base of Proof of Proof.
Below is a more detailed and specific outline of how a math proof PI
is created from a program P
in a programming language PL
:
K is used to define the formal semantics of
PL
that represents the math theory of the programming language.The LLVM backend of K uses the formal semantics of
PL
to automatically derive an interpreter forPL
, which is used to executeP
. The execution process is logged in the form of the proof hint.Using the proof hint and a predefined set of proof rules in the Proof Calculus, create an internal representation of the math proof
PI
.Finally, this internal representation is converted into a format, such as Metamath or a specialized block model, and is checked by a corresponding math proof checker of that format.
Proof Calculus and Matching Logic
Proof Calculus is at the heart of math proof generation. Matching logic is the foundation of Proof Calculus. It provides a unified way to define and reason about the semantics of any programming language. In matching logic, a programming language is formalized as a math theory, also called a logical theory, which is a structured collection of axioms that define the behaviors of all programs in that language. This logical structure makes it possible to reason about execution, correctness, and equivalence in a precise and formal way.
Matching logic is an expressive yet minimal logic, which makes it ideal to serve as the logical foundation of Proof of Proof.
Matching logic can express any programming paradigms (imperative, functional, object-oriented, logical, etc.), any semantics styles (operational, algebratic, denotational, etc.), and any program properties (safety, liveness, temporal, etc.).
Matching logic has a simple syntax and a simple proof system, which results in very small proof checkers in a few hundreds lines of code, reducing the trust base of Proof of Proof to an absolute minimum.
Matching logic uses a small set of constructs to express powerful logical patterns:
These expressions, called patterns, can match a wide range of structures—from simple terms to full program states.
Below is an explanation of what each component means:
x
: Element variables, like those in first-order logic (FOL), used to refer to individual elements.X
: Set variables, similar to propositional variables in modal logic, used for predicates or sets of elements.φ₁ φ₂
: Application. Applying the constructor/function/relation represented by φ₁ to φ₂.⊥
: Logical false.φ₁ → φ₂
: Logical implication.∃x.φ
: Existential quantifier, expressing that some value makes φ true.μX.φ
: Least fixpoint, used to express recursive or iterative properties (e.g., loops or reachability).
Patterns are the core building blocks of matching logic, allowing us to
Match data structures with specific shapes
Describe valid transitions between program states
Capture dynamic behaviors and constraints over time
In practice, this makes matching logic suitable for both low-level reasoning (e.g., arithmetic correctness) and high-level semantics (e.g., verifying smart contracts or system invariants).
Last updated
Was this helpful?