ITADN

Checker bare-op resolution is PYTHONHASHSEED-dependent when the effect row holds two effects declaring the same op name

#1215Openaallan 创建于 24 天前
bug
A
aallancommented
## Repro A fn whose effect row carries TWO put-bearing effects (`effects(<State<Nat>, Store>)` with `effect Store { op put(String -> Unit); }`): a bare `put(...)` call resolves through `lookup_effect_op`'s iteration over the row's frozenset (vera/environment.py `lookup_effect_op`, reached from checker/calls.py), so which effect's signature binds flips with PYTHONHASHSEED — probed across seeds 0–5: seeds 0/4/5 bind State (check-green for an Int argument), seeds 1/2/3 bind Store (E204 String mismatch). ## Notes The same class as the #1203-era nested-State determinism fix (which made the STATE-TYPE mapping innermost-first) — this is the OP-NAME resolution's version. Consequence beyond flappy checks: the verifier's bare-put obligation fallback (PR #1202's handled-effect stack) mirrors the checker for handled contexts, but in the two-put-row case no deterministic rule can match a nondeterministic checker — the disclosure label/guard flag is right on some seeds and wrong on others. Fix direction: deterministic resolution order (declaration order or innermost-handled-first extended to rows), matching whatever rule the spec picks. Surfaced by PR #1202's round-9 review (probe v2, seed-swept).
1 条评论