From 1e0bf953cd6d185ef2c4eb1d2a56c212a6cd4e3d Mon Sep 17 00:00:00 2001
From: Simon Scatton <sscatton@nvidia.com>
Date: Thu, 16 Jul 2026 17:07:47 +0200
Subject: [PATCH] feat!(openshell-cli): remove openshell policy prove command
 and z3 dependency

Signed-off-by: Simon Scatton <sscatton@nvidia.com>
---
 .github/workflows/docker-build.yml |  2 +-
 Cargo.lock                         |  1 -
 crates/openshell-cli/Cargo.toml    |  4 ---
 crates/openshell-cli/src/main.rs   | 47 ------------------------------
 4 files changed, 1 insertion(+), 53 deletions(-)

diff --git a/.github/workflows/docker-build.yml b/.github/workflows/docker-build.yml
index 4c92bc3857..0ed09d9d4b 100644
--- a/.github/workflows/docker-build.yml
+++ b/.github/workflows/docker-build.yml
@@ -96,7 +96,7 @@ jobs:
             cli)
               binary_component=cli
               binary_name=openshell
-              features="bundled-z3"
+              features=""
               has_image=false
               ;;
             *)
diff --git a/Cargo.lock b/Cargo.lock
index d061c74496..1de52d8841 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -3597,7 +3597,6 @@ dependencies = [
  "openshell-bootstrap",
  "openshell-core",
  "openshell-policy",
- "openshell-prover",
  "openshell-providers",
  "openshell-tui",
  "owo-colors",
diff --git a/crates/openshell-cli/Cargo.toml b/crates/openshell-cli/Cargo.toml
index 8e4cb3fb25..1cbfd7d474 100644
--- a/crates/openshell-cli/Cargo.toml
+++ b/crates/openshell-cli/Cargo.toml
@@ -19,7 +19,6 @@ openshell-bootstrap = { path = "../openshell-bootstrap" }
 openshell-core = { path = "../openshell-core", default-features = false }
 openshell-policy = { path = "../openshell-policy" }
 openshell-providers = { path = "../openshell-providers" }
-openshell-prover = { path = "../openshell-prover" }
 openshell-tui = { path = "../openshell-tui" }
 serde = { workspace = true }
 serde_json = { workspace = true }
@@ -84,9 +83,6 @@ tracing-subscriber = { workspace = true }
 [lints]
 workspace = true
 
-[features]
-bundled-z3 = ["openshell-prover/bundled-z3"]
-
 [dev-dependencies]
 futures = { workspace = true }
 rcgen = { version = "0.13", features = ["crypto", "pem"] }
diff --git a/crates/openshell-cli/src/main.rs b/crates/openshell-cli/src/main.rs
index b32e7fe9f9..07b302a027 100644
--- a/crates/openshell-cli/src/main.rs
+++ b/crates/openshell-cli/src/main.rs
@@ -1743,30 +1743,6 @@ enum PolicyCommands {
         #[arg(long)]
         yes: bool,
     },
-
-    /// Prove properties of a sandbox policy — or find counterexamples.
-    #[command(help_template = LEAF_HELP_TEMPLATE, next_help_heading = "FLAGS")]
-    Prove {
-        /// Path to `OpenShell` sandbox policy YAML.
-        #[arg(long, value_hint = ValueHint::FilePath)]
-        policy: String,
-
-        /// Path to credential descriptor YAML.
-        #[arg(long, value_hint = ValueHint::FilePath)]
-        credentials: String,
-
-        /// Path to capability registry directory (default: bundled).
-        #[arg(long, value_hint = ValueHint::DirPath)]
-        registry: Option<String>,
-
-        /// Path to accepted risks YAML.
-        #[arg(long, value_hint = ValueHint::FilePath)]
-        accepted_risks: Option<String>,
-
-        /// One-line-per-finding output (for demos and CI).
-        #[arg(long)]
-        compact: bool,
-    },
 }
 
 #[derive(Subcommand, Debug)]
@@ -2297,28 +2273,6 @@ async fn main() -> Result<()> {
         // -----------------------------------------------------------
         // Top-level policy (was `sandbox policy`)
         // -----------------------------------------------------------
-        Some(Commands::Policy {
-            command:
-                Some(PolicyCommands::Prove {
-                    policy,
-                    credentials,
-                    registry,
-                    accepted_risks,
-                    compact,
-                }),
-        }) => {
-            // Prove runs locally — no gateway needed.
-            let exit_code = openshell_prover::prove(
-                &policy,
-                &credentials,
-                registry.as_deref(),
-                accepted_risks.as_deref(),
-                compact,
-            )?;
-            if exit_code != 0 {
-                std::process::exit(exit_code);
-            }
-        }
         Some(Commands::Policy {
             command: Some(policy_cmd),
         }) => {
@@ -2438,7 +2392,6 @@ async fn main() -> Result<()> {
                     }
                     run::gateway_setting_delete(&ctx.endpoint, "policy", yes, &tls).await?;
                 }
-                PolicyCommands::Prove { .. } => unreachable!(),
             }
         }