Make x86 SHA-256 constructions generic over compression backends

ci/bench_arches.py

@@ -47,7 +47,7 @@
     "arm": {
         "os": "ubuntu-24.04-arm",
         "image": "ghcr.io/pyca/cryptography-runner-ubuntu-rolling:armv7l",
-        "options": "--env RUSTUP_HOME=/root/.rustup",
+        "options": "--env RUSTUP_HOME=/tmp/verified-garbage-rustup",
     },
 }
 

lean/VerifiedGarbage/Artifacts/Sha256/X86.lean

@@ -17,35 +17,12 @@ against the contract.
 namespace VG.Artifacts.Sha256.X86
 
 def artifacts : List Artifact := [
-  { Spec.Sha256.compressApi with
-    target := X86.target
-    doc := Spec.Sha256.compressApi.doc
-    code := Impl.Sha256.X86.compress
-    contract := Spec.Sha256.compressContract X86.abi
-    verified := Proof.Sha256.X86.Shared.compress
-    spSafe := Code.all_of_allInstrs (by lit_decide) },
   { Spec.Sha256.initApi with
     target := X86.target
     doc := Spec.Sha256.initApi.doc
     code := Impl.Sha256.X86.Stream.init
     contract := Spec.Sha256.initContract X86.abi
     verified := Proof.Sha256.X86.Shared.init
-    spSafe := Code.all_of_allInstrs (by lit_decide) },
-  { Spec.Sha256.updateApi with
-    target := X86.target
-    doc := Spec.Sha256.updateApi.doc
-    code := Impl.Sha256.X86.Stream.update
-    contract := Spec.Sha256.updateContract X86.abi 20
-    stack := 20
-    verified := Proof.Sha256.X86.Shared.update
-    spSafe := Code.all_of_allInstrs (by lit_decide) },
-  { Spec.Sha256.finalizeApi with
-    target := X86.target
-    doc := Spec.Sha256.finalizeApi.doc
-    code := Impl.Sha256.X86.Stream.finalize
-    contract := Spec.Sha256.finalizeContract X86.abi 20
-    stack := 20
-    verified := Proof.Sha256.X86.Shared.finalize
     spSafe := Code.all_of_allInstrs (by lit_decide) }]
 
 end VG.Artifacts.Sha256.X86

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

@@ -0,0 +1,30 @@
+import VerifiedGarbage.TCB.X86.Target
+import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface
+
+/-! Generic hmac registrations for every x86 SHA-256 backend. -/
+
+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
+    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
+    spSafe := v.initSp
+    features := v.features },
+  { Spec.Hmac.finalizeSha256OutApi with
+    name := Spec.Hmac.finalizeSha256OutApi.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
+    spSafe := v.finSp
+    features := v.features }]
+
+end VG.Generic.Sha256.X86.Hmac

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

@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86.Target
+import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface
+
+/-! Generic PBKDF2 iteration registration for every x86 SHA-256 backend. -/
+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
+    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
+    spSafe := v.iterSp
+    features := v.features }]
+
+end VG.Generic.Sha256.X86.Pbkdf2

lean/VerifiedGarbage/Generic/Sha256/X86/Stream.lean

@@ -0,0 +1,22 @@
+import VerifiedGarbage.TCB.X86.Target
+import VerifiedGarbage.Proof.Sha256.X86.Variants.Interface
+
+/-! Generic stream registrations for every x86 SHA-256 backend. -/
+
+namespace VG.Generic.Sha256.X86.Stream
+
+def artifacts (v : Proof.Sha256.X86.Variants.Backend) : List Artifact := v.functions.map fun f =>
+  { f.api with
+    name := f.api.name ++ v.suffix
+    target := X86.target
+    doc := f.api.doc
+    code := f.code
+    contract := f.contract
+    stack := f.stack
+    verified := f.verified
+    ofSig := f.ofSig
+    ofApi := f.ofApi
+    spSafe := f.spSafe
+    features := v.features }
+
+end VG.Generic.Sha256.X86.Stream

lean/VerifiedGarbage/Impl/Hmac/Sha256/X86.lean

