Merge pull request #101 from os-checker/verify-rust-std

Feat: add and deploy UI for verify-rust-std (kani)

Author: zjp-CN

.github/workflows/doc.yml

@@ -2,46 +2,50 @@ name: Deploy Doc
 
 on:
   push:
-    branches: [ main ]
 
 jobs:
-  # Build job
   build:
     # Specify runner +  build & upload the static files as an artifact
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - name: Build static files
-        env:
-          CARGO_TERM_COLOR: always
-        run: |
-          cargo doc --document-private-items --no-deps
-
-      - name: Install rustc internal docs
-        run: |
-          rustup toolchain list -v
-          # Find toolchain path
-          export TOOLCHAIN=$(rustc --print sysroot)
-          echo "toolchain=\"$TOOLCHAIN\""
-          # Remove rustc book
-          rm $TOOLCHAIN/share/doc/rust/html/rustc -rf
-          # Download rustc API docs
-          rustup component add rustc-docs
-          # Move the docs to deployment path
-          mv $TOOLCHAIN/share/doc/rust/html/rustc target/doc/rustc
-
-      - name: Prepare index.html
-        run: |
-          # Find toolchain name
-          export toolchain=$(rustc --print sysroot | grep -oP "nightly-\d{4}-\d{2}-\d{2}")
-          echo "toolchain=\"$toolchain\""
-          # Fill in toolchain placeholder in index.html
-          sed "s/nightly-xxxx-xx-xx/$toolchain/" .github/index.html > target/doc/index.html
-
+      # - name: Build static files
+      #   env:
+      #     CARGO_TERM_COLOR: always
+      #   run: |
+      #     cargo doc --document-private-items --no-deps
+      #
+      # - name: Install rustc internal docs
+      #   run: |
+      #     rustup toolchain list -v
+      #     # Find toolchain path
+      #     export TOOLCHAIN=$(rustc --print sysroot)
+      #     echo "toolchain=\"$TOOLCHAIN\""
+      #     # Remove rustc book
+      #     rm $TOOLCHAIN/share/doc/rust/html/rustc -rf
+      #     # Download rustc API docs
+      #     rustup component add rustc-docs
+      #     # Move the docs to deployment path
+      #     mv $TOOLCHAIN/share/doc/rust/html/rustc target/doc/rustc
+      #
+      # - name: Prepare index.html
+      #   run: |
+      #     # Find toolchain name
+      #     export toolchain=$(rustc --print sysroot | grep -oP "nightly-\d{4}-\d{2}-\d{2}")
+      #     echo "toolchain=\"$toolchain\""
+      #     # Fill in toolchain placeholder in index.html
+      #     sed "s/nightly-xxxx-xx-xx/$toolchain/" .github/index.html > target/doc/index.html
+      #
+      # - name: Upload static files as artifact
+      #   uses: actions/upload-pages-artifact@v3 # or specific "vX.X.X" version tag for this action
+      #   with:
+      #     path: target/doc/
+      - name: Build UI
+        run: cd ui && npm i && NUXT_APP_BASE_URL=/distributed-verification/ npm run generate
       - name: Upload static files as artifact
-        uses: actions/upload-pages-artifact@v3 # or specific "vX.X.X" version tag for this action
+        uses: actions/upload-pages-artifact@v3
         with:
-          path: target/doc/
+          path: ui/.output/public/
 
   # Deployment job
   deploy:

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "verify-rust-std"]
 	path = verify-rust-std
 	url = https://github.com/model-checking/verify-rust-std.git
+[submodule "ui/verify-rust-std_data"]
+	path = ui/verify-rust-std_data
+	url = https://github.com/os-checker/verify-rust-std_data.git

src/bin/verify_rust_std/merge.rs

@@ -48,18 +48,23 @@ impl SubCmdMerge {
         for func in &mut hash_json {
             let file = func.file.strip_prefix(&self.strip_hash_json_prefix).unwrap_or(&func.file);
             let fn_name = &*func.name;
-            let value = &*func.hash;
+            let value = (&*func.hash, func.proof_kind);
             hash_map.insert((file, fn_name), value);
         }
 
         let cap = kani_list.totals.standard_harnesses + kani_list.totals.contract_harnesses;
         let mut v_merge = Vec::with_capacity(cap);
         for file_func in kani_list.file_func_name() {
             let (file, func) = file_func;
+            let (hash, proof_kind) = match hash_map.get(&file_func) {
+                Some((hash, proof_kind)) => (Some((*hash).into()), *proof_kind),
+                None => (None, None),
+            };
             v_merge.push(MergeHashKaniList {
                 file: file.into(),
                 func: func.into(),
-                hash: hash_map.get(&file_func).map(|s| (*s).into()),
+                hash,
+                proof_kind,
             });
         }
         v_merge.sort_unstable();

src/diff.rs

@@ -254,6 +254,9 @@ pub struct MergeHashKaniList {
     #[serde(skip_serializing_if = "Option::is_none")]
     #[serde(default)]
     pub hash: Option<Box<str>>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    #[serde(default)]
+    pub proof_kind: Option<ProofKind>,
 }
 
 /// Compare two `MergeHashKaniList`, and returns the ones from new that don't match the old,