Skip to content

Commit

Permalink
Support symbolic contract storage slots with nonzero offsets (#663)
Browse files Browse the repository at this point in the history 
* Add symbolic contract storage slot with nonzero offsets

* Set Version: 0.1.334

* Add lemmas for offset symbolic storage structure

* Generalize asWord lemma, fix symbolic bytes lemma

* Set Version: 0.1.341

* Set Version: 0.1.347

* Set Version: 0.1.348

* Switch to using bytes for rest of storage slot

* Re-add lemmas

* Update expected output

* update expected output

* Update contract.k expected

* Set Version: 0.1.349

* Update expected output

* Set Version: 0.1.350

* Set Version: 0.1.351

* Set Version: 0.1.353

* Replace lemma, make +Bytes term right-associated

* Set Version: 0.1.356

* Set Version: 0.1.359

* Change before/after ordering

* Use different lemma

* Set Version: 0.1.360

* Update expected

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Palina Tolmach <[email protected]>
  • Loading branch information
@nwatson22 @palinatolmach
3 people authored Jul 23, 2024
1 parent 5c6ebeb commit 359f183
Show file tree
Hide file tree
Showing 6 changed files with 70 additions and 14 deletions.
53 changes: 49 additions & 4 deletions src/kontrol/prove.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1153,10 +1153,55 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner:
'_Map_', [map_item(intToken(field.slot), contract_account_variable), storage_map]
)
else:
# TODO: Support shared slots for contract variables
raise (
ValueError(
'Unsupported: CSE for contracts with contract or interface fields in shared slots.'
slot_var_before = KVariable(f'{field_name}_SLOT_BEFORE', sort=KSort('Bytes'))
slot_var_after = KVariable(f'{field_name}_SLOT_AFTER', sort=KSort('Bytes'))
masked_contract_account_var = KApply(
'asWord',
[
KApply(
'_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes',
[
slot_var_before,
KApply(
'_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes',
[
KEVM.buf(intToken(20), contract_account_variable),
slot_var_after,
],
),
],
)
],
)
storage_map = KApply(
'_Map_', [map_item(intToken(field.slot), masked_contract_account_var), storage_map]
)
new_account_constraints.append(
mlEqualsTrue(
KApply(
'_==K_',
[
KApply(
'lengthBytes(_)_BYTES-HOOKED_Int_Bytes',
[slot_var_after],
),
intToken(field.offset),
],
)
)
)
new_account_constraints.append(
mlEqualsTrue(
KApply(
'_==K_',
[
KApply(
'lengthBytes(_)_BYTES-HOOKED_Int_Bytes',
[slot_var_before],
),
intToken(32 - 20 - field.offset),
],
)
)
)

Expand Down
4 changes: 4 additions & 0 deletions src/tests/integration/test-data/cse-lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,10 @@ module CSE-LEMMAS
andBool X +Int 1 <=Int A
[concrete(X), simplification, preserves-definedness]

rule { #asWord ( X ) #Equals #asWord ( Y ) } => { X #Equals Y }
requires lengthBytes(X) ==Int lengthBytes(Y) andBool lengthBytes(X) <=Int 32
[simplification]

endmodule

module CSE-LEMMAS-SPEC
Expand Down
3 changes: 2 additions & 1 deletion src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ contract TToken {
}

contract TEscrow {
bool spacer;
TToken token;

constructor(address _token) {
Expand Down Expand Up @@ -53,4 +54,4 @@ contract ContractFieldTest is Test {
function testEscrowToken() public {
assert(escrow.getTokenTotalSupply() == 12345);
}
}
}
4 changes: 2 additions & 2 deletions src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
│
│ (2219 steps)
│ (2231 steps)
├─ 8 (terminal)
│ k: #halt ~> CONTINUATION:K
│ pc: 194
Expand Down Expand Up @@ -130,7 +130,7 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0
0
</balance>
<storage>
( .Map => ( 0 |-> 491460923342184218035706888008750043977755113263 ) )
( .Map => ( 0 |-> 125813996375599159817140963330240011258305308995328 ) )
</storage>
<origStorage>
.Map
Expand Down
18 changes: 12 additions & 6 deletions src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
C_TGOVERNANCE_ESCROW_BAL:Int
</balance>
<storage>
( ( 0 |-> C_TGOVERNANCE_ESCROW_TOKEN_ID:Int )
( ( 0 |-> #asWord ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_BEFORE:Bytes +Bytes #buf ( 20 , C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ) +Bytes C_TGOVERNANCE_ESCROW_TOKEN_SLOT_AFTER:Bytes ) )
C_TGOVERNANCE_ESCROW_STORAGE:Map )
</storage>
<nonce>
Expand Down Expand Up @@ -276,8 +276,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
andBool ( 1024 <=Int CALLDEPTH_CELL:Int
andBool ( 0 <=Int C_TGOVERNANCE_NONCE:Int
andBool ( C_TGOVERNANCE_ESCROW_ID:Int =/=Int C_TGOVERNANCE_ID:Int
andBool ( 1 ==Int lengthBytes ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_AFTER:Bytes )
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_ID:Int
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_BAL:Int
andBool ( 11 ==Int lengthBytes ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_BEFORE:Bytes )
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_NONCE:Int
andBool ( C_TGOVERNANCE_ESCROW_TOKEN_ID:Int =/=Int C_TGOVERNANCE_ID:Int
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_TOKEN_ID:Int
Expand Down Expand Up @@ -318,7 +320,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_TOKEN_ID:Int <= 9 ) )
)))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))
[priority(20), label(BASIC-BLOCK-13-TO-7)]

rule [BASIC-BLOCK-16-TO-10]: <foundry>
Expand Down Expand Up @@ -413,7 +415,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
C_TGOVERNANCE_ESCROW_BAL:Int
</balance>
<storage>
( ( 0 |-> C_TGOVERNANCE_ESCROW_TOKEN_ID:Int )
( ( 0 |-> #asWord ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_BEFORE:Bytes +Bytes #buf ( 20 , C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ) +Bytes C_TGOVERNANCE_ESCROW_TOKEN_SLOT_AFTER:Bytes ) )
C_TGOVERNANCE_ESCROW_STORAGE:Map )
</storage>
<nonce>
Expand Down Expand Up @@ -519,8 +521,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
andBool ( 0 <=Int C_TGOVERNANCE_BAL:Int
andBool ( 0 <=Int C_TGOVERNANCE_NONCE:Int
andBool ( C_TGOVERNANCE_ESCROW_ID:Int =/=Int C_TGOVERNANCE_ID:Int
andBool ( 1 ==Int lengthBytes ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_AFTER:Bytes )
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_ID:Int
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_BAL:Int
andBool ( 11 ==Int lengthBytes ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_BEFORE:Bytes )
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_NONCE:Int
andBool ( C_TGOVERNANCE_ESCROW_TOKEN_ID:Int =/=Int C_TGOVERNANCE_ID:Int
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_TOKEN_ID:Int
Expand Down Expand Up @@ -561,7 +565,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_TOKEN_ID:Int <= 9 ) )
))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))
[priority(20), label(BASIC-BLOCK-16-TO-10)]

rule [BASIC-BLOCK-17-TO-11]: <foundry>
Expand Down Expand Up @@ -656,7 +660,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
C_TGOVERNANCE_ESCROW_BAL:Int
</balance>
<storage>
( ( 0 |-> C_TGOVERNANCE_ESCROW_TOKEN_ID:Int )
( ( 0 |-> #asWord ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_BEFORE:Bytes +Bytes #buf ( 20 , C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ) +Bytes C_TGOVERNANCE_ESCROW_TOKEN_SLOT_AFTER:Bytes ) )
C_TGOVERNANCE_ESCROW_STORAGE:Map )
</storage>
<nonce>
Expand Down Expand Up @@ -759,8 +763,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
andBool ( 1023 <=Int CALLDEPTH_CELL:Int
andBool ( 0 <=Int C_TGOVERNANCE_NONCE:Int
andBool ( C_TGOVERNANCE_ESCROW_ID:Int =/=Int C_TGOVERNANCE_ID:Int
andBool ( 1 ==Int lengthBytes ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_AFTER:Bytes )
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_ID:Int
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_BAL:Int
andBool ( 11 ==Int lengthBytes ( C_TGOVERNANCE_ESCROW_TOKEN_SLOT_BEFORE:Bytes )
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_NONCE:Int
andBool ( C_TGOVERNANCE_ESCROW_TOKEN_ID:Int =/=Int C_TGOVERNANCE_ID:Int
andBool ( 0 <=Int C_TGOVERNANCE_ESCROW_TOKEN_ID:Int
Expand Down Expand Up @@ -801,7 +807,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_TOKEN_ID:Int <= 9 ) )
))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))
[priority(20), label(BASIC-BLOCK-17-TO-11)]

endmodule
2 changes: 1 addition & 1 deletion src/tests/integration/test-data/symbolic-bytes-lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,4 +100,4 @@ module SYMBOLIC-BYTES-LEMMAS
requires 0 <Int B andBool A modInt B ==Int 0
[simplification, concrete(A, B), comm, preserves-definedness]

endmodule
endmodule

0 comments on commit 359f183

Please sign in to comment.