HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 on ARMv7 and x86: the generic contracts and code

lean/VerifiedGarbage/Artifacts/HmacSha256/Arm.lean

@@ -1,25 +1,45 @@
 import VerifiedGarbage.TCB.Arm.Target
-import VerifiedGarbage.Proof.Hmac.Arm.Finalize
-import VerifiedGarbage.Proof.Hmac.Arm.Init
+import VerifiedGarbage.Proof.Pbkdf2.Md.Arm.Sha256
 
-/-! # HMAC-SHA-256 (RFC 2104) on ARMv7 -/
+/-!
+# 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`.
+
+`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.
+-/
 
 namespace VG.Artifacts.HmacSha256.Arm
 
+open VG.Proof.Hmac.Generic.Arm
+
 def artifacts : List Artifact := [
-  { Spec.Hmac.initSha256Api with
+  { Spec.Hmac.sha256I.initApi with
     target := Arm.target
-    doc := Spec.Hmac.initSha256Api.doc
-    code := Impl.Hmac.Arm.init
-    contract := Spec.Hmac.initSha256Contract Arm.abi
-    verified := Proof.Hmac.Arm.Init.init_verified
+    doc := Spec.Hmac.sha256I.initApi.doc
+    code := sha256H.init
+    contract := Spec.Hmac.sha256I.initContract Arm.abi 16
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
+    writeArgs := true
+    stack := 16
+    verified := Instances.sha256_init
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
-  { Spec.Hmac.finalizeSha256OutApi with
+  { Spec.Hmac.sha256I.finalizeApi with
     target := Arm.target
-    doc := Spec.Hmac.finalizeSha256OutApi.doc
-    code := Impl.Hmac.Arm.finalize
-    contract := Spec.Hmac.finalizeSha256OutContract Arm.abi
-    verified := Proof.Hmac.Arm.Finalize.finalize_verified
+    doc := Spec.Hmac.sha256I.finalizeApi.doc
+    code := Proof.Pbkdf2.Md.Arm.sha256Md.hmacFin
+    contract := Spec.Hmac.sha256I.finalizeContract Arm.abi 16
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
+    writeArgs := true
+    stack := 16
+    verified := Proof.Pbkdf2.Md.Arm.Instances.sha256_finalize
     spSafe := Code.all_of_forall (fun _ => rfl) _ }]
 
 end VG.Artifacts.HmacSha256.Arm

lean/VerifiedGarbage/Artifacts/Pbkdf2Sha256/Arm.lean

@@ -1,29 +1,34 @@
 import VerifiedGarbage.TCB.Arm.Target
-import VerifiedGarbage.Impl.Pbkdf2.Arm
-import VerifiedGarbage.Proof.Pbkdf2.Arm.Iterate
-import VerifiedGarbage.Proof.Pbkdf2.Arm.Lit
 import VerifiedGarbage.Proof.Pbkdf2.Whole.Arm.Sha256
 
 /-!
-# PBKDF2-HMAC-SHA-256 (RFC 8018) on 32-bit ARM: the iteration and the whole derivation
+# PBKDF2-HMAC-SHA-256 (RFC 8018) on ARMv7: the iteration and the whole derivation
+
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/Arm.lean`): each step is two calls of SHA-256's verified
+compression function (`vg_sha256_compress`), on blocks laid out once at fixed
+offsets in `scratch`. It uses no stack; `stack` is that of the shared
+contract, 16 bytes.
 
 The whole derivation, `pbkdf2`, is the one for every streaming hash function
