diff --git a/src/gates/insertion.rs b/src/gates/insertion.rs index 7cdd0242..ea1d37a7 100644 --- a/src/gates/insertion.rs +++ b/src/gates/insertion.rs @@ -25,14 +25,73 @@ impl InsertionGate { GateRef::new(gate) } - pub fn get, const D: usize>() -> GateRef { - - GateRef::new(InsertionGate) + pub fn wires_insertion_index() -> Range { + 0..D } - pub const CONST_INPUT: usize = 0; + pub fn wires_list_item(i: usize) -> Range { + let start = (i + 1) * D; + start..start + D + } - pub const WIRE_OUTPUT: usize = 0; + fn start_of_intermediate_wires() -> usize { + (i + 2) * D + } + + fn wires_per_round() -> { + // D wires needed for each of cur_index, insert_here, equality_dummy, new_item, new_item_plus_old_item, + // already_inserted, and not_already_inserted + 7 * D + } + + /// The wires corresponding to the "cur_index" variable in the gadget (non-gate) insert function. + pub fn cur_index_for_round_r(r: usize) -> Range { + let intermediate_index = 0; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } + + /// The wires corresponding to the "insert_here" variable in the gadget (non-gate) insert function. + pub fn insert_here_for_round_r(r: usize) -> Range { + let intermediate_index = 1; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } + + /// The wires corresponding to the "equality_dummy" variable in the gadget (non-gate) insert function. + pub fn equality_dummy_for_round_r(r: usize) -> Range { + let intermediate_index = 1; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } + + /// The wires corresponding to the "new_item" variable in the gadget (non-gate) insert function. + pub fn new_item_for_round_r(r: usize) -> Range { + let intermediate_index = 2; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } + + /// The wires corresponding to the "new_item_plus_old_item" variable in the gadget (non-gate) insert function. + pub fn new_item_plus_old_item_for_round_r(r: usize) -> Range { + let intermediate_index = 3; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } + + /// The wires corresponding to the "already_inserted" variable in the gadget (non-gate) insert function. + pub fn already_inserted_for_round_r(r: usize) -> Range { + let intermediate_index = 4; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } + + /// The wires corresponding to the "not_already_inserted" variable in the gadget (non-gate) insert function. + pub fn not_already_inserted_for_round_r(r: usize) -> Range { + let intermediate_index = 5; + let start = start_of_intermediate_wires() + r * wires_per_round() + D * intermediate_index; + start..start + D + } } impl, const D: usize> Gate for InsertionGate { @@ -41,9 +100,28 @@ impl, const D: usize> Gate for InsertionGate { } fn eval_unfiltered(&self, vars: EvaluationVars) -> Vec { - let input = vars.local_constants[Self::CONST_INPUT]; - let output = vars.local_wires[Self::WIRE_OUTPUT]; - vec![output - input] + let insertion_index = vars.get_local_ext_algebra(Self::wires_insertion_index()); + let mut list_items = Vec::new(); + for i in 0..self::vec_size { + list_items.push(vars.get_local_ext_algebra(Self::wires_list_item(i))); + } + + let mut constraints = Vec::new(); + + for r in 0..self::vec_size { + let this_round_cur_index = vars.get_local_ext_algebra(Self::cur_index_for_round_r(r)); + // TODO: set value of cur_index + + let this_round_insert_here = vars.get_local_ext_algebra(Self::insert_here_for_round_r(r)); + // enforce "insert_here = is_equal(cur_index, insertion_index)" + let this_round_equality_dummy = vars.get_local_ext_algebra(Self::equality_dummy_for_round_r(r)); + let computed_insert_here = (this_round_cur_index - insertion_index) * this_round_equality_dummy; + constraints.extend(computed_insert_here - this_round_insert_here).to_basefield_array()); + + + } + + constraints } fn eval_unfiltered_recursively( @@ -51,9 +129,7 @@ impl, const D: usize> Gate for InsertionGate { builder: &mut CircuitBuilder, vars: EvaluationTargets, ) -> Vec> { - let input = vars.local_constants[Self::CONST_INPUT]; - let output = vars.local_wires[Self::WIRE_OUTPUT]; - vec![builder.sub_extension(output, input)] + todo!() } fn generators( @@ -70,11 +146,14 @@ impl, const D: usize> Gate for InsertionGate { } fn num_wires(&self) -> usize { - 1 + let num_input_wires = self.vec_size + 1; // the original vector, and the insertion index + let num_output_wires = self.vec_size + 1; // the final vector, with the inserted element + let num_intermediate_wires = 6 * self.vec_size; // six intermediate variables needed for each element of the vector + self.vec_size + 1 } fn num_constants(&self) -> usize { - 1 + 0 } fn degree(&self) -> usize {