eliminate `get_tcb`

[lsf37]

This is a medium-size cleanup task.

The function get_tcb defined in ASpec was an early attempt at a nicer accessor function for the heap, specifically for TCBs. It ended up being annoying in proof goals, because there is no good infrastructure around for dealing with the corresponding case splits.

The function does the same thing as the projection tcbs_of, for which we have plenty of infrastructure. We should therefore replace it and use tcbs_of everywhere.

get_tcb is used more extensively in integrity and infoflow. We should specifically replace it there as well. This will hopefully lead to slightly nicer proof in multiple locations.

Draft steps:

• [ ] locate main uses and confirm that this is feasible (183 uses currently)
• [ ] lift definition of tcbs_of from somewhere deep in refinement up into ASpec
• [ ] replace uses of get_tcb in ASpec with tcbs_of. Note different argument order. Probably need to use assert_opt and friends.
• [ ] remove definition of get_tcb so we get errors for uses
• [ ] make sure main simp and update lemmas are available early in AInvs
• [ ] replace uses of get_tcb in proofs with proper projection stacks, esp integrity and infoflow (e.g. tcb_states_of_state)
• [ ] delete update lemmas that are no longer needed with projection stacks
• [ ] fix up proofs