a "getting started" guide

[andres-erbsen-sifive]

so I've been asked for this several times now. Here are some thoughts of what we should do.

References to non-bedrock2-specific background resources

• basic coq usage, like one or two chapters of software foundations or frap. no induction or datatypes stuff, just proof.
• Hoare logic (software foundations? frap? VST?)
• Separation Logic (* and emp, no fancy things like magic wand).
  • https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Map/Separation.v is actually short
• separation logic automation. perhaps read the first bedrock paper, and ignore the higher order stuff about code pointers http://adam.chlipala.net/papers/BedrockPLDI11/BedrockPLDI11.pdf chapter 2. SeparationLogic.ecancel is the bedrock2 script to perform cancellation.
• coq tactic lia, ring documentation
• reading coq type errors (reification by parametricity repo might have a thing on this?)

Common infrastructure in bedrock2 (just skim)

• https://github.com/mit-plv/coqutil/blob/master/src/Word/Interface.v
• https://github.com/mit-plv/coqutil/blob/master/src/Map/Interface.v

bedrock2 semantics (read enough to understand structure)

• https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Notations.v
• https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/WeakestPrecondition.v expr_body, its callees, and cmd_body
• first example proof: https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/swap.v
  • in particular, try to match up the spec_of_* definitions with WeakestPrecondition.call and try to think through in your head what the precondition ends up being
  • follow along with the bedrock paper, single-step straightline instead of using repeat
• loop invariant example https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/ipow.v#L74 (the arithmetic proof after the refine statement is not bedrock2-specific)
• how to mention memory in loop invariants: https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/Examples/bsearch.v#L89

Things that we don't really know how to teach

• how to actually prove interesting things about your program. this requires a clear plan and direction, and good understanding of coq to evaluate different choices of stating "the same" thing
• how to understand very generic dependently typed lemmas like `tailrec, copy-pasting their usages is hopefully fine though

[matu3ba]

All links are broken, since they were not pinning a specific commit (instead master).
One usually starts with the target audience and use cases, before going into the "how do I do stuff".

From my point of view there should be an estimation of additional effort vs gain and scalability and some reasoning how this differs to (I guess https://sel4.systems/ is current state of art?).
For example, currently it reads like there are only result semantics taken into consideration but not temporal properties and their combination (usually abstractly modeled with TLA+ because LTL and CTL do compose very poorly).