Deprecate klabel attribute

package/version

@@ -1 +1 @@
-0.1.334
+0.1.335

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.334"
+version = "0.1.335"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.334'
+VERSION: Final = '0.1.335'

src/kontrol/foundry.py

@@ -409,8 +409,8 @@ def loc_FOUNDRY_FAILED() -> KApply:  # noqa: N802
             KApply(
                 'contract_access_field',
                 [
-                    KApply('FoundryCheat_FOUNDRY-ACCOUNTS_FoundryContract'),
-                    KApply('Failed_FOUNDRY-ACCOUNTS_FoundryField'),
+                    KApply('contract_FoundryCheat'),
+                    KApply('slot_failed'),
                 ],
             )
         )

src/kontrol/kdist/cheatcodes.md

@@ -968,7 +968,7 @@ Utils
 - `#loadAccount ACCT` creates a new, empty account for `ACCT` if it does not already exist. Otherwise, it has no effect.
 
 ```k
-    syntax KItem ::= "#loadAccount" Int [klabel(foundry_loadAccount)]
+    syntax KItem ::= "#loadAccount" Int [symbol(foundry_loadAccount)]
  // -----------------------------------------------------------------
     rule <k> #loadAccount ACCT => #accessAccounts ACCT ... </k> <account> <acctID> ACCT </acctID> ... </account>
     rule <k> #loadAccount ACCT => #newAccount ACCT ~> #accessAccounts ACCT ... </k> [owise]
@@ -977,7 +977,7 @@ Utils
 - `#setBalance ACCTID NEWBAL` sets the balance of a given account.
 
 ```k
-    syntax KItem ::= "#setBalance" Int Int [klabel(foundry_setBalance)]
+    syntax KItem ::= "#setBalance" Int Int [symbol(foundry_setBalance)]
  // -------------------------------------------------------------------
     rule <k> #setBalance ACCTID NEWBAL => .K ... </k>
          <account>
@@ -990,7 +990,7 @@ Utils
 - `#setCode ACCTID CODE` sets the code of a given account.
 
 ```k
-    syntax KItem ::= "#setCode" Int Bytes [klabel(foundry_setCode)]
+    syntax KItem ::= "#setCode" Int Bytes [symbol(foundry_setCode)]
  // ---------------------------------------------------------------
     rule <k> #setCode ACCTID CODE => .K ... </k>
          <account>
@@ -1003,7 +1003,7 @@ Utils
 - `#returnNonce ACCTID` takes the nonce of a given account and places it on the `<output>` cell.
 
 ```k
-    syntax KItem ::= "#returnNonce" Int [klabel(foundry_returnNonce)]
+    syntax KItem ::= "#returnNonce" Int [symbol(foundry_returnNonce)]
  // -----------------------------------------------------------------
     rule <k> #returnNonce ACCTID => .K ... </k>
          <output> _ => #bufStrict(32, NONCE) </output>
@@ -1017,7 +1017,7 @@ Utils
 - `#setNonce ACCTID NONCE` takes a given account and a given nonce and update the account accordingly.
 
 ```k
-     syntax KItem ::= "#setNonce" Int Int [klabel(foundry_setNonce)]
+     syntax KItem ::= "#setNonce" Int Int [symbol(foundry_setNonce)]
  // ----------------------------------------------------------------
     rule <k> #setNonce ACCTID NONCE => .K ... </k>
          <account>
@@ -1030,7 +1030,7 @@ Utils
 - `#returnStorage ACCTID LOC` takes a storage value from a given account and places it on the `<output>` cell.
 
 ```k
-    syntax KItem ::= "#returnStorage" Int Int [klabel(foundry_returnStorage)]
+    syntax KItem ::= "#returnStorage" Int Int [symbol(foundry_returnStorage)]
  // -------------------------------------------------------------------------
     rule <k> #returnStorage ACCTID LOC => .K ... </k>
          <output> _ => #bufStrict(32, #lookup(STORAGE, LOC)) </output>
@@ -1045,7 +1045,7 @@ Utils
 - `#setStorage ACCTID LOC VALUE` sets a given value to a given location of an account.
 
 ```k
-    syntax KItem ::= "#setStorage" Int Int Int [klabel(foundry_setStorage)]
+    syntax KItem ::= "#setStorage" Int Int Int [symbol(foundry_setStorage)]
  // -----------------------------------------------------------------------
     rule <k> #setStorage ACCTID LOC VALUE => .K ... </k>
          <account>
@@ -1058,7 +1058,7 @@ Utils
 `#setSymbolicStorage ACCTID` takes a given account and makes its storage fully symbolic.
 
 ```k
-     syntax KItem ::= "#setSymbolicStorage" Int [klabel(foundry_setSymbolicStorage)]
+     syntax KItem ::= "#setSymbolicStorage" Int [symbol(foundry_setSymbolicStorage)]
 ```
 
 ```{.k .symbolic}
@@ -1074,7 +1074,7 @@ Utils
 - `#setExpectRevert` sets the `<expectedRevert>` subconfiguration with the current call depth and the expected message from `expectRevert`.
 
 ```k
-    syntax KItem ::= "#setExpectRevert" Bytes [klabel(foundry_setExpectRevert)]
+    syntax KItem ::= "#setExpectRevert" Bytes [symbol(foundry_setExpectRevert)]
  // ---------------------------------------------------------------------------
     rule <k> #setExpectRevert EXPECTED => .K ... </k>
          <callDepth> CD </callDepth>
@@ -1090,8 +1090,8 @@ When `bytes4` type parameter is used some of the information is not directly inc
 Here we set them manually to constant values.
 
 ```k
