Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reimplementing Mizar in Rust

Mario Carneiro

TL;DR

This work presents mizar-rs, a Rust reimplementation of Mizar's core proof-c checking and analysis components, enabling external proof export and substantial performance gains. By reencoding the checker and analyzer and integrating them with a modular pipeline, the authors verify the entire Mizar Mathematical Library (MML) in under 12 minutes on 8 cores, achieving roughly a 4–5× speedup over the Pascal baseline. They also use this project to audit the original system, uncovering several soundness bugs (four major issues plus an auxiliary one) and coordinating fixes with MML maintainers, illustrating the value of external checkers for reliability. The work discusses architectural decisions, parsing and name-resolution challenges, and the potential of proof-export tooling, while outlining future directions such as removing language-imposed constraints and extending the system beyond verification toward complete proof export.

Abstract

This paper describes a new open-source proof processing tool, mizar-rs, a wholesale reimplementation of core parts of the Mizar proof system, written in Rust. In particular, the "checker" and "analyzer" of Mizar are implemented, which together form the trusted core of Mizar. This is to our knowledge the first and only external implementation of these components. Thanks to the loose coupling of Mizar's passes, it is possible to use the checker as a drop-in replacement for the original, and we have used this to verify the entire MML in 11.8 minutes on 8 cores, a 4.8x speedup over the original Pascal implementation. Since Mizar is not designed to have a small trusted core, checking Mizar proofs entails following Mizar closely, so our ability to detect bugs is limited. Nevertheless, we were able to find multiple memory errors, four soundness bugs in the original (which were not being exploited in MML), in addition to one non-critical bug which was being exploited in 46 different MML articles. We hope to use this checker as a base for proof export tooling, as well as revitalizing development of the language.

Reimplementing Mizar in Rust

TL;DR

This work presents mizar-rs, a Rust reimplementation of Mizar's core proof-c checking and analysis components, enabling external proof export and substantial performance gains. By reencoding the checker and analyzer and integrating them with a modular pipeline, the authors verify the entire Mizar Mathematical Library (MML) in under 12 minutes on 8 cores, achieving roughly a 4–5× speedup over the Pascal baseline. They also use this project to audit the original system, uncovering several soundness bugs (four major issues plus an auxiliary one) and coordinating fixes with MML maintainers, illustrating the value of external checkers for reliability. The work discusses architectural decisions, parsing and name-resolution challenges, and the potential of proof-export tooling, while outlining future directions such as removing language-imposed constraints and extending the system beyond verification toward complete proof export.

Abstract

This paper describes a new open-source proof processing tool, mizar-rs, a wholesale reimplementation of core parts of the Mizar proof system, written in Rust. In particular, the "checker" and "analyzer" of Mizar are implemented, which together form the trusted core of Mizar. This is to our knowledge the first and only external implementation of these components. Thanks to the loose coupling of Mizar's passes, it is possible to use the checker as a drop-in replacement for the original, and we have used this to verify the entire MML in 11.8 minutes on 8 cores, a 4.8x speedup over the original Pascal implementation. Since Mizar is not designed to have a small trusted core, checking Mizar proofs entails following Mizar closely, so our ability to detect bugs is limited. Nevertheless, we were able to find multiple memory errors, four soundness bugs in the original (which were not being exploited in MML), in addition to one non-critical bug which was being exploited in 46 different MML articles. We hope to use this checker as a base for proof export tooling, as well as revitalizing development of the language.
Paper Structure (20 sections, 1 theorem, 5 equations, 2 figures, 2 tables)

This paper contains 20 sections, 1 theorem, 5 equations, 2 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Mizar internals: A (determined) user's perspective
  3. The checker
  4. Core syntax
  5. Structure of the checker
  6. Requirements
  7. Soundness considerations of the requirements
  8. The analyzer
  9. Name resolution (MSM)
  10. The parser
  11. The scanner
  12. The parser
  13. Mizar soundness bugs
  14. Exhibit 1: polynomial arithmetic overflow
  15. Exhibit 2: negation in the schematizer
  16. ...and 5 more sections

Key Result

Theorem 1

If $a$ and $n$ are numerals and $i:\mathbb{N}$, then is provable.

Figures (2)

  • Figure 1: Data flow between Mizar components. Files with only an extension like .miz correspond to files named after the input art.miz file. Files in red are in XML format. For example, art.atr is created by the accommodator and read by the checker and the exporter. Files like dep.dcl are produced for the current article by the exporter and aggregated by the accommodator in articles importing that dependency.
  • Figure 2: Scatter plot of files in the MML based on check time in verifier (vertical axis) vs. in mizar-rs (horizontal axis), in seconds. The left plot is linear and the right is log-log (including some outliers not in the left plot). The blue line is the best fit, indicating an average $4.93\times$ speedup, and the gray dashed line is a $1\times$ reference; there are no points below this line, indicating that mizar-rs was never slower than verifier on this run.

Theorems & Definitions (3)

  • Remark 1
  • Theorem 1
  • proof