Main report

README.md

@@ -0,0 +1,37 @@
+# Folidity - Formally Verifiable Smart Contract Language
+
+This project addresses the long-lasting problem involving the exploits of Smart Contract vulnerabilities. There are tools, such as in the formal verification field and alternative Smart Contract languages, that attempt to address these issues. However, neither approach has managed to combine the static formal verification and the generation of runtime assertions. Furthermore, this work believes that implicit hidden state transition is the root cause of security compromises. In light of the above, we introduce Folidity, a formally verifiable Smart Contract language with a unique approach to reasoning about the modelling and development of Smart Contract systems. Folidity features explicit state transition checks, a model-first approach, and built-in formal verification compilation stage.
+
+Folidity targets [Algorand Virtual Machine](https://developer.algorand.org/docs/get-details/dapps/avm) and emits [Teal](https://developer.algorand.org/docs/get-details/dapps/avm/teal/) bytecode. The EVM support is at the planned work.  
+
+## Installation
+
+- Prerequisites
+  - Install [`z3`](https://github.com/Z3Prover/z3).
+    - Most systems that have LLVM already have it installed.
+    - Otherwise, you can install it with the standard package manager (e.g. `brew install z3`)
+  - Install [rust stable](https://www.rust-lang.org/learn/get-started)
+- Install the binary: `cargo install --path crates/folidity`
+- (Optional) install cargo nightly for formatting when developing: `rustup toolchain install nightly`
+
+## Usage
+Start with `folidity help` to get the overview of the supported command and their options.
+
+- `folidity new ...` - Creates a new templated `folidity` counter project. with a basic contract, README and approval teal code
+- `folidity check ...` - Check the contract's code for parser, semantic and type errors
+- `folidity verify ...`  - Check the contract's code for errors and validate model consistency using static analysis and symbolic execution
+- `foliidty compile ...` - Check the contract's code for errors and validate model consistency using static analysis and symbolic execution
+
+## Status
+
+Folidity is an exprimental project and is not currently considered Production Ready for general use. It may have unexpected behavior outside of the scenarios it has been used for until now.
+
+## Changelog
+
+The project maintains a clear [changelog](CHANGELOG.md) of versions and adheres to semantic versioning.
+
+## License
+
+Folidity is currently licensed under the [University of Southampton Intellectual Property Regulation](https://www.southampton.ac.uk/about/governance/regulations-policies/general-regulations/intellectual-property).
+
+The project maintainer is at the negotiating stage to fully open-source the project under MIT/Apache 2.0 License.

concepts/grammar.md

@@ -24,7 +24,7 @@ Based on holistic approach
 
 <st_block>     := `st` <expr>
 
-<statement>    := <var> | <assign> | <if> | <for> | <foreach> | <return> | <func_call> | <state_t> `;`
+<statement>    := <var> | <assign> | <if> | <for> | <foreach> | <return> | <func_call> | <state_t> `skip` `;`
 <state_t>      := `move` <struct_init>
 <var>          := let `mut`? <var_ident> (`:` <type>)? (`=` <expr>)?
 <var_ident>    := (<ident> | <decon>)

crates/parser/src/tests.rs

@@ -937,7 +937,7 @@ fn () execute() when (RevealState s) -> ExecuteState {
     }
 }
 
-view(BeginState s) fn list<Address> get_voters() {
+view(BeginState s) fn list<address> get_voters() {
     return s.voters;
 }
 "#;

crates/semantics/src/symtable.rs

@@ -69,8 +69,6 @@ pub struct SymTable {
     pub context: ScopeContext,
 }
 
-impl SymTable {}
-
 #[derive(Debug, Clone)]
 pub struct Scope {
     /// Indexed map of variables

crates/verifier/src/links.rs

@@ -13,10 +13,6 @@ use crate::{
 
 type LinkGraph = Graph<usize, usize, Undirected, usize>;
 
-// pub struct LinkBlock<'ctx> {
-
-// }
-
 fn find_link_components(executor: &SymbolicExecutor) -> Vec<Vec<usize>> {
     let mut edges: HashSet<(usize, usize)> = HashSet::new();
 

reports/ECS.bib

@@ -338,4 +338,46 @@ @book{types_pierce
   publisher = {The MIT Press},
   title     = {Types and Programming Languages},
   year      = {2002}
-}
+}
+
+@misc{sorkin2012lr1,
+  title         = {LR(1) Parser Generation System: LR(1) Error Recovery, Oracles, and Generic Tokens},
+  author        = {Arthur Sorkin and Peter Donovan},
+  year          = {2012},
+  eprint        = {1010.1234},
+  archiveprefix = {arXiv},
+  primaryclass  = {cs.PL}
+}
+
+@inproceedings{component_interface,
+  author    = {Howar, Falk
+               and Giannakopoulou, Dimitra
+               and Mues, Malte
+               and Navas, Jorge A.},
+  editor    = {Margaria, Tiziana
+               and Steffen, Bernhard},
+  title     = {Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring},
+  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Verification},
+  year      = {2018},
+  publisher = {Springer International Publishing},
+  address   = {Cham},
+  pages     = {120--136}
+}
+
+@inbook{array_theory,
+  author    = {McCarthy, J.},
+  editor    = {Colburn, Timothy R.
+               and Fetzer, James H.
+               and Rankin, Terry L.},
+  title     = {Towards a Mathematical Science of Computation},
+  booktitle = {Program Verification: Fundamental Issues in Computer Science},
+  year      = {1993},
+  publisher = {Springer Netherlands},
+  address   = {Dordrecht},
+  pages     = {35--56},
+  abstract  = {In this paper I shall discuss the prospects for a mathematical science of computation. In a mathematical science, it is possible to deduce from the basic assumptions, the important properties of the entities treated by the science. Thus, from Newton's law of gravitation and his laws of motion, one can deduce that the planetary orbits obey Kepler's laws.},
+  isbn      = {978-94-011-1793-7},
+  doi       = {10.1007/978-94-011-1793-7_2},
+  url       = {https://doi.org/10.1007/978-94-011-1793-7_2}
+}
+

reports/ecsproject.typ

@@ -10,29 +10,20 @@
   }
 }
 
-// Rotate content, presetcing width
-#let rotatex(angle, body)= style(styles => layout(size => {
-  let size = measure(block(width: size.width, body), styles)
-  box(inset:(x: -size.width/2+(size.width*calc.abs(calc.cos(angle))+size.height*calc.abs(calc.sin(angle)))/2,
-             y: -size.height/2+(size.height*calc.abs(calc.cos(angle))+size.width*calc.abs(calc.sin(angle)))/2),
-             rotate(body,angle))
-}))
-
-
 #let margins = (inside: 1.4in, outside: 1.0in, top: 1.0in, bottom: 1.0in)
 
+#let body-font = "New Computer Modern"
+#let sans-font = "New Computer Modern Sans"
+
 #let page_style(
   page_numbering: "1",
   title_numbering: "1.",
   doc
 ) = {
-
   set page(
     numbering: page_numbering,
     margin: margins,
   )
-  let body-font = "New Computer Modern"
-  let sans-font = "New Computer Modern Sans"
   set text(
     font: body-font, 
     size: 12pt, 
@@ -52,7 +43,7 @@
     let counter_display = if it.numbering != none {
       counter(heading).display(it.numbering)
     }
-    pad(top: 1.2em, bottom: 1.0em, left: 0.2em, [
+    pad(top: 1.4em, bottom: 1.4em, left: 0.2em, [
         #table(
           columns: 2,
           stroke: none,
@@ -104,7 +95,7 @@
         let h_counter = counter(heading.where(level: 1)).display()
         let last_header = before_elems.last().body
         v(4em)
-        if last_header == text("Statement of Originality") {
+        if last_header == text("Statement of Originality") or last_header == text("Bibliography") {
           emph(last_header) + h(1fr) + counter(page).display(page_numbering)
         } else {
           emph(h_counter + " " + last_header) + h(1fr) + counter(page).display(page_numbering)
@@ -158,10 +149,11 @@
     ),
     date: "December 22, 2023",
     program: "BSc Computer Science",
+    department: "Electronics and Computer Science",
+    faculty: "Faculty of Engineering and Physical Sciences",
+    university: "University of Southampton",
     is_progress_report: false,
 ) = {
-  let body-font = "New Computer Modern"
-  let sans-font = "New Computer Modern Sans"
 
   set document(title: title, author: author.at("name"))
   set page(
@@ -179,9 +171,9 @@
 
   v(7em) 
   par()[
-      #text(14pt, "Electronics and Computer Science") \
-      #text(14pt, "Faculty of Engineering and Physical Sciences") \
-      #text(14pt, "University of Southampton")
+      #text(14pt, department) \
+      #text(14pt, faculty) \
+      #text(14pt, university)
   ]
 
   v(6.5em)
@@ -220,7 +212,6 @@
     #text(14pt, program)
   ]
 
-
 }
 
 #let abstract(
@@ -229,6 +220,9 @@
     email: none,
   ),
   program: "Program name",
+  department: "Electronics and Computer Science",
+  faculty: "Faculty of Engineering and Physical Sciences",
+  university: "University of Southampton",
   is_progress_report: false,
   content: lorem(150),
 ) = {
@@ -239,24 +233,22 @@
   counter(page).update(0)
 
   set align(center)
-  let body-font = "New Computer Modern"
-  let sans-font = "New Computer Modern Sans"
   set text(
       font: body-font, 
       size: 12pt, 
       lang: "en",
   )
 
   v(8.5em)
-  text("UNIVESITY OF SOUTHAMPTON")
+  text(upper(university))
 
   v(0.5em)
   underline(text("ABSTRACT"))
 
   v(0.5em)
   par()[
-    #text("FACULTY OF ENGINEERING AND PHYSICAL SCIENCES") \
-    #text("ELECTRONICS AND COMPUTER SCINCE")
+    #text(upper(faculty)) \
+    #text(upper(department))
   ]
 
   v(0.5em)
@@ -397,6 +389,9 @@
   ),
   date: "December 22, 2023",
   program: "BSc Computer Science",
+  department: "Electronics and Computer Science",
+  faculty: "Faculty of Engineering and Physical Sciences",
+  university: "University of Southampton",
   is_progress_report: false,
   originality_statements: (
     acknowledged: "I have acknowledged all sources, and identified any content taken from elsewhere.",
@@ -410,7 +405,6 @@
   acknowledgments_text: lorem(50),
   page_numbering: "1",
   title_numbering: "1.",
-
   doc
 ) = {
   cover(
@@ -420,12 +414,18 @@
     author: author,
     date: date,
     program: program,
+    department: department,
+    faculty: faculty,
+    university: university,
     is_progress_report: is_progress_report
   )
 
   abstract(
     author: author,
     program: program,
+    department: department,
+    faculty: faculty,
+    university: university,
     is_progress_report: is_progress_report,
     content: abstract_text
   )