splitting the repository

[andres-erbsen-sifive]

As discussed with @vmurali and @sifive-emarzion, it would be nice to eventually split this repository in a way that allows for the sifive end-to-end repository to include bedrock2 (and probably the compiler) but not mit mit-plv/kami.

[vmurali]

The best way to split this would be to keep only bedrock2 language and semantics in this repo. RISC-V semantics should be completely orthogonal to bedrock2 semantics (for instance bedrock2 should be compilable on intel CPUs too). There must be a separate repository that combines the compiler to RISC-V. I think there must be a third repository that proves the equivalence of the RISC-V compiler semantics and the RISC-V hardware semantics in Kami. @samuelgruetter @andres-erbsen @vmurali @sifive-emarzion @andres-erbsen-sifive

[andres-erbsen-sifive]

If this project is successful to the best of our hopes, the maximal splitting (and perhaps ideal) that I see is as follows:

• domain-specific provers from bedrock2 directory
• language semantics and basic program logic
• the compiler to risc v
• the compiler to C (currently unverified, perhaps later verified against some C semantics)
• riscv-coq
• sifive kami
• mit kami rv32im, which would include riscv-coq equivalence proof
• sifive kami risc v processor, which would include riscv-coq equivalence proof
• any software for an and-to-end demo that depends on all of the above would have its own repo

As for what would make sense to do right now, I would like to suggest the following policy: we split each component when there is more than one option for it. Currently there is only one verified compiler in sight, so I think it is fine to keep the bedrock2-to-riscv compiler in this repo. We have two versions of kami in sight, so we should split (although in this specific case we might just have sifive end-to-end demo include a download of MIT kami that is never Required because MIT kami will likely disappear once sifive kami has a better-than-single-cycle processor). As there is currently only one software platform for the two demos, I think there is no urgency to split that either.

[samuelgruetter]

I agree with @andres-erbsen-sifive

[joonwonc]

I also agree to the repository policy that @andres-erbsen-sifive suggested.

[vmurali]

I agree with Andres' overall splitting strategy. However, I still think it is a good idea to do the splitting that I mentioned, namely the compiler to machine code and the connection with hardware spec. This would make development much more easier on both MIT Kami and SiFive Kami, without having to do extra work each time someone wants to clone something. Andres' also mentioned the bedrock2 to C compiler, which SiFive could potentially work on - connecting SiFive Kami's semantics to VST/Compcert. That means, we might write a verified a non-optimizing compiler from bedrock2 to VST (with Andres' help/insights while he's here). Keeping all this together is definitely a hindrance requiring a hard fork that gets more and more painful to merge later on.

[andres-erbsen-sifive]

Could you please elaborate on the extra work hinderance you see in keeping the parts that are currently together as they are?

[spitters]

What is the current status of this issue? Has there been any progress in connecting bedrock to C semantics, such as CompCert/VST ?

[andres-erbsen]

We haven't done much on this front. The rupicola repository uses https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ToCString.v instead of the RISC-V backend, but I think having a separate Makefile target for the relevant parts is enough for that.

We do not have a use case for connecting to VST or CompCert right now. As far as performance is concerned, we either reall want evey last percent (so gcc or clang), or don't care at all (so bedrock2 RISC-V backend is fine). I also don't expect particularly convenient interoperability for proofs because VST and CompCert insist on the distinction between pointers and integers (https://stackoverflow.com/a/63743244) whereas bedrock2 nonchalantly mixes the two, relying on implementation-defined behavior of gcc and clang in the current C backend. I do expect that some connection could be made, but it might come down to mapping all bedrock2 memory accesses to indexing into the same array, so currently we lack enthusiasm to pursue this connection.