Skip to content

Commit 589374e

Browse files
committed
Collect empirical constraints
1 parent 5ccef50 commit 589374e

File tree

6 files changed

+632
-0
lines changed

6 files changed

+632
-0
lines changed
Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
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 itertools::Itertools;
7+
use serde::{Deserialize, Serialize};
8+
9+
/// "Constraints" that were inferred from execution statistics. They hold empirically
10+
/// (most of the time), but are not guaranteed to hold in all cases.
11+
#[derive(Serialize, Deserialize, Clone, Default, Debug)]
12+
pub struct EmpiricalConstraints {
13+
/// For each program counter, the range constraints for each column.
14+
/// The range might not hold in 100% of cases.
15+
pub column_ranges_by_pc: BTreeMap<u32, Vec<(u32, u32)>>,
16+
/// For each basic block (identified by its starting PC), the equivalence classes of columns.
17+
/// Each equivalence class is a list of (instruction index in block, column index).
18+
pub equivalence_classes_by_block: BTreeMap<u64, BTreeSet<BTreeSet<(usize, usize)>>>,
19+
}
20+
21+
/// Debug information mapping AIR ids to program counters and column names.
22+
#[derive(Serialize, Deserialize, Default)]
23+
pub struct DebugInfo {
24+
/// Mapping from program counter to AIR id.
25+
pub air_id_by_pc: BTreeMap<u32, usize>,
26+
/// Mapping from AIR id to column names.
27+
pub column_names_by_air_id: BTreeMap<usize, Vec<String>>,
28+
}
29+
30+
#[derive(Serialize, Deserialize)]
31+
pub struct EmpiricalConstraintsJson {
32+
pub empirical_constraints: EmpiricalConstraints,
33+
pub debug_info: DebugInfo,
34+
}
35+
36+
impl EmpiricalConstraints {
37+
pub fn combine_with(&mut self, other: EmpiricalConstraints) {
38+
// Combine column ranges by PC
39+
for (pc, ranges) in other.column_ranges_by_pc {
40+
self.column_ranges_by_pc
41+
.entry(pc)
42+
.and_modify(|existing_ranges| {
43+
for (i, (min, max)) in ranges.iter().enumerate() {
44+
if let Some((existing_min, existing_max)) = existing_ranges.get_mut(i) {
45+
*existing_min = (*existing_min).min(*min);
46+
*existing_max = (*existing_max).max(*max);
47+
}
48+
}
49+
})
50+
.or_insert(ranges);
51+
}
52+
53+
// Combine equivalence classes by block
54+
for (block_pc, classes) in other.equivalence_classes_by_block {
55+
self.equivalence_classes_by_block
56+
.entry(block_pc)
57+
.and_modify(|existing_classes| {
58+
let combined =
59+
intersect_partitions(&[existing_classes.clone(), classes.clone()]);
60+
*existing_classes = combined;
61+
})
62+
.or_insert(classes);
63+
}
64+
}
65+
}
66+
67+
impl DebugInfo {
68+
pub fn combine_with(&mut self, other: DebugInfo) {
69+
merge_maps(&mut self.air_id_by_pc, other.air_id_by_pc);
70+
merge_maps(
71+
&mut self.column_names_by_air_id,
72+
other.column_names_by_air_id,
73+
);
74+
}
75+
}
76+
77+
/// Merges two maps, asserting that existing keys map to equal values.
78+
fn merge_maps<K: Ord, V: Eq + Debug>(map1: &mut BTreeMap<K, V>, map2: BTreeMap<K, V>) {
79+
for (key, value) in map2 {
80+
match map1.entry(key) {
81+
Entry::Vacant(v) => {
82+
v.insert(value);
83+
}
84+
Entry::Occupied(existing) => {
85+
assert_eq!(*existing.get(), value,);
86+
}
87+
}
88+
}
89+
}
90+
91+
/// Intersects multiple partitions of the same universe into a single partition.
92+
/// In other words, two elements are in the same equivalence class in the resulting partition
93+
/// if and only if they are in the same equivalence class in all input partitions.
94+
/// Singleton equivalence classes are omitted from the result.
95+
pub fn intersect_partitions<Id>(partitions: &[BTreeSet<BTreeSet<Id>>]) -> BTreeSet<BTreeSet<Id>>
96+
where
97+
Id: Eq + Hash + Copy + Ord,
98+
{
99+
// For each partition, build a map: Id -> class_index
100+
let class_ids: Vec<HashMap<Id, usize>> = partitions
101+
.iter()
102+
.map(|partition| {
103+
partition
104+
.iter()
105+
.enumerate()
106+
.flat_map(|(class_idx, class)| class.iter().map(move |&id| (id, class_idx)))
107+
.collect()
108+
})
109+
.collect();
110+
111+
// Iterate over all elements in the universe
112+
partitions
113+
.iter()
114+
.flat_map(|partition| partition.iter())
115+
.flat_map(|class| class.iter().copied())
116+
.unique()
117+
.filter_map(|id| {
118+
// Build the signature of the element: the list of class indices it belongs to
119+
// (one index per partition)
120+
class_ids
121+
.iter()
122+
.map(|m| m.get(&id).cloned())
123+
// If an element did not appear in any one of the partitions, it is
124+
// a singleton and we skip it.
125+
.collect::<Option<Vec<usize>>>()
126+
.map(|signature| (signature, id))
127+
})
128+
// Group elements by their signatures
129+
.into_group_map()
130+
.into_values()
131+
// Remove singletons and convert to Set
132+
.filter_map(|ids| (ids.len() > 1).then_some(ids.into_iter().collect()))
133+
.collect()
134+
}
135+
136+
#[cfg(test)]
137+
mod tests {
138+
use std::collections::BTreeSet;
139+
140+
fn partition(sets: Vec<Vec<u32>>) -> BTreeSet<BTreeSet<u32>> {
141+
sets.into_iter().map(|s| s.into_iter().collect()).collect()
142+
}
143+
144+
#[test]
145+
fn test_intersect_partitions() {
146+
let partition1 = partition(vec![
147+
// Two classes: 1-4 and 5-9
148+
vec![1, 2, 3, 4],
149+
vec![5, 6, 7, 8, 9],
150+
]);
151+
let partition2 = partition(vec![
152+
// Four classes: 1, 2-3, 4-5, 6-8, 9 (implicit)
153+
vec![1],
154+
vec![2, 3],
155+
vec![4, 5],
156+
vec![6, 7, 8],
157+
]);
158+
159+
let result = super::intersect_partitions(&[partition1, partition2]);
160+
161+
let expected = partition(vec![vec![2, 3], vec![6, 7, 8]]);
162+
163+
assert_eq!(result, expected);
164+
}
165+
}

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)