Skip to content

Commit edadb39

Browse files
committed
feat: added new cloud settings with save
1 parent e0f9c74 commit edadb39

6 files changed

Lines changed: 230 additions & 54 deletions

File tree

Cargo.lock

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

crates/sui-prover/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ colored.workspace = true
1818
tracing.workspace = true
1919
regex.workspace = true
2020
serde.workspace = true
21+
toml.workspace = true
2122
codespan-reporting.workspace = true
2223
telemetry-subscribers.workspace = true
2324

crates/sui-prover/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,5 @@ pub mod legacy_builder;
33
pub mod llm_explain;
44
pub mod prompts;
55
pub mod prove;
6+
pub mod remote_config;
67
pub mod system_dependencies;

crates/sui-prover/src/main.rs

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,16 @@ use std::path::PathBuf;
33
use clap::*;
44
use colored::Colorize;
55
use move_stackless_bytecode::target_filter::TargetFilterOptions;
6-
use prove::{execute, BuildConfig, GeneralConfig, RemoteConfig};
6+
use prove::{execute, BuildConfig, GeneralConfig};
7+
use remote_config::RemoteConfig;
78
use tracing::debug;
89

910
mod build_model;
1011
mod legacy_builder;
1112
mod llm_explain;
1213
mod prompts;
1314
mod prove;
15+
mod remote_config;
1416
mod system_dependencies;
1517

