HMAC init on ARMv7 and x86: compress the padded key blocks directly

lean/VerifiedGarbage/Artifacts/HmacMd5/Arm.lean

@@ -4,31 +4,30 @@ import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Instances
 /-!
 # HMAC-MD5 (RFC 2104) on ARMv7
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/Arm.lean`), calling MD5's verified streaming `init` and
-`update`.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/Arm.lean`). `init` sets both states' hash values with MD5's
+verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word by word
+into their buffers, and absorbs each with one call of MD5's verified
+compression function.
 
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/Arm.lean`): it finalizes the inner state with MD5's verified
-streaming `finalize`, then computes the outer hash as one call of MD5's
-verified compression function (`vg_md5_compress`), on a block laid out at
-fixed offsets in `scratch`. It pushes 8 bytes of stack (the stack arguments of
-`finalize`); `stack` is that of the shared contract, 16 bytes.
+`finalize` finalizes the inner state with MD5's verified streaming `finalize`,
+then computes the outer hash as one call of MD5's verified compression
+function (`vg_md5_compress`), on a block laid out at fixed offsets in
+`scratch`. It pushes 8 bytes of stack (the stack arguments of `finalize`);
+`stack` is that of the shared contract, 16 bytes.
 -/
 
 namespace VG.Artifacts.HmacMd5.Arm
 
-open VG.Proof.Hmac.Generic.Arm
-
 def artifacts : List Artifact := [
   { Spec.Hmac.md5I.initApi with
     target := Arm.target
     doc := Spec.Hmac.md5I.initApi.doc
-    code := md5H.init
+    code := Proof.Pbkdf2.Md.Arm.md5Md.hmacInit
     contract := Spec.Hmac.md5I.initContract Arm.abi 16
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     stack := 16
-    verified := Instances.md5_init
+    verified := Proof.Pbkdf2.Md.Arm.Instances.md5_init
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
   { Spec.Hmac.md5I.finalizeApi with
     target := Arm.target

lean/VerifiedGarbage/Artifacts/HmacMd5/X86.lean

@@ -1,33 +1,32 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Hmac.Generic.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 
 /-!
 # HMAC-MD5 (RFC 2104) on x86
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling MD5's verified `init` and `update`.
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/X86.lean`): it calls MD5's verified streaming `finalize`
-for the inner hash, then computes the outer hash with one call of MD5's
-verified compression function, on a block it lays out word by word in
-`scratch`: the outer key's hash value, the inner digest, its padding and
-length.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`). `init` sets both states' hash values with MD5's
+verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word by word
+into their buffers, and absorbs each with one call of MD5's verified
+compression function.
+
+`finalize` calls MD5's verified streaming `finalize` for the inner hash, then
+computes the outer hash with one call of MD5's verified compression function,
+on a block it lays out word by word in `scratch`: the outer key's hash value,
+the inner digest, its padding and length.
 -/
 
 namespace VG.Artifacts.HmacMd5.X86
 
-open VG.Proof.Hmac.Generic.X86
-
 def artifacts : List Artifact := [
   { Spec.Hmac.md5I.initApi with
     target := X86.target
     doc := Spec.Hmac.md5I.initApi.doc
-    code := md5H.init
+    code := Proof.Pbkdf2.Md.X86.md5M.hmacInit
     contract := Spec.Hmac.md5I.initContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     stack := 48
-    verified := Instances.md5_init
+    verified := Proof.Pbkdf2.Md.X86.Instances.md5_init
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.md5I.finalizeApi with
     target := X86.target

lean/VerifiedGarbage/Artifacts/HmacSha1/Arm.lean

@@ -4,31 +4,30 @@ import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Instances
 /-!
 # HMAC-SHA-1 (RFC 2104) on ARMv7
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/Arm.lean`), calling SHA-1's verified streaming `init` and
-`update`.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/Arm.lean`). `init` sets both states' hash values with SHA-1's
+verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word by word
+into their buffers, and absorbs each with one call of SHA-1's verified
+compression function.
 
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/Arm.lean`): it finalizes the inner state with SHA-1's
-verified streaming `finalize`, then computes the outer hash as one call of
-SHA-1's verified compression function (`vg_sha1_compress`), on a block laid
-out at fixed offsets in `scratch`. It pushes 8 bytes of stack (the stack
-arguments of `finalize`); `stack` is that of the shared contract, 16 bytes.
+`finalize` finalizes the inner state with SHA-1's verified streaming
+`finalize`, then computes the outer hash as one call of SHA-1's verified
+compression function (`vg_sha1_compress`), on a block laid out at fixed
+offsets in `scratch`. It pushes 8 bytes of stack (the stack arguments of
+`finalize`); `stack` is that of the shared contract, 16 bytes.
 -/
 
 namespace VG.Artifacts.HmacSha1.Arm
 
