Feature/eng 452 remove functions to trackcsv

.github/workflows/docker-publish.yml

@@ -5,7 +5,7 @@ on:
     paths:
       - 'Dockerfile'
       - '.github/workflows/docker-publish.yml'
-    branches: [ "main" ]
+    branches: [ "master" ]
     tags: [ 'docker-v*' ]
   workflow_dispatch:
 
@@ -56,6 +56,8 @@ jobs:
           context: .
           platforms: linux/amd64
           push: ${{ github.event_name != 'pull_request' }}
+          build-args: |
+             CACHEBUST=${{ github.run_id }}
           tags: ${{ steps.meta.outputs.tags }}
           labels: ${{ steps.meta.outputs.labels }}
           cache-from: type=gha

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "verilib-cli"
-version = "0.1.9"
+version = "0.2.0-beta.1"
 edition = "2021"
 description = "A command-line tool for managing Verilib repositories and API interactions"
 homepage = "https://github.com/Beneficial-AI-Foundation/verilib-cli"

Dockerfile

@@ -26,11 +26,18 @@ RUN echo "n" | python3 verus_analyzer_installer.py
 RUN echo "n" | python3 scip_installer.py
 
 WORKDIR /build
+ARG CACHEBUST=1
 RUN git clone https://github.com/Beneficial-AI-Foundation/probe-verus.git
 
 WORKDIR /build/probe-verus
 RUN cargo install --path .
 
+# Download scripts
+WORKDIR /build
+RUN git clone https://github.com/Beneficial-AI-Foundation/dalek-lite.git /build/dalek-lite && \
+    cd /build/dalek-lite && \
+    git checkout c36b395aa5526af7940d1db0f66ea60db4e3a157
+
 FROM --platform=linux/amd64 rust:slim-bookworm AS runtime
 
 RUN apt-get update && apt-get install -y \
