refactor: Replace deprecated python script with probe-verus and fix d… by silverboyir · Pull Request #13 · Beneficial-AI-Foundation/verilib-cli

silverboyir · 2026-02-19T20:28:25Z

…ocker flow

Replaced usage in command with .
Updated command to respect configuration (fixing script not found errors).
Enhanced in to support preserving existing configuration fields.
Updated to support local Docker images by checking existence before pull.
Fixed ARM64 compatibility by removing hardcoded in runtime.
Added Python dependencies to Dockerfile.
Added CACHEBUST arg to Dockerfile and CI workflow to ensure fresh builds.
Updated README with instructions for building and using local Docker images.

…ocker flow - Replaced usage in command with . - Updated command to respect configuration (fixing script not found errors). - Enhanced in to support preserving existing configuration fields. - Updated to support local Docker images by checking existence before pull. - Fixed ARM64 compatibility by removing hardcoded in runtime. - Added Python dependencies to Dockerfile. - Added CACHEBUST arg to Dockerfile and CI workflow to ensure fresh builds. - Updated README with instructions for building and using local Docker images.

Copilot

Pull request overview

This pull request refactors the codebase to replace a deprecated Python script with the probe-verus tracked-csv command and improves Docker support, particularly for ARM64 compatibility. The changes streamline the execution flow by removing hardcoded platform constraints and enhancing the configuration management to preserve existing user settings.

Changes:

Replaced deprecated scripts/analyze_verus_specs_proofs.py with probe-verus tracked-csv command
Removed hardcoded --platform linux/amd64 flag from Docker run command in executor.rs for ARM64 compatibility
Enhanced configuration management to support preserving existing config fields when updating
Added CACHEBUST argument to Dockerfile and CI workflow to ensure fresh builds
Updated README with instructions for building and using local Docker images

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/structure/executor.rs	Relocated `ensure_image_pulled` function and removed platform flag from `run_docker` (but not from image pull)
src/structure/config.rs	Added `preserve_existing` parameter to `save()` method to allow selective field updates
src/commands/create.rs	Replaced Python script with `probe-verus tracked-csv`, added Docker/Local mode handling
README.md	Added documentation for building and using local Docker images
Dockerfile	Added CACHEBUST build argument to force fresh git clones
.github/workflows/docker-publish.yml	Updated branch from "main" to "master" and added CACHEBUST build arg

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-02-19T20:33:32Z