-    syntax KItem ::= "#setExpectRevertBytes4" Bytes [klabel(foundry_setExpectRevert)]
- // ---------------------------------------------------------------------------------
+    syntax KItem ::= "#setExpectRevertBytes4" Bytes [symbol(foundry_setExpectRevertBytes4)]
+ // ---------------------------------------------------------------------------------------
     rule <k> #setExpectRevertBytes4 EXPECTED => .K ... </k>
          <callDepth> CD </callDepth>
          <expectedRevert>
@@ -1104,7 +1104,7 @@ Here we set them manually to constant values.
 - `#clearExpectRevert` sets the `<expectedRevert>` subconfiguration to initial values.
 
 ```k
-    syntax KItem ::= "#clearExpectRevert" [klabel(foundry_clearExpectRevert)]
+    syntax KItem ::= "#clearExpectRevert" [symbol(foundry_clearExpectRevert)]
  // -------------------------------------------------------------------------
     rule <k> #clearExpectRevert => .K ... </k>
          <expectedRevert>
@@ -1118,7 +1118,7 @@ Here we set them manually to constant values.
 Otherwise, the output is already in the local memory, so `#setLocalMem` does not change anything.
 
 ```k
-    syntax KItem ::= "#updateRevertOutput" Int Int [klabel("foundry_updateRevertOutput")]
+    syntax KItem ::= "#updateRevertOutput" Int Int [symbol("foundry_updateRevertOutput")]
  // -------------------------------------------------------------------------------------
     rule <k> #updateRevertOutput START WIDTH => #setLocalMem START WIDTH OUT ... </k> <output> OUT </output>
 ```
@@ -1129,7 +1129,7 @@ Otherwise, if the status code is `EVMC_SUCCESS`, or the output does not match th
 `#clearExpectRevert` is used to end the `expectRevert` cheat code.
 
 ```k
-    syntax KItem ::= "#checkRevert" [klabel("foundry_checkRevert")]
+    syntax KItem ::= "#checkRevert" [symbol("foundry_checkRevert")]
  // ---------------------------------------------------------------
     rule <k> #checkRevert => #clearExpectRevert ... </k>
          <statusCode> SC => EVMC_SUCCESS </statusCode>
@@ -1179,7 +1179,7 @@ Otherwise, if the status code is `EVMC_SUCCESS`, or the output does not match th
     Since the encoding `abi.encode(abi.encodeWithSelector(Error.selector, 1, 2))` cannot be easily decoded when symbolic variables are used, the `<output>` Bytes object is encoded again when the default `Error(string)` is not used.
 
 ```k
-    syntax Bytes ::= "#encodeOutput" "(" Bytes ")" [function, total, klabel(foundry_encodeOutput)]
+    syntax Bytes ::= "#encodeOutput" "(" Bytes ")" [function, total, symbol(foundry_encodeOutput)]
  // ----------------------------------------------------------------------------------------------
     rule #encodeOutput(BA) => #abiCallData("expectRevert", #bytes(BA)) requires notBool #range(BA, 0, 4) ==K Int2Bytes(4, selector("Error(string)"), BE)
     rule #encodeOutput(BA) => BA [owise]
