Skip to content

Commit

Permalink
feat: mul_by_01234 (#731)
Browse files Browse the repository at this point in the history
* WIP: need to apply FieldExtension on Fq, Fq2 for mul_013_by_013 test

* Fix mul_013_by_013

* WIP: isolate issue

* Fix xi

* Update IntAdd

* fix

* Clean up

* Add chip for mul_013_by_013

* Update w/ new ExprBuilderConfig paradigm

* Remove extraneous items

* Fix lints

* WIP: coefficient order

* Fix coefficients

* Add chip items

* address PR comments

* Additional fixes

* Rebase

* Fix coefficients

* Rebase

* Rebase to updated mul_013_by_013

* Remove extraneous items

* Remove clone

* Update var names

* Fix lints

* Add comments

* Add todo comment

---------

Co-authored-by: luffykai <[email protected]>
  • Loading branch information
ytham and luffykai authored Nov 1, 2024
1 parent 09dad3b commit dd3e361
Show file tree
Hide file tree
Showing 6 changed files with 336 additions and 8 deletions.
103 changes: 100 additions & 3 deletions circuits/ecc/src/field_extension/fp12.rs
Original file line number Diff line number Diff line change
Expand Up @@ -88,9 +88,10 @@ impl Fp12 {
}

pub fn mul(&mut self, other: &mut Fp12, xi: [isize; 2]) -> Fp12 {
// c0 = cs0co0 + xi(cs1co2 + cs2co1 + cs3co5 + cs4co4 + cs5co5)
// c1 = cs0co1 + cs1co0 + cs3co0 + xi(cs2co2 + cs4co5 + cs5co4)
// c2 = cs0co2 + cs1co1 + cs2co0 + cs3co4 +cs4co3 + xi(cs5co5)
// The following multiplication is hand-derived for Fp12 * Fp12:
// c0 = cs0co0 + xi(cs1co2 + cs2co1 + cs3co5 + cs4co4 + cs5co3)
// c1 = cs0co1 + cs1co0 + cs3co3 + xi(cs2co2 + cs4co5 + cs5co4)
// c2 = cs0co2 + cs1co1 + cs2co0 + cs3co4 + cs4co3 + xi(cs5co5)
// c3 = cs0co3 + cs3co0 + xi(cs1co5 + cs2co4 + cs4co2 + cs5co1)
// c4 = cs0co4 + cs1co3 + cs3co1 + cs4co0 + xi(cs2co5 + cs5co2)
// c5 = cs0co5 + cs1co4 + cs2co3 + cs3co2 + cs4co1 + cs5co0
Expand Down Expand Up @@ -120,6 +121,102 @@ impl Fp12 {
}
}

pub fn mul_by_01234(
&mut self,
x0: &mut Fp2,
x1: &mut Fp2,
x2: &mut Fp2,
x3: &mut Fp2,
x4: &mut Fp2,
xi: [isize; 2],
) -> Fp12 {
// c0 = cs0co0 + xi(cs1co2 + cs2co1 + cs4co4 + cs5co3)
// c1 = cs0co1 + cs1co0 + cs3co3 + xi(cs2co2 + cs5co4)
// c2 = cs0co2 + cs1co1 + cs2co0 + cs3co4 + cs4co3
// c3 = cs0co3 + cs3co0 + xi(cs2co4 + cs4co2 + cs5co1)
// c4 = cs0co4 + cs1co3 + cs3co1 + cs4co0 + xi(cs5co2)
// c5 = cs1co4 + cs2co3 + cs3co2 + cs4co1 + cs5co0
// where cs*: self.c*

// we update the order of the coefficients to match the Fp12 coefficient ordering:
// Fp12 {
// c0: Fp6 {
// c0: x0,
// c1: x2,
// c2: x4,
// },
// c1: Fp6 {
// c0: x1,
// c1: x3,
// c2: x5,
// },
// }
let o0 = x0;
let o1 = x2;
let o2 = x4;
let o3 = x1;
let o4 = x3;

let c0 = self.c0.mul(o0).add(
&mut self
.c1
.mul(o2)
.add(&mut self.c2.mul(o1))
.add(&mut self.c4.mul(o4))
.add(&mut self.c5.mul(o3))
.int_mul(xi),
);

let c1 = self
.c0
.mul(o1)
.add(&mut self.c1.mul(o0))
.add(&mut self.c3.mul(o3))
.add(&mut self.c2.mul(o2).add(&mut self.c5.mul(o4)).int_mul(xi));

let c2 = self
.c0
.mul(o2)
.add(&mut self.c1.mul(o1))
.add(&mut self.c2.mul(o0))
.add(&mut self.c3.mul(o4))
.add(&mut self.c4.mul(o3));

let c3 = self.c0.mul(o3).add(&mut self.c3.mul(o0)).add(
&mut self
.c2
.mul(o4)
.add(&mut self.c4.mul(o2))
.add(&mut self.c5.mul(o1))
.int_mul(xi),
);

let c4 = self
.c0
.mul(o4)
.add(&mut self.c1.mul(o3))
.add(&mut self.c3.mul(o1))
.add(&mut self.c4.mul(o0))
.add(&mut self.c5.mul(o2).int_mul(xi));

let c5 = self
.c1
.mul(o4)
.add(&mut self.c2.mul(o3))
.add(&mut self.c3.mul(o2))
.add(&mut self.c4.mul(o1))
.add(&mut self.c5.mul(o0));

Fp12 {
c0,
c1,
c2,
c3,
c4,
c5,
}
}

pub fn div(&mut self, _other: &mut Fp12, _xi: [isize; 2]) -> Fp12 {
todo!()
}
Expand Down
19 changes: 18 additions & 1 deletion vm/src/arch/chip_set.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,10 @@ use crate::{
},
intrinsics::{
ecc::{
pairing::{EcLineMul013By013Chip, MillerDoubleAndAddStepChip, MillerDoubleStepChip},
pairing::{
EcLineMul013By013Chip, EcLineMulBy01234Chip, MillerDoubleAndAddStepChip,
MillerDoubleStepChip,
},
sw::{EcAddNeChip, EcDoubleChip},
},
hashes::{keccak::hasher::KeccakVmChip, poseidon2::Poseidon2Chip},
Expand Down Expand Up @@ -823,6 +826,20 @@ impl VmConfig {
executors.insert(global_opcode_idx, chip.clone().into());
chips.push(AxVmChip::EcLineMul013By013(chip));
}
ExecutorName::EcLineMulBy01234 => {
let chip = Rc::new(RefCell::new(EcLineMulBy01234Chip::new(
Rv32VecHeapAdapterChip::<F, 2, 12, 12, 32, 32>::new(
execution_bus,
program_bus,
memory_controller.clone(),
),
memory_controller.clone(),
config32,
class_offset,
)));
executors.insert(global_opcode_idx, chip.clone().into());
chips.push(AxVmChip::EcLineMulBy01234(chip));
}
_ => unreachable!("Unsupported executor"),
}
}
Expand Down
7 changes: 6 additions & 1 deletion vm/src/arch/chips.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,10 @@ use crate::{
arch::ExecutionState,
intrinsics::{
ecc::{
pairing::{EcLineMul013By013Chip, MillerDoubleAndAddStepChip, MillerDoubleStepChip},
pairing::{
EcLineMul013By013Chip, EcLineMulBy01234Chip, MillerDoubleAndAddStepChip,
MillerDoubleStepChip,
},
sw::{EcAddNeChip, EcDoubleChip},
},
hashes::{keccak::hasher::KeccakVmChip, poseidon2::Poseidon2Chip},
Expand Down Expand Up @@ -114,6 +117,7 @@ pub enum AxVmInstructionExecutor<F: PrimeField32> {
EcAddNeRv32_6x16(Rc<RefCell<EcAddNeChip<F, 6, 16>>>),
EcDoubleRv32_6x16(Rc<RefCell<EcDoubleChip<F, 6, 16>>>),
EcLineMul013By013(Rc<RefCell<EcLineMul013By013Chip<F, 4, 10, 32>>>),
EcLineMulBy01234(Rc<RefCell<EcLineMulBy01234Chip<F, 12, 12, 32>>>),
// 32-bytes or 48-bytes prime.
MillerDoubleStepRv32_32(Rc<RefCell<MillerDoubleStepChip<F, 4, 8, 32>>>),
MillerDoubleStepRv32_48(Rc<RefCell<MillerDoubleStepChip<F, 12, 24, 16>>>),
Expand Down Expand Up @@ -168,6 +172,7 @@ pub enum AxVmChip<F: PrimeField32> {
EcAddNeRv32_6x16(Rc<RefCell<EcAddNeChip<F, 6, 16>>>),
EcDoubleRv32_6x16(Rc<RefCell<EcDoubleChip<F, 6, 16>>>),
EcLineMul013By013(Rc<RefCell<EcLineMul013By013Chip<F, 4, 10, 32>>>),
EcLineMulBy01234(Rc<RefCell<EcLineMulBy01234Chip<F, 12, 12, 32>>>),
// 32-bytes or 48-bytes prime.
MillerDoubleStepRv32_32(Rc<RefCell<MillerDoubleStepChip<F, 4, 8, 32>>>),
MillerDoubleStepRv32_48(Rc<RefCell<MillerDoubleStepChip<F, 12, 24, 16>>>),
Expand Down
2 changes: 2 additions & 0 deletions vm/src/intrinsics/ecc/pairing/line/mod.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
mod mul_013_by_013;
mod mul_by_01234;

pub use mul_013_by_013::*;
pub use mul_by_01234::*;

#[cfg(test)]
mod tests;
101 changes: 101 additions & 0 deletions vm/src/intrinsics/ecc/pairing/line/mul_by_01234.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
use std::{cell::RefCell, rc::Rc};

use ax_circuit_derive::{Chip, ChipUsageGetter};
use ax_circuit_primitives::{
bigint::check_carry_mod_to_zero::CheckCarryModToZeroSubAir, var_range::VariableRangeCheckerBus,
};
use ax_ecc_primitives::{
field_expression::{ExprBuilder, ExprBuilderConfig, FieldExpr},
field_extension::{Fp12, Fp2},
};
use axvm_circuit_derive::InstructionExecutor;
use axvm_ecc_constants::BN254;
use axvm_instructions::PairingOpcode;
use p3_field::PrimeField32;

use crate::{
arch::VmChipWrapper, intrinsics::field_expression::FieldExpressionCoreChip,
rv32im::adapters::Rv32VecHeapAdapterChip, system::memory::MemoryControllerRef,
};

// TODO[yj]: Update to use 10 FE for 2nd input once the adapter change is merged for unbalanced inputs
// Input: 2 Fp12: 2 x 12 field elements
// Output: Fp12 -> 12 field elements
#[derive(Chip, ChipUsageGetter, InstructionExecutor)]
pub struct EcLineMulBy01234Chip<
F: PrimeField32,
const INPUT_BLOCKS: usize,
const OUTPUT_BLOCKS: usize,
const BLOCK_SIZE: usize,
>(
VmChipWrapper<
F,
Rv32VecHeapAdapterChip<F, 2, INPUT_BLOCKS, OUTPUT_BLOCKS, BLOCK_SIZE, BLOCK_SIZE>,
FieldExpressionCoreChip,
>,
);

impl<
F: PrimeField32,
const INPUT_BLOCKS: usize,
const OUTPUT_BLOCKS: usize,
const BLOCK_SIZE: usize,
> EcLineMulBy01234Chip<F, INPUT_BLOCKS, OUTPUT_BLOCKS, BLOCK_SIZE>
{
pub fn new(
adapter: Rv32VecHeapAdapterChip<F, 2, INPUT_BLOCKS, OUTPUT_BLOCKS, BLOCK_SIZE, BLOCK_SIZE>,
memory_controller: MemoryControllerRef<F>,
config: ExprBuilderConfig,
offset: usize,
) -> Self {
let expr = mul_by_01234_expr(
config,
memory_controller.borrow().range_checker.bus(),
BN254.XI,
);
let core = FieldExpressionCoreChip::new(
expr,
offset,
vec![PairingOpcode::MUL_BY_01234 as usize],
vec![],
memory_controller.borrow().range_checker.clone(),
"MulBy01234",
);
Self(VmChipWrapper::new(adapter, core, memory_controller))
}
}

pub fn mul_by_01234_expr(
config: ExprBuilderConfig,
range_bus: VariableRangeCheckerBus,
xi: [isize; 2],
) -> FieldExpr {
config.check_valid();
let builder = ExprBuilder::new(config.clone(), range_bus.range_max_bits);
let builder = Rc::new(RefCell::new(builder));
let subair = CheckCarryModToZeroSubAir::new(
config.modulus,
config.limb_bits,
range_bus.index,
range_bus.range_max_bits,
);

let mut f = Fp12::new(builder.clone());
let mut x0 = Fp2::new(builder.clone());
let mut x1 = Fp2::new(builder.clone());
let mut x2 = Fp2::new(builder.clone());
let mut x3 = Fp2::new(builder.clone());
let mut x4 = Fp2::new(builder.clone());
// x5 is unused; required for input sizes to balance to 12 on the adapter
let _x5 = Fp2::new(builder.clone());

let mut r = f.mul_by_01234(&mut x0, &mut x1, &mut x2, &mut x3, &mut x4, xi);
r.save_output();

let builder = builder.borrow().clone();
FieldExpr {
builder,
check_carry_mod_to_zero: subair,
range_bus,
}
}
Loading

0 comments on commit dd3e361

Please sign in to comment.