Merge pull request #476 from pq-code-package/cbmc-test

CBMC: add `tests cbmc` command
pq-code-package · Dec 3, 2024 · 425bc20 · 425bc20 · oqs-bot · Dec 3, 2024
2 parents 6ce990f + f88eeb6
commit 425bc20
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 2 deletions.
diff --git a/.github/actions/cbmc/action.yml b/.github/actions/cbmc/action.yml
@@ -46,7 +46,6 @@ runs:
       - name: Run CBMC proofs (MLKEM_K=${{ inputs.mlkem_k }})
         shell: ${{ env.SHELL }}
         run: |
-          cd cbmc/proofs;
           echo "::group::cbmc_${{ inputs.mlkem_k }}"
-          MLKEM_K=${{ inputs.mlkem_k }} ./run-cbmc-proofs.py --summarize --no-coverage -j8;
+          tests cbmc --k ${{ inputs.mlkem_k }};
           echo "::endgroup::"
diff --git a/scripts/lib/mlkem_test.py b/scripts/lib/mlkem_test.py
@@ -50,6 +50,7 @@ def __init__(self):
         self.run = True
         self.exec_wrapper = ""
         self.run_as_root = ""
+        self.k = "ALL"
 
 
 class Base:
@@ -709,3 +710,22 @@ def all(opt: bool):
             exit_code = exit_code or all(True)
 
         exit(exit_code)
