Argon2 on x86-64: prove complete independent-address generation

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCalls.lean

@@ -0,0 +1,37 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressHeader
+import VerifiedGarbage.Impl.Argon2.X86_64.ClearBlock
+import VerifiedGarbage.Spec.Argon2.Contract
+
+/-! Independent-address generation in the shared 16 KiB scratch allocation.
+G uses `[0,4096)`, temporary output `[4096,5120)`, input `[5120,6144)`,
+address output `[6144,7168)`, and the zero block `[7168,8192)`. Every stage
+reloads the scratch pointer from frame offset 248 after a compression call.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressCalls
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def pointer (offset : Nat) : List Instr := [
+  .mov .rdi (.mem (at_ .rbp 248)), .alu .add .rdi (.imm (BitVec.ofNat 32 offset))]
+
+def args (x y out : Nat) : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)),
+  .mov .rdi (.reg .rcx), .alu .add .rdi (.imm (BitVec.ofNat 32 x)),
+  .mov .rsi (.reg .rcx), .alu .add .rsi (.imm (BitVec.ofNat 32 y)),
+  .mov .rdx (.reg .rcx), .alu .add .rdx (.imm (BitVec.ofNat 32 out))]
+
+def stage (x y out : Nat) : Prog isa := .seq (.block (args x y out))
+  (.call Spec.Argon2.compressApi.name VG.Impl.Argon2.X86_64.compress)
+
+def calls : Prog isa := .seq (stage 7168 5120 4096) (stage 7168 4096 6144)
+
+def clearAt (offset : Nat) : Prog isa := .seq (.block (pointer offset)) ClearBlock.code
+
+def prepare : Prog isa := .seq (clearAt 5120) (.seq (clearAt 7168)
+  (.seq (.block (pointer 5120)) AddressHeader.code))
+
+def code : Prog isa := .seq prepare calls
+
+end VG.Impl.Argon2.X86_64.AddressCalls

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCalls.lean

@@ -0,0 +1,64 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsStage
+import VerifiedGarbage.Proof.Argon2.AddressInput
+
+/-! Both compression calls produce exactly the reviewed independent-address block. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+def writes (s : State) : List Region := [⟨work s, 8192⟩, below (s.gpr .rsp) 8]
+
+structure Generated (s t : State) (p : Params) (pass lane slice counter : Nat) : Prop where
+  block : blockAt t.mem (off (work s) 6144) = addressBlock p pass lane slice counter
+  ready : Ready t
+  work : work t = work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (writes s) s.mem t.mem
+
+theorem stage_frame_full {s t : State} {out : Nat} (bound : out + 1024 ≤ 8192)
+    (hf : Frame (stageWrites s out) s.mem t.mem) : Frame (writes s) s.mem t.mem := by
+  apply hf.sub
+  intro r hr
+  simp only [stageWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl
+  · exact ⟨⟨work s, 8192⟩, by simp [writes], Offset.sub_base _ bound⟩
+  · exact ⟨⟨work s, 8192⟩, by simp [writes], Region.sub_prefix (by decide)⟩
+  · exact ⟨_, by simp [writes], fun _ h => h⟩
+
+theorem zero_preserved {s t : State} (h : Ready s)
+    (hf : Frame (stageWrites s 4096) s.mem t.mem) :
+    blockAt t.mem (off (work s) 7168) = blockAt s.mem (off (work s) 7168) := by
+  apply FillCompress.block_frame hf
+  intro r hr
+  simp only [stageWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl
+  · exact Offset.disjoint _ (by decide) (by decide) (by decide)
+  · exact Offset.disjoint_base _ (by decide) (by decide)
+  · exact (h.stackWork.sub_right (Offset.sub_base _ (by decide))).symm
+
+theorem calls_ok (p : Params) (pass lane slice counter : Nat) (s : State) (h : Ready s)
+    (zero : blockAt s.mem (off (work s) 7168) = zeroBlock)
+    (input : blockAt s.mem (off (work s) 5120) = Proof.Argon2.addressInput p pass lane slice counter) :
+    WP isa calls s (Generated s · p pass lane slice counter) := by
+  unfold calls
+  refine WP.seq ((stage_ok s h 7168 5120 4096 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide)).mono ?_)
+  intro a first
+  refine (stage_ok a first.ready 7168 4096 6144 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide)).mono ?_
+  intro t second
+  refine ⟨?_, second.ready, second.work.trans first.work,
+    fun r hr => (second.regs r hr).trans (first.regs r hr),
+    second.rd.trans first.rd, second.wr.trans first.wr, ?_⟩
+  · have result := second.result
+    rw [first.work, zero_preserved h first.frame, zero, first.result, zero, input] at result
+    rw [Proof.Argon2.addressBlock_eq]
+    exact result
+  · have next := stage_frame_full (by decide) second.frame
+    simp only [writes, first.work, first.regs .rsp (by simp [calleeSaved])] at next
+    exact (stage_frame_full (by decide) first.frame).trans next
+
+end VG.Proof.Argon2.X86_64.AddressCalls

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsArgs.lean

