From 3b859531795e703c754de582118413fd9e733d94 Mon Sep 17 00:00:00 2001 From: GitHub Actions Date: Tue, 13 Feb 2024 14:34:06 +0000 Subject: [PATCH] Deploy verus-lang/blog to verus-lang/blog:gh-pages --- 404.html | 132 ++++++++++++++ announcements/blog/index.html | 148 ++++++++++++++++ authors/andrea-lattuada/index.html | 172 +++++++++++++++++++ authors/index.html | 135 +++++++++++++++ dark_mode.svg | 1 + index.html | 168 ++++++++++++++++++ light_mode.svg | 1 + main.css | 1 + robots.txt | 3 + sitemap.xml | 25 +++ verus-gentle-introduction/index.html | 248 +++++++++++++++++++++++++++ 11 files changed, 1034 insertions(+) create mode 100644 404.html create mode 100644 announcements/blog/index.html create mode 100644 authors/andrea-lattuada/index.html create mode 100644 authors/index.html create mode 100644 dark_mode.svg create mode 100644 index.html create mode 100644 light_mode.svg create mode 100644 main.css create mode 100644 robots.txt create mode 100644 sitemap.xml create mode 100644 verus-gentle-introduction/index.html diff --git a/404.html b/404.html new file mode 100644 index 0000000..b3316fe --- /dev/null +++ b/404.html @@ -0,0 +1,132 @@ + + + + + + + + + Verus blog + + + + + + + + + + +
+ +
+
+

+ Verus blog +

+

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

+

Verus is open-source at github.com/verus-lang/verus

+
+
+

Verus Announcements

+ + + +
+ 2024-02-13 We have a blog +
+ +
+
+
+
+ +
+
+ +
+
+

404: Page not found

+
+
+ Sorry, this page doesn't seem to exist. +
+
+ +
+
+

+ Powered by Zola, Theme Anpu (customized). +

+

+ + +

+
+
+
+ +
+ + +
+ + + + + + diff --git a/announcements/blog/index.html b/announcements/blog/index.html new file mode 100644 index 0000000..8ea954c --- /dev/null +++ b/announcements/blog/index.html @@ -0,0 +1,148 @@ + + + + + + + + + We have a blog + + + + + + + + + + +
+ +
+
+

+ Verus blog +

+

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

+

Verus is open-source at github.com/verus-lang/verus

+
+
+

Verus Announcements

+ + + +
+ 2024-02-13 We have a blog +
+ +
+
+
+
+ +
+
+ + +
+
+

We have a blog

+
+
+

This is a placeholder announcement.

+ +
+ + +
+ +
13 February 2024
+ +
+ + + +
+
+ +
+ + +
+
+

+ Powered by Zola, Theme Anpu (customized). +

+

+ + +

+
+
+
+ +
+ + +
+ + + + + + diff --git a/authors/andrea-lattuada/index.html b/authors/andrea-lattuada/index.html new file mode 100644 index 0000000..95ad6cf --- /dev/null +++ b/authors/andrea-lattuada/index.html @@ -0,0 +1,172 @@ + + + + + + + + + Andrea Lattuada + + + + + + + + + + +
+ +
+
+

+ Verus blog +

+

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

+

Verus is open-source at github.com/verus-lang/verus

+
+
+

Verus Announcements

+ + + +
+ 2024-02-13 We have a blog +
+ +
+
+
+
+ +
+
+ +

Author: Andrea Lattuada

+
+ To all authors +
+ + + +
+
+

+ A gentle introduction to checking code correctness in Verus +

+
+ + +
+ +

I'm going to talk about the tool we've been building, called Verus, which is a tool to verify Rust, and specifically to verify Rust code in the domain of system software: operating systems, file systems, things like that.

+ +
+ + + +
+ +
+ + Written by + + + + +
+
+ +
+ + + + +
+
+

+ Powered by Zola, Theme Anpu (customized). +

+

+ + +

+
+
+
+ +
+ + +
+ + + + + + diff --git a/authors/index.html b/authors/index.html new file mode 100644 index 0000000..9408aba --- /dev/null +++ b/authors/index.html @@ -0,0 +1,135 @@ + + + + + + + + + Authors + + + + + + + + + + +
+ +
+
+