1618
#[derive(Parser)]
@@ -63,15 +65,19 @@ async fn main() {
6365

6466
debug!("Sui-Prover CLI version: {}", env!("CARGO_PKG_VERSION"));
6567

66-
let result = execute(
67-
args.package_path.as_deref(),
68-
args.general_config,
69-
args.remote_config,
70-
args.build_config,
71-
args.boogie_config,
72-
args.filter_config,
73-
)
74-
.await;
68+
let result = if args.remote_config.cloud_config_create {
69+
args.remote_config.create()
70+
} else {
71+
execute(
72+
args.package_path.as_deref(),
73+
args.general_config,
74+
args.remote_config,
75+
args.build_config,
76+
args.boogie_config,
77+
args.filter_config,
78+
)
79+
.await
80+
};
7581

7682
match result {
7783
Ok(_) => (),

crates/sui-prover/src/prove.rs

Lines changed: 2 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
use crate::build_model::build_model;
22
use crate::llm_explain::explain_err;
3+
use crate::remote_config::RemoteConfig;
34
use clap::{Args, ValueEnum};
45
use codespan_reporting::term::termcolor::Buffer;
56
use log::LevelFilter;
@@ -8,7 +9,7 @@ use move_compiler::shared::known_attributes::ModeAttribute;
89
use move_core_types::account_address::AccountAddress;
910
use move_model::model::GlobalEnv;
1011
use move_package::{BuildConfig as MoveBuildConfig, LintFlag};
11-
use move_prover_boogie_backend::boogie_backend::options::{BoogieFileMode, RemoteOptions};
12+
use move_prover_boogie_backend::boogie_backend::options::BoogieFileMode;
1213
use move_prover_boogie_backend::generator::{create_and_process_bytecode, run_boogie_gen};
1314
use move_stackless_bytecode::function_stats;
1415
use move_stackless_bytecode::function_target_pipeline::FunctionHolderTarget;
@@ -156,49 +157,6 @@ pub struct BuildConfig {
156157
pub additional_named_addresses: BTreeMap<String, AccountAddress>,
157158
}
158159

159-
#[derive(Args, Default)]
160-
#[clap(next_help_heading = "Remote Options (concurrent remote boogie execution)")]
161-
pub struct RemoteConfig {
162-
/// Remote URL for the server
163-
#[clap(long = "remote-url", global = true)]
164-
pub remote_url: Option<String>,
165-
166-
/// Remote API key for authentication
167-
#[clap(long = "remote-api-key", global = true)]
168-
pub remote_api_key: Option<String>,
169-
170-
/// Remote calls concurrency value
171-
#[clap(long = "remote-concurrency", global = true)]
172-
pub remote_concurrency: Option<usize>,
173-
}
174-
175-
impl RemoteConfig {
176-
fn to_config(&self) -> anyhow::Result<Option<RemoteOptions>> {
177-
if self.remote_url.is_none() && self.remote_api_key.is_none() {
178-
return Ok(None);
179-
}
180-
181-
if self.remote_url.is_none() || self.remote_api_key.is_none() {
182-
return Err(anyhow::anyhow!(
183-
"Both remote-url and remote-api-key must be provided for remote proving."
184-
));
185-
}
186-
187-
let concurrency =
188-
if self.remote_concurrency.is_none() || self.remote_concurrency.unwrap() == 0 {
189-
10
190-
} else {
191-
self.remote_concurrency.unwrap()
192-
};
193-
194-
Ok(Some(RemoteOptions {
195-
url: self.remote_url.clone().unwrap(),
196-
api_key: self.remote_api_key.clone().unwrap(),
197-
concurrency,
198-
}))
199-
}
200-
}
201-
202160
#[derive(ValueEnum, Default, Clone)]
203161
pub enum BackendOptions {
204162
#[default]
Lines changed: 209 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,209 @@
1+
use clap::Args;
2+
use move_prover_boogie_backend::boogie_backend::options::RemoteOptions;
3+
use serde::{Deserialize, Serialize};
4+
use std::fs;
5+
use std::io::{self, Write};
6+
use std::path::{Path, PathBuf};
7+
8+
#[derive(Debug, Serialize, Deserialize, Clone)]
9+
struct CloudConfig {
10+
url: String,
11+
key: String,
12+
concurrency: usize,
13+
}
14+
15+
fn default_config_path() -> anyhow::Result<PathBuf> {
16+
let home = std::env::var("HOME")
17+
.or_else(|_| std::env::var("USERPROFILE"))
18+
.map_err(|_| anyhow::anyhow!("Could not determine home directory"))?;
19+
20+
Ok(PathBuf::from(home)
21+
.join(".asymptotic")
22+
.join("sui_prover.toml"))
23+
}
24+
25+
fn save_cloud_config(
26+
url: &str,
27+
key: &str,
28+
concurrency: usize,
29+
config_path: Option<&Path>,
30+
) -> anyhow::Result<PathBuf> {
31+
let config = CloudConfig {
32+
url: url.to_string(),
33+
key: key.to_string(),
34+
concurrency,
35+
};
36+
37+
let path = match config_path {
38+
Some(p) => p.to_path_buf(),
39+
None => default_config_path()?,
40+
};
41+
42+
if let Some(parent) = path.parent() {
43+
fs::create_dir_all(parent)?;
44+
}
45+
46+
let toml_string = toml::to_string_pretty(&config)?;
47+
fs::write(&path, toml_string)?;
48+
49+
Ok(path)
50+
}
51+
52+
fn load_cloud_config(config_path: Option<&Path>) -> anyhow::Result<CloudConfig> {
53+
let path = match config_path {
54+
Some(p) => p.to_path_buf(),
55+
None => default_config_path()?,
56+
};
57+
58+
if !path.exists() {
59+
return Err(anyhow::anyhow!(
60+
"Cloud config file not found at: {}",
61+
path.display()
62+
));
63+
}
64+
65+
let toml_string = fs::read_to_string(&path)?;
66+
let config: CloudConfig = toml::from_str(&toml_string)?;
67+
68+
Ok(config)
69+
}
70+
71+
#[derive(Args, Default)]
72+
#[clap(next_help_heading = "Remote Options (concurrent remote boogie execution)")]
73+
pub struct RemoteConfig {
74+
/// Use cloud configuration from file
75+
#[clap(long = "cloud", global = true)]
76+
pub cloud: bool,
77+
78+
/// Path to cloud configuration file (default: $HOME/.asymptotic/sui_prover.toml)
79+
#[clap(long = "cloud-config-path", global = true)]
80+
pub cloud_config_path: Option<PathBuf>,
81+
82+
/// Create/update cloud configuration file interactively
83+
#[clap(long = "cloud-config", global = true)]
84+
pub cloud_config_create: bool,
85+
}
86+
87+
impl RemoteConfig {
88+
pub fn create(&self) -> anyhow::Result<()> {
89+
println!("=== Cloud Configuration Setup ===\n");
90+
91+
// Try to load existing config
92+
let existing_config = load_cloud_config(self.cloud_config_path.as_deref()).ok();
93+
94+
if existing_config.is_some() {
95+
println!("Found existing configuration. Press Enter to keep current values.\n");
96+
}
97+
98+
// Prompt for URL
99+
let url = if let Some(ref config) = existing_config {
100+
print!("Enter remote URL [{}]: ", config.url);
101+
io::stdout().flush()?;
102+
let mut input = String::new();
103+
io::stdin().read_line(&mut input)?;
104+
let input = input.trim();
105+
106+
if input.is_empty() {
107+
config.url.clone()
108+
} else {
109+
input.to_string()
110+
}
111+
} else {
112+
print!("Enter remote URL: ");
113+
io::stdout().flush()?;
114+
let mut input = String::new();
115+
io::stdin().read_line(&mut input)?;
116+
let input = input.trim();
117+
118+
if input.is_empty() {
119+
return Err(anyhow::anyhow!("URL cannot be empty"));
120+
}
121+
input.to_string()
122+
};
123+
124+
// Prompt for API key
125+
let key = if let Some(ref config) = existing_config {
126+
print!("Enter API key [***hidden***]: ");
127+
io::stdout().flush()?;
128+
let mut input = String::new();
129+
io::stdin().read_line(&mut input)?;
130+
let input = input.trim();
131+
132+
if input.is_empty() {
133+
config.key.clone()
134+
} else {
135+
input.to_string()
136+
}
137+
} else {
138+
print!("Enter API key: ");
139+
io::stdout().flush()?;
140+
let mut input = String::new();
141+
io::stdin().read_line(&mut input)?;
142+
let input = input.trim();
143+
144+
if input.is_empty() {
145+
return Err(anyhow::anyhow!("API key cannot be empty"));
146+
}
147+
input.to_string()
148+
};
149+
150+
// Prompt for concurrency
151+
let concurrency = if let Some(ref config) = existing_config {
152+
print!("Enter concurrency [{}]: ", config.concurrency);
153+
io::stdout().flush()?;
154+
let mut input = String::new();
155+
io::stdin().read_line(&mut input)?;
156+
let input = input.trim();
157+
158+
if input.is_empty() {
159+
config.concurrency
160+
} else {
161+
input.parse::<usize>().map_err(|_| {
162+
anyhow::anyhow!("Invalid concurrency value. Must be a positive integer.")
163+
})?
164+
}
165+
} else {
166+
print!("Enter concurrency (default: 10): ");
167+
io::stdout().flush()?;
168+
let mut input = String::new();
169+
io::stdin().read_line(&mut input)?;
170+
let input = input.trim();
171+
172+
if input.is_empty() {
173+
10
174+
} else {
175+
input.parse::<usize>().map_err(|_| {
176+
anyhow::anyhow!("Invalid concurrency value. Must be a positive integer.")
177+
})?
178+
}
179+
};
180+
181+
let path = save_cloud_config(&url, &key, concurrency, self.cloud_config_path.as_deref())?;
182+
183+
println!("\n✓ Cloud configuration saved successfully!");
184+
println!(" Config file: {}", path.display());
185+
println!("\nYou can now use --cloud to load these settings.");
186+
std::process::exit(0);
187+
}
188+
189+
pub fn to_config(&self) -> anyhow::Result<Option<RemoteOptions>> {
190+
if !self.cloud {
191+
return Ok(None);
192+
}
193+
194+
let config = load_cloud_config(self.cloud_config_path.as_deref()).map_err(|e| {
195+
anyhow::anyhow!(
196+
"Failed to load cloud config: {}\n\
197+
Hint: Create a config file first using:\n\
198+
--cloud-config",
199+
e
200+
)
201+
})?;
202+
203+
Ok(Some(RemoteOptions {
204+
url: config.url,
205+
api_key: config.key,
206+
concurrency: config.concurrency,
207+
}))
208+
}
209+
}

0 commit comments

Comments
 (0)