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

lean/VerifiedGarbage/Impl/Md5/X86/Stream.lean

@@ -32,6 +32,8 @@ def init : Prog isa :=
 /-- The sizes, the length field and the digest. -/
 def params : Params where
   N := 16
+  B := 64
+  L := 8
   so := 64
   len := len64 64 72 false
   out := out32 4 false

lean/VerifiedGarbage/Impl/MdStream/X86.lean

@@ -3,15 +3,14 @@ import VerifiedGarbage.TCB.X86.Isa
 /-!
 # Streaming Merkle–Damgård hash functions: x86 (32-bit) implementation
 
-The streaming `update` and `finalize` of the hash functions whose blocks are
-64 bytes and whose length fields are 8 bytes, 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`). Each hash
-function's `Impl/<Alg>/X86/Stream.lean` instantiates them. The same
-algorithm as on x86-64 (`VG.Impl.MdStream.X86_64`).
+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>/X86/Stream.lean` instantiates
+them. The same algorithm as on x86-64 (`VG.Impl.MdStream.X86_64`).
 
-The streaming state (`N + 64` bytes at `state`) is the hash value (`N`
-bytes) followed by a 64-byte buffer. Every argument is on the stack (cdecl).
+The streaming state (`N + B` bytes at `state`) is the hash value (`N` bytes)
+followed by a `B`-byte buffer. Every argument is on the stack (cdecl).
 
 * `update(state, count, data, len, scratch)` compresses, in each iteration,
   every whole block left in `data` with one call if the buffer is empty (so
@@ -41,12 +40,16 @@ def at_ (b : Reg) (d : Nat) : MemOp := { base := b, disp := d }
 structure Params where
   /-- The size of the hash value, where the buffer starts. -/
   N : Nat
+  /-- The block size. -/
+  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; `finalize` keeps `count` and `out` after them,
   in `scratch[so+16..so+28)`. -/
   so : Nat
   /-- Stores the length field, from `count` in `[ebp + so + 16]` (low word)
-  and `[ebp + so + 20]` (high word), at `ebx + N + 56`; writes only `eax`,
+  and `[ebp + so + 20]` (high word), at `ebx + N + B - L`; writes only `eax`,
   `ecx` and `edx` (and the flags). -/
   len : List Instr
   /-- Writes the digest, from the hash value at `ebx`, to `eax`; writes only
@@ -83,29 +86,30 @@ Registers: `ebx` = `state`, `ebp` = `data`, `esi` = bytes of `data` left,
 compress and `ecx` = the number of blocks to compress there. `scratch` is read from its
 argument slot (`[esp + 24]`) when needed. -/
 
-/-- Every whole block left, straight from `data`: `esi - (esi & 63)` bytes,
-`(esi - (esi & 63)) >> 6` blocks. -/
+/-- Every whole block left, straight from `data`: `esi - esi mod B` bytes,
+`(esi - esi mod B) >> log₂ B` blocks. -/
 def direct : List Instr :=
-  [.mov .eax (.reg .ebp), .mov .ecx (.reg .esi), .alu .and .ecx (.imm 63), .mov .edx (.reg .esi),
-   .alu .sub .edx (.reg .ecx), .alu .add .ebp (.reg .edx), .mov .esi (.reg .ecx), .mov .ecx (.reg .edx),
-   .shift .shr .ecx 6]
+  [.mov .eax (.reg .ebp), .mov .ecx (.reg .esi), .alu .and .ecx (.imm (BitVec.ofNat 32 (P.B - 1))),
+   .mov .edx (.reg .esi), .alu .sub .edx (.reg .ecx), .alu .add .ebp (.reg .edx), .mov .esi (.reg .ecx),
+   .mov .ecx (.reg .edx), .shift .shr .ecx (Nat.log2 P.B)]
 
-/-- Copy `min(64 - edi, esi)` bytes of `data` into the buffer; if that fills it,
+/-- Copy `min(B - edi, esi)` bytes of `data` into the buffer; if that fills it,
 compress it. -/
 def fill : Prog isa :=
-  .seq (.block [.mov .eax (.imm 64), .alu .sub .eax (.reg .edi), .alu .cmp .esi (.reg .eax)])
+  .seq (.block [.mov .eax (.imm (BitVec.ofNat 32 P.B)), .alu .sub .eax (.reg .edi), .alu .cmp .esi (.reg .eax)])
   (.seq (.ite .b (.block [.mov .eax (.reg .esi)]) (.block []))
   (.seq (.block [.alu .sub .esi (.reg .eax), .alu .add .edi (.reg .ebx), .alu .test .eax (.reg .eax)])
   (.seq (.ite .e (.block [])
       (.loop (.block [.movzx8 .ecx (at_ .ebp 0), .store8 (at_ .edi P.N) .cl,
         .alu .add .ebp (.imm 1), .alu .add .edi (.imm 1), .alu .sub .eax (.imm 1)]) .ne))
-  (.seq (.block [.alu .sub .edi (.reg .ebx), .mov .ecx (.imm 0), .alu .cmp .edi (.imm 64)])
+  (.seq (.block [.alu .sub .edi (.reg .ebx), .mov .ecx (.imm 0), .alu .cmp .edi (.imm (BitVec.ofNat 32 P.B))])
     (.ite .e (.block [.mov .eax (.reg .ebx), .alu .add .eax (.imm (BitVec.ofNat 32 P.N)), .mov .edi (.imm 0),
         .mov .ecx (.imm 1)]) (.block []))))))
 
 def updateBody (name : String) (code : Prog isa) : Prog isa :=
   .seq (.block [.alu .test .edi (.reg .edi)])
-  (.seq (.ite .e (.seq (.block [.alu .cmp .esi (.imm 64)]) (.ite .ae (.block direct) (fill P))) (fill P))
+  (.seq (.ite .e (.seq (.block [.alu .cmp .esi (.imm (BitVec.ofNat 32 P.B))]) (.ite .ae (.block (direct P)) (fill P)))
+    (fill P))
   (.seq (.block [.alu .test .ecx (.reg .ecx)])
     (.ite .ne (.seq (.block [.mov .edx (.mem (at_ .esp 24))])
         (.seq (compressN name code .ebx .edx) (.block [.mov .ecx (.imm 1), .alu .test .ecx (.reg .ecx)])))
@@ -114,7 +118,7 @@ def updateBody (name : String) (code : Prog isa) : Prog isa :=
 def update (name : String) (code : Prog isa) : Prog isa :=
   .seq (.block ([.mov .eax (.mem (at_ .esp 24))] ++ save P .eax ++
       [.mov .ebx (.mem (at_ .esp 4)), .mov .ebp (.mem (at_ .esp 16)), .mov .esi (.mem (at_ .esp 20)),
-       .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm 63)]))
+       .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm (BitVec.ofNat 32 (P.B - 1)))]))
     (.seq (.loop (updateBody P name code) .ne) (.block (.mov .eax (.mem (at_ .esp 24)) :: restore P .eax)))
 
 /-! ## `finalize`
@@ -124,9 +128,9 @@ Registers: `ebx` = `state`, `ebp` = `scratch`, `edi` = bytes in the buffer,
 `out` are kept in `scratch[so+16..so+28)`. -/
 
 def finalizeBody (name : String) (code : Prog isa) : Prog isa :=
-  -- Zero the buffer from `edi` to 64, or to 56 in the last block.
-  .seq (.block [.mov .eax (.imm 64), .alu .test .esi (.reg .esi)])
-  (.seq (.ite .e (.block [.mov .eax (.imm 56)]) (.block []))
+  -- Zero the buffer from `edi` to `B`, or to `B - L` in the last block.
+  .seq (.block [.mov .eax (.imm (BitVec.ofNat 32 P.B)), .alu .test .esi (.reg .esi)])
+  (.seq (.ite .e (.block [.mov .eax (.imm (BitVec.ofNat 32 (P.B - P.L)))]) (.block []))
   (.seq (.block [.mov .ecx (.imm 0), .alu .sub .eax (.reg .edi)])
   (.seq (.ite .e (.block [])
       (.loop (.block [.mov .edx (.reg .ebx), .alu .add .edx (.reg .edi), .store8 (at_ .edx P.N) .cl,
@@ -144,12 +148,12 @@ def finalize (name : String) (code : Prog isa) : Prog isa :=
        .mov .ecx (.mem (at_ .esp 8)), .store (at_ .ebp (P.so + 16)) .ecx,
        .mov .ecx (.mem (at_ .esp 12)), .store (at_ .ebp (P.so + 20)) .ecx,
        .mov .ecx (.mem (at_ .esp 16)), .store (at_ .ebp (P.so + 24)) .ecx,
-       .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm 63),
+       .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm (BitVec.ofNat 32 (P.B - 1))),
        -- The `0x80` byte.
        .mov .edx (.reg .ebx), .alu .add .edx (.reg .edi), .mov .ecx (.imm 0x80),
        .store8 (at_ .edx P.N) .cl, .alu .add .edi (.imm 1),
-       -- Two blocks if it leaves fewer than 8 bytes for the length.
-       .mov .esi (.imm 0), .alu .cmp .edi (.imm 57)]))
+       -- Two blocks if it leaves fewer than `L` bytes for the length.
+       .mov .esi (.imm 0), .alu .cmp .edi (.imm (BitVec.ofNat 32 (P.B - P.L + 1)))]))
   (.seq (.ite .ae (.block [.mov .esi (.imm 1)]) (.block []))
   (.seq (.loop (finalizeBody P name code) .e)
     (.block (.mov .eax (.mem (at_ .ebp (P.so + 24))) :: (P.out ++ restore P .ebp)))))
@@ -158,21 +162,35 @@ def finalize (name : String) (code : Prog isa) : Prog isa :=
 
 The `len` and `out` of the hash functions here. -/
 
-/-- The length in bits, `8 · count` (modulo 2⁶⁴, from `count` in `[ebp + so +
-16]` and `[ebp + so + 20]`), as 8 bytes at `ebx + d`, big-endian if `be` and
+/-- The length in bits, `8 · count` (modulo 2⁶⁴, from `count` in `eax` (low
+word) and `ecx` (high word)), as 8 bytes at `ebx + d`, big-endian if `be` and
 little-endian otherwise. -/
-def len64 (so d : Nat) (be : Bool) : List Instr :=
-  [.mov .eax (.mem (at_ .ebp (so + 16))), .mov .ecx (.mem (at_ .ebp (so + 20))),
-   .alu .add .ecx (.reg .ecx), .alu .add .ecx (.reg .ecx), .alu .add .ecx (.reg .ecx),
+def len64Of (d : Nat) (be : Bool) : List Instr :=
+  [.alu .add .ecx (.reg .ecx), .alu .add .ecx (.reg .ecx), .alu .add .ecx (.reg .ecx),
    .mov .edx (.reg .eax), .shift .shr .edx 29, .alu .or .ecx (.reg .edx),
    .alu .add .eax (.reg .eax), .alu .add .eax (.reg .eax), .alu .add .eax (.reg .eax)] ++
   if be then [.bswap .ecx, .store (at_ .ebx d) .ecx, .bswap .eax, .store (at_ .ebx (d + 4)) .eax]
   else [.store (at_ .ebx d) .eax, .store (at_ .ebx (d + 4)) .ecx]
 
+/-- Load `count`, from `[ebp + so + 16]` (low word) and `[ebp + so + 20]`
+(high word), into `eax` and `ecx`. -/
+def loadCount (so : Nat) : List Instr :=
+  [.mov .eax (.mem (at_ .ebp (so + 16))), .mov .ecx (.mem (at_ .ebp (so + 20)))]
+
+/-- `len64Of` from `count` in scratch. -/
+def len64 (so d : Nat) (be : Bool) : List Instr := loadCount so ++ len64Of d be
+
 /-- The `n` 32-bit words at `ebx`, written to `eax`, big-endian if `be` and
 little-endian otherwise. -/
 def out32 (n : Nat) (be : Bool) : List Instr :=
   (List.range n).flatMap fun k => [.mov .ecx (.mem (at_ .ebx (4 * k)))] ++
     (if be then [.bswap .ecx] else []) ++ [.store (at_ .eax (4 * k)) .ecx]
 
+/-- The `n` 64-bit words at `ebx` (each little-endian: its low half first),
+written to `eax` big-endian. -/
+def out64 (n : Nat) : List Instr :=
+  (List.range n).flatMap fun k =>
+    [.mov .ecx (.mem (at_ .ebx (8 * k + 4))), .bswap .ecx, .store (at_ .eax (8 * k)) .ecx,
+     .mov .ecx (.mem (at_ .ebx (8 * k))), .bswap .ecx, .store (at_ .eax (8 * k + 4)) .ecx]
+
 end VG.Impl.MdStream.X86

lean/VerifiedGarbage/Impl/Sha1/X86/Stream.lean

@@ -32,6 +32,8 @@ def init : Prog isa :=
 /-- The sizes, the length field and the digest. -/
 def params : Params where
   N := 20
+  B := 64
+  L := 8
   so := 112
   len := len64 112 76 true
   out := out32 5 true

lean/VerifiedGarbage/Impl/Sha256/X86/Stream.lean

@@ -68,6 +68,8 @@ The generic streaming code (`Impl/MdStream/X86.lean`). -/
 /-- SHA-256's sizes, length field and digest in the generic streaming code. -/
 def params : MdStream.X86.Params where
   N := 32
+  B := 64
+  L := 8
   so := 112
   len := MdStream.X86.len64 112 88 true
   out := MdStream.X86.out32 8 true

lean/VerifiedGarbage/Impl/Sha512/X86/Stream.lean

@@ -1,4 +1,5 @@
 import VerifiedGarbage.Impl.Sha512.X86
+import VerifiedGarbage.Impl.MdStream.X86
 
 /-!
 # Streaming SHA-512: x86 (32-bit) implementation
@@ -9,29 +10,22 @@ value is stored little-endian, so as its low half followed by its high half.
 Every argument is on the stack (cdecl).
 
 * `init iv (state)` stores the initial hash value `iv`.
-* `update(state, count, data, len, scratch)` processes the data in pieces:
-  each iteration copies as many bytes as fit into the buffer, and compresses
-  the buffer once it is full.
-* `finalize(state, count, out, scratch)` 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. Each call pushes the four arguments
-(`scratch`, `1`, the buffer and `state`) in a frame of its own, popped (into
-`eax`) when it returns: with the return address the call stores, it uses the
-20 bytes below `esp`. The compression function preserves `ebx`, `esi`,
-`edi` and `ebp`, so our variables live there across it, and our caller's
-values of those registers are saved in `scratch[224..240)`; `scratch` and
-`count` are read from their argument slots when needed. Byte `r` of the
-buffer is addressed as `[eax + 64]` with `eax = state + r` computed just
-before the access. Every address and branch depends only on `esp`, the
-pointers, `count` and `len`.
+* `update(state, count, data, len, scratch)` and
+  `finalize(state, count, out, scratch)` are the generic streaming code of
+  `Impl/MdStream/X86.lean`, calling `vg_sha512_compress`
+  (`Impl.Sha512.X86.compress`) with `scratch[0..224)` as its scratch space;
+  our caller's callee-saved registers are saved in `scratch[224..240)`, and
+  `finalize` keeps `count` and `out` in `scratch[240..252)`. 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.X86.Stream
 
 open VG.X86
 open VG.Impl.Sha512.X86 (at_ compress lo hi)
+open VG.Impl.MdStream.X86 (Params loadCount len64Of out64)
 
 /-- Store word `k` of `iv`, at `eax`. -/
 def initW (iv : Spec.Sha512.HashValue) (k : Nat) : List Instr :=
@@ -41,103 +35,18 @@ def initW (iv : Spec.Sha512.HashValue) (k : Nat) : List Instr :=
 def init (iv : Spec.Sha512.HashValue) : Prog isa :=
   .block (.mov .eax (.mem (at_ .esp 4)) :: (List.range 8).flatMap (initW iv))
 
-/-- The callee-saved registers, and where they are saved in `scratch`. -/
-def saved : List (Reg × Nat) := [(.ebx, 224), (.esi, 228), (.edi, 232), (.ebp, 236)]
-
-/-- Save them, with `scratch` in `eax`. -/
-def save : List Instr := saved.map fun (r, d) => .store (at_ .eax d) r
-
-/-- Restore them, with `scratch` in `eax`. -/
-def restore : List Instr := saved.map fun (r, d) => .mov r (.mem (at_ .eax d))
-
-/-- A call of `vg_sha512_compress(ebx, eax, ecx, edx)`: its arguments pushed
-last to first. -/
-def compressCall : Prog isa :=
-  .frame (.push [.edx, .ecx, .eax, .ebx]) (.call "vg_sha512_compress" compress) (.pop .eax 4)
-
-/-- Compress the buffer of the state at `ebx` into its hash value, with the
-scratch space whose address is at `[esp + d]`. -/
-def compressAt (d : Nat) : Prog isa :=
-  .seq (.block [.mov .eax (.reg .ebx), .alu .add .eax (.imm 64), .mov .ecx (.imm 1),
-    .mov .edx (.mem (at_ .esp d))]) compressCall
-
-/-! ## `update`
-
-Registers: `ebx` = `state`, `esi` = `data`, `ebp` = bytes of `data` left,
-`edi` = bytes in the buffer (`r`); `scratch` is at `[esp + 24]`. The loop
-runs while `ebp ≠ 0`, so each iteration starts with `ebp ≥ 1` and `edi <
-128`. -/
-
-/-- Copy `ecx = min(128 - r, len) ≥ 1` bytes of `data` into the buffer; if
-that fills it, compress it. -/
-def fill : Prog isa :=
-  .seq (.block [.mov .ecx (.imm 128), .alu .sub .ecx (.reg .edi), .alu .cmp .ebp (.reg .ecx)])
-  (.seq (.ite .b (.block [.mov .ecx (.reg .ebp)]) (.block []))
-  (.seq (.block [.alu .sub .ebp (.reg .ecx)])
-  (.seq (.loop (.block [.movzx8 .edx (at_ .esi 0), .mov .eax (.reg .ebx), .alu .add .eax (.reg .edi),
-      .store8 (at_ .eax 64) .dl, .alu .add .esi (.imm 1), .alu .add .edi (.imm 1),
-      .alu .sub .ecx (.imm 1)]) .ne)
-  -- Full: compress the buffer.
-  (.seq (.block [.alu .cmp .edi (.imm 128)])
-    (.ite .e (.seq (compressAt 24) (.block [.mov .edi (.imm 0)])) (.block []))))))
-
-def updateBody : Prog isa := .seq fill (.block [.alu .test .ebp (.reg .ebp)])
-
-def update : Prog isa :=
-  .seq (.block ([.mov .eax (.mem (at_ .esp 24))] ++ save ++
-      [.mov .ebx (.mem (at_ .esp 4)), .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm 127),
-       .mov .esi (.mem (at_ .esp 16)), .mov .ebp (.mem (at_ .esp 20)), .alu .test .ebp (.reg .ebp)]))
-  (.seq (.ite .e (.block []) (.loop updateBody .ne))
-    (.block (.mov .eax (.mem (at_ .esp 24)) :: restore)))
-
-/-! ## `finalize`
-
-Registers: `ebx` = `state`, `edi` = bytes in the buffer (`r`), `esi` = 1
-while the block being padded is not the last one (then 0); `count` is at
-`[esp + 8]`, `out` at `[esp + 16]` and `scratch` at `[esp + 20]`. -/
-
-/-- 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⁶⁴). -/
-def lenW : List Instr :=
-  [.mov .eax (.mem (at_ .esp 8)), .mov .ecx (.mem (at_ .esp 12)),
-   .mov .edx (.imm 0), .store (at_ .ebx 176) .edx,
-   .mov .edx (.reg .ecx), .shift .shr .edx 29, .bswap .edx, .store (at_ .ebx 180) .edx,
-   .alu .add .ecx (.reg .ecx), .alu .add .ecx (.reg .ecx), .alu .add .ecx (.reg .ecx),
-   .mov .edx (.reg .eax), .shift .shr .edx 29, .alu .or .ecx (.reg .edx), .bswap .ecx,
-   .store (at_ .ebx 184) .ecx,
-   .alu .add .eax (.reg .eax), .alu .add .eax (.reg .eax), .alu .add .eax (.reg .eax), .bswap .eax,
-   .store (at_ .ebx 188) .eax]
-
-def finalizeBody : Prog isa :=
-  -- Zero the buffer from `r` to 128, or to 112 in the last block.
-  .seq (.block [.mov .eax (.imm 128), .alu .test .esi (.reg .esi)])
-  (.seq (.ite .e (.block [.mov .eax (.imm 112)]) (.block []))
-  (.seq (.block [.mov .ecx (.imm 0), .alu .sub .eax (.reg .edi)])
-  (.seq (.ite .e (.block [])
-      (.loop (.block [.mov .edx (.reg .ebx), .alu .add .edx (.reg .edi), .store8 (at_ .edx 64) .cl,
-        .alu .add .edi (.imm 1), .alu .sub .eax (.imm 1)]) .ne))
-  -- In the last block, the message length.
-  (.seq (.block [.alu .test .esi (.reg .esi)])
-  (.seq (.ite .e (.block lenW) (.block []))
-  (.seq (compressAt 20)
-    (.block [.mov .edi (.imm 0), .alu .sub .esi (.imm 1)])))))))
+/-- The sizes, the length field and the digest. -/
+def params : Params where
+  N := 64
+  B := 128
+  L := 16
+  so := 224
+  len := loadCount 224 ++ [.mov .edx (.imm 0), .store (at_ .ebx 176) .edx,
+    .mov .edx (.reg .ecx), .shift .shr .edx 29, .bswap .edx, .store (at_ .ebx 180) .edx] ++ len64Of 184 true
+  out := out64 8
 