@@ -1189,7 +1189,7 @@ Otherwise, if the status code is `EVMC_SUCCESS`, or the output does not match th
 Will also return true if REASON is `.Bytes`.
 
 ```k
-    syntax Bool ::= "#matchReason" "(" Bytes "," Bytes ")" [function, klabel(foundry_matchReason)]
+    syntax Bool ::= "#matchReason" "(" Bytes "," Bytes ")" [function, symbol(foundry_matchReason)]
  // ----------------------------------------------------------------------------------------------
     rule #matchReason(REASON, _) => true requires REASON ==K .Bytes
     rule #matchReason(REASON, OUT) => REASON ==K #range(OUT, 4, lengthBytes(OUT) -Int 4) requires REASON =/=K .Bytes
@@ -1199,7 +1199,7 @@ Will also return true if REASON is `.Bytes`.
 `CallType` is used to specify what `CALL*` opcode is expected.
 
 ```k
-    syntax KItem ::= "#setExpectOpcode" Account Bytes Int OpcodeType [klabel(foundry_setExpectOpcode)]
+    syntax KItem ::= "#setExpectOpcode" Account Bytes Int OpcodeType [symbol(foundry_setExpectOpcode)]
  // --------------------------------------------------------------------------------------------------
     rule <k> #setExpectOpcode ACCT DATA VALUE OPTYPE => .K ... </k>
          <expectedOpcode>
@@ -1214,7 +1214,7 @@ Will also return true if REASON is `.Bytes`.
 - `#clearExpectOpcode` restore the `<expectedOpcode>` subconfiguration to its initial values.
 
 ```k
-    syntax KItem ::= "#clearExpectOpcode" [klabel(foundry_clearExpectOpcode)]
+    syntax KItem ::= "#clearExpectOpcode" [symbol(foundry_clearExpectOpcode)]
  // -------------------------------------------------------------------------
     rule <k> #clearExpectOpcode => .K ... </k>
          <expectedOpcode>
@@ -1229,7 +1229,7 @@ Will also return true if REASON is `.Bytes`.
 - `#setPrank NEWCALLER NEWORIGIN SINGLEPRANK` will set the `<prank/>` subconfiguration for the given accounts.
 
 ```k
-    syntax KItem ::= "#setPrank" Int Account Bool [klabel(foundry_setPrank)]
+    syntax KItem ::= "#setPrank" Int Account Bool [symbol(foundry_setPrank)]
  // ------------------------------------------------------------------------
     rule <k> #setPrank NEWCALLER NEWORIGIN SINGLEPRANK => .K ... </k>
          <callDepth> CD </callDepth>
@@ -1250,7 +1250,7 @@ Will also return true if REASON is `.Bytes`.
 If the production is matched when no prank is active, it will be ignored.
 
 ```k
-    syntax KItem ::= "#endPrank" [klabel(foundry_endPrank)]
+    syntax KItem ::= "#endPrank" [symbol(foundry_endPrank)]
  // -------------------------------------------------------
     rule <k> #endPrank => #if SINGLECALL #then #clearPrank #else .K #fi ... </k>
         <id> _ => CL </id>
@@ -1273,7 +1273,7 @@ If the production is matched when no prank is active, it will be ignored.
 - `#clearPrank` will clear the prank subconfiguration.
 
 ```k
-    syntax KItem ::= "#clearPrank" [klabel(foundry_clearPrank)]
+    syntax KItem ::= "#clearPrank" [symbol(foundry_clearPrank)]
  // -----------------------------------------------------------
     rule <k> #clearPrank => .K ... </k>
         <prank>
@@ -1290,7 +1290,7 @@ If the production is matched when no prank is active, it will be ignored.
 - `#injectPrank` replaces the current account and the origin with the pranked values.
 
 ```k
-    syntax KItem ::= "#injectPrank" [klabel(foundry_inject)]
+    syntax KItem ::= "#injectPrank" [symbol(foundry_inject)]
  // --------------------------------------------------------
     rule <k> #injectPrank => .K ... </k>
          <id> _ => NCL </id>
@@ -1313,15 +1313,15 @@ If the production is matched when no prank is active, it will be ignored.
 ```
 
 ```k
-    syntax Bytes ::= #sign ( Bytes , Bytes ) [function,klabel(foundry_sign)]
+    syntax Bytes ::= #sign ( Bytes , Bytes ) [function,symbol(foundry_sign)]
  // ------------------------------------------------------------------------
     rule #sign(BA1, BA2) => #parseByteStack(ECDSASign(BA1, BA2)) [concrete]
 ```
 
 - `#setExpectEmit` will initialize the `<expectEmit/>` subconfiguration, based on the arguments provided with the `expectEmit` cheat code.
 
 ```k
-    syntax KItem ::= "#setExpectEmit" Bool Bool Bool Bool Account [klabel(foundry_setExpectEmit)]
+    syntax KItem ::= "#setExpectEmit" Bool Bool Bool Bool Account [symbol(foundry_setExpectEmit)]
  // ---------------------------------------------------------------------------------------------
     rule <k> #setExpectEmit T1 T2 T3 CHECKDATA ACCT => .K ... </k>
          <expectEmit>
@@ -1336,7 +1336,7 @@ If the production is matched when no prank is active, it will be ignored.
 - `#clearExpectEmit` is used to clear the `<expectEmit/>` subconfiguration and restore initial values.
 
 ```k
-    syntax KItem ::= "#clearExpectEmit" [klabel(foundry_clearExpectEmit)]
+    syntax KItem ::= "#clearExpectEmit" [symbol(foundry_clearExpectEmit)]
  // ---------------------------------------------------------------------
     rule <k> #clearExpectEmit => .K ... </k>
          <expectEmit>
@@ -1355,8 +1355,8 @@ It validates that the lists are of equal length before comparing topics as dicta
 If the flag is false, it skips comparison, assuming success; otherwise, it compares the topics for equality.
 
 ```k
