Skip to content

Commit bddc435

Browse files
committed
Collect empirical constraints
1 parent 5ccef50 commit bddc435

File tree

6 files changed

+609
-0
lines changed

6 files changed

+609
-0
lines changed
Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
use std::collections::btree_map::Entry;
2+
use std::collections::{BTreeMap, BTreeSet, HashMap};
3+
use std::fmt::Debug;
4+
use std::hash::Hash;
5+
6+
use serde::{Deserialize, Serialize};
7+
8+
/// "Constraints" that were inferred from execution statistics. They hold empirically
9+
/// (most of the time), but are not guaranteed to hold in all cases.
10+
#[derive(Serialize, Deserialize, Clone, Default, Debug)]
11+
pub struct EmpiricalConstraints {
12+
/// For each program counter, the range constraints for each column.
13+
/// The range might not hold in 100% of cases.
14+
pub column_ranges_by_pc: BTreeMap<u32, Vec<(u32, u32)>>,
15+
/// For each basic block (identified by its starting PC), the equivalence classes of columns.
16+
/// Each equivalence class is a list of (instruction index in block, column index).
17+
pub equivalence_classes_by_block: BTreeMap<u64, BTreeSet<BTreeSet<(usize, usize)>>>,
18+
}
19+
20+
/// Debug information mapping AIR ids to program counters and column names.
21+
#[derive(Serialize, Deserialize, Default)]
22+
pub struct DebugInfo {
23+
/// Mapping from program counter to AIR id.
24+
pub air_id_by_pc: BTreeMap<u32, usize>,
25+
/// Mapping from AIR id to column names.
26+
pub column_names_by_air_id: BTreeMap<usize, Vec<String>>,
27+
}
28+
29+
#[derive(Serialize, Deserialize)]
30+
pub struct EmpiricalConstraintsJson {
31+
pub empirical_constraints: EmpiricalConstraints,
32+
pub debug_info: DebugInfo,
33+
}
34+
35+
impl EmpiricalConstraints {
36+
pub fn combine_with(&mut self, other: EmpiricalConstraints) {
37+
// Combine column ranges by PC
38+
for (pc, ranges) in other.column_ranges_by_pc {
39+
self.column_ranges_by_pc
40+
.entry(pc)
41+
.and_modify(|existing_ranges| {
42+
for (i, (min, max)) in ranges.iter().enumerate() {
43+
if let Some((existing_min, existing_max)) = existing_ranges.get_mut(i) {
44+
*existing_min = (*existing_min).min(*min);
45+
*existing_max = (*existing_max).max(*max);
46+
}
47+
}
48+
})
49+
.or_insert(ranges);
50+
}
51+
52+
// Combine equivalence classes by block
53+
for (block_pc, classes) in other.equivalence_classes_by_block {
54+
self.equivalence_classes_by_block
55+
.entry(block_pc)
56+
.and_modify(|existing_classes| {
57+
let combined =
58+
intersect_partitions(&[existing_classes.clone(), classes.clone()]);
59+
*existing_classes = combined;
60+
})
61+
.or_insert(classes);
62+
}
63+
}
64+
}
65+
66+
impl DebugInfo {
67+
pub fn combine_with(&mut self, other: DebugInfo) {
68+
merge_maps(&mut self.air_id_by_pc, other.air_id_by_pc);
69+
merge_maps(
70+
&mut self.column_names_by_air_id,
71+
other.column_names_by_air_id,
72+
);
73+
}
74+
}
75+
76+
/// Merges two maps, asserting that existing keys map to equal values.
77+
fn merge_maps<K: Ord, V: Eq + Debug>(map1: &mut BTreeMap<K, V>, map2: BTreeMap<K, V>) {
78+
for (key, value) in map2 {
79+
match map1.entry(key) {
80+
Entry::Vacant(v) => {
81+
v.insert(value);
82+
}
83+
Entry::Occupied(existing) => {
84+
assert_eq!(*existing.get(), value,);
85+
}
86+
}
87+
}
88+
}
89+
90+
// ChatGPT generated code
91+
pub fn intersect_partitions<Id>(partitions: &[BTreeSet<BTreeSet<Id>>]) -> BTreeSet<BTreeSet<Id>>
92+
where
93+
Id: Eq + Hash + Copy + Ord,
94+
{
95+
if partitions.is_empty() {
96+
return BTreeSet::new();
97+
}
98+
99+
// 1) For each partition, build a map: Id -> class_index
100+
let mut maps: Vec<HashMap<Id, usize>> = Vec::with_capacity(partitions.len());
101+
for part in partitions {
102+
let mut m = HashMap::new();
103+
for (class_idx, class) in part.iter().enumerate() {
104+
for &id in class {
105+
m.insert(id, class_idx);
106+
}
107+
}
108+
maps.push(m);
109+
}
110+
111+
// 2) Collect the universe of all Ids
112+
let mut universe: BTreeSet<Id> = BTreeSet::new();
113+
for part in partitions {
114+
for class in part {
115+
for &id in class {
116+
universe.insert(id);
117+
}
118+
}
119+
}
120+
121+
// 3) For each Id, build its "signature" of class indices across all partitions
122+
// and group by that signature.
123+
let mut grouped: HashMap<Vec<usize>, BTreeSet<Id>> = HashMap::new();
124+
125+
for &id in &universe {
126+
let mut signature = Vec::with_capacity(maps.len());
127+
let mut is_singleton = false;
128+
for m in &maps {
129+
let Some(class_idx) = m.get(&id) else {
130+
// The element did not appear in one of the partition, so it is its
131+
// own equivalence class. We can also omit it in the output partition.
132+
is_singleton = true;
133+
break;
134+
};
135+
signature.push(*class_idx);
136+
}
137+
if !is_singleton {
138+
grouped.entry(signature).or_default().insert(id);
139+
}
140+
}
141+
142+
// 4) Resulting equivalence classes are the grouped values
143+
grouped.into_values().collect()
144+
}