@@ -0,0 +1,49 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCalls
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressHeaderWords
+
+/-! Independent-address compression arguments from one fixed frame read. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCalls
+
+def work (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 248) 64
+
+def displacement (n : Nat) : Addr := BitVec.signExtend 64 (BitVec.ofNat 32 n)
+
+theorem pointer_ok (s : State) (offset : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block (pointer offset)) s fun t =>
+      t.gpr .rdi = work s + displacement offset ∧ Divide.Keeps [.rdi] s t := by
+  apply WP.of_runBlock
+  simp only [pointer, work, displacement, runBlock_cons, runStep_some, runBlock_nil,
+    exec, readSrc, State.load64, ea_at, hr, execAlu, RegUpd.gpr_setReg,
+    RegUpd.gpr_arithFlags, ite_true, Option.map_some,
+    Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    simp only [RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, hr, ite_false]
+  all_goals rfl
+
+theorem args_ok (s : State) (x y out : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block (args x y out)) s fun t =>
+      t.gpr .rcx = work s ∧ t.gpr .rdi = work s + displacement x ∧
+      t.gpr .rsi = work s + displacement y ∧ t.gpr .rdx = work s + displacement out ∧
+      Divide.Keeps [.rcx, .rdi, .rsi, .rdx] s t := by
+  apply WP.of_runBlock
+  simp only [args, work, displacement, runBlock_cons, runStep_some, runBlock_nil,
+    exec, readSrc, State.load64, ea_at, hr, execAlu, RegUpd.gpr_setReg,
+    RegUpd.gpr_arithFlags, reduceCtorEq, ite_true, ite_false, Option.map_some,
+    Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, trivial, trivial, trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+    simp only [RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, hr.1, hr.2.1,
+      hr.2.2.1, hr.2.2.2, ite_false]
+  all_goals rfl
+
+end VG.Proof.Argon2.X86_64.AddressCalls

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsCT.lean

@@ -0,0 +1,94 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCalls
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCallCT
+
+/-! The two address-generation compression calls have public fixed addresses. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCalls
+
+structure Related (s t : State) : Prop where
+  left : Ready s
+  right : Ready t
+  bases : s.gpr .rbp = t.gpr .rbp
+  stacks : s.gpr .rsp = t.gpr .rsp
+  work : work s = work t
+
+structure CallRelated (s t : State) : Prop where
+  left : FillCompress.CallReady s
+  right : FillCompress.CallReady t
+  args : ∀ r ∈ [Reg.rdi, .rsi, .rdx, .rcx, .rsp], s.gpr r = t.gpr r
+
+theorem first_args_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block (args 7168 5120 4096)) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp])
+    (fun _ _ h => Taint.agree_ofRegs (by
+      intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      subst r
+      exact h)) (by taint_decide)
+
+theorem second_args_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block (args 7168 4096 6144)) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp])
+    (fun _ _ h => Taint.agree_ofRegs (by
+      intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      subst r
+      exact h)) (by taint_decide)
+
+theorem args_public_rel (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192)
+    (argTrace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+      (.block (args x y out)) (fun _ _ => True)) :
+    RelCT isa Related (.block (args x y out)) CallRelated := by
+  have trace := argTrace.mono (P' := Related) (fun _ _ hp => hp.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t hp =>
+    ⟨args_nat_ok s hp.left x y out (by omega) (by omega) (by omega),
+      args_nat_ok t hp.right x y out (by omega) (by omega) (by omega)⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨args_call_ready s a hp.left x y out hx hy ho bx by_ bo ha,
+    args_call_ready t b hp.right x y out hx hy ho bx by_ bo hb, ?_⟩
+  intro r hr
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl | rfl
+  · exact ha.left.trans ((congrArg (fun p => off p x) hp.work).trans hb.left.symm)
+  · exact ha.right.trans ((congrArg (fun p => off p y) hp.work).trans hb.right.symm)
+  · exact ha.output.trans ((congrArg (fun p => off p out) hp.work).trans hb.output.symm)
+  · exact ha.scratch.trans (hp.work.trans hb.scratch.symm)
+  · exact (ha.keeps.regs .rsp (by decide)).trans
+      (hp.stacks.trans (hb.keeps.regs .rsp (by decide)).symm)
+
+theorem stage_rel (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192)
+    (argTrace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+      (.block (args x y out)) (fun _ _ => True)) :
+    RelCT isa Related (stage x y out) Related := by
+  have call := FillCompress.call_rel Spec.Argon2.compressApi.name (P := CallRelated)
+    (fun _ _ hp => ⟨hp.left, hp.right, hp.args .rdi (by simp), hp.args .rsi (by simp),
+      hp.args .rdx (by simp), hp.args .rcx (by simp), hp.args .rsp (by simp)⟩)
+  have trace := (args_public_rel x y out hx hy ho bx by_ bo argTrace).seq call
+  have full := trace.wpDep (fun s t hp =>
+    ⟨stage_ok s hp.left x y out hx hy ho bx by_ bo,
+      stage_ok t hp.right x y out hx hy ho bx by_ bo⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact ⟨ha.ready, hb.ready,
+    (ha.regs .rbp (by simp [calleeSaved])).trans
+      (hp.bases.trans (hb.regs .rbp (by simp [calleeSaved])).symm),
+    (ha.regs .rsp (by simp [calleeSaved])).trans
+      (hp.stacks.trans (hb.regs .rsp (by simp [calleeSaved])).symm),
+    ha.work.trans (hp.work.trans hb.work.symm)⟩
+
+theorem calls_rel : RelCT isa Related calls Related :=
+  (stage_rel 7168 5120 4096 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide) first_args_rel).seq
+  (stage_rel 7168 4096 6144 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide) second_args_rel)
+
+end VG.Proof.Argon2.X86_64.AddressCalls

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsClear.lean

