vcpu: investigate if check in vppi_event can be dropped

[lsf37]

Currently, vppi_event is defined as

  "vppi_event irq = do
     cur_vcpu ← gets (arm_current_vcpu ∘ arch_state);
     case cur_vcpu
       of Some (vcpu_ptr, True) ⇒ do
            do_machine_op $ maskInterrupt True irq;
            vppi ← return $ the $ irq_vppi_event_index irq;
            vcpu_update vcpu_ptr
                        (λvcpu. vcpu⦇ vcpu_vppi_masked := (vcpu_vppi_masked vcpu)(vppi := True) ⦈);
            ct ← gets cur_thread;
            st ← get_thread_state ct;
            ― ‹until a proof links active current vcpu to runnable current thread, we need this
               check: @{term handle_fault} needs a runnable current thread›
            when (runnable st) $ handle_fault ct $ ArchFault $ VPPIEvent irq
          od
        | _ ⇒ return ()
   od"

Since we now have an invariant that the current thread and active vcpu are linked, we might have enough information to drop this check (and any corresponding checks in C).