Skip to content

Commit 27e63df

Browse files
chrisethchriseth
committed
Merge remote-tracking branch 'origin/main' into prover_functions_for_small_arith
2 parents 9578dd0 + 28307fb commit 27e63df

16 files changed

+339
-238
lines changed

Diff for: ‎.github/workflows/nightly-tests.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -76,4 +76,4 @@ jobs:
7676
- name: Build
7777
run: cargo build --all --release --all-features
7878
- name: Run tests
79-
run: cargo test --all --release --verbose --all-features -- --include-ignored --nocapture
79+
run: cargo test --all --release --verbose --all-features -- --include-ignored --nocapture --test-threads=2

Diff for: ‎.github/workflows/pr-tests.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ jobs:
104104
run: sudo apt-get update && sudo apt-get install -y binutils-riscv64-unknown-elf lld
105105
- uses: taiki-e/install-action@nextest
106106
- name: Run default tests
107-
run: cargo nextest run --archive-file tests.tar.zst --workspace-remap . --verbose --partition count:"${{ matrix.test }}"/2
107+
run: cargo nextest run --archive-file tests.tar.zst --workspace-remap . --verbose --partition count:"${{ matrix.test }}"/2 --no-tests=warn
108108
env:
109109
POWDR_STD: ${{ github.workspace }}/std/
110110

@@ -220,7 +220,7 @@ jobs:
220220
- name: Run slow tests
221221
run: |
222222
NIGHTLY_TESTS=$(cat .github/workflows/nightly_tests_list.txt)
223-
cargo nextest run --archive-file tests.tar.zst --workspace-remap . --verbose --run-ignored=ignored-only -E "!($NIGHTLY_TESTS)" --partition hash:"${{ matrix.test }}"/17
223+
cargo nextest run --archive-file tests.tar.zst --workspace-remap . --verbose --run-ignored=ignored-only -E "!($NIGHTLY_TESTS)" --partition hash:"${{ matrix.test }}"/17 --no-tests=warn
224224
shell: bash
225225
env:
226226
POWDR_STD: ${{ github.workspace }}/std/

Diff for: ‎ast/src/analyzed/mod.rs

+13
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,19 @@ impl<T> Analyzed<T> {
136136
.collect()
137137
}
138138

