@@ -5,21 +5,21 @@ use powdr_ast::parsed::asm::Part;
5
5
use powdr_ast:: {
6
6
analyzed:: {
7
7
AlgebraicBinaryOperation , AlgebraicBinaryOperator , AlgebraicExpression , AlgebraicReference ,
8
- AlgebraicUnaryOperator , Analyzed , BusInteractionIdentity , Identity , PolyID ,
9
- PolynomialIdentity , PolynomialType ,
8
+ AlgebraicUnaryOperator , Analyzed , BusInteractionIdentity , Identity , PolynomialIdentity ,
10
9
} ,
11
10
parsed:: {
12
11
asm:: SymbolPath , visitor:: AllChildren , ArrayLiteral , BinaryOperation , BinaryOperator ,
13
12
Expression , FunctionCall , NamespacedPolynomialReference , Number , PILFile , PilStatement ,
14
13
UnaryOperation , UnaryOperator ,
15
14
} ,
16
15
} ;
16
+ use powdr_executor:: witgen:: evaluators:: symbolic_evaluator:: SymbolicEvaluator ;
17
+ use powdr_executor:: witgen:: { AlgebraicVariable , PartialExpressionEvaluator } ;
17
18
use powdr_parser_util:: SourceRef ;
18
19
use powdr_pil_analyzer:: analyze_ast;
19
20
use powdr_pilopt:: optimize;
20
21
use serde:: { Deserialize , Serialize } ;
21
22
use std:: collections:: { BTreeMap , BTreeSet , HashSet } ;
22
- use std:: convert:: TryFrom ;
23
23
24
24
use powdr_number:: { BigUint , FieldElement , LargeInt } ;
25
25
use powdr_pilopt:: simplify_expression;
@@ -960,8 +960,7 @@ pub fn generate_precompile<T: FieldElement>(
960
960
sub_map_loadstore. extend ( loadstore_chip_info ( & machine, instr. opcode ) ) ;
961
961
}
962
962
963
- let opcode_a = AlgebraicExpression :: Number ( ( instr. opcode as u64 ) . into ( ) ) ;
964
- local_constraints. push ( ( pc_lookup. op - opcode_a) . into ( ) ) ;
963
+ add_opcode_constraints ( & mut local_constraints, instr. opcode , & pc_lookup. op ) ;
965
964
966
965
assert_eq ! ( instr. args. len( ) , pc_lookup. args. len( ) ) ;
967
966
if optimize {
@@ -1149,6 +1148,93 @@ pub fn generate_precompile<T: FieldElement>(
1149
1148
)
1150
1149
}
1151
1150
1151
+ fn add_opcode_constraints < T : FieldElement > (
1152
+ constraints : & mut Vec < SymbolicConstraint < T > > ,
1153
+ opcode : usize ,
1154
+ expected_opcode : & AlgebraicExpression < T > ,
1155
+ ) {
1156
+ let opcode_a = AlgebraicExpression :: Number ( ( opcode as u64 ) . into ( ) ) ;
1157
+ match try_compute_opcode_map ( expected_opcode) {
1158
+ Ok ( opcode_to_flag) => {
1159
+ let active_flag = opcode_to_flag. get ( & ( opcode as u64 ) ) . unwrap ( ) ;
1160
+ for flag_ref in opcode_to_flag. values ( ) {
1161
+ let expected_value = if flag_ref == active_flag {
1162
+ AlgebraicExpression :: Number ( 1u32 . into ( ) )
1163
+ } else {
1164
+ AlgebraicExpression :: Number ( 0u32 . into ( ) )
1165
+ } ;
1166
+ let flag_expr = AlgebraicExpression :: Reference ( flag_ref. clone ( ) ) ;
1167
+ let constraint = flag_expr - expected_value;
1168
+ constraints. push ( constraint. into ( ) ) ;
1169
+ }
1170
+ }
1171
+ Err ( _) => {
1172
+ // We were not able to extract the flags, so we keep them as witness columns
1173
+ // and add a constraint that the expected opcode needs to equal the compile-time opcode.
1174
+ constraints. push ( ( expected_opcode. clone ( ) - opcode_a) . into ( ) ) ;
1175
+ }
1176
+ }
1177
+ }
1178
+
1179
+ fn try_compute_opcode_map < T : FieldElement > (
1180
+ expected_opcode : & AlgebraicExpression < T > ,
1181
+ ) -> Result < BTreeMap < u64 , AlgebraicReference > , ( ) > {
1182
+ // Parse the expected opcode as an algebraic expression:
1183
+ // flag1 * c1 + flag2 * c2 + ... + offset
1184
+ let imm = BTreeMap :: new ( ) ;
1185
+ let affine_expression = PartialExpressionEvaluator :: new ( SymbolicEvaluator , & imm)
1186
+ . evaluate ( expected_opcode)
1187
+ . map_err ( |_| ( ) ) ?;
1188
+ println ! ( "GGG affine_expression = {affine_expression}" ) ;
1189
+
1190
+ // The above would not include any entry for `flag * 0` or `0 * flag`.
1191
+ // If it exists, we collect it here.
1192
+ let zero = AlgebraicExpression :: Number ( 0u32 . into ( ) ) ;
1193
+ let zero_flag = expected_opcode
1194
+ . all_children ( )
1195
+ . find_map ( |expr| match expr {
1196
+ AlgebraicExpression :: BinaryOperation ( AlgebraicBinaryOperation {
1197
+ op : AlgebraicBinaryOperator :: Mul ,
1198
+ left,
1199
+ right,
1200
+ } ) => {
1201
+ if * * left == zero {
1202
+ Some ( ( * * right) . clone ( ) )
1203
+ } else if * * right == zero {
1204
+ Some ( ( * * left) . clone ( ) )
1205
+ } else {
1206
+ None
1207
+ }
1208
+ }
1209
+ _ => None ,
1210
+ } )
1211
+ . and_then ( |expr| match expr {
1212
+ AlgebraicExpression :: Reference ( reference) => Some ( reference) ,
1213
+ _ => None ,
1214
+ } ) ;
1215
+
1216
+ let offset = affine_expression. offset ( ) ;
1217
+
1218
+ if !offset. is_zero ( ) && zero_flag. is_none ( ) {
1219
+ // We didn't find any flag with factor zero, and the offset is not zero.
1220
+ // Probably something went wrong.
1221
+ return Err ( ( ) ) ;
1222
+ }
1223
+
1224
+ Ok ( affine_expression
1225
+ . nonzero_coefficients ( )
1226
+ . map ( |( k, factor) | {
1227
+ let opcode = ( offset + * factor) . to_degree ( ) ;
1228
+ let flag = match k {
1229
+ AlgebraicVariable :: Column ( column) => ( * column) . clone ( ) ,
1230
+ AlgebraicVariable :: Public ( _) => unreachable ! ( ) ,
1231
+ } ;
1232
+ ( opcode, flag)
1233
+ } )
1234
+ . chain ( zero_flag. map ( |flag| ( offset. to_degree ( ) , flag. clone ( ) ) ) )
1235
+ . collect ( ) )
1236
+ }
1237
+
1152
1238
/// Use a SymbolicMachine to create a PILFile and run powdr's optimizations on it.
1153
1239
/// Then, translate the optimized constraints and interactions back to a SymbolicMachine
1154
1240
fn powdr_optimize < P : FieldElement > ( symbolic_machine : SymbolicMachine < P > ) -> SymbolicMachine < P > {
0 commit comments