|
1 | 1 | use crate::tower_verifier::binding::PointAndEvalVariable; |
2 | 2 | use crate::zkvm_verifier::binding::ZKVMChipProofInputVariable; |
| 3 | +use ceno_mle::StructuralWitInType::{ |
| 4 | + EqualDistanceSequence, InnerRepeatingIncrementalSequence, OuterRepeatingIncrementalSequence, |
| 5 | +}; |
3 | 6 | use ceno_mle::{Expression, Fixed, Instance}; |
4 | 7 | use ceno_zkvm::structs::{ChallengeId, WitnessId}; |
5 | 8 | use ff_ext::ExtensionField; |
@@ -573,10 +576,11 @@ pub fn evaluate_ceno_expr<C: Config, T>( |
573 | 576 | match expr { |
574 | 577 | Expression::Fixed(f) => fixed_in(builder, f), |
575 | 578 | Expression::WitIn(witness_id) => wit_in(builder, *witness_id), |
576 | | - Expression::StructuralWitIn(witness_id, max_len, offset, multi_factor) => { |
577 | | - structural_wit_in(builder, *witness_id, *max_len, *offset, *multi_factor) |
| 579 | + Expression::StructuralWitIn(witness_id, _) => { |
| 580 | + structural_wit_in(builder, *witness_id, 0, 0, 0) |
578 | 581 | } |
579 | 582 | Expression::Instance(i) => instance(builder, *i), |
| 583 | + Expression::InstanceScalar(i) => instance(builder, *i), |
580 | 584 | Expression::Constant(scalar) => match scalar { |
581 | 585 | Either::Left(s) => constant(builder, E::from_base(*s)), |
582 | 586 | Either::Right(s) => constant(builder, *s), |
@@ -688,7 +692,7 @@ pub fn evaluate_ceno_expr<C: Config, T>( |
688 | 692 | } |
689 | 693 |
|
690 | 694 | /// evaluate MLE M(x0, x1, x2, ..., xn) address vector with it evaluation format a*[0, 1, 2, 3, ....2^n-1] + b |
691 | | -/// on r = [r0, r1, r2, ...rn] succintly |
| 695 | +/// on r = [r0, r1, r2, ...rn] succinctly |
692 | 696 | /// a, b, is constant |
693 | 697 | /// the result M(r0, r1,... rn) = r0 + r1 * 2 + r2 * 2^2 + .... rn * 2^n |
694 | 698 | pub fn eval_wellform_address_vec<C: Config>( |
@@ -722,6 +726,62 @@ pub fn eval_wellform_address_vec<C: Config>( |
722 | 726 | res |
723 | 727 | } |
724 | 728 |
|
| 729 | +/// Evaluate MLE M(x0, x1, ..., xn) whose evaluations are [0, 0, 1, 1, 2, 2, 2, 2, ...] |
| 730 | +/// on r = [r0, r1, r2, ... rn] succinctly |
| 731 | +pub fn eval_stacked_constant<C: Config>( |
| 732 | + builder: &mut Builder<C>, |
| 733 | + r: &Array<C, Ext<C::F, C::EF>>, |
| 734 | +) -> Ext<C::F, C::EF> { |
| 735 | + let one: Ext<C::F, C::EF> = builder.constant(C::EF::ONE); |
| 736 | + let res: Ext<C::F, C::EF> = builder.constant(C::EF::ZERO); |
| 737 | + let loop_i: Ext<C::F, C::EF> = builder.constant(C::EF::ONE); |
| 738 | + |
| 739 | + builder.range(1, r.len()).for_each(|i_vec, builder| { |
| 740 | + let i: Var<C::N> = builder.eval(i_vec[0]); |
| 741 | + let ri = builder.get(r, i); |
| 742 | + // res = res * (1-ri) + ri * i |
| 743 | + builder.assign(&res, res * (one.clone() - ri.clone()) + ri * loop_i); |
| 744 | + builder.assign(&loop_i, loop_i + one); |
| 745 | + }); |
| 746 | + |
| 747 | + res |
| 748 | +} |
| 749 | + |
| 750 | +/// Evaluate MLE M(x0, x1, ..., xn) whose evaluations are [0, 0, 0, 1, 0, 1, 2, 3, ...] |
| 751 | +/// on r = [r0, r1, r2, ... rn] succinctly |
| 752 | +pub fn eval_stacked_wellform_address_vec<C: Config>( |
| 753 | + builder: &mut Builder<C>, |
| 754 | + r: &Array<C, Ext<C::F, C::EF>>, |
| 755 | +) -> Ext<C::F, C::EF> { |
| 756 | + let one: Ext<C::F, C::EF> = builder.constant(C::EF::ONE); |
| 757 | + |
| 758 | + let two: Ext<C::F, C::EF> = builder.constant(C::EF::TWO); |
| 759 | + let pow_two: Ext<C::F, C::EF> = builder.constant(C::EF::ONE); |
| 760 | + |
| 761 | + // compute \sum_j r_j * 2^j in an incremental way |
| 762 | + let well_formed_inc: Ext<C::F, C::EF> = builder.constant(C::EF::ZERO); |
| 763 | + let res: Ext<C::F, C::EF> = builder.constant(C::EF::ZERO); |
| 764 | + |
| 765 | + builder.range(1, r.len()).for_each(|i_vec, builder| { |
| 766 | + let i: Var<C::N> = builder.eval(i_vec[0]); |
| 767 | + let i_minus_1: Var<C::N> = builder.eval(i.clone() - RVar::from(1)); |
| 768 | + let ri = builder.get(r, i); |
| 769 | + let r_i_minus_1 = builder.get(r, i_minus_1); |
| 770 | + |
| 771 | + // well_formed_inc += 2^{i-1} * r_{i-1} |
| 772 | + builder.assign(&well_formed_inc, well_formed_inc + pow_two * r_i_minus_1); |
| 773 | + builder.assign(&pow_two, pow_two * two); |
| 774 | + |
| 775 | + // res = res * (1-ri) + ri * (\sum_{j < i} 2^j * rj) |
| 776 | + builder.assign( |
| 777 | + &res, |
| 778 | + res * (one - ri.clone()) + ri * well_formed_inc.clone(), |
| 779 | + ); |
| 780 | + }); |
| 781 | + |
| 782 | + res |
| 783 | +} |
| 784 | + |
725 | 785 | pub fn max_usize_vec<C: Config>(builder: &mut Builder<C>, vec: Vec<Usize<C::N>>) -> Usize<C::N> { |
726 | 786 | assert!(vec.len() > 0); |
727 | 787 |
|
@@ -968,3 +1028,66 @@ pub fn extend<C: Config>( |
968 | 1028 |
|
969 | 1029 | out |
970 | 1030 | } |
| 1031 | + |
| 1032 | +#[cfg(test)] |
| 1033 | +mod tests { |
| 1034 | + use ff_ext::BabyBearExt4; |
| 1035 | + use openvm_circuit::arch::{instructions::program::Program, SystemConfig, VmExecutor}; |
| 1036 | + use openvm_native_circuit::{Native, NativeConfig}; |
| 1037 | + use openvm_native_compiler::{ |
| 1038 | + asm::{AsmBuilder, AsmCompiler}, |
| 1039 | + conversion::{convert_program, CompilerOptions}, |
| 1040 | + ir::Ext, |
| 1041 | + }; |
| 1042 | + use p3_baby_bear::BabyBear; |
| 1043 | + use p3_field::FieldAlgebra; |
| 1044 | + |
| 1045 | + use crate::arithmetics::eval_stacked_wellform_address_vec; |
| 1046 | + |
| 1047 | + type E = BabyBearExt4; |
| 1048 | + type F = BabyBear; |
| 1049 | + |
| 1050 | + fn run_test_program(program: Program<F>) { |
| 1051 | + let system_config = SystemConfig::default() |
| 1052 | + .with_public_values(20) |
| 1053 | + .with_max_segment_len((1 << 22) - 100); |
| 1054 | + let config = NativeConfig::new(system_config, Native); |
| 1055 | + |
| 1056 | + let executor = VmExecutor::<F, NativeConfig>::new(config); |
| 1057 | + |
| 1058 | + executor |
| 1059 | + .execute_and_then(program.clone(), vec![], |_, seg| Ok(seg), |err| err) |
| 1060 | + .unwrap(); |
| 1061 | + } |
| 1062 | + |
| 1063 | + #[test] |
| 1064 | + fn test_structural_witness() { |
| 1065 | + let mut builder = AsmBuilder::<F, E>::default(); |
| 1066 | + |
| 1067 | + // eval_stacked_wellform_address_vec |
| 1068 | + let r = builder.dyn_array(4); |
| 1069 | + let expected = vec![0, 0, 0, 1, 0, 1, 2, 3, 0, 1, 2, 3, 4, 5, 6, 7]; |
| 1070 | + |
| 1071 | + for i in 0..16 { |
| 1072 | + for b in 0..4 { |
| 1073 | + let bit = (i >> b) & 1; |
| 1074 | + let bit: Ext<F, E> = builder.constant(E::from_canonical_u32(bit)); |
| 1075 | + builder.set_value(&r, b, bit); |
| 1076 | + } |
| 1077 | + let val = eval_stacked_wellform_address_vec(&mut builder, &r); |
| 1078 | + let expected_val: Ext<F, E> = |
| 1079 | + builder.constant(E::from_canonical_u32(expected[i as usize])); |
| 1080 | + |
| 1081 | + builder.assert_ext_eq(val, expected_val); |
| 1082 | + } |
| 1083 | + builder.halt(); |
| 1084 | + |
| 1085 | + let options = CompilerOptions::default(); |
| 1086 | + let mut compiler = AsmCompiler::new(options.word_size); |
| 1087 | + compiler.build(builder.operations); |
| 1088 | + let asm_code = compiler.code(); |
| 1089 | + |
| 1090 | + let program: Program<F> = convert_program(asm_code, options); |
| 1091 | + run_test_program(program); |
| 1092 | + } |
| 1093 | +} |
0 commit comments