Vectorize x86-64 RC2 mashing schedule scans with SSE2

bench/benches/primitives/rc2_cbc.rs

@@ -3,7 +3,7 @@
 use criterion::Criterion;
 
 /// The library modules whose code these benchmarks run.
-pub const USES: &[&str] = &["rc2_cbc"];
+pub const USES: &[&str] = &["rc2_cbc", "rc2"];
 
 #[cfg(any(
     target_arch = "x86_64",

ci/bench_arches.py

@@ -47,7 +47,7 @@
     "arm": {
         "os": "ubuntu-24.04-arm",
         "image": "ghcr.io/pyca/cryptography-runner-ubuntu-rolling:armv7l",
-        "options": "--env RUSTUP_HOME=/root/.rustup",
+        "options": "--env RUSTUP_HOME=/tmp/verified-garbage-rustup",
     },
 }
 

lean/VerifiedGarbage/Artifacts/Rc2/X86_64.lean

@@ -39,7 +39,7 @@ def artifacts : List Artifact := [
   { Spec.Rc2.encryptBlockApi with
     target := X86_64.target
     doc := Spec.Rc2.encryptBlockApi.doc
-      (notes := ["Baseline x86-64. Mashing scans all 64 schedule words in a fixed order."])
+      (notes := ["Baseline x86-64 SSE2. Mashing scans all 64 schedule words in a fixed order, eight words per vector."])
     code := Impl.Rc2.X86_64.encryptBlock
     contract := Spec.Rc2.encryptBlockContract X86_64.abi
     stack := 0
@@ -48,7 +48,7 @@ def artifacts : List Artifact := [
   { Spec.Rc2.decryptBlockApi with
     target := X86_64.target
     doc := Spec.Rc2.decryptBlockApi.doc
-      (notes := ["Baseline x86-64. Reverse mashing scans all 64 schedule words in a fixed order."])
+      (notes := ["Baseline x86-64 SSE2. Reverse mashing scans all 64 schedule words in a fixed order, eight words per vector."])
     code := Impl.Rc2.X86_64.decryptBlock
     contract := Spec.Rc2.decryptBlockContract X86_64.abi
     stack := 0

lean/VerifiedGarbage/Impl/Rc2/X86_64/Block.lean

@@ -1,4 +1,4 @@
-import VerifiedGarbage.Impl.Rc2.X86_64.Lookup
+import VerifiedGarbage.Impl.Rc2.X86_64.Sse2KeyLookup
 
 /-! # RC2 block encryption and decryption on baseline x86-64 -/
 
@@ -48,7 +48,7 @@ def reverseMix (j i : Nat) : List Instr :=
      .alu .and (wordReg i) (.imm 65535)]
 
 def mash (direction : Spec.Rc2.Direction) (i : Nat) : List Instr :=
-  [rr .rax (wordReg (i + 3))] ++ keyLookup ++
+  [rr .rax (wordReg (i + 3))] ++ Sse2.keyLookup ++
     [.alu (if direction = .encrypt then .add else .sub) (wordReg i) (.reg .rax),
      .alu .and (wordReg i) (.imm 65535)]
 

lean/VerifiedGarbage/Impl/Rc2/X86_64/Sse2KeyLookup.lean

@@ -0,0 +1,15 @@
+import VerifiedGarbage.Impl.Rc2.X86_64.Sse2Lookup
+
+/-! # Eight-way constant-time RC2 schedule scans on baseline x86-64 -/
+
+namespace VG.Impl.Rc2.X86_64.Sse2
+
+open VG.X86_64 VG.Impl.Rc2.X86_64
+
+def keyStep (n : Nat) : List Instr :=
+  [.movdquLoad .xmm4 (memOp .rdi (16 * n))] ++ select
+
+def keyLookup : List Instr :=
+  start .rdx 63 ++ (List.range 8).flatMap keyStep ++ finish .rdx
+
+end VG.Impl.Rc2.X86_64.Sse2

lean/VerifiedGarbage/Proof/Rc2/X86_64/Block.lean

@@ -63,8 +63,15 @@ theorem block_correct (d : Spec.Rc2.Direction) (s : State) (hs : (blockContract
     intro i hi
     rw [h₂.2.rd, h₂.2.wr, h₂.2.reg .rdi (by decide), h₁.1, h₁.2.1, h₁.2.2.1, hrd, hwr]
     exact ⟨⟨s.gpr .rdi, 128⟩, by simp, Offset.contains_base _ (by omega) (by omega)⟩
+  have scans₂ : ScanMemory s₂ := by
+    refine ⟨read₂, ?_, ?_⟩
+    · intro i hi
+      rw [h₂.2.rd, h₂.2.wr, h₂.2.reg .rdi (by decide), h₁.1, h₁.2.1, h₁.2.2.1, hrd, hwr]
+      exact ⟨⟨s.gpr .rdi, 128⟩, by simp, Offset.contains_base _ (by omega) (by omega)⟩
+    · rw [h₂.2.wr, h₂.2.reg .rdx (by decide), h₁.1, h₁.2.2.1, hwr]
+      exact ⟨⟨s.gpr .rdx, 256⟩, by simp, Offset.contains_base _ (by decide) (by decide)⟩
   rw [WP.block_append_iff]
-  apply WP.mono (rounds_ok d s₂ _ h₂.1 read₂)
+  apply WP.mono (rounds_ok d s₂ _ h₂.1 scans₂)
   intro s₃ h₃
   have keep₂₃ := h₂.2.trans h₃.2
   have ptr₃ : s₃.gpr .rsi = s.gpr .rsi := (keep₂₃.reg .rsi (by decide)).trans (congrFun h₁.1 .rsi)

lean/VerifiedGarbage/Proof/Rc2/X86_64/Cipher.lean

@@ -9,11 +9,11 @@ open VG VG.X86_64 VG.Impl.Rc2.X86_64
 theorem foldWords_ok (code : Nat → List Instr)
     (step : Spec.Rc2.Schedule → Nat → Spec.Rc2.State → Spec.Rc2.State) (is : List Nat)
     (correct : ∀ i ∈ is, ∀ (s : State) (v : Spec.Rc2.State), Words s v →
-      (∀ j < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 j) 1) →
+      (ScanMemory s) →
       WP isa (.block (code i)) s (fun s' =>
         Words s' (step (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) i v) ∧ Keep roundWrites s s'))
     (s : State) (v : Spec.Rc2.State) (hv : Words s v)
-    (readable : ∀ j < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 j) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block (is.flatMap code)) s (fun s' =>
       Words s' (is.foldl (fun v i => step (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) i v) v) ∧
       Keep roundWrites s s') := by
@@ -26,9 +26,7 @@ theorem foldWords_ok (code : Nat → List Instr)
     apply WP.mono (correct i (by simp) s v hv readable)
     intro s₁ h₁
     have ptr₁ := h₁.2.reg .rdi (by decide)
-    have read₁ : ∀ j < 128,
-        InRegions (s₁.rd ++ s₁.wr) (s₁.gpr .rdi + BitVec.ofNat 64 j) 1 := by
-      rw [h₁.2.rd, h₁.2.wr, ptr₁]; exact readable
+    have read₁ : ScanMemory s₁ := readable.keep h₁.2 (by decide) (by decide)
     apply WP.mono (ih (fun j hj => correct j (List.mem_cons_of_mem _ hj)) s₁ _ h₁.1 read₁)
     intro s₂ h₂
     refine ⟨?_, h₁.2.trans h₂.2⟩
@@ -37,19 +35,19 @@ theorem foldWords_ok (code : Nat → List Instr)
 
 theorem mixRound_ok (s : State) (v : Spec.Rc2.State) (hv : Words s v)
     (j : Nat) (hj : j < 16)
-    (readable : ∀ k < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 k) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block ((List.range 4).flatMap (fun i => mix (4 * j + i) i))) s (fun s' =>
       Words s' (Spec.Rc2.mixRound (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) j v) ∧
       Keep roundWrites s s') := by
   apply foldWords_ok (step := fun k i v => Spec.Rc2.mix k (4 * j + i) i v) _ _ _ s v hv readable
   intro i hi s v hv readable
   have bound := List.mem_range.mp hi
-  apply WP.mono (mix_ok s v hv i (4 * j + i) bound (by omega) readable)
+  apply WP.mono (mix_ok s v hv i (4 * j + i) bound (by omega) readable.bytes)
   exact fun _ h => ⟨h.1, h.2.round⟩
 
 theorem reverseMixRound_ok (s : State) (v : Spec.Rc2.State) (hv : Words s v)
     (j : Nat) (hj : j < 16)
-    (readable : ∀ k < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 k) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block ([3, 2, 1, 0].flatMap (fun i => reverseMix (4 * j + i) i))) s (fun s' =>
       Words s' (Spec.Rc2.reverseMixRound (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) j v) ∧
       Keep roundWrites s s') := by
@@ -58,7 +56,7 @@ theorem reverseMixRound_ok (s : State) (v : Spec.Rc2.State) (hv : Words s v)
   have bound : i < 4 := by
     simp only [List.mem_cons, List.not_mem_nil, or_false] at hi
     omega
-  apply WP.mono (reverseMix_ok s v hv i (4 * j + i) bound (by omega) readable)
+  apply WP.mono (reverseMix_ok s v hv i (4 * j + i) bound (by omega) readable.bytes)
   exact fun _ h => ⟨h.1, h.2.round⟩
 
 def mashRoundSpec (d : Spec.Rc2.Direction) (k : Spec.Rc2.Schedule)
@@ -73,7 +71,7 @@ def order (d : Spec.Rc2.Direction) : List Nat :=
   | .decrypt => [3, 2, 1, 0]
 
 theorem mashRound_ok (d : Spec.Rc2.Direction) (s : State) (v : Spec.Rc2.State) (hv : Words s v)
-    (readable : ∀ k < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 k) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block ((order d).flatMap (mash d))) s (fun s' =>
       Words s' (mashRoundSpec d (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) v) ∧
       Keep roundWrites s s') := by
@@ -100,7 +98,7 @@ def roundSpec (d : Spec.Rc2.Direction) (k : Spec.Rc2.Schedule) (j : Nat)
 
 theorem round_ok (d : Spec.Rc2.Direction) (s : State) (v : Spec.Rc2.State) (hv : Words s v)
     (j : Nat) (hj : j < 16)
-    (readable : ∀ k < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 k) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block (round d j)) s (fun s' =>
       Words s' (roundSpec d (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) j v) ∧
       Keep roundWrites s s') := by
@@ -111,9 +109,7 @@ theorem round_ok (d : Spec.Rc2.Direction) (s : State) (v : Spec.Rc2.State) (hv :
     by_cases h : j = 4 ∨ j = 10
     · rw [ite_eq_left h]
       have ptr₁ := h₁.2.reg .rdi (by decide)
-      have read₁ : ∀ k < 128,
-          InRegions (s₁.rd ++ s₁.wr) (s₁.gpr .rdi + BitVec.ofNat 64 k) 1 := by
-        rw [h₁.2.rd, h₁.2.wr, ptr₁]; exact readable
+      have read₁ : ScanMemory s₁ := readable.keep h₁.2 (by decide) (by decide)
       apply WP.mono (mashRound_ok d s₁ v₁ h₁.1 read₁)
       intro s₂ h₂
       rw [h₁.2.mem, ptr₁] at h₂
@@ -134,7 +130,7 @@ theorem round_ok (d : Spec.Rc2.Direction) (s : State) (v : Spec.Rc2.State) (hv :
     exact finish s₁ _ h₁
 
 theorem rounds_ok (d : Spec.Rc2.Direction) (s : State) (v : Spec.Rc2.State) (hv : Words s v)
-    (readable : ∀ k < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 k) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block ((List.range 16).flatMap (round d))) s (fun s' =>
       Words s' ((List.range 16).foldl (fun v j => roundSpec d
         (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) j v) v) ∧ Keep roundWrites s s') := by

lean/VerifiedGarbage/Proof/Rc2/X86_64/Rounds.lean

@@ -1,3 +1,5 @@
+import VerifiedGarbage.Proof.Rc2.X86_64.Sse2KeyLookup
+import VerifiedGarbage.Proof.Rc2.X86_64.ScanMemory
 import VerifiedGarbage.Impl.Rc2.X86_64.Block
 import VerifiedGarbage.Proof.Rc2.X86_64.Lookup
 import VerifiedGarbage.Proof.Rc2.Word
@@ -340,8 +342,7 @@ def mashSpec (direction : Spec.Rc2.Direction) (k : Spec.Rc2.Schedule)
 
 theorem mash_ok (direction : Spec.Rc2.Direction) (s : State)
     (v : Spec.Rc2.State) (hv : Words s v) (i : Nat) (hi : i < 4)
-    (readable : ∀ k < 128,
-      InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 k) 1) :
+    (readable : ScanMemory s) :
     WP isa (.block (mash direction i)) s (fun s' =>
       Words s' (mashSpec direction (Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)) i v) ∧
       Keep (wordReg i :: temps) s s') := by
@@ -359,10 +360,8 @@ theorem mash_ok (direction : Spec.Rc2.Direction) (s : State)
     · exact rd_setReg _ _ _
     · exact wr_setReg _ _ _
   have ptr₁ := keep₁.reg .rdi (by decide)
-  have read₁ : ∀ k < 128,
-      InRegions (s₁.rd ++ s₁.wr) (s₁.gpr .rdi + BitVec.ofNat 64 k) 1 := by
-    rw [keep₁.rd, keep₁.wr, ptr₁]; exact readable
-  apply WP.mono (keyLookup_ok s₁ read₁)
+  have read₁ : ScanMemory s₁ := readable.keep keep₁ (by decide) (by decide)
+  apply WP.mono (Sse2.keyLookup_ok s₁ read₁.vectors read₁.scratch)
   intro s₂ h₂
   let k := Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)
   let key := k.getD ((v.getD ((i + 3) % 4) 0 &&& 63).toNat) 0

lean/VerifiedGarbage/Proof/Rc2/X86_64/ScanMemory.lean

@@ -0,0 +1,28 @@
+import VerifiedGarbage.Proof.Rc2.X86_64.Lookup
+
+/-! # Existing contract permissions used by vector schedule scans -/
+
+namespace VG.Proof.Rc2.X86_64
+
+open VG VG.X86_64
+
+structure ScanMemory (s : State) : Prop where
+  bytes : ∀ i < 128, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 i) 1
+  vectors : ∀ i < 8, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 (16 * i)) 16
+  scratch : InRegions s.wr (s.gpr .rdx + BitVec.ofNat 64 64) 16
+
+instance (s : State) : CoeFun (ScanMemory s)
+    (fun _ => ∀ i, i < 128 → InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 i) 1) where
+  coe := fun h => h.bytes
+
+theorem ScanMemory.keep {s s' : State} {rs : List Reg} (h : ScanMemory s)
+    (keep : Keep rs s s') (hk : .rdi ∉ rs) (hs : .rdx ∉ rs) : ScanMemory s' := by
+  constructor
+  · rw [keep.rd, keep.wr, keep.reg .rdi hk]
+    exact h.bytes
+  · rw [keep.rd, keep.wr, keep.reg .rdi hk]
+    exact h.vectors
+  · rw [keep.wr, keep.reg .rdx hs]
+    exact h.scratch
+
+end VG.Proof.Rc2.X86_64

lean/VerifiedGarbage/Proof/Rc2/X86_64/Sse2KeyLookup.lean

@@ -0,0 +1,90 @@
+import VerifiedGarbage.Proof.Rc2.X86_64.Sse2KeySteps
+import VerifiedGarbage.Proof.Rc2.X86_64.Sse2Finish
+
+/-! # Verified constant-time SSE2 schedule lookup -/
+
+namespace VG.Proof.Rc2.X86_64.Sse2
+
+open VG VG.X86_64 VG.Impl.Rc2.X86_64
+
+theorem schedule_readWord (m : Mem) (p : Addr) (i : Nat) (hi : i < 64) :
+    m.readW (p + BitVec.ofNat 64 (2 * i)) 16 = (Spec.Rc2.scheduleAt m p).getD i 0 := by
+  rw [scheduleAt_getD _ _ _ hi]
+  apply BitVec.eq_of_getLsbD_eq
+  intro j hj
+  simp only [Mem.readW, BitVec.getLsbD_setWidth, BitVec.getLsbD_or,
+    BitVec.getLsbD_shiftLeft, decide_eq_true hj, Bool.true_and]
+  rw [getLsbD_read _ _ (by omega)]
+  by_cases h : j < 8
+  · simp only [h, decide_true, Bool.not_true, Bool.false_and, Bool.or_false,
+      Nat.div_eq_of_lt h, Nat.mod_eq_of_lt h, BitVec.add_zero]
+  · have hj' : j - 8 < 8 := by omega
+    simp only [h, decide_false, Bool.not_false]
+    have hdiv : j / 8 = 1 := by omega
+    have hmod : j % 8 = j - 8 := by omega
+    rw [hdiv, hmod]
+    have hp : p + BitVec.ofNat 64 (2 * i) + BitVec.ofNat 64 1 =
+        p + BitVec.ofNat 64 (2 * i + 1) := by rw [BitVec.add_assoc, ← BitVec.ofNat_add]
+    rw [hp]
+    simp (disch := omega) only [BitVec.getLsbD_of_ge, decide_eq_true,
+      Bool.true_and, Bool.false_or]
+
+theorem keyLookup_ok (s : State)
+    (hread : ∀ i < 8, InRegions (s.rd ++ s.wr) (s.gpr .rdi + BitVec.ofNat 64 (16 * i)) 16)
+    (hwrite : InRegions s.wr (s.gpr .rdx + BitVec.ofNat 64 64) 16) :
+    WP isa (.block Impl.Rc2.X86_64.Sse2.keyLookup) s (fun s' =>
+      s'.gpr .rax = ((Spec.Rc2.scheduleAt s.mem (s.gpr .rdi)).getD
+        ((s.gpr .rax).setWidth 6).toNat 0).setWidth 64 ∧
+      Keep [.rax, .rcx, .r8, .r9, .r10, .r11] s s') := by
+  have hsread : InRegions (s.rd ++ s.wr) (s.gpr .rdx + BitVec.ofNat 64 64) 16 := by
+    obtain ⟨r, hr, hc⟩ := hwrite
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  rw [Impl.Rc2.X86_64.Sse2.keyLookup, List.append_assoc, WP.block_append_iff]
+  obtain ⟨s₁, run₁, input₁, zero₁, idx₁, ones₁, eights₁, saved₁, keep₁⟩ := keyStart_ok s .rdx hsread
+  refine WP.of_runBlock ⟨s₁, run₁, ?_⟩
+  rw [WP.block_append_iff, List.range_eq_range']
+  let x : Byte := ((s.gpr .rax).setWidth 6).setWidth 8
+  let f (i : Nat) := s.mem.readW (s.gpr .rdi + BitVec.ofNat 64 (2 * i)) 16
+  have inv₁ : KeyScanInv f x 0 s₁ :=
+    ⟨input₁, zero₁.trans (acc_zero _ _).symm, idx₁, ones₁, eights₁⟩
+  have hf₁ : ∀ i < 64, f i = s₁.mem.readW (s₁.gpr .rdi + BitVec.ofNat 64 (2 * i)) 16 := by
+    rw [keep₁.mem, keep₁.reg .rdi (by decide)]
+    intro _ _; rfl
+  have hr₁ : ∀ i < 8, InRegions (s₁.rd ++ s₁.wr) (s₁.gpr .rdi + BitVec.ofNat 64 (16 * i)) 16 := by
+    rw [keep₁.rd, keep₁.wr, keep₁.reg .rdi (by decide)]; exact hread
+  apply WP.mono (keySteps_ok 8 0 (by decide) s₁ f x inv₁ hf₁ hr₁)
+  intro s₂ h₂
+  rw [Impl.Rc2.X86_64.Sse2.finish, WP.block_append_iff]
+  obtain ⟨s₃, run₃, reduced₃, keep₃⟩ := reduceOr_ok s₂
+  refine WP.of_runBlock ⟨s₃, run₃, ?_⟩
+  have keep₂ : Keep [.rax, .r10] s₁ s₂ := h₂.2.1.weaken (by simp)
+  have keep₃' : Keep [.rax, .r10] s₂ s₃ := keep₃.keep.weaken (by simp)
+  have kept : Keep [.rax, .r10] s s₃ := (keep₁.trans keep₂).trans keep₃'
+  have ptr : s₃.gpr .rdx = s.gpr .rdx := kept.reg .rdx (by decide)
+  have wr₃ : InRegions s₃.wr (s₃.gpr .rdx + BitVec.ofNat 64 64) 16 := by
+    rw [kept.wr, ptr]; exact hwrite
+  have rd₃ : InRegions (s₃.rd ++ s₃.wr) (s₃.gpr .rdx + BitVec.ofNat 64 64) 8 := by
+    rw [kept.rd, kept.wr, ptr]
+    obtain ⟨r, hr, hc⟩ := hsread
+    exact ⟨r, hr, by unfold Region.Contains at hc ⊢; omega⟩
+  have saved₃ : s₃.xmm .xmm8 = s₃.mem.readW (s₃.gpr .rdx + BitVec.ofNat 64 64) 128 := by
+    rw [keep₃.xmm .xmm8 (by decide), h₂.2.2, saved₁, kept.mem, ptr]
+  obtain ⟨s₄, run₄, out₄, keep₄⟩ := finishTail_ok s₃ .rdx (by decide) rd₃ wr₃ saved₃
+  refine WP.of_runBlock ⟨s₄, run₄, ?_⟩
+  constructor
+  · have xb : x.toNat < 64 := by
+      simp only [x, BitVec.toNat_setWidth]
+      have h := ((s.gpr .rax).setWidth 6).isLt
+      simp only [BitVec.toNat_setWidth] at h
+      omega
+    have xe : x.toNat = ((s.gpr .rax).setWidth 6).toNat := by
+      simp only [x, BitVec.toNat_setWidth]
+      have h := ((s.gpr .rax).setWidth 6).isLt
+      simp only [BitVec.toNat_setWidth] at h
+      omega
+    rw [out₄, reduced₃, h₂.1.acc, reduce_acc, ite_eq_left xb]
+    dsimp only [f]
+    rw [schedule_readWord _ _ _ xb, xe]
+  · exact (kept.trans (keep₄.weaken (by simp))).weaken (by simp)
+
+end VG.Proof.Rc2.X86_64.Sse2

lean/VerifiedGarbage/Proof/Rc2/X86_64/Sse2KeyStart.lean

@@ -0,0 +1,49 @@
+import VerifiedGarbage.Proof.Rc2.X86_64.Sse2Vector
+import VerifiedGarbage.Impl.Rc2.X86_64.Sse2KeyLookup
+
+/-! # Initialization of SSE2 RC2 schedule lookup state -/
+
+namespace VG.Proof.Rc2.X86_64.Sse2
+
+open VG VG.X86_64 VG.X86_64.RegUpd VG.Impl.Rc2.X86_64
+
+theorem keyStart_ok (s : State) (scratch : Reg)
+    (hread : InRegions (s.rd ++ s.wr) (s.gpr scratch + BitVec.ofNat 64 64) 16) :
+    ∃ s', runBlock isa (Sse2.start scratch 63) s = some s' ∧
+      s'.xmm .xmm0 = broadcast (((s.gpr .rax).setWidth 6).setWidth 8) ∧
+      s'.xmm .xmm1 = 0#128 ∧ s'.xmm .xmm2 = Sse2.indices 0 ∧
+      s'.xmm .xmm6 = Sse2.ones ∧ s'.xmm .xmm7 = Sse2.eights ∧
+      s'.xmm .xmm8 = s.mem.readW (s.gpr scratch + BitVec.ofNat 64 64) 128 ∧
+      Keep [.rax, .r10] s s' := by
+  refine ⟨_, by
+    simp (config := {decide := true}) only [Sse2.start, Sse2.loadConst,
+      List.cons_append, List.nil_append,
+      runBlock_cons, runStep_some, runBlock_nil, exec, execAlu, readSrc, XOp.exec,
+      State.load128, State.ea, memOp, offset_nat, hread, ite_true, Option.bind_some,
+      Option.map_some, gpr_setReg, gpr_setXmm, gpr_arithFlags,
+      xmm_setReg, xmm_setXmm_self, xmm_setXmm_of_ne]
+    rfl, ?_⟩
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · simp (config := {decide := true}) only [xmm_setXmm_self, xmm_setXmm_of_ne, xmm_setReg]
+    rw [show (63#32).signExtend 64 = (63 : BitVec 64) by decide, maskIndex]
+    apply ext_word
+    intro i hi
+    rw [broadcast, word_ofWords _ hi]
+    simpa using broadcast_word (((s.gpr .rax).setWidth 6).setWidth 8) i hi
+  · simp (config := {decide := true}) only [xmm_setXmm_self, xmm_setXmm_of_ne, xmm_setReg,
+      XBinOp.eval, BitVec.xor_self]
+  · simp (config := {decide := true}) only [xmm_setXmm_self, xmm_setXmm_of_ne, xmm_setReg]
+  · simp (config := {decide := true}) only [xmm_setXmm_self, xmm_setXmm_of_ne, xmm_setReg]
+  · simp only [xmm_setXmm_self]
+    exact movq_const _
+  · simp (config := {decide := true}) only [xmm_setXmm_of_ne, xmm_setReg,
+      xmm_arithFlags, xmm_setXmm_self]
+  · constructor
+    · intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+      simp only [gpr_setXmm, gpr_setReg_of_ne _ _ hr.1, gpr_setReg_of_ne _ _ hr.2, gpr_arithFlags]
+    · simp only [mem_setXmm, mem_setReg, mem_arithFlags]
+    · simp only [rd_setXmm, rd_setReg, rd_arithFlags]
+    · simp only [wr_setXmm, wr_setReg, wr_arithFlags]
+
+end VG.Proof.Rc2.X86_64.Sse2