fv crate

Author: g-r-a-n-t

.github/workflows/expensive.yml

@@ -29,10 +29,10 @@ jobs:
         uses: Swatinem/rust-cache@v1
 
       - name: Build
-        run: cargo test --workspace --all-features --no-run --locked -- --ignored
+        run: cargo test --workspace --features solc-backend --no-run --locked -- --ignored
       - name: Run expensive tests
         id: expensive_tests
-        run: cargo test --workspace --all-features --verbose -- --ignored
+        run: cargo test --workspace --features solc-backend --verbose -- --ignored
       - name: Report
         if: failure() && steps.expensive_tests.outcome == 'failure'
         run: |

.github/workflows/main.yml

@@ -121,9 +121,9 @@ jobs:
       - name: Cache Dependencies
         uses: Swatinem/rust-cache@v1
       - name: Build
-        run: cargo test --workspace --all-features --no-run --locked
+        run: cargo test --workspace --features solc-backend --no-run --locked
       - name: Run tests
-        run: cargo test --workspace --all-features --verbose
+        run: cargo test --workspace --features solc-backend --verbose
 
   wasm-test:
       runs-on: ubuntu-latest
@@ -179,7 +179,7 @@ jobs:
           toolchain: stable
           override: true
       - name: Build
-        run: cargo build --all-features --release && strip target/release/fe && mv target/release/fe target/release/${{ matrix.BIN_FILE }}
+        run: cargo build --features solc-backend --release && strip target/release/fe && mv target/release/fe target/release/${{ matrix.BIN_FILE }}
       - name: Release
         uses: softprops/action-gh-release@v1
         with:

Cargo.lock

@@ -75,11 +75,11 @@ docker-wasm-test:
 
 .PHONY: coverage
 coverage:
-	cargo tarpaulin --workspace --all-features --verbose --timeout 120 --exclude-files 'tests/*' --exclude-files 'main.rs' --out xml html -- --skip differential::
+	cargo tarpaulin --workspace --features solc-backend --verbose --timeout 120 --exclude-files 'tests/*' --exclude-files 'main.rs' --out xml html -- --skip differential::
 
 .PHONY: clippy
 clippy:
-	cargo clippy --workspace --all-targets --all-features -- -D warnings -A clippy::upper-case-acronyms -A clippy::large-enum-variant -W clippy::redundant_closure_for_method_calls
+	cargo clippy --workspace --all-targets --features solc-backend -- -D warnings -A clippy::upper-case-acronyms -A clippy::large-enum-variant -W clippy::redundant_closure_for_method_calls
 
 .PHONY: rustfmt
 rustfmt:

Makefile

@@ -30,6 +30,8 @@ pub struct CompiledContract {
     pub yul: String,
     #[cfg(feature = "solc-backend")]
     pub bytecode: String,
+    #[cfg(feature = "solc-backend")]
+    pub runtime_bytecode: String,
 }
 
 #[derive(Debug)]
@@ -128,6 +130,15 @@ fn compile_module_id(
         IndexMap::new()
     };
 
+    // compile runtimes to yul
+    let yul_contract_runtimes = fe_yulgen::compile_runtimes(db, lowered_module_id);
+
+    let _bytecode_contract_runtimes = if _with_bytecode {
+        compile_yul_runtimes(yul_contract_runtimes.iter(), _optimize)
+    } else {
+        IndexMap::new()
+    };
+
     // combine all of the named contract maps
     let contracts = json_abis
         .keys()
@@ -143,6 +154,12 @@ fn compile_module_id(
                     } else {
                         "".to_string()
                     },
+                    #[cfg(feature = "solc-backend")]
+                    runtime_bytecode: if _with_bytecode {
+                        _bytecode_contract_runtimes[name].to_owned()
+                    } else {
+                        "".to_string()
+                    },
                 },
             )
         })
@@ -185,3 +202,34 @@ fn compile_yul(
     #[cfg(not(feature = "solc-backend"))]
     IndexMap::new()
 }
