From 93e289040f4d3162bb19c6f306c14df77012d3d2 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 9 Jul 2026 13:54:52 +0100 Subject: [PATCH 1/4] chore: bump leanwuzla to 6a67c0b (per-(op,format) two-tuple min/max tie-breaks) Points the leanwuzla submodule at the min-max-two-tuples branch tip that threads two independent tie-break Bools (zpm/zmp) per (operator, format) through fp.min/ fp.max (fp-lean-private f7a5e86 provides the two-arg smtMin/smtMax). Closes the completeness gap where a single shared tie-break excluded the same-sign-for-both- orderings models of min/max on differing-signed zeros. Co-Authored-By: Claude Opus 4.8 (1M context) --- leanwuzla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/leanwuzla b/leanwuzla index 2c7cf25..6a67c0b 160000 --- a/leanwuzla +++ b/leanwuzla @@ -1 +1 @@ -Subproject commit 2c7cf25081a512eaec82bdf2e5ae214ad65101e6 +Subproject commit 6a67c0b31618bb97c709c1b0132dcd9025a749fb From c9344ff866c1cf2131f20aa7d1a08ae05b407b07 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 9 Jul 2026 14:14:12 +0100 Subject: [PATCH 2/4] feat: anonymize our solver as "ours"/"ours (nokernel)" in all plot figures Paper figures must not reveal the tool identity. Renames the display labels (bench.tool2label) used in the cactus legend + endpoint annotations, the LaTeX macro suffixes (plot._texname override: Ours / OursNokernel / OursNancanon), and the per-tool tex section comments -- so no "FP-Lean"/"fplean" string appears in cactus.{png,pdf,tex}. The internal ToolName ids ("fplean", ...) are unchanged (they still key commands, run dirs, and the manifest); only the figure-facing strings are anonymized. Co-Authored-By: Claude Opus 4.8 (1M context) --- bench.py | 6 ++++-- plot.py | 11 ++++++++++- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/bench.py b/bench.py index 26b9f09..2cb21f7 100644 --- a/bench.py +++ b/bench.py @@ -242,9 +242,11 @@ def __post_init__(self) -> None: tool2color: dict[ToolName, str] = { "bitwuzla": "#FFAB40", "fplean": "#2E7D32", "fplean-nokernel": "#1565C0", "fplean-nancanon": "#C62828", "exhaustive-enumeration": "#8E24AA"} +# Display labels for the plots. Our solver is presented anonymously as "ours" +# (never by its internal name) so no tool identity leaks into paper figures. tool2label: dict[ToolName, str] = { - "bitwuzla": "Bitwuzla", "fplean": "FP-Lean", "fplean-nokernel": "FP-Lean (no kernel)", - "fplean-nancanon": "FP-Lean + NaN-canon", "exhaustive-enumeration": "Exhaustive enum"} + "bitwuzla": "Bitwuzla", "fplean": "ours", "fplean-nokernel": "ours (nokernel)", + "fplean-nancanon": "ours (NaN-canon)", "exhaustive-enumeration": "Exhaustive enum"} class Problem(TypedDict): diff --git a/plot.py b/plot.py index 939c2d7..569f51a 100755 --- a/plot.py +++ b/plot.py @@ -28,9 +28,18 @@ # plotted are still reported in the summary and the LaTeX macros. +# Our solver is anonymized as "Ours" in LaTeX macro names too, so no tool +# identity leaks into the paper's \input'd macros. +_TEXNAME_OVERRIDE = { + "fplean": "Ours", "fplean-nokernel": "OursNokernel", + "fplean-nancanon": "OursNancanon"} + + def _texname(tool: str) -> str: """Letters-only, capitalized form of a tool name for use in LaTeX \\newcommand names (which may not contain hyphens or digits).""" + if tool in _TEXNAME_OVERRIDE: + return _TEXNAME_OVERRIDE[tool] return re.sub(r"[^A-Za-z]", "", tool).capitalize() @@ -295,7 +304,7 @@ def plot_cactus(indir: pathlib.Path, outdir: pathlib.Path, opts: argparse.Namesp f"{pfx}GeomeanMs{cap}": f"{s['geomean_ms']:.1f}", } lines.append("") - lines.append(f"%% {tool}") + lines.append(f"%% {bench.tool2label[tool]}") lines.extend(bench.format_newcommand(k, v) for k, v in per_tool.items()) speedups = { From 341cc3c9542cbd284f13b4178f68a8a2db97165b Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 9 Jul 2026 14:18:31 +0100 Subject: [PATCH 3/4] chore: bump leanwuzla to bb77e6b (merged min-max two-tuple tie-breaks into fp) Points at the fp-branch tip after PR #8 merged; content-identical to the prior 6a67c0b pin, now on the canonical integration branch. Co-Authored-By: Claude Opus 4.8 (1M context) --- leanwuzla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/leanwuzla b/leanwuzla index 6a67c0b..bb77e6b 160000 --- a/leanwuzla +++ b/leanwuzla @@ -1 +1 @@ -Subproject commit 6a67c0b31618bb97c709c1b0132dcd9025a749fb +Subproject commit bb77e6bb7e2afc1bf895d9f20fac2936b3f3ef7f From 34ed0cd4372956da7f5913b1e0e70441d711a03e Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 9 Jul 2026 18:13:04 +0100 Subject: [PATCH 4/4] chore: bump leanwuzla to 784c984 (chained fp comparison desugar) Post-submission improvement: incorporates the parser-error-fixes work (n-ary/chained fp.lt/fp.leq/fp.gt/fp.geq desugaring), resolving the 4 schanda kernel-solver errors. Branches off the POPL'26 submission snapshot (341cc3c). Co-Authored-By: Claude Opus 4.8 (1M context) --- leanwuzla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/leanwuzla b/leanwuzla index bb77e6b..784c984 160000 --- a/leanwuzla +++ b/leanwuzla @@ -1 +1 @@ -Subproject commit bb77e6bb7e2afc1bf895d9f20fac2936b3f3ef7f +Subproject commit 784c98459f80ddae02fd4d866f02401a91ac694b