KiJeong-Lim

(* plf/Equiv.v *)

Lemma aeval_weakening : forall x st a ni,
  var_not_used_in_aexp x a ->
  aeval (x !-> ni ; st) a = aeval st a.
Proof.
  intros. induction H; simpl; try congruence.
  eapply t_update_neq; eauto.
Qed.

Cr4sh

/*
 *********************************************************************

  Part of UEFI DXE driver code that injects Hyper-V VM exit handler
  backdoor into the Device Guard enabled Windows 10 Enterprise.
  
  Execution starts from new_ExitBootServices() -- a hook handler 
  for EFI_BOOT_SERVICES.ExitBootServices() which being called by
  winload!OslFwpKernelSetupPhase1(). After DXE phase exit winload.efi
  transfers exeution to previously loaded Hyper-V kernel (hvix64.sys)