Skip to content

Commit 413e4e4

Browse files
committed
Merge branch 'perf_xmss'
2 parents b081bc6 + 8200ffb commit 413e4e4

File tree

19 files changed

+494
-269
lines changed

19 files changed

+494
-269
lines changed

Cargo.lock

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

Cargo.toml

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,19 @@ packed_pcs.workspace = true
100100
p3-air.workspace = true
101101
multilinear-toolkit.workspace = true
102102

103+
# [patch."https://github.com/TomWambsgans/Plonky3.git"]
104+
# p3-koala-bear = { path = "../zk/Plonky3/koala-bear" }
105+
# p3-field = { path = "../zk/Plonky3/field" }
106+
# p3-poseidon2 = { path = "../zk/Plonky3/poseidon2" }
107+
# p3-matrix = { path = "../zk/Plonky3/matrix" }
108+
# p3-symmetric = { path = "../zk/Plonky3/symmetric" }
109+
# p3-air = { path = "../zk/Plonky3/air" }
110+
# p3-uni-stark = { path = "../zk/Plonky3/uni-stark" }
111+
# p3-poseidon2-air = { path = "../zk/Plonky3/poseidon2-air" }
112+
# p3-dft = { path = "../zk/Plonky3/dft" }
113+
# p3-challenger = { path = "../zk/Plonky3/challenger" }
114+
# p3-util = { path = "../zk/Plonky3/util" }
115+
103116
[dev-dependencies]
104117
criterion = { version = "0.7", default-features = false, features = ["cargo_bench_support"] }
105118
rec_aggregation.workspace = true

TODO.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@
1212
- avoid field embedding in the initial sumcheck of logup*, when table / values are in base field
1313
- opti logup* GKR when the indexes are not a power of 2 (which is the case in the execution table)
1414
- incremental merkle paths in whir-p3
15-
- Experiment to increase degree, and reduce commitments, in Poseidon arithmetization
15+
- Experiment to increase degree, and reduce commitments, in Poseidon arithmetization.
16+
Result: degree 9 is better than 3. TODO: degree 5, or 6 ? Also, the current degre 9 implem may not be perfectly optimal?
1617
- Avoid embedding overhead on the flag, len, and index columns in the AIR table for dot products
1718
- Batched logup*: when computing the eq() factor we can opti if the points contain boolean factor
1819
- Lev's trick to skip some low-level modular reduction
@@ -26,6 +27,7 @@
2627
- the interpreter of leanISA (+ witness generation) can be partially parallelized when there are some independent loops
2728
- (1 - x).r1 + x.r2 = x.(r2 - r1) + r1 TODO this opti is not everywhere currently + TODO generalize this with the univaraite skip
2829
- opti compute_eval_eq when scalar = ONE
30+
- Dmitry's range check, bonus: we can spare 2 memory cells if the value being range check is small (using the zeros present by conventio on the public memory)
2931

3032
About "the packed pcs" (similar to SP1 Jagged PCS, slightly less efficient, but simpler (no sumchecks)):
3133
- The best strategy is probably to pack as much as possible (the cost increasing the density = additional inner evaluations), if we can fit below a power of 2 - epsilon (epsilon = 20% for instance, tbd), if the sum of the non zero data is just above a power of 2, no packed technique, even the best, can help us, so we should spread aniway (to reduce the pressure of inner evaluations)

crates/lean_compiler/src/a_simplify_lang.rs

