hacking

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

crates/analyzer/src/db.rs

@@ -110,6 +110,8 @@ pub trait AnalyzerDb: SourceDb + Upcast<dyn SourceDb> + UpcastMut<dyn SourceDb>
     fn module_submodules(&self, module: ModuleId) -> Rc<[ModuleId]>;
     #[salsa::invoke(queries::module::module_tests)]
     fn module_tests(&self, module: ModuleId) -> Vec<FunctionId>;
+    #[salsa::invoke(queries::module::module_invariants)]
+    fn module_invariants(&self, module: ModuleId) -> Vec<FunctionId>;
 
     // Module Constant
     #[salsa::cycle(queries::module::module_constant_type_cycle)]

crates/analyzer/src/db/queries/module.rs

@@ -760,3 +760,12 @@ pub fn module_tests(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
         .filter(|function| function.is_test(db))
         .collect()
 }
+
+pub fn module_invariants(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
+    ingot
+        .all_functions(db)
+        .iter()
+        .copied()
+        .filter(|function| function.is_invariant(db))
+        .collect()
+}

crates/analyzer/src/namespace/items.rs

@@ -555,6 +555,10 @@ impl ModuleId {
         db.module_tests(*self)
     }
 
+    pub fn invariants(&self, db: &dyn AnalyzerDb) -> Vec<FunctionId> {
+        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 {

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) {

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::<Vec<_>>();
+    let call = function_call_statement! {[test_func_name]([call_args...])};
 
     let code = code! {
         [dep_functions...]

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
         }
     }
 

crates/driver/Cargo.toml

@@ -20,6 +20,7 @@ fe-codegen = {path = "../codegen", version = "^0.22.0"}
 fe-parser = {path = "../parser", version = "^0.22.0"}
 fe-yulc = {path = "../yulc", version = "^0.22.0", features = ["solc-backend"], optional = true}
 fe-test-runner = {path = "../test-runner", version = "^0.22.0"}
+fe-proof-service = {path = "../proof-service", version = "^0.22.0"}
 indexmap = "1.6.2"
 vfs = "0.5.1"
 smol_str = "0.1.21"

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<Vec<Invariant>, 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<Invariant> {
+    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,

crates/fe/Cargo.toml

@@ -24,3 +24,4 @@ fe-test-runner = {path = "../test-runner", version = "^0.22.0"}
 fe-common = {path = "../common", version = "^0.22.0"}
 fe-driver = {path = "../driver", version = "^0.22.0"}
 fe-parser = {path = "../parser", version = "^0.22.0"}
+fe-proof-service = {path = "../proof-service", version = "^0.22.0"}

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))
+//     )
+// }