@@ -0,0 +1,64 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsStage
+import VerifiedGarbage.Proof.Argon2.X86_64.ClearBlock
+
+/-! Clear an address-generation block, retaining the allocation invariants. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+structure Cleared (s t : State) (offset : Nat) : Prop where
+  block : blockAt t.mem (off (work s) offset) = zeroBlock
+  ready : Ready t
+  work_eq : work t = work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame [⟨off (work s) offset, 1024⟩] s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+
+theorem clearAt_ok (s : State) (h : Ready s) (offset : Nat) (bound : offset + 1024 ≤ 8192) :
+    WP isa (clearAt offset) s (Cleared s · offset) := by
+  unfold clearAt
+  refine WP.seq ((pointer_ok s offset h.frameRead).mono ?_)
+  rintro a ⟨dest, keeps⟩
+  rw [displacement_eq offset (by omega)] at dest
+  have write : Covers [⟨a.gpr .rdi, 1024⟩] a.wr := by
+    rw [dest, keeps.wr]; exact work_cover s h offset 1024 bound
+  refine (ClearBlock.code_ok a write).mono ?_
+  rintro t ⟨zero, frame, tk, mx⟩
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r := by
+    intro r hr
+    have ne : r ≠ .rax ∧ r ≠ .rdi := by
+      simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+    exact (tk.1 r ne.1).trans (keeps.regs r (by simpa only [List.mem_cons, List.not_mem_nil, or_false] using ne.2))
+  have rd := tk.2.1.trans keeps.rd
+  have wr := tk.2.2.trans keeps.wr
+  have hf : Frame [⟨off (work s) offset, 1024⟩] s.mem t.mem := by
+    rw [dest, keeps.mem] at frame; exact frame
+  have bigger : Frame (stageWrites s offset) s.mem t.mem :=
+    hf.mono (by
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      simp [stageWrites])
+  obtain ⟨ready, work'⟩ := ready_of_frame h offset bound regs rd wr bigger
+  rw [dest] at zero
+  exact ⟨zero, ready, work', regs, rd, wr, hf, mx.trans keeps.mxcsr⟩
+
+theorem Cleared.full_frame {s t : State} {offset : Nat} (h : Cleared s t offset)
+    (bound : offset + 1024 ≤ 8192) : Frame [⟨work s, 8192⟩] s.mem t.mem := by
+  apply h.frame.sub
+  intro r hr
+  simp only [List.mem_singleton] at hr
+  subst r
+  exact ⟨⟨work s, 8192⟩, by simp, Offset.sub_base _ bound⟩
+
+theorem frame_word {s t : State} (h : Ready s) (frame : Frame [⟨work s, 8192⟩] s.mem t.mem)
+    (d : Nat) (bound : d + 8 ≤ 272) :
+    t.mem.readW (off (s.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 :=
+  frame.readW (r := ⟨s.gpr .rbp, 272⟩) (Offset.contains_base _ bound (by omega))
+    (by intro r hr; simp only [List.mem_singleton] at hr; subst r; exact h.frameWork) (by decide)
+
+end VG.Proof.Argon2.X86_64.AddressCalls

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsLayout.lean

@@ -0,0 +1,79 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCall
+
+/-! Permissions and separation for either address-generation compression call. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64
+
+structure Ready (s : State) : Prop where
+  frameRead : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8
+  workWrite : Covers [⟨work s, 8192⟩] s.wr
+  frameWork : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨work s, 8192⟩
+  frameStack : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint (below (s.gpr .rsp) 8)
+  stackWork : (below (s.gpr .rsp) 8).Disjoint ⟨work s, 8192⟩
+
+theorem displacement_eq (n : Nat) (bound : n ≤ 8192) : displacement n = BitVec.ofNat 64 n := by
+  have n32 : n < 2 ^ 32 := by omega
+  have msb : (BitVec.ofNat 32 n).msb = false := by
+    rw [BitVec.msb_eq_false_iff_two_mul_lt, BitVec.toNat_ofNat, Nat.mod_eq_of_lt n32]
+    omega
+  unfold displacement
+  rw [BitVec.signExtend_eq_setWidth_of_msb_false msb,
+    BitVec.setWidth_ofNat_of_le_of_lt (by decide) n32]
+
+theorem work_cover (s : State) (h : Ready s) (d n : Nat) (hd : d + n ≤ 8192) :
+    Covers [⟨off (work s) d, n⟩] s.wr := by
+  have sub : Covers [⟨off (work s) d, n⟩] [⟨work s, 8192⟩] := by
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.mem_singleton] at hr
+    subst r
+    exact ⟨⟨work s, 8192⟩, by simp, d, rfl, hd⟩
+  exact fun p n hp => h.workWrite p n (sub p n hp)
+
+structure Args (s a : State) (x y out : Nat) : Prop where
+  scratch : a.gpr .rcx = work s
+  left : a.gpr .rdi = off (work s) x
+  right : a.gpr .rsi = off (work s) y
+  output : a.gpr .rdx = off (work s) out
+  keeps : Divide.Keeps [.rcx, .rdi, .rsi, .rdx] s a
+
+theorem args_nat_ok (s : State) (h : Ready s) (x y out : Nat)
+    (hx : x ≤ 8192) (hy : y ≤ 8192) (ho : out ≤ 8192) :
+    WP isa (.block (Impl.Argon2.X86_64.AddressCalls.args x y out)) s (Args s · x y out) := by
+  refine (args_ok s x y out h.frameRead).mono ?_
+  rintro a ⟨scratch, left, right, output, keeps⟩
+  rw [displacement_eq x hx] at left
+  rw [displacement_eq y hy] at right
+  rw [displacement_eq out ho] at output
+  exact ⟨scratch, left, right, output, keeps⟩
+
+theorem args_call_ready (s a : State) (h : Ready s) (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192)
+    (args : Args s a x y out) : FillCompress.CallReady a := by
+  have read (d : Nat) (hd : d + 1024 ≤ 8192) :
+      Covers [⟨off (work s) d, 1024⟩] (a.rd ++ a.wr) := by
+    rw [args.keeps.rd, args.keeps.wr]
+    intro p n hp
+    obtain ⟨r, hr, hc⟩ := work_cover s h d 1024 hd p n hp
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  have sp : a.gpr .rsp = s.gpr .rsp := args.keeps.regs .rsp (by decide)
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · rw [args.left]; exact read x bx
+  · rw [args.right]; exact read y by_
+  · rw [args.output, args.keeps.wr]; exact work_cover s h out 1024 bo
+  · rw [args.scratch, args.keeps.wr]
+    simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero]
+      using work_cover s h 0 4096 (by decide)
+  · rw [args.left, args.scratch]; exact Offset.disjoint_base _ hx (by omega)
+  · rw [args.right, args.scratch]; exact Offset.disjoint_base _ hy (by omega)
+  · rw [args.output, args.scratch]; exact Offset.disjoint_base _ ho (by omega)
+  · rw [sp, args.left]; exact h.stackWork.sub_right (Offset.sub_base _ bx)
+  · rw [sp, args.right]; exact h.stackWork.sub_right (Offset.sub_base _ by_)
+  · rw [sp, args.output]; exact h.stackWork.sub_right (Offset.sub_base _ bo)
+  · rw [sp, args.scratch]; exact h.stackWork.sub_right (Region.sub_prefix (by decide))
+
+end VG.Proof.Argon2.X86_64.AddressCalls