Update logbook and readme

README.md

@@ -5,3 +5,51 @@
 - [Official RustLog website](https://rustlog.pages.dev)
 - [Presentations PDF directory](pres/pdf/)
 - [Logbook](logbook.md)
+- [Final report](report/main.pdf)
+
+## How to use RustLog
+
+RustLog is a formalization of the Polonius model checker. It is written in Prolog and the rules are available in the [prog.pl](prog.pl) file. To use RustLog, you need to install [SWI-Prolog](https://www.swi-prolog.org/). Then, you can load the rules in the Prolog interpreter with the following command:
+
+```bash
+swipl -s prog.pl -s liveness.pl
+```
+
+You can then use the predicates defined in the rules to check borrow validity.
+
+### Example
+
+Let's say we have the following program:
+
+```rust
+let mut x = 42;
+let y = &mut x;
+x = 13;
+y;
+```
+
+We can convert this code to Prolog syntax and use the rules to check the validity of the borrow:
+
+- First define the liveness of the variables in the `liveness.pl` file:
+  - `liveUntil(x, 3).`
+  - `liveUntil(y, 4).`
+- Then start the Prolog interpreter and load the rules and the liveness files:
+
+```bash
+swipl -s prog.pl -s liveness.pl
+```
+
+- Finally we can check the validity of the borrow with the `borrowChecker` predicate:
+
+```prolog
+borrowChecker([(1, let, mut, x, 42), (2, let, immut, y, mut, x), (3, x, 13), (4, y)], [], CF).
+```
+
+The prolog prompt will output the following:
+
+```prolog
+?- borrowChecker([(1, let, mut, x, 42), (2, let, immut, y, mut, x), (3, x, 13), (4, y)], [], CF).
+Conflict detected at line: 3
+Trying to borrow x as mut while it is borrowed as mut by y
+true.
+```

liveness.pl

+liveUntil(y, 4).
\ No newline at end of file

logbook.md

@@ -161,3 +161,22 @@ _Neither a borrower nor a lender be; For loan oft loses both itself and friend._
 - [Polonius blogpost](http://smallcultfollowing.com/babysteps/blog/2019/01/17/polonius-and-region-errors/)
 - [Polonius presentation](https://www.youtube.com/watch?v=_agDeiWek8w)
 - [Slides](https://nikomatsakis.github.io/rust-belt-rust-2019)
+
+## 2023-05-25
+
+### What we did
+
+- We met with Aurélien Coet to discuss about the project and the grammar and the semantic rules we wrote. He gave us some advices and we will try to implement them.
+
+Until this day we continued to write the semantic rules and the grammar of RustLog. We also started to write the code of the borrow checker.
+
+We also started to write the report.
+
+## 2023-06-05
+
+### What we did
+
+- Finalize the report
+- Finalize the code of the borrow checker
+- Prepare the presentation
+- Prepare the demo

report/main.tex

@@ -70,9 +70,9 @@
 
 \section{Introduction}
 
-The Rust programming language is renowned for its systems programming capabilities, enabling developers to write robust, efficient, and safe code. One of the key features of Rust is its innovative system for handling memory management and data race conditions, known as the borrow checker. This is where Polonius comes into play, as the latest development in the evolution of Rust's borrow checker.
+The Rust programming language is renowned for its systems programming capabilities, enabling developers to write robust, efficient, and safe code. One of the key features of Rust is its innovative system for handling memory management and data race conditions, known as the borrow checker. This is where Polonius \cite{polonius:blogpost} comes into play, as the latest development in the evolution of Rust's borrow checker.
 
-Our original plan was to formalize Polonius, the new borrow checker of Rust, focusing on the intricate rules that ensure safe memory accesses while avoiding data races and null pointer dereferencing. However, Polonius' intricate nature and the complexity of Rust as a whole presented an arduous task beyond the scope of our current capabilities.
+Our original plan was to formalize Polonius, the new borrow checker of Rust \cite{polonius:book}, focusing on the intricate rules that ensure safe memory accesses while avoiding data races and null pointer dereferencing \cite{polonius:talk}. However, Polonius' intricate nature and the complexity of Rust as a whole presented an arduous task beyond the scope of our current capabilities.
 
 With the complexity in mind, we decided to focus our efforts on formalizing a more simplified model. This model represents a small subset of Rust, a language that we will refer to as RustLog. Although this language does not include the entirety of Rust's complexities and features, it incorporates the fundamental aspects of Rust's borrow checker, creating a reasonable stepping stone towards understanding and eventually formalizing Polonius.
 

report/refs.bib

-@misc{enwiki:aes,
-  author       = {{Wikipedia contributors}},
-  title        = {Advanced Encryption Standard --- {Wikipedia}{,} The Free Encyclopedia},
-  year         = {2023},
-  howpublished = {\url{https://en.wikipedia.org/w/index.php?title=Advanced_Encryption_Standard&oldid=1154244401}},
-  note         = {[Online; accessed 16-May-2023]}
+@misc{polonius:blogpost,
+  author       = {{Niko Matsais}},
+  title        = {An alias-based formulation of the borrow checker},
+  year         = {2018},
+  howpublished = {\url{http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/#an-alias-based-formulation-of-the-borrow-checker}},
 }
 
-@misc{enwiki:block-cipher-mode,
-  author       = {{Wikipedia contributors}},
-  title        = {Block cipher mode of operation --- {Wikipedia}{,} The Free Encyclopedia},
-  year         = {2023},
-  howpublished = {\url{https://en.wikipedia.org/w/index.php?title=Block_cipher_mode_of_operation&oldid=1154901199}},
-  note         = {[Online; accessed 16-May-2023]}
+@misc{polonius:book,
+  author       = {Polonius Development Team},
+  howpublished = {\url{https://rust-lang.github.io/polonius/}},
+  title        = {Polonius Book},
 }
 
-@misc{flast101:poracle,
-  author       = {flast101},
-  title        = {Padding Oracle Attack Explained},
-  year         = {2020},
-  howpublished = {\url{https://flast101.github.io/padding-oracle-attack-explained/}}
-}
-
-@misc{enwiki:padding-oracle-attack,
-  author       = {{Wikipedia contributors}},
-  title        = {Padding oracle attack --- {Wikipedia}{,} The Free Encyclopedia},
-  year         = {2022},
-  howpublished = {\url{https://en.wikipedia.org/w/index.php?title=Padding_oracle_attack&oldid=1088720142}},
-  note         = {[Online; accessed 16-May-2023]}
-}
-
-@book{van2021hardware,
-  title     = {The Hardware Hacking Handbook: Breaking Embedded Security with Hardware Attacks},
-  author    = {van Woudenberg, J. and O'Flynn, C.},
-  isbn      = {9781593278748},
-  lccn      = {2021027424},
-  url       = {https://books.google.fr/books?id=DEqatAEACAAJ},
-  year      = {2021},
-  publisher = {No Starch Press}
+@misc{polonius:talk,
+  author       = {Niko Matsakis},
+  title        = {Polonius: Either Borrower or Lender Be, but Responsibly - Niko Matsakis},
+  year         = {2019},
+  howpublished = {\url{https://youtu.be/_agDeiWek8w}},
 }