autoprecompiles/src/lib.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ pub mod adapter;
2626
pub mod blocks;
2727
pub mod bus_map;
2828
pub mod constraint_optimizer;
29+
pub mod empirical_constraints;
2930
pub mod evaluation;
3031
pub mod execution_profile;
3132
pub mod expression;
@@ -53,6 +54,8 @@ pub struct PowdrConfig {
5354
pub degree_bound: DegreeBound,
5455
/// The path to the APC candidates dir, if any.
5556
pub apc_candidates_dir_path: Option<PathBuf>,
57+
/// Whether to use optimistic precompiles.
58+
pub optimistic_precompiles: bool,
5659
}
5760

5861
impl PowdrConfig {
@@ -62,13 +65,19 @@ impl PowdrConfig {
6265
skip_autoprecompiles,
6366
degree_bound,
6467
apc_candidates_dir_path: None,
68+
optimistic_precompiles: false,
6569
}
6670
}
6771

6872
pub fn with_apc_candidates_dir<P: AsRef<Path>>(mut self, path: P) -> Self {
6973
self.apc_candidates_dir_path = Some(path.as_ref().to_path_buf());
7074
self
7175
}
76+
77+
pub fn with_optimistic_precompiles(mut self, optimistic: bool) -> Self {
78+
self.optimistic_precompiles = optimistic;
79+
self
80+
}
7281
}
7382

7483
#[derive(Debug, Clone, PartialEq, Hash, Eq, Serialize, Deserialize)]

cli-openvm/src/main.rs

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,11 @@ use metrics_tracing_context::{MetricsLayer, TracingContextLayer};
33
use metrics_util::{debugging::DebuggingRecorder, layers::Layer};
44
use openvm_sdk::StdIn;
55
use openvm_stark_sdk::bench::serialize_metric_snapshot;
6+
use powdr_autoprecompiles::empirical_constraints::EmpiricalConstraintsJson;
67
use powdr_autoprecompiles::pgo::{pgo_config, PgoType};
8+
use powdr_autoprecompiles::PowdrConfig;
79
use powdr_openvm::{compile_openvm, default_powdr_openvm_config, CompiledProgram, GuestOptions};
10+
use powdr_openvm::{detect_empirical_constraints, OriginalCompiledProgram};
811

912
#[cfg(feature = "metrics")]
1013
use openvm_stark_sdk::metrics_tracing::TimingMetricsLayer;
@@ -46,6 +49,12 @@ enum Commands {
4649
/// When `--pgo-mode cell`, the directory to persist all APC candidates + a metrics summary
4750
#[arg(long)]
4851
apc_candidates_dir: Option<PathBuf>,
52+
53+
/// If active, generates "optimistic" precompiles. Optimistic precompiles are smaller in size
54+
/// but may fail at runtime if the assumptions they make are violated.
55+
#[arg(long)]
56+
#[arg(default_value_t = false)]
57+
optimistic_precompiles: bool,
4958
},
5059

