Repository navigation
RCA: set () = { … } drops its value's dynamic kind; code is lost #4002
Description
Summary
RCA computes the kind of an assignment only from the locals it updates. set () = … updates no local, so the statement is Static even when its value contains measurement-dependent code. Partial evaluation then evaluates the block classically: a store into a mutable and gates inside the block are silently dropped. This gives wrong results on Adaptive_RI, Adaptive_RIF and Adaptive.
Minimal repro
operation Main() : Int {
use q = Qubit();
X(q);
let d = MResetZ(q) == One;
mutable z = 3;
set () = { if d { set z = 5; } () }; // assigns nothing; means: if d { set z = 5; }
return z;
}Gate variant (the X(t) is dropped):
operation Main() : Bool {
use (q, t) = (Qubit(), Qubit());
X(q);
let d = MResetZ(q) == One;
set () = { if d { X(t); } () };
return MResetZ(t) == One;
}Run with python check.py prog.qs "Main()"; check.py is in #4001. It runs the program on the simulator, then compiles it for Adaptive_RI, Adaptive_RIF and Adaptive and runs the QIR with qir-runner, one shot each.
Expected vs actual
| Program | Simulator (expected) | Adaptive_RI / Adaptive_RIF / Adaptive |
|---|---|---|
| store | 5 |
3 |
| gate variant | true |
false |
Output on main 1b8de0d17 (same on the earlier main commits a90b8f777 and 48449939c and on open PR #3902 577dc9382; qir-runner 0.9.7):
### store
simulator: 5
Adaptive_RI: OUTPUT INT 3 0_i
Adaptive_RIF: OUTPUT INT 3 0_i
Adaptive: OUTPUT INT 3 0_i
### gate variant
simulator: True
Adaptive_RI: OUTPUT BOOL false 0_b
Adaptive_RIF: OUTPUT BOOL false 0_b
Adaptive: OUTPUT BOOL false 0_b
The results are the same with #3977 (head 6228ff9ee): that PR does not change this path.
Root cause
analyze_expr_assign builds the statement's kind only from update_locals_compute_kind, the kind of the locals in the assignee (qsc_rca/src/core.rs#L149-L171, lines 160–169). With the assignee (), no local is updated, so the value's runtime features are discarded and the statement is Static.
History (Adaptive_RI): at #3733 (95c039f4b) and #3885 (45d8e3038) both programs were rejected with PartialEval.EvaluationFailed; since #3887 (96388a0da) they compile and give the wrong answer.
Suggested fix
In analyze_expr_assign, also aggregate the value expression's runtime features into the assignment's kind. For an assignee without () parts this adds nothing new, since the value's kind already reaches the statement through the updated locals (reasoned; consistent with no existing expect-test changing); for () (or a tuple with a () element) it restores the value's dynamic features.
I have this implemented (9 lines in core.rs, plus tests) and will open a PR. With it, the repros give 5 and true on Adaptive_RI, Adaptive_RIF and Adaptive. It is independent of #3977 and merges with it without conflicts.
How it was found
While proving properties of a formal model of the lowering: the proof required the kind of an assignment to include the kind of its value. Random differential testing did not find it (our program generator has no set ()).
Related issues
- No existing issue found. Searches: "set () unit", "unit tuple assignment", "assign to unit", "set () unit tuple", "assign unit tuple dynamic".
- Only keep matching static variable mappings across short-circuiting logical and/or exprs #3887: the partial-evaluation change after which these programs compile to wrong QIR instead of being rejected.
- [Panic] Assignment in the right operand of a measurement-dependent
and/or#3976 / RCA should catch update of an array inside of a nested dynamic logicalandexpression #3977: a different RCA bug in the right operand of a dynamicand/or; RCA should catch update of an array inside of a nested dynamic logicalandexpression #3977 does not fix this one.
Activity