SHA-384/512/512-224/512-256 streaming on ARMv7 through the shared MdStream code

lean/VerifiedGarbage/Impl/Md5/Arm/Stream.lean

@@ -31,6 +31,8 @@ The generic streaming code (`Impl/MdStream/Arm.lean`). -/
 
 def params : MdStream.Arm.Params where
   N := 16
+  B := 64
+  L := 8
   so := 64
   len := MdStream.Arm.len64 72 false
   out := MdStream.Arm.out32 4 false

lean/VerifiedGarbage/Impl/MdStream/Arm.lean

@@ -3,15 +3,15 @@ import VerifiedGarbage.TCB.Arm.Isa
 /-!
 # Streaming Merkle–Damgård hash functions: 32-bit ARM implementation
 
-The streaming `update` and `finalize` of MD5, SHA-1 and SHA-256, whose blocks
-are 64 bytes and whose length fields are 8 bytes, and which differ only in
-the size of their hash values, in how they store the message length and
-output the digest, and in the compression function they call (`Params`).
+The streaming `update` and `finalize` of MD5, SHA-1, SHA-256 and the SHA-512
+family, which differ only in their sizes, in how they store the message
+length and output the digest, and in the compression function they call
+(`Params`).
 Each hash function's `Impl/<Alg>/Arm/Stream.lean` instantiates them. The
 same algorithm as on AArch64 (`VG.Impl.MdStream.AArch64`).
 
-The streaming state (`N + 64` bytes at `state`) is the hash value (`N`
-bytes) followed by a 64-byte buffer.
+The streaming state (`N + B` bytes at `state`) is the hash value (`N`
+bytes) followed by a `B`-byte buffer.
 
 * `update(state = r0, count = r2:r3, data = [sp], len = [sp, #4],
   scratch = [sp, #8])` compresses, in each iteration, every whole block left
@@ -44,14 +44,18 @@ open VG.Arm
 structure Params where
   /-- The size of the hash value, where the buffer starts. -/
   N : Nat
+  /-- The block size, a power of two. -/
+  B : Nat
+  /-- The size of the length field at the end of the last block. -/
+  L : Nat
   /-- Where our caller's registers are saved in the scratch space, after the
   compression function's own. -/
   so : Nat
   /-- Stores the length field, from `count` in `r4:r5` (low, high), at
-  `r0 + N + 56`; writes only `r9`. -/
+  `r0 + N + B - L`; writes only `r9`. -/
   len : List Instr
   /-- Writes the digest, from the hash value at `r0`, to `r6`; writes only
-  `r9`. -/
+  `r9` and `r10`. -/
   out : List Instr
 
 variable (P : Params)
@@ -84,43 +88,46 @@ Registers: `r4` = bytes in the buffer (`r`), `r5` = `data`, `r6` = bytes of
 `data` left, `r7` = the number of blocks this iteration compresses (at
 `r1`).
 The loop runs while `r6 ≠ 0`, so each iteration starts with `r6 ≥ 1` and
-`r4 < 64`. -/
+`r4 < B`. -/
 
-/-- Every whole block left, straight from `data`: `len >> 6` blocks,
-`(len >> 6) << 6` bytes. -/
+/-- Every whole block left, straight from `data`: `len >> log₂ B` blocks,
+`(len >> log₂ B) << log₂ B` bytes. -/
 def direct : List Instr :=
