Doc: add GSoC2025 final report

GSoC2025.md

@@ -0,0 +1,113 @@
+# Google Summer of Code 2025 Final Report
+
+## Goal
+
+The main goal it to implement [distributed and resource-efficient verification][proposal]
+for verify-rust-std project. That is to implement
+
+> A system that can reliably run all verification tasks within a time limit (where that
+> time limit needs to be determined empirically), and for changes that do not impact any
+> contract no actual verification tool is invoked.
+
+[proposal]: https://github.com/rust-lang/google-summer-of-code/tree/45141d74c28d91e114cf621d2d56aea6c3f82547?tab=readme-ov-file#distributed-and-resource-efficient-verification
+
+## What I did
+
+I developed a set of tools to achieve the goal with 600+ commits, 70 issues, and 57 PRs
+from April to October.
+
+The first is `distributed-verification`, which analyzes all kani proofs in the standard
+library. The tool traverses calls in each proof, and computes a direct hash value based on
+the source code, then computes an aggregated hash value through all the functions reached.
+
+The second is `verify_rust_std`, which compares two versions of proofs by their hash
+values, and emits the proofs whose hash has changed. Specifically, `kani-list.json`
+generated by `kani` and JSONs generated by `distributed-verification` are merged into a
+`hash.json` file as one version of proofs by `verify_rust_std merge` command. Then `kani`
+filters the exact differentiated proof names and executes verification on them.
+
+The third is a static [webpage][home] deployed on Github Pages, showing verification
+results in details and in a statistical chart. The data derive from `results.json` and 
+`core.sqlite3`, stored in another Github repo.
+
+<details>
+
+<summary>WebUI</summary>
+
+![](https://github.com/user-attachments/assets/d49e4bce-9ba8-4df0-8d9b-f85690ac0d8b)
+
+![](https://github.com/user-attachments/assets/e923bcda-9c9f-4c55-b915-0ee41bd9e870)
+
+</details>
+
+The CI workflow [verify-rust-std.yml] demonstrates that kani proofs are partitioned onto 8
+machines to be verified.
+
+The usage and explanations have been documented in the [README][dv] of the repo.
+
+[dv]: https://github.com/os-checker/distributed-verification
+[home]: https://os-checker.github.io/distributed-verification/
+[verify-rust-std.yml]: https://github.com/os-checker/distributed-verification/blob/95a4bfe47a769be6bf5d897b729f918c0e18fcd3/.github/workflows/verify-rust-std.yml
+
+## Comparision
+
+Here's a rough comparision on verification process and duration without cache.
+
+| Duration (min) | Parameters | dv (amd) | dv (arm) | v-r-s (no auto) | v-r-s (auto) |
+|----------------|------------|---------:|---------:|----------------:|-------------:|
+| (installation) | kani       |        5 |       12 |               5 |            5 |
+| (installation) | dv         |      0.5 |      0.5 |                 |              |
+| installation   | =          |      5.5 |     12.5 |               5 |            5 |
+| gen proof info |            |        2 |        2 |               6 |            4 |
+| (verify)       | partition  |        8 |        8 |               4 |            1 |
+| (verify)       | kani -j    |        3 |        3 |               4 |            3 |
+| (verify)       | runner     |       10 |        8 |              15 |           50 |
+| (verify)       | total      |      240 |      192 |             240 |          150 |
+| **runner**     |            |       18 |       23 |              26 |           59 |
+
+* dv (amd) shows that generating annotated proofs with distributed-verification and
+verifying them on 8 amd64 machines may take 18 minutes. There are two jobs: partition job
+and verification job. The first is installing dv and generating proof info in 2.5 minutes,
+while partitioning proofs and uploading proof info just happen in a second. The second is
+installing dv and kani, and running verifications in 15.5 minutes. Since verification job
+is done in parallel, it takes 18 minutes to see the complete CI finishes.
+* dv (arm) shows that the same process on arm64 as that on amd64, whereas it takes a bit
+longer time to install kani because solvers are installed from source code instead of 
+`apt install`. It's 2 minutes less in partition verifications than on amd64 machines.
+* v-r-s (no auto) shows that kani is installed in 5 minutes, generates kani-list.json in 6
+minutes, and verifies partitioned proofs in 15 minutes, thus total 26 minutes for each
+runner in the verify-rust-std repo.
+* v-r-s (auto) shows a total 59 minutes in the whole process without proofs partitioned
+onto other machines. It takes the longest runner time, while least total verification
+time for no reason from my understanding: it does more verification work, because
+autoharnesses are also verified.
+
+For partial or incremental verification, the minimal duration is 2.5 minutes on both amd64
+and arm64 when no code reached is modified, because only the first job needs doing. As
+the code is increasingly modified with regard to some proofs, the duration in the second
+job increases. As a result, distributed-verification saves 10 to 20 times as much time as 
+verify-rust-std CI currently takes.
+
+Note that a Rust toolchain bump always invalidates all the current proof hashes, thus
+fresh verifications will be performed in this case.
+
+<!-- 0.5+2+5.5+10=18  -->
+<!-- 0.5+2+12.5+8=23 -->
+<!-- 5+6+15=26 -->
+<!-- 5+4+50=59 -->
+
+## What's left to do
+
+Unfortunately, the incremental machanism is not fully applicapable to the verify-rust-std
+project untile the following problems are solved:
+* [Partitioned proof runners regularly receive shutdown or communication lost][#143]
+  * This indicates that some runners are impossible to finish jobs on their own.
+* [Untrustworthy outputs of multi-threaded verifications][#4438]
+  * This indicates that `results.json` are unsable to be trusted to merge, especially when
+  a failure happens.
+  * At present, the incremental verification workflow is quite incomplete for several
+  other reasons. 
+* ESBMC or other verification tools are not supported.
+
+[#143]: https://github.com/os-checker/distributed-verification/issues/143
+[#4438]: https://github.com/model-checking/kani/issues/4438