From 4d880a296d0ba96c1f2850e27e4bf91232499e79 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Oct 2017 17:25:54 +0200
Subject: [PATCH] expand README
---
README.md | 86 +++++++++++++++++++++++++++++++++++++++++++++++++++++--
1 file changed, 83 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index fdceecb7..1d4259b8 100644
--- a/README.md
+++ b/README.md
@@ -32,8 +32,16 @@ CPU cores.
stuck.
* The folder [lifetime](theories/lifetime) proves the rules of the lifetime
logic, including derived constructions like (non-)atomic persistent borrows.
+ * The subfolder [model](theories/lifetime/model) proves the core rules, which
+ are then sealed behind a module signature in
+ [lifetime.v](theories/lifetime/lifetime.v).
* The folder [typing](theories/typing) defines the domain of semantic types,
interpretations of all the judgments, as well as proofs of all typing rules.
+ * [type.v](theories/typing/type.v) contains the definition of a semantic type.
+ * [programs.v](theories/typing/programs.v) defines the typing judgements for
+ instructions and function bodies.
+ * [soundness.v](theories/typing/soundness.v) contains the main soundness
+ theorem of the type system.
* The subfolder [examples](theories/typing/examples) shows how the examples
from the technical appendix can be type-checked in Coq.
* The subfolder [lib](theories/typing/lib) contains proofs of safety of some
@@ -42,10 +50,82 @@ CPU cores.
`thread::spawn`, `take_mut::take`, `alias::once` as well as converting `&&T`
to `&Box<T>`.
+## Where to Find the Proof Rules From the Paper
+
+### Type System Rules
+
+The files in [typing](theories/typing) prove semantic versions of the proof
+rules given in the paper. Notice that mutable borrows are called "unique
+borrows" in the Coq development.
+
+| Proof Rule | File | Lemma |
+|-----------------------|-----------------|-----------------------|
+| T-bor-lft (for shr) | shr_bor.v | shr_mono |
+| T-bor-lft (for mut) | uniq_bor.v | uniq_mono |
+| C-subtype | type_context.v | subtype_tctx_incl |
+| C-copy | type_context.v | copy_tctx_incl |
+| C-split-bor (for shr) | product_split.v | tctx_split_shr_prod2 |
+| C-split-bor (for mut) | product_split.v | tctx_split_uniq_prod2 |
+| C-share | borrow.v | tctx_share |
+| C-borrow | borrow.v | tctx_borrow |
+| C-reborrow | uniq_bor.v | tctx_reborrow_uniq |
+| Tread-own-copy | own.v | read_own_copy |
+| Tread-own-move | own.v | read_own_move |
+| Tread-bor (for shr) | shr_bor.v | read_shr |
+| Tread-bor (for mut) | uniq_bor.v | read_uniq |
+| Twrite-own | own.v | write_own |
+| Twrite-bor | uniq_bor.v | write_uniq |
+| S-num | int.v | type_int_instr |
+| S-nat-leq | int.v | type_le_instr |
+| S-new | own.v | type_new_instr |
+| S-delete | own.v | type_delete_instr |
+| S-deref | programs.v | type_deref_instr |
+| S-assign | programs.v | type_assign_instr |
+| F-consequence | programs.v | typed_body_mono |
+| F-let | programs.v | type_let' |
+| F-letcont | cont.v | type_cont |
+| F-jump | cont.v | type_jump |
+| F-newlft | programs.v | type_newlft |
+| F-endlft | programs.v | type_endlft |
+| F-call | function.v | type_call' |
+
+Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic. You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
+
+### Lifetime Logic Rules
+
+The files in [lifetime](theories/lifetime) prove the lifetime logic, with the
+core rules being proven in the [model](theories/lifetime/model) subfolder and
+then sealed behind a module signature in
+[lifetime.v](theories/lifetime/lifetime.v).
+
+
+| Proof Rule | File | Lemma |
+|-------------------|---------------------|----------------------|
+| LftL-begin | model/creation.v | lft_create |
+| LftL-tok-fract | model/primitive.v | lft_tok_fractional |
+| LftL-not-own-end | model/primitive.v | lft_tok_dead |
+| LftL-end-persist | model/definitions.v | lft_dead_persistent |
+| LftL-borrow | model/borrow.v | bor_create |
+| LftL-bor-split | model/bor_sep.v | bor_sep |
+| LftL-bor-acc | lifetime.v | bor_acc |
+| LftL-bor-shorten | model/primitive.v | bor_shorten |
+| LftL-incl-isect | model/primitive.v | lft_intersect_incl_l |
+| LftL-incl-glb | model/primitive.v | lft_incl_glb |
+| LftL-tok-inter | model/primitive.v | lft_tok_sep |
+| LftL-end-inter | model/primitive.v | lft_dead_or |
+| LftL-tok-unit | model/primitive.v | lft_tok_static |
+| LftL-end-unit | model/primitive.v | lft_dead_static |
+| LftL-reborrow | lifetime.v | rebor |
+| LftL-bor-fracture | frac_borrow.v | bor_fracture |
+| LftL-fract-acc | frac_borrow.v | frac_bor_atomic_acc |
+| LftL-bor-na | na_borrow.v | bor_na |
+| LftL-na-acc | na_borrow.v | na_bor_acc |
+
## For Developers: How to update the Iris dependency
* Do the change in Iris, push it.
-* In lambdaRust, change opam.pins to point to the new commit.
-* Run "make build-dep" (in lambdaRust) to install the new version of Iris.
-* You may have to do "make clean" as Coq will likely complain about .vo file
+* Wait for CI to publish a new Iris version on the opam archive.
+* In lambdaRust, change opam to depend on the new version.
+* Run `make build-dep` (in lambdaRust) to install the new version of Iris.
+* You may have to do `make clean` as Coq will likely complain about .vo file
mismatches.
--
GitLab