5160
Execute {
@@ -73,6 +82,12 @@ enum Commands {
7382
/// When `--pgo-mode cell`, the directory to persist all APC candidates + a metrics summary
7483
#[arg(long)]
7584
apc_candidates_dir: Option<PathBuf>,
85+
86+
/// If active, generates "optimistic" precompiles. Optimistic precompiles are smaller in size
87+
/// but may fail at runtime if the assumptions they make are violated.
88+
#[arg(long)]
89+
#[arg(default_value_t = false)]
90+
optimistic_precompiles: bool,
7691
},
7792

7893
Prove {
@@ -108,6 +123,12 @@ enum Commands {
108123
/// When `--pgo-mode cell`, the directory to persist all APC candidates + a metrics summary
109124
#[arg(long)]
110125
apc_candidates_dir: Option<PathBuf>,
126+
127+
/// If active, generates "optimistic" precompiles. Optimistic precompiles are smaller in size
128+
/// but may fail at runtime if the assumptions they make are violated.
129+
#[arg(long)]
130+
#[arg(default_value_t = false)]
131+
optimistic_precompiles: bool,
111132
},
112133
}
113134

@@ -135,15 +156,20 @@ fn run_command(command: Commands) {
135156
max_columns,
136157
input,
137158
apc_candidates_dir,
159+
optimistic_precompiles,
138160
} => {
139161
let mut powdr_config = default_powdr_openvm_config(autoprecompiles as u64, skip as u64);
140162
if let Some(apc_candidates_dir) = apc_candidates_dir {
141163
powdr_config = powdr_config.with_apc_candidates_dir(apc_candidates_dir);
142164
}
165+
if optimistic_precompiles {
166+
powdr_config = powdr_config.with_optimistic_precompiles(true);
167+
}
143168
let guest_program = compile_openvm(&guest, guest_opts.clone()).unwrap();
144169
let execution_profile =
145170
powdr_openvm::execution_profile_from_guest(&guest_program, stdin_from(input));
146171

172+
maybe_compute_empirical_constraints(&guest_program, &powdr_config, stdin_from(input));
147173
let pgo_config = pgo_config(pgo, max_columns, execution_profile);
148174
let program =
149175
powdr_openvm::compile_exe(guest_program, powdr_config, pgo_config).unwrap();
@@ -159,12 +185,17 @@ fn run_command(command: Commands) {
159185
input,
160186
metrics,
161187
apc_candidates_dir,
188+
optimistic_precompiles,
162189
} => {
163190
let mut powdr_config = default_powdr_openvm_config(autoprecompiles as u64, skip as u64);
164191
if let Some(apc_candidates_dir) = apc_candidates_dir {
165192
powdr_config = powdr_config.with_apc_candidates_dir(apc_candidates_dir);
166193
}
194+
if optimistic_precompiles {
195+
powdr_config = powdr_config.with_optimistic_precompiles(true);
196+
}
167197
let guest_program = compile_openvm(&guest, guest_opts.clone()).unwrap();
198+
maybe_compute_empirical_constraints(&guest_program, &powdr_config, stdin_from(input));
168199
let execution_profile =
169200
powdr_openvm::execution_profile_from_guest(&guest_program, stdin_from(input));
170201
let pgo_config = pgo_config(pgo, max_columns, execution_profile);
@@ -194,12 +225,17 @@ fn run_command(command: Commands) {
194225
input,
195226
metrics,
196227
apc_candidates_dir,
228+
optimistic_precompiles,
197229
} => {
198230
let mut powdr_config = default_powdr_openvm_config(autoprecompiles as u64, skip as u64);
199231
if let Some(apc_candidates_dir) = apc_candidates_dir {
200232
powdr_config = powdr_config.with_apc_candidates_dir(apc_candidates_dir);
201233
}
234+
if optimistic_precompiles {
235+
powdr_config = powdr_config.with_optimistic_precompiles(true);
236+
}
202237
let guest_program = compile_openvm(&guest, guest_opts).unwrap();
238+
maybe_compute_empirical_constraints(&guest_program, &powdr_config, stdin_from(input));
203239

204240
let execution_profile =
205241
powdr_openvm::execution_profile_from_guest(&guest_program, stdin_from(input));
@@ -261,3 +297,33 @@ pub fn run_with_metric_collection_to_file<R>(file: std::fs::File, f: impl FnOnce
261297
.unwrap();
262298
res
263299
}
300+
301+
fn maybe_compute_empirical_constraints(
302+
guest_program: &OriginalCompiledProgram,
303+
powdr_config: &PowdrConfig,
304+
stdin: StdIn,
305+
) {
306+
if !powdr_config.optimistic_precompiles {
307+
return;
308+
}
309+
310+
tracing::warn!(
311+
"Optimistic precompiles are not implemented yet. Computing empirical constraints..."
312+
);
313+
314+
let (empirical_constraints, debug_info) =
315+
detect_empirical_constraints(guest_program, powdr_config.degree_bound, vec![stdin]);
316+
317+
if let Some(path) = &powdr_config.apc_candidates_dir_path {
318+
tracing::info!(
319+
"Saving empirical constraints debug info to {}/empirical_constraints.json",
320+
path.display()
321+
);
322+
let export = EmpiricalConstraintsJson {
323+
empirical_constraints: empirical_constraints.clone(),
324+
debug_info,
325+
};
326+
let json = serde_json::to_string_pretty(&export).unwrap();
327+
std::fs::write(path.join("empirical_constraints.json"), json).unwrap();
328+
}
329+
}

0 commit comments

Comments
 (0)