Skip to content

Commit

Permalink
add cell to mcd-structured claims
Browse files Browse the repository at this point in the history
  • Loading branch information
@anvacaru
anvacaru committed Dec 11, 2024
1 parent f439fe0 commit f1508c1
Show file tree
Hide file tree
Showing 38 changed files with 45 additions and 1 deletion.
1 change: 0 additions & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,5 +5,4 @@
if TYPE_CHECKING:
from typing import Final


VERSION: Final = '1.0.678'
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/cat-exhaustiveness-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module CAT-EXHAUSTIVENESS-SPEC
<refund> _ => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module CAT-FILE-ADDR-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module DAI-ADDUU-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/dai-symbol-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module DAI-SYMBOL-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module DSTOKEN-APPROVE-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module DSVALUE-PEEK-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/dsvalue-read-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module DSVALUE-READ-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/end-cash-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module END-CASH-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/end-pack-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module END-PACK-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/end-subuu-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module END-SUBUU-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flipper-bids-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLIPPER-BIDS-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flipper-tau-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLIPPER-TAU-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flipper-ttl-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLIPPER-TTL-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flopper-cage-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ module FLOPPER-CAGE-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLOPPER-DENT-GUY-DIFF-TIC-NOT-0-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flopper-dent-guy-same-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLOPPER-DENT-GUY-SAME-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flopper-kick-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLOPPER-KICK-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module FLOPPER-TICK-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/pot-join-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module POT-JOIN-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-addui-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module VAT-ADDUI-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
6 changes: 6 additions & 0 deletions tests/specs/mcd-structured/vat-arithmetic-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ module VAT-ARITHMETIC-SPEC
<log> _ => ?_ </log>
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<createdAccounts> _ => ?_ </createdAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
</substate>
<gasPrice> _ </gasPrice>
Expand Down Expand Up @@ -136,6 +137,7 @@ module VAT-ARITHMETIC-SPEC
<log> _ => ?_ </log>
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<createdAccounts> _ => ?_ </createdAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
</substate>
<gasPrice> _ </gasPrice>
Expand Down Expand Up @@ -230,6 +232,7 @@ module VAT-ARITHMETIC-SPEC
<log> _ => ?_ </log>
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<createdAccounts> _ => ?_ </createdAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
</substate>
<gasPrice> _ </gasPrice>
Expand Down Expand Up @@ -330,6 +333,7 @@ module VAT-ARITHMETIC-SPEC
<log> _ => ?_ </log>
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<createdAccounts> _ => ?_ </createdAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
</substate>
<gasPrice> _ </gasPrice>
Expand Down Expand Up @@ -427,6 +431,7 @@ module VAT-ARITHMETIC-SPEC
<log> _ => ?_ </log>
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<createdAccounts> _ => ?_ </createdAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
</substate>
<gasPrice> _ </gasPrice>
Expand Down Expand Up @@ -524,6 +529,7 @@ module VAT-ARITHMETIC-SPEC
<log> _ => ?_ </log>
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<createdAccounts> _ => ?_ </createdAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
</substate>
<gasPrice> _ </gasPrice>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-dai-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ module VAT-DAI-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-deny-diff-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module VAT-DENY-DIFF-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-flux-diff-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ module VAT-FLUX-DIFF-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-flux-diff-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ module VAT-FLUX-DIFF-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-fold-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module VAT-FOLD-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-fork-diff-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module VAT-FORK-DIFF-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-frob-diff-zero-dart-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-heal-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ module VAT-HEAL-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-move-diff-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ module VAT-MOVE-DIFF-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-sin-pass-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ module VAT-SIN-PASS-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-slip-pass-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module VAT-SLIP-PASS-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
1 change: 1 addition & 0 deletions tests/specs/mcd-structured/vat-subui-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module VAT-SUBUI-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
2 changes: 2 additions & 0 deletions tests/specs/mcd-structured/vow-fess-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module VOW-FESS-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down Expand Up @@ -159,6 +160,7 @@ module VOW-FESS-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down
3 changes: 3 additions & 0 deletions tests/specs/mcd-structured/vow-flog-fail-rough-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ module VOW-FLOG-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down Expand Up @@ -152,6 +153,7 @@ module VOW-FLOG-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down Expand Up @@ -254,6 +256,7 @@ module VOW-FLOG-FAIL-ROUGH-SPEC
<refund> _Vrefund => ?_ </refund>
<accessedAccounts> _ => ?_ </accessedAccounts>
<accessedStorage> _ => ?_ </accessedStorage>
<createdAccounts> _ => ?_ </createdAccounts>
</substate>
<gasPrice> _ </gasPrice>
<origin> ORIGIN_ID </origin>
Expand Down

0 comments on commit f1508c1

Please sign in to comment.