|
1 | | -# Loom: A Framework for Automated Generation of Foundational Multi-Modal Verifiers |
| 1 | +# Port of the Neem MRDT and CRDT Framework to Lean |
2 | 2 |
|
3 | | -`Loom` is a framework for producing foundational multi-modal verifiers. Main features are: |
| 3 | +The code is built on top of the [Loom](https://github.com/verse-lab/loom/tree/master) repository. Initially, Loom was used to prove the correctness directly, but eventually pure Lean was used since the structures being verified did not have mutability. Therefore, some proofs use Loom and some do not. |
4 | 4 |
|
5 | | -* Automated weakest precondition generation |
| 5 | +## Steps to run |
6 | 6 |
|
7 | | -* Executable semantics |
| 7 | +Clone this repository, and run `lake update` followed by `lake build`. Ensure that the Lean version in `lean-toolchain` stays at `v4.23.0`. The various proofs are in the [Neem](CaseStudies/Neem) directory. Click on each Lean file in VS code to run all the verification conditions. |
8 | 8 |
|
9 | | -* Non-Determenism semantics |
| 9 | +# Data structures implemented and description |
10 | 10 |
|
11 | | -* Ready-to-use sample verifiers for imperative code with automated and interactive proofs |
12 | | - |
13 | | -`Loom` is based on the monadic shallow embedding of an executable program semantics into Lean 4 theorem prover. |
14 | | - |
15 | | -For automated weakest precondition generation, `Loom` uses Monad Transformer Algebras. |
16 | | - |
17 | | -## Build and Dependencies |
18 | | - |
19 | | -To build the project run `lake build` command in terminal from project's root directory. |
20 | | - |
21 | | -`Loom` has the following dependencies: |
22 | | - |
23 | | -- [Lean 4](https://lean-lang.org/) - foundational program verifier in which the framework was implemented. Version 4.20 is required. |
24 | | - |
25 | | -- [Mathlib4](https://github.com/leanprover-community/mathlib4) - Mathlib4 library for Lean, provides necessarily theoretical foundations |
26 | | - |
27 | | -- [lean-auto](https://github.com/leanprover-community/lean-auto) - SMT backend for `Velvet`. |
28 | | -Note that as `lean-auto` depends on `cvc5` which is not available for native Windows, therefore `Velvet` won't work on native Windows as well, but `Loom` is still available (use `lake build Loom` for standalone build) |
29 | | - |
30 | | -You need `cvc5` to be on your PATH to run `Velvet` examples. |
31 | | - |
32 | | -## Navigation Guide |
33 | | - |
34 | | -The repository consists of 2 key parts: |
35 | | - |
36 | | - - `Loom`, the framework itself |
37 | | - |
38 | | - - `CaseStudies`, examples for deriving and using Program Verifiers powered by Loom |
39 | | - |
40 | | - ### `Loom` folder |
41 | | - |
42 | | -This folder contains the theoretical foundation of the framework: |
43 | | - |
44 | | -- typeclass definitions for Ordered Monad Algebras (`MAlgOrdered`) and Monad Transformer Algebras (`MAlgLift`) in `Loom/MonadAlgebras/Defs.lean` |
45 | | - |
46 | | -- instances of Monad Transformer Algebras for key monads with effect (`ExceptT`, `StateT`, `ReaderT`) in `Loom/MonadAlgebras/Instances` |
47 | | - |
48 | | -- `NonDetT/NonDetT'` definitions and Weakest Precondition generators for Monad Transformers with Non-Determenisms in `Loom/MonadAlgebras` |
49 | | - |
50 | | -- Weakest Precondition generation and theorems for it in `Loom/MonadAlgebras/WP` |
51 | | - |
52 | | -Also it provides ready-to-use macros for an imperative `WHILE`-like language. |
53 | | - |
54 | | -### `CaseStudies` folder |
55 | | - |
56 | | -This folder contains two framework examples powered by Loom: `Velvet` and `Cashmere`. |
57 | | - |
58 | | -- `Velvet` is a framework for Dafny-style specification and verification of imperative programs. |
59 | | - |
60 | | - Theory about separated proofs for termination and correctness in Velvet is in `CaseStudies/Velvet/VelvetTheory.lean`, |
61 | | - related example file is `CaseStudies/Velvet/VelvetExamples/Total_Partial_example.lean` |
62 | | - |
63 | | - Please refer to `CaseStudies/Velvet/velvet_documentation.md` for detailed documentation about Velvet. |
64 | | - |
65 | | -- `Cashmere` is a simple framework used to showcase variety of monadic effects `Loom` can provide. |
66 | | - |
67 | | - Theory about Incorrectness reasoning in Cashmere is located in `CaseStudies/Cashmere/CashmereTheory.lean`, |
68 | | - related example file is `CaseStudies/Cashmere/CashmereIncorrectnessLogic.lean` |
69 | | - |
70 | | -- Both of them are supplied with `loom_solver`, `loom_solve`, `loom_solve!` and `loom_solve?` tactics. |
71 | | - |
72 | | - `loom_solve` tactic produces goals for VCs (each one corresponds to a single `invariant`/`assert`/`ensures` annotation in the program) with human-readable hypotheses and tries to discharge them with `loom_solver`. |
73 | | - |
74 | | - `loom_solver` is a main tactic for discharging VCs. This tactic can be set by user with Lean `macro_rules`: |
75 | | - ```lean |
76 | | - macro_rules |
77 | | - | `(tactic|loom_solver) => `(tactic|aesop) |
78 | | - ``` |
79 | | -
|
80 | | - For `Velvet` it is `auto` tactic with hints for closing complex goals, for `Cashmere` it is `aesop` tactic with additional theorems for proof reconstruction. |
81 | | -
|
82 | | - `loom_solve!` tactic works similarly to `loom_solve`, but also highlights invariants and pre/post-conditions that were not proven by `loom_solver`. |
83 | | -
|
84 | | - `loom_solve?` tactic suggests a sequence of more low-level tactics to get the same result as `loom_solve`. |
85 | | -
|
86 | | -
|
87 | | -#### Full list of implemented examples |
88 | | -
|
89 | | -Examples are organized in directories by their verifier: |
90 | | -
|
91 | | -- `CaseStudies/Cashmere` - directory with examples from Section 2 of the paper |
92 | | - - `Cashmere.lean` - definition of the computational monad for `Cashmere` examples as well as correctness proofs for all case studies up to Section 2.6 |
93 | | -
|
94 | | - - `CashmereIncorrectnessLogic.lean` - example from 2.7: using Angelic Non-Determenism to prove that there exists a bug in a program |
95 | | -- `CaseStudies/Velvet/VelvetExamples` - directory with examples from Section 8 of the paper |
96 | | -
|
97 | | - - `Examples.lean` - basic Dafny-like examples (`insertionSort`, `squareRoot`) in `Velvet` with partial correctness semantics |
98 | | -
|
99 | | - - `Examples_Total.lean` - similar examples but in Total semantics, also contains a `cbrt` example for manual proof after SMT failure |
100 | | -
|
101 | | - - `Total_Partial_example.lean` - concluding functional correctness in total semantics from termination and functional correctness in partial semantics effortlessly for `insertionSort` |
102 | | - |
103 | | - - `SpMSpV_Example.lean` - proving sparse matrix multiplication algorithms mixing automated and interactive proof modes with "two-layered paradigm" |
| 11 | +TODO |
0 commit comments