Merge branch 'master' into _update-deps/runtimeverification/k

anvacaru · web-flow · commit 2af889835abb · 2025-11-28T19:52:18.000+02:00
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -410,6 +410,7 @@ def _add_account_invariant(account: KApply) -> list[KApply]:
         )
         constraints.append(mlEqualsTrue(ltInt(KEVM.size_bytes(cterm.cell('CALLDATA_CELL')), KEVM.pow128())))
         constraints.append(mlEqualsTrue(KEVM.range_uint(256, cterm.cell('CALLVALUE_CELL'))))
+        constraints.append(mlEqualsTrue(KEVM.range_uint(256, cterm.cell('MIXHASH_CELL'))))
 
         constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('ORIGIN_CELL'))))
         constraints.append(

Original file line number	Diff line number	Diff line change
`@@ -410,6 +410,7 @@ def _add_account_invariant(account: KApply) -> list[KApply]:`
`410`	`410`	`)`
`411`	`411`	`constraints.append(mlEqualsTrue(ltInt(KEVM.size_bytes(cterm.cell('CALLDATA_CELL')), KEVM.pow128())))`
`412`	`412`	`constraints.append(mlEqualsTrue(KEVM.range_uint(256, cterm.cell('CALLVALUE_CELL'))))`
	`413`	`+ constraints.append(mlEqualsTrue(KEVM.range_uint(256, cterm.cell('MIXHASH_CELL'))))`
`413`	`414`
`414`	`415`	`constraints.append(mlEqualsTrue(KEVM.range_address(cterm.cell('ORIGIN_CELL'))))`
`415`	`416`	`constraints.append(`