Skip to content

Commit aeef1bd

Browse files
StevengreStevengre
authored
Simplify the summary rules for DUP, SWAP, and LOG. (#2726)
- Introduced a new static method `size_wordstack` in the KEVM class to calculate the size of the word stack. - Refactored the `stack_needed` function to return a single integer instead of a list, simplifying the logic for opcode stack size requirements. - Updated the `build_spec` method in KEVMSummarizer to utilize the new `size_wordstack` method and adjusted constraints for specific opcodes (DUP, SWAP, LOG). - Removed time-consuming opcode summarization skips in the test_summarize.py file to streamline testing.
1 parent 710742c commit aeef1bd

File tree

3 files changed

+82
-73
lines changed

3 files changed

+82
-73
lines changed

‎kevm-pyk/src/kevm_pyk/kevm.py

+4
Original file line numberDiff line numberDiff line change
@@ -523,6 +523,10 @@ def bool_2_word(cond: KInner) -> KApply:
523523
def size_bytes(ba: KInner) -> KApply:
524524
return KApply('lengthBytes(_)_BYTES-HOOKED_Int_Bytes', [ba])
525525

526+
@staticmethod
527+
def size_wordstack(ws: KInner) -> KApply:
528+
return KApply('#sizeWordStack', [ws])
529+
526530
@staticmethod
527531
def inf_gas(g: KInner) -> KApply:
528532
return KApply('infGas', [g])

‎kevm-pyk/src/kevm_pyk/summarizer.py

+77-66
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@
1515
from pyk.kcfg import KCFG, KCFGExplore
1616
from pyk.kdist import kdist
1717
from pyk.kore.rpc import KoreClient
18-
from pyk.prelude.kint import euclidModInt
19-
from pyk.prelude.ml import mlEquals, mlEqualsFalse, mlNot
18+
from pyk.prelude.kint import addInt, euclidModInt, leInt
19+
from pyk.prelude.ml import mlEquals, mlEqualsFalse, mlEqualsTrue, mlNot
2020
from pyk.proof import APRProof
2121
from pyk.proof.show import APRProofShow
2222
from pyk.utils import ensure_dir_path
@@ -286,30 +286,28 @@ def get_todo_list() -> list[str]:
286286
return todo_list
287287

288288

289-
def stack_needed(opcode_id: str) -> list[int]:
289+
def stack_needed(opcode_id: str) -> int:
290290
"""
291291
Return the stack size needed for the opcode, corresponding `#stackNeeded` in the semantics.
292292
"""
293293
opcode = OPCODES[opcode_id].label.name
294294
if 'CallOp' in opcode:
295-
return [7]
295+
return 7
296296
elif 'CallSixOp' in opcode:
297-
return [6]
297+
return 6
298298
elif 'LOG' in opcode:
299-
return list(range(5))
299+
return 2
300300
elif 'SWAP' in opcode:
301-
return list(range(1, 17))
302-
elif 'DUP' in opcode:
303-
return list(range(1, 17))
301+
return 1
304302
elif 'QuadStackOp' in opcode:
305-
return [4]
303+
return 4
306304
elif 'TernStackOp' in opcode:
307-
return [3]
305+
return 3
308306
elif 'BinStackOp' in opcode:
309-
return [2]
307+
return 2
310308
elif 'UnStackOp' in opcode:
311-
return [1]
312-
return [0]
309+
return 1
310+
return 0
313311

314312

315313
def accounts_cell(acct_id: str | KInner, exists: bool = True) -> tuple[KInner, KInner]:
@@ -451,59 +449,72 @@ def _build_spec(
451449
return APRProof.from_claim(self.kevm.definition, kclaim[0], {}, self.proof_dir)
452450

453451
def build_spec(self, opcode_symbol: str) -> list[APRProof]:
454-
needs = stack_needed(opcode_symbol)
452+
453+
def _ws_size(s: int) -> KInner:
454+
return KEVM.size_wordstack(KEVM.wordstack(s))
455+
456+
def _le(a: KInner, b: KInner) -> KInner:
457+
return mlEqualsTrue(leInt(a, b))
458+
459+
need = stack_needed(opcode_symbol)
455460
opcode = OPCODES[opcode_symbol]
456-
proofs = []
457-
for need in needs:
458-
if len(needs) > 1:
459-
opcode = KApply(opcode.label.name, KToken(str(need), KSort('Int')))
460-
461-
# (opcode, init_subst, init_constraints, final_subst, final_constraints, id_str)
462-
specs: list[tuple[KApply, dict[str, KInner], list[KInner], dict[str, KInner], list[KInner], str]] = []
463-
init_subst: dict[str, KInner] = {}
464-
final_subst: dict[str, KInner] = {}
465-
466-
if opcode_symbol in NOT_USEGAS_OPCODES:
467-
# TODO: Should allow infGas to calculate gas. Skip for now.
468-
init_subst['USEGAS_CELL'] = KToken('false', KSort('Bool'))
469-
470-
if opcode_symbol in ACCOUNT_QUERIES_OPCODES:
471-
w0 = KVariable('W0', KSort('Int'))
472-
pow160 = KToken(str(pow(2, 160)), KSort('Int'))
473-
474-
cell, constraint = accounts_cell(euclidModInt(w0, pow160), exists=False)
475-
init_subst['ACCOUNTS_CELL'] = cell
476-
# TODO: BALANCE doesn't need the above spec. Maybe a bug in the backend.
477-
specs.append((opcode, init_subst, [constraint], {}, [], '_OWISE'))
478-
479-
cell, constraint = accounts_cell(euclidModInt(w0, pow160), exists=True)
480-
init_subst['ACCOUNTS_CELL'] = cell
481-
specs.append((opcode, init_subst, [constraint], {}, [], '_NORMAL'))
482-
elif opcode_symbol in ACCOUNT_STORAGE_OPCODES or opcode_symbol == 'SELFBALANCE':
483-
cell, constraint = accounts_cell('ID_CELL')
484-
init_subst['ACCOUNTS_CELL'] = cell
485-
specs.append((opcode, init_subst, [constraint], {}, [], ''))
486-
elif opcode_symbol == 'JUMP':
487-
final_subst['K_CELL'] = KSequence([KEVM.end_basic_block(), KVariable('K_CELL')])
488-
specs.append((opcode, init_subst, [], final_subst, [], ''))
489-
elif opcode_symbol == 'JUMPI':
490-
constraint = mlEquals(KVariable('W1', KSort('Int')), KToken('0', KSort('Int')), 'Int')
491-
specs.append((opcode, init_subst, [constraint], {}, [], '_FALSE'))
492-
493-
constraint = mlNot(mlEquals(KVariable('W1', KSort('Int')), KToken('0', KSort('Int')), 'Int'))
494-
final_subst['K_CELL'] = KSequence([KEVM.end_basic_block(), KVariable('K_CELL')])
495-
specs.append((opcode, init_subst, [], final_subst, [], '_TRUE'))
496-
elif opcode_symbol == 'LOG':
497-
need += 2
498-
specs.append((opcode, init_subst, [], final_subst, [], ''))
499-
else:
500-
specs.append((opcode, init_subst, [], final_subst, [], ''))
501-
502-
for spec in specs:
503-
proof = self._build_spec(spec[0], need, spec[1], spec[2], spec[3], spec[4], id_str=spec[5])
504-
proofs.append(proof)
505-
506-
return proofs
461+
462+
if opcode_symbol in ['DUP', 'SWAP', 'LOG']:
463+
opcode = KApply(opcode.label.name, KVariable('N', KSort('Int')))
464+
465+
# (opcode, init_subst, init_constraints, final_subst, final_constraints, id_str)
466+
specs: list[tuple[KApply, dict[str, KInner], list[KInner], dict[str, KInner], list[KInner], str]] = []
467+
init_subst: dict[str, KInner] = {}
468+
final_subst: dict[str, KInner] = {}
469+
470+
if opcode_symbol in NOT_USEGAS_OPCODES:
471+
# TODO: Should allow infGas to calculate gas. Skip for now.
472+
init_subst['USEGAS_CELL'] = KToken('false', KSort('Bool'))
473+
474+
if opcode_symbol in ACCOUNT_QUERIES_OPCODES:
475+
w0 = KVariable('W0', KSort('Int'))
476+
pow160 = KToken(str(pow(2, 160)), KSort('Int'))
477+
478+
cell, constraint = accounts_cell(euclidModInt(w0, pow160), exists=False)
479+
init_subst['ACCOUNTS_CELL'] = cell
480+
# TODO: BALANCE doesn't need the above spec. Maybe a bug in the backend.
481+
specs.append((opcode, init_subst, [constraint], {}, [], '_OWISE'))
482+
483+
cell, constraint = accounts_cell(euclidModInt(w0, pow160), exists=True)
484+
init_subst['ACCOUNTS_CELL'] = cell
485+
specs.append((opcode, init_subst, [constraint], {}, [], '_NORMAL'))
486+
elif opcode_symbol in ACCOUNT_STORAGE_OPCODES or opcode_symbol == 'SELFBALANCE':
487+
cell, constraint = accounts_cell('ID_CELL')
488+
init_subst['ACCOUNTS_CELL'] = cell
489+
specs.append((opcode, init_subst, [constraint], {}, [], ''))
490+
elif opcode_symbol == 'JUMP':
491+
final_subst['K_CELL'] = KSequence([KEVM.end_basic_block(), KVariable('K_CELL')])
492+
specs.append((opcode, init_subst, [], final_subst, [], ''))
493+
elif opcode_symbol == 'JUMPI':
494+
constraint = mlEquals(KVariable('W1', KSort('Int')), KToken('0', KSort('Int')), 'Int')
495+
specs.append((opcode, init_subst, [constraint], {}, [], '_FALSE'))
496+
497+
constraint = mlNot(mlEquals(KVariable('W1', KSort('Int')), KToken('0', KSort('Int')), 'Int'))
498+
final_subst['K_CELL'] = KSequence([KEVM.end_basic_block(), KVariable('K_CELL')])
499+
specs.append((opcode, init_subst, [], final_subst, [], '_TRUE'))
500+
elif opcode_symbol == 'DUP':
501+
init_constraints: list[KInner] = [_le(KVariable('N', 'Int'), _ws_size(0))]
502+
init_constraints.append(_le(_ws_size(0), KToken('1023', 'Int')))
503+
specs.append((opcode, init_subst, init_constraints, final_subst, [], ''))
504+
elif opcode_symbol == 'SWAP':
505+
init_constraints = [_le(addInt(KVariable('N', 'Int'), KToken('1', 'Int')), _ws_size(1))]
506+
init_constraints.append(_le(_ws_size(1), KToken('1023', 'Int')))
507+
specs.append((opcode, init_subst, init_constraints, final_subst, [], ''))
508+
elif opcode_symbol == 'LOG':
509+
init_constraints = [_le(addInt(KVariable('N', 'Int'), KToken('2', 'Int')), _ws_size(2))]
510+
init_constraints.append(_le(KVariable('N', 'Int'), _ws_size(0)))
511+
init_constraints.append(_le(_ws_size(2), addInt(KVariable('N', 'Int'), KToken('1026', 'Int'))))
512+
init_subst['STATIC_CELL'] = KToken('false', KSort('Bool'))
513+
specs.append((opcode, init_subst, init_constraints, final_subst, [], ''))
514+
else:
515+
specs.append((opcode, init_subst, [], final_subst, [], ''))
516+
517+
return [self._build_spec(spec[0], need, spec[1], spec[2], spec[3], spec[4], spec[5]) for spec in specs]
507518

508519
def explore(self, proof: APRProof) -> bool:
509520
"""

‎kevm-pyk/src/tests/integration/test_summarize.py

+1-7
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,7 @@ def test_summarize(opcode: str) -> None:
1010
if get_summary_status(opcode) != 'PASSED':
1111
pytest.skip(f'{opcode} status: {OPCODES_SUMMARY_STATUS[opcode]}')
1212

13-
if opcode in ['DUP', 'SWAP', 'LOG']:
14-
pytest.skip(f'{opcode} summarization is time-consuming')
15-
16-
print(f'[{opcode}] selected')
17-
summarizer, proofs = summarize(opcode)
18-
print(f'[{opcode}] summarize finished')
19-
print(f'[{opcode}] {len(proofs)} proofs generated')
13+
_, proofs = summarize(opcode)
2014

2115
for proof in proofs:
2216
claims: list[KRuleLike] = []

0 commit comments

Comments
 (0)