Implement envOr(...) cheatcodes

src/kontrol/kdist/assert.md

@@ -93,13 +93,18 @@ Capturing cheat code calls
 
     rule [cheatcode.call.assertEq.Dtype]:
          <k> #cheatcode_call SELECTOR ARGS =>
-               #let ARG1_START = #asWord(#range(ARGS,  0, 32)) #in
-               #let ARG2_START = #asWord(#range(ARGS, 32, 32)) #in
-               #let ARG1_LEN   = #asWord(#range(ARGS, ARG1_START, 32)) #in
-               #let ARG2_LEN   = #asWord(#range(ARGS, ARG2_START, 32)) #in
-               #let ARG1_VALUE = #asWord(#range(ARGS, 32 +Int ARG1_START, ARG1_LEN)) #in
-               #let ARG2_VALUE = #asWord(#range(ARGS, 32 +Int ARG2_START, ARG2_LEN)) #in
-                 #assert_eq ARG1_VALUE ARG2_VALUE String2Bytes("assertion failed") ... </k>
+               //#let ARG1_START = #asWord(#range(ARGS,  0, 32)) #in
+               //#let ARG2_START = #asWord(#range(ARGS, 32, 32)) #in
+               //#let ARG1_LEN   = #asWord(#range(ARGS, ARG1_START, 32)) #in
+               //#let ARG2_LEN   = #asWord(#range(ARGS, ARG2_START, 32)) #in
+               //#let ARG1_VALUE = #asWord(#range(ARGS, 32 +Int ARG1_START, ARG1_LEN)) #in
+               //#let ARG2_VALUE = #asWord(#range(ARGS, 32 +Int ARG2_START, ARG2_LEN)) #in
+               //  #assert_eq ARG1_VALUE ARG2_VALUE String2Bytes("assertion failed") ... </k>
+               #assert_eq #asWord(#range(ARGS, 32 +Int #asWord(#range(ARGS,  0, 32)), #asWord(#range(ARGS, #asWord(#range(ARGS,  0, 32)), 32))))
+                          #asWord(#range(ARGS, 32 +Int #asWord(#range(ARGS, 32, 32)), #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32)))) 
+                          String2Bytes("assertion failed") 
+            ... 
+          </k>
       requires SELECTOR ==Int selector ( "assertEq(string,string)" )
         orBool SELECTOR ==Int selector ( "assertEq(bytes,bytes)" )
     [preserves-definedness]

src/kontrol/kdist/cheatcodes.md

@@ -43,6 +43,9 @@ module FOUNDRY-CHEAT-CODES
     imports EVM-ABI
     imports FOUNDRY-ACCOUNTS
     imports INFINITE-GAS
+    imports ID
+    imports BYTES
+    imports STRING
 
     configuration
       <cheatcodes>
@@ -92,6 +95,7 @@ module FOUNDRY-CHEAT-CODES
                <mockFunctionValues>  .Map </mockFunctionValues>
             </mockFunction>
          </mockFunctions>
+         <envVars> .Map </envVars>
       </cheatcodes>
 ```
 
@@ -642,6 +646,68 @@ 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-bytes]:
+               <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>
+         requires SELECTOR ==Int selector( "envOr(string,string)" ) orBool SELECTOR ==Int selector( "envOr(string,bytes)" )
+         [preserves-definedness]
+
+    rule [envOr-word-array]:
+          <k> #cheatcode_call SELECTOR ARGS =>
+           #getEnvOrArray SELECTOR
+                          #range(ARGS, 128, #asWord(#range(ARGS, 96, 32))) // KEY_VALUE
+                          Bytes2String( #range(ARGS, #asWord(#range(ARGS, 32, 32)) +Int 32, #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32)))) // DELIMITER
+                          (Int2Bytes(32, 32, BE) +Bytes #range(ARGS, #asWord(#range(ARGS, 64, 32)), lengthBytes(ARGS) -Int #asWord(#range(ARGS, 64, 32)))) // DEFAULT_VALUE
+            ...
+          </k>
+      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[])" ) )
+         SetItem( selector ( "envOr(string,string,string[])" ) )
+      )
+      [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
 ---------------------------------
 
@@ -1877,6 +1943,125 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
          <wordStack> _ : WS => 1 : WS </wordStack>
 ```
 
