fix mcd proofs

runtimeverification · Dec 18, 2024 · 8a1d67b · 8a1d67b
1 parent f1508c1
commit 8a1d67b
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 0 deletions.
diff --git a/tests/specs/mcd-structured/end-pack-pass-rough-spec.k b/tests/specs/mcd-structured/end-pack-pass-rough-spec.k
@@ -191,6 +191,7 @@ module END-PACK-PASS-ROUGH-SPEC
             <refund> _Vrefund => ?_ </refund>
             <accessedAccounts> _ => ?_ </accessedAccounts>
             <accessedStorage> _ => ?_ </accessedStorage>
+            <createdAccounts> _ => ?_ </createdAccounts>
           </substate>
           <gasPrice> _ </gasPrice>
           <origin> ORIGIN_ID </origin>
@@ -293,6 +294,7 @@ module END-PACK-PASS-ROUGH-SPEC
             <refund> _Vrefund => ?_ </refund>
             <accessedAccounts> _ => ?_ </accessedAccounts>
             <accessedStorage> _ => ?_ </accessedStorage>
+            <createdAccounts> _ => ?_ </createdAccounts>
           </substate>
           <gasPrice> _ </gasPrice>
           <origin> ORIGIN_ID </origin>
@@ -395,6 +397,7 @@ module END-PACK-PASS-ROUGH-SPEC
             <refund> _Vrefund => ?_ </refund>
             <accessedAccounts> _ => ?_ </accessedAccounts>
             <accessedStorage> _ => ?_ </accessedStorage>
+            <createdAccounts> _ => ?_ </createdAccounts>
           </substate>
           <gasPrice> _ </gasPrice>
           <origin> ORIGIN_ID </origin>

diff --git a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json
diff --git a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k
@@ -201,6 +201,7 @@ module FLAPPER-YANK-PASS-ROUGH-SPEC
             <refund> _Vrefund => ?_ </refund>
             <accessedAccounts> _ => ?_ </accessedAccounts>
             <accessedStorage> _ => ?_ </accessedStorage>
+            <createdAccounts> _ => ?_ </createdAccounts>
           </substate>
           <gasPrice> _ </gasPrice>
           <origin> ORIGIN_ID </origin>

diff --git a/tests/specs/mcd-structured/vat-spec.json b/tests/specs/mcd-structured/vat-spec.json