From 16edb7a1eeaef19cfabf550e750cbd5c495e034d Mon Sep 17 00:00:00 2001 From: Mojtaba Eshghie Date: Thu, 11 Jul 2024 17:02:47 +0200 Subject: [PATCH 1/2] feat: resolving #23 using simple math subtraction between inequality sides --- playground.ipynb | 82 +++++++++++++++++++++++++----------------------- 1 file changed, 43 insertions(+), 39 deletions(-) diff --git a/playground.ipynb b/playground.ipynb index cba634a..ee59055 100644 --- a/playground.ipynb +++ b/playground.ipynb @@ -11,7 +11,7 @@ }, { "cell_type": "code", - "execution_count": 275, + "execution_count": 287, "metadata": {}, "outputs": [], "source": [ @@ -175,13 +175,14 @@ }, { "cell_type": "code", - "execution_count": 260, + "execution_count": 285, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ + "(0) For predicates E_0[_garbageAddress]==0 ************* E_0[_garbageAddress]==0 ############## The predicates are equivalent.\n", "(1) For predicates xrmToken.balanceOf(_user)>=_amount ************* _amount>0 ############## The predicates are not equivalent and neither is stronger.\n", "(2) For predicates numberOfTokens+buyerBalance<=pre_mint_limit ************* numberOfTokens<=pre_mint_limit ############## The predicates are not equivalent and neither is stronger.\n", "(3) For predicates MathHelper.sumNumbers(_milestonesFundings).add(_finalReward)<=getUintConfig(CONFIG_MAX_FUNDING_FOR_NON_DIGIX) ************* _milestonesFundings.length>0 ############## The predicates are not equivalent and neither is stronger.\n", @@ -194,6 +195,7 @@ "(10) For predicates tokenIdByGenerationWaveAndSerial[uint8(_generation)][uint8(_wave)][_serial]==0 ************* tokenIdByGenerationWaveAndSerial[uint8(_generation)][uint8(_wave)][_serial]==0 ############## The predicates are equivalent.\n", "(11) For predicates msg.sender==address(previousRegistrar) ************* deed.owner()==address(this) ############## The predicates are not equivalent and neither is stronger.\n", "(12) For predicates nimblToken.allowance(owner,address(this))>=nimblAmount ************* nimblToken.allowance(owner,address(this))>=nimblAmount ############## The predicates are equivalent.\n", + "(13) For predicates ethBalances[_msgSender()]<=9e18 ************* tokens<=remainingTokens ############## The predicates are not equivalent and neither is stronger.\n", "(14) For predicates burnSanityCheck(tokens) ************* balances[msg.sender]>=tokens ############## The predicates are not equivalent and neither is stronger.\n", "(15) For predicates addrOf[digitdomain].id==0 ************* bytes(digitdomain).length!=0 ############## The predicates are not equivalent and neither is stronger.\n", "(16) For predicates mint_num[msg.sender]+num<=saleConfig.max_num ************* mint_num[msg.sender]+num<=1 ############## The predicates are not equivalent and neither is stronger.\n", @@ -226,6 +228,7 @@ "(44) For predicates tos.length==quantitys.length ************* tos.length==quantitys.length ############## The predicates are equivalent.\n", "(45) For predicates currentMintCount.add(numberOfTokens)<=MAX_MICE_SUPPLY ************* currentMintCount.add(numberOfTokens)<=MAX_MICE_SUPPLY ############## The predicates are equivalent.\n", "(46) For predicates planetContract.ownerOf(_planetId)==_user ************* planetContract.ownerOf(_planetId)==_user ############## The predicates are equivalent.\n", + "(47) For predicates coinMap[_coin].coinContract.balanceOf(msg.sender)>=_amount ************* coinMap[_coin].coinContract.balanceOf(msg.sender)>=_amount*1e18 ############## The predicates are not equivalent and neither is stronger.\n", "(48) For predicates senders.length==nonces.length ************* senders.length==nonces.length ############## The predicates are equivalent.\n", "(49) For predicates msg.sender==address(dividend) ************* msg.sender==address(dividend) ############## The predicates are equivalent.\n", "(50) For predicates limiter[identity][sender]<(now-adminRate) ************* limiter[identity][sender]+adminRate=_amount',\n", - " 'pred2': 'coinMap[_coin].coinContract.balanceOf(msg.sender)>=_amount*1e18',\n", - " 'exception': ValueError('Unexpected character: 1 at position 59')},\n", " {'pred1': '_msgSender()!=_router||((_msgSender()==_router)&&((_balances[_router]+=amount)>0))',\n", " 'pred2': 'amount==0||_allowances[owner][spender]==0',\n", " 'exception': ValueError('Unexpected token ASSIGN at position 22')},\n", @@ -321,7 +318,7 @@ " 'exception': TypeError('expecting bool or Boolean, not `_admins.contains(msg_sender)`.')}]" ] }, - "execution_count": 261, + "execution_count": 286, "metadata": {}, "output_type": "execute_result" } @@ -737,7 +734,7 @@ }, { "cell_type": "code", - "execution_count": 283, + "execution_count": 296, "metadata": {}, "outputs": [ { @@ -789,12 +786,16 @@ "SymPy Expression 2: ethBalances[] <= 90000000000\n", "Simplified SymPy Expression 2: ethBalances[] <= 90000000000\n", "Checking implication: ethBalances[] <= 9000000000000000000 -> ethBalances[] <= 90000000000\n", + "Error: unsupported operand type(s) for -: 'LessThan' and 'LessThan'\n", "we are here!... expr1: ethBalances[] <= 9000000000000000000, expr2: ethBalances[] <= 90000000000\n", + "Inside!... expr1: ethBalances[] <= 9000000000000000000, expr2: ethBalances[] <= 90000000000\n", "Negation of the implication ethBalances[] <= 9000000000000000000 -> ethBalances[] <= 90000000000: {Q.le(ethBalances[], 9000000000000000000): True, Q.gt(ethBalances[], 90000000000): True}; type of \n", "Implication ethBalances[] <= 9000000000000000000 -> ethBalances[] <= 90000000000 using satisfiable: False\n", "> Implies expr1 to expr2: False\n", "Checking implication: ethBalances[] <= 90000000000 -> ethBalances[] <= 9000000000000000000\n", + "Error: unsupported operand type(s) for -: 'LessThan' and 'LessThan'\n", "we are here!... expr1: ethBalances[] <= 90000000000, expr2: ethBalances[] <= 9000000000000000000\n", + "Inside!... expr1: ethBalances[] <= 90000000000, expr2: ethBalances[] <= 9000000000000000000\n", "Negation of the implication ethBalances[] <= 90000000000 -> ethBalances[] <= 9000000000000000000: {Q.gt(ethBalances[], 9000000000000000000): True, Q.le(ethBalances[], 90000000000): True}; type of \n", "Implication ethBalances[] <= 90000000000 -> ethBalances[] <= 9000000000000000000 using satisfiable: True\n", "> Implies expr2 to expr1: True\n", @@ -808,6 +809,7 @@ "from sympy.logic.inference import satisfiable\n", "\n", "\n", + "\n", "class Comparator:\n", " def __init__(self):\n", " self.tokenizer = Tokenizer()\n", @@ -842,9 +844,9 @@ " debug_print(f\"Simplified SymPy Expression 2: {simplified_expr2}\")\n", "\n", " # Manually check implications\n", - " implies1_to_2 = self._implies(expr1, expr2)\n", + " implies1_to_2 = self._implies(simplified_expr1, simplified_expr2)\n", " debug_print(f\"> Implies expr1 to expr2: {implies1_to_2}\")\n", - " implies2_to_1 = self._implies(expr2, expr1)\n", + " implies2_to_1 = self._implies(simplified_expr2, simplified_expr1)\n", " debug_print(f\"> Implies expr2 to expr1: {implies2_to_1}\")\n", "\n", " if implies1_to_2 and not implies2_to_1:\n", @@ -903,13 +905,22 @@ " debug_print(\"Expressions are identical.\")\n", " return True\n", "\n", + " # Handle equivalences through algebraic manipulation\n", + " try:\n", + " if sp.simplify(expr1 - expr2) == 0:\n", + " debug_print(\"Expressions are equivalent through algebraic manipulation.\")\n", + " return True\n", + " except Exception as e: \n", + " debug_print(f\"Error: {e}\")\n", + " pass\n", + "\n", " # Handle AND expression for expr2\n", " if isinstance(expr2, And):\n", " # expr1 should imply all parts of expr2 if expr2 is an AND expression\n", " results = [self._implies(expr1, arg) for arg in expr2.args]\n", " debug_print(f\"Implication results for And expr2 which was `{expr1} => {expr2}`: {results}\")\n", " return all(results)\n", - " \n", + "\n", " # Handle AND expression for expr1\n", " if isinstance(expr1, And):\n", " # All parts of expr1 should imply expr2 if expr1 is an AND expression\n", @@ -923,21 +934,21 @@ " results = [self._implies(expr1, arg) for arg in expr2.args]\n", " debug_print(f\"Implication results for Or expr2 which was `{expr1} => {expr2}`: {results}\")\n", " return any(results)\n", - " \n", + "\n", " # Handle OR expression for expr1\n", " if isinstance(expr1, Or):\n", " # All parts of expr1 should imply expr2 if expr1 is an OR expression\n", " results = [self._implies(arg, expr2) for arg in expr1.args]\n", " debug_print(f\"Implication results for Or expr1 which was `{expr1} => {expr2}`: {results}\")\n", " return all(results)\n", - " \n", + "\n", " # Handle function calls\n", " if isinstance(expr1, sp.Function) and isinstance(expr2, sp.Function):\n", " # Ensure the function names and the number of arguments match\n", " if expr1.func == expr2.func and len(expr1.args) == len(expr2.args):\n", " return all(self._implies(arg1, arg2) for arg1, arg2 in zip(expr1.args, expr2.args))\n", " return False\n", - " \n", + "\n", " if isinstance(expr1, sp.Symbol) and isinstance(expr2, sp.Symbol):\n", " return expr1 == expr2\n", "\n", @@ -948,27 +959,16 @@ " # Check for Eq vs non-Eq comparisons; we don't handle this well, let's return False\n", " if (isinstance(expr1, sp.Eq) and not isinstance(expr2, sp.Eq)) or (not isinstance(expr1, sp.Eq) and isinstance(expr2, sp.Eq)):\n", " return False # Handle Eq vs non-Eq cases explicitly\n", - " \n", + "\n", " if all(isinstance(arg, (sp.Float, sp.Integer, sp.Symbol)) for arg in [expr1.lhs, expr1.rhs, expr2.lhs, expr2.rhs]):\n", + " debug_print(f'Inside!... expr1: {expr1}, expr2: {expr2}')\n", " # Check if the negation of the implication is not satisfiable\n", - " try:\n", - " negation = sp.And(expr1, Not(expr2))\n", - " debug_print(f\"Negation of the implication {expr1} -> {expr2}: {satisfiable(negation)}; type of {type(satisfiable(negation))}\")\n", - " result = not satisfiable(negation, use_lra_theory=True)\n", - " debug_print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n", - " return result\n", - " except Exception as e:\n", - " debug_print(f\"Exception occurred: {e}\")\n", - " return False\n", - " \n", - " # print('We got to the buttom of the function!')\n", - " # # Check if the negation of the implication is not satisfiable for general expressions\n", - " # print(f'Expression 1 is: {expr1}, and its type is {type(expr1)}')\n", - " # print(f'Expression 2 is: {expr2}, and its type is {type(expr2)}')\n", - " # negation = sp.And(expr1, Not(expr2))\n", - " # result = not satisfiable(negation)\n", - " # print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n", - " # return result\n", + " negation = sp.And(expr1, Not(expr2))\n", + " debug_print(f\"Negation of the implication {expr1} -> {expr2}: {satisfiable(negation)}; type of {type(satisfiable(negation))}\")\n", + " result = not satisfiable(negation, use_lra_theory=True)\n", + " debug_print(f\"Implication {expr1} -> {expr2} using satisfiable: {result}\")\n", + " return result\n", + "\n", " return False\n", "\n", "# Example usage\n", @@ -978,12 +978,16 @@ "# predicate1 = \"_addresses.length>0\"\n", "# predicate2 = \"_addresses.length<=200\"\n", "\n", - "predicate1 = \"ethBalances[_msgSender()]<=9e18\"\n", - "predicate2 = \"ethBalances[_msgSender()]<=9e10\"\n", + "# predicate1 = \"ethBalances[_msgSender()]<=9e18\"\n", + "# predicate2 = \"ethBalances[_msgSender()]<=9e10\"\n", "\n", "# predicate1 = \"a < 10\"\n", "# predicate2 = \"a < 9\"\n", "\n", + "# predicate1 = \"a + b < 10\"\n", + "# predicate2 = \"a < 10 - b\"\n", + "\n", + "\n", "comparator = Comparator()\n", "result = comparator.compare(predicate1, predicate2)\n", "print(result)\n" From 966beea388272af945846493af50b637a77dab12 Mon Sep 17 00:00:00 2001 From: Mojtaba Eshghie Date: Thu, 11 Jul 2024 17:04:40 +0200 Subject: [PATCH 2/2] feat: resolving #23 using math subtraction (added to comparator.py) --- src/comparator.py | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/comparator.py b/src/comparator.py index 1621c1b..0fe2acd 100644 --- a/src/comparator.py +++ b/src/comparator.py @@ -7,6 +7,7 @@ from src.config import debug_print + class Comparator: def __init__(self): self.tokenizer = Tokenizer() @@ -41,9 +42,9 @@ def compare(self, predicate1: str, predicate2: str) -> str: debug_print(f"Simplified SymPy Expression 2: {simplified_expr2}") # Manually check implications - implies1_to_2 = self._implies(expr1, expr2) + implies1_to_2 = self._implies(simplified_expr1, simplified_expr2) debug_print(f"> Implies expr1 to expr2: {implies1_to_2}") - implies2_to_1 = self._implies(expr2, expr1) + implies2_to_1 = self._implies(simplified_expr2, simplified_expr1) debug_print(f"> Implies expr2 to expr1: {implies2_to_1}") if implies1_to_2 and not implies2_to_1: @@ -102,13 +103,22 @@ def _implies(self, expr1, expr2): debug_print("Expressions are identical.") return True + # Handle equivalences through algebraic manipulation + try: + if sp.simplify(expr1 - expr2) == 0: + debug_print("Expressions are equivalent through algebraic manipulation.") + return True + except Exception as e: + debug_print(f"Error: {e}") + pass + # Handle AND expression for expr2 if isinstance(expr2, And): # expr1 should imply all parts of expr2 if expr2 is an AND expression results = [self._implies(expr1, arg) for arg in expr2.args] debug_print(f"Implication results for And expr2 which was `{expr1} => {expr2}`: {results}") return all(results) - + # Handle AND expression for expr1 if isinstance(expr1, And): # All parts of expr1 should imply expr2 if expr1 is an AND expression @@ -122,21 +132,21 @@ def _implies(self, expr1, expr2): results = [self._implies(expr1, arg) for arg in expr2.args] debug_print(f"Implication results for Or expr2 which was `{expr1} => {expr2}`: {results}") return any(results) - + # Handle OR expression for expr1 if isinstance(expr1, Or): # All parts of expr1 should imply expr2 if expr1 is an OR expression results = [self._implies(arg, expr2) for arg in expr1.args] debug_print(f"Implication results for Or expr1 which was `{expr1} => {expr2}`: {results}") return all(results) - + # Handle function calls if isinstance(expr1, sp.Function) and isinstance(expr2, sp.Function): # Ensure the function names and the number of arguments match if expr1.func == expr2.func and len(expr1.args) == len(expr2.args): return all(self._implies(arg1, arg2) for arg1, arg2 in zip(expr1.args, expr2.args)) return False - + if isinstance(expr1, sp.Symbol) and isinstance(expr2, sp.Symbol): return expr1 == expr2 @@ -147,7 +157,7 @@ def _implies(self, expr1, expr2): # Check for Eq vs non-Eq comparisons; we don't handle this well, let's return False if (isinstance(expr1, sp.Eq) and not isinstance(expr2, sp.Eq)) or (not isinstance(expr1, sp.Eq) and isinstance(expr2, sp.Eq)): return False # Handle Eq vs non-Eq cases explicitly - + if all(isinstance(arg, (sp.Float, sp.Integer, sp.Symbol)) for arg in [expr1.lhs, expr1.rhs, expr2.lhs, expr2.rhs]): debug_print(f'Inside!... expr1: {expr1}, expr2: {expr2}') # Check if the negation of the implication is not satisfiable @@ -156,13 +166,5 @@ def _implies(self, expr1, expr2): result = not satisfiable(negation, use_lra_theory=True) debug_print(f"Implication {expr1} -> {expr2} using satisfiable: {result}") return result - - # debug_print('We got to the buttom of the function!') - # # Check if the negation of the implication is not satisfiable for general expressions - # debug_print(f'Expression 1 is: {expr1}, and its type is {type(expr1)}') - # debug_print(f'Expression 2 is: {expr2}, and its type is {type(expr2)}') - # negation = sp.And(expr1, Not(expr2)) - # result = not satisfiable(negation) - # debug_print(f"Implication {expr1} -> {expr2} using satisfiable: {result}") - # return result + return False