+- `#getEnvOrValue` will get and process the environment variable from the `<enVars>` mapping if it's there, or will return the default value for the variable otherwise.
+
+```k
+    syntax KItem ::= "#getEnvOrValue" Int Bytes Bytes [symbol(foundry_getEnvOrValue)]
+ // -----------------------------------------------------------------------------
+    rule <k> #getEnvOrValue SELECTOR VARNAME _ => .K ... </k>
+         <envVars> ... VARNAME |-> VARVALUE ... </envVars>
+         <output> _ => #enc( valueAsTypedArg(SELECTOR, VARVALUE) ) </output>
+      requires valueAsTypedArg(SELECTOR, VARVALUE) =/=K #bytes( .Bytes )
+
+    rule <k> #getEnvOrValue _ _ VARDEFAULTVALUE => .K ... </k>
+         <output> _ => VARDEFAULTVALUE </output>
+    [owise]
+```
+
+- `#getEnvOrArray` will get and process the environment variable from the `<enVars>` mapping if it's there, or will return the default array value for the variable otherwise.
+
+```k
+    syntax KItem ::= "#getEnvOrArray" Int Bytes String Bytes [symbol(foundry_getEnvOrArray)]
+ // -----------------------------------------------------------------------------
+    rule <k> #getEnvOrArray SELECTOR VARNAME DELIMITER VARDEFAULTVALUE =>
+               #let VALUES = split(VARVALUE, DELIMITER) #in
+               #processArrayOutput size(VALUES) mapTypedArgValue(SELECTOR, VALUES) VARDEFAULTVALUE
+            ...
+         </k>
+         <envVars> ... VARNAME |-> VARVALUE ... </envVars>
+
+    rule <k> #getEnvOrArray _ _ _ VARDEFAULTVALUE => .K ... </k>
+         <output> _ => VARDEFAULTVALUE </output>
+    [owise]
+```
+
+- ` #processArrayOutput` will process the output as an array based on the variable value retrieved from the environment variable mapping.
+
+```k
+    syntax KItem ::= "#processArrayOutput" Int TypedArgs Bytes [symbol(foundry_processArrayOutput)]
+   // -----------------------------------------------------------------------------
+    rule <k> #processArrayOutput SIZE OUT _ => .K ... </k>
+         <output> _ => #enc( #tuple( #array(#bytes( .Bytes ), SIZE, OUT) ) ) </output>
+      requires sizeOfTypedArgs(OUT) ==Int SIZE
+
+    rule <k> #processArrayOutput _ _ 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]
+
+
+syntax Bool ::= isHexString(String) [function]
+
+rule isHexString(S) => true
+  requires String2Base(replaceAll(S, "0x", ""), 16) ==K 0
+       orBool String2Base(replaceAll(S, "0x", ""), 16) =/=K 0
+rule isHexString(_) => false [owise]
+
+syntax TypedArg ::= valueAsTypedArg ( Int , String ) [function]
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #int256( String2Int(VALUE) )
+   requires (SELECTOR ==Int selector ( "envOr(string,int256)" ) orBool SELECTOR ==Int selector ( "envOr(string,string,int256[])" ))
+      andBool isIntegerString(VALUE)
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #uint256( String2Int(VALUE) )
+   requires (SELECTOR ==Int selector ( "envOr(string,uint256)" ) orBool SELECTOR ==Int selector ( "envOr(string,string,uint256[])" ))
+      andBool isUnsignedIntegerString(VALUE)
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #address( #parseHexWord(VALUE) ) 
+   requires (SELECTOR ==Int selector ( "envOr(string,address)" ) orBool SELECTOR ==Int selector ( "envOr(string,string,address[])" ))
+      andBool (lengthString(VALUE) ==Int 42 orBool lengthString(VALUE) ==Int 40)
+      andBool isHexString(VALUE)
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #bytes32( #parseHexWord(VALUE) ) 
+   requires (SELECTOR ==Int selector ( "envOr(string,bytes32)" ) orBool SELECTOR ==Int selector ( "envOr(string,string,bytes32[])" ))
+      andBool (lengthString(VALUE) ==Int 66 orBool lengthString(VALUE) ==Int 64)
+      andBool isHexString(VALUE)
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #bool( bool2Word( String2Bool(VALUE) )) 
+   requires (SELECTOR ==Int selector ( "envOr(string,bool)" ) orBool SELECTOR ==Int selector ( "envOr(string,string,bool[])" ))
+      andBool (VALUE ==K "true" orBool VALUE ==K "false")
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #tuple( #string(VALUE))
+   requires SELECTOR ==Int selector ( "envOr(string,string)" )
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #string(VALUE) 
+   requires SELECTOR ==Int selector ( "envOr(string,string,string[])" )
+
+rule valueAsTypedArg(SELECTOR, VALUE) => #tuple( #bytes( #parseByteStack(VALUE) ))
+   requires (SELECTOR ==Int selector ( "envOr(string,bytes)" ) orBool SELECTOR ==Int selector ( "envOr(string,string,bytes[])" ))
+      andBool isHexString(VALUE)
+
+rule valueAsTypedArg(_, _) => #bytes( .Bytes )
+   [owise]
+
+syntax List ::= split ( String , String ) [function]
+rule split(S, D) => ListItem(S) requires findString(S, D, 0) ==Int -1
+rule split(S, D) => ListItem(substrString(S, 0, findString(S, D, 0))) split(substrString(S, findString(S, D, 0) +Int lengthString(D), lengthString(S)), D) requires findString(S, D, 0) =/=Int -1
+
+syntax TypedArgs ::= mapTypedArgValue (Int, List) [function]
+rule mapTypedArgValue(SELECTOR, ListItem(X) XS) => valueAsTypedArg(SELECTOR, X), mapTypedArgValue(SELECTOR, XS)
+   requires valueAsTypedArg(SELECTOR, X) =/=K #bytes( .Bytes )
+rule mapTypedArgValue(_, _) => .TypedArgs
+   [owise]
+
+syntax Int ::= sizeOfTypedArgs ( TypedArgs ) [function]
+rule sizeOfTypedArgs(.TypedArgs) => 0
+rule sizeOfTypedArgs(_ , TAIL) => 1 +Int sizeOfTypedArgs(TAIL)
+```
+
+
 Selectors
 ---------
 