-  [.mov .r1 (.reg .r5), .mov .r7 (.shifted .r6 .lsr 6), .mov .r12 (.shifted .r7 .lsl 6),
+  [.mov .r1 (.reg .r5), .mov .r7 (.shifted .r6 .lsr (Nat.log2 P.B)),
+    .mov .r12 (.shifted .r7 .lsl (Nat.log2 P.B)),
     .dp .add .r5 .r5 (.reg .r12), .dp .sub .r6 .r6 (.reg .r12)]
 
-/-- Copy `n = min(64 - r, len) ≥ 1` bytes of `data` into the buffer; if that
+/-- Copy `n = min(B - r, len) ≥ 1` bytes of `data` into the buffer; if that
 fills it, compress it. -/
 def fill : Prog isa :=
-  -- r8 := 64 - r; if len < 64 and len + r < 64 (i.e. len < 64 - r), r8 := len.
-  .seq (.block [.mov .r8 (.imm 64), .dp .sub .r8 .r8 (.reg .r4), .mov .r12 (.shifted .r6 .lsr 6),
-      .cmp .r12 (.imm 0)])
+  -- r8 := B - r; if len < B and len + r < B (i.e. len < B - r), r8 := len.
+  .seq (.block [.mov .r8 (.imm (BitVec.ofNat 32 P.B)), .dp .sub .r8 .r8 (.reg .r4),
+      .mov .r12 (.shifted .r6 .lsr (Nat.log2 P.B)), .cmp .r12 (.imm 0)])
   (.seq (.ite .eq
-      (.seq (.block [.dp .add .r12 .r6 (.reg .r4), .mov .r12 (.shifted .r12 .lsr 6), .cmp .r12 (.imm 0)])
+      (.seq (.block [.dp .add .r12 .r6 (.reg .r4), .mov .r12 (.shifted .r12 .lsr (Nat.log2 P.B)),
+          .cmp .r12 (.imm 0)])
         (.ite .eq (.block [.mov .r8 (.reg .r6)]) (.block [])))
       (.block []))
   (.seq (.block [.dp .sub .r6 .r6 (.reg .r8)])
   (.seq (.loop (.block [.ldrb .r12 .r5 0, .dp .add .r1 .r0 (.reg .r4), .strb .r12 .r1 P.N,
       .dp .add .r5 .r5 (.imm 1), .dp .add .r4 .r4 (.imm 1), .subs .r8 .r8 (.imm 1)]) .ne)
   -- Full: compress the buffer.
-  (.seq (.block [.cmp .r4 (.imm 64)])
+  (.seq (.block [.cmp .r4 (.imm (BitVec.ofNat 32 P.B))])
     (.ite .eq (.block [.dp .add .r1 .r0 (.imm (BitVec.ofNat 32 P.N)), .mov .r4 (.imm 0), .mov .r7 (.imm 1)])
       (.block []))))))
 
 def updateBody (name : String) (code : Prog isa) : Prog isa :=
   .seq (.block [.mov .r7 (.imm 0), .cmp .r4 (.imm 0)])
   (.seq (.ite .eq
-      (.seq (.block [.mov .r12 (.shifted .r6 .lsr 6), .cmp .r12 (.imm 0)]) (.ite .eq (fill P) (.block direct)))
+      (.seq (.block [.mov .r12 (.shifted .r6 .lsr (Nat.log2 P.B)), .cmp .r12 (.imm 0)])
+        (.ite .eq (fill P) (.block (direct P))))
       (fill P))
   (.seq (.seq (.block [.cmp .r7 (.imm 0)]) (.ite .eq (.block []) (compressN name code)))
     (.block [.cmp .r6 (.imm 0)])))
 
 def update (name : String) (code : Prog isa) : Prog isa :=
-  .seq (.block ([.ldrSp .r12 8] ++ save P .r12 ++ [.mov .r3 (.reg .r12), .dp .and .r4 .r2 (.imm 63),
-      .ldrSp .r5 0, .ldrSp .r6 4, .cmp .r6 (.imm 0)]))
+  .seq (.block ([.ldrSp .r12 8] ++ save P .r12 ++ [.mov .r3 (.reg .r12),
+      .dp .and .r4 .r2 (.imm (BitVec.ofNat 32 (P.B - 1))), .ldrSp .r5 0, .ldrSp .r6 4, .cmp .r6 (.imm 0)]))
   (.seq (.ite .eq (.block []) (.loop (updateBody P name code) .ne))
     (.block (restore P)))
 
@@ -131,9 +138,9 @@ the buffer (`r`), `r8` = 1 while the block being padded is not the last one
 (then 0). -/
 
 def finalizeBody (name : String) (code : Prog isa) : Prog isa :=
-  -- Zero the buffer from `r` to 64, or to 56 in the last block.
-  .seq (.block [.mov .r9 (.imm 64), .cmp .r8 (.imm 0)])
-  (.seq (.ite .eq (.block [.mov .r9 (.imm 56)]) (.block []))
+  -- Zero the buffer from `r` to `B`, or to `B - L` in the last block.
+  .seq (.block [.mov .r9 (.imm (BitVec.ofNat 32 P.B)), .cmp .r8 (.imm 0)])
+  (.seq (.ite .eq (.block [.mov .r9 (.imm (BitVec.ofNat 32 (P.B - P.L)))]) (.block []))
   (.seq (.block [.mov .r12 (.imm 0), .subs .r9 .r9 (.reg .r7)])
   (.seq (.ite .eq (.block [])
       (.loop (.block [.dp .add .r1 .r0 (.reg .r7), .strb .r12 .r1 P.N, .dp .add .r7 .r7 (.imm 1),
@@ -147,11 +154,11 @@ def finalizeBody (name : String) (code : Prog isa) : Prog isa :=
 
 def finalize (name : String) (code : Prog isa) : Prog isa :=
   .seq (.block ([.ldrSp .r12 4] ++ save P .r12 ++ [.mov .r4 (.reg .r2), .mov .r5 (.reg .r3),
-      .mov .r3 (.reg .r12), .ldrSp .r6 0, .dp .and .r7 .r4 (.imm 63),
+      .mov .r3 (.reg .r12), .ldrSp .r6 0, .dp .and .r7 .r4 (.imm (BitVec.ofNat 32 (P.B - 1))),
       -- The `0x80` byte.
       .mov .r12 (.imm 0x80), .dp .add .r1 .r0 (.reg .r7), .strb .r12 .r1 P.N, .dp .add .r7 .r7 (.imm 1),
-      -- Two blocks iff that leaves fewer than 8 bytes for the length (r ≥ 57).
-      .dp .add .r8 .r7 (.imm 7), .mov .r8 (.shifted .r8 .lsr 6)]))
+      -- Two blocks iff that leaves fewer than `L` bytes for the length (r > B - L).
+      .dp .add .r8 .r7 (.imm (BitVec.ofNat 32 (P.L - 1))), .mov .r8 (.shifted .r8 .lsr (Nat.log2 P.B))]))
   (.seq (.loop (finalizeBody P name code) .eq)
     (.block (P.out ++ restore P)))
 

lean/VerifiedGarbage/Impl/Sha1/Arm/Stream.lean

@@ -31,6 +31,8 @@ The generic streaming code (`Impl/MdStream/Arm.lean`). -/
 
 def params : MdStream.Arm.Params where
   N := 20
+  B := 64
+  L := 8
   so := 112
   len := MdStream.Arm.len64 76 true
   out := MdStream.Arm.out32 5 true

lean/VerifiedGarbage/Impl/Sha256/Arm/Stream.lean

@@ -59,6 +59,8 @@ The generic streaming code (`Impl/MdStream/Arm.lean`). -/
 
 def params : MdStream.Arm.Params where
   N := 32
+  B := 64
+  L := 8
   so := 112
   len := MdStream.Arm.len64 88 true
   out := MdStream.Arm.out32 8 true

lean/VerifiedGarbage/Impl/Sha512/Arm/Stream.lean

@@ -1,4 +1,5 @@
 import VerifiedGarbage.Impl.Sha512.Arm
+import VerifiedGarbage.Impl.MdStream.Arm
 
 /-!
 # Streaming SHA-512: 32-bit ARM implementation
@@ -8,33 +9,20 @@ The streaming state (192 bytes at `state`) is the hash value followed by a
 value is stored little-endian, so as its low half followed by its high half.
 
 * `init iv (state = r0)` stores the initial hash value `iv`.
-* `update(state = r0, count = r2:r3, data = [sp], len = [sp, #4],
-  scratch = [sp, #8])` processes the data in pieces: each iteration copies
-  as many bytes as fit into the buffer (a whole block when the buffer is
-  empty and a whole block remains), and compresses the buffer once it is
-  full.
-* `finalize(state = r0, count = r2:r3, out = [sp], scratch = [sp, #4])` pads
-  the buffered bytes (one or two blocks), compresses them and writes the
-  final hash value.
-
-The buffer is compressed by calling `vg_sha512_compress`, with
-`scratch[0..224)` as its scratch space. Its code never writes `r0` or `r3`,
-so `state` stays in `r0` and `scratch` in `r3`; it preserves `r4`–`r11`, so
-our variables live in `r4`–`r6`. Our caller's `r4`–`r11` and our return
-address (`lr`, which the calls overwrite) are saved in `scratch[224..260)`.
-`finalize` also keeps `count` in `scratch[260..268)`.
-
-Byte `r` of the buffer is addressed as `[r1, #64]` with `r1 = state + r`
-computed just before the access, and `data` is consumed through a pointer
-that advances. Every comparison is a `cmp` or `subs` tested with `eq`/`ne`.
-Every address and branch depends only on `sp`, the pointers, `count` and
-`len`.
+* `update` and `finalize` are the generic streaming code
+  (`Impl/MdStream/Arm.lean`), calling the compression function
+  (`vg_sha512_compress`) with `scratch[0..224)` as its scratch space, and
+  saving our caller's `r4`–`r11` and `lr` in `scratch[224..260)`. The length
+  field is the length in bits as a 128-bit big-endian integer: `count >> 61`,
+  then `count << 3` (modulo 2⁶⁴); the words of the final hash value are
+  big-endian.
 -/
 
 namespace VG.Impl.Sha512.Arm.Stream
 
 open VG.Arm
 open VG.Impl.Sha512.Arm (compress lo hi)
+open VG.Impl.MdStream.Arm (Params len64)
 
 /-- Store word `k` of `iv`. -/
 def initW (iv : Spec.Sha512.HashValue) (k : Nat) : List Instr :=
@@ -46,98 +34,23 @@ def initW (iv : Spec.Sha512.HashValue) (k : Nat) : List Instr :=
 def init (iv : Spec.Sha512.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap (initW iv))
 
-/-- The callee-saved registers we use (and `lr`), and where they are saved in `scratch`. -/
-def saved : List (Reg × Nat) :=
-  [(.r4, 224), (.r5, 228), (.r6, 232), (.r7, 236), (.r8, 240), (.r9, 244), (.r10, 248), (.r11, 252),
-    (.lr, 256)]
-
-/-- Save them, with `scratch` in `b`. -/
-def save (b : Reg) : List Instr := saved.map fun (r, d) => .str r b d
-
-/-- Restore them from `scratch` in `r3`. -/
-def restore : List Instr := saved.map fun (r, d) => .ldr r .r3 d
-
-/-- A call of `vg_sha512_compress`. -/
-def compressCall : Prog isa := .call "vg_sha512_compress" compress
-
-/-- Compress the buffer of the state at `r0` into its hash value, with
-scratch space `r3`. -/
-def compressAt : Prog isa := .seq (.block [.dp .add .r1 .r0 (.imm 64), .mov .r2 (.imm 1)]) compressCall
-
-/-! ## `update`
-
-Registers: `r4` = bytes in the buffer (`r`), `r5` = `data`, `r6` = bytes of
-`data` left. The loop runs while `r6 ≠ 0`, so each iteration starts with
-`r6 ≥ 1` and `r4 < 128`. -/
-
-/-- Copy `n = min(128 - r, len) ≥ 1` bytes of `data` into the buffer; if that
-fills it, compress it. -/
-def fill : Prog isa :=
-  -- r8 := 128 - r; if len < 128 and len + r < 128 (i.e. len < 128 - r), r8 := len.
-  .seq (.block [.mov .r8 (.imm 128), .dp .sub .r8 .r8 (.reg .r4), .mov .r12 (.shifted .r6 .lsr 7),
-      .cmp .r12 (.imm 0)])
-  (.seq (.ite .eq
-      (.seq (.block [.dp .add .r12 .r6 (.reg .r4), .mov .r12 (.shifted .r12 .lsr 7), .cmp .r12 (.imm 0)])
-        (.ite .eq (.block [.mov .r8 (.reg .r6)]) (.block [])))
-      (.block []))
-  (.seq (.block [.dp .sub .r6 .r6 (.reg .r8)])
-  (.seq (.loop (.block [.ldrb .r12 .r5 0, .dp .add .r1 .r0 (.reg .r4), .strb .r12 .r1 64,
-      .dp .add .r5 .r5 (.imm 1), .dp .add .r4 .r4 (.imm 1), .subs .r8 .r8 (.imm 1)]) .ne)
-  -- Full: compress the buffer.
-  (.seq (.block [.cmp .r4 (.imm 128)])
-    (.ite .eq (.seq compressAt (.block [.mov .r4 (.imm 0)])) (.block []))))))
-
-def updateBody : Prog isa := .seq fill (.block [.cmp .r6 (.imm 0)])
-
-def update : Prog isa :=
-  .seq (.block ([.ldrSp .r12 8] ++ save .r12 ++ [.mov .r3 (.reg .r12), .dp .and .r4 .r2 (.imm 127),
-      .ldrSp .r5 0, .ldrSp .r6 4, .cmp .r6 (.imm 0)]))
-  (.seq (.ite .eq (.block []) (.loop updateBody .ne))
-    (.block restore))
-
-/-! ## `finalize`
-
-Registers: `r4` = bytes in the buffer (`r`), `r5` = 1 while the block being
-padded is not the last one (then 0), `r6` = `out`. -/
-
-/-- The message length in bits as a 128-bit big-endian integer, at the end of
-the buffer: `count >> 61`, then `count << 3` (modulo 2⁶⁴), from `count` in
-`scratch[260..268)`. -/
-def lenW : List Instr :=
-  [.ldr .r9 .r3 260, .ldr .r10 .r3 264,
-   .mov .r11 (.imm 0), .str .r11 .r0 176,
-   .mov .r11 (.shifted .r10 .lsr 29), .rev .r11 .r11, .str .r11 .r0 180,
-   .mov .r11 (.shifted .r10 .lsl 3), .dp .orr .r11 .r11 (.shifted .r9 .lsr 29), .rev .r11 .r11,
-   .str .r11 .r0 184,
-   .mov .r11 (.shifted .r9 .lsl 3), .rev .r11 .r11, .str .r11 .r0 188]
-
-def finalizeBody : Prog isa :=
-  -- Zero the buffer from `r` to 128, or to 112 in the last block.
-  .seq (.block [.mov .r9 (.imm 128), .cmp .r5 (.imm 0)])
-  (.seq (.ite .eq (.block [.mov .r9 (.imm 112)]) (.block []))
-  (.seq (.block [.mov .r12 (.imm 0), .subs .r9 .r9 (.reg .r4)])
-  (.seq (.ite .eq (.block [])
-      (.loop (.block [.dp .add .r1 .r0 (.reg .r4), .strb .r12 .r1 64, .dp .add .r4 .r4 (.imm 1),
-        .subs .r9 .r9 (.imm 1)]) .ne))
-  -- In the last block, the message length.
-  (.seq (.block [.cmp .r5 (.imm 0)])
-  (.seq (.ite .eq (.block lenW) (.block []))
-  (.seq compressAt
-    (.block [.mov .r4 (.imm 0), .subs .r5 .r5 (.imm 1)])))))))
-
 /-- Word `k` of the final hash value, big-endian. -/
 def outW (k : Nat) : List Instr :=
   [.ldr .r9 .r0 (8 * k), .ldr .r10 .r0 (8 * k + 4), .rev .r10 .r10, .rev .r9 .r9,
    .str .r10 .r6 (8 * k), .str .r9 .r6 (8 * k + 4)]
 
-def finalize : Prog isa :=
-  .seq (.block ([.ldrSp .r12 4] ++ save .r12 ++ [.str .r2 .r12 260, .str .r3 .r12 264,
-      .mov .r3 (.reg .r12), .ldrSp .r6 0, .dp .and .r4 .r2 (.imm 127),
-      -- The `0x80` byte.
-      .mov .r12 (.imm 0x80), .dp .add .r1 .r0 (.reg .r4), .strb .r12 .r1 64, .dp .add .r4 .r4 (.imm 1),
-      -- Two blocks iff that leaves fewer than 16 bytes for the length (r ≥ 113).
-      .dp .add .r5 .r4 (.imm 15), .mov .r5 (.shifted .r5 .lsr 7)]))
-  (.seq (.loop finalizeBody .eq)
-    (.block ((List.range 8).flatMap outW ++ restore)))
+/-- The sizes, the length field and the digest. -/
+def params : Params where
+  N := 64
+  B := 128
+  L := 16
+  so := 224
+  len := [.mov .r9 (.imm 0), .str .r9 .r0 176, .mov .r9 (.shifted .r5 .lsr 29), .rev .r9 .r9, .str .r9 .r0 180] ++
+    len64 184 true
+  out := (List.range 8).flatMap outW
+
+def update : Prog isa := MdStream.Arm.update params "vg_sha512_compress" compress
+
+def finalize : Prog isa := MdStream.Arm.finalize params "vg_sha512_compress" compress
 
 end VG.Impl.Sha512.Arm.Stream

lean/VerifiedGarbage/Proof/Ed25519/Arm/Whole/Hash.lean

@@ -14,12 +14,14 @@ private theorem rounds_noFrames (n : Nat) : (Impl.Sha512.Arm.rounds n).noFrames
   | succ n ih => simp only [Impl.Sha512.Arm.rounds, Code.noFrames, ih, Bool.and_self]
 
 theorem update_noFrames : update.noFrames = true := by
-  simp only [update, updateBody, fill, compressAt, compressCall,
+  simp only [update, Impl.MdStream.Arm.update, Impl.MdStream.Arm.updateBody, Impl.MdStream.Arm.fill,
+    Impl.MdStream.Arm.compressN, Impl.MdStream.Arm.compressWith,
     Impl.Sha512.Arm.compress, Impl.Sha512.Arm.body, Code.noFrames, Bool.and_self]
   rw [rounds_noFrames]; rfl
 
 theorem finalize_noFrames : finalize.noFrames = true := by
-  simp only [finalize, finalizeBody, compressAt, compressCall,
+  simp only [finalize, Impl.MdStream.Arm.finalize, Impl.MdStream.Arm.finalizeBody,
+    Impl.MdStream.Arm.compressAt, Impl.MdStream.Arm.compressWith,
     Impl.Sha512.Arm.compress, Impl.Sha512.Arm.body, Code.noFrames, Bool.and_self]
   rw [rounds_noFrames]; rfl
 

lean/VerifiedGarbage/Proof/Md5/Arm/Stream/Md.lean

@@ -23,13 +23,14 @@ open VG VG.Arm VG.Proof.MdStream VG.Proof.MdStream.Arm
 
 abbrev params := Impl.Md5.Arm.Stream.params
 
-theorem dims : Dims params := ⟨by decide, by decide, by decide⟩
+theorem dims : Dims params := ⟨.inl rfl, by decide, by decide, by decide, by decide, by decide⟩
 
 theorem shape : Shape (P := params) md where
-  len _ hfit hout := len64_ok (d := params.N + 56) (be := false) (by decide) (by omega) hout
+  len _ hfit hout := len64_ok (d := params.N + (params.B - params.L)) (be := false) (by decide)
+    (by have : params.B = 64 := rfl; have : params.L = 8 := rfl; omega) hout
   out _ f₀ f₆ hin hout hd := by
     refine (out32_ok (n := 4) false (by decide) f₀ f₆ hin hout hd).mono fun s' ⟨g, rd, wr, sp, m⟩ =>
-      ⟨g, rd, wr, sp, ?_⟩
+      ⟨fun r h _ => g r h, rd, wr, sp, ?_⟩
     rw [m, digest_eq]
 
 theorem callee : CalleeOk (P := params) md Impl.Md5.Arm.compress :=