@kryptosai/counterflow - npm Package Compare versions

Comparing version 0.5.1 to 0.6.0

CHANGELOG.md

@@ -5,2 +5,9 @@ # Changelog
 
+## [0.6.0] — 2026-07-23
+
+### Added
+
+- **Post-state-aware guards** — four new vocabulary entries: `swap_k_exact_in` and `swap_k_exact_out` (AMM constant-product preservation: (X±amt)(Y∓dy) ≥ XY), `healthy_position_after` and `healthy_position_after_collateral` (lending post-state per-actor health — borrow and withdraw collateral now model real Aave/Compound semantics). Total: 31 guards.
+- Real-contract example bindings (UniswapV2Swap, AaveLending, CompoundCToken) updated to use the new guards where applicable, tightening model fidelity.
+
 ## [0.5.1] — 2026-07-23
@@ -7,0 +14,0 @@

examples/AaveLending.binding.json

 {
   "model": "lending_pool",
-  "description": "Aave lending pool — deposit, collateral, borrow with health check, repay, withdraw, liquidate. Note: overcollateralized is omitted — aggregate protocol solvency is not a real Aave invariant (underwater positions exist pre-liquidation), and the per-position post-borrow health check requires a post-state-aware guard the current vocabulary cannot express; see README roadmap.",
+  "description": "Aave lending pool — deposit, collateral, borrow with health check, repay, withdraw, liquidate. Note: healthy_position_after and healthy_position_after_collateral guards (new in v0.6.0) now enforce post-state per-actor health on borrow and withdrawCollateral, matching real Aave semantics. overcollateralized remains omitted because the aggregate invariant does not hold when underwater positions exist (which real Aave allows pre-liquidation) — and adding all_positions_healthy as a universal invariant would be falsified by withdrawCollateral without this guard.",
   "functions": [
@@ -17,3 +17,3 @@ {
       "name": "borrow",
-      "guards": ["amt_gt_0", "healthy_position", "not_locked"],
+      "guards": ["amt_gt_0", "healthy_position", "not_locked", "healthy_position_after"],
       "effects": ["reentrancy_lock_acquire", "debt_add", "bal_add_amt", "reentrancy_lock_release"]
@@ -28,3 +28,3 @@ },
       "name": "withdrawCollateral",
-      "guards": ["amt_gt_0", "collateral_ge_amt", "healthy_position", "not_locked"],
+      "guards": ["amt_gt_0", "collateral_ge_amt", "healthy_position", "not_locked", "healthy_position_after_collateral"],
       "effects": ["reentrancy_lock_acquire", "collateral_sub", "bal_add_amt", "reentrancy_lock_release"]
@@ -31,0 +31,0 @@ },

examples/CompoundCToken.binding.json

 {
   "model": "lending_pool",
-  "description": "Compound cToken — mint/redeem for cToken collateral (1:1 with underlying at initial exchange rate), borrow/repay for debt with healthy_position guard. Borrow pulls underlying from pool (total_sub_amt), repay returns it (total_add_amt). Note: overcollateralized is omitted for the same reason as AaveLending — aggregate solvency is not a real Compound invariant and post-borrow health needs post-state-aware guards; see README roadmap.",
+  "description": "Compound cToken — mint/redeem for cToken collateral (1:1 with underlying at initial exchange rate), borrow/repay for debt with healthy_position guard. Borrow pulls underlying from pool (total_sub_amt), repay returns it (total_add_amt). Note: healthy_position_after guard (new in v0.6.0) now enforces post-state per-borrow health, matching real Compound semantics. overcollateralized remains omitted — composite lending invariants require all_positions_healthy which isn't universal without post-redeem guards (future vocab).",
   "functions": [
@@ -17,3 +17,3 @@ {
       "name": "borrow",
-      "guards": ["amt_gt_0", "healthy_position", "total_ge_amt"],
+      "guards": ["amt_gt_0", "healthy_position", "total_ge_amt", "healthy_position_after"],
       "effects": ["debt_add", "bal_add_amt", "total_sub_amt"]
@@ -20,0 +20,0 @@ },

examples/UniswapV2Swap.binding.json

 {
   "model": "amm_pool",
-  "description": "Uniswap V2 pair — constant-product swap with reentrancy lock, add/remove liquidity, swap-exact-output and swap-exact-input. Note: constant_product is omitted — preserving k across swaps requires a multiplicative post-state guard (dy bounded by the xy=k output formula), which the current vocabulary cannot express; see README roadmap.",
+  "description": "Uniswap V2 pair — constant-product swap with reentrancy lock, add/remove liquidity, swap-exact-output and swap-exact-input. Note: swap_k_exact_in and swap_k_exact_out guards (new in v0.6.0) now gate swaps to preserve the constant-product invariant; constant_product remains omitted because removeLiquidity can reduce product below the initial reference point without a proportional-removal guard — future vocab work.",
   "functions": [
     {
       "name": "swap",
-      "guards": ["dy_gt_0", "reserveX_ge_dx", "not_locked"],
+      "guards": ["dy_gt_0", "reserveX_ge_dx", "not_locked", "swap_k_exact_out"],
       "effects": ["reentrancy_lock_acquire", "reserveX_sub", "reserveY_add", "reentrancy_lock_release"]
@@ -12,3 +12,3 @@ },
       "name": "swapExactInput",
-      "guards": ["amt_gt_0", "dy_gt_0", "reserveY_ge_dy", "not_locked"],
+      "guards": ["amt_gt_0", "dy_gt_0", "reserveY_ge_dy", "not_locked", "swap_k_exact_in"],
       "effects": ["reentrancy_lock_acquire", "reserveX_add", "reserveY_sub", "reentrancy_lock_release"]
@@ -15,0 +15,0 @@ },

package.json

 {
   "name": "@kryptosai/counterflow",
-  "version": "0.5.1",
+  "version": "0.6.0",
   "description": "Prove the contract, or reveal the exploit — formal verification for Solidity and DeFi smart contracts. AI-translated invariants proved or refuted by Z3 SMT, with Halmos bytecode backstop and Foundry/Echidna export.",
@@ -5,0 +5,0 @@ "main": "src/verify.js",

README.md

@@ -25,3 +25,3 @@ # <picture><img src="assets/logo.png" height="48" align="left" alt="Counterflow logo"/></picture>Counterflow
         ▼
-  [validate]               deterministic vocabulary/schema gate (5 models, 27 guards, 43 effects, 33 invariants)
+  [validate]               deterministic vocabulary/schema gate (5 models, 31 guards, 43 effects, 33 invariants)
         │
@@ -28,0 +28,0 @@ ▼

solver/models.py

@@ -61,2 +61,3 @@ """
     "collateral_ge_amt", "debt_ge_amt", "healthy_position",
+    "healthy_position_after", "healthy_position_after_collateral",
     # Staking
@@ -68,2 +69,4 @@ "staked_ge_amt", "rewards_ge_amt",
     "price_ge_min", "price_valid", "twap_stale",
+    # AMM — post-state product
+    "swap_k_exact_in", "swap_k_exact_out",
     # Governance
@@ -213,2 +216,8 @@ "timelock_expired",
                          >= Select(s.debt_arr, actor) * BPB)
+        elif g == "healthy_position_after":
+            conds.append(Select(s.collateral, actor) * s.liqThreshold
+                         >= (Select(s.debt_arr, actor) + amt) * BPB)
+        elif g == "healthy_position_after_collateral":
+            conds.append((Select(s.collateral, actor) - amt) * s.liqThreshold
+                         >= Select(s.debt_arr, actor) * BPB)
         elif g == "staked_ge_amt":     conds.append(Select(s.staked, actor) >= amt)
@@ -224,2 +233,10 @@ elif g == "rewards_ge_amt":    conds.append(Select(s.rewards_arr, actor) >= amt)
         elif g == "twap_stale":        conds.append(s.twap_age < amt)
+        elif g == "swap_k_exact_in":
+            if dy is None:
+                raise ValueError("guard swap_k_exact_in requires a dy parameter")
+            conds.append((s.reserveX + amt) * (s.reserveY - dy) >= s.reserveX * s.reserveY)
+        elif g == "swap_k_exact_out":
+            if dy is None:
+                raise ValueError("guard swap_k_exact_out requires a dy parameter")
+            conds.append((s.reserveX - amt) * (s.reserveY + dy) >= s.reserveX * s.reserveY)
         elif g == "timelock_expired":  conds.append(s.timelock_time <= 0)
@@ -226,0 +243,0 @@ else:

src/translate.js

@@ -8,4 +8,4 @@ const { callLLM, extractJSON } = require('./llm');
   'dx_gt_0', 'dy_gt_0', 'reserveX_ge_dx', 'reserveY_ge_dy', 'lp_ge_amt',
-  'collateral_ge_amt', 'debt_ge_amt', 'healthy_position',
-  'staked_ge_amt', 'rewards_ge_amt',
+  'collateral_ge_amt', 'debt_ge_amt', 'healthy_position', 'healthy_position_after', 'healthy_position_after_collateral',
+  'staked_ge_amt', 'swap_k_exact_in', 'swap_k_exact_out', 'rewards_ge_amt',
   'cross_not_in_progress', 'cross_snapshot_match',
@@ -12,0 +12,0 @@ 'price_ge_min', 'price_valid', 'twap_stale',

New alerts

AI-detected potential code anomaly

Supply chain risk

AI has identified unusual behaviors that may pose a security risk.

URL strings

Supply chain risk

Package contains fragments of external URLs or IP addresses, which the package may be accessing at runtime.

Fixed alerts

AI-detected potential code anomaly

Supply chain risk

AI has identified unusual behaviors that may pose a security risk.

URL strings

Supply chain risk

Package contains fragments of external URLs or IP addresses, which the package may be accessing at runtime.

Improved metrics

Total package byte prevSize

2994248

0.07%

Lines of code

5147

0.35%

No dependency changes