+
+fn compile_yul_runtimes(
+    _contracts: impl Iterator<Item = (impl AsRef<str>, impl AsRef<str>)>,
+    _optimize: bool,
+) -> IndexMap<String, String> {
+    #[cfg(feature = "solc-backend")]
+    {
+        match fe_yulc::compile_runtimes(_contracts, _optimize) {
+            Err(error) => {
+                for error in serde_json::from_str::<Value>(&error.0)
+                    .expect("unable to deserialize json output")["errors"]
+                    .as_array()
+                    .expect("errors not an array")
+                {
+                    eprintln!(
+                        "Error: {}",
+                        error["formattedMessage"]
+                            .as_str()
+                            .expect("error value not a string")
+                            .replace("\\\n", "\n")
+                    )
+                }
+                panic!("Yul compilation failed with the above errors")
+            }
+            Ok(contracts) => contracts,
+        }
+    }
+
+    #[cfg(not(feature = "solc-backend"))]
+    IndexMap::new()
+}

crates/driver/src/lib.rs

@@ -22,6 +22,7 @@ arg_enum! {
         Ast,
         LoweredAst,
         Bytecode,
+        RuntimeBytecode,
         Tokens,
         Yul,
     }
@@ -52,7 +53,15 @@ pub fn main() {
                 .short("e")
                 .long("emit")
                 .help("Comma separated compile targets e.g. -e=bytecode,yul")
-                .possible_values(&["abi", "bytecode", "ast", "tokens", "yul", "loweredAst"])
+                .possible_values(&[
+                    "abi",
+                    "bytecode",
+                    "runtimeBytecode",
+                    "ast",
+                    "tokens",
+                    "yul",
+                    "loweredAst",
+                ])
                 .default_value("abi,bytecode")
                 .use_delimiter(true)
                 .takes_value(true),
@@ -240,6 +249,15 @@ fn write_compiled_module(
             let file_name = format!("{}.bin", &name);
             write_output(&contract_output_dir.join(file_name), &contract.bytecode)?;
         }
+
+        #[cfg(feature = "solc-backend")]
+        if targets.contains(&CompilationTarget::RuntimeBytecode) {
+            let file_name = format!("{}.runtime.bin", &name);
+            write_output(
+                &contract_output_dir.join(file_name),
+                &contract.runtime_bytecode,
+            )?;
+        }
     }
 
     Ok(())

crates/fe/src/main.rs

@@ -0,0 +1,20 @@
+[package]
+authors = ["The Fe Developers <snakecharmers@ethereum.org>"]
+categories = ["cryptography::cryptocurrencies", "command-line-utilities", "development-tools"]
+description = "Fe formal verification utilities"
+edition = "2021"
+keywords = ["ethereum", "fe", "yul", "smart", "contract", "compiler"]
+license = "GPL-3.0-or-later"
+name = "fv"
+readme = "README.md"
+repository = "https://github.com/ethereum/fe"
+version = "0.15.0-alpha"
+
+[features]
+solc-backend = ["fe-driver/solc-backend"]
+kevm-backend = []
+
+[dependencies]
+fe-driver = {path = "../driver", version = "^0.15.0-alpha"}
+fe-yulgen = {path = "../yulgen", version = "^0.15.0-alpha"}
+fe-test-files = {path = "../test-files", version = "^0.15.0-alpha"}

crates/fv/Cargo.toml