-    syntax Bool ::= "#checkTopic" "(" Bool "," Int "," Int ")" [function, klabel(foundry_checkTopic)]
-                  | "#checkTopics" "(" List "," List "," List ")" [function, klabel(foundry_checkTopics)]
+    syntax Bool ::= "#checkTopic" "(" Bool "," Int "," Int ")" [function, symbol(foundry_checkTopic)]
+                  | "#checkTopics" "(" List "," List "," List ")" [function, symbol(foundry_checkTopics)]
  // -----------------------------------------------------------------------------------------------------
     rule #checkTopic(CHECK, V1, V2) => (notBool CHECK) orBool (V1 ==Int V2)
 
@@ -1369,7 +1369,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
 - `#addAddressToWhitelist` enables the whitelist restriction for calls and adds an address to the whitelist.
 
 ```k
-    syntax KItem ::= "#addAddressToWhitelist" Int [klabel(foundry_addAddressToWhitelist)]
+    syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)]
  // -------------------------------------------------------------------------------------
     rule <k> #addAddressToWhitelist ACCT => .K ... </k>
         <whitelist>
@@ -1382,7 +1382,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
 - `#addStorageSlotToWhitelist` enables the whitelist restriction for storage chagnes and adds a `StorageSlot` item to the whitelist.
 
 ```k
-    syntax KItem ::= "#addStorageSlotToWhitelist" StorageSlot [klabel(foundry_addStorageSlotToWhitelist)]
+    syntax KItem ::= "#addStorageSlotToWhitelist" StorageSlot [symbol(foundry_addStorageSlotToWhitelist)]
  // -----------------------------------------------------------------------------------------------------
     rule <k> #addStorageSlotToWhitelist SLOT => .K ... </k>
         <whitelist>
@@ -1395,7 +1395,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
 - `#etchAccountIfEmpty Account` - sets an Account code to a single byte '0u8' if the account is empty to circumvent the `extcodesize` check that Solidity might perform ([source](https://github.com/foundry-rs/foundry/blob/b78289a0bc9df6e35624c632396e16f27d4ccb3f/crates/cheatcodes/src/evm/mock.rs#L54)).
 
 ```k
-    syntax KItem ::= "#etchAccountIfEmpty" Account [klabel(foundry_etchAccountIfEmpty)]
+    syntax KItem ::= "#etchAccountIfEmpty" Account [symbol(foundry_etchAccountIfEmpty)]
  // -----------------------------------------------------------------------------------
     rule <k> #etchAccountIfEmpty ACCT => .K ... </k>
          <accounts>
@@ -1413,7 +1413,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
 - `#setMockCall MOCKADDRESS MOCKCALLDATA MOCKRETURN` will update the `<mockcalls>` mapping for the given account.
 
 ```k
-    syntax KItem ::= "#setMockCall" Account Bytes Bytes [klabel(foundry_setMockCall)]
+    syntax KItem ::= "#setMockCall" Account Bytes Bytes [symbol(foundry_setMockCall)]
  // ---------------------------------------------------------------------------------
     rule <k> #setMockCall MOCKADDRESS MOCKCALLDATA MOCKRETURN => .K ... </k>
          <mockCall>
@@ -1436,7 +1436,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
 - `#execMockCall` will update the output of the function call with `RETURNDATA` using `#setLocalMem`. In case the function did not end with `EVMC_SUCCESS` it will update the status code to `EVMC_SUCCESS`.
 
 ```k
-    syntax KItem ::= "#execMockCall" Int Int Bytes [klabel(foundry_execMockCall)]
+    syntax KItem ::= "#execMockCall" Int Int Bytes [symbol(foundry_execMockCall)]
  // -----------------------------------------------------------------------------
     rule <k> #execMockCall RETSTART RETWIDTH RETURNDATA => 1 ~> #push ~> #setLocalMem RETSTART RETWIDTH RETURNDATA ... </k>
          <output> _ => RETURNDATA </output>

src/kontrol/kdist/foundry.md

@@ -48,13 +48,13 @@ module FOUNDRY-ACCOUNTS
     syntax Int             ::= #address ( Contract ) [macro]
     syntax Contract        ::= FoundryContract
     syntax Field           ::= FoundryField
-    syntax FoundryContract ::= "FoundryTest"  [klabel(contract_FoundryTest)]
-                             | "FoundryCheat" [klabel(contract_FoundryCheat)]
+    syntax FoundryContract ::= "FoundryTest"  [symbol(contract_FoundryTest)]
+                             | "FoundryCheat" [symbol(contract_FoundryCheat)]
  // -------------------------------------------------------------------------
     rule #address(FoundryTest)  => 728815563385977040452943777879061427756277306518  // 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496
     rule #address(FoundryCheat) => 645326474426547203313410069153905908525362434349  // 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D
 
-    syntax FoundryField ::= "Failed" [klabel(slot_failed)]
+    syntax FoundryField ::= "Failed" [symbol(slot_failed)]
  // ------------------------------------------------------
     rule #loc(FoundryCheat . Failed) => 46308022326495007027972728677917914892729792999299745830475596687180801507328 // 0x6661696c65640000000000000000000000000000000000000000000000000000
 ```