@@ -41,6 +48,9 @@ RUN apt-get update && apt-get install -y \
     python3-requests \
     && rm -rf /var/lib/apt/lists/*
 
+# Install uv python package manager
+RUN pip3 install uv --break-system-packages
+
 # Install specific Rust toolchain for Verus
 RUN rustup toolchain install 1.93.0
 
@@ -64,8 +74,22 @@ ENV PATH="/usr/local/verus-analyzer:${PATH}"
 COPY --from=builder /root/scip /usr/local/scip
 ENV PATH="/usr/local/scip:${PATH}"
 
+# Copy scripts from builder
+COPY --from=builder /build/dalek-lite/scripts /usr/local/bin/scripts
+ENV PATH="/usr/local/bin/scripts:${PATH}"
+
+# Add local analysis script override
+COPY scripts/analyze_verus_specs_proofs.py /usr/local/bin/scripts/analyze_verus_specs_proofs.py
+
+# Patch script to allow REPO_ROOT env var and generic crate name
+RUN sed -i 's|repo_root = script_dir.parent|import os; repo_root = Path(os.environ.get("REPO_ROOT", script_dir.parent))|' /usr/local/bin/scripts/analyze_verus_specs_proofs.py && \
+    sed -i 's|CRATE_NAME = "curve25519_dalek"|import os; CRATE_NAME = os.environ.get("CRATE_NAME", "curve25519_dalek")|' /usr/local/bin/scripts/analyze_verus_specs_proofs.py && \
+    sed -i 's|CRATE_DIR = "curve25519-dalek"|CRATE_DIR = os.environ.get("CRATE_DIR", "curve25519-dalek")|' /usr/local/bin/scripts/analyze_verus_specs_proofs.py && \
+    sed -i 's|skip_parts = {"curve25519-dalek", "src"}|skip_parts = {CRATE_DIR, "src"}|' /usr/local/bin/scripts/analyze_verus_specs_proofs.py && \
+    sed -i 's|module_stripped = module.replace(f"{CRATE_NAME}::", "")|module_stripped = module.replace(f"{CRATE_NAME}::", "")|' /usr/local/bin/scripts/analyze_verus_specs_proofs.py
+
 # Ensure permissions for copied tools
-RUN chmod -R a+rx /usr/local/verus /usr/local/verus-analyzer /usr/local/scip
+RUN chmod -R a+rx /usr/local/verus /usr/local/verus-analyzer /usr/local/scip /usr/local/bin/scripts
 
 # Setup workspace
 WORKDIR /workspace

README.md

@@ -16,6 +16,25 @@ A command-line tool for managing Verilib repositories, verification structure fi
 1.  **Docker (Recommended)**: Runs `probe-verus` in a container with all dependencies pre-installed. This ensures a consistent environment and avoids local setup issues. You simply need Docker installed and running.
 2.  **Local**: Runs `probe-verus` directly on your host machine. This requires you to install `probe-verus` and all its dependencies (Rust, Verus, etc.) manually.
 
+### Using a Local Docker Image
+
+If you want to use a locally built Docker image instead of pulling from the registry (e.g., for development or custom modifications), follow these steps:
+
+1.  **Build the Docker image locally:**
+    ```bash
+    docker build --build-arg CACHEBUST=$(date +%s) -t verilib-cli:local .
+    ```
+
+2.  **Update your configuration:**
+    Edit `.verilib/config.json` in your project root and set the `docker-image` field:
+    ```json
+    {
+      "execution-mode": "docker",
+      "docker-image": "verilib-cli:local",
+      ...
+    }
+    ```
+
 During initialization (`verilib-cli init`), you will be prompted to choose your preferred execution mode. You can also change it later by editing the `.verilib/config.json` file.
 
 > **Note for Local Mode:** If you choose to run locally and encounter issues with missing dependencies or environment configuration, please refer to the [probe-verus repository](https://github.com/Beneficial-AI-Foundation/probe-verus) for installation instructions and troubleshooting.
@@ -214,11 +233,9 @@ verilib-cli create --root custom/path
 |--------|-------------|
 | `--root <path>` | Custom structure root (default: `.verilib/structure`) |
 
-**Requirements:**
-- `scripts/analyze_verus_specs_proofs.py` script
-
 **Optional:**
-- `functions_to_track.csv` in project root — when absent, a minimal seed is used
+- `scripts/analyze_verus_specs_proofs.py` — when present (in project or bundled), generates structure files; when absent, create still runs and sets up config with no structure files
+- `functions_to_track.csv` in project root — when absent, all functions are tracked by default (when script runs)
 
 ### `atomize`
 Enrich structure files with metadata from SCIP atoms.

functions_to_track.csv

@@ -0,0 +1,136 @@
+function,module,impl_block
+parse,verilib-cli::structure::frontmatter,
+FileStorage::delete_password,verilib-cli::storage::file,
+create_repo_from_git_url,verilib-cli::commands::init,
+handle_create,verilib-cli::commands::create,
+save_config_from_response,verilib-cli::commands::deploy,
+fetch_verifier_versions,verilib-cli::commands::deploy,
+load_proofs_from_file,verilib-cli::commands::verify,
+run_analyze_verus_specs_proofs,verilib-cli::commands::create,
+cleanup_intermediate_files,verilib-cli::structure::probe,
+run_command,verilib-cli::structure::utils,
+generate_stubs,verilib-cli::commands::atomize,
+FileStorage::set_password,verilib-cli::storage::file,
+generate_probe_atoms,verilib-cli::commands::atomize,
+handle_list,verilib-cli::commands::api,
+get_credential_storage,verilib-cli::storage,
+StructureConfig::save,verilib-cli::structure::config,
+get_display_name,verilib-cli::structure::utils,
+update_structure_files,verilib-cli::commands::atomize,
+disambiguate_names,verilib-cli::commands::create,
+collect_certifications,verilib-cli::commands::specify,
+test_specify_check_only_reports_uncertified,verilib-cli::specify_tests,
+handle_batch,verilib-cli::commands::api,
+run_local,verilib-cli::structure::executor,
+require_probe_installed,verilib-cli::structure::probe,
+test_atomize_check_only_passes_when_stubs_match,verilib-cli::atomize_tests,
+enrich_stubs,verilib-cli::commands::atomize,
+write,verilib-cli::structure::frontmatter,
+check_stubs_match,verilib-cli::commands::atomize,
+check_admin_status,verilib-cli::commands::api,
+handle_api_error,verilib-cli::download::error,
+resolve_code_name_and_atom,verilib-cli::commands::atomize,
+load_atoms_from_file,verilib-cli::commands::atomize,
+print_platform_help,verilib-cli::storage,
+test_specify_no_probe_loads_specs_from_file,verilib-cli::specify_tests,
+test_commands_create_default_config_when_missing,verilib-cli::error_handling_tests,
+test_atomize_update_stubs_updates_md_files,verilib-cli::atomize_tests,
+tracked_to_structure,verilib-cli::commands::create,
+wait_for_atomization,verilib-cli::download::client,
+build_enriched_entry,verilib-cli::commands::atomize,
+is_git_available,verilib-cli::commands::reclone,
+get_platform_info,verilib-cli::storage,
+run_command,verilib-cli::structure::executor,
+ConfigPaths::load,verilib-cli::structure::config,
+FileStorage::ensure_secure_file,verilib-cli::storage::file,
+StructureConfig::new,verilib-cli::structure::config,
+test_api_key_validation,verilib-cli::tests,
+read_repo_id_from_config,verilib-cli::commands::deploy,
+run_docker,verilib-cli::structure::executor,
+update_stubs_with_verification,verilib-cli::commands::verify,
+incorporate_spec_text,verilib-cli::commands::specify,
+default_docker_image,verilib-cli::structure::executor,
+test_verify_updates_stubs_with_verification_status,verilib-cli::verify_tests,
+prompt_type,verilib-cli::commands::deploy,
+encode_name,verilib-cli::structure::certs,
+StorageType::should_use_file_storage,verilib-cli::storage::types,
+handle_reclone,verilib-cli::commands::reclone,
+validate_meta_file,verilib-cli::commands::api,
+write_stubs_json,verilib-cli::commands::specify,
+prompt_execution_mode,verilib-cli::commands::init,
+handle_set,verilib-cli::commands::api,
+init_required_msg,verilib-cli::constants,
+generate_structure_files,verilib-cli::commands::create,
+has_uncommitted_changes,verilib-cli::commands::reclone,
+test_verify_fails_without_stubs_json,verilib-cli::error_handling_tests,
+test_specify_check_only_passes_when_all_certified,verilib-cli::specify_tests,
+run_probe_specify,verilib-cli::commands::specify,
+StorageType::from_env,verilib-cli::storage::types,
+test_verify_check_only_detects_failures,verilib-cli::verify_tests,
+parse_github_link,verilib-cli::structure::utils,
+test_verify_no_probe_loads_proofs_from_file,verilib-cli::verify_tests,
+handle_api,verilib-cli::commands::api,
+test_atomize_no_probe_loads_atoms_from_file,verilib-cli::atomize_tests,
+check_all_certified,verilib-cli::commands::specify,
+handle_init,verilib-cli::commands::init,
+prompt_language,verilib-cli::commands::deploy,
+handle_get,verilib-cli::commands::api,
+save_config,verilib-cli::commands::init,
+update_stubs_specification_status,verilib-cli::commands::specify,
+CredentialStorageFactory::create,verilib-cli::CredentialStorageFactory<Result<Box<dyn::storage::factory,
+test_atomize_check_only_fails_when_stubs_mismatch,verilib-cli::atomize_tests,
+collect_deploy_info_with_path,verilib-cli::commands::deploy,
+ensure_image_pulled,verilib-cli::structure::executor,
+prompt_summary,verilib-cli::commands::deploy,
+resolve_file_path,verilib-cli::commands::api,
+detect_language_in_path,verilib-cli::commands::deploy,
+test_specify_no_probe_fails_without_specs_json,verilib-cli::specify_tests,
+handle_atomize,verilib-cli::commands::atomize,
+test_create_creates_config_and_verilib_dir,verilib-cli::create_tests,
+decode_name,verilib-cli::structure::certs,
+normalize_git_url,verilib-cli::commands::init,
+check_for_failures,verilib-cli::commands::verify,
+format_value,verilib-cli::structure::frontmatter,
+print_verification_summary,verilib-cli::commands::verify,
+get_existing_certs,verilib-cli::structure::certs,
+FileStorage::get_password,verilib-cli::storage::file,
+has_md_files,verilib-cli::commands::atomize,
+deserialize_layouts,verilib-cli::download::types,
+test_verify_check_only_passes_when_no_failures,verilib-cli::verify_tests,
+handle_verify,verilib-cli::commands::verify,
+create_cert,verilib-cli::structure::certs,
+read_stubs_json,verilib-cli::commands::specify,
+lookup_code_name,verilib-cli::commands::atomize,
+handle_specify,verilib-cli::commands::specify,
+detect_git_url,verilib-cli::commands::init,
+prompt_git_url,verilib-cli::commands::init,
+read_tracked_csv,verilib-cli::commands::create,
+FileStorage::new,verilib-cli::storage::file,
+handle_auth,verilib-cli::commands::auth,
+test_atomize_enriches_stubs_json,verilib-cli::atomize_tests,
+handle_deploy,verilib-cli::commands::deploy,
+display_menu,verilib-cli::structure::utils,
+collect_deploy_info,verilib-cli::commands::deploy,
+has_unpushed_commits,verilib-cli::commands::reclone,
+get_stored_api_key,verilib-cli::commands::status,
+handle_create_file,verilib-cli::commands::api,
+create_gitignore,verilib-cli::structure::config,
+build_tree,verilib-cli::commands::deploy,
+default_docker_image,verilib-cli::structure::config,
+CommandConfig::default,verilib-cli::structure::executor,
+CredentialStorageFactory::create_with_type,verilib-cli::storage::factory,
+test_create_tracks_all_functions_without_functions_to_track_csv,verilib-cli::create_tests,
+prompt_description,verilib-cli::commands::deploy,
+ExecutionMode::default,verilib-cli::structure::executor,
+build_layouts,verilib-cli::commands::deploy,
+find_uncertified_functions,verilib-cli::commands::specify,
+load_specs_from_file,verilib-cli::commands::specify,
+generate_functions_to_track_csv,verilib-cli::commands::create,
+handle_status,verilib-cli::commands::status,
+run_probe_verify,verilib-cli::commands::verify,
+auth_required_msg,verilib-cli::constants,
+test_verify_no_probe_fails_without_proofs_json,verilib-cli::verify_tests,
+build_line_index,verilib-cli::commands::atomize,
+find_files_with_extension,verilib-cli::commands::deploy,
+download_repo,verilib-cli::download::client,
+test_atomize_no_probe_fails_without_atoms_json,verilib-cli::atomize_tests,

src/commands/atomize.rs

@@ -72,18 +72,35 @@ pub async fn handle_atomize(
     Ok(())
 }
 
+/// Check if structure has any .md files (recursively).
+fn has_md_files(structure_root: &Path) -> bool {
+    walkdir::WalkDir::new(structure_root)
+        .into_iter()
+        .filter_map(|e| e.ok())
+        .any(|e| e.path().extension().map_or(false, |ext| ext == "md"))
+}
+
 /// Run probe-verus stubify to generate stubs.json from .md files.
 fn generate_stubs(
     project_root: &Path,
     structure_root: &Path,
     stubs_path: &Path,
     config: &CommandConfig,
 ) -> Result<HashMap<String, Value>> {
-    require_probe_installed(config)?;
-
     if let Some(parent) = stubs_path.parent() {
         std::fs::create_dir_all(parent)?;
     }
+    // Ensure structure root exists (create may have written 0 files)
+    std::fs::create_dir_all(structure_root)?;
+
+    // No .md files: stubify would fail; write empty stubs.json and continue
+    if !has_md_files(structure_root) {
+        println!("No .md structure files found; writing empty stubs.json");
+        std::fs::write(stubs_path, "{}")?;
+        return Ok(HashMap::new());
+    }
+
+    require_probe_installed(config)?;
 
     println!(
         "Running probe-verus stubify on {}...",