@@ -0,0 +1,41 @@
+# Fe Fv
+
+This crate contains utilities for building and running kevm specs.
+
+## kevm setup
+
+A system installation of [evm-semantics](https://github.com/fe-lang/evm-semantics) is required to run the specs. Please clone the repository and follow the installation directions.
+
+While in the `evm-semantics` project, `kompile` the Fe verification module:
+
+```commandline
+$ export PATH=$PATH:/path/to/evm-semantics/.build/usr/bin
+$ kevm kompile --backend haskell tests/specs/fe/verification.k                                  \
+    --directory tests/specs/fe/verification/haskell                                             \
+    --main-module VERIFICATION                                                                  \
+    --syntax-module VERIFICATION                                                                \
+    --concrete-rules-file tests/specs/fe/concrete-rules.txt                                     \
+    -I /usr/lib/kevm/include/kframework -I /usr/lib/kevm/blockchain-k-plugin/include/kframework
+```
+
+## running the proofs
+
+Once the evm-semantics project has been built, set the `KEVM_PATH` environment variable:
+
+```commandline
+$ export KEVM_PATH=/path/to/evm-semantics
+```
+
+and then run the tests: 
+
+```commandline
+$ cargo test --features "solc-backend, kevm-backend"
+```
+
+*Note: If you are working on a resource constrained device, you may not be able to run all tests simultaneously. If issues are encountered, run tests in smaller groups.*
+
+e.g.
+
+```commandline
+$ cargo test sanity_returns_42 --features "solc-backend, kevm-backend"
+```

crates/fv/README.md

@@ -0,0 +1,63 @@
+#![cfg(feature = "kevm-backend")]
+use fe_yulgen::Db;
+use std::path::Path;
+use std::process::Command;
+use std::{env, fs};
+
+const SPECS_DIR: &str = "tests/specs/fe/";
+
+pub fn kevm_path() -> String {
+    env::var("KEVM_PATH").expect("`KEVM_PATH` not set")
+}
+
+pub fn run_spec(name: &str, src_path: &str, src: &str, spec: &str) -> Result<(), String> {
+    let kevm_path = kevm_path();
+
+    let spec = build_spec(name, src_path, src, spec);
+    let spec_path = Path::new(&kevm_path)
+        .join(SPECS_DIR)
+        .join(name)
+        .with_extension("k");
+    fs::write(spec_path.clone(), spec).expect("unable to write file");
+
+    let path = env::var("PATH").expect("PATH is not set");
+
+    let out = Command::new("kevm")
+        .arg("prove")
+        .arg(spec_path.to_str().unwrap())
+        .arg("--backend")
+        .arg("haskell")
+        .arg("--format-failures")
+        .arg("--directory")
+        .arg("tests/specs/fe/verification/haskell")
+        .env("PATH", format!(".build/usr/bin:{}", path))
+        .current_dir(&kevm_path)
+        .output()
+        .expect("failed to execute process");
+
+    if out.status.code() != Some(0) {
+        Err(format!(
+            "{}\n{}",
+            String::from_utf8_lossy(&out.stderr),
+            String::from_utf8_lossy(&out.stdout)
+        ))
+    } else {
+        Ok(())
+    }
+}
+
+pub fn build_spec(name: &str, src_path: &str, src: &str, spec: &str) -> String {
+    let mut db = Db::default();
+    let module = fe_driver::compile_single_file(&mut db, src_path, src, true, true).unwrap();
+
+    // replace placeholders
+    let mut new_spec = spec.to_owned().replace("$TEST_NAME", &name.to_uppercase());
+    for (name, contract) in module.contracts.iter() {
+        new_spec = new_spec.replace(
+            &format!("${}::RUNTIME", name),
+            &format!("\"0x{}\"", contract.runtime_bytecode),
+        )
+    }
+
+    new_spec
+}

crates/fv/src/lib.rs

@@ -0,0 +1,49 @@
+#![cfg(feature = "kevm-backend")]
+
+/// Checks if a contract spec is valid.
+macro_rules! test_spec {
+    ($name:ident, $src_path:expr, $spec_path:expr) => {
+        #[test]
+        fn $name() {
+            let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
+            let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
+
+            if let Err(output) =
+                fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec)
+            {
+                panic!("{}", output)
+            }
+        }
+    };
+}
+
+/// Checks if a contract spec is invalid.
+macro_rules! test_spec_invalid {
+    ($name:ident, $src_path:expr, $spec_path:expr) => {
+        #[test]
+        fn $name() {
+            let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
+            let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
+
+            match fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec) {
+                Ok(()) => panic!("spec is valid"),
+                Err(output) => {
+                    // we want to make sure it didn't fail for some other reason
+                    if !output.contains("the claimed implication is not valid") {
+                        panic!("spec claim was not checked {}", output)
+                    }
+                }
+            }
+        }
+    };
+}
+
+test_spec! { sanity_returns_42, "sanity/foo.fe", "sanity/returns_42.k" }
+test_spec! { sanity_returns_in, "sanity/foo.fe", "sanity/returns_in.k" }
+test_spec! { sanity_returns_in_cond1, "sanity/foo.fe", "sanity/returns_in_cond1.k" }
+test_spec! { sanity_returns_in_cond2, "sanity/foo.fe", "sanity/returns_in_cond2.k" }
+
+// these are just for extra sanity
+test_spec_invalid! { sanity_returns_42_invalid, "sanity/foo.fe", "sanity/returns_42_invalid.k" }
+test_spec_invalid! { sanity_returns_in_invalid, "sanity/foo.fe", "sanity/returns_in_invalid.k" }
+test_spec_invalid! { sanity_returns_in_cond2_invalid, "sanity/foo.fe", "sanity/returns_in_cond2_invalid.k" }