+ Verus blog +

+

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

+

Verus is open-source at github.com/verus-lang/verus

+
+
+

Verus Announcements

+ + + +
+ 2024-02-13 We have a blog +
+ +
+
+
+
+ +
+
+ +

Authors

+ + + +
+
+

+ Powered by Zola, Theme Anpu (customized). +

+

+ + +

+
+
+
+ +
+ + +
+ + + + + + diff --git a/dark_mode.svg b/dark_mode.svg new file mode 100644 index 0000000..de44176 --- /dev/null +++ b/dark_mode.svg @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/index.html b/index.html new file mode 100644 index 0000000..5ef357f --- /dev/null +++ b/index.html @@ -0,0 +1,168 @@ + + + + + + + + + Verus blog + + + + + + + + + + +
+ +
+
+

+ Verus blog +

+

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

+

Verus is open-source at github.com/verus-lang/verus

+
+
+

Verus Announcements

+ + + +
+ 2024-02-13 We have a blog +
+ +
+
+
+
+ +
+
+ + + + +
+
+

+ A gentle introduction to checking code correctness in Verus +

+
+ + +
+ +

I'm going to talk about the tool we've been building, called Verus, which is a tool to verify Rust, and specifically to verify Rust code in the domain of system software: operating systems, file systems, things like that.

+ +
+ + + +
+ +
+ + Written by + + + + +
+
+ +
+ + + + +
+
+

+ Powered by Zola, Theme Anpu (customized). +

+

+ + +

