1
1
use ff_ext:: ExtensionField ;
2
2
use gkr_iop:: error:: CircuitBuilderError ;
3
3
4
- use crate :: {
5
- circuit_builder:: CircuitBuilder , gadgets:: AssertLtConfig ,
6
- instructions:: riscv:: constants:: UINT_LIMBS , structs:: RAMType ,
7
- } ;
4
+ use crate :: { circuit_builder:: CircuitBuilder , gadgets:: AssertLtConfig , structs:: RAMType } ;
8
5
use multilinear_extensions:: { Expression , ToExpr } ;
9
6
10
7
use super :: { RegisterChipOperations , RegisterExpr } ;
@@ -20,39 +17,7 @@ impl<E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOperati
20
17
ts : Expression < E > ,
21
18
value : RegisterExpr < E > ,
22
19
) -> Result < ( Expression < E > , AssertLtConfig ) , CircuitBuilderError > {
23
- self . namespace ( name_fn, |cb| {
24
- // READ (a, v, t)
25
- let read_record = [
26
- vec ! [ RAMType :: Register . into( ) ] ,
27
- vec ! [ register_id. expr( ) ] ,
28
- value. to_vec ( ) ,
29
- vec ! [ prev_ts. clone( ) ] ,
30
- ]
31
- . concat ( ) ;
32
- // Write (a, v, t)
33
- let write_record = [
34
- vec ! [ RAMType :: Register . into( ) ] ,
35
- vec ! [ register_id. expr( ) ] ,
36
- value. to_vec ( ) ,
37
- vec ! [ ts. clone( ) ] ,
38
- ]
39
- . concat ( ) ;
40
- cb. read_record ( || "read_record" , RAMType :: Register , read_record) ?;
41
- cb. write_record ( || "write_record" , RAMType :: Register , write_record) ?;
42
-
43
- // assert prev_ts < current_ts
44
- let lt_cfg = AssertLtConfig :: construct_circuit (
45
- cb,
46
- || "prev_ts < ts" ,
47
- prev_ts,
48
- ts. clone ( ) ,
49
- UINT_LIMBS ,
50
- ) ?;
51
-
52
- let next_ts = ts + 1 ;
53
-
54
- Ok ( ( next_ts, lt_cfg) )
55
- } )
20
+ self . ram_type_read ( name_fn, RAMType :: Register , register_id, prev_ts, ts, value)
56
21
}
57
22
58
23
fn register_write (
@@ -64,50 +29,14 @@ impl<E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOperati
64
29
prev_values : RegisterExpr < E > ,
65
30
value : RegisterExpr < E > ,
66
31
) -> Result < ( Expression < E > , AssertLtConfig ) , CircuitBuilderError > {
67
- assert ! ( register_id. expr( ) . degree( ) <= 1 ) ;
68
- self . namespace ( name_fn, |cb| {
69
- // READ (a, v, t)
70
- let read_record = [
71
- vec ! [ RAMType :: Register . into( ) ] ,
72
- vec ! [ register_id. expr( ) ] ,
73
- prev_values. to_vec ( ) ,
74
- vec ! [ prev_ts. clone( ) ] ,
75
- ]
76
- . concat ( ) ;
77
- // Write (a, v, t)
78
- let write_record = [
79
- vec ! [ RAMType :: Register . into( ) ] ,
80
- vec ! [ register_id. expr( ) ] ,
81
- value. to_vec ( ) ,
82
- vec ! [ ts. clone( ) ] ,
83
- ]
84
- . concat ( ) ;
85
- cb. read_record ( || "read_record" , RAMType :: Register , read_record) ?;
86
- cb. write_record ( || "write_record" , RAMType :: Register , write_record) ?;
87
-
88
- let lt_cfg = AssertLtConfig :: construct_circuit (
89
- cb,
90
- || "prev_ts < ts" ,
91
- prev_ts,
92
- ts. clone ( ) ,
93
- UINT_LIMBS ,
94
- ) ?;
95
-
96
- let next_ts = ts + 1 ;
97
-
98
- #[ cfg( test) ]
99
- {
100
- use gkr_iop:: circuit_builder:: DebugIndex ;
101
- use itertools:: izip;
102
- use multilinear_extensions:: power_sequence;
103
- let pow_u16 = power_sequence ( ( 1 << u16:: BITS as u64 ) . into ( ) ) ;
104
- cb. register_debug_expr (
105
- DebugIndex :: RdWrite as usize ,
106
- izip ! ( value, pow_u16) . map ( |( v, pow) | v * pow) . sum ( ) ,
107
- ) ;
108
- }
109
-
110
- Ok ( ( next_ts, lt_cfg) )
111
- } )
32
+ self . ram_type_write (
33
+ name_fn,
34
+ RAMType :: Register ,
35
+ register_id,
36
+ prev_ts,
37
+ ts,
38
+ prev_values,
39
+ value,
40
+ )
112
41
}
113
42
}
0 commit comments