diff --git a/crates/fv/src/lib.rs b/crates/fv/src/lib.rs
index a9c4a198c9..836b16ff7f 100644
--- a/crates/fv/src/lib.rs
+++ b/crates/fv/src/lib.rs
@@ -25,8 +25,10 @@ pub fn run_spec(name: &str, src_path: &str, src: &str, spec: &str) -> Result<(),
let out = Command::new("kevm")
.arg("prove")
.arg(spec_path.to_str().unwrap())
- .arg("--backend haskell")
+ .arg("--backend")
+ .arg("haskell")
.arg("--format-failures")
+ // we should define out own verification module
.arg("--directory")
.arg("tests/specs/erc20/verification/haskell")
.env("PATH", format!(".build/usr/bin:{}", path))
diff --git a/crates/fv/tests/specs.rs b/crates/fv/tests/specs.rs
index 30d6199c37..62148c4faa 100644
--- a/crates/fv/tests/specs.rs
+++ b/crates/fv/tests/specs.rs
@@ -8,8 +8,14 @@ macro_rules! test_spec {
let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
- fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec)
- .expect("spec failed");
+ if let Err(output) = fv::run_spec(
+ &stringify!($name).replace("_", "-"),
+ $src_path,
+ &src,
+ &spec
+ ) {
+ panic!("{}", output)
+ }
}
};
}
@@ -44,3 +50,17 @@ test_spec! { sanity_returns_in_cond2, "sanity/foo.fe", "sanity/returns_in_cond2.
test_spec_invalid! { sanity_returns_42_invalid, "sanity/foo.fe", "sanity/returns_42_invalid.k" }
test_spec_invalid! { sanity_returns_in_invalid, "sanity/foo.fe", "sanity/returns_in_invalid.k" }
test_spec_invalid! { sanity_returns_in_cond2_invalid, "sanity/foo.fe", "sanity/returns_in_cond2_invalid.k" }
+
+// encode/decode success
+test_spec! { abi_u256, "abi/foo.fe", "abi/u256.k" }
+test_spec! { abi_u8, "abi/foo.fe", "abi/u8.k" }
+test_spec! { abi_address, "abi/foo.fe", "abi/address.k" }
+test_spec! { abi_address_u16, "abi/foo.fe", "abi/address_u16.k" }
+
+// decode revert
+test_spec! { abi_address_revert, "abi/foo.fe", "abi/address_revert.k" }
+test_spec! { abi_address_u16_revert_0, "abi/foo.fe", "abi/address_u16_revert_0.k" }
+test_spec! { abi_address_u16_revert_1, "abi/foo.fe", "abi/address_u16_revert_1.k" }
+
+// storage
+test_spec! { store_u256, "storage/foo.fe", "storage/store_u256.k" }
diff --git a/crates/test-files/fixtures/kspecs/abi/address.k b/crates/test-files/fixtures/kspecs/abi/address.k
new file mode 100644
index 0000000000..55f6ee4ae8
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/address.k
@@ -0,0 +1,105 @@
+module $TEST_NAME
+ imports VERIFICATION
+
+ claim
+
+
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+
+ _ => EVMC_SUCCESS
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ #abiCallData("_address", #address(IN))
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+ // todo: check code
+
+ _ => EVMC_REVERT
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ // address sig ++ input
+ #buf(4, 652482574) ++ #buf(32, IN)
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+
+ _ => EVMC_SUCCESS
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ #abiCallData("_address_u16", #address(IN_ADDR), #uint16(IN_U16))
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+ // todo: check code
+
+ _ => EVMC_REVERT
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ // _address_u16 sig ++ input
+ #buf(4, 802626159) ++ #buf(32, IN_ADDR) ++ #buf(32, IN_U16)
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+ // todo: check code
+
+ _ => EVMC_REVERT
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ // _address_u16 sig ++ input
+ #buf(4, 802626159) ++ #buf(32, IN_ADDR) ++ #buf(32, IN_U16)
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID u256:
+ return baz
+
+ pub fn _address(baz: address) -> address:
+ return baz
+
+ pub fn _u8(baz: u8) -> u8:
+ return baz
+
+ pub fn _address_u16(bar: address, baz: u16) -> (address, u16):
+ return (bar, baz)
+
diff --git a/crates/test-files/fixtures/kspecs/abi/u256.k b/crates/test-files/fixtures/kspecs/abi/u256.k
new file mode 100644
index 0000000000..6b0c0c12d4
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/u256.k
@@ -0,0 +1,105 @@
+module $TEST_NAME
+ imports VERIFICATION
+
+ claim
+
+
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+
+ _ => EVMC_SUCCESS
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ #abiCallData("_u256", #uint256(IN))
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+
+ _ => EVMC_SUCCESS
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($Foo::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($Foo::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ #abiCallData("_u8", #uint8(IN))
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($Foo::RUNTIME)
+ _
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID #execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k b/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k
index 4756b57142..0e71314110 100644
--- a/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k
@@ -7,7 +7,7 @@ module $TEST_NAME
#execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in.k b/crates/test-files/fixtures/kspecs/sanity/returns_in.k
index 481b624ba8..424a2cf926 100644
--- a/crates/test-files/fixtures/kspecs/sanity/returns_in.k
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in.k
@@ -7,7 +7,7 @@ module $TEST_NAME
#execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k
index 18b3ea1635..5b2e30db9f 100644
--- a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k
@@ -7,7 +7,7 @@ module $TEST_NAME
#execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k
index 80ef9cbf8e..d9f5d61e87 100644
--- a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k
@@ -7,7 +7,7 @@ module $TEST_NAME
#execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k
index ab7739a78c..a7c57cd602 100644
--- a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k
@@ -7,7 +7,7 @@ module $TEST_NAME
#execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k
index 841308781d..9b94dcb1d3 100644
--- a/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k
@@ -7,7 +7,7 @@ module $TEST_NAME
#execute => #halt
1
NORMAL
- LONDON
+ ISTANBUL
diff --git a/crates/test-files/fixtures/kspecs/storage/foo.fe b/crates/test-files/fixtures/kspecs/storage/foo.fe
new file mode 100644
index 0000000000..4178ea8e5e
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/storage/foo.fe
@@ -0,0 +1,9 @@
+use std::evm
+
+contract StoreU256:
+ my_u256: u256
+
+ pub fn __call__(self):
+ unsafe:
+ evm::mstore(0, self.my_u256)
+ evm::return_mem(0, 32)
diff --git a/crates/test-files/fixtures/kspecs/storage/store_u256.k b/crates/test-files/fixtures/kspecs/storage/store_u256.k
new file mode 100644
index 0000000000..fb53e80378
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/storage/store_u256.k
@@ -0,0 +1,104 @@
+module $TEST_NAME
+ imports VERIFICATION
+
+ claim
+
+
+ #execute => #halt
+ 1
+ NORMAL
+ ISTANBUL
+
+
+
+
+ _ => EVMC_SUCCESS
+ _ => ?_
+ _
+ _
+ _ => ?_
+
+
+ #parseByteStack($StoreU256::RUNTIME)
+ #computeValidJumpDests(#parseByteStack($StoreU256::RUNTIME))
+
+ ACCT_ID // contract owner
+ CALLER_ID // who called this contract; in the beginning, origin // msg.sender
+
+ _
+
+ 0
+ .WordStack => ?_
+ .Memory => ?_
+ 0 => ?_
+ #gas(_VGAS) => ?_
+ 0 => ?_
+ _ => ?_
+
+ false // NOTE: non-static call
+ CALL_DEPTH
+
+
+
+ _
+ _
+ _ // TODO: more detail
+ _ => ?_
+ _ => ?_
+
+
+ _
+ ORIGIN_ID // who fires tx
+
+ _
+
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+ _
+
+
+
+
+ _
+
+ SetItem(ACCT_ID) _:Set
+
+
+
+ ACCT_ID
+ _
+ #parseByteStack($StoreU256::RUNTIME)
+ 60532348206132712130393038501709678949590013789985963502110323372208181384 |-> MY_U256 _:Map
+ _
+ _
+
+
+
+ _
+ _
+ _
+
+
+
+
+ requires 0 <=Int ACCT_ID andBool ACCT_ID ) -> yul::Express
pub fn nonce_to_ptr(nonce: usize) -> yul::Expression {
// set the last byte to `0x00` to ensure our pointer sits at the start of a word
let ptr = keccak::partial_right_padded(nonce.to_string().as_bytes(), 31);
+ println!("{}", ptr);
literal_expression! { (ptr) }
}
diff --git a/crates/yulgen/src/runtime/functions/abi.rs b/crates/yulgen/src/runtime/functions/abi.rs
index 9ad5312d99..a0f0653fac 100644
--- a/crates/yulgen/src/runtime/functions/abi.rs
+++ b/crates/yulgen/src/runtime/functions/abi.rs
@@ -409,9 +409,13 @@ pub fn decode_component_string(max_size: usize, location: AbiDecodeLocation) ->
pub fn is_left_padded() -> yul::Statement {
function_definition! {
function is_left_padded(size_bits, val) -> return_val {
- (let bits_shifted := sub(256, size_bits))
- (let shifted_val := shr(bits_shifted, val))
- (return_val := iszero(shifted_val))
+ (if (eq(size_bits, 0)) {
+ (return_val := 1)
+ (leave)
+ })
+
+ (let right_size := sub(256, size_bits))
+ (return_val := lt(val, (exp(2, right_size))))
}
}
}