Open andres-erbsen-sifive opened 5 years ago
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).
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
*
andemp
, no fancy things like magic wand).SeparationLogic.ecancel
is the bedrock2 script to perform cancellation.lia
,ring
documentationCommon infrastructure in bedrock2 (just skim)
bedrock2 semantics (read enough to understand structure)
expr_body
, its callees, andcmd_body
spec_of_
* definitions withWeakestPrecondition.call
and try to think through in your head what the precondition ends up beingstraightline
instead of usingrepeat
refine
statement is not bedrock2-specific)Things that we don't really know how to teach