Feat: Generate hash.json and split json folder; bump toolchain to nightly-2025-08-19

.github/gen_core.json.sh

@@ -4,7 +4,7 @@ set -o pipefail
 
 export WORKSPACE="${WORKSPACE:-$(pwd)}"
 
-export RUST_LOG=off
+export DV_LOG=off
 export OUTPUT_DIR=$WORKSPACE/assets
 export KANI_DIR=$WORKSPACE/kani/target/kani
 export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
@@ -13,7 +13,7 @@ export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
 # * update runid after verify-rust-std submodule syncs
 # * update snapshots after runid changes
 rm tmp -rf
-gh run download -D tmp -R model-checking/verify-rust-std 16777123952
+gh run download -D tmp -R model-checking/verify-rust-std 17086909032
 
 ls -alh $VERIFY_RUST_STD_LIBRARY
 

.github/install-kani.sh

@@ -1,20 +1,27 @@
-set -ex
+#!/usr/bin/bash
+set -exo pipefail
 
 # NOTE: verify-rust-std pins its kani commit, and
 # distributed-verification pins another.
 # So this means for verify-rust-std jobs,
 # distributed-verification may be broken to compile.
 git submodule update --init kani
 
+# Temporary patch to https://github.com/model-checking/kani/pull/4312
+cp .github/kani_contract_mode.patch kani
+
 # Install kani
 pushd kani
 git submodule update --init charon
 
+# Apply the patch
+git apply kani_contract_mode.patch
+
 ./scripts/setup/ubuntu/install_deps.sh
 cargo build-dev -- --release
 
 export PATH=$(pwd)/scripts:$PATH
-echo PATH=$PATH >>$GITHUB_ENV
+echo PATH="$PATH" >>"$GITHUB_ENV"
 kani --version
 
 popd

.github/kani_contract_mode.patch

