Lean Kernel Arena / con-agua

con-agua is con-leche reimplemented at the level of x86-64 assembly: a close clone of con-ron's checker, written in a small first-order language, compiled by a verified compiler, and shipped as one committed assembler file together with a C harness of about two hundred lines that reads the input and calls it.

A Lean theorem relates that assembler file, as an x86-64 program in Kraken's semantics, to con-ron's Lean twin, which con-ron proves to refine con-leche's pure checker: if the machine code reports accept, con-leche accepts the same bytes, so the accepted declarations have a model in set theory, and in particular no theorem of False is accepted. The code the CPU executes is the code the theorem is about, so neither a compiler nor a language runtime is trusted; what is trusted is Kraken's x86 semantics, the assembler and loader, and the C harness. The threaded mode used here has its own theorem, which takes the harness's thread scheduling as hypotheses.

So a proof accepted by con-leche, con-ron and con-agua is protected against a bug in the Lean compiler and runtime, in rustc and Aeneas, or in the x86 model, unless bugs in all three settings conspire.

It runs with four worker threads for the check phase, on raw lean4export NDJSON. It exits with 0 on accept, 1 on a rejection and 2 on a decline, each with the reason con-ron would give, and with 3 when a resource runs out or an abort has no specific reason (it then claims nothing). The theorem covers rejections and declines too: on exit 1 or 2, con-ron's twin fails on the same input with that kind of error (the message text is not part of the proof). Written by AI under supervision from Joachim Breitner at the Lean FRO.