From a255e19d41efe0a58e2197a0b565835ae5919f6b Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Thu, 18 May 2023 21:13:57 -0600 Subject: [PATCH 01/10] hacking --- Cargo.lock | 59 ++++- Cargo.toml | 2 +- crates/analyzer/src/db.rs | 2 + crates/analyzer/src/db/queries/module.rs | 9 + crates/analyzer/src/namespace/items.rs | 11 + crates/codegen/src/yul/isel/function.rs | 3 +- crates/codegen/src/yul/isel/test.rs | 16 +- crates/codegen/src/yul/runtime/mod.rs | 3 +- crates/driver/Cargo.toml | 1 + crates/driver/src/lib.rs | 39 ++++ crates/fe/Cargo.toml | 1 + crates/fe/fixtures/basic_equivalence.fe | 63 ++++++ crates/fe/fixtures/buf.fe | 79 +++++++ crates/fe/fixtures/sanity.fe | 98 +++++++++ crates/fe/foo.fe | 0 crates/fe/src/main.rs | 4 + crates/fe/src/task/mod.rs | 6 + crates/fe/src/task/prove.rs | 50 +++++ crates/kevm-proof-service/Cargo.toml | 18 ++ crates/kevm-proof-service/db.yaml | 36 +++ crates/kevm-proof-service/server.state | 19 ++ crates/kevm-proof-service/src/main.rs | 40 ++++ .../kevm-proof-service/src/server_impl/db.rs | 78 +++++++ .../kevm-proof-service/src/server_impl/mod.rs | 208 ++++++++++++++++++ .../src/server_impl/queue.rs | 87 ++++++++ crates/kevm/Cargo.toml | 11 + crates/kevm/src/lib.rs | 181 +++++++++++++++ crates/kevm/template.k | 106 +++++++++ crates/library/std/src/spec.fe | 85 +++++++ crates/proof-service/Cargo.toml | 12 + crates/proof-service/src/invariant.rs | 46 ++++ crates/proof-service/src/lib.rs | 62 ++++++ .../test-files/fixtures/kspecs/abi/address.k | 106 +++++++++ .../fixtures/kspecs/abi/address_revert.k | 107 +++++++++ .../fixtures/kspecs/abi/address_u16.k | 108 +++++++++ .../kspecs/abi/address_u16_revert_0.k | 112 ++++++++++ .../kspecs/abi/address_u16_revert_1.k | 112 ++++++++++ crates/test-files/fixtures/kspecs/abi/foo.fe | 13 ++ crates/test-files/fixtures/kspecs/abi/u256.k | 106 +++++++++ crates/test-files/fixtures/kspecs/abi/u8.k | 106 +++++++++ .../test-files/fixtures/kspecs/sanity/foo.fe | 31 +++ .../fixtures/kspecs/sanity/returns_42.k | 105 +++++++++ .../kspecs/sanity/returns_42_invalid.k | 106 +++++++++ .../fixtures/kspecs/sanity/returns_in.k | 106 +++++++++ .../fixtures/kspecs/sanity/returns_in_cond1.k | 108 +++++++++ .../fixtures/kspecs/sanity/returns_in_cond2.k | 106 +++++++++ .../kspecs/sanity/returns_in_cond2_invalid.k | 105 +++++++++ .../kspecs/sanity/returns_in_invalid.k | 106 +++++++++ .../test-files/fixtures/kspecs/storage/foo.fe | 30 +++ .../fixtures/kspecs/storage/store_fe_map.k | 110 +++++++++ .../fixtures/kspecs/storage/store_sol_map.k | 106 +++++++++ .../fixtures/kspecs/storage/store_u256.k | 106 +++++++++ specs/spec-spec.k | 106 +++++++++ 53 files changed, 3428 insertions(+), 8 deletions(-) create mode 100644 crates/fe/fixtures/basic_equivalence.fe create mode 100644 crates/fe/fixtures/buf.fe create mode 100644 crates/fe/fixtures/sanity.fe create mode 100644 crates/fe/foo.fe create mode 100644 crates/fe/src/task/prove.rs create mode 100644 crates/kevm-proof-service/Cargo.toml create mode 100644 crates/kevm-proof-service/db.yaml create mode 100644 crates/kevm-proof-service/server.state create mode 100644 crates/kevm-proof-service/src/main.rs create mode 100644 crates/kevm-proof-service/src/server_impl/db.rs create mode 100644 crates/kevm-proof-service/src/server_impl/mod.rs create mode 100644 crates/kevm-proof-service/src/server_impl/queue.rs create mode 100644 crates/kevm/Cargo.toml create mode 100644 crates/kevm/src/lib.rs create mode 100644 crates/kevm/template.k create mode 100644 crates/library/std/src/spec.fe create mode 100644 crates/proof-service/Cargo.toml create mode 100644 crates/proof-service/src/invariant.rs create mode 100644 crates/proof-service/src/lib.rs create mode 100644 crates/test-files/fixtures/kspecs/abi/address.k create mode 100644 crates/test-files/fixtures/kspecs/abi/address_revert.k create mode 100644 crates/test-files/fixtures/kspecs/abi/address_u16.k create mode 100644 crates/test-files/fixtures/kspecs/abi/address_u16_revert_0.k create mode 100644 crates/test-files/fixtures/kspecs/abi/address_u16_revert_1.k create mode 100644 crates/test-files/fixtures/kspecs/abi/foo.fe create mode 100644 crates/test-files/fixtures/kspecs/abi/u256.k create mode 100644 crates/test-files/fixtures/kspecs/abi/u8.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/foo.fe create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_42.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_in.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k create mode 100644 crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k create mode 100644 crates/test-files/fixtures/kspecs/storage/foo.fe create mode 100644 crates/test-files/fixtures/kspecs/storage/store_fe_map.k create mode 100644 crates/test-files/fixtures/kspecs/storage/store_sol_map.k create mode 100644 crates/test-files/fixtures/kspecs/storage/store_u256.k create mode 100644 specs/spec-spec.k diff --git a/Cargo.lock b/Cargo.lock index 45ac70a389..f6ba808d11 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -658,6 +658,7 @@ dependencies = [ "fe-common", "fe-driver", "fe-parser", + "fe-proof-service", "fe-test-runner", "fs_extra", "include_dir", @@ -805,6 +806,7 @@ dependencies = [ "fe-common", "fe-mir", "fe-parser", + "fe-proof-service", "fe-test-runner", "fe-yulc", "indexmap", @@ -862,6 +864,15 @@ dependencies = [ "wasm-bindgen-test", ] +[[package]] +name = "fe-proof-service" +version = "0.23.0" +dependencies = [ + "serde", + "serde_json", + "smol_str", +] + [[package]] name = "fe-test-files" version = "0.23.0" @@ -1158,6 +1169,7 @@ checksum = "1885e79c1fc4b10f0e172c475f458b7f7b93061064d98c3293e98c5ba0c8b399" dependencies = [ "autocfg", "hashbrown 0.12.3", + "serde", ] [[package]] @@ -1227,6 +1239,26 @@ dependencies = [ "cpufeatures", ] +[[package]] +name = "kevm" +version = "0.23.0" +dependencies = [ + "indexmap", + "smol_str", +] + +[[package]] +name = "kevm-proof-service" +version = "0.23.0" +dependencies = [ + "fe-proof-service", + "indexmap", + "kevm", + "serde", + "serde_yaml", + "smol_str", +] + [[package]] name = "lazy_static" version = "1.4.0" @@ -1583,9 +1615,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 +1648,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", ] @@ -2076,6 +2108,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" @@ -2360,6 +2405,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" 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..ad576c1f41 100644 --- a/crates/codegen/src/yul/isel/function.rs +++ b/crates/codegen/src/yul/isel/function.rs @@ -668,7 +668,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..b94473696a 100644 --- a/crates/codegen/src/yul/isel/test.rs +++ b/crates/codegen/src/yul/isel/test.rs @@ -22,7 +22,21 @@ pub fn lower_test(db: &dyn CodegenDb, test: FunctionId) -> yul::Object { .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_args = test + .signature(db.upcast()) + .params + .iter() + .enumerate() + .filter_map(|(n, param)| { + if param.name == "ctx" { + None + } else { + let value = literal_expression! { (n * 32) }; + Some(expression! { calldataload([value]) }) + } + }) + .collect::>(); + let call = function_call_statement! {[test_func_name]([call_args...])}; let code = code! { [dep_functions...] 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..373af4a760 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::invariant::Invariant; 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('"', "\\\""); + // panic!("{}", 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::invariant::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/fixtures/basic_equivalence.fe b/crates/fe/fixtures/basic_equivalence.fe new file mode 100644 index 0000000000..74779ae32c --- /dev/null +++ b/crates/fe/fixtures/basic_equivalence.fe @@ -0,0 +1,63 @@ +use std::spec +use std::evm + +#invariant +fn de_morgan_true(a: bool, b: bool) { + spec::given_true(a and b) + spec::assert_true(not ((not a) or (not b))) +} + +#invariant +fn de_morgan_false(a: bool, b: bool) { + spec::given_false(a and b) + spec::assert_false(not ((not a) or (not b))) +} + +#invariant +fn shl_shr_248(a: u256) { + spec::given_lte(a, 255) + + let shl_a: u256 = evm::shl(bits: 248, value: a) + spec::assert_eq( + a, + evm::shr(bits: 248, value: shl_a) + ) +} + +#invariant +fn shl_shr_n(a: u256, n: u256) { + spec::given_lte(a, 255) + spec::given_lte(n, 248) + + let shl_a: u256 = evm::shl(bits: n, value: a) + spec::assert_eq( + a, + evm::shr(bits: n, value: shl_a) + ) +} + +const FREE_MEM_PTR: u256 = 4096 + +#invariant +unsafe fn read_byte_shl_248(a: u8) { + evm::mstore( + offset: FREE_MEM_PTR, + value: evm::shl(bits: 248, value: a) + ) + + spec::assert_eq( + a, + evm::shr(bits: 248, value: evm::mload(offset: FREE_MEM_PTR)) + ) +} + +// #invariant +// incomplete +// unsafe fn read_byte_mstore8(a: u8) { +// evm::mstore8(offset: FREE_MEM_PTR, value: a) + +// spec::assert_eq( +// a, +// evm::shr(bits: 248, value: evm::mload(offset: FREE_MEM_PTR)) +// ) +// } diff --git a/crates/fe/fixtures/buf.fe b/crates/fe/fixtures/buf.fe new file mode 100644 index 0000000000..e8517de33a --- /dev/null +++ b/crates/fe/fixtures/buf.fe @@ -0,0 +1,79 @@ +use std::buf::{MemoryBuffer, MemoryBufferReader, MemoryBufferWriter} +use std::spec + +#invariant +fn rw_u8(a: u8, b: u8) { + let mut buf: MemoryBuffer = MemoryBuffer::new(len: 16) + let mut reader: MemoryBufferReader = buf.reader() + let mut writer: MemoryBufferWriter = buf.writer() + + writer.write_u8(value: a) + writer.write_u8(value: b) + + spec::assert_eq(reader.read_u8(), a) + spec::assert_eq(reader.read_u8(), b) +} + +#invariant +fn rw_single_u8(a: u8) { + let mut buf: MemoryBuffer = MemoryBuffer::new(len: 1) + let mut reader: MemoryBufferReader = buf.reader() + let mut writer: MemoryBufferWriter = buf.writer() + + writer.write_u8(value: a) + spec::assert_eq(reader.read_u8(), a) +} + +#invariant +fn rw_single_u16(a: u16) { + let mut buf: MemoryBuffer = MemoryBuffer::new(len: 2) + let mut reader: MemoryBufferReader = buf.reader() + let mut writer: MemoryBufferWriter = buf.writer() + + writer.write_u16(value: a) + spec::assert_eq(reader.read_u16(), a) +} + +#invariant +fn rw_u16(a: u16, b: u16) { + let mut buf: MemoryBuffer = MemoryBuffer::new(len: 4) + let mut reader: MemoryBufferReader = buf.reader() + let mut writer: MemoryBufferWriter = buf.writer() + + writer.write_u16(value: a) + writer.write_u16(value: b) + + spec::assert_eq(reader.read_u16(), a) + spec::assert_eq(reader.read_u16(), b) +} + + +#invariant +fn rw_u256(a: u256, b: u256) { + let mut buf: MemoryBuffer = MemoryBuffer::new(len: 64) + let mut reader: MemoryBufferReader = buf.reader() + let mut writer: MemoryBufferWriter = buf.writer() + + writer.write_u256(value: a) + writer.write_u256(value: b) + + spec::assert_eq(reader.read_u256(), a) + spec::assert_eq(reader.read_u256(), b) +} + +#invariant +fn rw_mix(a: u256, b: u8, c: u128, d: u128) { + let mut buf: MemoryBuffer = MemoryBuffer::new(len: 64) + let mut reader: MemoryBufferReader = buf.reader() + let mut writer: MemoryBufferWriter = buf.writer() + + writer.write_u256(value: a) + writer.write_u8(value: b) + writer.write_u128(value: c) + writer.write_u128(value: d) + + spec::assert_eq(reader.read_u256(), a) + spec::assert_eq(reader.read_u8(), b) + spec::assert_eq(reader.read_u128(), c) + spec::assert_eq(reader.read_u128(), d) +} diff --git a/crates/fe/fixtures/sanity.fe b/crates/fe/fixtures/sanity.fe new file mode 100644 index 0000000000..f4f4f59aea --- /dev/null +++ b/crates/fe/fixtures/sanity.fe @@ -0,0 +1,98 @@ +// use std::{evm, spec} +use std::spec +use std::evm + +#invariant +fn simple1(a: u256) { + spec::given_lte(a, 26) + + spec::assert_lte(a, 42) +} + +#invariant +fn simple2(a: u256) { + spec::given_lte(a, 42) + + spec::assert_ne(a, 43) +} + +#invariant +fn simple3(a: u256, b: u256) { + spec::given_lte(a, b) + spec::given_eq(a, 42) + + spec::assert_ne(b, 26) +} + +#invariant +fn simple4(a: u256, b: u256) { + spec::given_lte(a, 42) + spec::given_lte(b, 26) + + spec::assert_lte(evm::add(a, b), 68) +} + +#invariant +fn simple5(a: u256) { + spec::given_lte(a, 42) + spec::given_gte(a, 26) + + spec::assert_ne(a, 25) + spec::assert_ne(a, 45) +} + +#invariant +fn simple6(a: u256) { + spec::given_lte(a, 42) + spec::given_gte(a, 42) + + spec::assert_eq(a, 42) +} + +fn sq(_ a: u256) -> 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/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..97ab73d67a --- /dev/null +++ b/crates/fe/src/task/prove.rs @@ -0,0 +1,50 @@ +#![cfg(feature = "solc-backend")] +use clap::Args; +use fe_common::diagnostics::print_diagnostics; +use fe_proof_service::invariant::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, + #[clap(long, takes_value(true))] + optimize: Option, +} + +fn single_file_invariants(prove_arg: &ProveArgs) -> Vec { + let input_path = &prove_arg.input_path; + let optimize = prove_arg.optimize.unwrap_or(true); + + 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(prove_arg: ProveArgs) { + let invariants = single_file_invariants(&prove_arg); + let server = ProofClient::new("10.0.0.144:7878"); + + for invariant in invariants { + let name = invariant.name.clone(); + let status = server.check_invariant(invariant); + println!("{} (status: {})", &name, &status) + } +} diff --git a/crates/kevm-proof-service/Cargo.toml b/crates/kevm-proof-service/Cargo.toml new file mode 100644 index 0000000000..4f657529e5 --- /dev/null +++ b/crates/kevm-proof-service/Cargo.toml @@ -0,0 +1,18 @@ +[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"] } diff --git a/crates/kevm-proof-service/db.yaml b/crates/kevm-proof-service/db.yaml new file mode 100644 index 0000000000..2a19bc12e0 --- /dev/null +++ b/crates/kevm-proof-service/db.yaml @@ -0,0 +1,36 @@ +5577730546396304772: + name: simple1 + complete: true +6899393809540637772: + name: simple10 + complete: true +8550010896920530121: + name: simple2 + complete: true +8815378979428746437: + name: simple6 + complete: true +1316233277346233274: + name: simple4 + complete: true +3765551559799037737: + name: simple3 + complete: true +17173750684762914309: + name: simple5 + complete: true +5801784128720014789: + name: simple9 + complete: true +10197623413532063304: + name: simple8 + complete: false +8128742196276399630: + name: simple8 + complete: false +6899926631315549094: + name: simple8 + complete: true +11277133206842314137: + name: simple10 + complete: false diff --git a/crates/kevm-proof-service/server.state b/crates/kevm-proof-service/server.state new file mode 100644 index 0000000000..ed6e75b5f3 --- /dev/null +++ b/crates/kevm-proof-service/server.state @@ -0,0 +1,19 @@ +SystemTime { tv_sec: 1686952536, tv_nsec: 212990472 } +queue: + +execution pool: + +db: +id: 5577730546396304772 entry: (name: simple1 complete: true) +id: 6899393809540637772 entry: (name: simple10 complete: true) +id: 8550010896920530121 entry: (name: simple2 complete: true) +id: 8815378979428746437 entry: (name: simple6 complete: true) +id: 1316233277346233274 entry: (name: simple4 complete: true) +id: 3765551559799037737 entry: (name: simple3 complete: true) +id: 17173750684762914309 entry: (name: simple5 complete: true) +id: 5801784128720014789 entry: (name: simple9 complete: true) +id: 10197623413532063304 entry: (name: simple8 complete: false) +id: 8128742196276399630 entry: (name: simple8 complete: false) +id: 6899926631315549094 entry: (name: simple8 complete: true) +id: 11277133206842314137 entry: (name: simple10 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..2238bd9906 --- /dev/null +++ b/crates/kevm-proof-service/src/main.rs @@ -0,0 +1,40 @@ +use fe_proof_service::{invariant::Invariant, serde_json, ProofStatus}; +use std::{ + fs, + io::{BufRead, BufReader, BufWriter, Write}, + net::{TcpListener, TcpStream}, + thread, + time::Duration, +}; + +use server_impl::Server; + +mod server_impl; + +fn main() { + let listener = TcpListener::bind("10.0.0.144:7878").unwrap(); + let mut server = Server::new("db.yaml"); + + 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 status = server.check_invariant(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..b2494a85ad --- /dev/null +++ b/crates/kevm-proof-service/src/server_impl/db.rs @@ -0,0 +1,78 @@ +use std::{fmt::Display, fs, io::Write}; + +use indexmap::{indexmap, IndexMap}; +use serde::{Deserialize, Serialize}; +use smol_str::SmolStr; + +#[derive(Serialize, Deserialize)] +pub struct DbEntry { + pub name: SmolStr, + pub complete: 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: {} complete: {}", 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: {} entry: ({})", 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 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..bed1baeb4f --- /dev/null +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -0,0 +1,208 @@ +use std::{ + fmt::Display, + fs, + io::Write, + sync::{Arc, Mutex}, + thread, + time::{self, Duration}, +}; + +use fe_proof_service::{ + invariant::{Invariant, InvariantHeader}, + ProofStatus, +}; +use indexmap::{indexmap, IndexMap}; +use kevm::KSpecExecPool; +use smol_str::SmolStr; + +mod db; +mod queue; + +use self::{db::Db, queue::Spec}; +use self::{db::DbEntry, queue::Queue}; + +pub struct Server { + state: Arc>, +} + +impl Server { + pub fn new(db_path: &str) -> 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 check_invariant(&mut self, invariant: Invariant) -> ProofStatus { + let id = invariant.id(); + let spec = Spec::new_from_invariant(invariant); + self.state.lock().unwrap().add_spec(spec); + self.state.lock().unwrap().update(); + self.state.lock().unwrap().proof_status(id) + } + + // pub fn display(&self, mut writer: W) + // where + // W: Write + Send + 'static, + // { + // let state_clone = Arc::clone(&self.state); + + // thread::spawn(move || loop { + // thread::sleep(Duration::from_millis(1000)); + // let content = format!("{}", state_clone.lock().unwrap()); + // writer.write_all(content.as_bytes()).unwrap() + // }); + // } + + pub fn display(&self) { + let state_clone = Arc::clone(&self.state); + + thread::spawn(move || loop { + thread::sleep(Duration::from_millis(1000)); + let mut file = fs::OpenOptions::new() + .write(true) + .create(true) + .truncate(true) + .open("server.state") + .unwrap(); + let content = format!("{}", state_clone.lock().unwrap()); + file.write_all(content.as_bytes()).unwrap() + }); + } +} + +pub struct ServerState { + queue: Queue, + exec_pool: KSpecExecPool, + db: Db, +} + +impl Display for ServerState { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!(f, "{:?}", time::SystemTime::now())?; + + 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 { + queue: Queue::new(), + exec_pool: KSpecExecPool::new(), + db: Db::new(db_path), + } + } + + pub fn add_spec(&mut self, spec: Spec) { + self.queue.push_spec(spec) + } + + pub fn proof_status(&self, invariant_id: u64) -> ProofStatus { + if let Some(entry) = self.db.get(invariant_id) { + if entry.complete { + ProofStatus::Complete + } else { + ProofStatus::Incomplete + } + } else { + for spec in &self.queue.specs { + if spec.invariant_id == invariant_id { + return spec.status; + } + } + + panic!("missing invariant") + } + } + + 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-proof-service/src/server_impl/queue.rs b/crates/kevm-proof-service/src/server_impl/queue.rs new file mode 100644 index 0000000000..dd77a3908b --- /dev/null +++ b/crates/kevm-proof-service/src/server_impl/queue.rs @@ -0,0 +1,87 @@ +use std::fmt::Display; + +use fe_proof_service::{ + invariant::{Invariant, InvariantBody}, + ProofStatus, +}; +use kevm::{KSpec, KSpecType}; +use smol_str::SmolStr; + +pub struct Spec { + pub name: SmolStr, + pub k_spec: KSpec, + pub invariant_id: u64, + pub status: ProofStatus, +} + +pub fn k_type_from_fe_type(typ: &str) -> KSpecType { + match typ { + "u256" => KSpecType::U256, + "u128" => KSpecType::U128, + "u64" => KSpecType::U64, + "u32" => KSpecType::U32, + "u16" => KSpecType::U16, + "u8" => KSpecType::U8, + "bool" => KSpecType::Bool, + "Context" => KSpecType::Context, + _ => panic!("invalid fe type string: {}", typ), + } +} + +fn k_spec_from_invariant(invariant: Invariant) -> KSpec { + let Invariant { name: _, body } = invariant; + let InvariantBody { args, code } = body; + KSpec::new( + args.iter().map(|typ| k_type_from_fe_type(&typ)).collect(), + code, + ) +} + +impl Spec { + pub fn new_from_invariant(invariant: Invariant) -> Self { + let invariant_id = invariant.id(); + let name = invariant.name.clone(); + let k_spec = k_spec_from_invariant(invariant); + + Self { + name, + k_spec, + invariant_id, + status: ProofStatus::New, + } + } +} + +impl Display for &Spec { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!( + f, + "name: {} id: {} status: {}", + self.name, self.invariant_id, &self.status + ) + } +} + +pub struct Queue { + pub specs: Vec, +} + +impl Display for &Queue { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + for spec in &self.specs { + writeln!(f, "{}", spec)? + } + + Ok(()) + } +} + +impl Queue { + pub fn new() -> Self { + Self { specs: vec![] } + } + + pub fn push_spec(&mut self, spec: Spec) { + self.specs.push(spec) + } +} 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..da8284f9a1 --- /dev/null +++ b/crates/kevm/src/lib.rs @@ -0,0 +1,181 @@ +use std::{ + env, + fmt::Display, + fs, + io::Write, + process::Command, + sync::{Arc, Mutex}, + thread, +}; + +use indexmap::{indexmap, IndexMap}; + +const KSPEC_TEMPLATE: &str = include_str!("../template.k"); + +#[derive(Clone)] +pub enum KSpecType { + U256, + U128, + U64, + U32, + U16, + U8, + Bool, + Context, +} + +impl KSpecType { + pub fn bounds(&self, arg_name: &str) -> String { + match self { + KSpecType::U256 => { + format!("andBool 0 <=Int {arg_name} andBool {arg_name} { + format!("andBool 0 <=Int {arg_name} andBool {arg_name} { + format!("andBool 0 <=Int {arg_name} andBool {arg_name} { + format!("andBool 0 <=Int {arg_name} andBool {arg_name} { + format!("andBool 0 <=Int {arg_name} andBool {arg_name} { + format!("andBool 0 <=Int {arg_name} andBool {arg_name} format!("andBool (0 ==Int {arg_name} orBool {arg_name} ==Int 1)"), + KSpecType::Context => { + format!("andBool 0 ==Int {arg_name}") + } + } + } +} + +#[derive(Clone)] +pub struct KSpec { + args: Vec, + code: String, +} + +impl KSpec { + pub fn new(args: Vec, code: String) -> Self { + Self { args, code } + } + + 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"); + + 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"); + + cmd.arg("build") + .arg("test-prove-fe") + .current_dir(kevm_dir_path) + .env("FS_ID", fs_id) + .status() + .unwrap() + .success() + } +} + +impl Display for KSpec { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let calldata = if self.args.len() != 0 { + (0..self.args.len()) + .map(|n| format!("#buf(32, ARG_{})", n)) + .collect::>() + .join(" +Bytes ") + } else { + "_ => #buf(0, 0)".to_string() + }; + + let requirements = self + .args + .iter() + .enumerate() + .map(|(n, typ)| typ.bounds(&format!("ARG_{}", n))) + .collect::>() + .join("\n"); + + write!( + f, + "{}", + KSPEC_TEMPLATE + .replace("$CODE", &format!("\"0x{}\"", &self.code)) + .replace("$CALLDATA", &calldata) + .replace("$REQUIREMENTS", &requirements) + ) + } +} + +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) { + if self.cur_executing.remove(&id).is_none() { + panic!("no spec to remove") + } + } +} + +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/template.k b/crates/kevm/template.k new file mode 100644 index 0000000000..bd6e1b896d --- /dev/null +++ b/crates/kevm/template.k @@ -0,0 +1,106 @@ +module INVARIANT-SPEC + imports VERIFICATION + + claim + + + #execute => #halt + 1 + NORMAL + ISTANBUL + + + + _ => #buf(0, 0) + _ => EVMC_SUCCESS + _ + _ + _ => ?_ + + + // todo: gen this part + #parseByteStack($CODE) + #computeValidJumpDests(#parseByteStack($CODE)) + + ACCT_ID // contract owner + CALLER_ID // who called this contract; in the beginning, origin // msg.sender + + // todo: gen this part + $CALLDATA + + 0 + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(_VGAS) => ?_ + 0 => ?_ + _ => ?_ + + false // NOTE: non-static call + CALL_DEPTH + + + + _ + _ + _ + _ => ?_ + _ => ?_ + + + _ + ORIGIN_ID + + _ + + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + _ + + + + + _ + + SetItem(ACCT_ID) _:Set + + + + ACCT_ID + _ + #parseByteStack($CODE) + _ + _ + _ + + + + _ + _ + _ + + + + + requires 0 <=Int ACCT_ID andBool ACCT_ID "] +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" } \ No newline at end of file diff --git a/crates/proof-service/src/invariant.rs b/crates/proof-service/src/invariant.rs new file mode 100644 index 0000000000..2e5521d527 --- /dev/null +++ b/crates/proof-service/src/invariant.rs @@ -0,0 +1,46 @@ +use serde::{Deserialize, Serialize}; +use smol_str::SmolStr; +use std::{ + collections::hash_map::DefaultHasher, + hash::{Hash, Hasher}, +}; + +#[derive(Debug, Serialize, Deserialize)] +pub struct Invariant { + pub name: SmolStr, + pub body: InvariantBody, +} + +#[derive(Debug, Serialize, Deserialize)] +pub struct InvariantHeader { + pub name: SmolStr, + pub id: u64, +} + +#[derive(Hash, Debug, Serialize, Deserialize)] +pub struct InvariantBody { + pub args: Vec, + pub code: String, +} + +impl Invariant { + pub fn new(name: SmolStr, args: Vec, code: String) -> Self { + Self { + name, + body: InvariantBody { args, code }, + } + } + + pub fn id(&self) -> u64 { + let mut s = DefaultHasher::new(); + self.body.hash(&mut s); + s.finish() + } + + pub fn header(&self) -> InvariantHeader { + InvariantHeader { + name: self.name.clone(), + id: self.id(), + } + } +} diff --git a/crates/proof-service/src/lib.rs b/crates/proof-service/src/lib.rs new file mode 100644 index 0000000000..4a251e3c93 --- /dev/null +++ b/crates/proof-service/src/lib.rs @@ -0,0 +1,62 @@ +use invariant::{Invariant, InvariantHeader}; +use serde::{Deserialize, Serialize}; +use std::fmt::Display; +use std::io::{BufReader, BufWriter, Read, Write}; +use std::net::{Shutdown, SocketAddr, TcpStream, ToSocketAddrs}; +use std::sync::{Arc, Mutex}; +use std::thread; +use std::time::Duration; + +pub use serde_json; + +pub mod invariant; + +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, "Ready"), + 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 check_invariant(&self, invariant: Invariant) -> 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(&invariant).unwrap(); + writer.write(encoded_invariant.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/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 + #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 Date: Sat, 17 Jun 2023 17:34:15 -0600 Subject: [PATCH 02/10] hacking --- crates/codegen/src/yul/isel/function.rs | 30 +- crates/driver/src/lib.rs | 2 +- crates/kevm/src/lib.rs | 1 + crates/library/std/src/buf.fe | 31 +- .../basic_equivalence.fe | 0 {crates/fe/fixtures => fixtures}/buf.fe | 25 +- {crates/fe/fixtures => fixtures}/sanity.fe | 0 out.yul | 303 ++++++++++++++++++ 8 files changed, 328 insertions(+), 64 deletions(-) rename {crates/fe/fixtures => fixtures}/basic_equivalence.fe (100%) rename {crates/fe/fixtures => fixtures}/buf.fe (83%) rename {crates/fe/fixtures => fixtures}/sanity.fe (100%) create mode 100644 out.yul diff --git a/crates/codegen/src/yul/isel/function.rs b/crates/codegen/src/yul/isel/function.rs index ad576c1f41..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])}, diff --git a/crates/driver/src/lib.rs b/crates/driver/src/lib.rs index 373af4a760..b0dc086b87 100644 --- a/crates/driver/src/lib.rs +++ b/crates/driver/src/lib.rs @@ -214,7 +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('"', "\\\""); - // panic!("{}", yul_test); + println!("{}", yul_test); let bytecode = compile_to_evm("test", &yul_test, optimize); CompiledTest::new(test.name(db), bytecode) } diff --git a/crates/kevm/src/lib.rs b/crates/kevm/src/lib.rs index da8284f9a1..b656dcde51 100644 --- a/crates/kevm/src/lib.rs +++ b/crates/kevm/src/lib.rs @@ -85,6 +85,7 @@ impl KSpec { cmd.arg("build") .arg("test-prove-fe") + .arg("-j8") .current_dir(kevm_dir_path) .env("FS_ID", fs_id) .status() 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/fe/fixtures/basic_equivalence.fe b/fixtures/basic_equivalence.fe similarity index 100% rename from crates/fe/fixtures/basic_equivalence.fe rename to fixtures/basic_equivalence.fe diff --git a/crates/fe/fixtures/buf.fe b/fixtures/buf.fe similarity index 83% rename from crates/fe/fixtures/buf.fe rename to fixtures/buf.fe index e8517de33a..8e316ca8a5 100644 --- a/crates/fe/fixtures/buf.fe +++ b/fixtures/buf.fe @@ -7,8 +7,8 @@ fn rw_u8(a: u8, b: u8) { let mut reader: MemoryBufferReader = buf.reader() let mut writer: MemoryBufferWriter = buf.writer() - writer.write_u8(value: a) - writer.write_u8(value: b) + writer.write(value: a) + writer.write(value: b) spec::assert_eq(reader.read_u8(), a) spec::assert_eq(reader.read_u8(), b) @@ -20,7 +20,7 @@ fn rw_single_u8(a: u8) { let mut reader: MemoryBufferReader = buf.reader() let mut writer: MemoryBufferWriter = buf.writer() - writer.write_u8(value: a) + writer.write(value: a) spec::assert_eq(reader.read_u8(), a) } @@ -30,7 +30,7 @@ fn rw_single_u16(a: u16) { let mut reader: MemoryBufferReader = buf.reader() let mut writer: MemoryBufferWriter = buf.writer() - writer.write_u16(value: a) + writer.write(value: a) spec::assert_eq(reader.read_u16(), a) } @@ -40,22 +40,21 @@ fn rw_u16(a: u16, b: u16) { let mut reader: MemoryBufferReader = buf.reader() let mut writer: MemoryBufferWriter = buf.writer() - writer.write_u16(value: a) - writer.write_u16(value: b) + writer.write(value: a) + writer.write(value: b) spec::assert_eq(reader.read_u16(), a) spec::assert_eq(reader.read_u16(), b) } - #invariant fn rw_u256(a: u256, b: u256) { let mut buf: MemoryBuffer = MemoryBuffer::new(len: 64) let mut reader: MemoryBufferReader = buf.reader() let mut writer: MemoryBufferWriter = buf.writer() - writer.write_u256(value: a) - writer.write_u256(value: b) + writer.write(value: a) + writer.write(value: b) spec::assert_eq(reader.read_u256(), a) spec::assert_eq(reader.read_u256(), b) @@ -67,10 +66,10 @@ fn rw_mix(a: u256, b: u8, c: u128, d: u128) { let mut reader: MemoryBufferReader = buf.reader() let mut writer: MemoryBufferWriter = buf.writer() - writer.write_u256(value: a) - writer.write_u8(value: b) - writer.write_u128(value: c) - writer.write_u128(value: d) + writer.write(value: a) + writer.write(value: b) + writer.write(value: c) + writer.write(value: d) spec::assert_eq(reader.read_u256(), a) spec::assert_eq(reader.read_u8(), b) diff --git a/crates/fe/fixtures/sanity.fe b/fixtures/sanity.fe similarity index 100% rename from crates/fe/fixtures/sanity.fe rename to fixtures/sanity.fe 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() + } +} From e61d5ca66e57fa0e432f22ff5e8782caef03f2a0 Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Mon, 19 Jun 2023 22:34:04 -0600 Subject: [PATCH 03/10] hacking --- crates/codegen/src/yul/isel/test.rs | 4 ++- crates/kevm-proof-service/db.yaml | 38 +++----------------------- crates/kevm-proof-service/server.state | 16 ++--------- crates/kevm-proof-service/src/main.rs | 7 ++--- crates/kevm/src/lib.rs | 14 ++++++++-- fixtures/calldata.fe | 11 ++++++++ 6 files changed, 34 insertions(+), 56 deletions(-) create mode 100644 fixtures/calldata.fe diff --git a/crates/codegen/src/yul/isel/test.rs b/crates/codegen/src/yul/isel/test.rs index b94473696a..b9c54ef096 100644 --- a/crates/codegen/src/yul/isel/test.rs +++ b/crates/codegen/src/yul/isel/test.rs @@ -22,6 +22,7 @@ pub fn lower_test(db: &dyn CodegenDb, test: FunctionId) -> yul::Object { .map(yul::Statement::FunctionDefinition) .collect(); let test_func_name = identifier! { (db.codegen_function_symbol_name(test)) }; + let mut call_arg_offset = 0; let call_args = test .signature(db.upcast()) .params @@ -31,7 +32,8 @@ pub fn lower_test(db: &dyn CodegenDb, test: FunctionId) -> yul::Object { if param.name == "ctx" { None } else { - let value = literal_expression! { (n * 32) }; + let value = literal_expression! { (call_arg_offset) }; + call_arg_offset += 32; Some(expression! { calldataload([value]) }) } }) diff --git a/crates/kevm-proof-service/db.yaml b/crates/kevm-proof-service/db.yaml index 2a19bc12e0..be6179e262 100644 --- a/crates/kevm-proof-service/db.yaml +++ b/crates/kevm-proof-service/db.yaml @@ -1,36 +1,6 @@ -5577730546396304772: - name: simple1 - complete: true -6899393809540637772: - name: simple10 - complete: true -8550010896920530121: - name: simple2 - complete: true -8815378979428746437: - name: simple6 - complete: true -1316233277346233274: - name: simple4 - complete: true -3765551559799037737: - name: simple3 - complete: true -17173750684762914309: - name: simple5 - complete: true -5801784128720014789: - name: simple9 - complete: true -10197623413532063304: - name: simple8 +7408176950684564775: + name: msg_sig complete: false -8128742196276399630: - name: simple8 - complete: false -6899926631315549094: - name: simple8 - complete: true -11277133206842314137: - name: simple10 +16564614996415688757: + name: msg_sig complete: false diff --git a/crates/kevm-proof-service/server.state b/crates/kevm-proof-service/server.state index ed6e75b5f3..fbba1257dd 100644 --- a/crates/kevm-proof-service/server.state +++ b/crates/kevm-proof-service/server.state @@ -1,19 +1,9 @@ -SystemTime { tv_sec: 1686952536, tv_nsec: 212990472 } +SystemTime { tv_sec: 1687206428, tv_nsec: 731526170 } queue: execution pool: db: -id: 5577730546396304772 entry: (name: simple1 complete: true) -id: 6899393809540637772 entry: (name: simple10 complete: true) -id: 8550010896920530121 entry: (name: simple2 complete: true) -id: 8815378979428746437 entry: (name: simple6 complete: true) -id: 1316233277346233274 entry: (name: simple4 complete: true) -id: 3765551559799037737 entry: (name: simple3 complete: true) -id: 17173750684762914309 entry: (name: simple5 complete: true) -id: 5801784128720014789 entry: (name: simple9 complete: true) -id: 10197623413532063304 entry: (name: simple8 complete: false) -id: 8128742196276399630 entry: (name: simple8 complete: false) -id: 6899926631315549094 entry: (name: simple8 complete: true) -id: 11277133206842314137 entry: (name: simple10 complete: false) +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 index 2238bd9906..57474ececf 100644 --- a/crates/kevm-proof-service/src/main.rs +++ b/crates/kevm-proof-service/src/main.rs @@ -1,10 +1,7 @@ -use fe_proof_service::{invariant::Invariant, serde_json, ProofStatus}; +use fe_proof_service::{invariant::Invariant, serde_json}; use std::{ - fs, - io::{BufRead, BufReader, BufWriter, Write}, + io::{BufRead, BufReader, BufWriter}, net::{TcpListener, TcpStream}, - thread, - time::Duration, }; use server_impl::Server; diff --git a/crates/kevm/src/lib.rs b/crates/kevm/src/lib.rs index b656dcde51..fe55c56c39 100644 --- a/crates/kevm/src/lib.rs +++ b/crates/kevm/src/lib.rs @@ -12,7 +12,7 @@ use indexmap::{indexmap, IndexMap}; const KSPEC_TEMPLATE: &str = include_str!("../template.k"); -#[derive(Clone)] +#[derive(Clone, Copy, PartialEq, Eq)] pub enum KSpecType { U256, U128, @@ -97,8 +97,16 @@ impl KSpec { impl Display for KSpec { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let calldata = if self.args.len() != 0 { - (0..self.args.len()) - .map(|n| format!("#buf(32, ARG_{})", n)) + self.args + .iter() + .enumerate() + .map(|(n, typ)| { + if *typ == KSpecType::Context { + format!("#buf(0, ARG_{})", n) + } else { + format!("#buf(32, ARG_{})", n) + } + }) .collect::>() .join(" +Bytes ") } else { diff --git a/fixtures/calldata.fe b/fixtures/calldata.fe new file mode 100644 index 0000000000..b881faa79d --- /dev/null +++ b/fixtures/calldata.fe @@ -0,0 +1,11 @@ +use std::spec + +#invariant +fn msg_sig(ctx: Context, a: u256) { + spec::given_eq( + a, + 0x1000000100000000000000000000000000000000000000000000000000000000 + ) + + spec::assert_eq(ctx.msg_sig(), 0x10000001) +} \ No newline at end of file From 08fa80085d9957932e84a20e0b2a715972ceed07 Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Wed, 21 Jun 2023 14:57:13 -0600 Subject: [PATCH 04/10] hacking --- crates/codegen/src/yul/isel/test.rs | 48 ++++++++++++------- crates/fe/src/task/prove.rs | 2 +- crates/kevm-proof-service/src/main.rs | 2 +- .../kevm-proof-service/src/server_impl/mod.rs | 6 +-- crates/kevm/src/lib.rs | 46 ++++++++---------- crates/kevm/template.k | 6 +-- crates/proof-service/src/lib.rs | 9 ++-- db.yaml | 48 +++++++++++++++++++ fixtures/calldata.fe | 5 +- fixtures/contracts.fe | 12 +++++ server.state | 35 ++++++++++++++ 11 files changed, 156 insertions(+), 63 deletions(-) create mode 100644 db.yaml create mode 100644 fixtures/contracts.fe create mode 100644 server.state diff --git a/crates/codegen/src/yul/isel/test.rs b/crates/codegen/src/yul/isel/test.rs index b9c54ef096..71013957fd 100644 --- a/crates/codegen/src/yul/isel/test.rs +++ b/crates/codegen/src/yul/isel/test.rs @@ -21,29 +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 mut call_arg_offset = 0; - let call_args = test - .signature(db.upcast()) - .params - .iter() - .enumerate() - .filter_map(|(n, param)| { - if param.name == "ctx" { - None - } else { - let value = literal_expression! { (call_arg_offset) }; - call_arg_offset += 32; - Some(expression! { calldataload([value]) }) + 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 } - }) - .collect::>(); - let call = function_call_statement! {[test_func_name]([call_args...])}; + } + + 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/fe/src/task/prove.rs b/crates/fe/src/task/prove.rs index 97ab73d67a..317636217a 100644 --- a/crates/fe/src/task/prove.rs +++ b/crates/fe/src/task/prove.rs @@ -40,7 +40,7 @@ fn single_file_invariants(prove_arg: &ProveArgs) -> Vec { pub fn prove(prove_arg: ProveArgs) { let invariants = single_file_invariants(&prove_arg); - let server = ProofClient::new("10.0.0.144:7878"); + let server = ProofClient::new("127.0.0.1:7878"); for invariant in invariants { let name = invariant.name.clone(); diff --git a/crates/kevm-proof-service/src/main.rs b/crates/kevm-proof-service/src/main.rs index 57474ececf..9ee27b30ff 100644 --- a/crates/kevm-proof-service/src/main.rs +++ b/crates/kevm-proof-service/src/main.rs @@ -9,7 +9,7 @@ use server_impl::Server; mod server_impl; fn main() { - let listener = TcpListener::bind("10.0.0.144:7878").unwrap(); + let listener = TcpListener::bind("127.0.0.1:7878").unwrap(); let mut server = Server::new("db.yaml"); server.display(); diff --git a/crates/kevm-proof-service/src/server_impl/mod.rs b/crates/kevm-proof-service/src/server_impl/mod.rs index bed1baeb4f..bc8d977212 100644 --- a/crates/kevm-proof-service/src/server_impl/mod.rs +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -7,10 +7,7 @@ use std::{ time::{self, Duration}, }; -use fe_proof_service::{ - invariant::{Invariant, InvariantHeader}, - ProofStatus, -}; +use fe_proof_service::{invariant::Invariant, ProofStatus}; use indexmap::{indexmap, IndexMap}; use kevm::KSpecExecPool; use smol_str::SmolStr; @@ -44,6 +41,7 @@ impl Server { pub fn check_invariant(&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) diff --git a/crates/kevm/src/lib.rs b/crates/kevm/src/lib.rs index fe55c56c39..c7f748eadb 100644 --- a/crates/kevm/src/lib.rs +++ b/crates/kevm/src/lib.rs @@ -46,9 +46,7 @@ impl KSpecType { format!("andBool 0 <=Int {arg_name} andBool {arg_name} format!("andBool (0 ==Int {arg_name} orBool {arg_name} ==Int 1)"), - KSpecType::Context => { - format!("andBool 0 ==Int {arg_name}") - } + KSpecType::Context => panic!("no bounds for ctx"), } } } @@ -96,38 +94,32 @@ impl KSpec { impl Display for KSpec { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let calldata = if self.args.len() != 0 { - self.args - .iter() - .enumerate() - .map(|(n, typ)| { - if *typ == KSpecType::Context { - format!("#buf(0, ARG_{})", n) - } else { - format!("#buf(32, ARG_{})", n) - } - }) - .collect::>() - .join(" +Bytes ") + let mut mem_args = vec![]; + let mut requirements = vec![]; + let mut arg_num = 0; + + for arg in &self.args { + if *arg != KSpecType::Context { + let arg_name = format!("ARG_{}", arg_num); + requirements.push(arg.bounds(&arg_name)); + mem_args.push(format!("#buf(32, {})", arg_name)); + arg_num += 1; + } + } + + let mem_args = if mem_args.is_empty() { + "_".to_string() } else { - "_ => #buf(0, 0)".to_string() + mem_args.join(" +Bytes ") }; - let requirements = self - .args - .iter() - .enumerate() - .map(|(n, typ)| typ.bounds(&format!("ARG_{}", n))) - .collect::>() - .join("\n"); - write!( f, "{}", KSPEC_TEMPLATE .replace("$CODE", &format!("\"0x{}\"", &self.code)) - .replace("$CALLDATA", &calldata) - .replace("$REQUIREMENTS", &requirements) + .replace("$MEM_ARGS", &mem_args) + .replace("$REQUIREMENTS", &requirements.join("\n")) ) } } diff --git a/crates/kevm/template.k b/crates/kevm/template.k index bd6e1b896d..372933c883 100644 --- a/crates/kevm/template.k +++ b/crates/kevm/template.k @@ -18,19 +18,17 @@ module INVARIANT-SPEC _ => ?_ - // todo: gen this part #parseByteStack($CODE) #computeValidJumpDests(#parseByteStack($CODE)) ACCT_ID // contract owner CALLER_ID // who called this contract; in the beginning, origin // msg.sender - // todo: gen this part - $CALLDATA + _ 0 .WordStack => ?_ - .Bytes => ?_ + $MEM_ARGS 0 => ?_ #gas(_VGAS) => ?_ 0 => ?_ diff --git a/crates/proof-service/src/lib.rs b/crates/proof-service/src/lib.rs index 4a251e3c93..0697f028ff 100644 --- a/crates/proof-service/src/lib.rs +++ b/crates/proof-service/src/lib.rs @@ -1,11 +1,8 @@ -use invariant::{Invariant, InvariantHeader}; +use invariant::Invariant; use serde::{Deserialize, Serialize}; use std::fmt::Display; -use std::io::{BufReader, BufWriter, Read, Write}; -use std::net::{Shutdown, SocketAddr, TcpStream, ToSocketAddrs}; -use std::sync::{Arc, Mutex}; -use std::thread; -use std::time::Duration; +use std::io::{BufReader, BufWriter, Write}; +use std::net::{SocketAddr, TcpStream, ToSocketAddrs}; pub use serde_json; diff --git a/db.yaml b/db.yaml new file mode 100644 index 0000000000..4d6d5252bd --- /dev/null +++ b/db.yaml @@ -0,0 +1,48 @@ +6899393809540637772: + name: simple10 + complete: true +10648093925226451130: + name: simple1 + complete: true +9866189969293882850: + name: simple2 + complete: true +1491244125428245047: + name: simple6 + complete: true +17014316732147409137: + name: simple4 + complete: true +16497824417235581307: + name: simple3 + complete: true +14785961722918986698: + name: simple5 + complete: true +6672846181222220742: + name: simple9 + complete: true +2691375950895637890: + name: simple8 + complete: true +10351748462964682631: + name: simple6 + complete: false +13725409941853743582: + name: simple4 + complete: false +4205870993505503282: + name: read_byte_shl_248 + complete: true +17646573292089816401: + name: shl_shr_248 + complete: true +13658001998889555973: + name: shl_shr_n + complete: false +6342915096082124860: + name: de_morgan_true + complete: true +11455748359517230147: + name: de_morgan_false + complete: true diff --git a/fixtures/calldata.fe b/fixtures/calldata.fe index b881faa79d..9837faaeb6 100644 --- a/fixtures/calldata.fe +++ b/fixtures/calldata.fe @@ -1,9 +1,10 @@ use std::spec +use std::evm #invariant -fn msg_sig(ctx: Context, a: u256) { +unsafe fn msg_sig(ctx: Context) { spec::given_eq( - a, + evm::call_data_load(offset: 0), 0x1000000100000000000000000000000000000000000000000000000000000000 ) diff --git a/fixtures/contracts.fe b/fixtures/contracts.fe new file mode 100644 index 0000000000..ddea169b82 --- /dev/null +++ b/fixtures/contracts.fe @@ -0,0 +1,12 @@ +use std::spec + +contract Foo { + pub fn get_42(self) -> u256 { + return 42 + } +} + +#invariant +fn verify_get_42(ctx: Context, foo: Foo) { + spec::assert_eq(foo.get_42(), 42) +} \ No newline at end of file diff --git a/server.state b/server.state new file mode 100644 index 0000000000..683da5e13b --- /dev/null +++ b/server.state @@ -0,0 +1,35 @@ +SystemTime { tv_sec: 1687381029, tv_nsec: 882535660 } +queue: +name: rw_u8 id: 6399727362632061175 status: Proving +name: rw_single_u8 id: 17817826477954645223 status: Proving +name: rw_single_u16 id: 9719998087209853623 status: Proving +name: rw_u16 id: 11674158764454988378 status: Proving +name: rw_u256 id: 1012056005684586410 status: Proving +name: rw_mix id: 5152237306397595861 status: Proving + +execution pool: +6399727362632061175 +17817826477954645223 +9719998087209853623 +11674158764454988378 +1012056005684586410 +5152237306397595861 + +db: +id: 6899393809540637772 entry: (name: simple10 complete: true) +id: 10648093925226451130 entry: (name: simple1 complete: true) +id: 9866189969293882850 entry: (name: simple2 complete: true) +id: 1491244125428245047 entry: (name: simple6 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: 10351748462964682631 entry: (name: simple6 complete: false) +id: 13725409941853743582 entry: (name: simple4 complete: false) +id: 4205870993505503282 entry: (name: read_byte_shl_248 complete: true) +id: 17646573292089816401 entry: (name: shl_shr_248 complete: true) +id: 13658001998889555973 entry: (name: shl_shr_n complete: false) +id: 6342915096082124860 entry: (name: de_morgan_true complete: true) +id: 11455748359517230147 entry: (name: de_morgan_false complete: true) + From d91b25f4e2013806d1487b665acca054b67e9aaf Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Thu, 22 Jun 2023 11:33:31 -0600 Subject: [PATCH 05/10] hacking --- crates/driver/src/lib.rs | 2 +- .../kevm-proof-service/src/server_impl/mod.rs | 2 +- db.yaml | 24 +++++++------------ fixtures/contracts.fe | 4 ++-- server.state | 22 ++++------------- 5 files changed, 17 insertions(+), 37 deletions(-) diff --git a/crates/driver/src/lib.rs b/crates/driver/src/lib.rs index b0dc086b87..9d04b46b9c 100644 --- a/crates/driver/src/lib.rs +++ b/crates/driver/src/lib.rs @@ -214,7 +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); + // println!("{}", yul_test); let bytecode = compile_to_evm("test", &yul_test, optimize); CompiledTest::new(test.name(db), bytecode) } diff --git a/crates/kevm-proof-service/src/server_impl/mod.rs b/crates/kevm-proof-service/src/server_impl/mod.rs index bc8d977212..d0ca861367 100644 --- a/crates/kevm-proof-service/src/server_impl/mod.rs +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -41,7 +41,7 @@ impl Server { pub fn check_invariant(&mut self, invariant: Invariant) -> ProofStatus { let id = invariant.id(); let spec = Spec::new_from_invariant(invariant); - println!("{}", &spec.k_spec); + // println!("{}", &spec.k_spec); self.state.lock().unwrap().add_spec(spec); self.state.lock().unwrap().update(); self.state.lock().unwrap().proof_status(id) diff --git a/db.yaml b/db.yaml index 4d6d5252bd..7cd96721d9 100644 --- a/db.yaml +++ b/db.yaml @@ -1,15 +1,12 @@ +9866189969293882850: + name: simple2 + complete: true 6899393809540637772: name: simple10 complete: true 10648093925226451130: name: simple1 complete: true -9866189969293882850: - name: simple2 - complete: true -1491244125428245047: - name: simple6 - complete: true 17014316732147409137: name: simple4 complete: true @@ -25,24 +22,21 @@ 2691375950895637890: name: simple8 complete: true -10351748462964682631: - name: simple6 - complete: false -13725409941853743582: - name: simple4 - complete: false 4205870993505503282: name: read_byte_shl_248 complete: true 17646573292089816401: name: shl_shr_248 complete: true -13658001998889555973: - name: shl_shr_n - complete: false +1491244125428245047: + name: simple6 + complete: true 6342915096082124860: name: de_morgan_true complete: true 11455748359517230147: name: de_morgan_false complete: true +13658001998889555973: + name: shl_shr_n + complete: false diff --git a/fixtures/contracts.fe b/fixtures/contracts.fe index ddea169b82..3fedb01bb5 100644 --- a/fixtures/contracts.fe +++ b/fixtures/contracts.fe @@ -7,6 +7,6 @@ contract Foo { } #invariant -fn verify_get_42(ctx: Context, foo: Foo) { +fn verify_get_42(foo: Foo) { spec::assert_eq(foo.get_42(), 42) -} \ No newline at end of file +} diff --git a/server.state b/server.state index 683da5e13b..c2c24f3f61 100644 --- a/server.state +++ b/server.state @@ -1,35 +1,21 @@ -SystemTime { tv_sec: 1687381029, tv_nsec: 882535660 } +SystemTime { tv_sec: 1687455190, tv_nsec: 773921859 } queue: -name: rw_u8 id: 6399727362632061175 status: Proving -name: rw_single_u8 id: 17817826477954645223 status: Proving -name: rw_single_u16 id: 9719998087209853623 status: Proving -name: rw_u16 id: 11674158764454988378 status: Proving -name: rw_u256 id: 1012056005684586410 status: Proving -name: rw_mix id: 5152237306397595861 status: Proving execution pool: -6399727362632061175 -17817826477954645223 -9719998087209853623 -11674158764454988378 -1012056005684586410 -5152237306397595861 db: +id: 9866189969293882850 entry: (name: simple2 complete: true) id: 6899393809540637772 entry: (name: simple10 complete: true) id: 10648093925226451130 entry: (name: simple1 complete: true) -id: 9866189969293882850 entry: (name: simple2 complete: true) -id: 1491244125428245047 entry: (name: simple6 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: 10351748462964682631 entry: (name: simple6 complete: false) -id: 13725409941853743582 entry: (name: simple4 complete: false) id: 4205870993505503282 entry: (name: read_byte_shl_248 complete: true) id: 17646573292089816401 entry: (name: shl_shr_248 complete: true) -id: 13658001998889555973 entry: (name: shl_shr_n complete: false) +id: 1491244125428245047 entry: (name: simple6 complete: true) id: 6342915096082124860 entry: (name: de_morgan_true complete: true) id: 11455748359517230147 entry: (name: de_morgan_false complete: true) +id: 13658001998889555973 entry: (name: shl_shr_n complete: false) From 19f99ad2870e3813d638b7e2dd9ccd151e4c058f Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Mon, 10 Jul 2023 13:11:56 -0600 Subject: [PATCH 06/10] hacking --- crates/kevm-proof-service/src/server_impl/queue.rs | 1 + db.yaml | 10 +++++----- fixtures/contracts.fe | 4 +++- server.state | 6 +++--- 4 files changed, 12 insertions(+), 9 deletions(-) diff --git a/crates/kevm-proof-service/src/server_impl/queue.rs b/crates/kevm-proof-service/src/server_impl/queue.rs index dd77a3908b..0f032956fc 100644 --- a/crates/kevm-proof-service/src/server_impl/queue.rs +++ b/crates/kevm-proof-service/src/server_impl/queue.rs @@ -24,6 +24,7 @@ pub fn k_type_from_fe_type(typ: &str) -> KSpecType { "u8" => KSpecType::U8, "bool" => KSpecType::Bool, "Context" => KSpecType::Context, + "mut Context" => KSpecType::Context, _ => panic!("invalid fe type string: {}", typ), } } diff --git a/db.yaml b/db.yaml index 7cd96721d9..e579cad068 100644 --- a/db.yaml +++ b/db.yaml @@ -34,9 +34,9 @@ 6342915096082124860: name: de_morgan_true complete: true -11455748359517230147: - name: de_morgan_false - complete: true -13658001998889555973: - name: shl_shr_n +14977842676755773493: + name: verify_get_42 + complete: false +14111824353587072050: + name: verify_get_42 complete: false diff --git a/fixtures/contracts.fe b/fixtures/contracts.fe index 3fedb01bb5..3d4f2741d1 100644 --- a/fixtures/contracts.fe +++ b/fixtures/contracts.fe @@ -7,6 +7,8 @@ contract Foo { } #invariant -fn verify_get_42(foo: Foo) { +fn verify_get_42(mut ctx: Context) { + let foo: Foo = Foo.create(ctx, 0) + spec::given_eq(u256(address(foo)), 26) spec::assert_eq(foo.get_42(), 42) } diff --git a/server.state b/server.state index c2c24f3f61..cde123c955 100644 --- a/server.state +++ b/server.state @@ -1,4 +1,4 @@ -SystemTime { tv_sec: 1687455190, tv_nsec: 773921859 } +SystemTime { tv_sec: 1688767084, tv_nsec: 496605980 } queue: execution pool: @@ -16,6 +16,6 @@ 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: 11455748359517230147 entry: (name: de_morgan_false complete: true) -id: 13658001998889555973 entry: (name: shl_shr_n complete: false) +id: 14977842676755773493 entry: (name: verify_get_42 complete: false) +id: 14111824353587072050 entry: (name: verify_get_42 complete: false) From 1e6a7b328c2698056e6f87102050ee06bc7f3a47 Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Fri, 14 Jul 2023 08:49:56 -0600 Subject: [PATCH 07/10] hacking --- Cargo.lock | 175 +++++++++++++++++- crates/fe/src/task/prove.rs | 31 +++- crates/kevm-proof-service/Cargo.toml | 2 + crates/kevm-proof-service/db.yaml | 15 ++ crates/kevm-proof-service/server.state | 6 +- crates/kevm-proof-service/src/main.rs | 31 +++- .../kevm-proof-service/src/server_impl/db.rs | 4 + .../kevm-proof-service/src/server_impl/mod.rs | 43 ++--- .../src/server_impl/queue.rs | 4 + crates/kevm/src/lib.rs | 10 +- crates/proof-service/src/lib.rs | 7 +- db.yaml | 24 ++- fixtures/contracts.fe | 17 +- 13 files changed, 309 insertions(+), 60 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index f6ba808d11..1d441a584c 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" @@ -690,7 +715,7 @@ dependencies = [ "insta", "num-bigint", "num-traits", - "parking_lot_core", + "parking_lot_core 0.8.0", "petgraph", "pretty_assertions", "rstest", @@ -1251,6 +1276,8 @@ dependencies = [ name = "kevm-proof-service" version = "0.23.0" dependencies = [ + "clap 3.2.23", + "crossterm", "fe-proof-service", "indexmap", "kevm", @@ -1343,6 +1370,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" @@ -1491,7 +1530,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]] @@ -1504,11 +1553,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" @@ -1728,6 +1790,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" @@ -1943,7 +2014,7 @@ dependencies = [ "lock_api", "log", "oorandom", - "parking_lot", + "parking_lot 0.11.1", "rustc-hash", "salsa-macros", "smallvec", @@ -2142,6 +2213,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" @@ -2583,6 +2684,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/crates/fe/src/task/prove.rs b/crates/fe/src/task/prove.rs index 317636217a..4ec743c7e8 100644 --- a/crates/fe/src/task/prove.rs +++ b/crates/fe/src/task/prove.rs @@ -11,14 +11,16 @@ use fe_proof_service::ProofClient; #[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(prove_arg: &ProveArgs) -> Vec { - let input_path = &prove_arg.input_path; - let optimize = prove_arg.optimize.unwrap_or(true); - +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) => { @@ -38,13 +40,24 @@ fn single_file_invariants(prove_arg: &ProveArgs) -> Vec { } } -pub fn prove(prove_arg: ProveArgs) { - let invariants = single_file_invariants(&prove_arg); - let server = ProofClient::new("127.0.0.1:7878"); +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(); - let status = server.check_invariant(invariant); - println!("{} (status: {})", &name, &status) + + if let Some(match_name) = &args.name { + if name.contains(match_name) { + let status = server.check_invariant(invariant, rerun); + println!("{} (status: {})", &name, &status) + } + } else { + let status = server.check_invariant(invariant, rerun); + println!("{} (status: {})", &name, &status) + } } } diff --git a/crates/kevm-proof-service/Cargo.toml b/crates/kevm-proof-service/Cargo.toml index 4f657529e5..2da4f33129 100644 --- a/crates/kevm-proof-service/Cargo.toml +++ b/crates/kevm-proof-service/Cargo.toml @@ -16,3 +16,5 @@ 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 index be6179e262..f39c449d98 100644 --- a/crates/kevm-proof-service/db.yaml +++ b/crates/kevm-proof-service/db.yaml @@ -4,3 +4,18 @@ 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 index fbba1257dd..5adea41603 100644 --- a/crates/kevm-proof-service/server.state +++ b/crates/kevm-proof-service/server.state @@ -1,7 +1,11 @@ -SystemTime { tv_sec: 1687206428, tv_nsec: 731526170 } +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) diff --git a/crates/kevm-proof-service/src/main.rs b/crates/kevm-proof-service/src/main.rs index 9ee27b30ff..0dd5769287 100644 --- a/crates/kevm-proof-service/src/main.rs +++ b/crates/kevm-proof-service/src/main.rs @@ -8,11 +8,26 @@ 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(long, action)] + display: bool, +} + fn main() { - let listener = TcpListener::bind("127.0.0.1:7878").unwrap(); + let args = Args::parse(); + + let listener = TcpListener::bind(args.bind_addrs).unwrap(); let mut server = Server::new("db.yaml"); - server.display(); + if args.display { + server.display(); + } for stream in listener.incoming() { let stream = stream.unwrap(); @@ -32,6 +47,16 @@ fn connection_handler(server: &mut Server, mut stream: TcpStream) { serde_json::from_str(&invariant_encoded).expect("unable to decode invariant") }; - let status = server.check_invariant(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 index b2494a85ad..9294b68d04 100644 --- a/crates/kevm-proof-service/src/server_impl/db.rs +++ b/crates/kevm-proof-service/src/server_impl/db.rs @@ -72,6 +72,10 @@ impl Db { 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 index d0ca861367..4e3c689b83 100644 --- a/crates/kevm-proof-service/src/server_impl/mod.rs +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -1,12 +1,16 @@ use std::{ fmt::Display, - fs, - io::Write, + io::{self}, sync::{Arc, Mutex}, thread, time::{self, Duration}, }; +use crossterm::{ + cursor::MoveTo, + execute, + terminal::{Clear, ClearType}, +}; use fe_proof_service::{invariant::Invariant, ProofStatus}; use indexmap::{indexmap, IndexMap}; use kevm::KSpecExecPool; @@ -38,7 +42,13 @@ impl Server { Self { state } } - pub fn check_invariant(&mut self, invariant: Invariant) -> ProofStatus { + 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); @@ -47,32 +57,19 @@ impl Server { self.state.lock().unwrap().proof_status(id) } - // pub fn display(&self, mut writer: W) - // where - // W: Write + Send + 'static, - // { - // let state_clone = Arc::clone(&self.state); - - // thread::spawn(move || loop { - // thread::sleep(Duration::from_millis(1000)); - // let content = format!("{}", state_clone.lock().unwrap()); - // writer.write_all(content.as_bytes()).unwrap() - // }); - // } - pub fn display(&self) { let state_clone = Arc::clone(&self.state); thread::spawn(move || loop { thread::sleep(Duration::from_millis(1000)); - let mut file = fs::OpenOptions::new() - .write(true) - .create(true) - .truncate(true) - .open("server.state") - .unwrap(); + + let mut stdout = io::stdout(); + execute!(stdout, Clear(ClearType::All)).unwrap(); + let content = format!("{}", state_clone.lock().unwrap()); - file.write_all(content.as_bytes()).unwrap() + print!("{content}"); + + execute!(stdout, MoveTo(0, 0)).unwrap(); }); } } diff --git a/crates/kevm-proof-service/src/server_impl/queue.rs b/crates/kevm-proof-service/src/server_impl/queue.rs index 0f032956fc..6af07ce7ef 100644 --- a/crates/kevm-proof-service/src/server_impl/queue.rs +++ b/crates/kevm-proof-service/src/server_impl/queue.rs @@ -85,4 +85,8 @@ impl Queue { pub fn push_spec(&mut self, spec: Spec) { self.specs.push(spec) } + + pub fn remove(&mut self, id: u64) { + self.specs.retain(|spec| spec.invariant_id != id); + } } diff --git a/crates/kevm/src/lib.rs b/crates/kevm/src/lib.rs index c7f748eadb..952c7e6f2c 100644 --- a/crates/kevm/src/lib.rs +++ b/crates/kevm/src/lib.rs @@ -1,7 +1,7 @@ use std::{ env, fmt::Display, - fs, + fs::{self, File}, io::Write, process::Command, sync::{Arc, Mutex}, @@ -66,6 +66,7 @@ impl KSpec { 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(); @@ -80,12 +81,14 @@ impl KSpec { 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() @@ -159,9 +162,8 @@ impl KSpecExecPool { } pub fn remove(&mut self, id: u64) { - if self.cur_executing.remove(&id).is_none() { - panic!("no spec to remove") - } + // todo: actually terminate the process isntead of just forgetting about it + self.cur_executing.remove(&id); } } diff --git a/crates/proof-service/src/lib.rs b/crates/proof-service/src/lib.rs index 0697f028ff..e3c8a8acf2 100644 --- a/crates/proof-service/src/lib.rs +++ b/crates/proof-service/src/lib.rs @@ -41,7 +41,7 @@ impl ProofClient { } impl ProofClient { - pub fn check_invariant(&self, invariant: Invariant) -> ProofStatus { + pub fn check_invariant(&self, invariant: Invariant, rerun: bool) -> ProofStatus { let mut stream = TcpStream::connect(self.0).expect("connection failed"); let mut stream_clone = stream.try_clone().unwrap(); @@ -53,6 +53,11 @@ impl ProofClient { 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/db.yaml b/db.yaml index e579cad068..caea399894 100644 --- a/db.yaml +++ b/db.yaml @@ -22,21 +22,27 @@ 2691375950895637890: name: simple8 complete: true +14111824353587072050: + name: verify_get_42 + complete: false +14977842676755773493: + name: verify_get_42 + complete: false +1491244125428245047: + name: simple6 + complete: true 4205870993505503282: name: read_byte_shl_248 complete: true 17646573292089816401: name: shl_shr_248 complete: true -1491244125428245047: - name: simple6 - complete: true +13658001998889555973: + name: shl_shr_n + complete: false 6342915096082124860: name: de_morgan_true complete: true -14977842676755773493: - name: verify_get_42 - complete: false -14111824353587072050: - name: verify_get_42 - complete: false +11455748359517230147: + name: de_morgan_false + complete: true diff --git a/fixtures/contracts.fe b/fixtures/contracts.fe index 3d4f2741d1..fd74ee96e9 100644 --- a/fixtures/contracts.fe +++ b/fixtures/contracts.fe @@ -1,14 +1,19 @@ use std::spec +use std::evm +use std::buf::RawCallBuffer contract Foo { - pub fn get_42(self) -> u256 { - return 42 - } + pub fn __call__() { } } #invariant fn verify_get_42(mut ctx: Context) { - let foo: Foo = Foo.create(ctx, 0) - spec::given_eq(u256(address(foo)), 26) - spec::assert_eq(foo.get_42(), 42) + let foo: address = address(Foo.create(ctx, 0)) + let mut buf: RawCallBuffer = RawCallBuffer::new(input_len: 0, output_len: 0) + + spec::assert_true(ctx.raw_call( + addr: foo, + value: 0, + buf + )) } From 2547c355aa7887b3256a196faf0475f1f8ae217f Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Mon, 17 Jul 2023 10:38:07 -0600 Subject: [PATCH 08/10] hacking --- Cargo.lock | 1 + crates/fe/src/task/prove.rs | 4 ++-- crates/kevm-proof-service/src/server_impl/db.rs | 8 ++++++-- crates/kevm-proof-service/src/server_impl/mod.rs | 1 + crates/kevm-proof-service/src/server_impl/queue.rs | 2 +- crates/proof-service/Cargo.toml | 3 ++- 6 files changed, 13 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1d441a584c..19c35bd711 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -893,6 +893,7 @@ dependencies = [ name = "fe-proof-service" version = "0.23.0" dependencies = [ + "colored", "serde", "serde_json", "smol_str", diff --git a/crates/fe/src/task/prove.rs b/crates/fe/src/task/prove.rs index 4ec743c7e8..eb4e8a95b0 100644 --- a/crates/fe/src/task/prove.rs +++ b/crates/fe/src/task/prove.rs @@ -53,11 +53,11 @@ pub fn prove(args: ProveArgs) { if let Some(match_name) = &args.name { if name.contains(match_name) { let status = server.check_invariant(invariant, rerun); - println!("{} (status: {})", &name, &status) + println!("{0: <20} {1: <10}", &name, &status) } } else { let status = server.check_invariant(invariant, rerun); - println!("{} (status: {})", &name, &status) + println!("{0:.<20}{1: <10}", &name, &status) } } } diff --git a/crates/kevm-proof-service/src/server_impl/db.rs b/crates/kevm-proof-service/src/server_impl/db.rs index 9294b68d04..fec178eedc 100644 --- a/crates/kevm-proof-service/src/server_impl/db.rs +++ b/crates/kevm-proof-service/src/server_impl/db.rs @@ -18,7 +18,11 @@ impl DbEntry { impl Display for DbEntry { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "name: {} complete: {}", self.name, self.complete) + write!( + f, + "name: {0: <20} complete: {1: <5}", + self.name, self.complete + ) } } @@ -30,7 +34,7 @@ pub struct Db { 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: {} entry: ({})", id, entry)? + writeln!(f, "id: {0: <20} -> {1: <40}", id, entry)? } Ok(()) diff --git a/crates/kevm-proof-service/src/server_impl/mod.rs b/crates/kevm-proof-service/src/server_impl/mod.rs index 4e3c689b83..4a81aa516a 100644 --- a/crates/kevm-proof-service/src/server_impl/mod.rs +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -83,6 +83,7 @@ pub struct ServerState { 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)?; diff --git a/crates/kevm-proof-service/src/server_impl/queue.rs b/crates/kevm-proof-service/src/server_impl/queue.rs index 6af07ce7ef..2651d7a560 100644 --- a/crates/kevm-proof-service/src/server_impl/queue.rs +++ b/crates/kevm-proof-service/src/server_impl/queue.rs @@ -57,7 +57,7 @@ impl Display for &Spec { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!( f, - "name: {} id: {} status: {}", + "name: {0: <20} id: {1: <20} status: {2: <10}", self.name, self.invariant_id, &self.status ) } diff --git a/crates/proof-service/Cargo.toml b/crates/proof-service/Cargo.toml index 978bd0506f..e35dcaf782 100644 --- a/crates/proof-service/Cargo.toml +++ b/crates/proof-service/Cargo.toml @@ -9,4 +9,5 @@ repository = "https://github.com/ethereum/fe" [dependencies] smol_str = "0.1.21" serde = { version = "1.0", features = ["derive"] } -serde_json = { version = "1.0" } \ No newline at end of file +serde_json = { version = "1.0" } +colored = "2.0.0" \ No newline at end of file From 6fbb5eb37faf52a3121eecd728bd93caac8b435b Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Tue, 25 Jul 2023 10:14:26 -0600 Subject: [PATCH 09/10] WIP hacking --- crates/driver/src/lib.rs | 4 +- crates/fe/src/task/prove.rs | 2 +- crates/kevm-proof-service/src/main.rs | 6 +- .../kevm-proof-service/src/server_impl/db.rs | 5 +- .../kevm-proof-service/src/server_impl/mod.rs | 21 +- .../src/server_impl/queue.rs | 92 ------- crates/kevm/src/lib.rs | 236 +++++++++++++----- crates/kevm/templates/account.k | 8 + crates/kevm/{template.k => templates/spec.k} | 21 +- crates/proof-service/src/lib.rs | 10 +- .../src/{invariant.rs => symbolic_test.rs} | 23 +- 11 files changed, 213 insertions(+), 215 deletions(-) delete mode 100644 crates/kevm-proof-service/src/server_impl/queue.rs create mode 100644 crates/kevm/templates/account.k rename crates/kevm/{template.k => templates/spec.k} (78%) rename crates/proof-service/src/{invariant.rs => symbolic_test.rs} (57%) diff --git a/crates/driver/src/lib.rs b/crates/driver/src/lib.rs index 9d04b46b9c..d2fd46b5ea 100644 --- a/crates/driver/src/lib.rs +++ b/crates/driver/src/lib.rs @@ -7,7 +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::invariant::Invariant; +use fe_proof_service::symbolic_test::SymbolicTest; use fe_test_runner::TestSink; use indexmap::{indexmap, IndexMap}; use serde_json::Value; @@ -230,7 +230,7 @@ fn compile_module_tests(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec #[cfg(feature = "solc-backend")] fn compile_module_invariants(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec { - use fe_proof_service::invariant::Invariant; + use fe_proof_service::symbolic_test::Invariant; module_id .invariants(db) diff --git a/crates/fe/src/task/prove.rs b/crates/fe/src/task/prove.rs index eb4e8a95b0..a61ef528ed 100644 --- a/crates/fe/src/task/prove.rs +++ b/crates/fe/src/task/prove.rs @@ -1,7 +1,7 @@ #![cfg(feature = "solc-backend")] use clap::Args; use fe_common::diagnostics::print_diagnostics; -use fe_proof_service::invariant::Invariant; +use fe_proof_service::symbolic_test::Invariant; use fe_proof_service::ProofClient; // const DEFAULT_OUTPUT_DIR_NAME: &str = "prove"; diff --git a/crates/kevm-proof-service/src/main.rs b/crates/kevm-proof-service/src/main.rs index 0dd5769287..b2adb771e4 100644 --- a/crates/kevm-proof-service/src/main.rs +++ b/crates/kevm-proof-service/src/main.rs @@ -15,8 +15,12 @@ use clap::Parser; struct Args { #[clap(short, long, default_value = "127.0.0.1:7878")] bind_addrs: String, - #[clap(long, action)] + #[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() { diff --git a/crates/kevm-proof-service/src/server_impl/db.rs b/crates/kevm-proof-service/src/server_impl/db.rs index fec178eedc..8d8e5a9da5 100644 --- a/crates/kevm-proof-service/src/server_impl/db.rs +++ b/crates/kevm-proof-service/src/server_impl/db.rs @@ -1,13 +1,14 @@ 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 { - pub name: SmolStr, - pub complete: bool, + name: SmolStr, + is_success: bool, } impl DbEntry { diff --git a/crates/kevm-proof-service/src/server_impl/mod.rs b/crates/kevm-proof-service/src/server_impl/mod.rs index 4a81aa516a..31762edcbb 100644 --- a/crates/kevm-proof-service/src/server_impl/mod.rs +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -11,23 +11,21 @@ use crossterm::{ execute, terminal::{Clear, ClearType}, }; -use fe_proof_service::{invariant::Invariant, ProofStatus}; +use fe_proof_service::{symbolic_test::SymbolicTest, ProofStatus}; use indexmap::{indexmap, IndexMap}; -use kevm::KSpecExecPool; +use kevm::{KSpec, KSpecExecPool}; use smol_str::SmolStr; mod db; -mod queue; -use self::{db::Db, queue::Spec}; -use self::{db::DbEntry, queue::Queue}; +use self::db::Db; pub struct Server { state: Arc>, } impl Server { - pub fn new(db_path: &str) -> Self { + 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); @@ -61,8 +59,6 @@ impl Server { let state_clone = Arc::clone(&self.state); thread::spawn(move || loop { - thread::sleep(Duration::from_millis(1000)); - let mut stdout = io::stdout(); execute!(stdout, Clear(ClearType::All)).unwrap(); @@ -70,13 +66,16 @@ impl Server { print!("{content}"); execute!(stdout, MoveTo(0, 0)).unwrap(); + thread::sleep(Duration::from_millis(1000)); }); } } pub struct ServerState { - queue: Queue, - exec_pool: KSpecExecPool, + tests: IndexMap, + statuses: IndexMap, + queue: Vec, + pool: KSpecExecPool, db: Db, } @@ -105,7 +104,7 @@ impl ServerState { } } - pub fn add_spec(&mut self, spec: Spec) { + pub fn add_test(&mut self, test: SymbolicTest) { self.queue.push_spec(spec) } diff --git a/crates/kevm-proof-service/src/server_impl/queue.rs b/crates/kevm-proof-service/src/server_impl/queue.rs deleted file mode 100644 index 2651d7a560..0000000000 --- a/crates/kevm-proof-service/src/server_impl/queue.rs +++ /dev/null @@ -1,92 +0,0 @@ -use std::fmt::Display; - -use fe_proof_service::{ - invariant::{Invariant, InvariantBody}, - ProofStatus, -}; -use kevm::{KSpec, KSpecType}; -use smol_str::SmolStr; - -pub struct Spec { - pub name: SmolStr, - pub k_spec: KSpec, - pub invariant_id: u64, - pub status: ProofStatus, -} - -pub fn k_type_from_fe_type(typ: &str) -> KSpecType { - match typ { - "u256" => KSpecType::U256, - "u128" => KSpecType::U128, - "u64" => KSpecType::U64, - "u32" => KSpecType::U32, - "u16" => KSpecType::U16, - "u8" => KSpecType::U8, - "bool" => KSpecType::Bool, - "Context" => KSpecType::Context, - "mut Context" => KSpecType::Context, - _ => panic!("invalid fe type string: {}", typ), - } -} - -fn k_spec_from_invariant(invariant: Invariant) -> KSpec { - let Invariant { name: _, body } = invariant; - let InvariantBody { args, code } = body; - KSpec::new( - args.iter().map(|typ| k_type_from_fe_type(&typ)).collect(), - code, - ) -} - -impl Spec { - pub fn new_from_invariant(invariant: Invariant) -> Self { - let invariant_id = invariant.id(); - let name = invariant.name.clone(); - let k_spec = k_spec_from_invariant(invariant); - - Self { - name, - k_spec, - invariant_id, - status: ProofStatus::New, - } - } -} - -impl Display for &Spec { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!( - f, - "name: {0: <20} id: {1: <20} status: {2: <10}", - self.name, self.invariant_id, &self.status - ) - } -} - -pub struct Queue { - pub specs: Vec, -} - -impl Display for &Queue { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - for spec in &self.specs { - writeln!(f, "{}", spec)? - } - - Ok(()) - } -} - -impl Queue { - pub fn new() -> Self { - Self { specs: vec![] } - } - - pub fn push_spec(&mut self, spec: Spec) { - self.specs.push(spec) - } - - pub fn remove(&mut self, id: u64) { - self.specs.retain(|spec| spec.invariant_id != id); - } -} diff --git a/crates/kevm/src/lib.rs b/crates/kevm/src/lib.rs index 952c7e6f2c..4b3b870897 100644 --- a/crates/kevm/src/lib.rs +++ b/crates/kevm/src/lib.rs @@ -9,59 +9,193 @@ use std::{ }; use indexmap::{indexmap, IndexMap}; +use smol_str::SmolStr; -const KSPEC_TEMPLATE: &str = include_str!("../template.k"); +const KSPEC_TEMPLATE: &str = include_str!("../templates/spec.k"); +const KACCT_TEMPLATE: &str = include_str!("../templates/account.k"); -#[derive(Clone, Copy, PartialEq, Eq)] -pub enum KSpecType { - U256, - U128, - U64, - U32, - U16, - U8, - Bool, - Context, +#[derive(Clone)] +pub enum KSymbol { + Name(SmolStr), + None, } -impl KSpecType { - pub fn bounds(&self, arg_name: &str) -> String { +impl Display for KSymbol { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - KSpecType::U256 => { - format!("andBool 0 <=Int {arg_name} andBool {arg_name} { - format!("andBool 0 <=Int {arg_name} andBool {arg_name} { - format!("andBool 0 <=Int {arg_name} andBool {arg_name} { - format!("andBool 0 <=Int {arg_name} andBool {arg_name} { - format!("andBool 0 <=Int {arg_name} andBool {arg_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) } - KSpecType::U8 => { - format!("andBool 0 <=Int {arg_name} andBool {arg_name} { + let s = inners + .iter() + .map(|inner| inner.to_string()) + .collect::>() + .join(" +Bytes "); + write!(f, "{}", s) } - KSpecType::Bool => format!("andBool (0 ==Int {arg_name} orBool {arg_name} ==Int 1)"), - KSpecType::Context => panic!("no bounds for ctx"), } } } +#[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 { - args: Vec, + local_mem: KBuf, code: String, + origin: KSymbol, + accounts: Vec, + requirements: KBool, } -impl KSpec { - pub fn new(args: Vec, code: String) -> Self { - Self { args, code } +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}"); @@ -95,38 +229,6 @@ impl KSpec { } } -impl Display for KSpec { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let mut mem_args = vec![]; - let mut requirements = vec![]; - let mut arg_num = 0; - - for arg in &self.args { - if *arg != KSpecType::Context { - let arg_name = format!("ARG_{}", arg_num); - requirements.push(arg.bounds(&arg_name)); - mem_args.push(format!("#buf(32, {})", arg_name)); - arg_num += 1; - } - } - - let mem_args = if mem_args.is_empty() { - "_".to_string() - } else { - mem_args.join(" +Bytes ") - }; - - write!( - f, - "{}", - KSPEC_TEMPLATE - .replace("$CODE", &format!("\"0x{}\"", &self.code)) - .replace("$MEM_ARGS", &mem_args) - .replace("$REQUIREMENTS", &requirements.join("\n")) - ) - } -} - pub struct KSpecExecPool { cur_executing: IndexMap>>>, } 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/template.k b/crates/kevm/templates/spec.k similarity index 78% rename from crates/kevm/template.k rename to crates/kevm/templates/spec.k index 372933c883..91a20931c3 100644 --- a/crates/kevm/template.k +++ b/crates/kevm/templates/spec.k @@ -28,7 +28,7 @@ module INVARIANT-SPEC 0 .WordStack => ?_ - $MEM_ARGS + $LOCAL_MEM 0 => ?_ #gas(_VGAS) => ?_ 0 => ?_ @@ -47,7 +47,7 @@ module INVARIANT-SPEC _ - ORIGIN_ID + $ORIGIN _ @@ -74,17 +74,10 @@ module INVARIANT-SPEC _ - SetItem(ACCT_ID) _:Set + $ACTIVE_ACCOUNTS - - ACCT_ID - _ - #parseByteStack($CODE) - _ - _ - _ - + $ACCOUNTS _ @@ -94,11 +87,7 @@ module INVARIANT-SPEC - requires 0 <=Int ACCT_ID andBool ACCT_ID ) -> std::fmt::Result { match self { ProofStatus::New => write!(f, "New"), - ProofStatus::Ready => write!(f, "Ready"), + ProofStatus::Ready => write!(f, "Queued"), ProofStatus::Proving => write!(f, "Proving"), ProofStatus::Complete => write!(f, "Complete"), ProofStatus::Incomplete => write!(f, "Incomplete"), @@ -41,14 +41,14 @@ impl ProofClient { } impl ProofClient { - pub fn check_invariant(&self, invariant: Invariant, rerun: bool) -> ProofStatus { + 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(&invariant).unwrap(); + 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(); diff --git a/crates/proof-service/src/invariant.rs b/crates/proof-service/src/symbolic_test.rs similarity index 57% rename from crates/proof-service/src/invariant.rs rename to crates/proof-service/src/symbolic_test.rs index 2e5521d527..b806b12cc6 100644 --- a/crates/proof-service/src/invariant.rs +++ b/crates/proof-service/src/symbolic_test.rs @@ -6,28 +6,22 @@ use std::{ }; #[derive(Debug, Serialize, Deserialize)] -pub struct Invariant { +pub struct SymbolicTest { pub name: SmolStr, - pub body: InvariantBody, -} - -#[derive(Debug, Serialize, Deserialize)] -pub struct InvariantHeader { - pub name: SmolStr, - pub id: u64, + pub body: SymbolicTestBody, } #[derive(Hash, Debug, Serialize, Deserialize)] -pub struct InvariantBody { +pub struct SymbolicTestBody { pub args: Vec, pub code: String, } -impl Invariant { +impl SymbolicTest { pub fn new(name: SmolStr, args: Vec, code: String) -> Self { Self { name, - body: InvariantBody { args, code }, + body: SymbolicTestBody { args, code }, } } @@ -36,11 +30,4 @@ impl Invariant { self.body.hash(&mut s); s.finish() } - - pub fn header(&self) -> InvariantHeader { - InvariantHeader { - name: self.name.clone(), - id: self.id(), - } - } } From 5f017caf26674f7273fb676845c5994465a2cacb Mon Sep 17 00:00:00 2001 From: Grant Wuerker Date: Fri, 18 Aug 2023 19:25:45 +0200 Subject: [PATCH 10/10] hacking --- .../kevm-proof-service/src/server_impl/mod.rs | 41 +++++++++---------- 1 file changed, 20 insertions(+), 21 deletions(-) diff --git a/crates/kevm-proof-service/src/server_impl/mod.rs b/crates/kevm-proof-service/src/server_impl/mod.rs index 31762edcbb..a7572f9d9b 100644 --- a/crates/kevm-proof-service/src/server_impl/mod.rs +++ b/crates/kevm-proof-service/src/server_impl/mod.rs @@ -72,10 +72,14 @@ impl Server { } pub struct ServerState { + // contains all known tests tests: IndexMap, - statuses: IndexMap, - queue: Vec, + // 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, } @@ -85,10 +89,10 @@ impl Display for ServerState { writeln!(f, "")?; writeln!(f, "queue:")?; - writeln!(f, "{}", &self.queue)?; + writeln!(f, "{:?}", &self.queue)?; writeln!(f, "execution pool:")?; - writeln!(f, "{}", &self.exec_pool)?; + writeln!(f, "{:?}", &self.exec_pool)?; writeln!(f, "db:")?; writeln!(f, "{}", &self.db) @@ -98,31 +102,26 @@ impl Display for ServerState { impl ServerState { pub fn new(db_path: &str) -> Self { ServerState { - queue: Queue::new(), - exec_pool: KSpecExecPool::new(), + tests: indexmap! {}, + stack: vec![], + pool: KSpecExecPool::new(), db: Db::new(db_path), } } pub fn add_test(&mut self, test: SymbolicTest) { - self.queue.push_spec(spec) + let id = test.id(); + + if !self.stack.contains(id) && !self.db.contains(id) {} } - pub fn proof_status(&self, invariant_id: u64) -> ProofStatus { - if let Some(entry) = self.db.get(invariant_id) { - if entry.complete { - ProofStatus::Complete - } else { - ProofStatus::Incomplete - } + 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 { - for spec in &self.queue.specs { - if spec.invariant_id == invariant_id { - return spec.status; - } - } - - panic!("missing invariant") + // unknown } }