Tracking issue: Tock errors

[enjhnsn2]

This issue is intended to track progress on supporting Tock kernel code. Below, I have made two tables describing the code that we currently have to ignore or trust in Tock. As I create minimized examples and create issues for these individual bugs, I will add links here

Trusted functions

Category	Num bugs	Example	Related issues
ICE: to_sort_list called on bound variable list with non-refinements	6	PrioritySched::next	#829
ICE: Expected array or slice type	3	ReadableProcessSlice::copy_to_slice_or_err	#733
assignment might be unsafe caused by extern spec on Option	2	ProcessStandard::switch_to	#782
Cannot move out of non-strong reference	1	ProcessStandard::create	#671
ICE: incompatible types	1	ProcessGrant::access_grant_with_allocator
ICE: Invalid deref of *mut	1	assign_gpios
Other (below)	12	N/A	N/A
Total	26	N/A	N/A

Here I outline the functions that are trusted because of valid refinement errors (i.e., Arithmetic errors, OOB, can't prove predondition, etc.) for my own use.

Other

Category	Num functions	Reasons
Arithmetic	7	Need range spec, bitwise logic
Refinement	3
Need spec for enumerate	1
???	1
Total	12