Verifier 1 (#10)

* add crate

* introduce runner trait and merge parser and sem errors

* verifier ast

* docs

* fix enum access

* translate literals to z3 primitives

* transform basic operations and literals

* rename module

* add math model concept

* [untested] transdorm expressions to Z3 AST

* test expression translation

* delete project files

* partially resolve models

* optimise ast lifetimes

* [untested] resolve declarations

* simplify context passing and lifetimes

* [untested] check individual blocks

* [tested] improve constraint generation respecting co-dependent structs

* cleanup

* parse params object to transformer

* cleanup

* add `verify` command and support nested errors

* apply addition on strings

* fix test

* clippy suggestions

* small cleanup

* [tested] verify consistency in linked blocks

* add changelog

* refine the test

* add docs

* update examples and add CI test

.github/workflows/ci.yml

@@ -27,10 +27,30 @@ jobs:
   fmt:
     name: Check formatting
     runs-on: ubuntu-latest
+
     steps:
       - uses: actions/checkout@v4
       - uses: Swatinem/rust-cache@v2
       - uses: dtolnay/rust-toolchain@nightly
         with: 
           components: rustfmt
-      - run: cargo +nightly fmt --all -- --check --verbose
+      - run: cargo +nightly fmt --all -- --check --verbose
+
+  examples:
+    strategy:
+      matrix:
+        job:
+          - check
+          - verify
+    name: Compile and formally test examples
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: Swatinem/rust-cache@v2
+      - uses: dtolnay/rust-toolchain@stable
+      - run: | 
+           for example in examples/*/; do
+               echo "Processing example: $example";
+               cargo run ${{ matrix.job }} $example/contract.fol
+           done
+            

.gitignore

@@ -308,5 +308,6 @@ Cargo.lock
 .DS_Store
 
 reports/ecsproject.pdf
+.vscode
 
 /auto

CHANGELOG.md

@@ -5,6 +5,7 @@ Contains important changes as part of the project development adhering to [seman
 ## Unreleased
 
 ### Added 
+- Verifier 1 - [#10](https://github.com/SkymanOne/folidity/pull/10)
 - Compiler executable 1 - [#9](https://github.com/SkymanOne/folidity/pull/9)
 - Semantics 1 - [#7](https://github.com/SkymanOne/folidity/pull/7)
 - Parser - [#4](https://github.com/SkymanOne/folidity/pull/4)

Cargo.toml

@@ -5,7 +5,8 @@ members = [
     "crates/diagnostics",
     "crates/folidity",
     "crates/parser", 
-    "crates/semantics",
+    "crates/semantics", 
+    "crates/verifier", 
 ]
 
 [workspace.package]
@@ -21,8 +22,9 @@ version = "1.0.0"
 [workspace.dependencies]
 folidity-parser = { path = "crates/parser" }
 folidity-diagnostics = { path = "crates/diagnostics" }
-derive-node = { path = "crates/derive_node" }
 folidity-semantics = { path = "crates/semantics" }
+folidity-verifier = { path = "crates/verifier" }
+derive-node = { path = "crates/derive_node" }
 logos = "0.14"
 lalrpop-util = "0.20"
 lalrpop = "0.20"
@@ -43,4 +45,6 @@ clap = { version ="4.5", features = ["derive"]}
 ariadne = { version = "0.4", features = ["auto-color"] }
 anyhow = "1.0"
 walkdir = "2.5"
-yansi = "1.0"
+yansi = "1.0"
+# we need to pin to commit as the crate version doesn't allow us to detect local `z3` binary.
+z3 =  { git = "https://github.com/prove-rs/z3.rs.git", rev = "247d308f27d8b59152ad402e2d8b13d617a1a6a1" }