Implement verified Triple DES ECB on AArch64

README.md

@@ -399,7 +399,7 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 <td>❌</td>
 

bench/benches/primitives/triple_des_ecb.rs

@@ -5,7 +5,7 @@ use criterion::Criterion;
 /// The library modules whose code these benchmarks run.
 pub const USES: &[&str] = &["triple_des_ecb", "triple_des"];
 
-#[cfg(target_arch = "x86_64")]
+#[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))]
 pub fn bench(c: &mut Criterion) {
     use std::hint::black_box;
 
@@ -59,5 +59,5 @@ pub fn bench(c: &mut Criterion) {
     }
 }
 
-#[cfg(not(target_arch = "x86_64"))]
+#[cfg(not(any(target_arch = "x86_64", target_arch = "aarch64")))]
 pub fn bench(_: &mut Criterion) {}

lean/VerifiedGarbage/Artifacts/TripleDes/AArch64.lean

@@ -0,0 +1,56 @@
+import VerifiedGarbage.Proof.TripleDes.AArch64.VerifiedBlock
+import VerifiedGarbage.Proof.TripleDes.AArch64.Key.Verified
+import VerifiedGarbage.Proof.TripleDes.AArch64.Ecb.Verified
+
+namespace VG.Artifacts.TripleDes.AArch64
+
+def artifacts : List Artifact := [
+  { Spec.TripleDes.expandKeyApi with
+    target := AArch64.target
+    doc := Spec.TripleDes.expandKeyApi.doc
+      (notes := ["Baseline AArch64 scalar key expansion with fixed permutations and public round-count branches."])
+    code := Impl.TripleDes.AArch64.Key.expandKey
+    contract := Spec.TripleDes.expandKeyContract AArch64.abi
+    stack := 0
+    verified := Proof.TripleDes.AArch64.Key.verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.encryptBlockApi with
+    target := AArch64.target
+    doc := Spec.TripleDes.encryptBlockApi.doc
+      (notes := ["Baseline AArch64 scalar Boolean S-box circuits; IP and FP shared across all three DES passes."])
+    code := Impl.TripleDes.AArch64.encryptBlock
+    contract := Spec.TripleDes.encryptBlockContract AArch64.abi
+    stack := 0
+    verified := Proof.TripleDes.AArch64.encrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.decryptBlockApi with
+    target := AArch64.target
+    doc := Spec.TripleDes.decryptBlockApi.doc
+      (notes := ["Baseline AArch64 scalar Boolean S-box circuits with reverse EDE key order."])
+    code := Impl.TripleDes.AArch64.decryptBlock
+    contract := Spec.TripleDes.decryptBlockContract AArch64.abi
+    stack := 0
+    verified := Proof.TripleDes.AArch64.decrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.ecbEncryptApi with
+    target := AArch64.target
+    doc := Spec.TripleDes.ecbEncryptApi.doc
+      (notes := ["Baseline AArch64, calling the verified Triple DES block primitive for each complete block."])
+    code := Impl.TripleDes.AArch64.Ecb.encrypt
+    contract := Spec.TripleDes.ecbEncryptContract AArch64.abi 0
+    stack := 0
+    ofSig := ⟨_, _, _, by unfold Spec.TripleDes.ecbEncryptContract Spec.TripleDes.ecbContract; rfl⟩
+    verified := Proof.TripleDes.AArch64.Ecb.encrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.TripleDes.ecbDecryptApi with
+    target := AArch64.target
+    doc := Spec.TripleDes.ecbDecryptApi.doc
+      (notes := ["Baseline AArch64, calling the verified Triple DES block primitive for each complete block."])
+    code := Impl.TripleDes.AArch64.Ecb.decrypt
+    contract := Spec.TripleDes.ecbDecryptContract AArch64.abi 0
+    stack := 0
+    ofSig := ⟨_, _, _, by unfold Spec.TripleDes.ecbDecryptContract Spec.TripleDes.ecbContract; rfl⟩
+    verified := Proof.TripleDes.AArch64.Ecb.decrypt_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.TripleDes.AArch64

lean/VerifiedGarbage/Impl/TripleDes/AArch64/Block.lean

@@ -0,0 +1,67 @@
+import VerifiedGarbage.Impl.TripleDes.AArch64.Common
+import VerifiedGarbage.Impl.TripleDes.AArch64.Sbox
+
+namespace VG.Impl.TripleDes.AArch64
+
+open VG.AArch64
+open VG.Spec.TripleDes (Direction)
+
+def savedRegs : List Reg := [.x19, .x20, .x21, .x22]
+
+def blockSave : List Instr := savedRegs.zipIdx.map fun (r, i) => .str .x r .x2 (8 * i)
+def blockRestore : List Instr := savedRegs.zipIdx.map fun (r, i) => .ldr .x r .x2 (8 * i)
+
+def blockLoad : List Instr :=
+  [.ldr .x .x3 .x1 0, .rev .x3 .x3] ++
+    permuteCode Spec.TripleDes.ip 64 .x10 .x3 .x11 .x12 ++
+    [.lsr .x .x19 .x10 32, rr .x20 .x10] ++ mask .x20 32
+
+def sboxInputs (i : Nat) : List Instr :=
+  [.ldr .x .x10 .x22 0, imm .x12 1] ++ (List.range 6).flatMap fun j =>
+    let k := 6 * i + 5 - j
+    [rr (q j) .x20] ++ shr (q j) (32 - Spec.TripleDes.expansion.getD k 1) ++
+      [rr .x11 .x10] ++ shr .x11 (47 - k) ++
+      [.logic .eor .x (q j) (q j) .x11, .logic .and .x (q j) (q j) .x12]
+
+def sboxOutputs (i : Nat) : List Instr :=
+  [imm .x10 1] ++ (List.range 4).flatMap fun j =>
+    let position := 4 * i + 4 - j
+    let dst := (Spec.TripleDes.p.toList.findIdx? (· == position)).getD 0
+    [.logic .and .x (q j) (q j) .x10] ++ placeBit (q j) (31 - dst) ++
+      [.logic .eor .x .x19 .x19 (q j)]
+
+def box (i : Nat) : List Instr := sboxInputs i ++ sboxCode i ++ sboxOutputs i
+
+def swapHalves : List Instr := [rr .x3 .x19, rr .x19 .x20, rr .x20 .x3]
+
+def roundBody : List Instr := (List.range 8).flatMap box ++ swapHalves
+
+def roundAdvance (d : Direction) : List Instr :=
+  [if d = .encrypt then .addImm .x .x22 .x22 8 else .subImm .x .x22 .x22 8,
+    .subImm .x .x21 .x21 1]
+
+def passStart (component : Nat) (d : Direction) : List Instr :=
+  [.addImm .x .x22 .x0 (128 * component + if d = .encrypt then 0 else 120),
+    imm .x21 16]
+
+def pass (component : Nat) (d : Direction) : Prog isa :=
+  .seq (.block (passStart component d))
+    (.seq (.loop (.block (roundBody ++ roundAdvance d)) (.nonzero .x .x21)) (.block swapHalves))
+
+def blockBody (d : Direction) : Prog isa :=
+  match d with
+  | .encrypt => .seq (pass 0 .encrypt) (.seq (pass 1 .decrypt) (pass 2 .encrypt))
+  | .decrypt => .seq (pass 2 .decrypt) (.seq (pass 1 .encrypt) (pass 0 .decrypt))
+
+def blockStore : List Instr :=
+  [.lsl .x .x3 .x19 32, .logic .eor .x .x3 .x3 .x20] ++
+    permuteCode Spec.TripleDes.fp 64 .x10 .x3 .x11 .x12 ++ [.rev .x3 .x10]
+
+def block (d : Direction) : Prog isa :=
+  .seq (.block (blockSave ++ blockLoad))
+    (.seq (blockBody d) (.block (blockStore ++ blockRestore ++ [.str .x .x3 .x1 0])))
+
+def encryptBlock : Prog isa := block .encrypt
+def decryptBlock : Prog isa := block .decrypt
+
+end VG.Impl.TripleDes.AArch64

lean/VerifiedGarbage/Impl/TripleDes/AArch64/Common.lean

@@ -0,0 +1,26 @@
+import VerifiedGarbage.Spec.TripleDes
+import VerifiedGarbage.TCB.AArch64.Isa
+
+namespace VG.Impl.TripleDes.AArch64
+
+open VG.AArch64
+
+def rr (d n : Reg) : Instr := .addImm .x d n 0
+
+def imm (r : Reg) (n : Nat) : Instr := .movz .x r (BitVec.ofNat 16 n) 0
+
+def shr (r : Reg) (n : Nat) : List Instr := if n = 0 then [] else [.lsr .x r r n]
+
+def placeBit (r : Reg) (n : Nat) : List Instr := if n = 0 then [] else [.ror .x r r (64 - n)]
+
+/-- Keep exactly the low `n` bits with two fixed shifts. -/
+def mask (r : Reg) (n : Nat) : List Instr :=
+  [.lsl .x r r (64 - n), .lsr .x r r (64 - n)]
+
+def permuteCode {m : Nat} (positions : Vector Nat m) (n : Nat) (dst src tmp bit : Reg) : List Instr :=
+  [imm dst 0, imm bit 1] ++ (List.range m).flatMap fun j =>
+    [rr tmp src] ++ shr tmp (n - positions.getD j 1) ++
+      [.logic .and .x tmp tmp bit] ++ placeBit tmp (m - 1 - j) ++
+      [.logic .eor .x dst dst tmp]
+
+end VG.Impl.TripleDes.AArch64

lean/VerifiedGarbage/Impl/TripleDes/AArch64/Ecb.lean

@@ -0,0 +1,27 @@
+import VerifiedGarbage.Impl.TripleDes.AArch64.Block
+
+namespace VG.Impl.TripleDes.AArch64.Ecb
+
+open VG.AArch64 VG.Impl.TripleDes.AArch64
+open VG.Spec.TripleDes (Direction)
+
+def save : List Instr := [.str .x .x23 .x3 512, .str .x .x30 .x3 520]
+def setup : List Instr := [rr .x23 .x2, rr .x2 .x3]
+def restore : List Instr := [.ldr .x .x23 .x2 512, .ldr .x .x30 .x2 520]
+
+def blockCall (d : Direction) : Prog isa :=
+  match d with
+  | .encrypt => .call "vg_triple_des_encrypt_block" encryptBlock
+  | .decrypt => .call "vg_triple_des_decrypt_block" decryptBlock
+
+def advance : List Instr := [.addImm .x .x1 .x1 8, .subImm .x .x23 .x23 1]
+
+def ecb (d : Direction) : Prog isa :=
+  .seq (.block (save ++ setup))
+    (.seq (.ite (.zero .x .x23) (.block [])
+      (.loop (.seq (blockCall d) (.block advance)) (.nonzero .x .x23))) (.block restore))
+
+def encrypt : Prog isa := ecb .encrypt
+def decrypt : Prog isa := ecb .decrypt
+
+end VG.Impl.TripleDes.AArch64.Ecb

lean/VerifiedGarbage/Impl/TripleDes/AArch64/ExpandKey.lean

@@ -0,0 +1,50 @@
+import VerifiedGarbage.Impl.TripleDes.AArch64.Common
+
+namespace VG.Impl.TripleDes.AArch64.Key
+
+open VG.AArch64 VG.Impl.TripleDes.AArch64
+
+def savedRegs : List Reg := [.x19, .x20, .x21, .x22]
+
+def save : List Instr := savedRegs.zipIdx.map fun (r, i) => .str .x r .x3 (8 * i)
+def restore : List Instr := savedRegs.zipIdx.map fun (r, i) => .ldr .x r .x3 (8 * i)
+
+def load (offset component : Nat) : List Instr :=
+  [.ldr .x .x4 .x0 offset, .rev .x4 .x4] ++
+    permuteCode Spec.TripleDes.pc1 64 .x5 .x4 .x6 .x7 ++
+    [.lsr .x .x19 .x5 28, rr .x20 .x5] ++ mask .x20 28 ++
+    [imm .x21 0, .addImm .x .x22 .x2 (128 * component)]
+
+def rotate28 (r : Reg) (n : Nat) : List Instr :=
+  [.lsr .x .x4 r (28 - n), .ror .x r r (64 - n), .logic .eor .x r r .x4] ++ mask r 28
+
+def rotate (n : Nat) : Prog isa := .block (rotate28 .x19 n ++ rotate28 .x20 n)
+
+def rotation : Prog isa :=
+  .seq (.block [.lsr .x .x4 .x21 1])
+    (.ite (.zero .x .x4) (rotate 1)
+      (.seq (.block [.subImm .x .x4 .x21 8])
+        (.ite (.zero .x .x4) (rotate 1)
+          (.seq (.block [.subImm .x .x4 .x21 15])
+            (.ite (.zero .x .x4) (rotate 1) (rotate 2))))))
+
+def storeRound : List Instr :=
+  [.lsl .x .x4 .x19 28, .logic .eor .x .x4 .x4 .x20] ++
+    permuteCode Spec.TripleDes.pc2 56 .x5 .x4 .x6 .x7 ++
+    [.str .x .x5 .x22 0, .addImm .x .x22 .x22 8, .addImm .x .x21 .x21 1,
+      .subImm .x .x4 .x21 16]
+
+def component (offset index : Nat) : Prog isa :=
+  .seq (.block (load offset index)) (.loop (.seq rotation (.block storeRound)) (.nonzero .x .x4))
+
+def copyThird : List Instr :=
+  (List.range 16).flatMap fun j => [.ldr .x .x4 .x2 (8 * j), .str .x .x4 .x2 (256 + 8 * j)]
+
+def expandKey : Prog isa :=
+  .seq (.block save)
+    (.seq (component 0 0)
+      (.seq (component 8 1)
+        (.seq (.block [.subImm .x .x4 .x1 16])
+          (.seq (.ite (.zero .x .x4) (.block copyThird) (component 16 2)) (.block restore)))))
+
+end VG.Impl.TripleDes.AArch64.Key

lean/VerifiedGarbage/Impl/TripleDes/AArch64/Permutation.lean

@@ -0,0 +1,12 @@
+import VerifiedGarbage.Impl.TripleDes.AArch64.Common
+
+namespace VG.Impl.TripleDes.AArch64
+
+open VG.AArch64
+
+def initialPermutation : Prog isa := .block (permuteCode Spec.TripleDes.ip 64 .x10 .x3 .x11 .x12)
+def finalPermutation : Prog isa := .block (permuteCode Spec.TripleDes.fp 64 .x10 .x3 .x11 .x12)
+def keyPermutation1 : Prog isa := .block (permuteCode Spec.TripleDes.pc1 64 .x5 .x4 .x6 .x7)
+def keyPermutation2 : Prog isa := .block (permuteCode Spec.TripleDes.pc2 56 .x5 .x4 .x6 .x7)
+
+end VG.Impl.TripleDes.AArch64

lean/VerifiedGarbage/Impl/TripleDes/AArch64/Sbox.lean

@@ -0,0 +1,30 @@
+import VerifiedGarbage.Impl.TripleDes.Circuit
+import VerifiedGarbage.Impl.Aes.AArch64.Alloc
+
+namespace VG.Impl.TripleDes.AArch64
+
+open VG.AArch64
+
+def q : Nat → Reg
+  | 0 => .x3 | 1 => .x4 | 2 => .x5 | 3 => .x6 | 4 => .x7 | _ => .x8
+
+def sboxIns : List (Nat × Reg) := (List.range 6).map fun i => (i, q i)
+
+def sboxOuts (i : Nat) : List (Nat × Reg) :=
+  (List.range 4).map fun j => ((Circuit.outputs i).getD j 0, q j)
+
+/-- Six input planes and eight temporary registers; scratch slots 0–3 are reserved. -/
+def sboxCode (i : Nat) : List Instr :=
+  VG.Impl.Aes.AArch64.compile .x2 (Circuit.gates i) sboxIns (sboxOuts i)
+    [.x10, .x11, .x12, .x13, .x14, .x15, .x16, .x17] .x9 (List.range' 4 48)
+
+def sbox0 : Prog isa := .block (sboxCode 0)
+def sbox1 : Prog isa := .block (sboxCode 1)
+def sbox2 : Prog isa := .block (sboxCode 2)
+def sbox3 : Prog isa := .block (sboxCode 3)
+def sbox4 : Prog isa := .block (sboxCode 4)
+def sbox5 : Prog isa := .block (sboxCode 5)
+def sbox6 : Prog isa := .block (sboxCode 6)
+def sbox7 : Prog isa := .block (sboxCode 7)
+
+end VG.Impl.TripleDes.AArch64

lean/VerifiedGarbage/Proof/TripleDes/AArch64/Block.lean

@@ -0,0 +1,85 @@
+import VerifiedGarbage.Proof.TripleDes.AArch64.Head
+import VerifiedGarbage.Proof.TripleDes.AArch64.Tail
+
+namespace VG.Proof.TripleDes.AArch64
+
+open VG VG.AArch64 VG.Impl.TripleDes.AArch64
+open VG.Spec.TripleDes (Direction Schedule)
+
+def blockResult (keys : Schedule) (direction : Direction) (b : Spec.TripleDes.Block) :
+    Spec.TripleDes.Block :=
+  match direction with
+  | .encrypt => Spec.TripleDes.encryptBlock keys b
+  | .decrypt => Spec.TripleDes.decryptBlock keys b
+
+theorem blockResult_core (keys : Schedule) (direction : Direction) (b : Spec.TripleDes.Block) :
+    Spec.TripleDes.encodeBlock (Spec.TripleDes.permute Spec.TripleDes.fp
+      (blockCore (Spec.TripleDes.componentSchedule keys) direction
+        (Spec.TripleDes.permute Spec.TripleDes.ip (Spec.TripleDes.decodeBlock b)))) =
+      blockResult keys direction b := by
+  cases direction
+  · exact (VG.Proof.TripleDes.encryptBlock_eq_cores keys b).symm
+  · exact (VG.Proof.TripleDes.decryptBlock_eq_cores keys b).symm
+
+def blockRegions (s : State) : List Region := [⟨s.gpr .x1, 8⟩, ⟨s.gpr .x2, 512⟩]
+
+structure BlockPost (keys : Schedule) (direction : Direction) (original s : State) : Prop where
+  result : Spec.TripleDes.blockAt s.mem (original.gpr .x1) =
+    blockResult keys direction (Spec.TripleDes.blockAt original.mem (original.gpr .x1))
+  saved : ∀ r ∈ savedRegs, s.gpr r = original.gpr r
+  rd : s.rd = original.rd
+  wr : s.wr = original.wr
+  sp : s.sp = original.sp
+  regs : ∀ q ∈ roundStepKept, s.gpr q = original.gpr q
+  frame : Frame (blockRegions original) original.mem s.mem
+
+theorem block_ok (keys : Schedule) (base : Addr) (direction : Direction) (s : State)
+    (hp : HeadPre (Spec.TripleDes.componentSchedule keys) base s)
+    (hwrite : InRegions s.wr (s.gpr .x1) 8) :
+    WP isa (block direction) s (BlockPost keys direction s) := by
+  apply WP.seq
+  apply WP.mono (blockHead_ok (Spec.TripleDes.componentSchedule keys) base s hp)
+  intro s₁ hs₁
+  apply WP.seq
+  apply WP.mono (blockBody_ok (Spec.TripleDes.componentSchedule keys) base s₁ _ direction hs₁.ready hs₁.word)
+  intro s₂ hs₂
+  have hregs₂ : ∀ q ∈ roundStepKept, s₂.gpr q = s.gpr q := by
+    intro q hq
+    have hkeep : ∀ r ∈ roundStepKept, r ∈ loadKept := by decide
+    exact (hs₂.2.2.regs q hq).trans (hs₁.regs q (hkeep q hq))
+  have saved₂ := hs₁.saved.congr (hs₂.2.2.regs .x2 (by decide)) hs₂.2.2.frame
+  have savedRead₂ : ∀ i < 4, InRegions (s₂.rd ++ s₂.wr) (s₂.gpr .x2 + BitVec.ofNat 64 (8 * i)) 8 := by
+    rw [hs₂.2.2.rd, hs₂.2.2.wr, hs₁.rd, hs₁.wr, hregs₂ .x2 (by decide)]
+    exact hp.saveRead
+  have hwrite₂ : InRegions s₂.wr (s₂.gpr .x1) 8 := by
+    rw [hs₂.2.2.wr, hs₁.wr, hregs₂ .x1 (by decide)]
+    exact hwrite
+  apply WP.mono (blockTail_ok s s₂ _ hs₂.1 saved₂ savedRead₂ hwrite₂)
+  intro s₃ hs₃
+  refine ⟨?_, hs₃.saved, hs₃.rd.trans (hs₂.2.2.rd.trans hs₁.rd),
+    hs₃.wr.trans (hs₂.2.2.wr.trans hs₁.wr),
+    hs₃.sp.trans (hs₂.2.2.sp.trans hs₁.sp),
+    fun q hq => (hs₃.regs q hq).trans (hregs₂ q hq), ?_⟩
+  · have hresult := hs₃.result
+    rw [hregs₂ .x1 (by decide)] at hresult
+    exact hresult.trans (blockResult_core keys direction _)
+  · have hf₁ : Frame (blockRegions s) s.mem s₁.mem := hs₁.frame.sub (by
+      intro r hr
+      obtain rfl := List.mem_singleton.mp hr
+      exact ⟨⟨s.gpr .x2, 512⟩, by simp [blockRegions], Region.sub_prefix (by decide)⟩)
+    have hf₂ : Frame (blockRegions s) s₁.mem s₂.mem := hs₂.2.2.frame.sub (by
+      intro r hr
+      obtain rfl := List.mem_singleton.mp hr
+      refine ⟨⟨s.gpr .x2, 512⟩, by simp [blockRegions], ?_⟩
+      have hbase := hs₁.regs .x2 (by decide)
+      change Region.Sub ⟨s₁.gpr .x2 + BitVec.ofNat 64 32, 384⟩ ⟨s.gpr .x2, 512⟩
+      rw [hbase]
+      exact Offset.sub_base _ (by decide))
+    have hf₃ : Frame (blockRegions s) s₂.mem s₃.mem := hs₃.frame.sub (by
+      intro r hr
+      obtain rfl := List.mem_singleton.mp hr
+      rw [hregs₂ .x1 (by decide)]
+      exact ⟨⟨s.gpr .x1, 8⟩, by simp [blockRegions], fun _ h => h⟩)
+    exact hf₁.trans (hf₂.trans hf₃)
+
+end VG.Proof.TripleDes.AArch64