From 73c4b082f41cd445c1cb6d3d7ca2df3df9d6eb52 Mon Sep 17 00:00:00 2001
From: Thomas Coratger <60488569+tcoratger@users.noreply.github.com>
Date: Thu, 21 May 2026 00:18:16 +0200
Subject: [PATCH] refactor(lstar): use math.ceil for 2/3 supermajority
 threshold

Replace the -(-n * 2 // 3) ceiling-division trick with math.ceil.
The trick relied on the reader recognising that flooring on a
negated value yields a ceiling; math.ceil expresses the intent
directly. Validator counts are capped well within float precision,
and the int() cast keeps the multiplication out of the Uint64
operator that rejects plain-int operands.

Equivalence verified across n = 0, 1, 2, 3, 99..101, 4096, 8192,
99999.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 src/lean_spec/forks/lstar/spec.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/lean_spec/forks/lstar/spec.py b/src/lean_spec/forks/lstar/spec.py
index a65e0a59..e2e1b992 100644
--- a/src/lean_spec/forks/lstar/spec.py
+++ b/src/lean_spec/forks/lstar/spec.py
@@ -1,5 +1,6 @@
 """Lstar fork — identity and construction facade."""
 
+import math
 from collections import defaultdict
 from collections.abc import Iterable, Sequence, Set as AbstractSet
 from typing import Any, ClassVar
@@ -1570,9 +1571,9 @@ def update_safe_target(self, store: LstarStore) -> LstarStore:
         # Compute the 2/3 supermajority threshold.
         #
         # A block needs at least this many attestation votes to be "safe".
-        # The ceiling division (negation trick) ensures we round UP.
+        # The threshold is rounded UP so a strict majority is required.
         # For example, 100 validators => threshold is 67, not 66.
-        min_target_score = -(-num_validators * 2 // 3)
+        min_target_score = math.ceil(int(num_validators) * 2 / 3)
 
         # Unpack "new" payloads into a flat validator -> vote mapping.
         # "Known" is excluded by design.