Implement envOr(...) cheatcodes

src/kontrol/kdist/cheatcodes.md

@@ -43,6 +43,7 @@ module FOUNDRY-CHEAT-CODES
     imports EVM-ABI
     imports FOUNDRY-ACCOUNTS
     imports INFINITE-GAS
+    imports ID
 
     configuration
       <cheatcodes>
@@ -92,6 +93,7 @@ module FOUNDRY-CHEAT-CODES
                <mockFunctionValues>  .Map </mockFunctionValues>
             </mockFunction>
          </mockFunctions>
+         <envVars> .Map </envVars>
       </cheatcodes>
 ```
 
@@ -642,6 +644,82 @@ function toString(int256) external returns (string memory);
       [preserves-definedness]
 ```
 
+### `envOr(...)` cheatcodes
+
+The `envOr` cheatcodes in Foundry are used to read environment variables with a fallback.
+In Kontrol, `envOr` is currently only implemented for concrete execution, and we always
+returns the default value.
+
+```k
+    rule [envOr-word]:
+          <k> #cheatcode_call SELECTOR ARGS
+            => #getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #range(ARGS, 32, 32)
+            ...
+          </k>
+      requires SELECTOR in (
+         SetItem( selector ( "envOr(string,bool)" ) )
+         SetItem( selector ( "envOr(string,uint256)" ) )
+         SetItem( selector ( "envOr(string,int256)" ) )
+         SetItem( selector ( "envOr(string,address)" ) )
+         SetItem( selector ( "envOr(string,bytes32)" ) )
+      )
+      [preserves-definedness]
+
+      rule [envOr-string]:
+               <k> #cheatcode_call SELECTOR ARGS
+                  => #getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) (Int2Bytes(32, 32, BE) +Bytes #range(ARGS, #asWord(#range(ARGS, 32, 32)), lengthBytes(ARGS) -Int #asWord(#range(ARGS, 32, 32)))) ... </k>
+                  //#getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #enc( #tuple( #string( "default" ) ) ) ... </k>
+         requires SELECTOR ==Int selector( "envOr(string,string)" )
+         [preserves-definedness]
+         // The following rule, which is more readable, doesn't work. Needs investigation.
+         //      #let DATA_OFFSET = #asWord(#range(ARGS, 32, 32)) #in
+         //      #let DATA_SIZE   = #asWord(#range(ARGS, DATA_OFFSET, 32)) #in
+         //      #let DATA = #range(ARGS, 32 +Int DATA_OFFSET, DATA_SIZE) #in
+         //      #let VARNAME = #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #in
+         //      #getEnvOrValue SELECTOR VARNAME DATA
+
+    rule [envOr-bytes]:
+          <k> #cheatcode_call SELECTOR ARGS
+            => #getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #range(ARGS, #asWord(#range(ARGS, 32, 32)), 32 +Int #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32)))... </k>
+      requires SELECTOR ==Int selector( "envOr(string,bytes)" )
+      [preserves-definedness]
+
+    rule [envOr-word-array]:
+          <k> #cheatcode_call SELECTOR ARGS => .K ... </k>
+          <output> _ => 
+            #let DATA_OFFSET = #asWord(#range(ARGS, 64, 32)) #in
+            #let DATA_SIZE   = #range(ARGS, DATA_OFFSET, 32) #in
+            #let DATA        = #range(ARGS, DATA_OFFSET +Int 32, #asWord(DATA_SIZE) *Int 32) #in
+            #let HEAD        = Int2Bytes(32, 32, BE) #in
+            #let BODY        = DATA_SIZE +Bytes DATA #in
+            HEAD +Bytes BODY
+          </output>
+      requires SELECTOR in (
+         SetItem( selector ( "envOr(string,string,bool[])" ) )
+         SetItem( selector ( "envOr(string,string,uint256[])" ) )
+         SetItem( selector ( "envOr(string,string,int256[])" ) )
+         SetItem( selector ( "envOr(string,string,address[])" ) )
+         SetItem( selector ( "envOr(string,string,bytes32[])" ) )
+      )
+      [preserves-definedness]
+
+    rule [envOr-dynamic-array]:
+          <k> #cheatcode_call SELECTOR ARGS => .K ... </k>
+          <output> _ => 
+            #let DATA_OFFSET = #asWord(#range(ARGS, 64, 32)) #in
+            #let DATA_SIZE   = #range(ARGS, DATA_OFFSET, 32) #in
+            #let DATA        = #range(ARGS, DATA_OFFSET +Int 32, #asWord(DATA_SIZE) *Int 32) #in
+            #let HEAD        = Int2Bytes(32, 32, BE) #in
+            #let BODY        = DATA_SIZE +Bytes DATA #in 
+            HEAD +Bytes BODY
+          </output>
+      requires SELECTOR in (
+         SetItem( selector ( "envOr(string,string,string[])" ) )
+         SetItem( selector ( "envOr(string,string,bytes[])" ) )
+      )
+      [preserves-definedness]
+```
+
 Expecting the next call to revert
 ---------------------------------
 
