Vectorize x86-64 RC2 key expansion and mashing 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

@@ -30,7 +30,7 @@ def artifacts : List Artifact := [
   { Spec.Rc2.expandKeyApi with
     target := X86_64.target
     doc := Spec.Rc2.expandKeyApi.doc
-      (notes := ["Baseline x86-64. PITABLE selection scans all 256 candidates in a fixed order."])
+      (notes := ["Baseline x86-64 SSE2. PITABLE selection scans all 256 candidates in a fixed order, eight candidates per vector."])
     code := Impl.Rc2.X86_64.expandKey
     contract := Spec.Rc2.expandKeyContract X86_64.abi
     stack := 0
@@ -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/ExpandKey.lean

@@ -1,10 +1,10 @@
-import VerifiedGarbage.Impl.Rc2.X86_64.Lookup
+import VerifiedGarbage.Impl.Rc2.X86_64.Sse2Lookup
 
 /-! # RC2 key expansion on baseline x86-64
 
 The public key length controls copying and expansion. The effective bit
 count controls the reduction mask and descending loop. PITABLE selection
-always scans all 256 candidates with arithmetic masks.
+always scans all 256 candidates with eight parallel SSE2 arithmetic masks.
 -/
 
 namespace VG.Impl.Rc2.X86_64
@@ -27,7 +27,7 @@ def copyKey : List Instr :=
 
 def fillKey : List Instr :=
   [.movzx8 .rax (indexed .r14 .rbx (-1)), rr .r9 .rbx, .alu .sub .r9 (.reg .r13),
-   .movzx8 .rcx (indexed .r14 .r9), .alu .add .rax (.reg .rcx)] ++ piLookup ++
+   .movzx8 .rcx (indexed .r14 .r9), .alu .add .rax (.reg .rcx)] ++ Sse2.piLookup ++
     [.store8 (indexed .r14 .rbx) .rax, .alu .add .rbx (.imm 1), .alu .cmp .rbx (.imm 128)]
 
 /-- TM = 2^(T1 mod 8) - 1, with TM = 255 for a multiple of eight. All
@@ -39,13 +39,13 @@ def maskCode : Prog isa :=
         (.seq (.ite .e (.block [imm .rdx (2 ^ (i + 1) - 1)]) (.block [])) rest)) (.block []))
 
 def reduceKey : List Instr :=
-  [.movzx8 .rax (indexed .r14 .rbx), .alu .and .rax (.reg .rdx)] ++ piLookup ++
+  [.movzx8 .rax (indexed .r14 .rbx), .alu .and .rax (.reg .rdx)] ++ Sse2.piLookup ++
     [.store8 (indexed .r14 .rbx) .rax]
 
 def descendKey : List Instr :=
   [.alu .sub .rbx (.imm 1), .movzx8 .rax (indexed .r14 .rbx 1), rr .r9 .rbx,
    .alu .add .r9 (.reg .rbp), .movzx8 .rcx (indexed .r14 .r9), .alu .xor .rax (.reg .rcx)] ++
-    piLookup ++ [.store8 (indexed .r14 .rbx) .rax, .alu .cmp .rbx (.imm 0)]
+    Sse2.piLookup ++ [.store8 (indexed .r14 .rbx) .rax, .alu .cmp .rbx (.imm 0)]
 
 def expandCopyFill : Prog isa :=
   .seq (.loop (.block copyKey) .ne)

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/Impl/Rc2/X86_64/Sse2Lookup.lean