@@ -0,0 +1,13 @@
+diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+index ed8bde7f8..d8f2eae87 100644
+--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
++++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+@@ -71,7 +71,7 @@ const fn kani_register_contract<T, F: FnOnce() -> T>(f: F) -> T {
+                 }
+                 // Dummy function that we replace to pick the contract mode.
+                 // By default, return ORIGINAL
+-                #[inline(never)]
++                #[inline]
+                 #[kanitool::fn_marker = "kani_contract_mode"]
+                 const fn kani_contract_mode() -> kani::internal::Mode {
+                     kani::internal::ORIGINAL

.github/workflows/test.yml

@@ -54,7 +54,7 @@ jobs:
         autoharness: ["", "-autoharness"]
     if: true
     env:
-      UNSTABLE_ARGS: -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts
+      UNSTABLE_ARGS: -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z stubbing
       AUTO: ${{ matrix.autoharness }}
     steps:
       - name: Remove unnecessary software to free up disk space

.gitignore

@@ -13,5 +13,6 @@ core.json
 *.sqlite3
 *.db
 *.diff
+*.log
 
 tmp/

Cargo.toml

@@ -17,13 +17,13 @@ eyre = "0.6"
 color-eyre = "0.6"
 
 # logger
+log = "0.4.27"
 tracing = "0.1"
 tracing-subscriber = { version = "0.3", features = ["env-filter"] }
 tracing-error = "0.2"
 
 # db
 rusqlite = { version = "0.36.0", features = ["bundled", "jiff"] }
-serde_rusqlite = "0.39.1"
 jiff = { version = "0.2", features = ["serde"] }
 
 [dev-dependencies]

assets/hash.sql

@@ -0,0 +1,30 @@
+-- sqlite3 ../artifacts/artifact-libcore/core.sqlite3 <hash.sql | jq -s '.' >../ui/verify-rust-std_data/hash.json
+WITH
+  df AS (
+    SELECT
+      file,
+      name,
+      proof_kind,
+      hash
+    FROM
+      db
+    ORDER BY
+      file,
+      name
+  )
+SELECT
+  JSON_PATCH (
+    '{}',
+    JSON_OBJECT (
+      'file',
+      file,
+      'name',
+      name,
+      'proof_kind',
+      proof_kind,
+      'hash',
+      hash
+    )
+  )
+FROM
+  df;

assets/split.sh

@@ -0,0 +1,35 @@
+#!/usr/bin/bash
+
+set -eou pipefail
+
+# Usage: sqlite.sh db-path sql-path
+# e.g. ./split.sh ../artifacts/artifact-libcore/core.sqlite3 split.sql ../tmp/json
+db=$1
+sql=$2
+base=$3
+
+echo "db=$db, sql=$sql, base=$base"
+
+# Let parallel use bash.
+export PARALLEL_SHELL=$(type -p bash)
+
+run() {
+  PREFIX=/home/runner/work/verify-rust-std/verify-rust-std/library/
+
+  # Read all arguments and JSON from stdin through parallel pipe.
+  while IFS=$'\t' read -r filename hash json; do
+    # $base is unavaible in parallel run, so pass it as env var.
+    json_folder="$BASE/${filename#"$PREFIX"}"
+    json_file="$json_folder/$hash.json"
+    echo "$json_file"
+    mkdir -p "$json_folder"
+    jq 'del(.[] | select(. == []))' <<<"$json" >"$json_file"
+  done
+}
+
+# Let parallel call the function.
+export -f run
+
+sqlite3 -batch "$db" -separator $'\t' <"$sql" |
+  parallel --colsep '\t' --pipe --progress --tagstring '[Job {#}]' \
+    "BASE=$base run"

assets/split.sql

@@ -0,0 +1,33 @@
+SELECT
+  file,
+  hash,
+  JSON_PATCH (
+    '{}',
+    JSON_OBJECT (
+      'file',
+      file,
+      'name',
+      name,
+      'hash',
+      hash,
+      'hash_direct',
+      hash_direct,
+      'inst_kind',
+      inst_kind,
+      'proof_kind',
+      proof_kind,
+      'attrs',
+      JSON (attrs),
+      'src',
+      src,
+      'macro_backtrace',
+      JSON (macro_backtrace),
+      'callees',
+      JSON (callees)
+    )
+  ) AS data
+FROM
+  db
+ORDER BY
+  file,
+  hash;

src/bin/distributed-verification/functions/cache/db.rs

@@ -1,46 +1,21 @@
 use super::Functions;
 use crate::Result;
-use distributed_verification::db::DbFunction;
+use distributed_verification::db::{
+    DbFunction,
+    sql::{SQL_CREATE, SQL_DROP, SQL_INSERT, SQL_VACUUM, db_file},
+};
 use eyre::{Context, ContextCompat};
 use rusqlite::{Connection, named_params};
 use serde_json::to_string_pretty;
 
-const DB_FILE: &str = "db.sqlite3";
-const SQL_DROP: &str = "DROP TABLE IF EXISTS db;";
-// cannot VACUUM from within a transaction
-const SQL_VACUUM: &str = "VACUUM;";
-const SQL_CREATE: &str = "\
-CREATE TABLE IF NOT EXISTS db (
-  file TEXT NOT NULL,
-  name TEXT NOT NULL,
-  hash TEXT NOT NULL PRIMARY KEY,
-  hash_direct TEXT NOT NULL,
-  inst_kind TEXT,
-  proof_kind TEXT,
-  attrs TEXT,
-  src TEXT,
-  macro_backtrace_len INTEGER,
-  macro_backtrace TEXT,
-  callees_len INTEGER,
-  callees TEXT
-) STRICT;
-";
-const SQL_INSERT: &str = "\
-INSERT INTO db (file, name, hash, hash_direct, inst_kind, proof_kind, attrs, src, macro_backtrace_len, macro_backtrace, callees_len, callees) 
-VALUES (:file, :name, :hash, :hash_direct, :inst_kind, :proof_kind, :attrs, :src, :macro_backtrace_len, :macro_backtrace, :callees_len, :callees)
-";
-
 pub struct Db {
     db: Connection,
 }
 
 impl Db {
     /// Create a timestamp.sqlite3 file and db table.
     pub fn new() -> Result<Db> {
-        const VAR_DB_FILE: &str = "DB_FILE";
-        let db_file = std::env::var(VAR_DB_FILE);
-        let db_file = db_file.as_deref().unwrap_or(DB_FILE);
-
+        let db_file = db_file();
         info!(db_file, "start sqlite db");
         let _span = error_span!("Db::new", db_file).entered();
         let db = Connection::open(db_file).context("Failed to open or create db file.")?;

src/bin/distributed-verification/functions/mod.rs

@@ -18,6 +18,7 @@ mod utils;
 pub fn analyze(tcx: TyCtxt) -> Vec<SerFunction> {
     let local_items = all_local_items();
     let cap = local_items.len();
+    dbg!(cap);
 
     let mut entries = Vec::with_capacity(cap);
 

src/bin/verify_rust_std/diff.rs

@@ -1,8 +1,10 @@
 use crate::{Result, read_json};
 use clap::Parser;
 use distributed_verification::diff::{MergeHashKaniList, diff};
+use distributed_verification::logger;
 
 pub fn run(args: &[String]) -> Result<()> {
+    logger::init();
     SubCmdDiff::parse_from(args).run()
 }
 

src/bin/verify_rust_std/main.rs

@@ -1,7 +1,6 @@
 //! `VERIFY_RUST_STD_LIBRARY=path/to/verify-rust-std/library` and
 //! `KANI_DIR=path/to/kani` should be set beforehand.
 
-use distributed_verification::logger;
 use eyre::{Context, Result};
 use std::process::{Command, Stdio};
 
@@ -17,46 +16,50 @@ mod diff;
 mod merge;
 
 fn main() -> Result<()> {
-    let mut args = std::env::args().collect::<Vec<_>>();
+    // arguments passed to rustc
+    let mut args = std::env::args().skip(1).collect::<Vec<_>>();
 
-    if args.len() == 2 && args[1].as_str() == "-vV" {
+    if args.as_slice() == ["-vv"] {
         // cargo invokes `rustc -vV` first
         run("rustc", &["-vV".to_owned()], &[])
     } else if env::is_wrapper() {
         // then cargo invokes `rustc - --crate-name ___ --print=file-names`
-        if args[1] == "-" {
+        if args[0] == "-" {
             // `rustc -` is a substitute file name from stdin
             // see https://rust-lang.zulipchat.com/#narrow/channel/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20What.20does.20.60rustc.20-.60do.3F/with/514494493
-            args[1] = "src/lib.rs".to_owned();
+            args[0] = "src/lib.rs".to_owned();
         }
 
-        let rustc_args = &args[1..];
         if args.iter().any(|arg| arg == "core") {
             let json = serde_json::json!({
-                "rustflags": &rustc_args,
-                "rustc": format!("rustc {}", rustc_args.join(" "))
+                "rustflags": &args,
+                "rustc": format!("rustc {}", args.join(" "))
             });
             ENV.write_rustflags_json(&json)?;
-            build_core(args.split_off(1))
+            build_core(args)
         } else {
             // build non-core crates
-            run("rustc", rustc_args, &[])
+            run("rustc", &args, &[])
+        }
+    } else if let Some(subcmd) = args.first() {
+        match subcmd.as_str() {
+            "merge" => merge::run(&args),
+            "diff" => diff::run(&args),
+            _ => run_cargo(),
         }
-    } else if args.get(1).map(|arg| arg == "merge").unwrap_or(false) {
-        logger::init();
-        merge::run(&args[1..])
-    } else if args.get(1).map(|arg| arg == "diff").unwrap_or(false) {
-        logger::init();
-        diff::run(&args[1..])
     } else {
-        run(
-            "cargo",
-            &["build", "-Zbuild-std=core"].map(String::from),
-            &[env::set_rustc_wrapper(), env::set_wrapper()],
-        )
+        run_cargo()
     }
 }
 
+fn run_cargo() -> std::result::Result<(), eyre::Error> {
+    run(
+        "cargo",
+        &["build", "-Zbuild-std=core"].map(String::from),
+        &[env::set_rustc_wrapper(), env::set_wrapper()],
+    )
+}
+
 fn run(cmd: &str, args: &[String], vars: &[(&str, &str)]) -> Result<()> {
     let library = &*ENV.VERIFY_RUST_STD_LIBRARY;
     let rustflags = &*ENV.CARGO_ENCODED_RUSTFLAGS;

src/bin/verify_rust_std/merge.rs

@@ -3,10 +3,12 @@ use clap::Parser;
 use distributed_verification::{
     SerFunction,
     diff::{KaniListJson, MergeHashKaniList},
+    logger,
 };
 use std::collections::HashMap;
 
 pub fn run(args: &[String]) -> Result<()> {
+    logger::init();
     SubCmdMerge::parse_from(args).run()
 }