Skip to content

Commit 9f9d7ee

Browse files
committed
zkDSL: introduce CustomHint
1 parent d24eb0c commit 9f9d7ee

File tree

13 files changed

+196
-330
lines changed

13 files changed

+196
-330
lines changed

Cargo.lock

Lines changed: 47 additions & 25 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@ itertools = "0.14.0"
6767
colored = "3.0.0"
6868
tracing = "0.1.26"
6969
serde_json = "1.0.145"
70+
strum = { version = "0.27.2", features = ["derive"] }
7071
serde = { version = "1.0.228", features = ["derive"] }
7172
bincode = "1.3.3"
7273
num_enum = "0.7.5"

crates/lean_compiler/src/a_simplify_lang.rs

Lines changed: 15 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use crate::{
66
Expression, Function, Line, Program, Scope, SimpleExpr, Var,
77
},
88
};
9-
use lean_vm::{Boolean, BooleanExpr, FileId, SourceLineNumber, SourceLocation, Table, TableT};
9+
use lean_vm::{Boolean, BooleanExpr, CustomHint, FileId, SourceLineNumber, SourceLocation, Table, TableT};
1010
use std::{
1111
collections::{BTreeMap, BTreeSet},
1212
fmt::{Display, Formatter},
@@ -114,18 +114,11 @@ pub enum SimpleLine {
114114
},
115115
Panic,
116116
// Hints
117-
DecomposeBits {
118-
var: Var, // a pointer to 31 * len(to_decompose) field elements, containing the bits of "to_decompose"
119-
to_decompose: Vec<SimpleExpr>,
120-
label: ConstMallocLabel,
121-
},
122117
/// each field element x is decomposed to: (a0, a1, a2, ..., a11, b) where:
123118
/// x = a0 + a1.4 + a2.4^2 + a3.4^3 + ... + a11.4^11 + b.2^24
124119
/// and ai < 4, b < 2^7 - 1
125120
/// The decomposition is unique, and always exists (except for x = -1)
126-
DecomposeCustom {
127-
args: Vec<SimpleExpr>,
128-
},
121+
CustomHint(CustomHint, Vec<SimpleExpr>),
129122
PrivateInputStart {
130123
result: Var,
131124
},
@@ -488,18 +481,7 @@ fn check_block_scoping(block: &[Line], ctx: &mut Context) {
488481
);
489482
last_scope.vars.insert(var.clone());
490483
}
491-
Line::DecomposeBits { var, to_decompose } => {
492-
for expr in to_decompose {
493-
check_expr_scoping(expr, ctx);
494-
}
495-
let last_scope = ctx.scopes.last_mut().unwrap();
496-
assert!(
497-
!last_scope.vars.contains(var),
498-
"Variable declared multiple times in the same scope: {var}",
499-
);
500-
last_scope.vars.insert(var.clone());
501-
}
502-
Line::DecomposeCustom { args } => {
484+
Line::CustomHint(_, args) => {
503485
for arg in args {
504486
check_expr_scoping(arg, ctx);
505487
}
@@ -1105,29 +1087,15 @@ fn simplify_lines(
11051087
}
11061088
}
11071089
}
1108-
Line::DecomposeBits { var, to_decompose } => {
1109-
let simplified_to_decompose = to_decompose
1110-
.iter()
1111-
.map(|expr| simplify_expr(expr, &mut res, counters, array_manager, const_malloc, const_arrays))
1112-
.collect::<Vec<_>>();
1113-
let label = const_malloc.counter;
1114-
const_malloc.counter += 1;
1115-
const_malloc.map.insert(var.clone(), label);
1116-
res.push(SimpleLine::DecomposeBits {
1117-
var: var.clone(),
1118-
to_decompose: simplified_to_decompose,
1119-
label,
1120-
});
1121-
}
11221090
Line::PrivateInputStart { result } => {
11231091
res.push(SimpleLine::PrivateInputStart { result: result.clone() });
11241092
}
1125-
Line::DecomposeCustom { args } => {
1093+
Line::CustomHint(hint, args) => {
11261094
let simplified_args = args
11271095
.iter()
11281096
.map(|expr| simplify_expr(expr, &mut res, counters, array_manager, const_malloc, const_arrays))
11291097
.collect::<Vec<_>>();
1130-
res.push(SimpleLine::DecomposeCustom { args: simplified_args });
1098+
res.push(SimpleLine::CustomHint(*hint, simplified_args));
11311099
}
11321100
Line::Panic => {
11331101
res.push(SimpleLine::Panic);
@@ -1355,16 +1323,10 @@ pub fn find_variable_usage(
13551323
on_new_expr(var, &internal_vars, &mut external_vars);
13561324
}
13571325
}
1358-
Line::DecomposeBits { var, to_decompose } => {
1359-
for expr in to_decompose {
1360-
on_new_expr(expr, &internal_vars, &mut external_vars);
1361-
}
1362-
internal_vars.insert(var.clone());
1363-
}
13641326
Line::PrivateInputStart { result } => {
13651327
internal_vars.insert(result.clone());
13661328
}
1367-
Line::DecomposeCustom { args } => {
1329+
Line::CustomHint(_, args) => {
13681330
for expr in args {
13691331
on_new_expr(expr, &internal_vars, &mut external_vars);
13701332
}
@@ -1543,14 +1505,8 @@ fn inline_lines(
15431505
inline_expr(var, args, inlining_count);
15441506
}
15451507
}
1546-
Line::DecomposeBits { var, to_decompose } => {
1547-
for expr in to_decompose {
1548-
inline_expr(expr, args, inlining_count);
1549-
}
1550-
inline_internal_var(var);
1551-
}
1552-
Line::DecomposeCustom { args: decompose_args } => {
1553-
for expr in decompose_args {
1508+
Line::CustomHint(_, decomposed_args) => {
1509+
for expr in decomposed_args {
15541510
inline_expr(expr, args, inlining_count);
15551511
}
15561512
}
@@ -1938,19 +1894,12 @@ fn replace_vars_for_unroll(
19381894
replace_vars_for_unroll_in_expr(size, iterator, unroll_index, iterator_value, internal_vars);
19391895
replace_vars_for_unroll_in_expr(vectorized_len, iterator, unroll_index, iterator_value, internal_vars);
19401896
}
1941-
Line::DecomposeBits { var, to_decompose } => {
1942-
assert!(var != iterator, "Weird");
1943-
*var = format!("@unrolled_{unroll_index}_{iterator_value}_{var}");
1944-
for expr in to_decompose {
1945-
replace_vars_for_unroll_in_expr(expr, iterator, unroll_index, iterator_value, internal_vars);
1946-
}
1947-
}
19481897
Line::PrivateInputStart { result } => {
19491898
assert!(result != iterator, "Weird");
19501899
*result = format!("@unrolled_{unroll_index}_{iterator_value}_{result}");
19511900
}
1952-
Line::DecomposeCustom { args } => {
1953-
for expr in args {
1901+
Line::CustomHint(_, decomposed_args) => {
1902+
for expr in decomposed_args {
19541903
replace_vars_for_unroll_in_expr(expr, iterator, unroll_index, iterator_value, internal_vars);
19551904
}
19561905
}
@@ -2410,14 +2359,8 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
24102359
replace_vars_by_const_in_expr(var, map);
24112360
}
24122361
}
2413-
Line::DecomposeBits { var, to_decompose } => {
2414-
assert!(!map.contains_key(var), "Variable {var} is a constant");
2415-
for expr in to_decompose {
2416-
replace_vars_by_const_in_expr(expr, map);
2417-
}
2418-
}
2419-
Line::DecomposeCustom { args } => {
2420-
for expr in args {
2362+
Line::CustomHint(_, decomposed_args) => {
2363+
for expr in decomposed_args {
24212364
replace_vars_by_const_in_expr(expr, map);
24222365
}
24232366
}
@@ -2484,24 +2427,10 @@ impl SimpleLine {
24842427
} => {
24852428
format!("{var} = {arg0} {operation} {arg1}")
24862429
}
2487-
Self::DecomposeBits {
2488-
var: result,
2489-
to_decompose,
2490-
label: _,
2491-
} => {
2492-
format!(
2493-
"{} = decompose_bits({})",
2494-
result,
2495-
to_decompose
2496-
.iter()
2497-
.map(|expr| format!("{expr}"))
2498-
.collect::<Vec<_>>()
2499-
.join(", ")
2500-
)
2501-
}
2502-
Self::DecomposeCustom { args } => {
2430+
Self::CustomHint(hint, args) => {
25032431
format!(
2504-
"decompose_custom({})",
2432+
"{}({})",
2433+
hint.name(),
25052434
args.iter().map(|expr| format!("{expr}")).collect::<Vec<_>>().join(", ")
25062435
)
25072436
}

0 commit comments

Comments
 (0)