Further summarize script updates, add manual inputs, add renderable t…

…able
verus-lang · Aug 19, 2024 · 298febb · 298febb
1 parent 48dd717
commit 298febb
Show file tree

Hide file tree

Showing 5 changed files with 316 additions and 266 deletions.
diff --git a/macro-stats/.gitignore b/macro-stats/.gitignore
@@ -1,2 +1,2 @@
 /repos/
-/results/
+/results*
diff --git a/macro-stats/summarize/manual.json b/macro-stats/summarize/manual.json
@@ -0,0 +1,34 @@
+[
+    {
+        "project-id": "ironsht",
+        "dafny-baseline": {
+            "linecount": {
+                "trusted": 1205,
+                "proof": 8070,
+                "exec": 1923,
+                "proof-code-ratio": 4.2
+            },
+            "encoding-size-mbs": 352
+        }
+    }, {
+        "project-id": "nr",
+        "dafny-baseline": {
+            "linecount": {
+                "trusted": 104,
+                "proof": 7828,
+                "exec": 730,
+                "proof-code-ratio": 10.7
+            },
+            "encoding-size-mbs": 2063
+        }
+    }, {
+        "project-id": "page-table",
+        "verus": {
+            "linecount-delta": {
+                "trusted": 0,
+                "proof": 32,
+                "exec": 93
+            }
+        }
+    }
+]
diff --git a/macro-stats/summarize/render/.gitignore b/macro-stats/summarize/render/.gitignore
@@ -0,0 +1,5 @@
+macro-table.aux
+macro-table.fdb_latexmk
+macro-table.fls
+macro-table.log
+macro-table.pdf
diff --git a/macro-stats/summarize/render/macro-table.tex b/macro-stats/summarize/render/macro-table.tex
@@ -0,0 +1,35 @@
+\documentclass{article}
+\usepackage{multirow}
+\usepackage{rotating}
+\usepackage{xspace}
+\newcommand*{\tablerot}{\rotatebox{90}}
+\newcommand*{\name}{Verus\xspace}
+\begin{document}
+
+\input{../../results/results-latex-commands.tex}
+\begin{tabular}{l|rrr|r|rr|r}
+    \multirow{2}{1.6cm}{\vfill{}System \\ $\rightarrow$ Verifier}
+    & \multicolumn{3}{c|}{Line Count}
+    & \multirow{2}{.2cm}{\tablerot{P/C Ratio}}
+    & \multicolumn{2}{c|}{Time (s)}
+    & \multirow{2}{.2cm}{\tablerot{SMT (MB)}} \\
+
+     & \tablerot{trusted}
+     & \tablerot{proof}
+     & \tablerot{code}
+     &
+     & \tablerot{1 core}
+     & \tablerot{\evalParallelNumThreads\xspace cores}
+     & \\ \hline
+    IronKV &   &   &   &   &   &   &   \\
+    $\rightarrow$ \name & \evalVerusIronshtLineCountTrusted & \evalVerusIronshtLineCountProof & \evalVerusIronshtLineCountExec & \evalVerusIronshtLineCountProofCodeRatio & \evalVerusIronshtSinglethreadWallTime & \evalVerusIronshtParallelWallTime & \evalVerusIronshtEncodingSizeMB \\
+    $\rightarrow$ Dafny & \evalDafnyIronshtLineCountTrusted & \evalDafnyIronshtLineCountProof & \evalDafnyIronshtLineCountExec & \evalDafnyIronshtLineCountProofCodeRatio & \evalDafnyIronshtSinglethreadWallTime & \evalDafnyIronshtParallelWallTime & \evalDafnyIronshtEncodingSizeMB \\
+   \hline  NR &   &   &   &   &   &   &   \\
+    $\rightarrow$ \name & \evalVerusNrLineCountTrusted & \evalVerusNrLineCountProof & \evalVerusNrLineCountExec & \evalVerusNrLineCountProofCodeRatio & \evalVerusNrSinglethreadWallTime & \evalVerusNrParallelWallTime & \evalVerusNrEncodingSizeMB \\
+    $\rightarrow$ L.Dafny & \evalLinearDafnyNrLineCountTrusted & \evalLinearDafnyNrLineCountProof & \evalLinearDafnyNrLineCountExec & \evalLinearDafnyNrLineCountProofCodeRatio & \evalLinearDafnyNrSinglethreadWallTime & \evalLinearDafnyNrParallelWallTime & \evalLinearDafnyNrEncodingSizeMB \\
+   \hline \hline  Page table & \evalVerusPageTableLineCountTrusted & \evalVerusPageTableLineCountProof & \evalVerusPageTableLineCountExec & \evalVerusPageTableLineCountProofCodeRatio & \evalVerusPageTableSinglethreadWallTime & \evalVerusPageTableParallelWallTime & \evalVerusPageTableEncodingSizeMB \\
+   \hline  Mimalloc & \evalVerusMimallocLineCountTrusted & \evalVerusMimallocLineCountProof & \evalVerusMimallocLineCountExec & \evalVerusMimallocLineCountProofCodeRatio & \evalVerusMimallocSinglethreadWallTime & \evalVerusMimallocParallelWallTime & \evalVerusMimallocEncodingSizeMB \\
+   \hline  P. log & \evalVerusVerifiedStorageLineCountTrusted & \evalVerusVerifiedStorageLineCountProof & \evalVerusVerifiedStorageLineCountExec & \evalVerusVerifiedStorageLineCountProofCodeRatio & \evalVerusVerifiedStorageSinglethreadWallTime & \evalVerusVerifiedStorageParallelWallTime & \evalVerusVerifiedStorageEncodingSizeMB \\
+   \hline \hline  Verus total & \evalVerusTotalLinesTrusted & \evalVerusTotalLinesProof & \evalVerusTotalLinesExec & \evalVerusTotalLinesProofCodeRatio \\
+\end{tabular}
+\end{document}