Lines changed: 51 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,15 @@ pub enum SimpleLine {
116116
to_decompose: Vec<SimpleExpr>,
117117
label: ConstMallocLabel,
118118
},
119+
/// each field element x is decomposed to: (a0, a1, a2, ..., a11, b) where:
120+
/// x = a0 + a1.4 + a2.4^2 + a3.4^3 + ... + a11.4^11 + b.2^24
121+
/// and ai < 4, b < 2^7 - 1
122+
/// The decomposition is unique, and always exists (except for x = -1)
123+
DecomposeCustom {
124+
var: Var, // a pointer to 13 * len(to_decompose) field elements
125+
to_decompose: Vec<SimpleExpr>,
126+
label: ConstMallocLabel,
127+
},
119128
CounterHint {
120129
var: Var,
121130
},
@@ -653,6 +662,23 @@ fn simplify_lines(
653662
label,
654663
});
655664
}
665+
Line::DecomposeCustom { var, to_decompose } => {
666+
assert!(!const_malloc.forbidden_vars.contains(var), "TODO");
667+
let simplified_to_decompose = to_decompose
668+
.iter()
669+
.map(|expr| {
670+
simplify_expr(expr, &mut res, counters, array_manager, const_malloc)
671+
})
672+
.collect::<Vec<_>>();
673+
let label = const_malloc.counter;
674+
const_malloc.counter += 1;
675+
const_malloc.map.insert(var.clone(), label);
676+
res.push(SimpleLine::DecomposeCustom {
677+
var: var.clone(),
678+
to_decompose: simplified_to_decompose,
679+
label,
680+
});
681+
}
656682
Line::CounterHint { var } => {
657683
res.push(SimpleLine::CounterHint { var: var.clone() });
658684
}
@@ -837,12 +863,14 @@ pub fn find_variable_usage(lines: &[Line]) -> (BTreeSet<Var>, BTreeSet<Var>) {
837863
on_new_expr(var, &internal_vars, &mut external_vars);
838864
}
839865
}
840-
Line::DecomposeBits { var, to_decompose } => {
866+
Line::DecomposeBits { var, to_decompose }
867+
| Line::DecomposeCustom { var, to_decompose } => {
841868
for expr in to_decompose {
842869
on_new_expr(expr, &internal_vars, &mut external_vars);
843870
}
844871
internal_vars.insert(var.clone());
845872
}
873+
846874
Line::CounterHint { var } => {
847875
internal_vars.insert(var.clone());
848876
}
@@ -1002,7 +1030,8 @@ pub fn inline_lines(
10021030
inline_expr(var, args, inlining_count);
10031031
}
10041032
}
1005-
Line::DecomposeBits { var, to_decompose } => {
1033+
Line::DecomposeBits { var, to_decompose }
1034+
| Line::DecomposeCustom { var, to_decompose } => {
10061035
for expr in to_decompose {
10071036
inline_expr(expr, args, inlining_count);
10081037
}
@@ -1485,7 +1514,8 @@ fn replace_vars_for_unroll(
14851514
internal_vars,
14861515
);
14871516
}
1488-
Line::DecomposeBits { var, to_decompose } => {
1517+
Line::DecomposeBits { var, to_decompose }
1518+
| Line::DecomposeCustom { var, to_decompose } => {
14891519
assert!(var != iterator, "Weird");
14901520
*var = format!("@unrolled_{unroll_index}_{iterator_value}_{var}");
14911521
for expr in to_decompose {
@@ -1886,6 +1916,7 @@ fn get_function_called(lines: &[Line], function_called: &mut Vec<String>) {
18861916
| Line::Precompile { .. }
18871917
| Line::Print { .. }
18881918
| Line::DecomposeBits { .. }
1919+
| Line::DecomposeCustom { .. }
18891920
| Line::CounterHint { .. }
18901921
| Line::MAlloc { .. }
18911922
| Line::Panic
@@ -1980,7 +2011,8 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
19802011
replace_vars_by_const_in_expr(var, map);
19812012
}
19822013
}
1983-
Line::DecomposeBits { var, to_decompose } => {
2014+
Line::DecomposeBits { var, to_decompose }
2015+
| Line::DecomposeCustom { var, to_decompose } => {
19842016
assert!(!map.contains_key(var), "Variable {var} is a constant");
19852017
for expr in to_decompose {
19862018
replace_vars_by_const_in_expr(expr, map);
@@ -2063,6 +2095,21 @@ impl SimpleLine {
20632095
.join(", ")
20642096
)
20652097
}
2098+
Self::DecomposeCustom {
2099+
var: result,
2100+
to_decompose,
2101+
label: _,
2102+
} => {
2103+
format!(
2104+
"{} = decompose_custom({})",
2105+
result,
2106+
to_decompose
2107+
.iter()
2108+
.map(|expr| format!("{expr}"))
2109+
.collect::<Vec<_>>()
2110+
.join(", ")
2111+
)
2112+
}
20662113
Self::CounterHint { var: result } => {
20672114
format!("{result} = counter_hint()")
20682115
}

0 commit comments

Comments
 (0)