Skip to content

Commit

Permalink
Merge pull request #31 from mojtaba-eshghie/feat_issue_28
Browse files Browse the repository at this point in the history 
Feat issue 28
  • Loading branch information
@mojtaba-eshghie
mojtaba-eshghie authored Jul 11, 2024
2 parents a42e1cf + 966beea commit 8643883
Show file tree
Hide file tree
Showing 2 changed files with 61 additions and 55 deletions.
82 changes: 43 additions & 39 deletions playground.ipynb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
},
{
"cell_type": "code",
"execution_count": 275,
"execution_count": 287,
"metadata": {},
"outputs": [],
"source": [
Expand Down Expand Up @@ -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",
Expand All @@ -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",
Expand Down Expand Up @@ -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<now ############## The predicates are not equivalent and neither is stronger.\n",
Expand Down Expand Up @@ -298,21 +301,15 @@
},
{
"cell_type": "code",
"execution_count": 261,
"execution_count": 286,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"[{'pred1': 'ethBalances[_msgSender()]<=9e18',\n",
" 'pred2': 'tokens<=remainingTokens',\n",
" 'exception': ValueError('Unexpected character: 9 at position 27')},\n",
" {'pred1': '_poolIndexFromPosted(postedSwap)==0',\n",
"[{'pred1': '_poolIndexFromPosted(postedSwap)==0',\n",
" 'pred2': '(postedSwap&poolIndex)==0',\n",
" 'exception': ValueError('Expected token RPAREN but got BITWISE_AND at position 2')},\n",
" {'pred1': 'coinMap[_coin].coinContract.balanceOf(msg.sender)>=_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",
Expand All @@ -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"
}
Expand Down Expand Up @@ -737,7 +734,7 @@
},
{
"cell_type": "code",
"execution_count": 283,
"execution_count": 296,
"metadata": {},
"outputs": [
{
Expand Down Expand Up @@ -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 <class 'dict'>\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 <class 'dict'>\n",
"Implication ethBalances[] <= 90000000000 -> ethBalances[] <= 9000000000000000000 using satisfiable: True\n",
"> Implies expr2 to expr1: True\n",
Expand All @@ -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",
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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",
Expand All @@ -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",
Expand All @@ -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",
Expand All @@ -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"
Expand Down
34 changes: 18 additions & 16 deletions src/comparator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
from src.config import debug_print



class Comparator:
def __init__(self):
self.tokenizer = Tokenizer()
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand All @@ -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
Expand All @@ -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

0 comments on commit 8643883

Please sign in to comment.