the C abstract machine and code extraction

Stream: new members

[Huỳnh Trần Khanh]

Is it possible to implement the C abstract machine with inductive types? Where can I get started? I want to be able to reason about C programs and I'm willing to put in some work to formalize C semantics.

[Huỳnh Trần Khanh]

As a side note: I'm really infatuated with inductive types since they can be used to formalize many models. They are just so powerful.

[Johan Commelin]

You might be interested in Mario's mm0 and mm1

[Johan Commelin]

Then you don't have to implement everything yourself. But you don't get 100% pure C

[Huỳnh Trần Khanh]

Thanks. But how does that relate to my question though? I thought mm0 was just an insanely fast verifier that is incredibly, incredibly low level and had nothing to do with formalizing C semantics.

[Eric Wieser]

It might help to think about the type of statement you want to formalize

[Mario Carneiro]

Actually I've been building a verified compiler for a C-like language in mm0. But probably a closer match to your question is CompCert, which formalized (most of) the semantics of C inside Coq and built a verified compiler for it. I got some ways through porting it to lean many years ago

[Mario Carneiro]

I also object to "incredibly, incredibly low level". It's somewhat low level but quite a bit higher level than metamath

[Mario Carneiro]

and in principle the only thing stopping it from being even more usable is more UX work that I don't have the time to work on since it's basically a one man project right now

[Horatiu Cheval]

Maybe the IMP chapter from software foundations would be a lighter introduction to this? It walks you through representing a basic imperative language in Coq and proving stuff about the behaviour of programs in it.

[Chris B]

There's also the new-ish SF volume "Verifiable C": https://softwarefoundations.cis.upenn.edu/vc-current/index.html. It uses coq, but it's probably a pretty good on-ramp for reasoning about C in a CiC-flavored ITP. Volume 6 was just released, and is about seapration logic, which might be of interest as well.

[Kevin Buzzard]

I learnt a lot about lean by doing all the exercises from the first volume of that series in Lean.

[Huỳnh Trần Khanh]

(removed)

[Huỳnh Trần Khanh]

(removed)

[Huỳnh Trần Khanh]

Mario Carneiro said:

Actually I've been building a verified compiler for a C-like language in mm0. But probably a closer match to your question is CompCert, which formalized (most of) the semantics of C inside Coq and built a verified compiler for it. I got some ways through porting it to lean many years ago

Is the code for an older version of Lean? I just cloned the Lean port and the code doesn't seem to work...

[Huỳnh Trần Khanh]

And by "work" I mean the code verifies cleanly

[Huỳnh Trần Khanh]

This is what I am seeing: Screenshot-from-2021-06-04-11-05-21.png

[Bryan Gin-ge Chen]

Since the latest timestamp in Mario's repo is from early Jun 2017, I suspect that the code only works with Lean 3.1.0: https://github.com/leanprover/lean/releases

[Huỳnh Trần Khanh]

The data.nat.bquant looks like the code is written for Lean 2 though. Let me rollback to Lean 2 and see if the code works or not.

[Huỳnh Trần Khanh]

Oh, and I have to install Emacs. The horror!

[Bryan Gin-ge Chen]

I think you're right,data.nat.bquant was already moved to old_library in even in Lean 3.0.0: https://github.com/leanprover/lean/blob/dae1c9dac28d1db1865ae2b1b3a39408b8ee5504/old_library/data/nat/bquant.lean

[Mario Carneiro]

I'm pretty sure it is lean 3 code, not lean 2, although like Bryan says it's quite old

[Mario Carneiro]

But there are very few proofs outside a few files, it's mostly defining inductive types and I think the syntax for that is still basically the same, so updating the project shouldn't be too bad

[Mario Carneiro]

just remove the imports of nonexisting files