This repository was archived by the owner on Jun 13, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathless_than_v2.rs
153 lines (124 loc) · 4.04 KB
/
less_than_v2.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
use eth_types::Field;
use gadgets::less_than::{LtChip, LtConfig, LtInstruction};
use std::marker::PhantomData;
use halo2_proofs::{circuit::*, plonk::*, poly::Rotation};
#[derive(Default)]
// define circuit struct using array of usernames and balances
struct MyCircuit<F> {
pub value_l: u64,
pub value_r: u64,
pub check: bool,
_marker: PhantomData<F>,
}
#[derive(Clone, Debug)]
struct TestCircuitConfig<F> {
q_enable: Selector,
value_l: Column<Advice>,
value_r: Column<Advice>,
check: Column<Advice>,
lt: LtConfig<F, 8>,
}
impl<F: Field> Circuit<F> for MyCircuit<F> {
type Config = TestCircuitConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let q_enable = meta.complex_selector();
let value_l = meta.advice_column();
let value_r = meta.advice_column();
let check = meta.advice_column();
let lt = LtChip::configure(
meta,
|meta| meta.query_selector(q_enable),
|meta| meta.query_advice(value_l, Rotation::cur()),
|meta| meta.query_advice(value_r, Rotation::cur()),
);
let config = Self::Config {
q_enable,
value_l,
value_r,
check,
lt,
};
meta.create_gate(
"verifies that `check` current confif = is_lt from LtChip ",
|meta| {
let q_enable = meta.query_selector(q_enable);
// This verifies lt(value_l::cur, value_r::cur) is calculated correctly
let check = meta.query_advice(config.check, Rotation::cur());
vec![q_enable * (config.lt.is_lt(meta, None) - check)]
},
);
config
}
fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let chip = LtChip::construct(config.lt);
chip.load(&mut layouter)?;
layouter.assign_region(
|| "witness",
|mut region| {
region.assign_advice(
|| "value left",
config.value_l,
0,
|| Value::known(F::from(self.value_l)),
)?;
region.assign_advice(
|| "value right",
config.value_r,
0,
|| Value::known(F::from(self.value_r)),
)?;
region.assign_advice(
|| "check",
config.check,
0,
|| Value::known(F::from(self.check as u64)),
)?;
config.q_enable.enable(&mut region, 0)?;
chip.assign(&mut region, 0, F::from(self.value_l), F::from(self.value_r))?;
Ok(())
},
)
}
}
#[cfg(test)]
mod tests {
use super::MyCircuit;
use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr as Fp};
use std::marker::PhantomData;
#[test]
fn test_less_than_2() {
let k = 9;
// initate usernames and balances array
let value_l: u64 = 5;
let value_r: u64 = 10;
let check = true;
let mut circuit = MyCircuit::<Fp> {
value_l,
value_r,
check,
_marker: PhantomData,
};
// Test 1 - should be valid
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
prover.assert_satisfied();
// switch value_l and value_r
circuit.value_l = 10;
circuit.value_r = 5;
// Test 2 - should be invalid
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert!(prover.verify().is_err());
// let check to be false
circuit.check = false;
// Test 3 - should be valid
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
prover.assert_satisfied();
}
}