Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feat issue 28 #31

Merged
merged 2 commits into from
Jul 11, 2024
Merged

Feat issue 28 #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
16edb7a
feat: resolving #23 using simple math subtraction between inequality …
mojtaba-eshghie Jul 11, 2024
966beea
feat: resolving #23 using math subtraction (added to comparator.py)
mojtaba-eshghie Jul 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 43 additions & 39 deletions playground.ipynb
View file
Open in desktop
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
Open in desktop
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
Loading