From 0c7a4ad49f49a8e21f063f7adbfebac83e903e3e Mon Sep 17 00:00:00 2001 From: crStiv Date: Fri, 5 Dec 2025 11:38:25 +0100 Subject: [PATCH 1/3] Fix current interval calculation in store.py --- src/lean_spec/subspecs/forkchoice/store.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lean_spec/subspecs/forkchoice/store.py b/src/lean_spec/subspecs/forkchoice/store.py index 2f48ff13..b840fac0 100644 --- a/src/lean_spec/subspecs/forkchoice/store.py +++ b/src/lean_spec/subspecs/forkchoice/store.py @@ -732,7 +732,7 @@ def tick_interval(self, has_proposal: bool) -> "Store": """ # Advance time by one interval store = self.model_copy(update={"time": self.time + Uint64(1)}) - current_interval = store.time % SECONDS_PER_SLOT % INTERVALS_PER_SLOT + current_interval = store.time % INTERVALS_PER_SLOT if current_interval == Uint64(0): # Start of slot - process attestations if proposal exists From 1a5f10df5b4a106b5331fbbe9fa66cc3bc7fade1 Mon Sep 17 00:00:00 2001 From: crStiv Date: Tue, 13 Jan 2026 19:53:32 +0200 Subject: [PATCH 2/3] Update store.py --- src/lean_spec/subspecs/forkchoice/store.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/lean_spec/subspecs/forkchoice/store.py b/src/lean_spec/subspecs/forkchoice/store.py index b840fac0..b79d04f2 100644 --- a/src/lean_spec/subspecs/forkchoice/store.py +++ b/src/lean_spec/subspecs/forkchoice/store.py @@ -732,7 +732,15 @@ def tick_interval(self, has_proposal: bool) -> "Store": """ # Advance time by one interval store = self.model_copy(update={"time": self.time + Uint64(1)}) - current_interval = store.time % INTERVALS_PER_SLOT + # Calculate current interval within slot + # time is in seconds, so we need to: + # 1. Get seconds within current slot: time % SECONDS_PER_SLOT + # 2. Convert to intervals: // SECONDS_PER_INTERVAL + # This formula correctly handles the case when SECONDS_PER_SLOT != INTERVALS_PER_SLOT, + # unlike the incorrect formula: time % INTERVALS_PER_SLOT + # Note: This requires that SECONDS_PER_SLOT is a multiple of INTERVALS_PER_SLOT + # (i.e., SECONDS_PER_INTERVAL must be an integer >= 1) + current_interval = (store.time % SECONDS_PER_SLOT) // SECONDS_PER_INTERVAL if current_interval == Uint64(0): # Start of slot - process attestations if proposal exists From 984ab2e523243e3a7861dfc3215c32c036b5aef2 Mon Sep 17 00:00:00 2001 From: Unnawut Leepaisalsuwanna <921194+unnawut@users.noreply.github.com> Date: Mon, 19 Jan 2026 16:52:50 +0700 Subject: [PATCH 3/3] Update store.py --- src/lean_spec/subspecs/forkchoice/store.py | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/lean_spec/subspecs/forkchoice/store.py b/src/lean_spec/subspecs/forkchoice/store.py index b79d04f2..b840fac0 100644 --- a/src/lean_spec/subspecs/forkchoice/store.py +++ b/src/lean_spec/subspecs/forkchoice/store.py @@ -732,15 +732,7 @@ def tick_interval(self, has_proposal: bool) -> "Store": """ # Advance time by one interval store = self.model_copy(update={"time": self.time + Uint64(1)}) - # Calculate current interval within slot - # time is in seconds, so we need to: - # 1. Get seconds within current slot: time % SECONDS_PER_SLOT - # 2. Convert to intervals: // SECONDS_PER_INTERVAL - # This formula correctly handles the case when SECONDS_PER_SLOT != INTERVALS_PER_SLOT, - # unlike the incorrect formula: time % INTERVALS_PER_SLOT - # Note: This requires that SECONDS_PER_SLOT is a multiple of INTERVALS_PER_SLOT - # (i.e., SECONDS_PER_INTERVAL must be an integer >= 1) - current_interval = (store.time % SECONDS_PER_SLOT) // SECONDS_PER_INTERVAL + current_interval = store.time % INTERVALS_PER_SLOT if current_interval == Uint64(0): # Start of slot - process attestations if proposal exists