chore: cleanup z3

.python-version

@@ -0,0 +1 @@
+3.13

pyproject.toml

@@ -0,0 +1,12 @@
+[project]
+name = "aave-v4"
+version = "0.1.0"
+readme = "README.md"
+requires-python = ">=3.13"
+dependencies = ["z3-solver>=4.15.7.0"]
+
+[dependency-groups]
+dev = ["ruff>=0.15.0"]
+
+[tool.ruff.format]
+quote-style = "single"

tests/misc/calculate_linear_interest.py → tests/misc/z3/calculate_linear_interest.py

@@ -1,14 +1,13 @@
-from z3 import *
+from commons import *
 
 s = Optimize()
 
 UINT256_MAX = IntVal(2**256 - 1)
-RAY = IntVal(10**27)
 SECONDS_PER_YEAR = IntVal(365 * 24 * 60 * 60)
 
 rate = IntVal(2**96 - 1)
 lastUpdateTimestamp = IntVal(1)
-currentTimestamp = Int("currentTimestamp")
+currentTimestamp = Int('currentTimestamp')
 elapsed = currentTimestamp - lastUpdateTimestamp
 
 s.add(elapsed >= 0)
@@ -19,4 +18,4 @@
 
 assert s.check() == sat
 m = s.model()
-print("currentTimestamp max =", m[currentTimestamp])
+print('currentTimestamp max =', m[currentTimestamp])

tests/misc/z3/commons.py

@@ -53,9 +53,19 @@ def fromRayUp(a):
 def toRay(a):
     return a * RAY
 
+
 def min(a, b):
     return If(a <= b, a, b)
 
+
+def percentMulUp(value, percentage):
+    return (value * percentage + PERCENTAGE_FACTOR - 1) / PERCENTAGE_FACTOR
+
+
+def percentMulDown(value, percentage):
+    return (value * percentage) / PERCENTAGE_FACTOR
+
+
 def toAddedSharesDown(assets, totalAddedAssets, addedShares):
     return mulDivDown(
         assets, addedShares + VIRTUAL_SHARES, totalAddedAssets + VIRTUAL_ASSETS
@@ -102,39 +112,39 @@ def toValue(amount, decimals, price):
 
 
 def proveValid(s, propertyDescription, property, assumptions=[], variables=[]):
-    propertyDescriptionOutput = f"-- VALID Property: {propertyDescription} --"
-    print("=" * len(propertyDescriptionOutput))
+    propertyDescriptionOutput = f'-- VALID Property: {propertyDescription} --'
+    print('=' * len(propertyDescriptionOutput))
     print(propertyDescriptionOutput)
 
     result = s.check(Not(property), *assumptions)
     if result == sat:
-        print("❌ Property is not valid:")
+        print('❌ Property is not valid:')
         print(s.model())
         for variable, variableName in variables:
-            print(f"{variableName}: {s.model().eval(variable)}")
+            print(f'{variableName}: {s.model().eval(variable)}')
     elif result == unsat:
-        print(f"✅ Property is valid.")
+        print(f'✅ Property is valid.')
     elif result == unknown:
-        print("❓ Timed out or unknown.")
+        print('❓ Timed out or unknown.')
 
-    print("=" * len(propertyDescriptionOutput))
+    print('=' * len(propertyDescriptionOutput))
 
 
 def proveSatisfiable(s, propertyDescription, property, assumptions=[], variables=[]):
-    propertyDescriptionOutput = f"-- SATISFIABLE Property: {propertyDescription} --"
-    print("=" * len(propertyDescriptionOutput))
+    propertyDescriptionOutput = f'-- SATISFIABLE Property: {propertyDescription} --'
+    print('=' * len(propertyDescriptionOutput))
     print(propertyDescriptionOutput)
 
     result = s.check(property, *assumptions)
     if result == sat:
-        print("✅ Property is satisfiable")
+        print('✅ Property is satisfiable')
         m = s.model()
         print(m)
         for variable, variableName in variables:
-            print(f"{variableName}: {m.eval(variable)}")
+            print(f'{variableName}: {m.eval(variable)}')
     elif result == unsat:
-        print("❌ Property is unsatisfiable.")
+        print('❌ Property is unsatisfiable.')
     elif result == unknown:
-        print("❓ Timed out or unknown.")
+        print('❓ Timed out or unknown.')
 
-    print("=" * len(propertyDescriptionOutput))
+    print('=' * len(propertyDescriptionOutput))