|
| 1 | +use ark_ff::Field; |
| 2 | +use ark_relations::gr1cs::{ |
| 3 | + trace::{ConstraintLayer, TracingMode}, |
| 4 | + ConstraintSystem, ConstraintSystemRef, LinearCombination, SynthesisError, Variable, |
| 5 | +}; |
| 6 | +use ark_test_curves::bls12_381::Fr; |
| 7 | + |
| 8 | +use tracing_subscriber::{fmt, layer::SubscriberExt, Registry}; |
| 9 | + |
| 10 | +fn main() { |
| 11 | + // Set up tracing with a ConstraintLayer |
| 12 | + let constraint_layer = ConstraintLayer::new(TracingMode::All); |
| 13 | + let subscriber = Registry::default() |
| 14 | + .with(fmt::layer()) // Optional: Log formatted output to stdout |
| 15 | + .with(constraint_layer); |
| 16 | + |
| 17 | + tracing::subscriber::set_global_default(subscriber) |
| 18 | + .expect("Failed to set global default subscriber"); |
| 19 | + |
| 20 | + // Initialize a constraint system |
| 21 | + let cs = ConstraintSystem::<Fr>::new_ref(); |
| 22 | + |
| 23 | + // Create input variables |
| 24 | + let p1 = cs.new_input_variable(|| Ok(Fr::from(3u32))).unwrap(); |
| 25 | + let p2 = cs.new_input_variable(|| Ok(Fr::from(4u32))).unwrap(); |
| 26 | + let p3 = cs.new_input_variable(|| Ok(Fr::from(6u32))).unwrap(); |
| 27 | + let p4 = cs.new_input_variable(|| Ok(Fr::from(7u32))).unwrap(); |
| 28 | + |
| 29 | + // Create witness variables |
| 30 | + // Note that w3 has a wrong value |
| 31 | + let w1 = cs.new_witness_variable(|| Ok(Fr::from(2u32))).unwrap(); |
| 32 | + let w2 = cs.new_witness_variable(|| Ok(Fr::from(5u32))).unwrap(); |
| 33 | + let w3 = cs.new_witness_variable(|| Ok(Fr::from(8u32))).unwrap(); |
| 34 | + let w4 = cs.new_witness_variable(|| Ok(Fr::from(9u32))).unwrap(); |
| 35 | + // Create expected result as a witness |
| 36 | + let expected_result = cs.new_input_variable(|| Ok(Fr::from(198))).unwrap(); |
| 37 | + // Build the circuit |
| 38 | + let _result_var = |
| 39 | + generate_constraints(cs.clone(), p1, p2, p3, p4, w1, w2, w3, w4, expected_result).unwrap(); |
| 40 | + let trace = cs.which_predicate_is_unsatisfied().unwrap().unwrap(); |
| 41 | + println!( |
| 42 | + "This is the trace of non-satisfied scenario, Check out the trace:\n{}", |
| 43 | + trace |
| 44 | + ) |
| 45 | +} |
| 46 | +// Function to enforce the overall constraints by combining subcircuits |
| 47 | +#[tracing::instrument(target = "gr1cs")] |
| 48 | +fn generate_constraints<F: Field>( |
| 49 | + cs: ConstraintSystemRef<F>, |
| 50 | + p1: Variable, |
| 51 | + p2: Variable, |
| 52 | + p3: Variable, |
| 53 | + p4: Variable, |
| 54 | + w1: Variable, |
| 55 | + w2: Variable, |
| 56 | + w3: Variable, |
| 57 | + w4: Variable, |
| 58 | + expected_result: Variable, |
| 59 | +) -> Result<Variable, SynthesisError> { |
| 60 | + // Subcircuit 1 |
| 61 | + let subcircuit1_result = enforce_subcircuit1(cs.clone(), p1, p2, w1, w2)?; |
| 62 | + |
| 63 | + // Subcircuit 2 |
| 64 | + let subcircuit2_result = enforce_subcircuit2(cs.clone(), p3, p4, w3, w4)?; |
| 65 | + |
| 66 | + // Final operation: sum the results of the two subcircuits |
| 67 | + let final_result = enforce_addition(cs.clone(), subcircuit1_result, subcircuit2_result)?; |
| 68 | + // Verify that the final result matches the expected result |
| 69 | + cs.enforce_r1cs_constraint( |
| 70 | + LinearCombination::from(final_result), |
| 71 | + LinearCombination::from(Variable::One), |
| 72 | + LinearCombination::from(expected_result), |
| 73 | + )?; |
| 74 | + |
| 75 | + Ok(final_result) |
| 76 | +} |
| 77 | + |
| 78 | +// Enforces the constraints for Subcircuit 1 |
| 79 | +#[tracing::instrument(target = "gr1cs")] |
| 80 | +fn enforce_subcircuit1<F: Field>( |
| 81 | + cs: ConstraintSystemRef<F>, |
| 82 | + p1: Variable, |
| 83 | + p2: Variable, |
| 84 | + w1: Variable, |
| 85 | + w2: Variable, |
| 86 | +) -> Result<Variable, SynthesisError> { |
| 87 | + // let cs = ns!(cs, "subcircuit1").cs(); |
| 88 | + |
| 89 | + // Multiplication gate: p1 * p2 |
| 90 | + let product = enforce_multiplication(cs.clone(), p1, p2)?; |
| 91 | + |
| 92 | + // Addition gate: w1 + w2 |
| 93 | + let sum = enforce_addition(cs.clone(), w1, w2)?; |
| 94 | + |
| 95 | + // Final multiplication: sum * product |
| 96 | + let result = enforce_multiplication(cs, sum, product)?; |
| 97 | + |
| 98 | + Ok(result) |
| 99 | +} |
| 100 | + |
| 101 | +// Enforces the constraints for Subcircuit 2 |
| 102 | +#[tracing::instrument(target = "gr1cs")] |
| 103 | +fn enforce_subcircuit2<F: Field>( |
| 104 | + cs: ConstraintSystemRef<F>, |
| 105 | + p3: Variable, |
| 106 | + p4: Variable, |
| 107 | + w3: Variable, |
| 108 | + w4: Variable, |
| 109 | +) -> Result<Variable, SynthesisError> { |
| 110 | + // let cs = ns!(cs, "subcircuit2").cs(); |
| 111 | + |
| 112 | + // Multiplication gate 1: p3 * w3 |
| 113 | + let product1 = enforce_multiplication(cs.clone(), p3, p4)?; |
| 114 | + |
| 115 | + // Multiplication gate 2: p4 * w4 |
| 116 | + let product2 = enforce_multiplication(cs.clone(), w3, w4)?; |
| 117 | + |
| 118 | + // Final addition: product1 + product2 |
| 119 | + let result = enforce_addition(cs, product1, product2)?; |
| 120 | + |
| 121 | + Ok(result) |
| 122 | +} |
| 123 | + |
| 124 | +// Function to enforce a multiplication constraint |
| 125 | +#[tracing::instrument(target = "gr1cs")] |
| 126 | +fn enforce_multiplication<F: Field>( |
| 127 | + cs: ConstraintSystemRef<F>, |
| 128 | + left: Variable, |
| 129 | + right: Variable, |
| 130 | +) -> Result<Variable, SynthesisError> { |
| 131 | + // let cs = ns!(cs, "multiplication").cs(); |
| 132 | + |
| 133 | + let product = cs.new_witness_variable(|| { |
| 134 | + Ok(cs.assigned_value(left).unwrap() * cs.assigned_value(right).unwrap()) |
| 135 | + })?; // Placeholder for product |
| 136 | + |
| 137 | + cs.enforce_r1cs_constraint( |
| 138 | + LinearCombination::from(left), |
| 139 | + LinearCombination::from(right), |
| 140 | + LinearCombination::from(product), |
| 141 | + )?; |
| 142 | + |
| 143 | + Ok(product) |
| 144 | +} |
| 145 | + |
| 146 | +// Function to enforce an addition constraint |
| 147 | +#[tracing::instrument(target = "gr1cs")] |
| 148 | +fn enforce_addition<F: Field>( |
| 149 | + cs: ConstraintSystemRef<F>, |
| 150 | + left: Variable, |
| 151 | + right: Variable, |
| 152 | +) -> Result<Variable, SynthesisError> { |
| 153 | + // let cs = ns!(cs, "addition").cs(); |
| 154 | + |
| 155 | + // Instead of + we use *, This is intentioanlly made to fail |
| 156 | + let sum = cs.new_witness_variable(|| { |
| 157 | + Ok(cs.assigned_value(left).unwrap() * cs.assigned_value(right).unwrap()) |
| 158 | + })?; // Placeholder for sum |
| 159 | + |
| 160 | + cs.enforce_r1cs_constraint( |
| 161 | + LinearCombination::from(left) + LinearCombination::from(right), |
| 162 | + LinearCombination::from(Variable::One), |
| 163 | + LinearCombination::from(sum), |
| 164 | + )?; |
| 165 | + |
| 166 | + Ok(sum) |
| 167 | +} |
0 commit comments