@@ -0,0 +1,52 @@
+import VerifiedGarbage.Impl.Rc2.X86_64.Lookup
+
+/-! # Eight-way constant-time RC2 scans on baseline x86-64
+
+SSE2 is part of the target baseline. Each word-sized XOR is at most 255;
+subtracting one and shifting arithmetically produces a full equality mask.
+The scans visit every candidate in order, eight candidates per vector.
+The temporary vector store is restored before returning.
+-/
+
+namespace VG.Impl.Rc2.X86_64.Sse2
+
+open VG.X86_64 VG.Impl.Rc2.X86_64
+
+def loadConst (dst : XReg) (v : BitVec 128) : List Instr :=
+  [.movImm64 .r10 (v.extractLsb' 0 64), .xop (.movq dst .r10),
+   .movImm64 .r10 (v.extractLsb' 64 64), .xop (.movq .xmm5 .r10),
+   .xop (.bin .punpcklqdq dst .xmm5)]
+
+def indices (n : Nat) : BitVec 128 := ofWords fun j => BitVec.ofNat 16 (8 * n + j)
+def ones : BitVec 128 := ofWords fun _ => 1
+def eights : BitVec 128 := ofWords fun _ => 8
+def piValues (n : Nat) : BitVec 128 :=
+  ofWords fun j => (VG.Spec.Rc2.piTable.getD (8 * n + j) 0).setWidth 16
+
+def start (scratch : Reg) (mask : Nat) : List Instr :=
+  [.movdquLoad .xmm8 (memOp scratch 64), .alu .and .rax (.imm (BitVec.ofNat 32 mask)),
+   .xop (.movq .xmm0 .rax), .xop (.bin .punpcklwd .xmm0 .xmm0),
+   .xop (.pshufd .xmm0 .xmm0 0), .xop (.bin .pxor .xmm1 .xmm1)] ++
+   loadConst .xmm2 (indices 0) ++ loadConst .xmm6 ones ++ loadConst .xmm7 eights
+
+def select : List Instr :=
+  [.xop (.bin .movdqa .xmm3 .xmm0), .xop (.bin .pxor .xmm3 .xmm2),
+   .xop (.bin .psubw .xmm3 .xmm6), .xop (.shift .psraw .xmm3 15),
+   .xop (.bin .pand .xmm3 .xmm4), .xop (.bin .por .xmm1 .xmm3),
+   .xop (.bin .paddw .xmm2 .xmm7)]
+
+def piStep (n : Nat) : List Instr := loadConst .xmm4 (piValues n) ++ select
+
+def reduceOr : List Instr :=
+  [8, 4, 2].flatMap fun n =>
+    [.xop (.bin .movdqa .xmm3 .xmm1), .xop (.shift .psrldq .xmm3 (BitVec.ofNat 8 n)),
+     .xop (.bin .por .xmm1 .xmm3)]
+
+def finish (scratch : Reg) : List Instr := reduceOr ++
+  [.movdquStore (memOp scratch 64) .xmm1, .mov .rax (.mem (memOp scratch 64)),
+   .alu .and .rax (.imm 65535), .movdquStore (memOp scratch 64) .xmm8]
+
+def piLookup : List Instr :=
+  start .r8 255 ++ (List.range 32).flatMap piStep ++ finish .r8
+
+end VG.Impl.Rc2.X86_64.Sse2

lean/VerifiedGarbage/Proof/Rc2/RestoreMemory.lean

@@ -0,0 +1,19 @@
+import VerifiedGarbage.Proof.Framework.Mem
+
+/-! # Restoring a temporary vector store exactly -/
+
+namespace VG.Proof.Rc2
+
+theorem restore128 (m : VG.Mem) (p : VG.Addr) (v : BitVec 128) :
+    (m.writeW p v).writeW p (m.readW p 128) = m := by
+  funext q
+  by_cases h : (q - p).toNat < 16
+  · simp only [VG.Mem.writeW, VG.Mem.write, BitVec.setWidth_eq, h, ite_true,
+      VG.Mem.readW]
+    rw [VG.Mem.extractLsb'_read m p h]
+    have he : p + BitVec.ofNat 64 (q - p).toNat = q := by
+      rw [BitVec.ofNat_toNat, BitVec.setWidth_eq, BitVec.add_comm p, BitVec.sub_add_cancel]
+    rw [he]
+  · simp only [VG.Mem.writeW, VG.Mem.write, h, ite_false]
+
+end VG.Proof.Rc2

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/DescendKey.lean

@@ -6,7 +6,8 @@ namespace VG.Proof.Rc2.X86_64
 
 open VG VG.X86_64 VG.Impl.Rc2.X86_64
 
-theorem descendLoop_ok (s : State) (l : KeyBytes) (t8 : Nat) (ht : 1 ≤ t8) (ht' : t8 < 128)
+theorem descendLoop_ok (s : State)
+    (hlookup : InRegions s.wr (s.gpr .r8 + BitVec.ofNat 64 64) 16) (l : KeyBytes) (t8 : Nat) (ht : 1 ≤ t8) (ht' : t8 < 128)
     (len : s.gpr .rbp = BitVec.ofNat 64 t8) (start : s.gpr .rbx = BitVec.ofNat 64 (128 - t8))
     (writable : ∀ i < 128, InRegions s.wr (s.gpr .r14 + BitVec.ofNat 64 i) 1)
     (initialPrefix : BytesPrefix s.mem (s.gpr .r14) l 128) :
@@ -48,7 +49,8 @@ theorem descendLoop_ok (s : State) (l : KeyBytes) (t8 : Nat) (ht : 1 ≤ t8) (ht
     rw [loAddr]; exact read₁ _ (by omega)
   have readHi : InRegions (s₁.rd ++ s₁.wr) (s₁.gpr .r14 + (s₁.gpr .rbx - 1#64 + s₁.gpr .rbp)) 1 := by
     rw [hiAddr]; exact read₁ _ (by omega)
-  apply WP.mono (descendKey_ok s₁ readLo readHi write₁)
+  apply WP.mono (descendKey_ok s₁ (by
+    rw [frame₁.wr, frame₁.reg .r8 (by decide)]; exact hlookup) readLo readHi write₁)
   intro s₂ h₂
   let b := Spec.Rc2.pi ((descend l t8 j).getD (127 - t8 - j + 1) 0 ^^^
     (descend l t8 j).getD (127 - t8 - j + t8) 0)

lean/VerifiedGarbage/Proof/Rc2/X86_64/FillKey.lean

@@ -6,7 +6,8 @@ namespace VG.Proof.Rc2.X86_64
 
 open VG VG.X86_64 VG.Impl.Rc2.X86_64
 
-theorem fillLoop_ok (s : State) (key : List Byte) (ht : 1 ≤ key.length) (ht' : key.length < 128)
+theorem fillLoop_ok (s : State)
+    (hlookup : InRegions s.wr (s.gpr .r8 + BitVec.ofNat 64 64) 16) (key : List Byte) (ht : 1 ≤ key.length) (ht' : key.length < 128)
     (len : s.gpr .r13 = BitVec.ofNat 64 key.length) (start : s.gpr .rbx = BitVec.ofNat 64 key.length)
     (writable : ∀ i < 128, InRegions s.wr (s.gpr .r14 + BitVec.ofNat 64 i) 1)
     (initialPrefix : BytesPrefix s.mem (s.gpr .r14) (fill key 0) key.length) :
@@ -45,7 +46,8 @@ theorem fillLoop_ok (s : State) (key : List Byte) (ht : 1 ≤ key.length) (ht' :
     rw [loAddr]; exact read₁ _ (by omega)
   have readHi : InRegions (s₁.rd ++ s₁.wr) (s₁.gpr .r14 + (s₁.gpr .rbx - s₁.gpr .r13)) 1 := by
     rw [hiAddr]; exact read₁ _ (by omega)
-  apply WP.mono (fillKey_ok s₁ readLo readHi write₁)
+  apply WP.mono (fillKey_ok s₁ (by
+    rw [frame₁.wr, frame₁.reg .r8 (by decide)]; exact hlookup) readLo readHi write₁)
   intro s₂ h₂
   let b := Spec.Rc2.pi ((fill key j).getD (key.length + j - 1) 0 + (fill key j).getD j 0)
   have keep₂ : Keep keyTemps {s₁ with

lean/VerifiedGarbage/Proof/Rc2/X86_64/Key.lean

@@ -59,14 +59,18 @@ theorem key_body_correct (s : State) (hs : keyContract.pre s) :
     intro i hi
     rw [wr₂, ptr₂, hwr]
     exact ⟨⟨s.gpr .rcx, 128⟩, by simp, Offset.contains_base _ (by omega) (by omega)⟩
+  have lookup₂ : InRegions s₂.wr (s₂.gpr .r8 + BitVec.ofNat 64 64) 16 := by
+    rw [wr₂, r8₂, hwr]
+    exact ⟨⟨s.gpr .r8, 512⟩, by simp, Offset.contains_base _ (by decide) (by decide)⟩
   apply WP.seq
-  apply WP.mono (expandCopyFill_ok s₂ (s.gpr .rsi).toNat ht ht'
+  apply WP.mono (expandCopyFill_ok s₂ lookup₂ (s.gpr .rsi).toNat ht ht'
     (by simpa using len₂) zero₂ read₂ write₂ (by rw [key₂, ptr₂]; exact keyOut))
   intro s₃ h₃
   apply WP.seq
   have write₃ : ∀ i < 128, InRegions s₃.wr (s₃.gpr .r14 + BitVec.ofNat 64 i) 1 := by
     rw [h₃.1.wr, h₃.1.reg .r14 (by decide)]; exact write₂
-  apply WP.mono (expandReduce_ok s₃ _ (s.gpr .rdx).toNat hb hb'
+  apply WP.mono (expandReduce_ok s₃ (by
+    rw [h₃.1.wr, h₃.1.reg .r8 (by decide)]; exact lookup₂) _ (s.gpr .rdx).toNat hb hb'
     (by simpa using (h₃.1.reg .r15 (by decide)).trans bits₂) write₃
     (by rw [h₃.1.reg .r14 (by decide)]; exact h₃.2))
   intro s₄ h₄