+
+    def cbmc(self, k):
+        config_logger(self.verbose)
+        def run_cbmc(mlkem_k):
+            envvars = {"MLKEM_K": mlkem_k}
+            cpucount = os.cpu_count()
+            p = subprocess.Popen(
+                ["python3", "run-cbmc-proofs.py", "--summarize",  "--no-coverage", f"-j{cpucount}"],
+                cwd="cbmc/proofs",
+                env=os.environ.copy() | envvars,
+            )
+            p.communicate()
+            assert p.returncode == 0
+        if k == "ALL":
+            run_cbmc("2")
+            run_cbmc("3")
+            run_cbmc("4")
+        else: 
+            run_cbmc(k)
diff --git a/scripts/tests b/scripts/tests
@@ -291,5 +291,28 @@ def all(
     Tests(opts).all(func, kat, nistkat, acvp)
 
 
+@cli.command(
+    short_help="Run the CBMC proofs for all parameter sets",
+    context_settings={"show_default": True},
+)
+@click.make_pass_decorator(Options, ensure=True)
+@add_options(
+    [
+        click.option(
+            "--k",
+            expose_value=False,
+            nargs=1,
+            type=click.Choice(["2", "3", "4", "ALL"]),
+            show_default=True,
+            default="ALL",
+            help="MLKEM parameter set (MLKEM_K).",
+            callback=__callback("k"),
+        )
+    ]
+)
+def cbmc(opts: Options):
+    Tests(opts).cbmc(opts.k)
+
+
 if __name__ == "__main__":
     cli()
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`29175` cycles	`29176` cycles	`1.00`
`ML-KEM-512 encaps`	`35852` cycles	`35851` cycles	`1.00`
`ML-KEM-512 decaps`	`46653` cycles	`46653` cycles	`1`
`ML-KEM-768 keypair`	`49174` cycles	`49177` cycles	`1.00`
`ML-KEM-768 encaps`	`55839` cycles	`55840` cycles	`1.00`
`ML-KEM-768 decaps`	`71008` cycles	`71009` cycles	`1.00`
`ML-KEM-1024 keypair`	`72211` cycles	`72213` cycles	`1.00`
`ML-KEM-1024 encaps`	`81519` cycles	`81523` cycles	`1.00`
`ML-KEM-1024 decaps`	`102032` cycles	`102027` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`18152` cycles	`18207` cycles	`1.00`
`ML-KEM-512 encaps`	`23137` cycles	`23125` cycles	`1.00`
`ML-KEM-512 decaps`	`30396` cycles	`30388` cycles	`1.00`
`ML-KEM-768 keypair`	`31050` cycles	`31088` cycles	`1.00`
`ML-KEM-768 encaps`	`33990` cycles	`33989` cycles	`1.00`
`ML-KEM-768 decaps`	`44804` cycles	`44894` cycles	`1.00`
`ML-KEM-1024 keypair`	`44728` cycles	`44796` cycles	`1.00`
`ML-KEM-1024 encaps`	`50036` cycles	`50021` cycles	`1.00`
`ML-KEM-1024 decaps`	`64742` cycles	`64761` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`15076` cycles	`15070` cycles	`1.00`
`ML-KEM-512 encaps`	`19754` cycles	`19759` cycles	`1.00`
`ML-KEM-512 decaps`	`26413` cycles	`26401` cycles	`1.00`
`ML-KEM-768 keypair`	`25586` cycles	`25738` cycles	`0.99`
`ML-KEM-768 encaps`	`28233` cycles	`28192` cycles	`1.00`
`ML-KEM-768 decaps`	`38203` cycles	`38199` cycles	`1.00`
`ML-KEM-1024 keypair`	`35635` cycles	`35662` cycles	`1.00`
`ML-KEM-1024 encaps`	`41255` cycles	`41237` cycles	`1.00`
`ML-KEM-1024 decaps`	`54608` cycles	`54744` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`20326` cycles	`20325` cycles	`1.00`
`ML-KEM-512 encaps`	`27129` cycles	`27127` cycles	`1.00`
`ML-KEM-512 decaps`	`36210` cycles	`36213` cycles	`1.00`
`ML-KEM-768 keypair`	`34834` cycles	`34857` cycles	`1.00`
`ML-KEM-768 encaps`	`38193` cycles	`38217` cycles	`1.00`
`ML-KEM-768 decaps`	`51360` cycles	`51402` cycles	`1.00`
`ML-KEM-1024 keypair`	`48074` cycles	`48094` cycles	`1.00`
`ML-KEM-1024 encaps`	`54249` cycles	`54247` cycles	`1.00`
`ML-KEM-1024 decaps`	`72137` cycles	`72161` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`13864` cycles	`13918` cycles	`1.00`
`ML-KEM-512 encaps`	`18199` cycles	`18219` cycles	`1.00`
`ML-KEM-512 decaps`	`24094` cycles	`24133` cycles	`1.00`
`ML-KEM-768 keypair`	`22428` cycles	`22423` cycles	`1.00`
`ML-KEM-768 encaps`	`24506` cycles	`24575` cycles	`1.00`
`ML-KEM-768 decaps`	`32521` cycles	`32626` cycles	`1.00`
`ML-KEM-1024 keypair`	`32155` cycles	`32145` cycles	`1.00`
`ML-KEM-1024 encaps`	`35727` cycles	`35673` cycles	`1.00`
`ML-KEM-1024 decaps`	`47393` cycles	`47323` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`19032` cycles	`19032` cycles	`1`
`ML-KEM-512 encaps`	`23843` cycles	`23845` cycles	`1.00`
`ML-KEM-512 decaps`	`31228` cycles	`31230` cycles	`1.00`
`ML-KEM-768 keypair`	`32332` cycles	`32333` cycles	`1.00`
`ML-KEM-768 encaps`	`36084` cycles	`36083` cycles	`1.00`
`ML-KEM-768 decaps`	`46492` cycles	`46493` cycles	`1.00`
`ML-KEM-1024 keypair`	`46970` cycles	`46969` cycles	`1.00`
`ML-KEM-1024 encaps`	`53090` cycles	`53086` cycles	`1.00`
`ML-KEM-1024 decaps`	`67403` cycles	`67405` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`58051` cycles	`58016` cycles	`1.00`
`ML-KEM-512 encaps`	`65739` cycles	`65688` cycles	`1.00`
`ML-KEM-512 decaps`	`84356` cycles	`84278` cycles	`1.00`
`ML-KEM-768 keypair`	`98398` cycles	`98227` cycles	`1.00`
`ML-KEM-768 encaps`	`110291` cycles	`110272` cycles	`1.00`
`ML-KEM-768 decaps`	`136959` cycles	`136639` cycles	`1.00`
`ML-KEM-1024 keypair`	`149545` cycles	`149130` cycles	`1.00`
`ML-KEM-1024 encaps`	`166765` cycles	`166256` cycles	`1.00`
`ML-KEM-1024 decaps`	`203329` cycles	`202343` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`36182` cycles	`36296` cycles	`1.00`
`ML-KEM-512 encaps`	`46391` cycles	`46306` cycles	`1.00`
`ML-KEM-512 decaps`	`61856` cycles	`61607` cycles	`1.00`
`ML-KEM-768 keypair`	`59068` cycles	`58855` cycles	`1.00`
`ML-KEM-768 encaps`	`73046` cycles	`72584` cycles	`1.01`
`ML-KEM-768 decaps`	`91650` cycles	`91279` cycles	`1.00`
`ML-KEM-1024 keypair`	`88479` cycles	`88811` cycles	`1.00`
`ML-KEM-1024 encaps`	`109304` cycles	`109324` cycles	`1.00`
`ML-KEM-1024 decaps`	`133582` cycles	`132904` cycles	`1.01`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`45709` cycles	`45946` cycles	`0.99`
`ML-KEM-512 encaps`	`58758` cycles	`58762` cycles	`1.00`
`ML-KEM-512 decaps`	`79981` cycles	`79995` cycles	`1.00`
`ML-KEM-768 keypair`	`74596` cycles	`74601` cycles	`1.00`
`ML-KEM-768 encaps`	`91419` cycles	`91466` cycles	`1.00`
`ML-KEM-768 decaps`	`120104` cycles	`120171` cycles	`1.00`
`ML-KEM-1024 keypair`	`109864` cycles	`109869` cycles	`1.00`
`ML-KEM-1024 encaps`	`130993` cycles	`130986` cycles	`1.00`
`ML-KEM-1024 decaps`	`167584` cycles	`167659` cycles	`1.00`
Benchmark suite	Current: `425bc20`	Previous: `6ce990f`	Ratio
`ML-KEM-512 keypair`	`52315` cycles	`52330` cycles	`1.00`
`ML-KEM-512 encaps`	`67782` cycles	`67782` cycles	`1`
`ML-KEM-512 decaps`	`92653` cycles	`92630` cycles	`1.00`
`ML-KEM-768 keypair`	`84684` cycles	`84688` cycles	`1.00`
`ML-KEM-768 encaps`	`104896` cycles	`104906` cycles	`1.00`
`ML-KEM-768 decaps`	`138153` cycles	`137848` cycles	`1.00`
`ML-KEM-1024 keypair`	`125485` cycles	`125830` cycles	`1.00`
`ML-KEM-1024 encaps`	`149721` cycles	`149763` cycles	`1.00`
`ML-KEM-1024 decaps`	`192289` cycles	`192318` cycles	`1.00`