Summary
A precondition-bearing call passed as an argument to an effect operation (a QualifiedCall such as IO.print(...)) is never precondition-checked — no E501 fires, though vera verify reports clean. translate_expr has no dispatch branch for QualifiedCall and falls through to return None (vera/smt.py), so it never recurses into the effect op's arguments; the nested call is therefore never translated and its requires(...) is never checked statically.
Repro
private fn fmt_pos(@Nat -> @String)
requires(@Nat.0 >= 1)
ensures(true)
effects(pure)
{ "x" }
public fn caller(@Nat -> @Nat)
requires(true)
ensures(true)
effects(<IO>)
{ IO.print(fmt_pos(@Nat.0)); @Nat.0 }
vera verify → OK: (clean), but fmt_pos's requires(@Nat.0 >= 1) is violable (the caller only guarantees true). The same call not wrapped in an effect op — need_pos(@Nat.0); — correctly fires E501 after #730.
Root cause
translate_expr dispatches FnCall / ModuleCall to the call-precondition path (_translate_call_with_info, which checks each Requires), but a QualifiedCall (effect operation) is intentionally not translated to a Z3 term — effects in contract predicates violate purity — so it returns None without recursing into its arguments. A call-precondition-bearing argument is collateral. (The @Nat / refinement narrowing walkers do descend into QualifiedCall args, so narrowing obligations at effect-op-arg sites are unaffected — only the E501 call precondition is missed.) The callee's runtime requires(...) still guards it, so this is a verification-completeness gap, not a silent wrong answer.
Scope
Distinct from #730 (direct statement-position calls, now fixed) and #764 (a call at/after a let-destructure). This is the effect-op-argument facet of the same "calls whose preconditions escape static checking" family.
Fix direction
Recurse into a QualifiedCall's argument expressions for their call-precondition side effect (without translating the effect op itself to a Z3 term) — mirroring how the #730 fix translates ExprStmt.expr for its side effect, and how the narrowing walkers already descend into effect-op args.
Related
Summary
A precondition-bearing call passed as an argument to an effect operation (a
QualifiedCallsuch asIO.print(...)) is never precondition-checked — no E501 fires, thoughvera verifyreports clean.translate_exprhas no dispatch branch forQualifiedCalland falls through toreturn None(vera/smt.py), so it never recurses into the effect op's arguments; the nested call is therefore never translated and itsrequires(...)is never checked statically.Repro
vera verify→OK:(clean), butfmt_pos'srequires(@Nat.0 >= 1)is violable (the caller only guaranteestrue). The same call not wrapped in an effect op —need_pos(@Nat.0);— correctly fires E501 after #730.Root cause
translate_exprdispatchesFnCall/ModuleCallto the call-precondition path (_translate_call_with_info, which checks eachRequires), but aQualifiedCall(effect operation) is intentionally not translated to a Z3 term — effects in contract predicates violate purity — so it returnsNonewithout recursing into its arguments. A call-precondition-bearing argument is collateral. (The@Nat/ refinement narrowing walkers do descend intoQualifiedCallargs, so narrowing obligations at effect-op-arg sites are unaffected — only the E501 call precondition is missed.) The callee's runtimerequires(...)still guards it, so this is a verification-completeness gap, not a silent wrong answer.Scope
Distinct from #730 (direct statement-position calls, now fixed) and #764 (a call at/after a
let-destructure). This is the effect-op-argument facet of the same "calls whose preconditions escape static checking" family.Fix direction
Recurse into a
QualifiedCall's argument expressions for their call-precondition side effect (without translating the effect op itself to a Z3 term) — mirroring how the #730 fix translatesExprStmt.exprfor its side effect, and how the narrowing walkers already descend into effect-op args.Related
let-destructure are not statically checked (_translate_block truncates at LetDestruct) #764 (let-destructure truncation), @Nat narrowing: effect-op-argument runtime guard + dedicated guard trap kind #754 / Codegen: extend the #747 @Nat runtime-guard backstop to generic-instantiated constructor fields #757 (effect-op-arg runtime guards for@Nat).