@@ -1848,6 +1926,60 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
          <wordStack> _ : WS => 1 : WS </wordStack>
 ```
 
+- `#getEnvOrValue` will get the return the environment variable from the `<enVars>` mapping iif it's there, or will return the default value for the variable
+
+```k
+    syntax KItem ::= "#getEnvOrValue" Int Bytes Bytes [symbol(foundry_getEnvOrValue)]
+ // -----------------------------------------------------------------------------
+    rule <k> #getEnvOrValue SELECTOR VARNAME VARDEFAULTVALUE => #processOutput SELECTOR VARVALUE VARDEFAULTVALUE ... </k>
+         <envVars> ... VARNAME |-> VARVALUE ... </envVars>
+
+    rule <k> #getEnvOrValue _ _ VARDEFAULTVALUE => .K ... </k>
+         <output> _ => VARDEFAULTVALUE </output>
+    [owise]
+```
+
+```k
+    syntax KItem ::= "#processOutput" Int String Bytes [symbol(foundry_processOutputAsInt)]
+ // -----------------------------------------------------------------------------
+    rule <k> #processOutput SELECTOR VARVALUE _ => .K ... </k>
+         <output> _ => Int2Bytes(32, String2Int(VARVALUE), BE) </output>
+      requires SELECTOR ==Int selector ( "envOr(string,int256)" ) andBool isIntegerString(VARVALUE)
+
+    rule <k> #processOutput SELECTOR VARVALUE _ => .K ... </k>
+         <output> _ => Int2Bytes(32, String2Int(VARVALUE), BE) </output>
+      requires SELECTOR ==Int selector ( "envOr(string,uint256)" ) andBool isUnsignedIntegerString(VARVALUE)
+
+    rule <k> #processOutput SELECTOR VARVALUE _ => .K ... </k>
+         <output> _ => Int2Bytes(32, #parseHexWord(VARVALUE), BE) </output>
+      requires SELECTOR ==Int selector ( "envOr(string,address)" ) andBool (lengthString(VARVALUE) ==Int 42 orBool lengthString(VARVALUE) ==Int 40)
+
+    rule <k> #processOutput SELECTOR VARVALUE _ => .K ... </k>
+         <output> _ => Int2Bytes(32, #parseHexWord(VARVALUE), BE)</output>
+      requires SELECTOR ==Int selector ( "envOr(string,bytes32)" ) andBool (lengthString(VARVALUE) ==Int 66 orBool lengthString(VARVALUE) ==Int 64)
+
+    rule <k> #processOutput SELECTOR VARVALUE _ => .K ... </k>
+         <output> _ => Int2Bytes(32, bool2Word( String2Bool(VARVALUE) ), BE) </output>
+      requires SELECTOR ==Int selector ( "envOr(string,bool)" ) andBool (VARVALUE ==K "true" orBool VARVALUE ==K "false")
+
+    rule <k> #processOutput _ _ VARDEFAULTVALUE => .K ... </k>
+         <output> _ => VARDEFAULTVALUE </output>
+     [owise]
+```
+
+```k
+syntax Bool ::= isIntegerString(String) [function]
+
+rule isIntegerString(S) => true requires String2Int(S) ==K 0 orBool String2Int(S) =/=K 0
+rule isIntegerString(_) => false [owise]
+
+syntax Bool ::= isUnsignedIntegerString(String) [function]
+
+rule isUnsignedIntegerString(S) => true requires String2Int(S) >=Int 0
+rule isUnsignedIntegerString(_) => false [owise]
+```
+
+
 Selectors
 ---------
 
@@ -1920,6 +2052,20 @@ Selectors for **implemented** cheat code functions.
     rule ( selector ( "toString(bool)" )                           => 1910302682 )
     rule ( selector ( "toString(uint256)" )                        => 1761649582 )
     rule ( selector ( "toString(int256)" )                         => 2736964622 )