@@ -0,0 +1,48 @@
+import VerifiedGarbage.Impl.Hmac.X86
+import VerifiedGarbage.Impl.MdStream.X86
+
+/-! SHA-256's efficient x86 HMAC bodies, generic over compression. -/
+namespace VG.Impl.Hmac.Sha256.X86
+open VG.X86
+open VG.Impl.Sha256.X86 (at_)
+open VG.Impl.Sha256.X86.Stream (save restore)
+open VG.Impl.Hmac.X86 (h0 keyLoop padLoop opadWord bswapWord copyWord padWords)
+
+def compressBuf (name : String) (code : Prog isa) (b : Reg) : Prog isa :=
+  .seq (.block [.mov .eax (.reg b), .alu .add .eax (.imm 32)]) (Impl.MdStream.X86.compressAt name code b .ebp)
+
+def init (name : String) (code : Prog isa) : Prog isa :=
+  .seq (.block ([.mov .eax (.mem (at_ .esp 20))] ++ save .eax ++
+      [.mov .ebp (.reg .eax), .mov .ebx (.mem (at_ .esp 4)), .mov .esi (.mem (at_ .esp 8))] ++
+      h0 .ebx ++ h0 .esi ++
+      [.mov .edi (.mem (at_ .esp 12)), .mov .ecx (.mem (at_ .esp 16)), .mov .edx (.reg .ebx),
+       .alu .add .edx (.imm 32), .alu .test .ecx (.reg .ecx)]))
+  (.seq (.ite .e (.block []) keyLoop)
+  (.seq (.block [.mov .eax (.reg .ebx), .alu .add .eax (.imm 96), .mov .ecx (.imm 0x36),
+      .alu .cmp .edx (.reg .eax)])
+  (.seq (.ite .e (.block []) padLoop)
+  (.seq (.block ((List.range 16).flatMap opadWord))
+  (.seq (compressBuf name code .ebx)
+  (.seq (compressBuf name code .esi)
+    (.block (.mov .eax (.reg .ebp) :: restore .eax))))))))
+
+def finalizeHash (name : String) (code : Prog isa) : Prog isa :=
+  match Impl.MdStream.X86.finalize Impl.Sha256.X86.Stream.params name code with
+  | .seq a (.seq b (.seq c _)) => .seq a (.seq b c)
+  | p => p
+
+def finalize (name : String) (code : Prog isa) : Prog isa :=
+  .seq (.block [.mov .edx (.mem (at_ .esp 24)), .mov .ecx (.mem (at_ .esp 8)), .store (at_ .edx 176) .ecx,
+      .mov .ecx (.mem (at_ .esp 12)), .store (at_ .esp 8) .ecx,
+      .mov .ecx (.mem (at_ .esp 16)), .store (at_ .esp 12) .ecx,
+      .mov .ecx (.mem (at_ .esp 20)), .store (at_ .esp 16) .ecx, .store (at_ .esp 20) .edx])
+  (.seq (finalizeHash name code)
+  -- The inner digest into the inner buffer, and the outer hash value into the inner state.
+  (.seq (.block ((List.range 8).flatMap (bswapWord .ebx .ebx 0 32) ++ .mov .edx (.mem (at_ .ebp 176)) ::
+      (List.range 8).flatMap (copyWord .edx .ebx 0 0) ++ padWords ++
+      [.mov .eax (.reg .ebx), .alu .add .eax (.imm 32)]))
+  (.seq (Impl.MdStream.X86.compressAt name code .ebx .ebp)
+    (.block (.mov .eax (.mem (at_ .ebp 136)) :: (List.range 8).flatMap (bswapWord .ebx .eax 0 0) ++
+      .mov .eax (.reg .ebp) :: restore .eax)))))
+
+end VG.Impl.Hmac.Sha256.X86

lean/VerifiedGarbage/Impl/Pbkdf2/Sha256/X86.lean

@@ -0,0 +1,20 @@
+import VerifiedGarbage.Impl.Pbkdf2.X86
+import VerifiedGarbage.Impl.MdStream.X86
+
+/-! PBKDF2-SHA-256's two-compression iteration, generic over compression. -/
+namespace VG.Impl.Pbkdf2.Sha256.X86
+open VG.X86
+open VG.Impl.Pbkdf2.X86 (load atBlock digest xorW prologue epilogue)
+
+def body (name : String) (code : Prog isa) : Prog isa :=
+  .seq (.block (load 0 ++ atBlock))
+  (.seq (Impl.MdStream.X86.compressAt name code .ebx .ebp)
+  (.seq (.block (digest ++ load 96 ++ atBlock))
+  (.seq (Impl.MdStream.X86.compressAt name code .ebx .ebp)
+    (.block (digest ++ (List.range 8).flatMap xorW ++ [.alu .sub .edi (.imm 1)])))))
+
+def iterate (name : String) (code : Prog isa) : Prog isa :=
+  .seq (.block prologue)
+  (.seq (.ite .e (.block []) (.loop (body name code) .ne)) (.block epilogue))
+
+end VG.Impl.Pbkdf2.Sha256.X86