bedrock1 CPS semantics vs bedrock2 postcondition semantics

[spitters]

It looks the semantics style has changed between bedrock1 and bedrock2.
Is there an overview of which properties we can expect to continue to hold?
Of course, one could read the Coq sources, but a more high-level description of the difference between bedrock1 and bedrock2 would be helpful.

[andres-erbsen]

Hi,

I don't think we have written an extensive comparison anywhere, but it's clearly about time, so let me give it a start. Overall, bedrock2 aims to fill in roughly the same place in an verified stack as bedrock1 would, but has significant differences. Here are some important ones:

• structured syntax: bedrock2 offers a barebones C-like syntax whereas bedrock1 offered an assembly-like language with 3 registers. This means we can pretty-print bedrock2 as C or straightforwardly compile it to target architectures in a way that uses more than 3 registers.
• no macro system (so far): bedrock1 eventually developed a significant library of macros for encoding higher-level constructs: variables, loops, etc. Some of these are already included in bedrock2 syntax and others are simply not available right now. While the rupicola (proof-search-based gallina-to-bedrock2 compilation) may cover some of the use cases of the latter, we are not aiming for feature parity.
• no function pointers (so far). For example, you cannot implement a dynamic thread scheduler as a pure bedrock2 library. We might add function pointers later; omitting them was a design simplification made before we settled on CPS semantics.
• total correctness. In bedrock1, an infinite loop satisfied every spec, and libraries such as the memory allocator carefully exploited this to avoid spending verification effort in cases believed to be unreachable. All bedrock2 functions must terminate, although we do provide a top-level event-loop wrapper as a part of the risc-v compiler.
• semantics for I/O. All correctness conditions in bedrock1 were encoded as assertions in the source code, with a toolchain-level theorem that assertions never fail if verification conditions are proven. bedrock1 includes a notion of I/O traces in the semantics and has a syntactic construct for I/O modeled as external function calls.
• CPS semantics: this is the semantic style we converged on based on the decisions to have structured syntax, total correctness, and I/O inside the language. It has similarities to Cito/Facade (higher-level languages that compiled to bedrock2) and significant differences from e.g. CompCert.
• direct weakest-precondition proofs instead of generating individual verification conditions. This means that statements in a function have to be verified in the order they would execute, with the upside being that proof context is preserved from one line to the next.
• no reflective automation (so far): bedrock2 has performance issues, as any serious software engineering project in coq, but we think they are not yet at the level to invest in building reflective automation as bedrock1 used (our current ltac scripts are also more flexible than bedrock1 automation).
• memory model unchanged: memory is a partial map from words to bytes, with no further structure or restrictions imposed upon it.
• separation logic as just an assertion language: bedrock1 built separation logic into the program logic, bedrock2 has a basic hoare logic and our specifications just happen to use separation logic for assertions. The jury is still out on whether this was a good idea, but we do have verified code that uses it to support various forms of aliasing (for example, field arithmetic x+=y). We still provide tail-recursion-style loop lemmas familiar from bedrock1 and other goodies often associated with separation logic.

I am not currently aware of any significant breaking changes planned for bedrock2; and I think we have enough code that we're invested in that we would seriously consider alternatives before breaking it.

I hope this helps,
Andres