lfglabs-dev · Th0rgal · Apr 22, 2026 · Apr 22, 2026 · Apr 22, 2026 · Apr 22, 2026
diff --git a/.github/actions/setup-lean/action.yml b/.github/actions/setup-lean/action.yml
@@ -30,12 +30,13 @@ runs:
         LEAN_TOOLCHAIN_HASH: ${{ hashFiles('lean-toolchain') }}
         LAKEFILE_HASH: ${{ hashFiles('lakefile.lean') }}
         LAKE_MANIFEST_HASH: ${{ hashFiles('lake-manifest.json') }}
+        CACHE_SALT_HASH: ${{ hashFiles('.github/cache-salt') }}
       run: |
-        elan_key="elan-benchmark-${CACHE_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}"
-        packages_key="lake-packages-benchmark-${CACHE_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}"
-        packages_main_key="lake-packages-benchmark-${MAIN_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}"
-        build_key="lake-build-benchmark-${CACHE_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}"
-        build_main_key="lake-build-benchmark-${MAIN_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}"
+        elan_key="elan-benchmark-${CACHE_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${CACHE_SALT_HASH}"
+        packages_key="lake-packages-benchmark-${CACHE_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}-${CACHE_SALT_HASH}"
+        packages_main_key="lake-packages-benchmark-${MAIN_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}-${CACHE_SALT_HASH}"
+        build_key="lake-build-benchmark-${CACHE_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}-${CACHE_SALT_HASH}"
+        build_main_key="lake-build-benchmark-${MAIN_BUCKET}-${RUNNER_OS_NAME}-${LEAN_TOOLCHAIN_HASH}-${LAKEFILE_HASH}-${LAKE_MANIFEST_HASH}-${CACHE_SALT_HASH}"
         {
           echo "use_sticky=${USE_STICKY}"
           echo "use_build_sticky=${USE_BUILD_STICKY}"

diff --git a/.github/cache-salt b/.github/cache-salt
@@ -0,0 +1 @@
+1
diff --git a/Benchmark/GeneratedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/DepositSetsPoolBalance.lean b/Benchmark/GeneratedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/DepositSetsPoolBalance.lean
@@ -0,0 +1,22 @@
+import Benchmark.Cases.DamnVulnerableDeFi.SideEntrance.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `deposit` stores `oldPoolBalance + amount` in `poolBalance`.
+-/
+theorem deposit_sets_pool_balance
+    (amount : Uint256) (s : ContractState) :
+    let s' := ((SideEntrance.deposit amount).run s).snd
+    deposit_sets_pool_balance_spec amount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold deposit_sets_pool_balance_spec
+  grind [SideEntrance.deposit, SideEntrance.poolBalance, SideEntrance.totalCredits, SideEntrance.creditOf]
+
+end Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
diff --git a/...hmark/GeneratedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/DepositSetsSenderCredit.lean b/...hmark/GeneratedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/DepositSetsSenderCredit.lean
@@ -0,0 +1,22 @@
+import Benchmark.Cases.DamnVulnerableDeFi.SideEntrance.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `deposit` increases the caller's credited balance by `amount`.
+-/
+theorem deposit_sets_sender_credit
+    (amount : Uint256) (s : ContractState) :
+    let s' := ((SideEntrance.deposit amount).run s).snd
+    deposit_sets_sender_credit_spec amount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold deposit_sets_sender_credit_spec
+  grind [SideEntrance.deposit, SideEntrance.poolBalance, SideEntrance.totalCredits, SideEntrance.creditOf]
+
+end Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
diff --git a/Benchmark/GeneratedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/ExploitTraceDrainsPool.lean b/Benchmark/GeneratedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/ExploitTraceDrainsPool.lean
@@ -0,0 +1,27 @@
+import Benchmark.Cases.DamnVulnerableDeFi.SideEntrance.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+If the caller starts with zero credited balance, then borrowing `amount`,
+repaying through `deposit`, and withdrawing immediately reduces pool ETH by
+exactly `amount`.
+-/
+theorem exploit_trace_drains_pool
+    (amount : Uint256) (s : ContractState)
+    (hBorrow : amount <= s.storage 0)
+    (hFresh : s.storageMap 2 s.sender = 0) :
+    let s' := ((SideEntrance.flashLoanViaDeposit amount).run s).snd
+    let s'' := ((SideEntrance.withdraw).run s').snd
+    exploit_trace_drains_pool_spec amount s s'' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold exploit_trace_drains_pool_spec
+  grind [SideEntrance.flashLoanViaDeposit, SideEntrance.withdraw, SideEntrance.poolBalance, SideEntrance.totalCredits, SideEntrance.creditOf]
+
+end Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
diff --git a/...review/DamnVulnerableDeFi/SideEntrance/Tasks/FlashLoanViaDepositPreservesPoolBalance.lean b/...review/DamnVulnerableDeFi/SideEntrance/Tasks/FlashLoanViaDepositPreservesPoolBalance.lean
@@ -0,0 +1,24 @@
+import Benchmark.Cases.DamnVulnerableDeFi.SideEntrance.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing the summarized flash-loan-plus-deposit path leaves tracked pool ETH
+unchanged.
+-/
+theorem flashLoanViaDeposit_preserves_pool_balance
+    (amount : Uint256) (s : ContractState)
+    (hBorrow : amount <= s.storage 0) :
+    let s' := ((SideEntrance.flashLoanViaDeposit amount).run s).snd
+    flashLoanViaDeposit_preserves_pool_balance_spec amount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold flashLoanViaDeposit_preserves_pool_balance_spec
+  grind [SideEntrance.flashLoanViaDeposit, SideEntrance.poolBalance, SideEntrance.totalCredits, SideEntrance.creditOf]
+
+end Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
diff --git a/...tedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/FlashLoanViaDepositSetsSenderCredit.lean b/...tedPreview/DamnVulnerableDeFi/SideEntrance/Tasks/FlashLoanViaDepositSetsSenderCredit.lean
@@ -0,0 +1,24 @@
+import Benchmark.Cases.DamnVulnerableDeFi.SideEntrance.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing the summarized flash-loan-plus-deposit path mints caller credit
+equal to the borrowed amount.
+-/
+theorem flashLoanViaDeposit_sets_sender_credit
+    (amount : Uint256) (s : ContractState)
+    (hBorrow : amount <= s.storage 0) :
+    let s' := ((SideEntrance.flashLoanViaDeposit amount).run s).snd
+    flashLoanViaDeposit_sets_sender_credit_spec amount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold flashLoanViaDeposit_sets_sender_credit_spec
+  grind [SideEntrance.flashLoanViaDeposit, SideEntrance.poolBalance, SideEntrance.totalCredits, SideEntrance.creditOf]
+
+end Benchmark.Cases.DamnVulnerableDeFi.SideEntrance
diff --git a/Benchmark/GeneratedPreview/Ethereum/DepositContractMinimal/Tasks/ChainStartThreshold.lean b/Benchmark/GeneratedPreview/Ethereum/DepositContractMinimal/Tasks/ChainStartThreshold.lean
@@ -0,0 +1,26 @@
+import Benchmark.Cases.Ethereum.DepositContractMinimal.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Ethereum.DepositContractMinimal
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing a threshold-crossing full deposit sets `chainStarted`.
+-/
+theorem full_deposit_starts_chain_at_threshold
+    (depositAmount : Uint256) (s : ContractState)
+    (hCount : s.storage 0 < 4294967295)
+    (hMin : depositAmount >= 1000000000)
+    (hFull : depositAmount >= 32000000000)
+    (hThreshold : add (s.storage 1) 1 = 65536) :
+    let s' := ((DepositContractMinimal.deposit depositAmount).run s).snd
+    deposit_starts_chain_at_threshold_spec depositAmount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold deposit_starts_chain_at_threshold_spec
+  grind [DepositContractMinimal.deposit, DepositContractMinimal.depositCount, DepositContractMinimal.fullDepositCount, DepositContractMinimal.chainStarted]
+
+end Benchmark.Cases.Ethereum.DepositContractMinimal
diff --git a/Benchmark/GeneratedPreview/Ethereum/DepositContractMinimal/Tasks/DepositCount.lean b/Benchmark/GeneratedPreview/Ethereum/DepositContractMinimal/Tasks/DepositCount.lean
@@ -0,0 +1,25 @@
+import Benchmark.Cases.Ethereum.DepositContractMinimal.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Ethereum.DepositContractMinimal
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `deposit` on the successful path increments the total deposit counter
+by exactly one.
+-/
+theorem deposit_increments_deposit_count
+    (depositAmount : Uint256) (s : ContractState)
+    (hCount : s.storage 0 < 4294967295)
+    (hMin : depositAmount >= 1000000000) :
+    let s' := ((DepositContractMinimal.deposit depositAmount).run s).snd
+    deposit_increments_deposit_count_spec s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold deposit_increments_deposit_count_spec
+  grind [DepositContractMinimal.deposit, DepositContractMinimal.depositCount, DepositContractMinimal.fullDepositCount, DepositContractMinimal.chainStarted]
+
+end Benchmark.Cases.Ethereum.DepositContractMinimal
diff --git a/...eneratedPreview/Ethereum/DepositContractMinimal/Tasks/FullDepositIncrementsFullCount.lean b/...eneratedPreview/Ethereum/DepositContractMinimal/Tasks/FullDepositIncrementsFullCount.lean
@@ -0,0 +1,26 @@
+import Benchmark.Cases.Ethereum.DepositContractMinimal.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Ethereum.DepositContractMinimal
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `deposit` at or above the full threshold increments
+`fullDepositCount` by one.
+-/
+theorem full_deposit_increments_full_count
+    (depositAmount : Uint256) (s : ContractState)
+    (hCount : s.storage 0 < 4294967295)
+    (hMin : depositAmount >= 1000000000)
+    (hFull : depositAmount >= 32000000000) :
+    let s' := ((DepositContractMinimal.deposit depositAmount).run s).snd
+    deposit_increments_full_count_for_full_deposit_spec depositAmount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold deposit_increments_full_count_for_full_deposit_spec
+  grind [DepositContractMinimal.deposit, DepositContractMinimal.depositCount, DepositContractMinimal.fullDepositCount, DepositContractMinimal.chainStarted]
+
+end Benchmark.Cases.Ethereum.DepositContractMinimal
diff --git a/...eneratedPreview/Ethereum/DepositContractMinimal/Tasks/FullDepositPreservesPartialGap.lean b/...eneratedPreview/Ethereum/DepositContractMinimal/Tasks/FullDepositPreservesPartialGap.lean
@@ -0,0 +1,25 @@
+import Benchmark.Cases.Ethereum.DepositContractMinimal.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Ethereum.DepositContractMinimal
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing a full deposit increments both counters in lockstep, so the gap
+between all deposits and full deposits is preserved.
+-/
+theorem full_deposit_preserves_partial_gap
+    (depositAmount : Uint256) (s : ContractState)
+    (hCount : s.storage 0 < 4294967295)
+    (hMin : depositAmount >= 1000000000)
+    (hFull : depositAmount >= 32000000000) :
+    let s' := ((DepositContractMinimal.deposit depositAmount).run s).snd
+    s'.storage 0 - s'.storage 1 = s.storage 0 - s.storage 1 := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  grind [DepositContractMinimal.deposit, DepositContractMinimal.depositCount, DepositContractMinimal.fullDepositCount, DepositContractMinimal.chainStarted]
+
+end Benchmark.Cases.Ethereum.DepositContractMinimal
diff --git a/...eneratedPreview/Ethereum/DepositContractMinimal/Tasks/SmallDepositPreservesFullCount.lean b/...eneratedPreview/Ethereum/DepositContractMinimal/Tasks/SmallDepositPreservesFullCount.lean
@@ -0,0 +1,26 @@
+import Benchmark.Cases.Ethereum.DepositContractMinimal.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Ethereum.DepositContractMinimal
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `deposit` below the full threshold leaves `fullDepositCount`
+unchanged.
+-/
+theorem small_deposit_preserves_full_count
+    (depositAmount : Uint256) (s : ContractState)
+    (hCount : s.storage 0 < 4294967295)
+    (hMin : depositAmount >= 1000000000)
+    (hSmall : depositAmount < 32000000000) :
+    let s' := ((DepositContractMinimal.deposit depositAmount).run s).snd
+    deposit_preserves_full_count_for_small_deposit_spec depositAmount s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold deposit_preserves_full_count_for_small_deposit_spec
+  grind [DepositContractMinimal.deposit, DepositContractMinimal.depositCount, DepositContractMinimal.fullDepositCount, DepositContractMinimal.chainStarted]
+
+end Benchmark.Cases.Ethereum.DepositContractMinimal
diff --git a/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/DrawIntervalMatchesWeights.lean b/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/DrawIntervalMatchesWeights.lean
@@ -0,0 +1,25 @@
+import Benchmark.Cases.Kleros.SortitionTrees.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Kleros.SortitionTrees
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `draw` follows the encoded ticket intervals used by the
+implementation.
+-/
+theorem draw_interval_matches_weights
+    (ticket : Uint256) (s : ContractState)
+    (hRoot : s.storage 0 != 0)
+    (hInRange : ticket < s.storage 0) :
+    let s' := ((SortitionTrees.draw ticket).run s).snd
+    draw_interval_matches_weights_spec ticket s s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold draw_interval_matches_weights_spec
+  grind [SortitionTrees.draw, SortitionTrees.rootSum, SortitionTrees.leftSum, SortitionTrees.rightSum, SortitionTrees.leaf0, SortitionTrees.leaf1, SortitionTrees.leaf2, SortitionTrees.leaf3, SortitionTrees.nodeIndexesToIDs, SortitionTrees.IDsToNodeIndexes, SortitionTrees.selectedNode]
+
+end Benchmark.Cases.Kleros.SortitionTrees
diff --git a/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/DrawSelectsValidLeaf.lean b/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/DrawSelectsValidLeaf.lean
@@ -0,0 +1,24 @@
+import Benchmark.Cases.Kleros.SortitionTrees.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Kleros.SortitionTrees
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Any successful `draw` resolves to one of the four leaf node indices.
+-/
+theorem draw_selects_valid_leaf
+    (ticket : Uint256) (s : ContractState)
+    (hRoot : s.storage 0 != 0)
+    (hInRange : ticket < s.storage 0) :
+    let s' := ((SortitionTrees.draw ticket).run s).snd
+    draw_selects_valid_leaf_spec s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold draw_selects_valid_leaf_spec
+  grind [SortitionTrees.draw, SortitionTrees.rootSum, SortitionTrees.leftSum, SortitionTrees.rightSum, SortitionTrees.leaf0, SortitionTrees.leaf1, SortitionTrees.leaf2, SortitionTrees.leaf3, SortitionTrees.nodeIndexesToIDs, SortitionTrees.IDsToNodeIndexes, SortitionTrees.selectedNode]
+
+end Benchmark.Cases.Kleros.SortitionTrees
diff --git a/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/NodeIdBijection.lean b/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/NodeIdBijection.lean
@@ -0,0 +1,25 @@
+import Benchmark.Cases.Kleros.SortitionTrees.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Kleros.SortitionTrees
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `setLeaf` writes matching forward and reverse mapping entries for the
+updated node and stake-path id.
+-/
+theorem node_id_bijection
+    (nodeIndex stakePathID weight : Uint256) (s : ContractState)
+    (hLow : nodeIndex >= 3)
+    (hHigh : nodeIndex <= 6) :
+    let s' := ((SortitionTrees.setLeaf nodeIndex stakePathID weight).run s).snd
+    node_id_bijection_spec nodeIndex stakePathID s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold node_id_bijection_spec
+  grind [SortitionTrees.setLeaf, SortitionTrees.rootSum, SortitionTrees.leftSum, SortitionTrees.rightSum, SortitionTrees.leaf0, SortitionTrees.leaf1, SortitionTrees.leaf2, SortitionTrees.leaf3, SortitionTrees.nodeIndexesToIDs, SortitionTrees.IDsToNodeIndexes, SortitionTrees.selectedNode]
+
+end Benchmark.Cases.Kleros.SortitionTrees
diff --git a/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/ParentEqualsSumOfChildren.lean b/Benchmark/GeneratedPreview/Kleros/SortitionTrees/Tasks/ParentEqualsSumOfChildren.lean
@@ -0,0 +1,24 @@
+import Benchmark.Cases.Kleros.SortitionTrees.Specs
+import Benchmark.Grindset
+
+namespace Benchmark.Cases.Kleros.SortitionTrees
+
+open Verity
+open Verity.EVM.Uint256
+
+/--
+Executing `setLeaf` recomputes each parent node from its direct children.
+-/
+theorem parent_equals_sum_of_children
+    (nodeIndex stakePathID weight : Uint256) (s : ContractState)
+    (hLow : nodeIndex >= 3)
+    (hHigh : nodeIndex <= 6) :
+    let s' := ((SortitionTrees.setLeaf nodeIndex stakePathID weight).run s).snd
+    parent_equals_sum_of_children_spec s' := by
+  -- Grindset-first skeleton. See harness/PROOF_PATTERNS.md.
+  -- Try `grind` with contract symbol hints; fall back to `simp` /
+  -- `by_cases` if grind leaves goals. Use `grind?` for hints.
+  unfold parent_equals_sum_of_children_spec
+  grind [SortitionTrees.setLeaf, SortitionTrees.rootSum, SortitionTrees.leftSum, SortitionTrees.rightSum, SortitionTrees.leaf0, SortitionTrees.leaf1, SortitionTrees.leaf2, SortitionTrees.leaf3, SortitionTrees.nodeIndexesToIDs, SortitionTrees.IDsToNodeIndexes, SortitionTrees.selectedNode]
+
+end Benchmark.Cases.Kleros.SortitionTrees