Contract storage fields in CSE #571

anvacaru · 2024-05-17T16:15:40Z

~~Blocked on : #570 to bring in the changes from runtimeverification/evm-semantics#2433 to clean some of the code first.~~

First PR for #362:

extending the StorageField class to store the numberOfBytes property
implementing _create_initial_storage in prove.py that creates the KAst representation of the storage layout for a given set of storage fields.
This representation is used to populate the storage of CONTRACT_ID symbolic account in CSE only.
For now supporting just uint*, address and bool

src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected

PetarMax · 2024-05-24T09:18:46Z

There is a problem with test_add_const in CSE, it would appear the summaries are not getting used. Investigating now.

PetarMax · 2024-05-24T11:15:57Z

src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected

-┃  │  (464 steps)
-┃  └─ 12 (vacuous, leaf)
-┃      k: #execute ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K
+┃  │  (979 steps)


This increase is due to a problem with the specification of setConst.

PetarMax · 2024-05-24T11:16:08Z

src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected

-   │  (1123 steps)
-   ├─ 13 (terminal)
+   │  (1417 steps)


This increase is due to a problem with the specification of setConst.

PetarMax · 2024-05-24T11:47:00Z

We have a problem. By setting the storage in this way, we cannot use the generated specifications when a slot has not been explicitly initialised---this, for example, is the case for the AddConst.setConst function, where slot 0 holds an uint256 and whose specification has

<storage>
  ( 0 |-> ( SF_C:Int => VV0_x_114b9705:Int ) )
</storage>

but when the CSETest.test_add_const initialises the AddConst contract, the storage is set to

<storage>
  .Map
</storage>

implicitly having all slots set to zero and using #lookup to leverage this implicitness. As a result, the specification of setConst is not used in test_add_const, and this is visible in the increase of steps in the expected outpute here and here.

I have two solutions in mind, first more favourable than the second, I think:

We do not create an explicit storage layout, but instead have a fully symbolic storage and work in terms of #lookup and &Int / >>Int masks and shifts, just like the compiler does. For the setConst contract, this would mean just introducing the constraints 0 <=Int #lookup(STORAGE, 0) andBool #lookup(STORAGE, 0) <Int pow256, which actually hold by construction, and the specification would have <storage> STORAGE => STORAGE [ 0 <-| VV0_x_114b9705:Int ] </storage>. I see the following pros and cons
- Pros: resilient to presence or absence of explicit fields in storage, can handle all storage constructs;
- Cons: more complex expressions in the path constraint, hindering readability and potentially slowing down execution.
We create an explicit storage layout as much as we can for tests as well. I am not sure how this would be done other than intercepting constructor calls, and it would not be feasible for mappings, which would have to remain implicit in the style of solution 1.

@anvacaru, @ehildenb, @palinatolmach, let's discuss this a bit, please. Other ideas welcome.

anvacaru · 2024-05-24T12:58:27Z

Closing this since we won't merge it.

PetarMax · 2024-05-31T10:12:34Z

src/kontrol/solc_to_k.py

+def type_constraint(data_type: str, symbolic_var: KVariable) -> KApply:
+    # TODO: fill with rest of the cases
+    data_type = data_type.lower()
+    if data_type.startswith('uint'):
+        return mlEqualsTrue(KEVM.range_uint(int(data_type[4:]), symbolic_var))
+
+    match data_type:
+        case 'address':
+            return mlEqualsTrue(KEVM.range_address(symbolic_var))
+        case 'bool':
+            return mlEqualsTrue(KEVM.range_bool(symbolic_var))
+        case _:
+            raise ValueError(f'Unimplemented: {data_type}')


Note: This will be useful for future.

PetarMax · 2024-05-31T10:12:34Z

src/kontrol/solc_to_k.py

+def type_constraint(data_type: str, symbolic_var: KVariable) -> KApply:
+    # TODO: fill with rest of the cases
+    data_type = data_type.lower()
+    if data_type.startswith('uint'):
+        return mlEqualsTrue(KEVM.range_uint(int(data_type[4:]), symbolic_var))
+
+    match data_type:
+        case 'address':
+            return mlEqualsTrue(KEVM.range_address(symbolic_var))
+        case 'bool':
+            return mlEqualsTrue(KEVM.range_bool(symbolic_var))
+        case _:
+            raise ValueError(f'Unimplemented: {data_type}')


Note: this will be useful in future.

anvacaru added 3 commits May 17, 2024 18:45

solc_to_k.py: add length field to StorageField

fe72c6d

prove.py: encode storage layout in kast

ae14033

update expected output

cff7dff

anvacaru self-assigned this May 17, 2024

devops and others added 2 commits May 17, 2024 16:15

Set Version: 0.1.281

d36f419

prove.py: apply storage field constraints only for symbolic exploration

6b55465

anvacaru requested review from PetarMax, tothtamas28 and palinatolmach and removed request for PetarMax May 20, 2024 06:41

anvacaru added enhancement New feature or request cse labels May 20, 2024

PetarMax and others added 2 commits May 20, 2024 12:09

Merge branch 'master' into storage-field2

c9304eb

Set Version: 0.1.282

641ce6c

PetarMax reviewed May 20, 2024

View reviewed changes

src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected Outdated Show resolved Hide resolved

anvacaru and others added 5 commits May 20, 2024 13:45

prove.py: use KAst helper functions

ebe458d

prove.py: store fields as words

1e86af9

Merge remote-tracking branch 'origin/master' into storage-field2

39bd29e

update expected output

f759350

Set Version: 0.1.283

a792b72

palinatolmach approved these changes May 21, 2024

View reviewed changes

anvacaru and others added 2 commits May 22, 2024 08:50

Merge branch 'master' into storage-field2

7353ad5

Set Version: 0.1.284

5ed0d5d

palinatolmach mentioned this pull request May 22, 2024

Use structured symbolic storage with symbolicStorage/--symbolic-storage #577

Open

anvacaru and others added 2 commits May 23, 2024 14:05

Merge branch 'master' into storage-field2

2dca1d5

Set Version: 0.1.285

e3b2ba9

PetarMax added the do not merge Do not merge this PR while label present label May 24, 2024

Merge branch 'master' into storage-field2

c762d87

Set Version: 0.1.286

c75471a

PetarMax reviewed May 24, 2024

View reviewed changes

anvacaru closed this May 24, 2024

PetarMax reviewed May 31, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Contract storage fields in CSE #571

Contract storage fields in CSE #571

anvacaru commented May 17, 2024 •

edited

PetarMax commented May 24, 2024

PetarMax May 24, 2024

PetarMax May 24, 2024

PetarMax commented May 24, 2024

anvacaru commented May 24, 2024

PetarMax May 31, 2024

PetarMax May 31, 2024

Contract storage fields in CSE #571

Contract storage fields in CSE #571

Conversation

anvacaru commented May 17, 2024 • edited

PetarMax commented May 24, 2024

PetarMax May 24, 2024

Choose a reason for hiding this comment

PetarMax May 24, 2024

Choose a reason for hiding this comment

PetarMax commented May 24, 2024

anvacaru commented May 24, 2024

PetarMax May 31, 2024

Choose a reason for hiding this comment

PetarMax May 31, 2024

Choose a reason for hiding this comment

anvacaru commented May 17, 2024 •

edited