From a63fcd9b5610f2dcedf9a3d98297b51199212013 Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Tue, 29 Jul 2025 10:48:59 +0300 Subject: [PATCH] Add mutation 001: accumulateFlows off-by-one --- .../mutations/001_accumulateFlows_off_by_one.patch | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 certora/mutations/001_accumulateFlows_off_by_one.patch diff --git a/certora/mutations/001_accumulateFlows_off_by_one.patch b/certora/mutations/001_accumulateFlows_off_by_one.patch new file mode 100644 index 0000000..538be7d --- /dev/null +++ b/certora/mutations/001_accumulateFlows_off_by_one.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol +index 3066e7d..c93554d 100644 +--- a/contracts/vault/Accounts.sol ++++ b/contracts/vault/Accounts.sol +@@ -81,7 +81,7 @@ library Accounts { + Timestamp timestamp + ) internal pure { + Duration duration = account.flow.updated.until(timestamp); +- account.balance.available -= account.flow.outgoing.accumulate(duration); ++ account.balance.available -= account.flow.outgoing.accumulate(duration) + 1; + account.balance.designated += account.flow.incoming.accumulate(duration); + account.flow.updated = timestamp; + }