diff --git a/include-hax/fake_masm/macamd64.inc b/include-hax/fake_masm/macamd64.inc
new file mode 100644
index 0000000000..970487f4dc
--- /dev/null
+++ b/include-hax/fake_masm/macamd64.inc
@@ -0,0 +1,9 @@
+push_reg macro Reg
+	push Reg
+	.pushreg Reg
+	endm
+
+alloc_stack macro Size
+	sub rsp, Size
+	.allocstack Size
+	endm
diff --git a/src/trusted/service_runtime/arch/x86_64/nacl_switch_unwind_win.asm b/src/trusted/service_runtime/arch/x86_64/nacl_switch_unwind_win.asm
index d5dd93a9a1..6ead09486a 100644
--- a/src/trusted/service_runtime/arch/x86_64/nacl_switch_unwind_win.asm
+++ b/src/trusted/service_runtime/arch/x86_64/nacl_switch_unwind_win.asm
@@ -2,7 +2,7 @@
 ; Use of this source code is governed by a BSD-style license that can be
 ; found in the LICENSE file.
 
-include ksamd64.inc
+include macamd64.inc
 
 EXTERN NaClSwitch : QWORD