Implement AES-CMAC on ARMv7

README.md

@@ -219,7 +219,7 @@ yours to keep:
 
 <td>✅ AES, PMULL</td>
 
-<td>❌</td>
+<td>✅</td>
 
 <td>❌</td>
 

bench/benches/primitives/cmac_aes.rs

@@ -8,7 +8,7 @@ pub const USES: &[&str] = &["cmac_aes", "aes"];
 
 /// The MAC of a message with a 16-byte key (setup included), computed and
 /// verified.
-#[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))]
+#[cfg(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm"))]
 pub fn bench(c: &mut Criterion) {
     use std::hint::black_box;
 
@@ -63,5 +63,5 @@ pub fn bench(c: &mut Criterion) {
     g.finish();
 }
 
-#[cfg(not(any(target_arch = "x86_64", target_arch = "aarch64")))]
+#[cfg(not(any(target_arch = "x86_64", target_arch = "aarch64", target_arch = "arm")))]
 pub fn bench(_: &mut Criterion) {}

lean/VerifiedGarbage/Artifacts/CmacAes/Arm.lean

@@ -0,0 +1,53 @@
+import VerifiedGarbage.TCB.Arm.Target
+import VerifiedGarbage.Proof.CmacAes.Arm.Verified
+
+/-!
+# AES-CMAC (NIST SP 800-38B) on ARMv7
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+
+Each function calls `vg_aes_ctr32` in a frame that pushes its two stack
+arguments, so uses 8 bytes of stack.
+-/
+
+namespace VG.Artifacts.CmacAes.Arm
+
+open VG.Proof.CmacAes.Arm
+
+/-- How the functions encrypt a block. -/
+def ctrNote : String := "This implementation encrypts each block with `vg_aes_ctr32`."
+
+def artifacts : List Artifact := [
+  { Spec.Cmac.aesSubkeysApi with
+    target := Arm.target
+    doc := Spec.Cmac.aesSubkeysApi.doc (notes := [ctrNote])
+    code := Impl.CmacAes.Arm.subkeys
+    contract := Spec.Cmac.aesSubkeysContract Arm.abi 8
+    stack := 8
+    verified := subkeys_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Cmac.aesUpdateApi with
+    target := Arm.target
+    doc := Spec.Cmac.aesUpdateApi.doc (notes := [ctrNote])
+    code := Impl.CmacAes.Arm.update
+    contract := Spec.Cmac.aesUpdateContract Arm.abi 8
+    stack := 8
+    verified := update_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Cmac.aesFinalizeApi with
+    target := Arm.target
+    doc := Spec.Cmac.aesFinalizeApi.doc (notes := [ctrNote])
+    code := Impl.CmacAes.Arm.finalize
+    contract := Spec.Cmac.aesFinalizeContract Arm.abi 8
+    stack := 8
+    verified := finalize_verified
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.CmacAes.Arm

lean/VerifiedGarbage/Impl/CmacAes/Arm.lean

@@ -0,0 +1,183 @@
+import VerifiedGarbage.Impl.Aes.Arm.Ctr32
+
+/-!
+# AES-CMAC: 32-bit ARM implementation
+
+`vg_cmac_aes_subkeys(schedule = r0, rounds = r1, subkeys = r2, scratch = r3)`,
+`vg_cmac_aes_update(schedule = r0, rounds = r1, state = r2, data = r3, n = [sp], scratch = [sp + 4])`
+and `vg_cmac_aes_finalize(key = r0, rounds = r1, state = r2, last = r3, last_len = [sp], scratch = [sp + 4])`
+(see `VG.Spec.Cmac.aesSubkeysContract` and the others), composed of calls of
+the verified `vg_aes_ctr32`, one block at a time: with a counter block `X`
+and a zero data block, it leaves `CIPH_K(X)` in the data block.
+
+`vg_aes_ctr32(schedule, rounds, counter, data, n, scratch)` takes `n` and
+`scratch` on the stack: a frame pushes them (`push {rA, rB}`, `n = 1` in
+`rA` at `[sp]`) around each call, and its pop loads `rA` back. So the
+functions use 8 bytes of stack.
+
+The scratch buffer (2176 bytes): `[0, 2048)` is the working space of
+`vg_aes_ctr32`, `[2048, 2064)` the counter block, and `[2064, 2096)` our
+caller's callee-saved registers and our return address `lr`.
+
+* `subkeys` computes `L = CIPH_K(0)` into the first block of `subkeys`, and
+  doubles it there (`K1`) and into the second block (`K2`): the block as a
+  big-endian 128-bit integer in `r0:r1:r2:r3`, shifted left by one bit, and
+  XORed with `0x87` masked by the bit shifted out. `r6` holds `subkeys` and
+  `r5` the scratch buffer across the call.
+* `update` keeps its arguments in `r4` (schedule), `r5` (rounds), `r6`
+  (state), `r7` (data), `r8` (blocks left) and `r10` (scratch) across the
+  calls; each block, the counter block is `C ⊕ Mᵢ` and the state, zeroed,
+  receives `CIPH_K(C ⊕ Mᵢ)`.
+* `finalize` forms `Mₙ` in the counter block: `Mₙ* ⊕ K1` for a complete
+  block, else `Mₙ*` copied a byte at a time onto zeros, `0x80` after it, and
+  XORed with `K2`. It XORs in the chaining value and calls `vg_aes_ctr32`
+  last, keeping only the scratch buffer (in `r5`) across the call.
+
+The model has no register-offset addressing: the last bytes are copied
+through advancing pointers, counting down with `subs`. Only the pointers,
+`rounds`, `n` and `last_len` can affect timing: the branches are on `n` and
+`last_len`, and the doubling is masked.
+-/
+
+namespace VG.Impl.CmacAes.Arm
+
+open VG.Arm
+
+/-- `mov d, n`. -/
+def mov (d n : Reg) : Instr := .mov d (.reg n)
+
+/-- The offset of the counter block in the scratch buffer. -/
+def cOff : Nat := 2048
+
+/-- The call of `vg_aes_ctr32`, with `n` (1) in `ra` and the scratch buffer in
+`rb` pushed as its stack arguments, and `ra` popped. -/
+def ctrCall (ra rb : Reg) : Prog isa :=
+  .frame (.push [ra, rb]) (.call "vg_aes_ctr32" Impl.Aes.Arm.ctr32) (.pop ra 8)
+
+/-! ## `vg_cmac_aes_subkeys` -/
+
+/-- Saves `r4`–`r6` and `lr`, keeps `subkeys` in `r6` and the scratch buffer
+in `r5`, zeroes the counter block and the first block of `subkeys`, and sets
+up the arguments of `vg_aes_ctr32`. -/
+def subkeysPre : List Instr :=
+  [.str .r4 .r3 2064, .str .r5 .r3 2068, .str .r6 .r3 2072, .str .lr .r3 2076, mov .r6 .r2, mov .r5 .r3,
+   .mov .r12 (.imm 0), .str .r12 .r3 cOff, .str .r12 .r3 (cOff + 4), .str .r12 .r3 (cOff + 8),
+   .str .r12 .r3 (cOff + 12), .str .r12 .r2 0, .str .r12 .r2 4, .str .r12 .r2 8, .str .r12 .r2 12,
+   .dp .add .r2 .r5 (.imm (BitVec.ofNat 32 cOff)), mov .r3 .r6, .mov .r4 (.imm 1)]
+
+/-- The block at `r6 + src`, doubled (`VG.Spec.Cmac.dbl 16`), to `r6 + dst`. -/
+def dbl (src dst : Nat) : List Instr :=
+  [.ldr .r0 .r6 src, .ldr .r1 .r6 (src + 4), .ldr .r2 .r6 (src + 8), .ldr .r3 .r6 (src + 12),
+   .rev .r0 .r0, .rev .r1 .r1, .rev .r2 .r2, .rev .r3 .r3,
+   .mov .r12 (.shifted .r0 .lsr 31), .mov .r4 (.imm 0), .dp .sub .r12 .r4 (.reg .r12),
+   .dp .and .r12 .r12 (.imm 0x87),
+   .mov .r0 (.shifted .r0 .lsl 1), .dp .orr .r0 .r0 (.shifted .r1 .lsr 31),
+   .mov .r1 (.shifted .r1 .lsl 1), .dp .orr .r1 .r1 (.shifted .r2 .lsr 31),
+   .mov .r2 (.shifted .r2 .lsl 1), .dp .orr .r2 .r2 (.shifted .r3 .lsr 31),
+   .mov .r3 (.shifted .r3 .lsl 1), .dp .eor .r3 .r3 (.reg .r12),
+   .rev .r0 .r0, .rev .r1 .r1, .rev .r2 .r2, .rev .r3 .r3,
+   .str .r0 .r6 dst, .str .r1 .r6 (dst + 4), .str .r2 .r6 (dst + 8), .str .r3 .r6 (dst + 12)]
+
+/-- `K1` over `L`, `K2` after it, and the saved registers restored. -/
+def subkeysPost : List Instr :=
+  dbl 0 0 ++ dbl 0 16 ++
+    [.ldr .r4 .r5 2064, .ldr .r6 .r5 2072, .ldr .lr .r5 2076, .ldr .r5 .r5 2068]
+
+def subkeys : Prog isa :=
+  .seq (.block subkeysPre) (.seq (ctrCall .r4 .r5) (.block subkeysPost))
+
+/-! ## `vg_cmac_aes_update` -/
+
+/-- The registers saved in the scratch buffer, and where (`r10`, the base of
+the restore, last). -/
+def saved : List (Reg × Nat) :=
+  [(.r4, 2064), (.r5, 2068), (.r6, 2072), (.r7, 2076), (.r8, 2080), (.r9, 2084), (.lr, 2092),
+   (.r10, 2088)]
+
+/-- Saves them, with the scratch buffer (the second stack argument) in `r12`. -/
+def save : List Instr := .ldrSp .r12 4 :: saved.map fun (r, d) => .str r .r12 d
+
+/-- Restores them, with `r10` (restored last) the scratch buffer. -/
+def restore : List Instr := saved.map fun (r, d) => .ldr r .r10 d
+
+/-- The arguments to their registers; Z is set if there are no blocks. -/
+def setup : List Instr :=
+  [mov .r4 .r0, mov .r5 .r1, mov .r6 .r2, mov .r7 .r3, .ldrSp .r8 0, mov .r10 .r12, .cmp .r8 (.imm 0)]
+
+/-- The counter block `C ⊕ Mᵢ` (the state at `r6`, the block at `r7`), and
+the state zeroed. -/
+def chainIn : List Instr :=
+  [.ldr .r0 .r6 0, .ldr .r1 .r7 0, .dp .eor .r0 .r0 (.reg .r1), .str .r0 .r10 cOff,
+   .ldr .r0 .r6 4, .ldr .r1 .r7 4, .dp .eor .r0 .r0 (.reg .r1), .str .r0 .r10 (cOff + 4),
+   .ldr .r0 .r6 8, .ldr .r1 .r7 8, .dp .eor .r0 .r0 (.reg .r1), .str .r0 .r10 (cOff + 8),
+   .ldr .r0 .r6 12, .ldr .r1 .r7 12, .dp .eor .r0 .r0 (.reg .r1), .str .r0 .r10 (cOff + 12),
+   .mov .r0 (.imm 0), .str .r0 .r6 0, .str .r0 .r6 4, .str .r0 .r6 8, .str .r0 .r6 12]
+
+/-- The arguments of `vg_aes_ctr32` for the block. -/
+def updArgs : List Instr :=
+  [mov .r0 .r4, mov .r1 .r5, .dp .add .r2 .r10 (.imm (BitVec.ofNat 32 cOff)), mov .r3 .r6, .mov .r9 (.imm 1)]
+
+/-- On to the next block (Z is set when none are left). -/
+def advance : List Instr := [.dp .add .r7 .r7 (.imm 16), .subs .r8 .r8 (.imm 1)]
+
+/-- One block. -/
+def body : Prog isa :=
+  .seq (.block (chainIn ++ updArgs)) (.seq (ctrCall .r9 .r10) (.block advance))
+
+def update : Prog isa :=
+  .seq (.block (save ++ setup)) (.seq (.ite .eq (.block []) (.loop body .ne)) (.block restore))
+
+/-! ## `vg_cmac_aes_finalize` -/
+
+/-- The four words at `pb + pd` and `qb + qd` XORed into `cb + cd`, with
+`r12` and `lr`. -/
+def xor4 (pb qb cb : Reg) (pd qd cd : Nat) : List Instr :=
+  (List.range 4).flatMap fun i =>
+    [.ldr .r12 pb (pd + 4 * i), .ldr .lr qb (qd + 4 * i), .dp .eor .r12 .r12 (.reg .lr),
+     .str .r12 cb (cd + 4 * i)]
+
+/-- Saves `r4`, `r5` and `lr`, keeps the scratch buffer in `r5` and `last_len`
+in `r4`; Z is set if `last_len` is 16. -/
+def finSave : List Instr :=
+  [.ldrSp .r12 4, .str .r4 .r12 2064, .str .r5 .r12 2068, .str .lr .r12 2072, mov .r5 .r12,
+   .ldrSp .r4 0, .cmp .r4 (.imm 16)]
+
+/-- `Mₙ = Mₙ* ⊕ K1` (`K1` at `r0 + 240`), for a complete last block. -/
+def full : List Instr := xor4 .r3 .r0 .r5 0 240 cOff
+
+/-- The counter block zeroed, with `lr` pointing at it; Z is set if
+`last_len` is 0. -/
+def zero : List Instr :=
+  [.mov .r12 (.imm 0), .str .r12 .r5 cOff, .str .r12 .r5 (cOff + 4), .str .r12 .r5 (cOff + 8),
+   .str .r12 .r5 (cOff + 12), .dp .add .lr .r5 (.imm (BitVec.ofNat 32 cOff)), .cmp .r4 (.imm 0)]
+
+/-- The `r4` (nonzero) bytes at `r3` copied to `lr`, advancing both. -/
+def copy : Prog isa :=
+  .loop (.block [.ldrb .r12 .r3 0, .strb .r12 .lr 0, .dp .add .r3 .r3 (.imm 1),
+    .dp .add .lr .lr (.imm 1), .subs .r4 .r4 (.imm 1)]) .ne
+
+/-- `0x80` after the bytes (at `lr`), and the block XORed with `K2` (at
+`r0 + 256`). -/
+def padK2 : List Instr :=
+  [.mov .r12 (.imm 0x80), .strb .r12 .lr 0] ++ xor4 .r5 .r0 .r5 cOff 256 cOff
+
+/-- `Mₙ = K2 ⊕ (Mₙ* ‖ 10ʲ)`, for a partial last block (`last_len < 16`). -/
+def partialBlock : Prog isa :=
+  .seq (.block zero) (.seq (.ite .eq (.block []) copy) (.block padK2))
+
+/-- The counter block `C ⊕ Mₙ` (the state at `r2`), the state zeroed, and the
+arguments of `vg_aes_ctr32` but the schedule (`r0`) and the rounds (`r1`),
+which are ours. -/
+def finArgs : List Instr :=
+  xor4 .r5 .r2 .r5 cOff 0 cOff ++
+    [.mov .r12 (.imm 0), .str .r12 .r2 0, .str .r12 .r2 4, .str .r12 .r2 8, .str .r12 .r2 12,
+     mov .r3 .r2, .dp .add .r2 .r5 (.imm (BitVec.ofNat 32 cOff)), .mov .r4 (.imm 1)]
+
+/-- Everything before the call. -/
+def finPre : Prog isa :=
+  .seq (.block finSave) (.seq (.ite .eq (.block full) partialBlock) (.block finArgs))
+
+def finalize : Prog isa :=
+  .seq finPre (.seq (ctrCall .r4 .r5) (.block [.ldr .r4 .r5 2064, .ldr .lr .r5 2072, .ldr .r5 .r5 2068]))
+
+end VG.Impl.CmacAes.Arm

lean/VerifiedGarbage/Proof/Cmac/Block32.lean

@@ -0,0 +1,104 @@
+import VerifiedGarbage.Proof.Cmac.Mem32
+import VerifiedGarbage.Proof.Cmac.Block
+
+/-!
+# CMAC: blocks formed a 32-bit word at a time
+
+Untrusted: everything here is checked by Lean. What the 32-bit targets'
+stores leave: the XOR of two blocks stored a word at a time (`xor4Mem`; the
+block written may be one of those read, as long as no word written is read
+afterwards, `Sep4`), a zeroed block (`zero4`), and a counter block `C = P ⊕ Q`
+with `P` zeroed (`chainMem4`).
+-/
+
+namespace VG.Proof.Cmac
+
+open VG
+
+/-- No word written at `c` is read at `p` after it: the word `i` written is
+disjoint from every word `j > i` of `p`. -/
+def Sep4 (c p : Addr) : Prop :=
+  ∀ i < 4, ∀ j < 4, i < j → (⟨c + BitVec.ofNat 64 (4 * i), 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 (4 * j), 4⟩
+
+theorem Sep4.self (c : Addr) : Sep4 c c := fun i hi j hj hij =>
+  Offset.disjoint c (by omega) (by omega) (by omega)
+
+theorem Sep4.of_disjoint {c p : Addr} (h : (⟨c, 16⟩ : Region).Disjoint ⟨p, 16⟩) : Sep4 c p :=
+  fun i hi j hj _ => (h.sub_left (Offset.sub_base c (by omega))).sub_right (Offset.sub_base p (by omega))
+
+theorem readW_writeW_disj {m : Mem} {a b : Addr} (v : BitVec 32) (h : (⟨a, 4⟩ : Region).Disjoint ⟨b, 4⟩) :
+    (m.writeW a v).readW b 32 = m.readW b 32 :=
+  Mem.readW_writeW_sep (h.symm.sep (Region.contains_self _ _) (Region.contains_self _ _)) (by decide)
+
+/-- The memory after storing at `c` the XOR of the blocks at `p` and `q`, a
+word at a time. -/
+def xor4Mem (m : Mem) (c p q : Addr) : Mem :=
+  let m₁ := m.writeW c (m.readW p 32 ^^^ m.readW q 32)
+  let m₂ := m₁.writeW (c + BitVec.ofNat 64 4)
+    (m₁.readW (p + BitVec.ofNat 64 4) 32 ^^^ m₁.readW (q + BitVec.ofNat 64 4) 32)
+  let m₃ := m₂.writeW (c + BitVec.ofNat 64 8)
+    (m₂.readW (p + BitVec.ofNat 64 8) 32 ^^^ m₂.readW (q + BitVec.ofNat 64 8) 32)
+  m₃.writeW (c + BitVec.ofNat 64 12) (m₃.readW (p + BitVec.ofNat 64 12) 32 ^^^ m₃.readW (q + BitVec.ofNat 64 12) 32)
+
+theorem xor4Mem_eq (m : Mem) {c p q : Addr} (hp : Sep4 c p) (hq : Sep4 c q) :
+    xor4Mem m c p q = store4 m c (m.readW p 32 ^^^ m.readW q 32)
+      (m.readW (p + BitVec.ofNat 64 4) 32 ^^^ m.readW (q + BitVec.ofNat 64 4) 32)
+      (m.readW (p + BitVec.ofNat 64 8) 32 ^^^ m.readW (q + BitVec.ofNat 64 8) 32)
+      (m.readW (p + BitVec.ofNat 64 12) 32 ^^^ m.readW (q + BitVec.ofNat 64 12) 32) := by
+  have e (x : Addr) (h : Sep4 c x) (i j : Nat) (hi : i < 4) (hj : j < 4) (hij : i < j) :
+      (⟨c + BitVec.ofNat 64 (4 * i), 4⟩ : Region).Disjoint ⟨x + BitVec.ofNat 64 (4 * j), 4⟩ := h i hi j hj hij
+  have p01 : (⟨c, 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 4, 4⟩ := by simpa using e p hp 0 1 (by decide) (by decide) (by decide)
+  have q01 : (⟨c, 4⟩ : Region).Disjoint ⟨q + BitVec.ofNat 64 4, 4⟩ := by simpa using e q hq 0 1 (by decide) (by decide) (by decide)
+  have p02 : (⟨c, 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 8, 4⟩ := by simpa using e p hp 0 2 (by decide) (by decide) (by decide)
+  have q02 : (⟨c, 4⟩ : Region).Disjoint ⟨q + BitVec.ofNat 64 8, 4⟩ := by simpa using e q hq 0 2 (by decide) (by decide) (by decide)
+  have p03 : (⟨c, 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 12, 4⟩ := by simpa using e p hp 0 3 (by decide) (by decide) (by decide)
+  have q03 : (⟨c, 4⟩ : Region).Disjoint ⟨q + BitVec.ofNat 64 12, 4⟩ := by simpa using e q hq 0 3 (by decide) (by decide) (by decide)
+  have p12 : (⟨c + BitVec.ofNat 64 4, 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 8, 4⟩ := e p hp 1 2 (by decide) (by decide) (by decide)
+  have q12 : (⟨c + BitVec.ofNat 64 4, 4⟩ : Region).Disjoint ⟨q + BitVec.ofNat 64 8, 4⟩ := e q hq 1 2 (by decide) (by decide) (by decide)
+  have p13 : (⟨c + BitVec.ofNat 64 4, 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 12, 4⟩ := e p hp 1 3 (by decide) (by decide) (by decide)
+  have q13 : (⟨c + BitVec.ofNat 64 4, 4⟩ : Region).Disjoint ⟨q + BitVec.ofNat 64 12, 4⟩ := e q hq 1 3 (by decide) (by decide) (by decide)
+  have p23 : (⟨c + BitVec.ofNat 64 8, 4⟩ : Region).Disjoint ⟨p + BitVec.ofNat 64 12, 4⟩ := e p hp 2 3 (by decide) (by decide) (by decide)
+  have q23 : (⟨c + BitVec.ofNat 64 8, 4⟩ : Region).Disjoint ⟨q + BitVec.ofNat 64 12, 4⟩ := e q hq 2 3 (by decide) (by decide) (by decide)
+  simp only [xor4Mem, store4, readW_writeW_disj _ p01, readW_writeW_disj _ q01, readW_writeW_disj _ p02,
+    readW_writeW_disj _ q02, readW_writeW_disj _ p03, readW_writeW_disj _ q03, readW_writeW_disj _ p12,
+    readW_writeW_disj _ q12, readW_writeW_disj _ p13, readW_writeW_disj _ q13, readW_writeW_disj _ p23,
+    readW_writeW_disj _ q23]
+
+theorem xor4Mem_frame (m : Mem) (c p q : Addr) : Frame [⟨c, 16⟩] m (xor4Mem m c p q) := by
+  have k (d : Nat) (h : d + 4 ≤ 16) : (⟨c, 16⟩ : Region).Contains (c + BitVec.ofNat 64 d) 4 :=
+    Offset.contains_base c h (by omega)
+  have k0 : (⟨c, 16⟩ : Region).Contains c 4 := by simpa using k 0 (by decide)
+  exact ((((Frame.refl _ _).writeW (List.mem_singleton_self _) _ k0).writeW (List.mem_singleton_self _) _
+    (k 4 (by decide))).writeW (List.mem_singleton_self _) _ (k 8 (by decide))).writeW
+    (List.mem_singleton_self _) _ (k 12 (by decide))
+
+theorem xor4Mem_bytes (m : Mem) {c p q : Addr} (hp : Sep4 c p) (hq : Sep4 c q) :
+    Spec.Aes.bytesAt (xor4Mem m c p q) c 16 =
+      Spec.Cmac.xor (Spec.Aes.bytesAt m p 16) (Spec.Aes.bytesAt m q 16) := by
+  rw [xor4Mem_eq m hp hq, bytesAt_store4, xor_words4]
+
+/-- The memory after zeroing the block at `c`, a word at a time. -/
+def zero4 (m : Mem) (c : Addr) : Mem := store4 m c 0 0 0 0
+
+theorem zero4_bytes (m : Mem) (c : Addr) : Spec.Aes.bytesAt (zero4 m c) c 16 = Spec.Cmac.zeros 16 := by
+  rw [zero4, bytesAt_store4, le4_zero]; decide
+
+/-- The memory after forming a counter block: the block at `c` is the block
+at `p` XORed with the block at `q`, and the block at `p` is zeroed. -/
+def chainMem4 (m : Mem) (c p q : Addr) : Mem := zero4 (xor4Mem m c p q) p
+
+theorem chainMem4_frame (m : Mem) (C P Q : Addr) : Frame [⟨C, 16⟩, ⟨P, 16⟩] m (chainMem4 m C P Q) :=
+  ((xor4Mem_frame m C P Q).mono (fun r hr => by simp only [List.mem_singleton] at hr; simp [hr])).trans
+    ((frame_store4 P 0 0 0 0).mono (fun r hr => by simp only [List.mem_singleton] at hr; simp [hr]))
+
+theorem chainMem4_state (m : Mem) (C P Q : Addr) :
+    Spec.Aes.bytesAt (chainMem4 m C P Q) P 16 = Spec.Cmac.zeros 16 := zero4_bytes _ _
+
+theorem chainMem4_counter (m : Mem) {C P Q : Addr} (hcp : (⟨C, 16⟩ : Region).Disjoint ⟨P, 16⟩)
+    (hcq : (⟨C, 16⟩ : Region).Disjoint ⟨Q, 16⟩) :
+    Spec.Aes.bytesAt (chainMem4 m C P Q) C 16 =
+      Spec.Cmac.xor (Spec.Aes.bytesAt m P 16) (Spec.Aes.bytesAt m Q 16) := by
+  rw [chainMem4, zero4, bytesAt_frame16 (frame_store4 P 0 0 0 0) (by simpa using hcp),
+    xor4Mem_bytes m (Sep4.of_disjoint hcp) (Sep4.of_disjoint hcq)]
+
+end VG.Proof.Cmac