Note: Alloy logs critiqued by PIRTM counter-paper
Browse files
README.md
CHANGED
|
@@ -14,6 +14,9 @@ tags:
|
|
| 14 |
|
| 15 |
> Mirrored from [https://github.com/SNAPKITTYWEST/hcalc](https://github.com/SNAPKITTYWEST/hcalc) at commit `5d8fa46`. Part of the **SnapKitty October 2026 main drop**.
|
| 16 |
|
|
|
|
|
|
|
|
|
|
| 17 |
<!--
|
| 18 |
Copyright (C) 2026 HCALC contributors
|
| 19 |
SPDX-License-Identifier: AGPL-3.0-only
|
|
|
|
| 14 |
|
| 15 |
> Mirrored from [https://github.com/SNAPKITTYWEST/hcalc](https://github.com/SNAPKITTYWEST/hcalc) at commit `5d8fa46`. Part of the **SnapKitty October 2026 main drop**.
|
| 16 |
|
| 17 |
+
> [!NOTE]
|
| 18 |
+
> **About the Alloy logs:** the counter-paper [Snapkitty/PIRTM](https://huggingface.co/Snapkitty/PIRTM) shows that the Alloy checks in `alloy/` cannot fail. Each `UNSAT (PASS)` assertion (A1–A7, P1–P8, `INV_*`) restates a fact the model already enforces, and the same pattern returns `UNSAT` for a deliberately false claim. Read those results as consistency checks, not as verification of the mathematics. The counter-paper does **not** dispute HCALC's definitions, its mathematics or its Lean 4 formalization.
|
| 19 |
+
|
| 20 |
<!--
|
| 21 |
Copyright (C) 2026 HCALC contributors
|
| 22 |
SPDX-License-Identifier: AGPL-3.0-only
|