-/-- Word `k` of the final hash value, big-endian, to `out` at `eax`. -/
-def outW (k : Nat) : List Instr :=
-  [.mov .ecx (.mem (at_ .ebx (8 * k))), .mov .edx (.mem (at_ .ebx (8 * k + 4))), .bswap .edx,
-   .bswap .ecx, .store (at_ .eax (8 * k)) .edx, .store (at_ .eax (8 * k + 4)) .ecx]
+def update : Prog isa := MdStream.X86.update params "vg_sha512_compress" compress
 
-def finalize : Prog isa :=
-  .seq (.block ([.mov .eax (.mem (at_ .esp 20))] ++ save ++
-      [.mov .ebx (.mem (at_ .esp 4)), .mov .edi (.mem (at_ .esp 8)), .alu .and .edi (.imm 127),
-       -- The `0x80` byte.
-       .mov .eax (.reg .ebx), .alu .add .eax (.reg .edi), .mov .ecx (.imm 0x80),
-       .store8 (at_ .eax 64) .cl, .alu .add .edi (.imm 1),
-       -- Two blocks if that leaves fewer than 16 bytes for the length (r ≥ 113).
-       .mov .esi (.imm 0), .alu .cmp .edi (.imm 113)]))
-  (.seq (.ite .ae (.block [.mov .esi (.imm 1)]) (.block []))
-  (.seq (.loop finalizeBody .e)
-    (.block (.mov .eax (.mem (at_ .esp 16)) :: (List.range 8).flatMap outW ++
-      .mov .eax (.mem (at_ .esp 20)) :: restore))))
+def finalize : Prog isa := MdStream.X86.finalize params "vg_sha512_compress" compress
 
 end VG.Impl.Sha512.X86.Stream

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

@@ -25,11 +25,12 @@ open VG VG.X86 VG.Proof.MdStream VG.Proof.MdStream.X86
 
 abbrev params := Impl.Md5.X86.Stream.params
 
-theorem dims : Dims params 112 := ⟨by decide, by decide, by decide⟩
+theorem dims : Dims params 112 := ⟨.inl rfl, by decide, by decide, by decide, by decide⟩
 
 theorem shape : Shape (P := params) md where
-  len _ hfit hlo hhi ho₁ ho₂ := len64_ok (so := params.so) (d := params.N + 56) (be := false) (by omega)
-    hlo hhi ho₁ ho₂
+  len _ hfit hlo hhi ho := len64_ok (so := params.so) (d := params.N + params.B - params.L) (be := false)
+    (by have : params.N + params.B - params.L + 8 = params.N + params.B := rfl; omega) hlo hhi
+    (ho _ (Nat.le_refl _) (by decide)) (ho _ (by decide) (by decide))
   out _ hbx hax hin hout hd := by
     refine (out32_ok (n := 4) false (by decide) hbx hax hin hout hd).mono fun s' ⟨g, rd, wr, m⟩ =>
       ⟨g, rd, wr, ?_⟩