Lean's TCB for executable programs

Stream: general

[Jason Rute]

On the Coq zulip, there is an interesting conversation about Lean vs Coq on writing programs and extracting code. My understanding of the consensus is that Coq is more focused on a complete verified toolchain including code extraction, while Lean is more focused on being able to quickly open up Lean and write executable verified applications in Lean (at the cost of a larger TCB). But in particular, @Karl Palmskog asked

Is there a breakdown of the TCB for running Lean programs? My impression is that without running a checker post-hoc on terms stored in files, Lean gives very few guarantees about any results (due to input/output, etc.)

[Jason Rute]

I'm not sure if the "running a checker post-hoc" comment is about executable code or more about
something like #general > PSA about trusting Lean proofs.

[Mario Carneiro]

The TCB for compiled lean programs is:

1. You trust that the lean logic is sound
2. (If you didn't prove the program correct) You trust that the elaborator has converted your input into the lean expression denoting the program you expect
3. (If you did prove the program correct) You trust that the proofs about the program have been checked <- use lean4checker / other external checkers to eliminate this
4. You trust that any compiler overrides (extern / implemented_by) do not violate the lean logic (i.e. the model matches the implementation)
5. You trust the lean compiler (which lowered the lean code to C) to preserve the semantics of the program
6. You trust clang / LLVM to convert the C program into an executable with the same semantics
7. You trust that the hardware / firmware / OS software running all of the above didn't break or lie to you
8. (When running the program) You trust that the hardware / firmware / OS software faithfully executes the program according to spec and there are no debuggers or magnets on the hard drive or cosmic rays messing with your output

[Mario Carneiro]

As far as I know, the default situation for programs written in Coq is much the same as for Lean, with "code extractor" replacing "lean compiler" and "ocaml compiler" replacing "clang / LLVM"

[Jason Rute]

I feel 4 (overrides) is probably one of the biggest areas of trust.

[Mario Carneiro]

well, all of the above are actually very complicated things to ensure

[Mario Carneiro]

4 is at least easy to enumerate

[Mario Carneiro]

from a software verification standpoint the only things we have a hope of eliminating given infinite effort are 4, 5 and 6

[Mario Carneiro]

In some cases we can outright prove instances of 4, in other cases you can prove it only as a refinement, and in still others one has to reason about properties of the lean runtime

[Mario Carneiro]

Of course some of the cases of 4 involve IO and there you need to prove properties about the glue code, assuming correctness of libc (which is some combination of 6 and 7)

[Shreyas Srinivas]

Maybe this belongs in one of the documentation pages

[Shreyas Srinivas]

Along with basic conceptual explanations and comparisons with the TCB of similar systems under similar situations.