+    rule ( selector ( "envOr(string,address)" )                    => 1444930880 )
+    rule ( selector ( "envOr(string,bool)" )                       => 1199043535 )
+    rule ( selector ( "envOr(string,bytes)" )                      => 3018094341 )
+    rule ( selector ( "envOr(string,bytes32)" )                    => 3030931602 )
+    rule ( selector ( "envOr(string,int256)" )                     => 3150672190 )
+    rule ( selector ( "envOr(string,string)" )                     => 3510989676 )
+    rule ( selector ( "envOr(string,string,address[])" )           => 3343818219 )
+    rule ( selector ( "envOr(string,string,bool[])" )              => 3951421499 )
+    rule ( selector ( "envOr(string,string,bytes32[])" )           => 578941799  )
+    rule ( selector ( "envOr(string,string,bytes[])" )             => 1690058340 )
+    rule ( selector ( "envOr(string,string,int256[])" )            => 1191237451 )
+    rule ( selector ( "envOr(string,string,string[])" )            => 2240943804 )
+    rule ( selector ( "envOr(string,string,uint256[])" )           => 1949402408 )
+    rule ( selector ( "envOr(string,uint256)" )                    => 1586967695 )
 ```
 
 Selectors for **unimplemented** cheat code functions.
@@ -1985,4 +2131,4 @@ Selector for Solidity built-in Error
 ```
 ```k
 endmodule
-```
+```

src/kontrol/prove.py

@@ -39,7 +39,7 @@
 from .natspec import apply_natspec_preconditions
 from .options import ConfigType
 from .solc_to_k import Contract, decode_kinner_output
-from .utils import console, parse_test_version_tuple, replace_k_words
+from .utils import console, parse_foundry_env, parse_test_version_tuple, replace_k_words
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
@@ -1003,8 +1003,16 @@ def _init_cterm(
         'ALLOWEDCALLSLIST_CELL': list_empty(),
         'MOCKCALLS_CELL': KApply('.MockCallCellMap'),
         'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'),
+        'ENVVARS_CELL': KApply('.Map'),
     }
 
+    # Initialize ENVVARS_CELL with environment variables from .env file
+    env_vars = parse_foundry_env(foundry._root)
+    env_map = map_empty()
+    for key, value in env_vars.items():
+        env_map = KApply('_Map_', [map_item(bytesToken(key.encode('utf-8')), token(value)), env_map])
+    init_subst['ENVVARS_CELL'] = env_map
+
     storage_constraints: list[KApply] = []
 
     if config_type == ConfigType.TEST_CONFIG or active_simbolik:

src/kontrol/utils.py

@@ -331,6 +331,42 @@ def decode_log_message(token: str, selector: int) -> str | None:
         return None
 
 
+def parse_env_file(file_path: Path) -> dict[str, str]:
+    """Parse a .env file into a dictionary of key-value pairs.
+
+    :param file_path: Path to the .env file
+    :return: Dictionary with environment variable names as keys and their values as strings
+    """
+    env_vars = {}
+    if not file_path.exists():
+        return env_vars
+    with open(file_path, 'r', encoding='utf-8') as f:
+        for line in f:
+            line = line.strip()
+            if not line or line.startswith('#'):
+                continue
+            if '=' not in line:
+                continue
+            key, value = line.split('=', 1)
+            key = key.strip()
+            value = value.strip()
+            # Remove surrounding quotes if present
+            if (value.startswith('"') and value.endswith('"')) or (value.startswith("'") and value.endswith("'")):
+                value = value[1:-1]
+            env_vars[key] = value
+    return env_vars
+
+
+def parse_foundry_env(foundry_root: Path) -> dict[str, str]:
+    """Parse the .env file located in the Foundry root directory.
+
+    :param foundry_root: Path to the Foundry project root directory
+    :return: Dictionary with environment variable names as keys and their values as strings
+    """
+    env_file = foundry_root / '.env'
+    return parse_env_file(env_file)
+
+
 EMPTY_LOG_SELECTOR = 1368866505
 # a mapping from function selectors to the argument types used in the log functions from
 # https://github.com/foundry-rs/forge-std/blob/ee93fdc45d1e5e4dee883afe0103109881a83549/src/console.sol

src/tests/integration/test-data/foundry-prove-all

@@ -100,6 +100,15 @@ EnvTest.testEnvString()
 EnvTest.testEnvStringArray()
 EnvTest.testEnvUInt()
 EnvTest.testEnvUIntArray()
+EnvOrTest.testEnvOrUint256()
+EnvOrTest.testEnvOrInt256()
+EnvOrTest.testEnvOrAddress()
+EnvOrTest.testEnvOrBytes32()
+EnvOrTest.testEnvOrBool()
+EnvOrTest.testEnvOrString()
+EnvOrTest.testEnvOrBytes()
+EnvOrTest.testEnvOrUint256Array()
+EnvOrTest.testEnvOrStringArray()
 ExpectCallTest.testExpectRegularCall()
 ExpectCallTest.testExpectStaticCall()
 ExpectRevertTest.test_expectRevert_bytes4()