diff --git a/Cargo.lock b/Cargo.lock index 45ac70a389..19c35bd711 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -358,6 +358,31 @@ dependencies = [ "cfg-if 1.0.0", ] +[[package]] +name = "crossterm" +version = "0.26.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a84cda67535339806297f1b331d6dd6320470d2a0fe65381e79ee9e156dd3d13" +dependencies = [ + "bitflags", + "crossterm_winapi", + "libc", + "mio", + "parking_lot 0.12.1", + "signal-hook", + "signal-hook-mio", + "winapi", +] + +[[package]] +name = "crossterm_winapi" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acdd7c62a3665c7f6830a51635d9ac9b23ed385797f70a83bb8bafe9c572ab2b" +dependencies = [ + "winapi", +] + [[package]] name = "crunchy" version = "0.2.2" @@ -658,6 +683,7 @@ dependencies = [ "fe-common", "fe-driver", "fe-parser", + "fe-proof-service", "fe-test-runner", "fs_extra", "include_dir", @@ -689,7 +715,7 @@ dependencies = [ "insta", "num-bigint", "num-traits", - "parking_lot_core", + "parking_lot_core 0.8.0", "petgraph", "pretty_assertions", "rstest", @@ -805,6 +831,7 @@ dependencies = [ "fe-common", "fe-mir", "fe-parser", + "fe-proof-service", "fe-test-runner", "fe-yulc", "indexmap", @@ -862,6 +889,16 @@ dependencies = [ "wasm-bindgen-test", ] +[[package]] +name = "fe-proof-service" +version = "0.23.0" +dependencies = [ + "colored", + "serde", + "serde_json", + "smol_str", +] + [[package]] name = "fe-test-files" version = "0.23.0" @@ -1158,6 +1195,7 @@ checksum = "1885e79c1fc4b10f0e172c475f458b7f7b93061064d98c3293e98c5ba0c8b399" dependencies = [ "autocfg", "hashbrown 0.12.3", + "serde", ] [[package]] @@ -1227,6 +1265,28 @@ dependencies = [ "cpufeatures", ] +[[package]] +name = "kevm" +version = "0.23.0" +dependencies = [ + "indexmap", + "smol_str", +] + +[[package]] +name = "kevm-proof-service" +version = "0.23.0" +dependencies = [ + "clap 3.2.23", + "crossterm", + "fe-proof-service", + "indexmap", + "kevm", + "serde", + "serde_yaml", + "smol_str", +] + [[package]] name = "lazy_static" version = "1.4.0" @@ -1311,6 +1371,18 @@ dependencies = [ "autocfg", ] +[[package]] +name = "mio" +version = "0.8.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "927a765cd3fc26206e66b296465fa9d3e5ab003e651c1b3c060e7956d96b19d2" +dependencies = [ + "libc", + "log", + "wasi", + "windows-sys", +] + [[package]] name = "num" version = "0.4.0" @@ -1459,7 +1531,17 @@ checksum = "6d7744ac029df22dca6284efe4e898991d28e3085c706c972bcd7da4a27a15eb" dependencies = [ "instant", "lock_api", - "parking_lot_core", + "parking_lot_core 0.8.0", +] + +[[package]] +name = "parking_lot" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f" +dependencies = [ + "lock_api", + "parking_lot_core 0.9.8", ] [[package]] @@ -1472,11 +1554,24 @@ dependencies = [ "cloudabi", "instant", "libc", - "redox_syscall", + "redox_syscall 0.1.57", "smallvec", "winapi", ] +[[package]] +name = "parking_lot_core" +version = "0.9.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93f00c865fe7cabf650081affecd3871070f26767e7b2070a3ffae14c654b447" +dependencies = [ + "cfg-if 1.0.0", + "libc", + "redox_syscall 0.3.5", + "smallvec", + "windows-targets", +] + [[package]] name = "petgraph" version = "0.6.3" @@ -1583,9 +1678,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.51" +version = "1.0.59" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5d727cae5b39d21da60fa540906919ad737832fe0b1c165da3a34d6548c849d6" +checksum = "6aeca18b86b413c660b781aa319e4e2648a3e6f9eadc9b47e9038e6fe9f3451b" dependencies = [ "unicode-ident", ] @@ -1616,9 +1711,9 @@ checksum = "a993555f31e5a609f617c12db6250dedcac1b0a85076912c436e6fc9b2c8e6a3" [[package]] name = "quote" -version = "1.0.23" +version = "1.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8856d8364d252a14d474036ea1358d63c9e6965c8e5c1885c18f73d70bff9c7b" +checksum = "1b9ab9c7eadfd8df19006f1cf1a4aed13540ed5cbc047010ece5826e10825488" dependencies = [ "proc-macro2", ] @@ -1696,6 +1791,15 @@ version = "0.1.57" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "41cc0f7e4d5d4544e8861606a285bb08d3e70712ccc7d2b84d7c0ccfaf4b05ce" +[[package]] +name = "redox_syscall" +version = "0.3.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29" +dependencies = [ + "bitflags", +] + [[package]] name = "regex" version = "1.7.1" @@ -1911,7 +2015,7 @@ dependencies = [ "lock_api", "log", "oorandom", - "parking_lot", + "parking_lot 0.11.1", "rustc-hash", "salsa-macros", "smallvec", @@ -2076,6 +2180,19 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_yaml" +version = "0.9.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9d684e3ec7de3bf5466b32bd75303ac16f0736426e5a4e0d6e489559ce1249c" +dependencies = [ + "indexmap", + "itoa", + "ryu", + "serde", + "unsafe-libyaml", +] + [[package]] name = "sha2" version = "0.10.6" @@ -2097,6 +2214,36 @@ dependencies = [ "keccak", ] +[[package]] +name = "signal-hook" +version = "0.3.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "732768f1176d21d09e076c23a93123d40bba92d50c4058da34d45c8de8e682b9" +dependencies = [ + "libc", + "signal-hook-registry", +] + +[[package]] +name = "signal-hook-mio" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29ad2e15f37ec9a6cc544097b78a1ec90001e9f71b81338ca39f430adaca99af" +dependencies = [ + "libc", + "mio", + "signal-hook", +] + +[[package]] +name = "signal-hook-registry" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d8229b473baa5980ac72ef434c4415e70c4b5e71b423043adb4ba059f89c99a1" +dependencies = [ + "libc", +] + [[package]] name = "signature" version = "1.6.4" @@ -2360,6 +2507,12 @@ version = "0.1.10" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" +[[package]] +name = "unsafe-libyaml" +version = "0.2.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1865806a559042e51ab5414598446a5871b561d21b6764f2eabb0dd481d880a6" + [[package]] name = "vec1" version = "1.10.1" @@ -2532,6 +2685,72 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-sys" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.48.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" + +[[package]] +name = "windows_i686_gnu" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" + +[[package]] +name = "windows_i686_msvc" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" + [[package]] name = "winnow" version = "0.3.4" diff --git a/Cargo.toml b/Cargo.toml index daafdfa420..806ad6088e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,5 +5,5 @@ members = ["crates/*"] opt-level = 3 [profile.dev] -# Speeds up the build. May need to diable for debugging. +# Speeds up the build. May need to disable for debugging. debug = 0 diff --git a/crates/analyzer/src/db.rs b/crates/analyzer/src/db.rs index f094a51ecc..e5ce2edf71 100644 --- a/crates/analyzer/src/db.rs +++ b/crates/analyzer/src/db.rs @@ -110,6 +110,8 @@ pub trait AnalyzerDb: SourceDb + Upcast + UpcastMut fn module_submodules(&self, module: ModuleId) -> Rc<[ModuleId]>; #[salsa::invoke(queries::module::module_tests)] fn module_tests(&self, module: ModuleId) -> Vec; + #[salsa::invoke(queries::module::module_invariants)] + fn module_invariants(&self, module: ModuleId) -> Vec; // Module Constant #[salsa::cycle(queries::module::module_constant_type_cycle)] diff --git a/crates/analyzer/src/db/queries/module.rs b/crates/analyzer/src/db/queries/module.rs index 37286fa1e9..ac8f585b5c 100644 --- a/crates/analyzer/src/db/queries/module.rs +++ b/crates/analyzer/src/db/queries/module.rs @@ -760,3 +760,12 @@ pub fn module_tests(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec { .filter(|function| function.is_test(db)) .collect() } + +pub fn module_invariants(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec { + ingot + .all_functions(db) + .iter() + .copied() + .filter(|function| function.is_invariant(db)) + .collect() +} diff --git a/crates/analyzer/src/namespace/items.rs b/crates/analyzer/src/namespace/items.rs index 779c719664..572fbb89d5 100644 --- a/crates/analyzer/src/namespace/items.rs +++ b/crates/analyzer/src/namespace/items.rs @@ -555,6 +555,10 @@ impl ModuleId { db.module_tests(*self) } + pub fn invariants(&self, db: &dyn AnalyzerDb) -> Vec { + db.module_invariants(*self) + } + /// Returns `true` if the `item` is in scope of the module. pub fn is_in_scope(&self, db: &dyn AnalyzerDb, item: Item) -> bool { if let Some(val) = item.module(db) { @@ -1351,6 +1355,13 @@ impl FunctionId { .iter() .any(|attribute| attribute.name(db) == "test") } + + pub fn is_invariant(&self, db: &dyn AnalyzerDb) -> bool { + Item::Function(*self) + .attributes(db) + .iter() + .any(|attribute| attribute.name(db) == "invariant") + } } trait FunctionsAsItems { diff --git a/crates/codegen/src/yul/isel/function.rs b/crates/codegen/src/yul/isel/function.rs index 9170ce2904..5707347a12 100644 --- a/crates/codegen/src/yul/isel/function.rs +++ b/crates/codegen/src/yul/isel/function.rs @@ -619,30 +619,12 @@ impl<'db, 'a> FuncLowerHelper<'db, 'a> { .ty(self.db.upcast(), &self.body.store) .deref(self.db.upcast()); match op { - BinOp::Add => self - .ctx - .runtime - .safe_add(self.db, lhs_expr, rhs_expr, inst_result_ty), - BinOp::Sub => self - .ctx - .runtime - .safe_sub(self.db, lhs_expr, rhs_expr, inst_result_ty), - BinOp::Mul => self - .ctx - .runtime - .safe_mul(self.db, lhs_expr, rhs_expr, inst_result_ty), - BinOp::Div => self - .ctx - .runtime - .safe_div(self.db, lhs_expr, rhs_expr, inst_result_ty), - BinOp::Mod => self - .ctx - .runtime - .safe_mod(self.db, lhs_expr, rhs_expr, inst_result_ty), - BinOp::Pow => self - .ctx - .runtime - .safe_pow(self.db, lhs_expr, rhs_expr, inst_result_ty), + BinOp::Add => expression! { add([lhs_expr], [rhs_expr]) }, + BinOp::Sub => expression! { sub([lhs_expr], [rhs_expr]) }, + BinOp::Mul => expression! { mul([lhs_expr], [rhs_expr]) }, + BinOp::Div => expression! { div([lhs_expr], [rhs_expr]) }, + BinOp::Mod => expression! { mod([lhs_expr], [rhs_expr]) }, + BinOp::Pow => expression! { pow([lhs_expr], [rhs_expr]) }, BinOp::Shl => expression! {shl([rhs_expr], [lhs_expr])}, BinOp::Shr if is_result_signed => expression! {sar([rhs_expr], [lhs_expr])}, BinOp::Shr => expression! {shr([rhs_expr], [lhs_expr])}, @@ -668,7 +650,8 @@ impl<'db, 'a> FuncLowerHelper<'db, 'a> { debug_assert!(to.is_primitive(self.db.upcast())); let value = self.value_expr(value); - self.ctx.runtime.primitive_cast(self.db, value, from_ty) + // self.ctx.runtime.primitive_cast(self.db, value, from_ty) + value } fn assign_inst_result(&mut self, inst: InstId, rhs: yul::Expression, rhs_ty: TypeId) { diff --git a/crates/codegen/src/yul/isel/test.rs b/crates/codegen/src/yul/isel/test.rs index 9fe6186933..71013957fd 100644 --- a/crates/codegen/src/yul/isel/test.rs +++ b/crates/codegen/src/yul/isel/test.rs @@ -21,13 +21,41 @@ pub fn lower_test(db: &dyn CodegenDb, test: FunctionId) -> yul::Object { .into_iter() .map(yul::Statement::FunctionDefinition) .collect(); - let test_func_name = identifier! { (db.codegen_function_symbol_name(test)) }; - let call = function_call_statement! {[test_func_name]()}; + let call = { + let test_func_name = identifier! { (db.codegen_function_symbol_name(test)) }; + let mut assignments = vec![]; + let mut call_args = vec![]; + + let mut arg_num = 0; + for param in test.signature(db.upcast()).params.iter() { + if param.name != "ctx" { + let arg_name = format!("arg_{}", arg_num); + let arg_ident = identifier! { (arg_name) }; + let arg_offset = literal_expression! { (arg_num * 32) }; + + assignments.append(&mut statements! { + (let [arg_ident.clone()] := mload([arg_offset.clone()])) + (mstore([arg_offset], 0)) + }); + + call_args.push(identifier_expression! { [arg_ident] }); + + arg_num += 1 + } + } + + let call = function_call_statement! {[test_func_name]([call_args...])}; + + statements! { + [assignments...] + [call] + } + }; let code = code! { [dep_functions...] [runtime_funcs...] - [call] + [call...] (stop()) }; diff --git a/crates/codegen/src/yul/runtime/mod.rs b/crates/codegen/src/yul/runtime/mod.rs index 5cb6fb7a64..8c2e55202b 100644 --- a/crates/codegen/src/yul/runtime/mod.rs +++ b/crates/codegen/src/yul/runtime/mod.rs @@ -163,7 +163,8 @@ pub trait RuntimeProvider { expression! { signextend([significant], [value]) } } else { let mask = BitMask::new(from_size); - expression! { and([value], [mask.as_expr()]) } + // expression! { and([value], [mask.as_expr()]) } + value } } diff --git a/crates/driver/Cargo.toml b/crates/driver/Cargo.toml index 31a17336e2..db1f7bbc9a 100644 --- a/crates/driver/Cargo.toml +++ b/crates/driver/Cargo.toml @@ -20,6 +20,7 @@ fe-codegen = {path = "../codegen", version = "^0.23.0"} fe-parser = {path = "../parser", version = "^0.23.0"} fe-yulc = {path = "../yulc", version = "^0.23.0", features = ["solc-backend"], optional = true} fe-test-runner = {path = "../test-runner", version = "^0.23.0"} +fe-proof-service = {path = "../proof-service", version = "^0.23.0"} indexmap = "1.6.2" vfs = "0.5.1" smol_str = "0.1.21" diff --git a/crates/driver/src/lib.rs b/crates/driver/src/lib.rs index 91c6a47012..d2fd46b5ea 100644 --- a/crates/driver/src/lib.rs +++ b/crates/driver/src/lib.rs @@ -7,6 +7,7 @@ use fe_common::db::Upcast; use fe_common::diagnostics::Diagnostic; use fe_common::files::FileKind; use fe_parser::ast::SmolStr; +use fe_proof_service::symbolic_test::SymbolicTest; use fe_test_runner::TestSink; use indexmap::{indexmap, IndexMap}; use serde_json::Value; @@ -86,6 +87,23 @@ pub fn compile_single_file_tests( } } +#[cfg(feature = "solc-backend")] +pub fn compile_single_file_invariants( + db: &mut Db, + path: &str, + src: &str, + optimize: bool, +) -> Result, CompileError> { + let module = ModuleId::new_standalone(db, path, src); + let diags = module.diagnostics(db); + + if diags.is_empty() { + Ok(compile_module_invariants(db, module, optimize)) + } else { + Err(CompileError(diags)) + } +} + // Run analysis with ingot // Return vector error,waring... pub fn check_ingot( @@ -196,6 +214,7 @@ fn compile_test(db: &mut Db, test: FunctionId, optimize: bool) -> CompiledTest { let yul_test = fe_codegen::yul::isel::lower_test(db, test) .to_string() .replace('"', "\\\""); + // println!("{}", yul_test); let bytecode = compile_to_evm("test", &yul_test, optimize); CompiledTest::new(test.name(db), bytecode) } @@ -209,6 +228,26 @@ fn compile_module_tests(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec .collect() } +#[cfg(feature = "solc-backend")] +fn compile_module_invariants(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec { + use fe_proof_service::symbolic_test::Invariant; + + module_id + .invariants(db) + .iter() + .map(|test| { + let args = test + .signature(db) + .params + .iter() + .map(|param| param.typ.as_ref().unwrap().name(db)) + .collect(); + let test = compile_test(db, *test, optimize); + Invariant::new(test.name, args, test.bytecode) + }) + .collect() +} + #[cfg(feature = "solc-backend")] fn compile_module( db: &mut Db, diff --git a/crates/fe/Cargo.toml b/crates/fe/Cargo.toml index 2915d5bf45..46f8295a3a 100644 --- a/crates/fe/Cargo.toml +++ b/crates/fe/Cargo.toml @@ -24,3 +24,4 @@ fe-test-runner = {path = "../test-runner", version = "^0.23.0"} fe-common = {path = "../common", version = "^0.23.0"} fe-driver = {path = "../driver", version = "^0.23.0"} fe-parser = {path = "../parser", version = "^0.23.0"} +fe-proof-service = {path = "../proof-service", version = "^0.23.0"} diff --git a/crates/fe/foo.fe b/crates/fe/foo.fe new file mode 100644 index 0000000000..e69de29bb2 diff --git a/crates/fe/src/main.rs b/crates/fe/src/main.rs index 71f4781428..dfbc02e423 100644 --- a/crates/fe/src/main.rs +++ b/crates/fe/src/main.rs @@ -30,5 +30,9 @@ fn main() { Commands::Test(arg) => { task::test(arg); } + #[cfg(feature = "solc-backend")] + Commands::Prove(arg) => { + task::prove(arg); + } } } diff --git a/crates/fe/src/task/mod.rs b/crates/fe/src/task/mod.rs index 34ac1b6350..fdfc1b1e11 100644 --- a/crates/fe/src/task/mod.rs +++ b/crates/fe/src/task/mod.rs @@ -2,6 +2,8 @@ mod build; mod check; mod new; #[cfg(feature = "solc-backend")] +mod prove; +#[cfg(feature = "solc-backend")] mod test; mod utils; @@ -10,6 +12,8 @@ pub use check::{check, CheckArgs}; use clap::Subcommand; pub use new::{create_new_project, NewProjectArgs}; #[cfg(feature = "solc-backend")] +pub use prove::{prove, ProveArgs}; +#[cfg(feature = "solc-backend")] pub use test::{test, TestArgs}; #[derive(Subcommand)] @@ -19,4 +23,6 @@ pub enum Commands { New(NewProjectArgs), #[cfg(feature = "solc-backend")] Test(TestArgs), + #[cfg(feature = "solc-backend")] + Prove(ProveArgs), } diff --git a/crates/fe/src/task/prove.rs b/crates/fe/src/task/prove.rs new file mode 100644 index 0000000000..a61ef528ed --- /dev/null +++ b/crates/fe/src/task/prove.rs @@ -0,0 +1,63 @@ +#![cfg(feature = "solc-backend")] +use clap::Args; +use fe_common::diagnostics::print_diagnostics; +use fe_proof_service::symbolic_test::Invariant; +use fe_proof_service::ProofClient; + +// const DEFAULT_OUTPUT_DIR_NAME: &str = "prove"; +// const DEFAULT_INGOT: &str = "main"; + +#[derive(Args)] +#[clap(about = "Generate specs for the current project")] +pub struct ProveArgs { + input_path: String, + name: Option, + #[clap(long, default_value = "127.0.0.1:7878")] + server: String, + #[clap(long, action)] + rerun: bool, + #[clap(long, takes_value(true))] + optimize: Option, +} + +fn single_file_invariants(input_path: &str, optimize: bool) -> Vec { + let mut db = fe_driver::Db::default(); + let content = match std::fs::read_to_string(input_path) { + Err(err) => { + eprintln!("Failed to load file: `{input_path}`. Error: {err}"); + std::process::exit(1) + } + Ok(content) => content, + }; + + match fe_driver::compile_single_file_invariants(&mut db, input_path, &content, optimize) { + Ok(invariants) => invariants, + Err(error) => { + eprintln!("Unable to compile {input_path}."); + print_diagnostics(&db, &error.0); + std::process::exit(1) + } + } +} + +pub fn prove(args: ProveArgs) { + let input_path = args.input_path; + let optimize = args.optimize.unwrap_or(true); + let rerun = args.rerun; + let invariants = single_file_invariants(&input_path, optimize); + let server = ProofClient::new(args.server); + + for invariant in invariants { + let name = invariant.name.clone(); + + if let Some(match_name) = &args.name { + if name.contains(match_name) { + let status = server.check_invariant(invariant, rerun); + println!("{0: <20} {1: <10}", &name, &status) + } + } else { + let status = server.check_invariant(invariant, rerun); + println!("{0:.<20}{1: <10}", &name, &status) + } + } +} diff --git a/crates/kevm-proof-service/Cargo.toml b/crates/kevm-proof-service/Cargo.toml new file mode 100644 index 0000000000..2da4f33129 --- /dev/null +++ b/crates/kevm-proof-service/Cargo.toml @@ -0,0 +1,20 @@ +[package] +authors = ["The Fe Developers "] +categories = ["cryptography::cryptocurrencies", "command-line-utilities", "development-tools"] +description = "proof backend for Fe defintions" +edition = "2021" +keywords = ["fe", "kevm"] +license = "GPL-3.0-or-later" +name = "kevm-proof-service" +repository = "https://github.com/ethereum/fe" +version = "0.23.0" + +[dependencies] +fe-proof-service = {path = "../proof-service", version = "^0.23.0"} +kevm = {path = "../kevm", version = "^0.23.0"} +smol_str = "0.1.21" +serde_yaml = "0.9" +serde = { version = "1.0", features = ["derive"] } +indexmap = { version="1.6.2", features = ["serde"] } +clap = {version="3.1.18", features = ["derive"]} +crossterm = "0.26.1" \ No newline at end of file diff --git a/crates/kevm-proof-service/db.yaml b/crates/kevm-proof-service/db.yaml new file mode 100644 index 0000000000..f39c449d98 --- /dev/null +++ b/crates/kevm-proof-service/db.yaml @@ -0,0 +1,21 @@ +7408176950684564775: + name: msg_sig + complete: false +16564614996415688757: + name: msg_sig + complete: false +6342915096082124860: + name: de_morgan_true + complete: true +11455748359517230147: + name: de_morgan_false + complete: true +4205870993505503282: + name: read_byte_shl_248 + complete: true +17646573292089816401: + name: shl_shr_248 + complete: true +13658001998889555973: + name: shl_shr_n + complete: false diff --git a/crates/kevm-proof-service/server.state b/crates/kevm-proof-service/server.state new file mode 100644 index 0000000000..5adea41603 --- /dev/null +++ b/crates/kevm-proof-service/server.state @@ -0,0 +1,13 @@ +SystemTime { tv_sec: 1689216017, tv_nsec: 193844161 } +queue: +name: de_morgan_true id: 6342915096082124860 status: Proving +name: de_morgan_false id: 11455748359517230147 status: Proving + +execution pool: +6342915096082124860 +11455748359517230147 + +db: +id: 7408176950684564775 entry: (name: msg_sig complete: false) +id: 16564614996415688757 entry: (name: msg_sig complete: false) + diff --git a/crates/kevm-proof-service/src/main.rs b/crates/kevm-proof-service/src/main.rs new file mode 100644 index 0000000000..b2adb771e4 --- /dev/null +++ b/crates/kevm-proof-service/src/main.rs @@ -0,0 +1,66 @@ +use fe_proof_service::{invariant::Invariant, serde_json}; +use std::{ + io::{BufRead, BufReader, BufWriter}, + net::{TcpListener, TcpStream}, +}; + +use server_impl::Server; + +mod server_impl; + +use clap::Parser; + +#[derive(Parser)] +#[clap(author, version, about, long_about = None)] +struct Args { + #[clap(short, long, default_value = "127.0.0.1:7878")] + bind_addrs: String, + #[clap(short, long, action)] + display: bool, + #[clap(short, long, default_value = "8")] + max_proofs: usize, + #[clap(short, long, default_value = "db.yaml")] + db_path: usize, +} + +fn main() { + let args = Args::parse(); + + let listener = TcpListener::bind(args.bind_addrs).unwrap(); + let mut server = Server::new("db.yaml"); + + if args.display { + server.display(); + } + + for stream in listener.incoming() { + let stream = stream.unwrap(); + connection_handler(&mut server, stream); + } +} + +fn connection_handler(server: &mut Server, mut stream: TcpStream) { + let mut stream_clone = stream.try_clone().unwrap(); + + let mut reader = BufReader::new(&mut stream); + let mut writer = BufWriter::new(&mut stream_clone); + + let invariant: Invariant = { + let mut invariant_encoded = String::new(); + reader.read_line(&mut invariant_encoded).unwrap(); + serde_json::from_str(&invariant_encoded).expect("unable to decode invariant") + }; + + let rerun: bool = { + let mut rerun_encoded = String::new(); + reader.read_line(&mut rerun_encoded).unwrap(); + serde_json::from_str(&rerun_encoded).expect("unable to decode rerun") + }; + + if rerun { + server.forget(invariant.id()); + } + + let status = server.verify(invariant); + serde_json::to_writer(&mut writer, &status).expect("unable to encode invariant status"); +} diff --git a/crates/kevm-proof-service/src/server_impl/db.rs b/crates/kevm-proof-service/src/server_impl/db.rs new file mode 100644 index 0000000000..8d8e5a9da5 --- /dev/null +++ b/crates/kevm-proof-service/src/server_impl/db.rs @@ -0,0 +1,87 @@ +use std::{fmt::Display, fs, io::Write}; + +use indexmap::{indexmap, IndexMap}; +use kevm::KSpec; +use serde::{Deserialize, Serialize}; +use smol_str::SmolStr; + +#[derive(Serialize, Deserialize)] +pub struct DbEntry { + name: SmolStr, + is_success: bool, +} + +impl DbEntry { + pub fn new(name: SmolStr, complete: bool) -> Self { + Self { name, complete } + } +} + +impl Display for DbEntry { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "name: {0: <20} complete: {1: <5}", + self.name, self.complete + ) + } +} + +pub struct Db { + path: String, + entries: IndexMap, +} + +impl Display for &Db { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + for (id, entry) in self.entries.iter() { + writeln!(f, "id: {0: <20} -> {1: <40}", id, entry)? + } + + Ok(()) + } +} + +impl Db { + pub fn new(path: &str) -> Self { + let content = fs::read(path).unwrap(); + + let entries: IndexMap = if content.len() == 0 { + indexmap! {} + } else { + serde_yaml::from_slice(&content).unwrap() + }; + + Db { + path: path.to_string(), + entries, + } + } + + pub fn write(&self) { + let mut file = fs::OpenOptions::new() + .write(true) + .create(true) + .truncate(true) + .open(&self.path) + .unwrap(); + file.write_all(serde_yaml::to_string(&self.entries).unwrap().as_bytes()) + .unwrap(); + } + + pub fn update(&mut self, id: u64, entry: DbEntry) { + self.entries.insert(id, entry); + } + + pub fn get(&self, id: u64) -> Option<&DbEntry> { + self.entries.get(&id) + } + + pub fn evict(&mut self, id: u64) { + self.entries.remove(&id); + } + + pub fn get_mut(&mut self, id: u64) -> Option<&mut DbEntry> { + self.entries.get_mut(&id) + } +} diff --git a/crates/kevm-proof-service/src/server_impl/mod.rs b/crates/kevm-proof-service/src/server_impl/mod.rs new file mode 100644 index 0000000000..a7572f9d9b --- /dev/null +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -0,0 +1,202 @@ +use std::{ + fmt::Display, + io::{self}, + sync::{Arc, Mutex}, + thread, + time::{self, Duration}, +}; + +use crossterm::{ + cursor::MoveTo, + execute, + terminal::{Clear, ClearType}, +}; +use fe_proof_service::{symbolic_test::SymbolicTest, ProofStatus}; +use indexmap::{indexmap, IndexMap}; +use kevm::{KSpec, KSpecExecPool}; +use smol_str::SmolStr; + +mod db; + +use self::db::Db; + +pub struct Server { + state: Arc>, +} + +impl Server { + pub fn new(db_path: &str, max_proofs: usize) -> Self { + let state = Arc::new(Mutex::new(ServerState::new(db_path))); + let state_clone = Arc::clone(&state); + + thread::spawn(move || loop { + thread::sleep(Duration::from_millis(100)); + + if let Ok(mut state) = state_clone.lock() { + state.update(); + } + }); + + Self { state } + } + + pub fn forget(&mut self, invariant_id: u64) { + self.state.lock().unwrap().db.evict(invariant_id); + self.state.lock().unwrap().queue.remove(invariant_id); + self.state.lock().unwrap().exec_pool.remove(invariant_id); + } + + pub fn verify(&mut self, invariant: Invariant) -> ProofStatus { + let id = invariant.id(); + let spec = Spec::new_from_invariant(invariant); + // println!("{}", &spec.k_spec); + self.state.lock().unwrap().add_spec(spec); + self.state.lock().unwrap().update(); + self.state.lock().unwrap().proof_status(id) + } + + pub fn display(&self) { + let state_clone = Arc::clone(&self.state); + + thread::spawn(move || loop { + let mut stdout = io::stdout(); + execute!(stdout, Clear(ClearType::All)).unwrap(); + + let content = format!("{}", state_clone.lock().unwrap()); + print!("{content}"); + + execute!(stdout, MoveTo(0, 0)).unwrap(); + thread::sleep(Duration::from_millis(1000)); + }); + } +} + +pub struct ServerState { + // contains all known tests + tests: IndexMap, + // tests waiting to be added to the pool + // first in first out allows for easy test prioritization + stack: Vec, + // currently executing tests + pool: KSpecExecPool, + // all tests that have been completed + db: Db, +} + +impl Display for ServerState { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!(f, "{:?}", time::SystemTime::now())?; + writeln!(f, "")?; + + writeln!(f, "queue:")?; + writeln!(f, "{:?}", &self.queue)?; + + writeln!(f, "execution pool:")?; + writeln!(f, "{:?}", &self.exec_pool)?; + + writeln!(f, "db:")?; + writeln!(f, "{}", &self.db) + } +} + +impl ServerState { + pub fn new(db_path: &str) -> Self { + ServerState { + tests: indexmap! {}, + stack: vec![], + pool: KSpecExecPool::new(), + db: Db::new(db_path), + } + } + + pub fn add_test(&mut self, test: SymbolicTest) { + let id = test.id(); + + if !self.stack.contains(id) && !self.db.contains(id) {} + } + + pub fn test_status(&self, id: u64) -> ProofStatus { + if self.queue.contains(id) { + // queued + } else if Some(result) = self.db.get(id) { + // valid or invalid + } else { + // unknown + } + } + + pub fn update(&mut self) { + let mut first_indices: IndexMap = indexmap! {}; + + let mut renames: Vec<(usize, SmolStr)> = vec![]; + let mut removals: Vec = vec![]; + let mut db_changed = false; + + for (index, spec) in self.queue.specs.iter_mut().enumerate() { + if let Some(first_index) = first_indices.get(&spec.invariant_id) { + // duplicate spec + renames.push((*first_index, spec.name.clone())); + removals.push(index); + } else { + // non-duplicate spec + first_indices.insert(spec.invariant_id, index); + + match spec.status { + ProofStatus::New => { + if let Some(entry) = self.db.get_mut(spec.invariant_id) { + spec.status = if entry.complete { + ProofStatus::Complete + } else { + ProofStatus::Incomplete + } + } else { + spec.status = ProofStatus::Ready + } + } + ProofStatus::Ready => { + self.exec_pool + .execute_spec(spec.invariant_id, spec.k_spec.clone()); + spec.status = ProofStatus::Proving + } + ProofStatus::Proving => { + if let Some(result) = self.exec_pool.get_status(spec.invariant_id) { + if result { + spec.status = ProofStatus::Complete + } else { + spec.status = ProofStatus::Incomplete + } + + self.exec_pool.remove(spec.invariant_id) + } + } + ProofStatus::Complete => { + self.db + .update(spec.invariant_id, DbEntry::new(spec.name.clone(), true)); + removals.push(index); + db_changed = true + } + ProofStatus::Incomplete => { + self.db + .update(spec.invariant_id, DbEntry::new(spec.name.clone(), false)); + removals.push(index); + db_changed = true + } + } + } + } + + if db_changed { + self.db.write(); + } + + for (index, name) in renames { + self.queue.specs[index].name = name + } + + removals.reverse(); + + for index in removals { + self.queue.specs.remove(index); + } + } +} diff --git a/crates/kevm/Cargo.toml b/crates/kevm/Cargo.toml new file mode 100644 index 0000000000..a73b011a73 --- /dev/null +++ b/crates/kevm/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "kevm" +version = "0.23.0" +authors = ["The Fe Developers "] +edition = "2021" +license = "GPL-3.0-or-later" +repository = "https://github.com/ethereum/fe" + +[dependencies] +smol_str = "0.1.21" +indexmap = { version="1.6.2", features = ["serde"] } \ No newline at end of file diff --git a/crates/kevm/src/lib.rs b/crates/kevm/src/lib.rs new file mode 100644 index 0000000000..4b3b870897 --- /dev/null +++ b/crates/kevm/src/lib.rs @@ -0,0 +1,286 @@ +use std::{ + env, + fmt::Display, + fs::{self, File}, + io::Write, + process::Command, + sync::{Arc, Mutex}, + thread, +}; + +use indexmap::{indexmap, IndexMap}; +use smol_str::SmolStr; + +const KSPEC_TEMPLATE: &str = include_str!("../templates/spec.k"); +const KACCT_TEMPLATE: &str = include_str!("../templates/account.k"); + +#[derive(Clone)] +pub enum KSymbol { + Name(SmolStr), + None, +} + +impl Display for KSymbol { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + KSymbol::Name(name) => write!(f, "{}", name), + KSymbol::None => write!(f, "_"), + } + } +} + +#[derive(Clone)] +pub enum KInt { + Literal(usize), + // a ^ b + Pow { base: Box, exp: Box }, +} + +impl KInt { + const TWO: Self = KInt::Literal(2); + + pub fn literal(value: usize) -> Self { + Self::Literal(value) + } + + pub fn pow_2(exp: usize) -> Self { + let exp = Self::Literal(exp); + + Self::Pow { + base: Box::new(Self::TWO), + exp: Box::new(exp), + } + } +} + +impl Display for KInt { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + KInt::Literal(value) => write!(f, "{}", value), + KInt::Pow { base, exp } => write!(f, "{} ^Int {}", base, exp), + } + } +} + +#[derive(Clone)] +pub enum KBuf { + Single { size: KInt, symbol: KSymbol }, + Concatenated { inners: Vec }, +} + +impl Display for KBuf { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + KBuf::Single { size, symbol } => { + write!(f, "#buf({}, {})", size, symbol) + } + KBuf::Concatenated { inners } => { + let s = inners + .iter() + .map(|inner| inner.to_string()) + .collect::>() + .join(" +Bytes "); + write!(f, "{}", s) + } + } + } +} + +#[derive(Clone)] +pub enum KBool { + And { a: Box, b: Box }, + Or { a: Box, b: Box }, + Gte { a: KInt, b: KInt }, + Lt { a: KInt, b: KInt }, +} + +impl Display for KBool { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + KBool::And { a, b } => write!(f, "{} andBool {}", a, b), + KBool::Or { a, b } => write!(f, "{} orBool {}", a, b), + KBool::Gte { a, b } => write!(f, "{} >=Int {}", a, b), + KBool::Lt { a, b } => write!(f, "{} , +} + +impl KSet { + pub fn new() -> Self { + KSet { members: vec![] } + } + + pub fn insert(&mut self, name: KSymbol) { + self.members.push(name) + } +} + +impl Display for KSet { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "{} _:Set", + self.members + .iter() + .map(|symbol| format!("SetItem({})", symbol)) + .collect::>() + .join(" ") + ) + } +} + +#[derive(Clone)] +struct KAccount { + name: KSymbol, + code: String, +} + +impl Display for KAccount { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "{}", + KACCT_TEMPLATE + .replace("$ACCT_ID", &format!("{}", self.name)) + .replace("$CODE", &format!("\"0x{}\"", self.code)) + ) + } +} + +#[derive(Clone)] +pub struct KSpec { + local_mem: KBuf, + code: String, + origin: KSymbol, + accounts: Vec, + requirements: KBool, +} + +fn account_symbol_set(accounts: &[KAccount]) -> KSet { + let mut set = KSet::new(); + + for account in accounts { + set.insert(account.name.clone()) + } + + set +} + +impl Display for KSpec { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let active_accounts = account_symbol_set(&self.accounts); + let accounts = self + .accounts + .iter() + .map(|account| account.to_string()) + .collect::>() + .join("\n"); + + write!( + f, + "{}", + KSPEC_TEMPLATE + .replace("$LOCAL_MEM", &format!("{}", self.local_mem)) + .replace("$CODE", &format!("\"0x{}\"", self.code)) + .replace("$ORIGIN", &format!("{}", self.origin)) + .replace("$ACTIVE_ACCOUNTS", &format!("{}", active_accounts)) + .replace("$ACCOUNTS", &format!("{}", accounts)) + .replace("$REQUIREMENTS", &format!("{}", self.requirements)) + ) + } +} + +impl KSpec { + pub fn execute(&self, fs_id: &str) -> bool { + let kevm_dir_path = env::var("KEVM_DIR").unwrap(); + let spec_dir_path = format!("{kevm_dir_path}/tests/specs/fe/{fs_id}"); + let spec_file_path = format!("{spec_dir_path}/invariant-spec.k"); + let log_file_path = format!("{fs_id}.out"); + + if fs::metadata(&spec_dir_path).is_err() { + fs::create_dir(&spec_dir_path).unwrap(); + } + + let mut file = fs::OpenOptions::new() + .write(true) + .create(true) + .truncate(true) + .open(spec_file_path) + .unwrap(); + file.write_all(self.to_string().as_bytes()).unwrap(); + + let mut cmd = Command::new("make"); + let log = File::create(log_file_path).expect("failed to open log"); + + cmd.arg("build") + .arg("test-prove-fe") + .arg("-j8") + .current_dir(kevm_dir_path) + .env("FS_ID", fs_id) + .stdout(log) + .status() + .unwrap() + .success() + } +} + +pub struct KSpecExecPool { + cur_executing: IndexMap>>>, +} + +impl KSpecExecPool { + pub fn new() -> Self { + Self { + cur_executing: indexmap! {}, + } + } + + pub fn execute_spec(&mut self, id: u64, spec: KSpec) { + let result = Arc::new(Mutex::new(None)); + let result_clone = Arc::clone(&result); + + thread::spawn(move || { + let result = spec.execute(&id.to_string()); + *result_clone.lock().unwrap() = Some(result) + }); + + if self.cur_executing.insert(id, result).is_some() { + panic!("already executing spec for this ID") + } + } + + pub fn get_status(&self, id: u64) -> Option { + self.cur_executing + .get(&id) + .unwrap() + .lock() + .unwrap() + .to_owned() + } + + pub fn remove(&mut self, id: u64) { + // todo: actually terminate the process isntead of just forgetting about it + self.cur_executing.remove(&id); + } +} + +impl Display for &KSpecExecPool { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + for id in self.cur_executing.keys() { + writeln!(f, "{}", id)? + } + + Ok(()) + } +} + +// #[test] +// fn test_returns() { +// let k_spec = KSpec::new(vec![], "".to_string()); +// assert!(k_spec.execute()) +// } diff --git a/crates/kevm/templates/account.k b/crates/kevm/templates/account.k new file mode 100644 index 0000000000..01bb124901 --- /dev/null +++ b/crates/kevm/templates/account.k @@ -0,0 +1,8 @@ + + $ACCT_ID + _ + #parseByteStack($CODE) + _ + _ + _ + diff --git a/crates/kevm/templates/spec.k b/crates/kevm/templates/spec.k new file mode 100644 index 0000000000..91a20931c3 --- /dev/null +++ b/crates/kevm/templates/spec.k @@ -0,0 +1,93 @@ +module INVARIANT-SPEC + imports VERIFICATION + + claim + + + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(0, 0) + _ => EVMC_SUCCESS + _ + _ + _ => ?_ + + + #parseByteStack($CODE) + #computeValidJumpDests(#parseByteStack($CODE)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + _ + + 0 + .WordStack => ?_ + $LOCAL_MEM + 0 => ?_ + #gas(_VGAS) => ?_ + 0 => ?_ + _ => ?_ + + false // NOTE: non-static call + CALL_DEPTH + + + + _ + _ + _ + _ => ?_ + _ => ?_ + + + _ + $ORIGIN + + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + + + + + _ + + $ACTIVE_ACCOUNTS + + + $ACCOUNTS + + + _ + _ + _ + + + + + requires $REQUIREMENTS + +endmodule + diff --git a/crates/library/std/src/buf.fe b/crates/library/std/src/buf.fe index 291471f4a4..4eae7ff840 100644 --- a/crates/library/std/src/buf.fe +++ b/crates/library/std/src/buf.fe @@ -29,7 +29,7 @@ struct Cursor { /// Reverts if the cursor is advanced beyond the given length. pub fn advance(mut self, len: u256) -> u256 { let cur: u256 = self.cur - assert cur + len < self.len + 1 + // assert cur + len < self.len + 1 self.cur += len return cur } @@ -47,7 +47,7 @@ pub struct MemoryBuffer { pub fn new(len: u256) -> Self { unsafe { - return MemoryBuffer(offset: alloc(len), len) + return MemoryBuffer(offset: alloc(len: len + 31), len) } } @@ -103,7 +103,8 @@ pub struct MemoryBufferWriter { pub fn write_n(mut self, value: u256, len: u256) { let offset: u256 = self.write_offset(len) - unsafe { rewrite_slot(offset, value, len) } + let shifted_value: u256 = evm::shl(bits: 256 - len * 8, value) + unsafe { evm::mstore(offset, value: shifted_value) } } pub fn write_buf(mut self, buf: MemoryBuffer) { @@ -164,8 +165,7 @@ impl MemoryBufferWrite for u16 { impl MemoryBufferWrite for u8 { fn write_buf(self, mut writer: MemoryBufferWriter) { - let offset: u256 = writer.write_offset(len: 1) - unsafe { evm::mstore8(offset, value: self) } + writer.write_n(value: u256(self), len: 1) } } @@ -174,27 +174,6 @@ impl MemoryBufferWrite for () { fn write_buf(self, mut writer: MemoryBufferWriter) {} } -/// Rewrites the left-most `len` bytes in slot with the right-most `len` bytes of `value`. -unsafe fn rewrite_slot(offset: u256, value: u256, len: u256) { - // bit mask for right side of 256 bit slot - let mask: u256 = evm::shr( - bits: len * 8, - value: 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff - ) - // new value shifted to left - let shifted_value: u256 = evm::shl( - bits: 256 - len * 8, - value - ) - - let old_value: u256 = evm::mload(offset) - let new_value: u256 = evm::bitwise_or( - evm::bitwise_and(mask, old_value), - shifted_value - ) - evm::mstore(offset, value: new_value) -} - /// Memory buffer reader abstraction. pub struct MemoryBufferReader { buf: MemoryBuffer diff --git a/crates/library/std/src/spec.fe b/crates/library/std/src/spec.fe new file mode 100644 index 0000000000..9be092483b --- /dev/null +++ b/crates/library/std/src/spec.fe @@ -0,0 +1,85 @@ +use ingot::evm + +fn valid() { + unsafe { + evm::return_mem(offset: 0, len: 0) + } +} + +fn invalid() { + unsafe { + evm::revert_mem(offset: 0, len: 0) + } +} + +pub fn given_eq(_ a: u256, _ b: u256) { + if evm::eq(a, b) == 0 { + valid() + } +} + +pub fn given_ne(_ a: u256, _ b: u256) { + if evm::eq(a, b) == 1 { + valid() + } +} + +pub fn given_lte(_ a: u256, _ b: u256) { + if evm::gt(a, b) == 1 { + valid() + } +} + +pub fn given_gte(_ a: u256, _ b: u256) { + if evm::lt(a, b) == 1 { + valid() + } +} + +pub fn given_true(_ a: bool) { + if not a { + valid() + } +} + +pub fn given_false(_ a: bool) { + if a { + valid() + } +} + +pub fn assert_eq(_ a: u256, _ b: u256) { + if evm::eq(a, b) == 0 { + invalid() + } +} + +pub fn assert_ne(_ a: u256, _ b: u256) { + if evm::eq(a, b) == 1 { + invalid() + } +} + +pub fn assert_lte(_ a: u256, _ b: u256) { + if evm::gt(a, b) == 1 { + invalid() + } +} + +pub fn assert_gte(_ a: u256, _ b: u256) { + if evm::lt(a, b) == 1 { + invalid() + } +} + +pub fn assert_true(_ a: bool) { + if not a { + invalid() + } +} + +pub fn assert_false(_ a: bool) { + if a { + invalid() + } +} diff --git a/crates/proof-service/Cargo.toml b/crates/proof-service/Cargo.toml new file mode 100644 index 0000000000..e35dcaf782 --- /dev/null +++ b/crates/proof-service/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "fe-proof-service" +version = "0.23.0" +authors = ["The Fe Developers "] +edition = "2021" +license = "GPL-3.0-or-later" +repository = "https://github.com/ethereum/fe" + +[dependencies] +smol_str = "0.1.21" +serde = { version = "1.0", features = ["derive"] } +serde_json = { version = "1.0" } +colored = "2.0.0" \ No newline at end of file diff --git a/crates/proof-service/src/lib.rs b/crates/proof-service/src/lib.rs new file mode 100644 index 0000000000..497e9a199a --- /dev/null +++ b/crates/proof-service/src/lib.rs @@ -0,0 +1,64 @@ +use serde::{Deserialize, Serialize}; +use std::fmt::Display; +use std::io::{BufReader, BufWriter, Write}; +use std::net::{SocketAddr, TcpStream, ToSocketAddrs}; +use symbolic_test::SymbolicTest; + +pub use serde_json; + +pub mod symbolic_test; + +pub struct ProofClient(SocketAddr); + +#[derive(PartialEq, Eq, Serialize, Deserialize, Clone, Copy, Debug)] +pub enum ProofStatus { + New, + Ready, + Proving, + Complete, + Incomplete, +} + +impl Display for &ProofStatus { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + ProofStatus::New => write!(f, "New"), + ProofStatus::Ready => write!(f, "Queued"), + ProofStatus::Proving => write!(f, "Proving"), + ProofStatus::Complete => write!(f, "Complete"), + ProofStatus::Incomplete => write!(f, "Incomplete"), + } + } +} + +impl ProofClient { + pub fn new(addr: A) -> Self + where + A: ToSocketAddrs, + { + Self(addr.to_socket_addrs().unwrap().into_iter().last().unwrap()) + } +} + +impl ProofClient { + pub fn prove_symbolic_test(&self, test: SymbolicTest, rerun: bool) -> ProofStatus { + let mut stream = TcpStream::connect(self.0).expect("connection failed"); + let mut stream_clone = stream.try_clone().unwrap(); + + let mut reader = BufReader::new(&mut stream); + let mut writer = BufWriter::new(&mut stream_clone); + + let encoded_invariant = serde_json::to_string(&test).unwrap(); + writer.write(encoded_invariant.as_bytes()).unwrap(); + writer.write("\n".as_bytes()).unwrap(); + writer.flush().unwrap(); + + let encoded_rerun = serde_json::to_string(&rerun).unwrap(); + writer.write(encoded_rerun.as_bytes()).unwrap(); + writer.write("\n".as_bytes()).unwrap(); + writer.flush().unwrap(); + + let status = serde_json::from_reader(&mut reader).unwrap(); + status + } +} diff --git a/crates/proof-service/src/symbolic_test.rs b/crates/proof-service/src/symbolic_test.rs new file mode 100644 index 0000000000..b806b12cc6 --- /dev/null +++ b/crates/proof-service/src/symbolic_test.rs @@ -0,0 +1,33 @@ +use serde::{Deserialize, Serialize}; +use smol_str::SmolStr; +use std::{ + collections::hash_map::DefaultHasher, + hash::{Hash, Hasher}, +}; + +#[derive(Debug, Serialize, Deserialize)] +pub struct SymbolicTest { + pub name: SmolStr, + pub body: SymbolicTestBody, +} + +#[derive(Hash, Debug, Serialize, Deserialize)] +pub struct SymbolicTestBody { + pub args: Vec, + pub code: String, +} + +impl SymbolicTest { + pub fn new(name: SmolStr, args: Vec, code: String) -> Self { + Self { + name, + body: SymbolicTestBody { args, code }, + } + } + + pub fn id(&self) -> u64 { + let mut s = DefaultHasher::new(); + self.body.hash(&mut s); + s.finish() + } +} 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..d05a673f94 --- /dev/null +++ b/crates/test-files/fixtures/kspecs/abi/address.k @@ -0,0 +1,106 @@ +module $TEST_NAME + imports VERIFICATION + + claim + + + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => 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 + _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" + _ => 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 + + + + _ => #buf(32, OUT_ADDR) ++ #buf(32, OUT_U16) + _ => 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 + _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" + _ => 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 + _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" + _ => 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..3eb549999e --- /dev/null +++ b/crates/test-files/fixtures/kspecs/abi/u256.k @@ -0,0 +1,106 @@ +module $TEST_NAME + imports VERIFICATION + + claim + + + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => 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 + + + + _ => #buf(32, OUT) + _ => 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 + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($Returns42::RUNTIME) + #computeValidJumpDests(#parseByteStack($Returns42::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($Returns42::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($Returns42::RUNTIME) + #computeValidJumpDests(#parseByteStack($Returns42::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($Returns42::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($ReturnsIn::RUNTIME) + #computeValidJumpDests(#parseByteStack($ReturnsIn::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #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($ReturnsIn::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($ReturnsInCond::RUNTIME) + #computeValidJumpDests(#parseByteStack($ReturnsInCond::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #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($ReturnsInCond::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($ReturnsInCond::RUNTIME) + #computeValidJumpDests(#parseByteStack($ReturnsInCond::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #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($ReturnsInCond::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($ReturnsInCond::RUNTIME) + #computeValidJumpDests(#parseByteStack($ReturnsInCond::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #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($ReturnsInCond::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($ReturnsIn::RUNTIME) + #computeValidJumpDests(#parseByteStack($ReturnsIn::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #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($ReturnsIn::RUNTIME) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + + pub fn __call__(self): + unsafe: + let key: u256 = evm::call_data_load(offset: 0) + evm::mstore(offset: 0, value: self.my_map[key]) + evm::return_mem(offset: 0, len: 32) diff --git a/crates/test-files/fixtures/kspecs/storage/store_fe_map.k b/crates/test-files/fixtures/kspecs/storage/store_fe_map.k new file mode 100644 index 0000000000..cbe274cc25 --- /dev/null +++ b/crates/test-files/fixtures/kspecs/storage/store_fe_map.k @@ -0,0 +1,110 @@ +module $TEST_NAME + imports VERIFICATION + + claim + + + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + #buf(32, VAL) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($StoreFeMap::RUNTIME) + #computeValidJumpDests(#parseByteStack($StoreFeMap::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #buf(32, KEY) + + 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($StoreFeMap::RUNTIME) + #hashedLocation("Fe", 0, KEY) |-> VAL _:Map + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + #buf(32, VAL) + _ => EVMC_SUCCESS + _ => ?_ + _ + _ + _ => ?_ + + + #parseByteStack($StoreSolMap::RUNTIME) + #computeValidJumpDests(#parseByteStack($StoreSolMap::RUNTIME)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + #buf(32, KEY) + + 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($StoreSolMap::RUNTIME) + #hashedLocation("Solidity", 0, KEY) |-> VAL _:Map + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(32, OUT) + _ => 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 u256 { + return evm::mul(a, a) +} + +// #invariant +// // rewrite fails +// fn simple7(a: u256, b: u256, c: u256) { +// spec::given_lte(a, 1023) +// spec::given_lte(b, 1023) +// spec::given_lte(c, 1023) + +// // a ^ 2 + b ^ 2 = c ^ 2 +// spec::given_eq( +// evm::add(sq(a), sq(a)), +// sq(c) +// ) +// spec::given_eq(b, 4) + +// spec::assert_eq(c, 5) +// } + +#invariant +fn simple8(a: u256, b: u256, c: u256) { + spec::given_eq(a, 42) + spec::given_eq(c, 68) + spec::given_eq(b, 1023) + + // a + b = c + spec::given_eq(evm::add(a, b), c) + + spec::assert_eq(b, 26) +} + +#invariant +fn simple9(a: bool, b: bool) { + spec::given_false(a) + spec::given_true(b) + + spec::assert_true(a or b) + spec::assert_false(a and b) +} + +#invariant +fn simple10(ctx: Context) { + spec::given_lte(ctx.block_number(), 26) + spec::assert_ne(ctx.block_number(), 27) +} \ No newline at end of file diff --git a/out.yul b/out.yul new file mode 100644 index 0000000000..7ec5a7c3f3 --- /dev/null +++ b/out.yul @@ -0,0 +1,303 @@ +object \"test\" { + code { + function buf$rw_u16($a, $b) { + let $$tmp_2 := $$alloc(64) + let $$tmp_4 := $$alloc(64) + $$tmp_4 := buf$MemoryBuffer$new(4) + $mcopym($$tmp_4, $$tmp_2, 64) + let $$tmp_5 := $$alloc(128) + let $$tmp_6 := $$alloc(128) + $$tmp_6 := buf$MemoryBuffer$reader($$tmp_2) + $mcopym($$tmp_6, $$tmp_5, 128) + let $$tmp_7 := $$alloc(128) + let $$tmp_8 := $$alloc(128) + $$tmp_8 := buf$MemoryBuffer$writer($$tmp_2) + $mcopym($$tmp_8, $$tmp_7, 128) + buf$MemoryBufferWriter$write_u16($$tmp_7, $a) + buf$MemoryBufferWriter$write_u16($$tmp_7, $b) + let $$tmp_11 + $$tmp_11 := buf$MemoryBufferReader$read_u16($$tmp_5) + let $$tmp_12 + $$tmp_12 := $$tmp_11 + let $$tmp_13 + $$tmp_13 := $a + spec$assert_eq($$tmp_12, $$tmp_13) + let $$tmp_15 + $$tmp_15 := buf$MemoryBufferReader$read_u16($$tmp_5) + let $$tmp_16 + $$tmp_16 := $$tmp_15 + let $$tmp_17 + $$tmp_17 := $b + spec$assert_eq($$tmp_16, $$tmp_17) + leave + } + function buf$MemoryBuffer$new($len) -> $$ret { + let $$tmp_2 + $$tmp_2 := add($len, 31) + let $$tmp_3 + $$tmp_3 := buf$alloc($$tmp_2) + let $$tmp_4 := $$alloc(64) + $aggregate_init_10($$tmp_4, $$tmp_3, $len) + $$ret := $$tmp_4 + leave + } + function buf$MemoryBuffer$reader($self) -> $$ret { + let $$tmp_1 := $$alloc(128) + $$tmp_1 := buf$MemoryBufferReader$new($self) + let $$tmp_2 := $$alloc(128) + $mcopym($$tmp_1, $$tmp_2, 128) + $$ret := $$tmp_2 + leave + } + function buf$MemoryBuffer$writer($self) -> $$ret { + let $$tmp_1 := $$alloc(128) + $$tmp_1 := buf$MemoryBufferWriter$new($self) + let $$tmp_2 := $$alloc(128) + $mcopym($$tmp_1, $$tmp_2, 128) + $$ret := $$tmp_2 + leave + } + function buf$MemoryBufferWriter$write_u16($self, $value) { + buf$MemoryBufferWrite$u16$write_buf($value, $self) + leave + } + function buf$MemoryBufferReader$read_u16($self) -> $$ret { + let $$tmp_2 + $$tmp_2 := buf$MemoryBufferReader$read_n($self, 2) + let $$tmp_3 + $$tmp_3 := $$tmp_2 + $$ret := $$tmp_3 + leave + } + function spec$assert_eq($a, $b) { + let $$tmp_2 + $$tmp_2 := evm$eq($a, $b) + let $$tmp_4 + $$tmp_4 := eq($$tmp_2, 0) + switch $$tmp_4 + case 1 { spec$invalid() } + case 0 { } + leave + } + function buf$alloc($len) -> $$ret { + let $$tmp_1 + $$tmp_1 := buf$avail() + let $$tmp_3 + $$tmp_3 := add($$tmp_1, $len) + evm$mstore(64, $$tmp_3) + $$ret := $$tmp_1 + leave + } + function buf$MemoryBufferReader$new($buf) -> $$ret { + let $$tmp_1 := $$alloc(64) + $mcopym($buf, $$tmp_1, 64) + let $$tmp_2 + $$tmp_2 := buf$MemoryBuffer$len($buf) + let $$tmp_3 := $$alloc(64) + $$tmp_3 := buf$Cursor$new($$tmp_2) + let $$tmp_4 := $$alloc(64) + $mcopym($$tmp_3, $$tmp_4, 64) + let $$tmp_5 := $$alloc(128) + $aggregate_init_11($$tmp_5, $$tmp_1, $$tmp_4) + $$ret := $$tmp_5 + leave + } + function buf$MemoryBufferWriter$new($buf) -> $$ret { + let $$tmp_1 := $$alloc(64) + $mcopym($buf, $$tmp_1, 64) + let $$tmp_2 + $$tmp_2 := buf$MemoryBuffer$len($buf) + let $$tmp_3 := $$alloc(64) + $$tmp_3 := buf$Cursor$new($$tmp_2) + let $$tmp_4 := $$alloc(64) + $mcopym($$tmp_3, $$tmp_4, 64) + let $$tmp_5 := $$alloc(128) + $aggregate_init_12($$tmp_5, $$tmp_1, $$tmp_4) + $$ret := $$tmp_5 + leave + } + function buf$MemoryBufferWrite$u16$write_buf($self, $writer) { + let $$tmp_2 + $$tmp_2 := $self + buf$MemoryBufferWriter$write_n($writer, $$tmp_2, 2) + leave + } + function buf$MemoryBufferReader$read_n($self, $len) -> $$ret { + let $$tmp_2 + $$tmp_2 := buf$MemoryBufferReader$read_offset($self, $len) + let $$tmp_3 + $$tmp_3 := evm$mload($$tmp_2) + let $$tmp_6 + $$tmp_6 := mul($len, 8) + let $$tmp_7 + $$tmp_7 := sub(256, $$tmp_6) + let $$tmp_8 + $$tmp_8 := evm$shr($$tmp_7, $$tmp_3) + $$ret := $$tmp_8 + leave + } + function evm$eq($x, $y) -> $$ret { + let $$tmp_2 + $$tmp_2 := eq($x, $y) + $$ret := $$tmp_2 + leave + } + function spec$invalid() { + evm$revert_mem(0, 0) + leave + } + function buf$avail() -> $$ret { + let $$tmp_0 + $$tmp_0 := evm$mload(64) + let $$tmp_3 + $$tmp_3 := eq($$tmp_0, 0) + switch $$tmp_3 + case 1 { + $$ret := 96 + leave + } + case 0 { + $$ret := $$tmp_0 + leave + } + } + function evm$mstore($p, $v) { + mstore($p, $v) + leave + } + function buf$MemoryBuffer$len($self) -> $$ret { + let $$tmp_2 + $$tmp_2 := $$mptr_load(add($self, 32), 0) + $$ret := $$tmp_2 + leave + } + function buf$Cursor$new($len) -> $$ret { + let $$tmp_2 := $$alloc(64) + $aggregate_init_15($$tmp_2, 0, $len) + $$ret := $$tmp_2 + leave + } + function buf$MemoryBufferWriter$write_n($self, $value, $len) { + let $$tmp_3 + $$tmp_3 := buf$MemoryBufferWriter$write_offset($self, $len) + let $$tmp_4 + let $$tmp_7 + $$tmp_7 := mul($len, 8) + let $$tmp_8 + $$tmp_8 := sub(256, $$tmp_7) + $$tmp_4 := evm$shl($$tmp_8, $value) + evm$mstore($$tmp_3, $$tmp_4) + leave + } + function buf$MemoryBufferReader$read_offset($self, $len) -> $$ret { + let $$tmp_3 := $$alloc(64) + $$tmp_3 := add($self, 0) + let $$tmp_4 + $$tmp_4 := buf$MemoryBuffer$offset($$tmp_3) + let $$tmp_6 := $$alloc(64) + $$tmp_6 := add($self, 64) + let $$tmp_7 + $$tmp_7 := buf$Cursor$advance($$tmp_6, $len) + let $$tmp_8 + $$tmp_8 := add($$tmp_4, $$tmp_7) + $$ret := $$tmp_8 + leave + } + function evm$mload($p) -> $$ret { + let $$tmp_1 + $$tmp_1 := mload($p) + $$ret := $$tmp_1 + leave + } + function evm$shr($bits, $value) -> $$ret { + let $$tmp_2 + $$tmp_2 := shr($bits, $value) + $$ret := $$tmp_2 + leave + } + function evm$revert_mem($offset, $len) { revert($offset, $len) } + function buf$MemoryBufferWriter$write_offset($self, $len) -> $$ret { + let $$tmp_3 := $$alloc(64) + $$tmp_3 := add($self, 0) + let $$tmp_4 + $$tmp_4 := buf$MemoryBuffer$offset($$tmp_3) + let $$tmp_6 := $$alloc(64) + $$tmp_6 := add($self, 64) + let $$tmp_7 + $$tmp_7 := buf$Cursor$advance($$tmp_6, $len) + let $$tmp_8 + $$tmp_8 := add($$tmp_4, $$tmp_7) + $$ret := $$tmp_8 + leave + } + function evm$shl($bits, $value) -> $$ret { + let $$tmp_2 + $$tmp_2 := shl($bits, $value) + $$ret := $$tmp_2 + leave + } + function buf$MemoryBuffer$offset($self) -> $$ret { + let $$tmp_2 + $$tmp_2 := $$mptr_load(add($self, 0), 0) + $$ret := $$tmp_2 + leave + } + function buf$Cursor$advance($self, $len) -> $$ret { + let $$tmp_2 + $$tmp_2 := $$mptr_load(add($self, 0), 0) + let $$tmp_4 + $$tmp_4 := $$mptr_load(add($self, 0), 0) + $$mptr_store(add($self, 0), add($$tmp_4, $len), 0, 0x0) + $$ret := $$tmp_2 + leave + } + function $$alloc(size) -> ptr { + ptr := mload(64) + if eq(ptr, 0x00) { ptr := 96 } + mstore(64, add(ptr, size)) + } + function $mcopym($src, $dst, $size) { + let iter_count := div($size, 32) + let original_src := $src + for { let i := 0 } lt(i, iter_count) { i := add(i, 1) } { + mstore($dst, mload($src)) + $src := add($src, 32) + $dst := add($dst, 32) + } + let rem := sub($size, sub($src, original_src)) + if gt(rem, 0) { + let rem_bits := mul(rem, 8) + let dst_mask := sub(shl(sub(256, rem_bits), 1), 1) + let src_mask := not(dst_mask) + let src_value := and(mload($src), src_mask) + let dst_value := and(mload($dst), dst_mask) + mstore($dst, or(src_value, dst_value)) + } + } + function $$mptr_store(ptr, value, shift_num, mask) { + value := shl(shift_num, value) + let ptr_value := and(mload(ptr), mask) + value := or(value, ptr_value) + mstore(ptr, value) + } + function $aggregate_init_10($ptr, $arg0, $arg1) { + $$mptr_store(add($ptr, 0), $arg0, 0, 0x0) + $$mptr_store(add($ptr, 32), $arg1, 0, 0x0) + } + function $aggregate_init_11($ptr, $arg0, $arg1) { + $mcopym($arg0, add($ptr, 0), 64) + $mcopym($arg1, add($ptr, 64), 64) + } + function $aggregate_init_12($ptr, $arg0, $arg1) { + $mcopym($arg0, add($ptr, 0), 64) + $mcopym($arg1, add($ptr, 64), 64) + } + function $$mptr_load(ptr, shift_num) -> ret { ret := shr(shift_num, mload(ptr)) } + function $aggregate_init_15($ptr, $arg0, $arg1) { + $$mptr_store(add($ptr, 0), $arg0, 0, 0x0) + $$mptr_store(add($ptr, 32), $arg1, 0, 0x0) + } + buf$rw_u16(calldataload(0), calldataload(32)) + stop() + } +} diff --git a/server.state b/server.state new file mode 100644 index 0000000000..cde123c955 --- /dev/null +++ b/server.state @@ -0,0 +1,21 @@ +SystemTime { tv_sec: 1688767084, tv_nsec: 496605980 } +queue: + +execution pool: + +db: +id: 9866189969293882850 entry: (name: simple2 complete: true) +id: 6899393809540637772 entry: (name: simple10 complete: true) +id: 10648093925226451130 entry: (name: simple1 complete: true) +id: 17014316732147409137 entry: (name: simple4 complete: true) +id: 16497824417235581307 entry: (name: simple3 complete: true) +id: 14785961722918986698 entry: (name: simple5 complete: true) +id: 6672846181222220742 entry: (name: simple9 complete: true) +id: 2691375950895637890 entry: (name: simple8 complete: true) +id: 4205870993505503282 entry: (name: read_byte_shl_248 complete: true) +id: 17646573292089816401 entry: (name: shl_shr_248 complete: true) +id: 1491244125428245047 entry: (name: simple6 complete: true) +id: 6342915096082124860 entry: (name: de_morgan_true complete: true) +id: 14977842676755773493 entry: (name: verify_get_42 complete: false) +id: 14111824353587072050 entry: (name: verify_get_42 complete: false) + diff --git a/specs/spec-spec.k b/specs/spec-spec.k new file mode 100644 index 0000000000..d020be98bb --- /dev/null +++ b/specs/spec-spec.k @@ -0,0 +1,106 @@ +module SPEC-SPEC + imports VERIFICATION + + claim + + + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(0, 0) + _ => EVMC_SUCCESS + _ + _ + _ => ?_ + + + // todo: gen this part + #parseByteStack("0x6001601a43111460011460205760016019431414600114601b57005b600080fd5b00") + #computeValidJumpDests(#parseByteStack("0x6001601a43111460011460205760016019431414600114601b57005b600080fd5b00")) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + // todo: gen this part + #buf(32, ARG_0) + + 0 + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(_VGAS) => ?_ + 0 => ?_ + _ => ?_ + + false // NOTE: non-static call + CALL_DEPTH + + + + _ + _ + _ + _ => ?_ + _ => ?_ + + + _ + ORIGIN_ID + + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + + + + + _ + + SetItem(ACCT_ID) _:Set + + + + ACCT_ID + _ + #parseByteStack("0x6001601a43111460011460205760016019431414600114601b57005b600080fd5b00") + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID