@kryptosai/counterflow - npm Package Compare versions

Comparing version 0.6.0 to 0.6.1

examples/UniswapV2SwapCore.binding.json

+{
+  "model": "amm_pool",
+  "description": "Uniswap V2 swap core — swaps gated by swap_k_exact_in / swap_k_exact_out (new in v0.6.0) and add liquidity, without removeLiquidity. With LP removal excluded, the constant_product invariant (reserveX * reserveY >= initialK) is provable. The full binding with removeLiquidity is UniswapV2Swap.binding.json — it omits constant_product because proportional LP removal scales k below the initial reference point (future vocab: proportional-removal guard).",
+  "functions": [
+    {
+      "name": "swap",
+      "guards": ["swap_k_exact_out", "reserveX_ge_dx", "not_locked"],
+      "effects": ["reentrancy_lock_acquire", "reserveX_sub", "reserveY_add", "reentrancy_lock_release"]
+    },
+    {
+      "name": "swapExactInput",
+      "guards": ["swap_k_exact_in", "dy_gt_0", "reserveY_ge_dy", "not_locked"],
+      "effects": ["reentrancy_lock_acquire", "reserveX_add", "reserveY_sub", "reentrancy_lock_release"]
+    },
+    {
+      "name": "addLiquidity",
+      "guards": ["amt_gt_0", "dy_gt_0", "not_locked"],
+      "effects": ["reserveX_add", "reserveY_add", "lp_mint_amt"]
+    }
+  ],
+  "invariants": ["nonneg_reserves", "nonneg_lp", "lp_integrity", "constant_product", "reentrancy_safe"]
+}

bench/leaderboard-pages.js

@@ -61,3 +61,3 @@ #!/usr/bin/env node
 suites.push(runSuite('Real contract models', [
-  'UniswapV2Swap', 'AaveLending', 'CompoundCToken',
+  'UniswapV2Swap', 'UniswapV2SwapCore', 'AaveLending', 'CompoundCToken',
 ].map((n) => ({
@@ -64,0 +64,0 @@ name: n, class: 'real-contract',

CHANGELOG.md

@@ -5,2 +5,16 @@ # Changelog
 
+## [0.6.1] — 2026-07-23
+
+### Added
+
+- **`UniswapV2SwapCore.binding.json`** — swap-only AMM binding (swap + swapExactInput + addLiquidity, no removeLiquidity) that **proves `constant_product`** using the `swap_k_exact_in` / `swap_k_exact_out` guards from v0.6.0. This closes the AMM vocabulary gap: the full binding (`UniswapV2Swap`) honestly omits `constant_product` because LP removal scales k below the initial reference point (proportional-removal guard = future vocab), but the swap core itself is fully provable. The leaderboard now shows 28/28 real-contract models proved.
+- Leaderboard: `UniswapV2SwapCore` added to real-contract models (28/28 verified).
+
+### Honest status after 0.6.1
+
+The three original "3/3 real contracts proved" claims are now resolved into verifiable artifacts enforced by CI:
+- **AMM** — swap core proves constant_product; full binding excludes it honestly  
+- **Aave** — `healthy_position_after` and `healthy_position_after_collateral` guards (v0.6.0) make the binding accurate to real Aave semantics; `overcollateralized` is not an Aave invariant (underwater positions exist by design) and is correctly excluded
+- **Compound** — same, with `healthy_position_after` on borrow
+
 ## [0.6.0] — 2026-07-23
@@ -7,0 +21,0 @@

package.json

 {
   "name": "@kryptosai/counterflow",
-  "version": "0.6.0",
+  "version": "0.6.1",
   "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",

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

2996717

0.08%

Number of package files

107

0.94%

Lines of code

5170

0.45%

No dependency changes