HMAC finalize and PBKDF2 iterate on x86 call the compression function

lean/VerifiedGarbage/Artifacts/HmacMd5/X86.lean

@@ -1,12 +1,18 @@
 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
 
-The code is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling MD5's verified `init`, `update`
-and `finalize`.
+`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.
 -/
 
 namespace VG.Artifacts.HmacMd5.X86
@@ -26,11 +32,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.md5I.finalizeApi with
     target := X86.target
     doc := Spec.Hmac.md5I.finalizeApi.doc
-    code := md5H.finalize
+    code := Proof.Pbkdf2.Md.X86.md5M.hmacFin
     contract := Spec.Hmac.md5I.finalizeContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
     stack := 48
-    verified := Instances.md5_finalize
+    verified := Proof.Pbkdf2.Md.X86.Instances.md5_finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.HmacMd5.X86

lean/VerifiedGarbage/Artifacts/HmacSha1/X86.lean

@@ -1,12 +1,18 @@
 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
 
-The code is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-1's verified `init`, `update`
-and `finalize`.
+`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.
 -/
 
 namespace VG.Artifacts.HmacSha1.X86
@@ -26,11 +32,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha1I.finalizeApi with
     target := X86.target
     doc := Spec.Hmac.sha1I.finalizeApi.doc
-    code := sha1H.finalize
+    code := Proof.Pbkdf2.Md.X86.sha1M.hmacFin
     contract := Spec.Hmac.sha1I.finalizeContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
     stack := 48
-    verified := Instances.sha1_finalize
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha1_finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.HmacSha1.X86

lean/VerifiedGarbage/Artifacts/HmacSha384/X86.lean

@@ -1,12 +1,18 @@
 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
 
