From a0667458672b1c258b2a2c5a4e55cfe25deea36a Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Wed, 20 Apr 2022 03:00:26 +0900
Subject: [PATCH] Update README.md
---
README.md | 21 ++++++++++++++-------
1 file changed, 14 insertions(+), 7 deletions(-)
diff --git a/README.md b/README.md
index e13bd896..b27f3a3d 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,7 @@
# RustHornBelt COQ DEVELOPMENT
-This is the Coq development for "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code".
+This is the Coq development for "RustHornBelt: A Semantic Foundation for
+Functional Verification of Rust Programs with Unsafe Code".
## Prerequisites
@@ -28,6 +29,14 @@ To update, do `git pull`. After an update, the development may fail to compile
because of outdated dependencies. To fix that, please run `opam update`
followed by `make build-dep`.
+## Walkthrough
+
+We have a [walkthrough](walkthrough.md) of RustHornBelt's Coq mechanization.
+
+It explains in detail how to verify integer addition, model `Vec`, verify
+`Vec::new`, and verify `mem::swap` (featuring mutable borrows).
+It focuses on the things you need to know to extend our Coq mechanization.
+
## Structure
- The folder [util](theories/util) contains utility for basic concepts.
@@ -58,14 +67,12 @@ followed by `make build-dep`.
with unsafe code from the Rust standard library and some user crates.
Some libraries are not yet verified, being commented out in `_CoqProject`.
-## Where to Find the Proof Rules From the Paper
-
-The derived rules mentioned in the paper can be found [here](theories/typing/examples/derived_rules.v).
-
### Key Type-Spec Rules --- from the RustHornBelt Paper
-The following table contains the location of every rule mentioned in the RustHornBelt paper.
-The filenames are spread across `theories/typing/examples`, `theories/typing`, `theories/typing/lib` (and its subfolders), and `theories/prophecy`.
+The following table contains the location of every rule mentioned in the
+RustHornBelt paper.
+The filenames are spread across `theories/typing/examples`, `theories/typing`,
+`theories/typing/lib` (and its subfolders), and `theories/prophecy`.
| Proof Rule | File | Lemma |
| ------------------- | ----------------- | ------------------------ |
--
GitLab