@@ -1950,6 +2135,20 @@ Selectors for **implemented** cheat code functions.
     rule ( selector ( "toString(uint256)" )                        => 1761649582 )
     rule ( selector ( "toString(int256)" )                         => 2736964622 )
     rule ( selector ( "ffi(string[])" )                            => 2299921511 )
+    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.
@@ -2014,4 +2213,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
@@ -1005,8 +1005,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

@@ -332,6 +332,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: dict[str, str] = {}
+    if not file_path.exists():
+        return env_vars
+    with open(file_path, 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,34 @@ EnvTest.testEnvString()
 EnvTest.testEnvStringArray()
 EnvTest.testEnvUInt()
 EnvTest.testEnvUIntArray()
+EnvOrTest.testEnvOrUint256()
+EnvOrTest.testEnvOrUint256Default()
+EnvOrTest.testEnvOrUint256Bad()
+EnvOrTest.testEnvOrInt256()
+EnvOrTest.testEnvOrInt256Default()
+EnvOrTest.testEnvOrInt256Bad()
+EnvOrTest.testEnvOrAddress()
+EnvOrTest.testEnvOrAddressInt()
+EnvOrTest.testEnvOrAddressDefault()
+EnvOrTest.testEnvOrAddressBad()
+EnvOrTest.testEnvOrBytes32()
+EnvOrTest.testEnvOrBytes32Default()
+EnvOrTest.testEnvOrBytes32Bad()
+EnvOrTest.testEnvOrBool()
+EnvOrTest.testEnvOrBoolDefault()
+EnvOrTest.testEnvOrBoolBad()
+EnvOrTest.testEnvOrString()
+EnvOrTest.testEnvOrStringDefault()
+EnvOrTest.testEnvOrBytes()
+EnvOrTest.testEnvOrBytesDefault()
+EnvOrTest.testEnvOrArrayUint256()
+EnvOrTest.testEnvOrArrayUint256Default()
+EnvOrTest.testEnvOrArrayInt256()
+EnvOrTest.testEnvOrArrayAddress()
+EnvOrTest.testEnvOrArrayBytes32()
+EnvOrTest.testEnvOrArrayBool()
+EnvOrTest.testEnvOrArrayString()
+EnvOrTest.testEnvOrArrayStringDefault()
 ExpectCallTest.testExpectRegularCall()
 ExpectCallTest.testExpectStaticCall()
 ExpectRevertTest.test_expectRevert_bytes4()

src/tests/integration/test-data/foundry/.env

@@ -0,0 +1,21 @@
+UINT256=100
+BADUINT256=-100
+INT256=-100
+BADINT256=notanint
+ADDRESS=0x1234567890123456789012345678901234567890
+ADDRESSINT=7584896468543216876435687541650546890874
+BADADDRESS=0xGHIJKLMNOPQRSTUVWXYZ1234567890ABCDEFGHSL
+BYTES32=0x123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0
+BADBYTES32=0xbadbytes32_badbytes32_badbytes32_badbytes32_badbytes32_badbytes3
+BOOLFALSE=false
+BADBOOLFALSE=notaboolvalue
+BOOLTRUE=true
+BADBOOLTRUE=notaboolvalue
+BYTES=0xdeadbeef
+STRING=hello_world
+UINT256ARRAY=0,1,2,3,4
+INT256ARRAY=-2,-1,0,1,2
+ADDRESSARRAY=0x1234567890123456789012345678901234567890,0x2345678901234567890123456789012345678901,0x3456789012345678901234567890123456789012
+BYTES32ARRAY=0x123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0,0x15864864541fe8548484c8548654189d4184864a48618c54615156d165651f65,0x7468697264d18561e8691a891968f189868c18969d1868641f1818861685a189
+BOOLARRAY=true,false,true,false
+STRINGARRAY=one,two