+            json["docker-image"] = serde_json::Value::String(self.docker_image.clone());
+        }
+
+        if !preserve_existing || (json.get("auto-validate-specs").is_none() && json.get("auto_validate_specs").is_none()) {


Line 75 checks for both "auto-validate-specs" (kebab-case) and "auto_validate_specs" (snake_case) field names, but line 159 in the load method only checks for "auto-validate-specs". This inconsistency could lead to issues if users have the snake_case version in their config. Either both locations should check both variants, or the dual check in line 75 should be removed if snake_case was never supported.

Suggested change

if !preserve_existing || (json.get("auto-validate-specs").is_none() && json.get("auto_validate_specs").is_none()) {

if !preserve_existing || json.get("auto-validate-specs").is_none() {

Copilot · 2026-02-19T20:33:32Z

+    println!("Docker image '{}' not found locally. Pulling...", image);
+
+    let status = Command::new("docker")
+        .args(&["pull", "--platform", "linux/amd64", image])


The --platform flag is still hardcoded to linux/amd64 in the ensure_image_pulled function when pulling Docker images. According to the PR description, this should be removed to fix ARM64 compatibility issues. This is inconsistent with the removal of the platform flag from the run_docker function.

Suggested change

.args(&["pull", "--platform", "linux/amd64", image])

.args(&["pull", image])

Copilot · 2026-02-19T20:33:33Z

+fn run_probe_verus_tracked_csv(
    project_root: &Path,
-    seed_path: &Path,
+    _seed_path: &Path,


The parameter _seed_path is prefixed with an underscore to indicate it's intentionally unused, but this represents a significant behavior change. The old implementation used the seed path to analyze specific functions, while the new implementation using probe-verus tracked-csv processes the entire workspace (. in local mode, /workspace in Docker mode). This could lead to different results compared to the old behavior. Consider whether this change in functionality is intentional and whether it should be documented.

Copilot · 2026-02-19T20:33:33Z

+    match config.execution_mode {
+        ExecutionMode::Local => {
+
+            let output_relative = output_path
+                .strip_prefix(project_root)
+                .unwrap_or(output_path)
+                .to_string_lossy();
+
+            let output = run_command(
+                "probe-verus",
+                &[
+                    "tracked-csv",
+                    ".", 
+                    "--output",
+                    &output_relative,
+                ],
+                Some(project_root),
+                config,
+            )?;
+
+            if !output.status.success() {
+                let stderr = String::from_utf8_lossy(&output.stderr);
+                eprintln!("Error running probe-verus tracked-csv:\n{}", stderr);
+                bail!("probe-verus tracked-csv failed");
+            }
+        }
+        ExecutionMode::Docker => {
+            let workspace_mount = "/workspace";
+
+            let output_relative = output_path
+                .strip_prefix(project_root)
+                .unwrap_or(output_path)
+                .to_string_lossy();
+
+            let output_in_container = format!("{}/{}", workspace_mount, output_relative);
+
+            let output = run_command(
+                "probe-verus",
+                &[
+                    "tracked-csv",
+                    workspace_mount, 
+                    "--output",
+                    &output_in_container
+                ],
+                Some(project_root),
+                config,
+            )?;
+
+            if !output.status.success() {
+                let stderr = String::from_utf8_lossy(&output.stderr);
+                eprintln!("Error running probe-verus tracked-csv in Docker:\n{}", stderr);
+                bail!("probe-verus tracked-csv failed");
+            }
+        }


There's significant code duplication between the Local and Docker execution modes. The output path computation and error handling are nearly identical. Consider refactoring to reduce duplication by computing these values before the match statement and only varying the actual command arguments and error messages.

Suggested change

match config.execution_mode {

ExecutionMode::Local => {

let output_relative = output_path

.strip_prefix(project_root)

.unwrap_or(output_path)

.to_string_lossy();

let output = run_command(

"probe-verus",

&[

"tracked-csv",

".",

"--output",

&output_relative,

],

Some(project_root),

config,

)?;

if !output.status.success() {

let stderr = String::from_utf8_lossy(&output.stderr);

eprintln!("Error running probe-verus tracked-csv:\n{}", stderr);

bail!("probe-verus tracked-csv failed");

}

}

ExecutionMode::Docker => {

let workspace_mount = "/workspace";

let output_relative = output_path

.strip_prefix(project_root)

.unwrap_or(output_path)

.to_string_lossy();

let output_in_container = format!("{}/{}", workspace_mount, output_relative);

let output = run_command(

"probe-verus",

&[

"tracked-csv",

workspace_mount,

"--output",

&output_in_container

],

Some(project_root),

config,

)?;

if !output.status.success() {

let stderr = String::from_utf8_lossy(&output.stderr);

eprintln!("Error running probe-verus tracked-csv in Docker:\n{}", stderr);

bail!("probe-verus tracked-csv failed");

}

}

let output_relative = output_path

.strip_prefix(project_root)

.unwrap_or(output_path)

.to_string_lossy()

.to_string();

let (args, error_prefix): (Vec<String>, &str) = match config.execution_mode {

ExecutionMode::Local => (

vec![

"tracked-csv".to_string(),

".".to_string(),

"--output".to_string(),

output_relative.clone(),

],

"Error running probe-verus tracked-csv",

),

ExecutionMode::Docker => {

let workspace_mount = "/workspace";

let output_in_container = format!("{}/{}", workspace_mount, output_relative);

(

vec![

"tracked-csv".to_string(),

workspace_mount.to_string(),

"--output".to_string(),

output_in_container,

],

"Error running probe-verus tracked-csv in Docker",

)

}

};

let arg_refs: Vec<&str> = args.iter().map(|s| s.as_str()).collect();

let output = run_command("probe-verus", &arg_refs, Some(project_root), config)?;

if !output.status.success() {

let stderr = String::from_utf8_lossy(&output.stderr);

eprintln!("{}:\n{}", error_prefix, stderr);

bail!("probe-verus tracked-csv failed");

Copilot · 2026-02-19T20:33:33Z

-        bail!("analyze_verus_specs_proofs.py failed");
+    match config.execution_mode {
+        ExecutionMode::Local => {
+


There's an empty line (line 77) with trailing whitespace after the opening of the Local execution mode branch. This is inconsistent with line 103 in the Docker branch which doesn't have this issue. Consider removing this extra blank line for consistency.

Suggested change

…ure/update-probe-verus

Copilot

Pull request overview

Copilot reviewed 11 out of 12 changed files in this pull request and generated 8 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-02-20T05:53:16Z

@@ -24,30 +24,35 @@ pub async fn handle_create(project_root: PathBuf, root: Option<PathBuf>) -> Resu

    // Write config file with ONLY structure-root field


This comment is inaccurate: StructureConfig::save writes execution-mode, docker-image, and auto-validate-specs when those keys are missing (even with preserve_existing=true), not only structure-root. Please update the comment to match the actual behavior.

Suggested change

// Write config file with ONLY structure-root field

// Initialize config with only structure-root explicitly set; StructureConfig::save

// will also write default values for execution-mode, docker-image, and

// auto-validate-specs when those keys are missing, even with preserve_existing = true.

Copilot · 2026-02-20T05:53:17Z

+        // No functions_to_track.csv - create invokes script without --seed (tracks all functions)
        let output = run_command(&["create"], temp_dir.path());


This test comment says create invokes the script “without --seed”, but run_analyze_verus_specs_proofs always passes --seed (using functions_to_track.csv, generating it if missing). Please update the comment (or the behavior) so the test description matches what the code actually does.

Copilot · 2026-02-20T05:53:17Z

 **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)


README claims create “still runs and sets up config with no structure files” when scripts/analyze_verus_specs_proofs.py is absent. In local execution mode, create currently bails out if scripts/analyze_verus_specs_proofs.py is missing (Script not found locally). Please clarify the README (e.g., optional only in Docker mode with bundled scripts) or adjust create to not error when the script is absent.

Copilot · 2026-02-20T05:53:17Z

    paths:
      - 'Dockerfile'
      - '.github/workflows/docker-publish.yml'
-    branches: [ "main" ]
+    branches: [ "master" ]
    tags: [ 'docker-v*' ]


This workflow now runs on pushes to master, but the metadata step still enables the latest tag only for refs/heads/main (later in this file). As-is, pushes to master will never publish/update the latest tag. Please update the ref check to match master (or keep the workflow on main).

Copilot · 2026-02-20T05:53:18Z

+        return
+
+    if not src_dir.exists():
+        print(f"Error: Source directory not found at {src_dir}")
+        return


When the seed file (or src_dir) is missing, the script prints an error and returns, which will exit with status code 0. That can make callers treat the run as successful and fail later in less obvious ways. Consider exiting non-zero (e.g., raise SystemExit(1)) so failures propagate correctly to verilib-cli create.

Suggested change

return

if not src_dir.exists():

print(f"Error: Source directory not found at {src_dir}")

return

raise SystemExit(1)

if not src_dir.exists():

print(f"Error: Source directory not found at {src_dir}")

raise SystemExit(1)

Copilot · 2026-02-20T05:53:18Z

+    println!("Docker image '{}' not found locally. Pulling...", image);
+
+    let status = Command::new("docker")
+        .args(&["pull", "--platform", "linux/amd64", image])


ensure_image_pulled still forces docker pull --platform linux/amd64, but run_docker no longer pins a platform. This undermines running/pulling native ARM64 images and can lead to inconsistent behavior across hosts. Consider removing the hardcoded platform (or making it conditional/configurable) so pull and run use the same platform selection logic.

Suggested change

.args(&["pull", "--platform", "linux/amd64", image])

.args(&["pull", image])

Copilot · 2026-02-20T05:53:18Z


 WORKDIR /build
+ARG CACHEBUST=1
 RUN git clone https://github.com/Beneficial-AI-Foundation/probe-verus.git


RUN git clone https://github.com/Beneficial-AI-Foundation/probe-verus.git pulls and builds remote code from a mutable branch without pinning to an immutable commit, which creates a supply-chain risk if that repository or its distribution channel is compromised. An attacker who gains control over that repo or can interfere with network traffic to GitHub can inject arbitrary code into the built image and any environment where this image runs. Pin this dependency to a specific trusted commit or release to ensure builds are reproducible and cannot be silently altered upstream.

Copilot · 2026-02-20T05:53:18Z

    && rm -rf /var/lib/apt/lists/*

+# Install uv python package manager
+RUN pip3 install uv --break-system-packages


RUN pip3 install uv --break-system-packages installs and executes code from PyPI at build time without pinning a version or verifying integrity, so any compromise of the uv package or the PyPI distribution path can inject arbitrary code into the resulting image. This command runs with full privileges during the build, so a malicious update to uv would automatically be trusted on rebuild and could exfiltrate secrets or tamper with artifacts. Pin uv to a specific version and, where possible, enable hash-based verification or vendor the dependency so the build is reproducible and resistant to upstream compromise.

astefano · 2026-02-20T10:37:53Z

This PR doesn't replace the python script, the script is added to this branch.

avrevic and others added 6 commits February 19, 2026 17:22

Make functions_to_track.csv not mandatory for create

05e4b46

Remove py file dependency, generate dummy config file if needed

ed8538c

Merge branch 'master' into feature/ENG-452-remove-functions-to-trackcsv

d09dc34

Generate structure even with 0 stubs

a3e7547

Atomize now works without stubs

1cc1ab4

Copilot AI review requested due to automatic review settings February 19, 2026 20:28

Copilot started reviewing on behalf of silverboyir February 19, 2026 20:28 View session

Copilot AI reviewed Feb 19, 2026

View reviewed changes

silverboyir added 2 commits February 19, 2026 12:39

Merge branch 'feature/ENG-452-remove-functions-to-trackcsv' into feat…

b144b96

…ure/update-probe-verus

latest fixes

cba2ce3

Copilot AI review requested due to automatic review settings February 20, 2026 05:45

Copilot started reviewing on behalf of silverboyir February 20, 2026 05:45 View session

0.2.0-beta

c3baf80

Copilot AI reviewed Feb 20, 2026

View reviewed changes

silverboyir added 2 commits February 19, 2026 22:16

remove git ignore

5b4387c

0.2.0-beta.1

bd62843

silverboyir force-pushed the master branch 5 times, most recently from 1f8ff36 to 7f94348 Compare February 24, 2026 21:52

	if !preserve_existing \|\| (json.get("auto-validate-specs").is_none() && json.get("auto_validate_specs").is_none()) {
	if !preserve_existing \|\| json.get("auto-validate-specs").is_none() {

	.args(&["pull", "--platform", "linux/amd64", image])
	.args(&["pull", image])

		@@ -24,30 +24,35 @@ pub async fn handle_create(project_root: PathBuf, root: Option<PathBuf>) -> Resu

		// Write config file with ONLY structure-root field

-    // Write config file with ONLY structure-root field
+    // Initialize config with only structure-root explicitly set; StructureConfig::save
+    // will also write default values for execution-mode, docker-image, and
+    // auto-validate-specs when those keys are missing, even with preserve_existing = true.

		// No functions_to_track.csv - create invokes script without --seed (tracks all functions)
		let output = run_command(&["create"], temp_dir.path());

Conversation

silverboyir commented Feb 19, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Feb 19, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 19, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 19, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 19, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 19, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 20, 2026

Choose a reason for hiding this comment

Uh oh!

astefano commented Feb 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants