@@ -298,6 +298,8 @@ mod test {
298
298
let expectation = r#"namespace main(16);
299
299
pol commit _operation_id(i) query ("hint", 4);
300
300
pol commit pc;
301
+ pol commit X;
302
+ pol commit Y;
301
303
pol commit reg_write_X_A;
302
304
pol commit reg_write_Y_A;
303
305
pol commit A;
@@ -312,12 +314,12 @@ mod test {
312
314
pol commit X_read_free;
313
315
pol commit read_X_A;
314
316
pol commit read_X_pc;
315
- pol X = ((((read_X_A * A) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value));
317
+ ( X = ((((read_X_A * A) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value) ));
316
318
pol commit Y_const;
317
319
pol commit Y_read_free;
318
320
pol commit read_Y_A;
319
321
pol commit read_Y_pc;
320
- pol Y = ((((read_Y_A * A) + (read_Y_pc * pc)) + Y_const) + (Y_read_free * Y_free_value));
322
+ ( Y = ((((read_Y_A * A) + (read_Y_pc * pc)) + Y_const) + (Y_read_free * Y_free_value) ));
321
323
pol constant first_step = [1] + [0]*;
322
324
(A' = ((((reg_write_X_A * X) + (reg_write_Y_A * Y)) + (instr__reset * 0)) + ((1 - ((reg_write_X_A + reg_write_Y_A) + instr__reset)) * A)));
323
325
pol pc_update = ((((instr__jump_to_operation * _operation_id) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - ((instr__jump_to_operation + instr__loop) + instr_return)) * (pc + 1)));
@@ -356,6 +358,7 @@ namespace main_sub(16);
356
358
pol commit _operation_id(i) query ("hint", 5);
357
359
pol commit pc;
358
360
pol commit _input_0;
361
+ pol commit _output_0;
359
362
pol commit instr__jump_to_operation;
360
363
pol commit instr__reset;
361
364
pol commit instr__loop;
@@ -364,7 +367,7 @@ namespace main_sub(16);
364
367
pol commit _output_0_read_free;
365
368
pol commit read__output_0_pc;
366
369
pol commit read__output_0__input_0;
367
- pol _output_0 = ((((read__output_0_pc * pc) + (read__output_0__input_0 * _input_0)) + _output_0_const) + (_output_0_read_free * _output_0_free_value));
370
+ ( _output_0 = ((((read__output_0_pc * pc) + (read__output_0__input_0 * _input_0)) + _output_0_const) + (_output_0_read_free * _output_0_free_value) ));
368
371
pol constant first_step = [1] + [0]*;
369
372
(((1 - instr__reset) * (_input_0' - _input_0)) = 0);
370
373
pol pc_update = ((((instr__jump_to_operation * _operation_id) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - ((instr__jump_to_operation + instr__loop) + instr_return)) * (pc + 1)));
@@ -405,6 +408,7 @@ namespace main_sub(16);
405
408
((XIsZero * (1 - XIsZero)) = 0);
406
409
pol commit _operation_id(i) query ("hint", 10);
407
410
pol commit pc;
411
+ pol commit X;
408
412
pol commit reg_write_X_A;
409
413
pol commit A;
410
414
pol commit reg_write_X_CNT;
@@ -427,7 +431,7 @@ namespace main_sub(16);
427
431
pol commit read_X_A;
428
432
pol commit read_X_CNT;
429
433
pol commit read_X_pc;
430
- pol X = (((((read_X_A * A) + (read_X_CNT * CNT)) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value));
434
+ ( X = (((((read_X_A * A) + (read_X_CNT * CNT)) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value) ));
431
435
pol constant first_step = [1] + [0]*;
432
436
(A' = (((reg_write_X_A * X) + (instr__reset * 0)) + ((1 - (reg_write_X_A + instr__reset)) * A)));
433
437
(CNT' = ((((reg_write_X_CNT * X) + (instr_dec_CNT * (CNT - 1))) + (instr__reset * 0)) + ((1 - ((reg_write_X_CNT + instr_dec_CNT) + instr__reset)) * CNT)));
@@ -578,6 +582,7 @@ machine Main {
578
582
let expected = r#"namespace main(1024);
579
583
pol commit _operation_id(i) query ("hint", 3);
580
584
pol commit pc;
585
+ pol commit X;
581
586
pol commit reg_write_X_A;
582
587
pol commit A;
583
588
pol commit instr_add5_into_A;
@@ -589,7 +594,7 @@ machine Main {
589
594
pol commit X_read_free;
590
595
pol commit read_X_A;
591
596
pol commit read_X_pc;
592
- pol X = ((((read_X_A * A) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value));
597
+ ( X = ((((read_X_A * A) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value) ));
593
598
pol constant first_step = [1] + [0]*;
594
599
(A' = ((((reg_write_X_A * X) + (instr_add5_into_A * A')) + (instr__reset * 0)) + ((1 - ((reg_write_X_A + instr_add5_into_A) + instr__reset)) * A)));
595
600
pol pc_update = ((((instr__jump_to_operation * _operation_id) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - ((instr__jump_to_operation + instr__loop) + instr_return)) * (pc + 1)));
0 commit comments