139+
/// Tries to resolve a symbol by name. Does not support individual array elements,
140+
/// just plain symbols. Also supports intermediate columns.
141+
pub fn try_symbol_by_name(&self, name: &str) -> Option<&Symbol> {
142+
self.definitions
143+
.get(name)
144+
.map(|(symbol, _)| symbol)
145+
.or_else(|| {
146+
self.intermediate_columns
147+
.get(name)
148+
.map(|(symbol, _)| symbol)
149+
})
150+
}
151+
139152
pub fn constant_polys_in_source_order(
140153
&self,
141154
) -> impl Iterator<Item = &(Symbol, Option<FunctionValueDefinition>)> {

Diff for: ‎executor/src/witgen/jit/affine_symbolic_expression.rs

+63-36
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use std::{
66

77
use itertools::Itertools;
88
use num_traits::Zero;
9-
use powdr_number::{log2_exact, FieldElement};
9+
use powdr_number::{log2_exact, FieldElement, LargeInt};
1010

1111
use crate::witgen::jit::effect::Assertion;
1212

@@ -243,66 +243,93 @@ impl<T: FieldElement, V: Ord + Clone + Display> AffineSymbolicExpression<T, V> {
243243
.coefficients
244244
.iter()
245245
.map(|(var, coeff)| {
246-
let c = coeff.try_to_number()?;
246+
let coeff = coeff.try_to_number()?;
247247
let rc = self.range_constraints.get(var)?;
248-
Some((var.clone(), c, rc))
248+
let is_negative = !coeff.is_in_lower_half();
249+
let coeff_abs = if is_negative { -coeff } else { coeff };
250+
// We could work with non-powers of two, but it would require
251+
// division instead of shifts.
252+
let exponent = log2_exact(coeff_abs.to_arbitrary_integer())?;
253+
// We negate here because we are solving
254+
// c_1 * x_1 + c_2 * x_2 + ... + offset = 0,
255+
// instead of
256+
// c_1 * x_1 + c_2 * x_2 + ... = offset.
257+
Some((var.clone(), rc, !is_negative, coeff_abs, exponent))
249258
})
250259
.collect::<Option<Vec<_>>>();
251260
let Some(constrained_coefficients) = constrained_coefficients else {
252261
return Ok(ProcessResult::empty());
253262
};
254263

264+
// If the offset is a known number, we gradually remove the
265+
// components from this number.
266+
let mut offset = self.offset.try_to_number();
267+
let mut concrete_assignments = vec![];
268+
255269
// Check if they are mutually exclusive and compute assignments.
256270
let mut covered_bits: <T as FieldElement>::Integer = 0.into();
257271
let mut components = vec![];
258-
for (variable, coeff, constraint) in constrained_coefficients {
259-
let is_negative = !coeff.is_in_lower_half();
260-
let coeff_abs = if is_negative { -coeff } else { coeff };
261-
let Some(exponent) = log2_exact(coeff_abs.to_arbitrary_integer()) else {
262-
// We could work with non-powers of two, but it would require
263-
// division instead of shifts.
264-
return Ok(ProcessResult::empty());
265-
};
272+
for (variable, constraint, is_negative, coeff_abs, exponent) in constrained_coefficients
273+
.into_iter()
274+
.sorted_by_key(|(_, _, _, _, exponent)| *exponent)
275+
{
266276
let bit_mask = *constraint.multiple(coeff_abs).mask();
267277
if !(bit_mask & covered_bits).is_zero() {
268278
// Overlapping range constraints.
269279
return Ok(ProcessResult::empty());
270280
} else {
271281
covered_bits |= bit_mask;
272282
}
273-
components.push(BitDecompositionComponent {
274-
variable,
275-
// We negate here because we are solving
276-
// c_1 * x_1 + c_2 * x_2 + ... + offset = 0,
277-
// instead of
278-
// c_1 * x_1 + c_2 * x_2 + ... = offset.
279-
is_negative: !is_negative,
280-
exponent: exponent as u64,
281-
bit_mask,
282-
});
283+
284+
// If the offset is a known number, we create concrete assignments and modify the offset.
285+
// if it is not known, we return a BitDecomposition effect.
286+
if let Some(offset) = &mut offset {
287+
let mut component = if is_negative { -*offset } else { *offset }.to_integer();
288+
if component > (T::modulus() - 1.into()) >> 1 {
289+
// Convert a signed finite field element into two's complement.
290+
// a regular subtraction would underflow, so we do this.
291+
// We add the difference between negative numbers in the field
292+
// and negative numbers in two's complement.
293+
component += T::Integer::MAX - T::modulus() + 1.into();
294+
};
295+
component &= bit_mask;
296+
concrete_assignments.push(Effect::Assignment(
297+
variable.clone(),
298+
T::from(component >> exponent).into(),
299+
));
300+
if is_negative {
301+
*offset += T::from(component);
302+
} else {
303+
*offset -= T::from(component);
304+
}
305+
} else {
306+
components.push(BitDecompositionComponent {
307+
variable,
308+
is_negative,
309+
exponent: exponent as u64,
310+
bit_mask,
311+
});
312+
}
283313
}
284314

285315
if covered_bits >= T::modulus() {
286316
return Ok(ProcessResult::empty());
287317
}
288318

289-
if !components.iter().any(|c| c.is_negative) {
290-
// If all coefficients are positive and the offset is known, we can check
291-
// that all bits are covered. If not, then there is no way to extract
292-
// the components and thus we have a conflict.
293-
if let Some(offset) = self.offset.try_to_number() {
294-
if offset.to_integer() & !covered_bits != 0.into() {
295-
return Err(Error::ConflictingRangeConstraints);
296-
}
319+
if let Some(offset) = offset {
320+
if offset != 0.into() {
321+
return Err(Error::ConstraintUnsatisfiable);
297322
}
323+
assert_eq!(concrete_assignments.len(), self.coefficients.len());
324+
Ok(ProcessResult::complete(concrete_assignments))
325+
} else {
326+
Ok(ProcessResult::complete(vec![Effect::BitDecomposition(
327+
BitDecomposition {
328+
value: self.offset.clone(),
329+
components,
330+
},
331+
)]))
298332
}
299-
300-
Ok(ProcessResult::complete(vec![Effect::BitDecomposition(
301-
BitDecomposition {
302-
value: self.offset.clone(),
303-
components,
304-
},
305-
)]))
306333
}
307334

308335
fn transfer_constraints(&self) -> Option<Effect<T, V>> {

Diff for: ‎executor/src/witgen/jit/block_machine_processor.rs

+91-28
Original file line numberDiff line numberDiff line change
@@ -167,7 +167,6 @@ impl<'a, T: FieldElement> BlockMachineProcessor<'a, T> {
167167
.filter_map(|(i, is_input)| (!is_input).then_some(Variable::Param(i)))
168168
.collect_vec();
169169
let mut result = Processor::new(
170-
self.fixed_data,
171170
identities,
172171
queue_items,
173172
requested_known.iter().cloned(),
@@ -513,29 +512,31 @@ main_binary::operation_id[3] = params[0];
513512
main_binary::A[3] = params[1];
514513
main_binary::B[3] = params[2];
515514
main_binary::operation_id[2] = main_binary::operation_id[3];
515+
2**0 * main_binary::A[2] + 2**24 * main_binary::A_byte[2] := main_binary::A[3];
516+
2**0 * main_binary::B[2] + 2**24 * main_binary::B_byte[2] := main_binary::B[3];
517+
main_binary::operation_id_next[2] = main_binary::operation_id[3];
518+
call_var(9, 2, 1) = main_binary::A_byte[2];
519+
call_var(9, 2, 2) = main_binary::B_byte[2];
520+
call_var(9, 2, 0) = main_binary::operation_id_next[2];
516521
main_binary::operation_id[1] = main_binary::operation_id[2];
522+
2**0 * main_binary::A[1] + 2**16 * main_binary::A_byte[1] := main_binary::A[2];
523+
2**0 * main_binary::B[1] + 2**16 * main_binary::B_byte[1] := main_binary::B[2];
524+
main_binary::operation_id_next[1] = main_binary::operation_id[2];
517525
main_binary::operation_id[0] = main_binary::operation_id[1];
518-
main_binary::operation_id_next[-1] = main_binary::operation_id[0];
519-
call_var(9, -1, 0) = main_binary::operation_id_next[-1];
520526
main_binary::operation_id_next[0] = main_binary::operation_id[1];
521-
call_var(9, 0, 0) = main_binary::operation_id_next[0];
522-
main_binary::operation_id_next[1] = main_binary::operation_id[2];
523-
call_var(9, 1, 0) = main_binary::operation_id_next[1];
524-
2**24 * main_binary::A_byte[2] + 2**0 * main_binary::A[2] := main_binary::A[3];
525-
call_var(9, 2, 1) = main_binary::A_byte[2];
526-
2**16 * main_binary::A_byte[1] + 2**0 * main_binary::A[1] := main_binary::A[2];
527+
2**0 * main_binary::A[0] + 2**8 * main_binary::A_byte[0] := main_binary::A[1];
527528
call_var(9, 1, 1) = main_binary::A_byte[1];
528-
2**8 * main_binary::A_byte[0] + 2**0 * main_binary::A[0] := main_binary::A[1];
529-
call_var(9, 0, 1) = main_binary::A_byte[0];
530-
main_binary::A_byte[-1] = main_binary::A[0];
531-
call_var(9, -1, 1) = main_binary::A_byte[-1];
532-
2**24 * main_binary::B_byte[2] + 2**0 * main_binary::B[2] := main_binary::B[3];
533-
call_var(9, 2, 2) = main_binary::B_byte[2];
534-
2**16 * main_binary::B_byte[1] + 2**0 * main_binary::B[1] := main_binary::B[2];
529+
2**0 * main_binary::B[0] + 2**8 * main_binary::B_byte[0] := main_binary::B[1];
535530
call_var(9, 1, 2) = main_binary::B_byte[1];
536-
2**8 * main_binary::B_byte[0] + 2**0 * main_binary::B[0] := main_binary::B[1];
537-
call_var(9, 0, 2) = main_binary::B_byte[0];
531+
call_var(9, 1, 0) = main_binary::operation_id_next[1];
532+
main_binary::operation_id_next[-1] = main_binary::operation_id[0];
533+
call_var(9, 0, 0) = main_binary::operation_id_next[0];
534+
main_binary::A_byte[-1] = main_binary::A[0];
535+
call_var(9, 0, 1) = main_binary::A_byte[0];
538536
main_binary::B_byte[-1] = main_binary::B[0];
537+
call_var(9, 0, 2) = main_binary::B_byte[0];
538+
call_var(9, -1, 0) = main_binary::operation_id_next[-1];
539+
call_var(9, -1, 1) = main_binary::A_byte[-1];
539540
call_var(9, -1, 2) = main_binary::B_byte[-1];
540541
machine_call(2, [Known(call_var(9, -1, 0)), Known(call_var(9, -1, 1)), Known(call_var(9, -1, 2)), Unknown(call_var(9, -1, 3))]);
541542
main_binary::C_byte[-1] = call_var(9, -1, 3);
@@ -546,8 +547,6 @@ main_binary::C[1] = (main_binary::C[0] + (main_binary::C_byte[0] * 256));
546547
machine_call(2, [Known(call_var(9, 1, 0)), Known(call_var(9, 1, 1)), Known(call_var(9, 1, 2)), Unknown(call_var(9, 1, 3))]);
547548
main_binary::C_byte[1] = call_var(9, 1, 3);
548549
main_binary::C[2] = (main_binary::C[1] + (main_binary::C_byte[1] * 65536));
549-
main_binary::operation_id_next[2] = main_binary::operation_id[3];
550-
call_var(9, 2, 0) = main_binary::operation_id_next[2];
551550
machine_call(2, [Known(call_var(9, 2, 0)), Known(call_var(9, 2, 1)), Known(call_var(9, 2, 2)), Unknown(call_var(9, 2, 3))]);
552551
main_binary::C_byte[2] = call_var(9, 2, 3);
553552
main_binary::C[3] = (main_binary::C[2] + (main_binary::C_byte[2] * 16777216));
@@ -608,16 +607,16 @@ params[1] = Sub::b[0];"
608607
assert_eq!(
609608
format_code(&code),
610609
"SubM::a[0] = params[0];
611-
2**8 * SubM::b[0] + 2**0 * SubM::c[0] := SubM::a[0];
610+
2**0 * SubM::c[0] + 2**8 * SubM::b[0] := SubM::a[0];
612611
params[1] = SubM::b[0];
613612
params[2] = SubM::c[0];
614613
call_var(1, 0, 0) = SubM::c[0];
615-
machine_call(2, [Known(call_var(1, 0, 0))]);
614+
SubM::c[1] = SubM::c[0];
616615
SubM::b[1] = SubM::b[0];
617616
call_var(1, 1, 0) = SubM::b[1];
618-
SubM::c[1] = SubM::c[0];
619-
machine_call(2, [Known(call_var(1, 1, 0))]);
620-
SubM::a[1] = ((SubM::b[1] * 256) + SubM::c[1]);"
617+
SubM::a[1] = ((SubM::b[1] * 256) + SubM::c[1]);
618+
machine_call(2, [Known(call_var(1, 0, 0))]);
619+
machine_call(2, [Known(call_var(1, 1, 0))]);"
621620
);
622621
}
623622

@@ -671,15 +670,15 @@ machine_call(3, [Known(call_var(3, 0, 0))]);"
671670
code,
672671
"S::a[0] = params[0];
673672
S::b[0] = 0;
674-
params[1] = 0;
675673
S::b[1] = 0;
676674
S::c[0] = 1;
677-
params[2] = 1;
678675
S::b[2] = 0;
679676
S::c[1] = 1;
680677
S::b[3] = 8;
681678
S::c[2] = 1;
682-
S::c[3] = 9;"
679+
S::c[3] = 9;
680+
params[1] = 0;
681+
params[2] = 1;"
683682
);
684683
}
685684

@@ -817,4 +816,68 @@ S::Z[0] = params[1];
817816
params[2] = S::carry[0];"
818817
);
819818
}
819+
820+
#[test]
821+
fn bit_decomp_negative_concrete() {
822+
let input = "
823+
namespace Main(256);
824+
col witness a, b, c;
825+
[a, b, c] is [S.Y, S.Z, S.carry];
826+
namespace S(256);
827+
let BYTE: col = |i| i & 0xff;
828+
let X;
829+
let Y;
830+
let Z;
831+
Y = 19;
832+
Z = 16;
833+
let carry;
834+
carry * (1 - carry) = 0;
835+
[ X ] in [ BYTE ];
836+
[ Y ] in [ BYTE ];
837+
[ Z ] in [ BYTE ];
838+
X + Y = Z + 256 * carry;
839+
";
840+
let code = format_code(&generate_for_block_machine(input, "S", 2, 1).unwrap().code);
841+
assert_eq!(
842+
code,
843+
"\
844+
S::Y[0] = params[0];
845+
S::Z[0] = params[1];
846+
S::X[0] = 253;
847+
S::carry[0] = 1;
848+
params[2] = 1;"
849+
);
850+
}
851+
852+
#[test]
853+
fn bit_decomp_negative_concrete_2() {
854+
let input = "
855+
namespace Main(256);
856+
col witness a, b, c;
857+
[a, b, c] is [S.Y, S.Z, S.carry];
858+
namespace S(256);
859+
let BYTE: col = |i| i & 0xff;
860+
let X;
861+
let Y;
862+
let Z;
863+
Y = 1;
864+
Z = 16;
865+
let carry;
866+
carry * (1 - carry) = 0;
867+
[ X ] in [ BYTE ];
868+
[ Y ] in [ BYTE ];
869+
[ Z ] in [ BYTE ];
870+
X + Y = Z + 256 * carry;
871+
";
872+
let code = format_code(&generate_for_block_machine(input, "S", 2, 1).unwrap().code);
873+
assert_eq!(
874+
code,
875+
"\
876+
S::Y[0] = params[0];
877+
S::Z[0] = params[1];
878+
S::X[0] = 15;
879+
S::carry[0] = 0;
880+
params[2] = 0;"
881+
);
882+
}
820883
}

0 commit comments

Comments
 (0)