This is a reimplementation of the external Lean checker con-leche, verified at the x86 assembly level.
This was written by AI under supervision from Joachim Breitner at the Lean FRO. This README is genuinely human written; the rest of the repository is not. The file OVERVIEW.md contains a much more detailed, AI written exposition of the project.
The con-agua checker joins con-ron in providing extra assurance by reimplementing con-leche in a different setting. All three are proven to implement essentially the same consistent checking algorithm. But any such verification work leaves something left to be trusted:
con-leche, written in Lean, in particular requires the Lean compiler and the Lean runtime with its bignum implementation to be correct.con-ron, written in Rust, in particular requires the Rust compiler as well as the Aeneas verification tool to be correct.con-agua, verified at the assembly level, in particular requires the Kraken x86 semantics to be correct.
A bug in any of these trusted components threatens the validity of that checker's result. But if you check your proof with all three of them, the likelihood of bugs existing in all three settings that can be exploited together diminishes.
Run make and call ./checker FILE.ndjson. Pass --jobs=n if you want parallel checking. See OVERVIEW.md for more details.
We use the Kraken x86 semantics to prove that if the type checker in the assembly file checker.s accepts, then con-leche and con-ron accept too (up to resource limits). See EndToEnd.lean for the main theorems of this development.
The assembly is produced from code written in our own little ad-hoc low-level language L with a verified compiler. The L code is proven to simulate con-leche (via con-ron’s Lean model, which already handles hash-consing and caching).
The small, trusted main.c file reads the input and invokes the entry point of the assembly function. With --jobs=n, after parsing the input (using the verified assembly for that), it spawns threads and invokes the verified assembly once for each declaration group.
Again, more detail to be found in OVERVIEW.md.
Unsolicited PRs against this repo are unlikely to be useful; well-written issues with bug reports or feature requests are welcome.