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 for PL, which is used to execute P. 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:

φ ::= x | X | φ₁ φ₂ | ⊥ | φ₁ → φ₂ | ∃x.φ | μX.φ   (if X is positive in φ)

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).

PreviousArchitecture NextMath Proof Checker

Last updated 9 hours ago

Was this helpful?

Proof Calculus and Matching Logic

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:

φ ::= x | X | φ₁ φ₂ | ⊥ | φ₁ → φ₂ | ∃x.φ | μX.φ   (if X is positive in φ)

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).