michaelmcinerney

Make sizes of C structs available in higher level specs

1

It would be convenient to have direct and automatic access to the sizes of C structs in the higher level specs, namely the abstract spec and the design spec, and...

mcs: more uniformly handle ready and release queue updates

2

This introduces library functions for updating the linked lists which use the `tcbSchedNext` and `tcbSchedPrev` pointers of a TCB, and uses these to perform the updates to the ready queues...

Investigate adding `projectKOs` to the simp set

1

`projectKOs` is in the simp set on RISCV64 and AARCH64, but not on the other architectures. We should investigate standardising this and adding it to the simp set on all...

Greater use of heap projections in invariants and in `state_relation` may ease some reasoning in Refine. For example, `pspace_relation`, the greatest component of `state_relation`, could make far greater use of...

There are likely many lemmas in `Detype_C.thy` and `Retype_C.thy` that would be suitable for inclusion within the CParser session. This would reduce duplication and aid any future arch splitting effort

One immediate use is `valid_bound_ntfn'`, which could use the abbreviation `opt_tcb_at'`, which uses `none_top`. Others include places where `case_option` is used, and where `case` statements are used with option types.