-open VG.Proof.Hmac.Generic.Arm
-
 def artifacts : List Artifact := [
   { Spec.Hmac.sha1I.initApi with
     target := Arm.target
     doc := Spec.Hmac.sha1I.initApi.doc
-    code := sha1H.init
+    code := Proof.Pbkdf2.Md.Arm.sha1Md.hmacInit
     contract := Spec.Hmac.sha1I.initContract Arm.abi 16
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     stack := 16
-    verified := Instances.sha1_init
+    verified := Proof.Pbkdf2.Md.Arm.Instances.sha1_init
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
   { Spec.Hmac.sha1I.finalizeApi with
     target := Arm.target

lean/VerifiedGarbage/Artifacts/HmacSha1/X86.lean

@@ -1,33 +1,32 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Hmac.Generic.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 
 /-!
 # HMAC-SHA-1 (RFC 2104) on x86
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-1's verified `init` and `update`.
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/X86.lean`): it calls SHA-1's verified streaming `finalize`
-for the inner hash, then computes the outer hash with one call of SHA-1's
-verified compression function, on a block it lays out word by word in
-`scratch`: the outer key's hash value, the inner digest, its padding and
-length.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`). `init` sets both states' hash values with SHA-1's
+verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word by word
+into their buffers, and absorbs each with one call of SHA-1's verified
+compression function.
+
+`finalize` calls SHA-1's verified streaming `finalize` for the inner hash,
+then computes the outer hash with one call of SHA-1's verified compression
+function, on a block it lays out word by word in `scratch`: the outer key's
+hash value, the inner digest, its padding and length.
 -/
 
 namespace VG.Artifacts.HmacSha1.X86
 
-open VG.Proof.Hmac.Generic.X86
-
 def artifacts : List Artifact := [
   { Spec.Hmac.sha1I.initApi with
     target := X86.target
     doc := Spec.Hmac.sha1I.initApi.doc
-    code := sha1H.init
+    code := Proof.Pbkdf2.Md.X86.sha1M.hmacInit
     contract := Spec.Hmac.sha1I.initContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     stack := 48
-    verified := Instances.sha1_init
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha1_init
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.sha1I.finalizeApi with
     target := X86.target

lean/VerifiedGarbage/Artifacts/HmacSha224/Arm.lean

@@ -4,32 +4,31 @@ import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Sha224
 /-!
 # HMAC-SHA-224 (RFC 2104) on ARMv7
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/Arm.lean`), calling SHA-224's verified streaming `init`
-and SHA-256's `update`.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/Arm.lean`). `init` sets both states' hash values with
+SHA-224's verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word
+by word into their buffers, and absorbs each with one call of SHA-256's
+verified compression function (`vg_sha256_compress`).
 
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/Arm.lean`): it finalizes the inner state with SHA-256's
-verified streaming `finalize`, then computes the outer hash as one call of
-SHA-256's verified compression function (`vg_sha256_compress`), on a block
-laid out at fixed offsets in `scratch`. It pushes 8 bytes of stack (the stack
-arguments of `finalize`); `stack` is that of the shared contract, 16 bytes.
+`finalize` finalizes the inner state with SHA-256's verified streaming
+`finalize`, then computes the outer hash as one call of SHA-256's verified
+compression function (`vg_sha256_compress`), on a block laid out at fixed
+offsets in `scratch`. It pushes 8 bytes of stack (the stack arguments of
+`finalize`); `stack` is that of the shared contract, 16 bytes.
 -/
 
 namespace VG.Artifacts.HmacSha224.Arm
 
-open VG.Proof.Hmac.Generic.Arm
-
 def artifacts : List Artifact := [
   { Spec.Hmac.sha224I.initApi with
     target := Arm.target
     doc := Spec.Hmac.sha224I.initApi.doc
-    code := sha224H.init
+    code := Proof.Pbkdf2.Md.Arm.sha224Md.hmacInit
     contract := Spec.Hmac.sha224I.initContract Arm.abi 16
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     writeArgs := true
     stack := 16
-    verified := Instances.sha224_init
+    verified := Proof.Pbkdf2.Md.Arm.Instances.sha224_init
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
   { Spec.Hmac.sha224I.finalizeApi with
     target := Arm.target

lean/VerifiedGarbage/Artifacts/HmacSha256/Arm.lean

@@ -4,32 +4,31 @@ import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Sha256
 /-!
 # HMAC-SHA-256 (RFC 2104) on ARMv7
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/Arm.lean`), calling SHA-256's verified streaming `init`
-and `update`.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/Arm.lean`). `init` sets both states' hash values with
+SHA-256's verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word
+by word into their buffers, and absorbs each with one call of SHA-256's
+verified compression function.
 
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/Arm.lean`): it finalizes the inner state with SHA-256's
-verified streaming `finalize`, then computes the outer hash as one call of
-SHA-256's verified compression function (`vg_sha256_compress`), on a block
-laid out at fixed offsets in `scratch`. It pushes 8 bytes of stack (the stack
-arguments of `finalize`); `stack` is that of the shared contract, 16 bytes.
+`finalize` finalizes the inner state with SHA-256's verified streaming
+`finalize`, then computes the outer hash as one call of SHA-256's verified
+compression function (`vg_sha256_compress`), on a block laid out at fixed
+offsets in `scratch`. It pushes 8 bytes of stack (the stack arguments of
+`finalize`); `stack` is that of the shared contract, 16 bytes.
 -/
 
 namespace VG.Artifacts.HmacSha256.Arm
 
-open VG.Proof.Hmac.Generic.Arm
-
 def artifacts : List Artifact := [
   { Spec.Hmac.sha256I.initApi with
     target := Arm.target
     doc := Spec.Hmac.sha256I.initApi.doc
-    code := sha256H.init
+    code := Proof.Pbkdf2.Md.Arm.sha256Md.hmacInit
     contract := Spec.Hmac.sha256I.initContract Arm.abi 16
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     writeArgs := true
     stack := 16
-    verified := Instances.sha256_init
+    verified := Proof.Pbkdf2.Md.Arm.Instances.sha256_init
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
   { Spec.Hmac.sha256I.finalizeApi with
     target := Arm.target

lean/VerifiedGarbage/Artifacts/HmacSha384/Arm.lean

@@ -4,31 +4,30 @@ import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Instances
 /-!
 # HMAC-SHA-384 (RFC 2104) on ARMv7
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/Arm.lean`), calling SHA-384's verified streaming `init`
-and `update`.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/Arm.lean`). `init` sets both states' hash values with
+SHA-384's verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word
+by word into their buffers, and absorbs each with one call of SHA-384's
+verified compression function.
 
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/Arm.lean`): it finalizes the inner state with SHA-384's
-verified streaming `finalize`, then computes the outer hash as one call of
-SHA-512's verified compression function (`vg_sha512_compress`), on a block
-laid out at fixed offsets in `scratch`. It pushes 8 bytes of stack (the stack
-arguments of `finalize`); `stack` is that of the shared contract, 16 bytes.
+`finalize` finalizes the inner state with SHA-384's verified streaming
+`finalize`, then computes the outer hash as one call of SHA-512's verified
+compression function (`vg_sha512_compress`), on a block laid out at fixed
+offsets in `scratch`. It pushes 8 bytes of stack (the stack arguments of
+`finalize`); `stack` is that of the shared contract, 16 bytes.
 -/
 
 namespace VG.Artifacts.HmacSha384.Arm
 
-open VG.Proof.Hmac.Generic.Arm
-
 def artifacts : List Artifact := [
   { Spec.Hmac.sha384I.initApi with
     target := Arm.target
     doc := Spec.Hmac.sha384I.initApi.doc
-    code := sha384H.init
+    code := Proof.Pbkdf2.Md.Arm.sha384Md.hmacInit
     contract := Spec.Hmac.sha384I.initContract Arm.abi 16
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     stack := 16
-    verified := Instances.sha384_init
+    verified := Proof.Pbkdf2.Md.Arm.Instances.sha384_init
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
   { Spec.Hmac.sha384I.finalizeApi with
     target := Arm.target

lean/VerifiedGarbage/Artifacts/HmacSha384/X86.lean

@@ -1,33 +1,32 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Hmac.Generic.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 
 /-!
 # HMAC-SHA-384 (RFC 2104) on x86
 
-`init` is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-384's verified `init` and `update`.
-`finalize` is the one for every Merkle–Damgård hash function
-(`Impl/Pbkdf2/Md/X86.lean`): it calls SHA-384's verified streaming `finalize`
-for the inner hash, then computes the outer hash with one call of SHA-384's
-verified compression function, on a block it lays out word by word in
-`scratch`: the outer key's hash value, the inner digest, its padding and
-length.
+`init` and `finalize` are the ones for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`). `init` sets both states' hash values with
+SHA-384's verified streaming `init`, writes `K₀ ⊕ ipad` and `K₀ ⊕ opad` word
+by word into their buffers, and absorbs each with one call of SHA-384's
+verified compression function.
+
+`finalize` calls SHA-384's verified streaming `finalize` for the inner hash,
+then computes the outer hash with one call of SHA-384's verified compression
+function, on a block it lays out word by word in `scratch`: the outer key's
+hash value, the inner digest, its padding and length.
 -/
 
 namespace VG.Artifacts.HmacSha384.X86
 
-open VG.Proof.Hmac.Generic.X86
-
 def artifacts : List Artifact := [
   { Spec.Hmac.sha384I.initApi with
     target := X86.target
     doc := Spec.Hmac.sha384I.initApi.doc
-    code := sha384H.init
+    code := Proof.Pbkdf2.Md.X86.sha384M.hmacInit
     contract := Spec.Hmac.sha384I.initContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
     stack := 48
-    verified := Instances.sha384_init
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha384_init
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.sha384I.finalizeApi with
     target := X86.target