update bihu specs

runtimeverification · Mar 19, 2024 · fd32f43 · fd32f43
1 parent 7f79d7b
commit fd32f43
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 11 deletions.
diff --git a/tests/specs/bihu/collectToken-spec.k b/tests/specs/bihu/collectToken-spec.k
@@ -30,7 +30,7 @@ module COLLECTTOKEN-SPEC
           <callData> #abiCallData("collectToken", #uint256(NOW), #uint256(START)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> GASCAP => ?_ </gas>
@@ -145,8 +145,8 @@ ensures ?VALUE ==Int @canExtractThisYear(COLLECTED +Int BAL, NOW, START) +Int BA
           <callData> _ </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> CANEXTRACT : CANEXTRACTTHISYEAR : TOTALREWARDTHISYEAR : INDEX     : YEARCOUNT : REMAINING : TOTAL : RETURNVAL : START : NOW : RPC : FUNID : .WordStack
-=> CANEXTRACT : CANEXTRACTTHISYEAR : TOTALREWARDTHISYEAR : YEARCOUNT : YEARCOUNT : #roundpower(REMAINING, 90, 100, YEARCOUNT -Int INDEX) : TOTAL : RETURNVAL : START : NOW : RPC : FUNID : .WordStack </wordStack>
+          <wordStack> ListItem(CANEXTRACT) ListItem(CANEXTRACTTHISYEAR) ListItem(TOTALREWARDTHISYEAR) ListItem(INDEX    ) ListItem(YEARCOUNT) ListItem(REMAINING) ListItem(TOTAL) ListItem(RETURNVAL) ListItem(START) ListItem(NOW) ListItem(RPC) ListItem(FUNID) .List
+=> ListItem(CANEXTRACT) ListItem(CANEXTRACTTHISYEAR) ListItem(TOTALREWARDTHISYEAR) ListItem(YEARCOUNT) ListItem(YEARCOUNT) ListItem(#roundpower(REMAINING, 90, 100, YEARCOUNT -Int INDEX)) ListItem(TOTAL) ListItem(RETURNVAL) ListItem(START) ListItem(NOW) ListItem(RPC) ListItem(FUNID) .List </wordStack>
           <localMem> _ </localMem>
           <pc> 498 => 545 </pc>
           <gas> GASCAP => GASCAP -Int (293 *Int (YEARCOUNT -Int INDEX)) -Int 26 </gas>
@@ -250,7 +250,7 @@ andBool GASCAP >=Int ((293 *Int (YEARCOUNT -Int INDEX)) +Int 26)
           <callData> _ </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> Y : X : RET : WS => X : Y : RET : X *Int Y : WS </wordStack>
+          <wordStack> ListItem(Y) ListItem(X) ListItem(RET) WS => ListItem(X) ListItem(Y) ListItem(RET) ListItem(X *Int Y) WS </wordStack>
           <localMem> _ </localMem>
           <pc> 750 => 793 </pc>
           <gas> GASCAP => GASCAP -Int 114 </gas>
@@ -325,7 +325,7 @@ andBool 0 <=Int Y          andBool Y          <Int (2 ^Int 256)
 andBool 0 <=Int X *Int Y   andBool X *Int Y   <Int (2 ^Int 256)
 andBool 0 <=Int MU         andBool MU         <Int (2 ^Int 256)
 //
-andBool #sizeWordStack(WS) <Int 20
+andBool size(WS) <Int 20
 //
 andBool GASCAP >=Int 114   // for the current spec
 

diff --git a/tests/specs/bihu/forwardToHotWallet-failure-1-spec.k b/tests/specs/bihu/forwardToHotWallet-failure-1-spec.k
@@ -30,7 +30,7 @@ module FORWARDTOHOTWALLET-FAILURE-1-SPEC
           <callData> #abiCallData("forwardToHotWallet", #uint256(AMOUNT)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> 22000 => ?_ </gas>

diff --git a/tests/specs/bihu/forwardToHotWallet-failure-2-spec.k b/tests/specs/bihu/forwardToHotWallet-failure-2-spec.k
@@ -30,7 +30,7 @@ module FORWARDTOHOTWALLET-FAILURE-2-SPEC
           <callData> #abiCallData("forwardToHotWallet", #uint256(AMOUNT)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> 22000 => ?_ </gas>

diff --git a/tests/specs/bihu/forwardToHotWallet-failure-3-spec.k b/tests/specs/bihu/forwardToHotWallet-failure-3-spec.k
@@ -30,7 +30,7 @@ module FORWARDTOHOTWALLET-FAILURE-3-SPEC
           <callData> #abiCallData("forwardToHotWallet", #uint256(AMOUNT)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> 22000 => ?_ </gas>

diff --git a/tests/specs/bihu/forwardToHotWallet-failure-4-spec.k b/tests/specs/bihu/forwardToHotWallet-failure-4-spec.k
@@ -30,7 +30,7 @@ module FORWARDTOHOTWALLET-FAILURE-4-SPEC
           <callData> #abiCallData("forwardToHotWallet", #uint256(AMOUNT)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> 22000 => ?_ </gas>

diff --git a/tests/specs/bihu/forwardToHotWallet-success-1-spec.k b/tests/specs/bihu/forwardToHotWallet-success-1-spec.k
@@ -30,7 +30,7 @@ module FORWARDTOHOTWALLET-SUCCESS-1-SPEC
           <callData> #abiCallData("forwardToHotWallet", #uint256(AMOUNT)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> 22000 => ?_ </gas>

diff --git a/tests/specs/bihu/forwardToHotWallet-success-2-spec.k b/tests/specs/bihu/forwardToHotWallet-success-2-spec.k
@@ -30,7 +30,7 @@ module FORWARDTOHOTWALLET-SUCCESS-2-SPEC
           <callData> #abiCallData("forwardToHotWallet", #uint256(AMOUNT)) </callData>
 
           <callValue> 0 </callValue>
-          <wordStack> .WordStack => ?_ </wordStack>
+          <wordStack> .List => ?_ </wordStack>
           <localMem> .Bytes => ?_ </localMem>
           <pc> 0 => ?_ </pc>
           <gas> 22000 => ?_ </gas>