docs: record the LowerSwitch ordering constraint it now relies on - #2100
docs: record the LowerSwitch ordering constraint it now relies on#2100OlivierBBB wants to merge 1 commit into
Conversation
Follow-up to #2095. Two comment fixes, no behavioural change. The bit-select-diamond check reasons that the pattern "can't arise from lowerSwitch, but only directly from .zkc program". The first half holds only because LowerSwitch was moved after FactorSkipConditions, and the second half is not accurate: LowerSwitch emits exactly this shape (one diamond per case, per its own doc), FactorLimbEqualities emits one per limb, and factorSkipIf emits it as well. None of them reaches the check today, purely by pass ordering. So state the dependency instead of the impossibility, and note that breaking it would only cost an unnecessary factorisation rather than correctness. Then record the requirement where someone reordering the pass will read it: LowerSwitch's doc already carries its "must run before register splitting" note, so the new "must run after FactorSkipConditions" joins it there. Otherwise the next reordering silently invalidates the reasoning, with nothing failing to signal it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
There was a problem hiding this comment.
Pull request overview
Documents a pass-ordering dependency in the ZkC VM transform pipeline, clarifying why certain “bit-select diamond” patterns are assumed not to appear when FactorSkipConditions runs (performance rationale, not correctness).
Changes:
- Updates the
FactorSkipConditionscommentary to explain that the “bit-select diamond” pattern is not unique to hand-written.zkc, and that ordering changes only affect performance. - Extends
LowerSwitch’s doc comment to record that it is expected to run afterFactorSkipConditionsin the compilation pipeline.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| pkg/zkc/vm/transform.go | Adds an ordering note to LowerSwitch’s documentation to capture its pipeline dependency. |
| pkg/zkc/vm/internal/transform/factor_skip_conditions.go | Rewords the “bit equality / diamond” comment to reflect actual sources of the pattern and ordering implications. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // NOTE: this transform must run before register splitting (which does not | ||
| // support Switch bytecodes). | ||
| // support Switch bytecodes), and after FactorSkipConditions: it emits one | ||
| // bit-select diamond per case, which that pass would otherwise re-factor for no | ||
| // gain (see bodyContainsOnlyBitEquality, whose reasoning assumes these diamonds | ||
| // have not been introduced yet). |
There was a problem hiding this comment.
comment is false - as I added one more condition to factor the skip If
| // Nothing to factorize if the body of the skip is a bit equality like b = x == 0 ? 1 :0. | ||
| // Note that as we lowerSwitch later, this pattern can't arise from lowerSwitch, but only | ||
| // directly from .zkc program. | ||
| // Nothing to factorize when the body is already a bit-select diamond, as |
There was a problem hiding this comment.
=>
// Nothing to factorize if the body of the skip is a bit equality like b = x == 0 ? 1 :0.
// Note that as we lowerSwitch later, this pattern can't arise from lowerSwitch, but only
// directly from .zkc program or other lowering steps (FactorLimbEqualities ...)
Follow-up to #2095 — comments only, no behavioural change.
Why
bodyContainsOnlyBitEqualitycarries this justification:Two problems with it:
The first half is true only by pass ordering — which perf: don't factor skipIf when not required #2095 itself changed. Nothing enforces it, and nothing fails if it is broken again.
The second half is not accurate. The shape is not unique to hand-written
.zkc:LowerSwitchemits exactly it, one diamond per case (see its own doc:if x == 1 {b_1 = 1} else {b_1 = 0});FactorLimbEqualitiesemits one per limb;factorSkipIf, in the same file, emits it too (though its output is never re-examined, sincefactor[]is decided over the original vector).None of them reaches the check today — purely because all three run later in the pipeline.
What
LowerSwitch's doc, next to themust run before register splittingnote it already carries. That is where someone reordering the pass will actually look; without it, movingLowerSwitchback aboveFactorSkipConditionswould satisfy every documented constraint while silently invalidating the reasoning in the other file — and nothing would fail to signal it.Verification
Comment-only (the diff contains no non-comment lines).
go build ./...andgolangci-lint run pkg/zkc/...clean.🤖 Generated with Claude Code