Amend formalisation following the feedback from POPL21 artifact evaluation

In response to the concerns and suggestions from the POPL21 artifact evaluation team, we make the following changes:

1. The adequacy theorem receives a more direct statement in line with other Iris-based developments (the language HeapLang itself being such an example). The necessary amendments were all derived by one of the reviewers (Reviewer A).

2. An implementation of QueueLib is added to the theory queue_lib.v.

3. Minor corrections and enhancements to the README.md page and the scheduler.v theory are also performed.