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

lean/VerifiedGarbage/Artifacts/HmacSha256/Arm.lean

@@ -1,6 +1,5 @@
 import VerifiedGarbage.TCB.Arm.Target
-import VerifiedGarbage.Proof.Hmac.Arm.Finalize
-import VerifiedGarbage.Proof.Hmac.Arm.Init
+import VerifiedGarbage.Proof.Hmac.Generic.Arm.Instances
 
 /-!
 # HMAC-SHA-256 (RFC 2104) on ARMv7
@@ -12,25 +11,36 @@ artifact made from a function's `Api` (in `Spec/`, reviewed with the
 contract) takes them from there, and this file adds only notes on the
 implementation. The emitter adds the `# Safety` items that depend on the
 target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
-against the contract.
+against the contract (after unfolding the `Instance`'s contract to the
+generic one, which is a `Sig.contract`).
+
+The code is the one HMAC implementation for every streaming hash function
+(`Impl/Hmac/Generic/Arm.lean`), calling SHA-256's verified `init`, `update`
+and `finalize`.
 -/
 
 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⟩
+    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 := sha256H.finalize
+    contract := Spec.Hmac.sha256I.finalizeContract Arm.abi 16
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.finalizeContract; rfl⟩
+    stack := 16
+    verified := Instances.sha256_finalize
     spSafe := Code.all_of_forall (fun _ => rfl) _ }]
 
 end VG.Artifacts.HmacSha256.Arm

lean/VerifiedGarbage/Artifacts/Pbkdf2Sha256/Arm.lean

@@ -1,10 +1,8 @@
 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.Generic.Arm.Instances
 
 /-!
-# The PBKDF2-HMAC-SHA-256 iteration (RFC 8018) on 32-bit ARM
+# The PBKDF2-HMAC-SHA-256 iteration (RFC 8018) on ARMv7
 
 A registration file (see `TCB/Emit.lean`): the artifacts it lists are
 emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
@@ -13,19 +11,27 @@ artifact made from a function's `Api` (in `Spec/`, reviewed with the
 contract) takes them from there, and this file adds only notes on the
 implementation. The emitter adds the `# Safety` items that depend on the
 target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
-against the contract.
+against the contract (after unfolding the `Instance`'s contract to the
+generic one, which is a `Sig.contract`).
+
+The code is the one PBKDF2 iteration for every streaming hash function
+(`Impl/Pbkdf2/Generic/Arm.lean`), calling SHA-256's verified `update` and
+`finalize`.
 -/
 
 namespace VG.Artifacts.Pbkdf2Sha256.Arm
 
+open VG.Proof.Hmac.Generic.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 := Impl.Pbkdf2.Generic.Arm.iterate sha256H
+    contract := Spec.Hmac.sha256I.iterateContract Arm.abi 16
+    ofSig := ⟨_, _, _, by unfold Spec.Hmac.Instance.iterateContract; rfl⟩
+    stack := 16
+    verified := Proof.Pbkdf2.Generic.Arm.Instances.sha256
     spSafe := Code.all_of_forall (fun _ => rfl) _ }]
 
 end VG.Artifacts.Pbkdf2Sha256.Arm

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

@@ -1,29 +1,46 @@
 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
+
+A generic file (see `TCB/Emit.lean`): HMAC's `init` and `finalize`, the one
+implementation for every streaming hash function
+(`Impl/Hmac/Generic/X86.lean`), calling SHA-256's streaming functions made
+with the variant's compression function, are emitted once for each variant
+(`Variants/Sha256/X86/`), named with its suffix. **Review note**: `sig` and
+`doc` are trusted, as they tie the Rust caller to the contract; check them
+against the contract's `pre`/`post`. An artifact made from a function's
+`Api` (in `Spec/`, reviewed with the contract) takes them from there. The
+emitter adds the `# Safety` items that depend on the target
+(`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks against
+the contract (after unfolding the `Instance`'s contract to the generic one,
+which is a `Sig.contract`), and the CPU features the implementation needs.
+-/
 
 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.H.finalize
+    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

@@ -1,19 +1,35 @@
 import VerifiedGarbage.TCB.X86.Target
 import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface
 
-/-! Generic PBKDF2 iteration registration for every x86 SHA-256 backend. -/
+/-!
+# The PBKDF2-HMAC-SHA-256 iteration (RFC 8018) on x86
+
+A generic file (see `TCB/Emit.lean`): PBKDF2's `iterate`, the one iteration
+for every streaming hash function (`Impl/Pbkdf2/Generic/X86.lean`), calling
+SHA-256's streaming functions made with the variant's compression function,
+is emitted once for each variant (`Variants/Sha256/X86/`), named with its
+suffix. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there. The emitter adds the `# Safety` items that
+depend on the target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which
+`ofSig` checks against the contract (after unfolding the `Instance`'s
+contract to the generic one, which is a `Sig.contract`), and the CPU
+features the implementation needs.
+-/
+
 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 := Impl.Pbkdf2.Generic.X86.iterate v.H
+    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 }]