diff --git a/src/gadget.hpp b/src/gadget.hpp index 5d43108..681949d 100644 --- a/src/gadget.hpp +++ b/src/gadget.hpp @@ -3,10 +3,32 @@ using namespace libsnark; +template +class sodoku_cell_gadget : public gadget { +public: + pb_linear_combination &number; + unsigned int dimension; + + /* + This is an array of bits which indicates whether this + cell is a particular number in the dimension. It is + the size of the dimension N^2 of the puzzle. Only one + bit is set. + */ + pb_variable_array flags; + + sodoku_cell_gadget(protoboard &pb, + unsigned int dimension, + pb_linear_combination &number + ); + void generate_r1cs_constraints(); + void generate_r1cs_witness(); +}; + template class l_gadget : public gadget { public: - unsigned int dimension; /* N */ + unsigned int dimension; pb_variable_array input_as_field_elements; /* R1CS input */ pb_variable_array input_as_bits; /* unpacked R1CS input */ @@ -18,6 +40,8 @@ public: std::vector> puzzle_numbers; std::vector> solution_numbers; + std::vector>> cells; + pb_variable_array puzzle_enforce; diff --git a/src/gadget.tcc b/src/gadget.tcc index 0fde5a1..d04d54f 100644 --- a/src/gadget.tcc +++ b/src/gadget.tcc @@ -1,3 +1,34 @@ +template +sodoku_cell_gadget::sodoku_cell_gadget(protoboard &pb, + unsigned int dimension, + pb_linear_combination &number + ) : gadget(pb, FMT(annotation_prefix, " sodoku_cell_gadget")), + number(number), dimension(dimension) +{ + flags.allocate(pb, dimension, "flags for each possible number"); +} + +template +void sodoku_cell_gadget::generate_r1cs_constraints() +{ + for (unsigned int i = 0; i < dimension; i++) { + generate_boolean_r1cs_constraint(this->pb, flags[i], "enforcement bitness"); + this->pb.add_r1cs_constraint(r1cs_constraint(number - (i+1), flags[i], 0), "enforcement"); + } +} + +template +void sodoku_cell_gadget::generate_r1cs_witness() +{ + for (unsigned int i = 0; i < dimension; i++) { + if (this->pb.lc_val(number) == (i+1)) { + this->pb.val(flags[i]) = FieldT::one(); + } else { + this->pb.val(flags[i]) = FieldT::zero(); + } + } +} + template l_gadget::l_gadget(protoboard &pb, unsigned int n) : gadget(pb, FMT(annotation_prefix, " l_gadget")) @@ -17,6 +48,7 @@ l_gadget::l_gadget(protoboard &pb, unsigned int n) : puzzle_numbers.resize(dimension*dimension); solution_values.resize(dimension*dimension); solution_numbers.resize(dimension*dimension); + cells.resize(dimension*dimension); for (unsigned int i = 0; i < (dimension*dimension); i++) { puzzle_values[i].allocate(pb, 8, "puzzle_values[i]"); @@ -26,6 +58,8 @@ l_gadget::l_gadget(protoboard &pb, unsigned int n) : solution_numbers[i].assign(pb, pb_packing_sum(pb_variable_array(solution_values[i].rbegin(), solution_values[i].rend()))); input_as_bits.insert(input_as_bits.end(), puzzle_values[i].begin(), puzzle_values[i].end()); + + cells[i].reset(new sodoku_cell_gadget(this->pb, dimension, solution_numbers[i])); } assert(input_as_bits.size() == input_size_in_bits); @@ -51,6 +85,9 @@ void l_gadget::generate_r1cs_constraints() // solution_numbers[i] must equal puzzle_numbers[i] if puzzle_enforce[i] is 1 this->pb.add_r1cs_constraint(r1cs_constraint(puzzle_enforce[i], (solution_numbers[i] - puzzle_numbers[i]), 0), "enforcement equality"); + + // enforce cell constraints + cells[i]->generate_r1cs_constraints(); } unpack_inputs->generate_r1cs_constraints(true); @@ -83,6 +120,8 @@ void l_gadget::generate_r1cs_witness(std::vector &input_puzz } this->pb.val(puzzle_enforce[i]) = enforce ? FieldT::one() : FieldT::zero(); + + cells[i]->generate_r1cs_witness(); } unpack_inputs->generate_r1cs_witness_from_bits();