+
+
+
+ +
+ + +
+ + + + + + diff --git a/light_mode.svg b/light_mode.svg new file mode 100644 index 0000000..34f0707 --- /dev/null +++ b/light_mode.svg @@ -0,0 +1 @@ +sun-warm \ No newline at end of file diff --git a/main.css b/main.css new file mode 100644 index 0000000..02472c3 --- /dev/null +++ b/main.css @@ -0,0 +1 @@ +@import url("https://fonts.googleapis.com/css?family=Montserrat&display=swap");@media (prefers-color-scheme: light){body{color:#222;background-color:#eee}body .secondary{color:gray}body a,body a:link,body a:visited{color:#3d3cba}body a:hover{color:#171746}body blockquote{border-left:2px solid gray}body code{background-color:#ddd}body pre code{background-color:rgba(0,0,0,0)}body .footnote-definition sup{color:gray}}@media (prefers-color-scheme: dark){body{color:#eee;background-color:#161616}body .secondary{color:#999}body a,body a:link,body a:visited{color:#959bf0}body a:hover{color:#c2c5f6}body blockquote{border-left:2px solid #999}body code{background-color:#444}body pre code{background-color:rgba(0,0,0,0)}body .footnote-definition sup{color:#999}}.dark-mode-buttons{position:absolute;top:1em;right:1em}.dark-mode-button{border:none;background-color:rgba(0,0,0,0)}.dark-mode-button:hover{cursor:pointer}body:not(.dark-mode){color:#222;background-color:#eee}body:not(.dark-mode) .secondary{color:gray}body:not(.dark-mode) a,body:not(.dark-mode) a:link,body:not(.dark-mode) a:visited{color:#3d3cba}body:not(.dark-mode) a:hover{color:#171746}body:not(.dark-mode) blockquote{border-left:2px solid gray}body:not(.dark-mode) code{background-color:#ddd}body:not(.dark-mode) pre code{background-color:rgba(0,0,0,0)}body:not(.dark-mode) .footnote-definition sup{color:gray}body:not(.dark-mode) #dark-mode-on{display:inline}body:not(.dark-mode) #dark-mode-off{display:none}body.dark-mode{color:#eee;background-color:#161616}body.dark-mode .secondary{color:#999}body.dark-mode a,body.dark-mode a:link,body.dark-mode a:visited{color:#959bf0}body.dark-mode a:hover{color:#c2c5f6}body.dark-mode blockquote{border-left:2px solid #999}body.dark-mode code{background-color:#444}body.dark-mode pre code{background-color:rgba(0,0,0,0)}body.dark-mode .footnote-definition sup{color:#999}body.dark-mode #dark-mode-on{display:none}body.dark-mode #dark-mode-off{display:inline}html{font-family:-apple-system,BlinkMacSystemFont,"Montserrat","Segoe UI",Roboto,Oxygen,Ubuntu,Cantarell,"Open Sans","Helvetica Neue",sans-serif;-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;}body{margin:0;background:#fff;color:#333;font-size:18px;line-height:1.5;-webkit-font-smoothing:antialiased}article,aside,details,figcaption,figure,footer,header,hgroup,main,menu,nav,section,summary{display:block}.container{max-width:42em;margin:0 auto}main{outline:none}h1{font-size:1.35em}h2{font-size:1.2em}h3{font-size:1.1em}a{color:#1d60a3;text-decoration:none}a:active,a:hover{outline:0}a:hover,a:focus{color:#a31d1d;border-bottom:1px solid rgba(163,29,29,.5)}a:active{color:#a31d1d;opacity:.9;border-bottom:1px solid rgba(163,29,29,.5)}a.active{color:#a31d1d}a.skip-main{left:-999px;position:absolute;top:auto;width:1px;height:1px;overflow:hidden;z-index:-999}a.skip-main:focus,a.skip-main:active{left:auto;top:0px;width:auto;height:auto;overflow:auto;z-index:999;padding:4px 6px 4px 6px;text-decoration:underline;border:none}.table-wrapper{overflow-x:auto}table{max-width:100%;border-spacing:0}thead{background:lightgrey}th,td{padding:.5em 1em;border:1px double lightgrey}pre{padding:1em;background-color:#f1f1f1;max-width:100%;overflow:auto}code,pre,kbd{font-family:monospace;font-size:.9em;line-height:154%}blockquote{border-left:2px solid #ccc;padding:.1em 1em;margin-left:.75em}p{margin-top:.5em;margin-bottom:.5em}hr{height:1px;border:0;border-top:1px solid #ccc}ul ol,ol ol,ul ul{margin:0em 2em}header{display:flex;justify-content:space-between}header h1{font-size:1em;margin-top:1em;margin-bottom:0;font-weight:normal}header h2{font-size:1em;margin:0;font-weight:normal}header nav{margin-top:1em;max-width:100%;text-align:right;margin-bottom:1em}header nav a{margin-left:2em}header a{color:#333}.site-header{white-space:nowrap}main h1{margin-top:1em;font-weight:normal;line-height:1.1em;margin-bottom:.5em;font-weight:600}.post-short-list:first-of-type{margin-top:1em}article:not(:last-of-type){border-bottom:thin solid #f1f1f1;padding-bottom:2em}article header h1{font-size:1.35em;line-height:1.1em;margin-bottom:.5em;font-weight:600}article header h1 a{border:none;text-decoration:none;color:#333}.article-info{font-size:.75em;color:grey;margin-top:1em}.article-info a{color:grey}.article-info a:hover{color:#a31d1d}.post-short-list .article-info{margin-top:0;margin-bottom:1.5em}.article-taxonomies{display:inline}.article-date{white-space:nowrap}.article-categories{display:inline;list-style-type:none;padding:0}.article-categories li{display:inline;margin-right:1em}.article-tags{display:inline;list-style-type:none;padding:0;margin:0}.article-tags li{display:inline;margin-right:1em}article img{max-width:100%;display:block;height:auto;margin:0 auto .5em}.read-more{font-size:.85em}.divider{display:block;height:1px;border:0;border-top:thin solid #f1f1f1;width:25%;margin:1em auto}.post-summary{margin-top:.5em;display:block}.post-summary>p{display:block}.terms{list-style-type:none;padding:0;line-height:2em}.pagination{display:flex;justify-content:space-between;margin-top:3em}.pagination{text-align:center}.pagination-item{background:#fafafa;padding:.75em .75em}.disabled{visibility:hidden}.pagination-item a{color:#333}.pagination-item a:hover,.pagination-item a:focus{color:#a31d1d;border-bottom:0}footer{border-top:thin solid #f1f1f1;margin-top:3em;font-size:16px}ul.language-select{padding-left:0;list-style:none;display:flex}ul.language-select>li{margin-right:1em}@media (max-width: 840px){.main-wrapper{margin:0;max-width:none;overflow-x:hidden;padding-left:25px;padding-right:25px}.container{max-width:90%;margin:0 auto}.pagination-item{padding:.5em .5em;font-size:14px}header{display:block}.site-header{text-align:center}header nav{margin-top:1em;max-width:100%;text-align:center;padding:.5em 0}header nav a:first-of-type{margin-left:0}header nav a{margin-left:5%}}.container{margin-top:20px}.site-header{font-size:2em}.powered-by-footer{font-size:80%}.flex-container{display:flex;justify-content:flex-start;align-items:flex-start}.container{max-width:42em;margin:inherit;margin-right:40px}.left-float{display:flex;flex-direction:column;flex-shrink:0;margin-left:20px;margin-right:20px;width:260px;padding:0px 20px 20px 20px}.left-header{font-size:70%}.article-authors{display:inline;list-style-type:none;padding:0}.article-authors li{display:inline;margin-right:1em}.article-info{font-size:.9em;color:grey;margin-top:1em}.left-announcements>h2{margin-bottom:2px}.left-announcement-item{margin-bottom:8px}.left-announcement-date{font-size:80%;display:block;margin-bottom:0px}@media (max-width: 840px){.main-wrapper{margin:0;max-width:none;overflow-x:hidden;padding-left:25px;padding-right:25px}.flex-container{display:flex;flex-direction:column}.container{max-width:inherit;margin:inherit;margin-right:inherit}.pagination-item{padding:.5em .5em;font-size:14px}header{display:inherit}.site-header{text-align:inherit}header nav{margin-top:inherit;max-width:inherit;text-align:inherit;padding:inherit}header nav a:first-of-type{margin-left:inherit}header nav a{margin-left:inherit}}@media (max-width: 72em){.flex-container{display:flex;flex-direction:column}.container{margin-left:20px;margin-right:20px}.left-float{display:flex;flex-direction:row;width:auto;margin-left:0px}.left-header{width:260px;flex-shrink:0}}@media (min-width: 641px) and (max-width: 72em){.left-announcements{margin-left:20px}}@media (max-width: 640px){.left-announcements{display:none}}pre{background-color:inherit;padding:1rem;overflow:auto}pre[data-linenos]{padding:1rem 0}pre table td{padding:0;border-style:hidden}pre table td:nth-of-type(1){text-align:center;user-select:none}pre mark{display:block;background-color:rgba(254,252,232,.9)}pre table{width:100%;border-collapse:collapse}code,pre,kbd{font-family:monospace;font-size:.9em;line-height:120%}.ansi-html{color:#fff;background-color:#2b2c2f} \ No newline at end of file diff --git a/robots.txt b/robots.txt new file mode 100644 index 0000000..f68294f --- /dev/null +++ b/robots.txt @@ -0,0 +1,3 @@ +User-agent: * +Disallow: / +Allow: diff --git a/sitemap.xml b/sitemap.xml new file mode 100644 index 0000000..ca5bf34 --- /dev/null +++ b/sitemap.xml @@ -0,0 +1,25 @@ + + + + https://verus-lang.github.io/blog/ + + + https://verus-lang.github.io/blog/announcements/blog/ + 2024-02-13 + + + https://verus-lang.github.io/blog/authors/ + + + https://verus-lang.github.io/blog/authors/andrea-lattuada/ + + + https://verus-lang.github.io/blog/categories/ + + + https://verus-lang.github.io/blog/tags/ + + + https://verus-lang.github.io/blog/verus-gentle-introduction/ + + diff --git a/verus-gentle-introduction/index.html b/verus-gentle-introduction/index.html new file mode 100644 index 0000000..167e017 --- /dev/null +++ b/verus-gentle-introduction/index.html @@ -0,0 +1,248 @@ + + + + + + + + + A gentle introduction to checking code correctness in Verus + + + + + + + + + + +
+ +
+
+

+ Verus blog +

+

Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.

+

Verus is open-source at github.com/verus-lang/verus

+
+
+

Verus Announcements

+ + + +
+ 2024-02-13 We have a blog +
+ +
+
+
+
+ +
+
+ + +
+
+

A gentle introduction to checking code correctness in Verus

+
+
+ +

I'm going to talk about the tool we've been building, called Verus, which is a tool to verify Rust, and specifically to verify Rust code in the domain of system software: operating systems, file systems, things like that.

+ +

This post is based, in part, on the talk "Verified Rust for low-level systems code - Rust Zürisee June 2023".

+

Checking code correctness with testing

+

Instead of trying to explain what verification is, I'm just going to jump into an example. You're writing a very simple max function here. What you might do is try to write a test for it.

+
1fn max(a: u64, b: u64) -> u64 {
+
2    if a >= b { b } else { a }
+
3}
+
4
+
5fn max_test_1() {
+
6    let x = 4;
+
7    let y = 4;
+
8    let ret = max(x, y);
+
9    assert!(ret == 4);
+
10}
+
11
+
12fn main() {
+
13    max_test_1();
+
14    println!("success");
+
15}
+
+

I'm keeping things extremely simple here, just writing a simple test. We have a max function, we call it with certain arguments, and check that the result is the one we expect. If we run this program, it passes. We wrote a test, it passes, we're happy.

+

You may have already spotted the problem here. Two problems, in fact: there's a bug, but also that the test case I wrote was insufficient. It was testing a very specific case and didn't catch the "edge" case. You could go and write another test and run it, and now finally, we get the test failing because we swapped DNA over here.

+
1fn max_test_2() {
+
2    let x = 4;
+
3    let y = 3;
+
4    let ret = max(x, y);
+
5    assert_eq!(ret, 4);
+
6}
+
7
+
8fn main() {
+
9    max_test_1();
+
10    max_test_2();
+
11    println!("success");
+
12}
+
+

That's how test-based development works, and it can work well. One needs to pay attention that the tests they write will catch edge cases or unexpected behavior. Let's see if we can do better: the way I'm writing this next test is a bit different. Instead of writing the return value that we expect exactly, I'm stating the property I want the return value to have.

+
1fn max_test_3() {
+
2    let x = 4;
+
3    let y = 3;
+
4    let ret = max(x, y);
+
5    assert!(ret == x || ret == y);
+
6    assert!(ret >= x && ret >= y);
+
7}
+
8
+
9fn main() {
+
10    max_test_3();
+
11    println!("success");
+
12}
+
+

I'm saying the return value here should be either of the two arguments and should be the greater one of the two. In this test we would fail the assertion on line 6, because max is not returning the maximum.

+

When writing tests you have to write a test case for each point in the input space of this function, but you never really know that you've caught all the possible issues and bugs because you can't possibly test for all the cases.

+

From tests to formal specifications

+

To use our tool, Verus, we need to re-organize the code a bit.

+
1use vstd::prelude::*;
+
2verus! {
+
3
+
4fn max(a: u64, b: u64) -> u64 {
+
5    if a >= b { a } else { b }
+
6}
+
7
+
8fn max_test() {
+
9    let x = 4;
+
10    let y = 3;
+
11    let ret = max(x, y);
+
12    assert(ret == x || ret == y);
+
13    assert(ret >= x && ret >= y);
+
14}
+
15
+
16} // verus!
+
+

I took the max function from before, fixed the issue, and then wrote Verus assertions as part of the max_test functions (on lines 12 and 13): these look different from regular rust assertion but I'm keeping the property that we wanted: the return value is either of the inputs and it is greater or equal to both.

+
error: assertion failed
+  --> /Users/andreal1/Demo/A2-program-0.rs:13:12
+   |
+13 |     assert(ret == x || ret == y);
+   |            ^^^^^^^^^^^^^^^^^^^^ assertion failed
+
+error: assertion failed
+  --> /Users/andreal1/Demo/A2-program-0.rs:14:12
+   |
+14 |     assert(ret >= x && ret >= y);
+   |            ^^^^^^^^^^^^^^^^^^^^ assertion failed
+
+error: aborting due to 2 previous errors
+
+verification results:: 1 verified, 1 errors
+
+

The error message we get from Verus is different; it's not a panic. We actually never run the code here. What Verus does is it statically checks every possible way that the program could run and checks whether these assertions are true in every possible case.

+

...

+ +
+ + +
+ +
+ + Written by + + + + +
+
+ +
+ + +
+
+

+ Powered by Zola, Theme Anpu (customized). +

+

+ + +

+
+
+
+ +
+ + +
+ + + + + +