-The code is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-384's verified `init`, `update`
-and `finalize`.
+`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.
 -/
 
 namespace VG.Artifacts.HmacSha384.X86
@@ -26,11 +32,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha384I.finalizeApi with
     target := X86.target
     doc := Spec.Hmac.sha384I.finalizeApi.doc
-    code := sha384H.finalize
+    code := Proof.Pbkdf2.Md.X86.sha384M.hmacFin
     contract := Spec.Hmac.sha384I.finalizeContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
     stack := 48
-    verified := Instances.sha384_finalize
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha384_finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.HmacSha384.X86

lean/VerifiedGarbage/Artifacts/HmacSha512/X86.lean

@@ -1,12 +1,18 @@
 import VerifiedGarbage.TCB.X86.Target
 import VerifiedGarbage.Proof.Hmac.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 
 /-!
 # HMAC-SHA-512 (RFC 2104) on x86
 
-The code is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-512's verified `init`, `update`
-and `finalize`.
+`init` is the one HMAC implementation for every streaming hash function
+(`Impl/Hmac/Generic/X86.lean`), calling SHA-512's verified `init` and `update`.
+`finalize` is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): it calls SHA-512's verified streaming `finalize`
+for the inner hash, then computes the outer hash with one call of SHA-512'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.HmacSha512.X86
@@ -26,11 +32,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha512I.finalizeApi with
     target := X86.target
     doc := Spec.Hmac.sha512I.finalizeApi.doc
-    code := sha512H'.finalize
+    code := Proof.Pbkdf2.Md.X86.sha512M'.hmacFin
     contract := Spec.Hmac.sha512I.finalizeContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
     stack := 48
-    verified := Instances.sha512_finalize
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha512_finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.HmacSha512.X86

lean/VerifiedGarbage/Artifacts/HmacSha512_224/X86.lean

@@ -1,12 +1,18 @@
 import VerifiedGarbage.TCB.X86.Target
 import VerifiedGarbage.Proof.Hmac.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 
 /-!
 # HMAC-SHA-512/224 (RFC 2104) on x86
 
-The code is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-512/224's verified `init`, `update`
-and `finalize`.
+`init` is the one HMAC implementation for every streaming hash function
+(`Impl/Hmac/Generic/X86.lean`), calling SHA-512/224's verified `init` and `update`.
+`finalize` is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): it calls SHA-512/224's verified streaming `finalize`
+for the inner hash, then computes the outer hash with one call of SHA-512/224'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.HmacSha512_224.X86
@@ -26,11 +32,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha512_224I.finalizeApi with
     target := X86.target
     doc := Spec.Hmac.sha512_224I.finalizeApi.doc
-    code := sha512_224H.finalize
+    code := Proof.Pbkdf2.Md.X86.sha512_224M.hmacFin
     contract := Spec.Hmac.sha512_224I.finalizeContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
     stack := 48
-    verified := Instances.sha512_224_finalize
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha512_224_finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.HmacSha512_224.X86

lean/VerifiedGarbage/Artifacts/HmacSha512_256/X86.lean

@@ -1,12 +1,18 @@
 import VerifiedGarbage.TCB.X86.Target
 import VerifiedGarbage.Proof.Hmac.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 
 /-!
 # HMAC-SHA-512/256 (RFC 2104) on x86
 
-The code is the one HMAC implementation for every streaming hash function
-(`Impl/Hmac/Generic/X86.lean`), calling SHA-512/256's verified `init`, `update`
-and `finalize`.
+`init` is the one HMAC implementation for every streaming hash function
+(`Impl/Hmac/Generic/X86.lean`), calling SHA-512/256's verified `init` and `update`.
+`finalize` is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): it calls SHA-512/256's verified streaming `finalize`
+for the inner hash, then computes the outer hash with one call of SHA-512/256'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.HmacSha512_256.X86
@@ -26,11 +32,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha512_256I.finalizeApi with
     target := X86.target
     doc := Spec.Hmac.sha512_256I.finalizeApi.doc
-    code := sha512_256H.finalize
+    code := Proof.Pbkdf2.Md.X86.sha512_256M.hmacFin
     contract := Spec.Hmac.sha512_256I.finalizeContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
     stack := 48
-    verified := Instances.sha512_256_finalize
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha512_256_finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.HmacSha512_256.X86

lean/VerifiedGarbage/Artifacts/Pbkdf2Md5/X86.lean

@@ -1,13 +1,15 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Pbkdf2.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Whole.X86.Instances
 
 /-!
 # PBKDF2-HMAC-MD5 (RFC 8018) on x86: the iteration and the whole derivation
 
-The code is the one PBKDF2 iteration for every streaming hash function
-(`Impl/Pbkdf2/Generic/X86.lean`), calling MD5's verified `update` and
-`finalize`.
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): each step is two calls of MD5's verified
+compression function, on a block laid out once, word by word, in `scratch`
+(`U`, its padding and length), starting from the key's inner and outer hash
+values.
 
 The whole derivation, `pbkdf2`, is the one for every streaming hash function
 (`Impl/Pbkdf2/Whole/X86.lean`), calling the hash function's streaming
@@ -25,11 +27,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.md5I.iterateApi with
     target := X86.target
     doc := Spec.Hmac.md5I.iterateApi.doc
-    code := Impl.Pbkdf2.Generic.X86.iterate md5H
+    code := Proof.Pbkdf2.Md.X86.md5M.iterate
     contract := Spec.Hmac.md5I.iterateContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
     stack := 48
-    verified := Proof.Pbkdf2.Generic.X86.Instances.md5
+    verified := Proof.Pbkdf2.Md.X86.Instances.md5_iterate
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.md5I.pbkdf2Api with
     target := X86.target

lean/VerifiedGarbage/Artifacts/Pbkdf2Sha1/X86.lean

@@ -1,13 +1,15 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Pbkdf2.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Whole.X86.Instances
 
 /-!
 # PBKDF2-HMAC-SHA-1 (RFC 8018) on x86: the iteration and the whole derivation
 
-The code is the one PBKDF2 iteration for every streaming hash function
-(`Impl/Pbkdf2/Generic/X86.lean`), calling SHA-1's verified `update` and
-`finalize`.
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): each step is two calls of SHA-1's verified
+compression function, on a block laid out once, word by word, in `scratch`
+(`U`, its padding and length), starting from the key's inner and outer hash
+values.
 
 The whole derivation, `pbkdf2`, is the one for every streaming hash function
 (`Impl/Pbkdf2/Whole/X86.lean`), calling the hash function's streaming
@@ -25,11 +27,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha1I.iterateApi with
     target := X86.target
     doc := Spec.Hmac.sha1I.iterateApi.doc
-    code := Impl.Pbkdf2.Generic.X86.iterate sha1H
+    code := Proof.Pbkdf2.Md.X86.sha1M.iterate
     contract := Spec.Hmac.sha1I.iterateContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
     stack := 48
-    verified := Proof.Pbkdf2.Generic.X86.Instances.sha1
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha1_iterate
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.sha1I.pbkdf2Api with
     target := X86.target

lean/VerifiedGarbage/Artifacts/Pbkdf2Sha384/X86.lean

@@ -1,13 +1,15 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Pbkdf2.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Whole.X86.Instances
 
 /-!
 # PBKDF2-HMAC-SHA-384 (RFC 8018) on x86: the iteration and the whole derivation
 
-The code is the one PBKDF2 iteration for every streaming hash function
-(`Impl/Pbkdf2/Generic/X86.lean`), calling SHA-384's verified `update` and
-`finalize`.
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): each step is two calls of SHA-384's verified
+compression function, on a block laid out once, word by word, in `scratch`
+(`U`, its padding and length), starting from the key's inner and outer hash
+values.
 
 The whole derivation, `pbkdf2`, is the one for every streaming hash function
 (`Impl/Pbkdf2/Whole/X86.lean`), calling the hash function's streaming
@@ -25,11 +27,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha384I.iterateApi with
     target := X86.target
     doc := Spec.Hmac.sha384I.iterateApi.doc
-    code := Impl.Pbkdf2.Generic.X86.iterate sha384H
+    code := Proof.Pbkdf2.Md.X86.sha384M.iterate
     contract := Spec.Hmac.sha384I.iterateContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
     stack := 48
-    verified := Proof.Pbkdf2.Generic.X86.Instances.sha384
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha384_iterate
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.sha384I.pbkdf2Api with
     target := X86.target

lean/VerifiedGarbage/Artifacts/Pbkdf2Sha512/X86.lean

@@ -1,13 +1,15 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Pbkdf2.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Whole.X86.Instances
 
 /-!
 # PBKDF2-HMAC-SHA-512 (RFC 8018) on x86: the iteration and the whole derivation
 
-The code is the one PBKDF2 iteration for every streaming hash function
-(`Impl/Pbkdf2/Generic/X86.lean`), calling SHA-512's verified `update` and
-`finalize`.
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): each step is two calls of SHA-512's verified
+compression function, on a block laid out once, word by word, in `scratch`
+(`U`, its padding and length), starting from the key's inner and outer hash
+values.
 
 The whole derivation, `pbkdf2`, is the one for every streaming hash function
 (`Impl/Pbkdf2/Whole/X86.lean`), calling the hash function's streaming
@@ -25,11 +27,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha512I.iterateApi with
     target := X86.target
     doc := Spec.Hmac.sha512I.iterateApi.doc
-    code := Impl.Pbkdf2.Generic.X86.iterate sha512H'
+    code := Proof.Pbkdf2.Md.X86.sha512M'.iterate
     contract := Spec.Hmac.sha512I.iterateContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
     stack := 48
-    verified := Proof.Pbkdf2.Generic.X86.Instances.sha512
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha512_iterate
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.sha512I.pbkdf2Api with
     target := X86.target

lean/VerifiedGarbage/Artifacts/Pbkdf2Sha512_224/X86.lean

@@ -1,13 +1,15 @@
 import VerifiedGarbage.TCB.X86.Target
-import VerifiedGarbage.Proof.Pbkdf2.Generic.X86.Instances
+import VerifiedGarbage.Proof.Pbkdf2.Md.X86.Instances
 import VerifiedGarbage.Proof.Pbkdf2.Whole.X86.Instances
 
 /-!
 # PBKDF2-HMAC-SHA-512/224 (RFC 8018) on x86: the iteration and the whole derivation
 
-The code is the one PBKDF2 iteration for every streaming hash function
-(`Impl/Pbkdf2/Generic/X86.lean`), calling SHA-512/224's verified `update` and
-`finalize`.
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): each step is two calls of SHA-512/224's verified
+compression function, on a block laid out once, word by word, in `scratch`
+(`U`, its padding and length), starting from the key's inner and outer hash
+values.
 
 The whole derivation, `pbkdf2`, is the one for every streaming hash function
 (`Impl/Pbkdf2/Whole/X86.lean`), calling the hash function's streaming
@@ -25,11 +27,11 @@ def artifacts : List Artifact := [
   { Spec.Hmac.sha512_224I.iterateApi with
     target := X86.target
     doc := Spec.Hmac.sha512_224I.iterateApi.doc
-    code := Impl.Pbkdf2.Generic.X86.iterate sha512_224H
+    code := Proof.Pbkdf2.Md.X86.sha512_224M.iterate
     contract := Spec.Hmac.sha512_224I.iterateContract X86.abi 48
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
     stack := 48
-    verified := Proof.Pbkdf2.Generic.X86.Instances.sha512_224
+    verified := Proof.Pbkdf2.Md.X86.Instances.sha512_224_iterate
     spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Hmac.sha512_224I.pbkdf2Api with
     target := X86.target