@@ -65,11 +65,11 @@ Then, we define helpers in K which can:
 -   Set the `FoundryCheat . Failed` location to `True`.
 
 ```k
-    syntax KItem ::= #assume ( Bool ) [klabel(cheatcode_assume), symbol]
- // --------------------------------------------------------------------
+    syntax KItem ::= #assume ( Bool ) [symbol(cheatcode_assume)]
+ // ------------------------------------------------------------
     rule <k> #assume(B) => .K ... </k> ensures B
 
-     syntax KItem ::= "#markAsFailed" [klabel(foundry_markAsFailed)]
+     syntax KItem ::= "#markAsFailed" [symbol(foundry_markAsFailed)]
   // ---------------------------------------------------------------
      rule <k> #markAsFailed => .K ... </k>
           <account>
@@ -104,9 +104,9 @@ We define two productions named `#cheatcode_return` and `#cheatcode_call`, which
 The rule `cheatcode.return` will rewrite the `#cheatcode_return` production into other productions that will place the output of the execution into the local memory, refund the gas value of the call and push the value `1` on the call stack.
 
 ```k
-    syntax KItem ::= "#cheatcode_return" Int Int  [klabel(cheatcode_return)]
-                   | "#cheatcode_call" Int Bytes  [klabel(cheatcode_call)  ]
-                   | "#cheatcode_error" Int Bytes [klabel(cheatcode_error) ]
+    syntax KItem ::= "#cheatcode_return" Int Int  [symbol(cheatcode_return)]
+                   | "#cheatcode_call" Int Bytes  [symbol(cheatcode_call)  ]
+                   | "#cheatcode_error" Int Bytes [symbol(cheatcode_error) ]
  // ------------------------------------------------------------------------
     rule [cheatcode.return]:
          <k> #cheatcode_return RETSTART RETWIDTH
@@ -155,8 +155,8 @@ module FOUNDRY-SUCCESS
         opcodeExpected: Bool ","
         recordEventExpected: Bool ","
         eventExpected: Bool
-      ")" [function, klabel(foundry_success), symbol]
- // -------------------------------------------------
+      ")" [function, symbol(foundry_success)]
+ // -----------------------------------------
     rule foundry_success(EVMC_SUCCESS, 0, false, false, false, false) => true
     rule foundry_success(_, _, _, _, _, _)                            => false [owise]