-(`Impl/Pbkdf2/Whole/Arm.lean`), calling SHA-256's streaming functions,
-HMAC-SHA-256's `init` and `finalize` and the iteration above, which use no
-stack. Its `stack` is that of the shared contract: 24 bytes (it pushes up to
-16).
+(`Impl/Pbkdf2/Whole/Arm.lean`), calling the hash function's streaming
+functions, HMAC's `init` and `finalize` and the iteration above. `stack` is
+that of the shared contract, 24 bytes: `pbkdf2` pushes `update`'s 16 bytes of
+stack arguments, or 8 bytes around a call of a function that uses 16.
 -/
 
 namespace VG.Artifacts.Pbkdf2Sha256.Arm
 
 def artifacts : List Artifact := [
-  { Spec.Pbkdf2.iterateSha256Api with
+  { Spec.Hmac.sha256I.iterateApi with
     target := Arm.target
-    doc := Spec.Pbkdf2.iterateSha256Api.doc
-      (notes := ["The function uses no stack: it saves its return address in `scratch`."])
-    code := Impl.Pbkdf2.Arm.iterate
-    contract := Spec.Pbkdf2.iterateSha256Contract Arm.abi
-    verified := Proof.Pbkdf2.Arm.iterate_verified
+    doc := Spec.Hmac.sha256I.iterateApi.doc
+    code := Proof.Pbkdf2.Md.Arm.sha256Md.iterate
+    contract := Spec.Hmac.sha256I.iterateContract Arm.abi 16
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
+    writeArgs := true
+    stack := 16
+    verified := Proof.Pbkdf2.Md.Arm.Instances.sha256_iterate
     spSafe := Code.all_of_forall (fun _ => rfl) _ },
   { Spec.Hmac.sha256I.pbkdf2Api with
     target := Arm.target

lean/VerifiedGarbage/Generic/Sha256/X86/Hmac.lean

@@ -1,29 +1,42 @@
 import VerifiedGarbage.TCB.X86.Target
 import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface
 
-/-! Generic hmac registrations for every x86 SHA-256 backend. -/
+/-!
+# HMAC-SHA-256 (RFC 2104) on x86, for every x86 SHA-256 backend
+
+`init` is the one HMAC implementation for every streaming hash function
+(`Impl/Hmac/Generic/X86.lean`), calling SHA-256's verified streaming `init`
+and the backend's `update`. `finalize` is the one for every Merkle–Damgård
+hash function (`Impl/Pbkdf2/Md/X86.lean`): it calls the backend's verified
+streaming `finalize` for the inner hash, then computes the outer hash with one
+call of the backend'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.Generic.Sha256.X86.Hmac
 
 def artifacts (v : Proof.Sha256.X86.Variants.Backend) : List Artifact := [
-  { Spec.Hmac.initSha256Api with
-    name := Spec.Hmac.initSha256Api.name ++ v.suffix
+  { Spec.Hmac.sha256I.initApi with
+    name := Spec.Hmac.sha256I.initApi.name ++ v.suffix
     target := X86.target
-    doc := Spec.Hmac.initSha256Api.doc
-    code := Impl.Hmac.Sha256.X86.init v.cmpN v.cmpC
-    contract := Spec.Hmac.initSha256Contract X86.abi 20
-    stack := 20
-    verified := Proof.Hmac.Sha256.X86.Init.verified v.cmp v.cmpSp v.cmpStack v.initCt
+    doc := Spec.Hmac.sha256I.initApi.doc
+    code := v.H.init
+    contract := Spec.Hmac.sha256I.initContract X86.abi 48
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.initContract; rfl⟩
+    stack := 48
+    verified := v.hmacInit
     spSafe := v.initSp
     features := v.features },
-  { Spec.Hmac.finalizeSha256OutApi with
-    name := Spec.Hmac.finalizeSha256OutApi.name ++ v.suffix
+  { Spec.Hmac.sha256I.finalizeApi with
+    name := Spec.Hmac.sha256I.finalizeApi.name ++ v.suffix
     target := X86.target
-    doc := Spec.Hmac.finalizeSha256OutApi.doc
-    code := Impl.Hmac.Sha256.X86.finalize v.cmpN v.cmpC
-    contract := Spec.Hmac.finalizeSha256OutContract X86.abi 20
-    stack := 20
-    verified := Proof.Hmac.Sha256.X86.Finalize.verified v.cmp v.cmpSp v.cmpStack v.finHashSp v.finHashStack v.finCt
+    doc := Spec.Hmac.sha256I.finalizeApi.doc
+    code := v.M.hmacFin
+    contract := Spec.Hmac.sha256I.finalizeContract X86.abi 48
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
+    stack := 48
+    verified := v.hmacFin
     spSafe := v.finSp
     features := v.features }]
 

lean/VerifiedGarbage/Generic/Sha256/X86/Pbkdf2.lean

@@ -3,32 +3,41 @@ import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface
 import VerifiedGarbage.Proof.Pbkdf2.Whole.X86.Sha256
 
 /-!
-Generic PBKDF2 registrations for every x86 SHA-256 backend: the iteration,
-and the whole derivation (`Impl/Pbkdf2/Whole/X86.lean`), which calls the
-backend's streaming, HMAC and PBKDF2 functions (`Proof.Pbkdf2.Whole.X86.sha256Fns`).
-`stack` is that of the shared contracts: 76 bytes for `pbkdf2`, which pushes
-up to 24 bytes of arguments for the functions it calls, and their return
-address, and gives them 48.
+# PBKDF2-HMAC-SHA-256 (RFC 8018) on x86, for every x86 SHA-256 backend: the iteration and the whole derivation
+
+The iteration is the one for every Merkle–Damgård hash function
+(`Impl/Pbkdf2/Md/X86.lean`): each step is two calls of the backend'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 backend's streaming functions,
+HMAC's `init` and `finalize` and the iteration above, made with the backend.
+`stack` is that of the shared contracts: 48 bytes for the iteration, and 76
+for `pbkdf2`, which pushes up to 24 bytes of arguments for the functions it
+calls, and their return address, and gives them 48.
 -/
+
 namespace VG.Generic.Sha256.X86.Pbkdf2
 
 def artifacts (v : Proof.Sha256.X86.Variants.Backend) : List Artifact := [
-  { Spec.Pbkdf2.iterateSha256Api with
-    name := Spec.Pbkdf2.iterateSha256Api.name ++ v.suffix
+  { Spec.Hmac.sha256I.iterateApi with
+    name := Spec.Hmac.sha256I.iterateApi.name ++ v.suffix
     target := X86.target
-    doc := Spec.Pbkdf2.iterateSha256Api.doc
-    code := Impl.Pbkdf2.Sha256.X86.iterate v.cmpN v.cmpC
-    contract := Spec.Pbkdf2.iterateSha256Contract X86.abi 20
-    writeArgs := true
-    stack := 20
-    verified := Proof.Pbkdf2.Sha256.X86.verified v.cmp v.cmpSp v.cmpStack v.iterCt
+    doc := Spec.Hmac.sha256I.iterateApi.doc
+    code := v.M.iterate
+    contract := Spec.Hmac.sha256I.iterateContract X86.abi 48
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
+    stack := 48
+    verified := v.iterate
     spSafe := v.iterSp
     features := v.features },
   { Spec.Hmac.sha256I.pbkdf2Api with
     name := Spec.Hmac.sha256I.pbkdf2Api.name ++ v.suffix
     target := X86.target
     doc := Spec.Hmac.sha256I.pbkdf2Api.doc
-    code := (Proof.Pbkdf2.Whole.X86.sha256FnsOf v).pbkdf2
+    code := v.F.pbkdf2
     contract := Spec.Hmac.sha256I.pbkdf2Contract X86.abi 76
     ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.pbkdf2Contract; rfl⟩
     stack := 76