Skip to content

refactor(lstar): use math.ceil for 2/3 supermajority threshold #742

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
tcoratger merged 1 commit into from
May 21, 2026
Merged

refactor(lstar): use math.ceil for 2/3 supermajority threshold #742

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/lean_spec/forks/lstar/spec.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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.
Expand Down
Loading