vera/verifier.py (2)

2033-2057: ⚠️ Potential issue | 🔴 Critical | ⚡ Quick win

Use fresh pattern bindings when the match scrutinee is opaque.

When scrutinee_z3 is None, arm_env remains slot_env. A branch like Some(@int) -> 10 / @Int.0`` can then prove the divisor obligation against an outer @Int.0, not the pattern payload, so an effect/call-returned `Some(0)` can still trap after a clean verify. Use `_fresh_pattern_env(...)` here, as the nat-binding walker already does for the same shadowing case.

Suggested fix

                 if scrutinee_z3 is not None:
                     bound = smt._bind_pattern(
                         scrutinee_z3, arm.pattern, slot_env,
                     )
                     if bound is not None:
                         arm_env = bound
                     pat_cond = smt._pattern_condition(
                         scrutinee_z3, arm.pattern,
                     )
+                else:
+                    arm_env = self._fresh_pattern_env(
+                        arm.pattern, slot_env, smt,
+                    )

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 2033 - 2057, When the match scrutinee is
opaque (scrutinee_z3 is None), the code currently leaves arm_env as slot_env,
which causes pattern variables to shadow outer scope variables and leads to
incorrect verification. Modify the pattern handling logic in this match
expression block so that when scrutinee_z3 is None, call _fresh_pattern_env()
with the pattern and slot_env to create fresh bindings for the pattern
variables, similar to how the nat-binding walker handles the same shadowing
case. This ensures that proof obligations are verified against the correct
pattern payloads, not outer variables.

---

1960-1980: ⚠️ Potential issue | 🔴 Critical | ⚡ Quick win

Invalidate shadowing block bindings before checking later primitive ops.

Line 1967 only pushes a let binding when its RHS translates. If the RHS is untranslatable, later @Int.0/@Array<T>.0 references in the block resolve to an outer binding, so an outer requires(@Int.0 != 0) can incorrectly discharge 10 / @Int.0`` after let @Int` = E.next(())`. `LetDestruct` is also skipped entirely, which misses RHS primitive ops and leaves destructured slots stale. Mirror the fresh-rebind approach from the nat-binding walker, including fresh array variables for index checks.

One possible direction

                 if isinstance(stmt, ast.LetStmt):
                     self._walk_for_primitive_op_obligations(
                         decl, stmt.value, smt, cur_env, assumptions,
                     )
                     val = smt.translate_expr(stmt.value, cur_env)
+                    if val is None:
+                        let_ty = self._resolve_type(stmt.type_expr)
+                        if self._is_array_type(let_ty):
+                            val = self._declare_array_var(
+                                smt, smt._fresh_name("primitive_let"), let_ty,
+                            )
+                        else:
+                            val = self._fresh_slot_var(smt, stmt.type_expr)
                     if val is not None:
                         type_name = smt._type_expr_to_slot_name(stmt.type_expr)
                         if type_name is not None:
                             cur_env = cur_env.push(type_name, val)
+                elif isinstance(stmt, ast.LetDestruct):
+                    self._walk_for_primitive_op_obligations(
+                        decl, stmt.value, smt, cur_env, assumptions,
+                    )
+                    # Rebind destructured slots to exact literal components
+                    # when available, otherwise fresh placeholders, before
+                    # walking subsequent statements.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 1960 - 1980, The block walker currently only
pushes a let binding when the RHS translates successfully, which allows later
primitive op checks to incorrectly resolve to outer bindings. Additionally,
LetDestruct statements are not handled at all. To fix this: (1) Ensure that for
each LetStmt, a fresh binding is pushed into cur_env regardless of whether the
RHS translates (similar to the nat-binding walker approach), (2) Add handling
for ast.LetDestruct statements to walk their RHS for primitive ops and push
fresh bindings for the destructured slots, (3) Include fresh array variables for
index checks when pushing bindings, and (4) Use this updated cur_env when
walking the final expr.expr to ensure shadowed bindings are properly
invalidated.

vera/verifier.py (3)

3943-3949: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Render the actual divisor in the E526 fix hint.

The current hint hard-codes @Int.1, but the divisor may be @Int.0, a @Nat, or a compound expression. That can send users to guard the wrong De Bruijn slot.

Suggested fix

+        divisor_src = ast.format_expr(expr.right)
+        operation_src = ast.format_expr(expr)
         self._error(
             expr,
             description,
@@
             fix=(
-                "Add a precondition ruling out a zero divisor, e.g. "
-                "`requires(`@Int.1` != 0)`.  Alternatively, guard the "
-                "operation (`if `@Int.1` == 0 then 0 else `@Int.0` / `@Int.1`` — "
+                "Add a precondition or guard that proves the divisor is "
+                f"non-zero, e.g. `{divisor_src} != 0`.  Alternatively, guard "
+                f"the operation (`if {divisor_src} == 0 then 0 else "
+                f"{operation_src}` — "
                 "the path condition discharges the obligation in the "
                 "else-branch) or give the divisor a refinement type such "
                 "as `{ `@Int` | `@Int.0` != 0 }`."
             ),

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 3943 - 3949, The E526 division by zero error
hint in the fix string hard-codes `@Int.1` as the divisor, but the actual
divisor could be `@Int.0`, `@Nat`, or a compound expression, which misleads
users about which De Bruijn slot to guard. Locate where the fix hint is
constructed for this error, capture the actual divisor expression being used in
the division operation, and dynamically insert the rendered divisor into the
hint message instead of hard-coding `@Int.1`, ensuring the message references
the correct divisor value.

---

2040-2064: ⚠️ Potential issue | 🔴 Critical | ⚡ Quick win

Fresh-shadow match bindings when the scrutinee is opaque.

If smt.translate_expr(expr.scrutinee, slot_env) returns None, arm_env remains the outer environment. A pattern binding such as Some(@int) can then leave @Int.0 in the arm body pointing at an outer parameter, so 1 / @Int.0`` may verify against the caller’s precondition instead of the matched payload. Mirror the narrowing walker’s _fresh_pattern_env(...) fallback here.

Suggested fix

                 if scrutinee_z3 is not None:
                     bound = smt._bind_pattern(
                         scrutinee_z3, arm.pattern, slot_env,
                     )
                     if bound is not None:
                         arm_env = bound
                     pat_cond = smt._pattern_condition(
                         scrutinee_z3, arm.pattern,
                     )
+                else:
+                    arm_env = self._fresh_pattern_env(
+                        arm.pattern, slot_env, smt,
+                    )

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 2040 - 2064, When scrutinee_z3 is None
(meaning the scrutinee is opaque and cannot be translated), the current code
leaves arm_env as the outer slot_env, which allows pattern bindings like
Some(`@Int`) to incorrectly reference outer parameters instead of the matched
payload. To fix this, when scrutinee_z3 is None, create a fresh pattern
environment for arm_env similar to how the narrowing walker handles this case
with _fresh_pattern_env(...). This ensures pattern variables are properly
isolated from the outer scope and verified against the matched payload rather
than the caller's precondition.

---

1967-1984: ⚠️ Potential issue | 🔴 Critical | 🏗️ Heavy lift

Mirror block binding semantics before checking later primitive ops.

When a let RHS is untranslatable, this walker does not push a fresh shadow slot, so a later 1 / @Int.0`` can resolve to an outer parameter and discharge from the wrong requires. The same block also skips `LetDestruct` entirely, missing trapping ops in the destructure RHS and any slots it introduces. That can turn an effect-produced zero divisor or out-of-bounds array into a false Tier-1 verification.

Suggested direction

                 if isinstance(stmt, ast.LetStmt):
                     self._walk_for_primitive_op_obligations(
                         decl, stmt.value, smt, cur_env, assumptions,
                     )
                     val = smt.translate_expr(stmt.value, cur_env)
+                    if val is None:
+                        val = self._fresh_slot_var(smt, stmt.type_expr)
+                    if val is None:
+                        type_name = smt._type_expr_to_slot_name(stmt.type_expr)
+                        stale = (
+                            cur_env.resolve(type_name, 0)
+                            if type_name is not None else None
+                        )
+                        if stale is not None:
+                            val = z3.FreshConst(stale.sort(), prefix="letbind")
                     if val is not None:
                         type_name = smt._type_expr_to_slot_name(stmt.type_expr)
                         if type_name is not None:
                             cur_env = cur_env.push(type_name, val)
+                elif isinstance(stmt, ast.LetDestruct):
+                    self._walk_for_primitive_op_obligations(
+                        decl, stmt.value, smt, cur_env, assumptions,
+                    )
+                    # Rebind each destructured slot to either its translated
+                    # literal component or a fresh shadow value, matching the
+                    # stale-slot invalidation used by the narrowing walker.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 1967 - 1984, The block walker does not
maintain correct variable scoping when translating let statement RHS values.
When val is None (untranslatable RHS), the code skips pushing a fresh shadow
slot, causing later expressions to incorrectly resolve to outer parameters
instead of the current scope. Additionally, the code completely ignores
LetDestruct statements, missing trapping operations in their RHS and any slots
they introduce. Fix this by ensuring that even when val is None, a shadow slot
is still pushed for the let binding in the cur_env to maintain correct scoping
semantics. Also add handling for ast.LetDestruct statements by walking their RHS
for primitive op obligations and pushing appropriate bindings to cur_env,
similar to the LetStmt handling.

vera/verifier.py (2)

2040-2064: ⚠️ Potential issue | 🔴 Critical | ⚡ Quick win

Freshen match-arm bindings before discharging arm-body traps.

When scrutinee_z3 is None, arm_env remains the outer slot_env; a pattern such as Box(@int) then shadows an outer @Int at runtime, but the walker proves 1 / @Int.0`` against the outer slot. Also thread constructor source facts into arm assumptions so refined fields such as Box(NonZero) can discharge `@NonZero.0 != 0` instead of false-failing. This should mirror the match handling already used by `_walk_for_nat_binding_obligations`.

Suggested shape

                 if scrutinee_z3 is not None:
                     bound = smt._bind_pattern(
                         scrutinee_z3, arm.pattern, slot_env,
                     )
                     if bound is not None:
                         arm_env = bound
                     pat_cond = smt._pattern_condition(
                         scrutinee_z3, arm.pattern,
                     )
+                else:
+                    arm_env = self._fresh_pattern_env(
+                        arm.pattern, slot_env, smt,
+                    )
+                arm_assumptions = assumptions
+                if isinstance(arm.pattern, ast.ConstructorPattern):
+                    arm_assumptions = assumptions + self._subpattern_source_facts(
+                        expr.scrutinee, scrutinee_z3, arm.pattern, smt,
+                    )
                 if pat_cond is not None:
                     smt._path_conditions.append(pat_cond)
                     try:
                         self._walk_for_primitive_op_obligations(
-                            decl, arm.body, smt, arm_env, assumptions,
+                            decl, arm.body, smt, arm_env, arm_assumptions,
                         )
                     finally:
                         smt._path_conditions.pop()
                 else:
                     self._walk_for_primitive_op_obligations(
-                        decl, arm.body, smt, arm_env, assumptions,
+                        decl, arm.body, smt, arm_env, arm_assumptions,
                     )

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 2040 - 2064, When scrutinee_z3 is None, the
pattern bindings are not freshened, causing the walker to prove obligations
against the outer slot_env instead of the freshened bindings. Modify the
match-arm handling in the method to freshen pattern bindings even when
scrutinee_z3 is None by calling an appropriate freshening function on the
pattern, similar to how _walk_for_nat_binding_obligations handles match
expressions. Additionally, thread constructor source facts into the assumptions
parameter passed to _walk_for_primitive_op_obligations calls so that refined
field constraints like NonZero can be properly discharged during arm body
verification.

---

1967-1987: ⚠️ Potential issue | 🔴 Critical | ⚡ Quick win

Mirror block binding rebinding so later checks use the new slot.

For let @int= <untranslatable>; 1 /@Int.0``, val is None leaves `cur_env` pointing at any outer `@Int.0`, so the div-zero proof can discharge against the wrong variable. `LetDestruct` is also skipped entirely, so traps in the destructure RHS and later uses of destructured slots are missed. Mirror the nat-binding walker: walk `LetDestruct.value`, and push a fresh slot for every new binding when the exact RHS/component term is unavailable.

Localised direction

                     val = smt.translate_expr(stmt.value, cur_env)
+                    if val is None:
+                        val = self._fresh_slot_var(smt, stmt.type_expr)
                     if val is not None:
                         type_name = smt._type_expr_to_slot_name(stmt.type_expr)
                         if type_name is not None:
                             cur_env = cur_env.push(type_name, val)
+                elif isinstance(stmt, ast.LetDestruct):
+                    self._walk_for_primitive_op_obligations(
+                        decl, stmt.value, smt, cur_env, assumptions,
+                    )
+                    # Rebind destructured slots here as well, using exact
+                    # literal components when available and `_fresh_slot_var`
+                    # otherwise, so following expressions cannot resolve stale
+                    # outer bindings.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 1967 - 1987, In the block statement processing
within the method handling ast.Block, fix the environment binding by ensuring
that when translating stmt.value in a LetStmt results in None (untranslatable),
still push a fresh slot binding to cur_env instead of skipping it, and add
missing handling for ast.LetDestruct statements by walking their value
expressions for primitive op obligations and pushing fresh slots for all
destructured bindings to mirror the nat-binding walker behavior, ensuring later
checks use the correct slot binding rather than falling back to outer scopes.

FAQ.md (1)

53-59: ⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Add the Tier-3 escape hatch for opaque divisors.

The division sentence is still too absolute: the verifier only proves integer div/mod safety when it can translate the divisor; otherwise it records a Tier-3 runtime guard. Mention that fallback here so readers do not think every unguarded divisor is a compile error.

Suggested wording

- Integer division and modulo are decidable, so an unguarded divisor is always a compile error.
+ Integer division and modulo are Tier-1 decidable when the divisor can be translated to SMT; otherwise they fall back to a Tier-3 runtime-guarded check.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@FAQ.md` around lines 53 - 59, The second paragraph statement "Integer
division and modulo are decidable, so an unguarded divisor is always a compile
error" is too absolute and doesn't account for opaque divisors. Revise this
sentence to clarify that divisors whose values can be determined through
preconditions or path conditions are statically proven and trigger compile error
E526 if unguarded, but when the divisor is opaque (similar to how array_length
is treated), the safety obligation falls to a Tier-3 runtime guard instead of a
static error. This aligns the divisor behavior with the array bounds explanation
already present in the paragraph.

vera/verifier.py (2)

2051-2065: ⚠️ Potential issue | 🟠 Major | ⚡ Quick win

Include failed earlier match arms in the arm path condition.

This only assumes the current pattern condition. For ordered matches, a wildcard/binding arm is also reached because all previous arms failed; without those negated conditions, a safe shape like match @Int.0{ 0 -> 0, _ -> 1 /@Int.0 } is checked without @Int.0 != 0 and can produce a false E526. Track prior translatable pattern conditions and push not previous && current for each arm.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 2051 - 2065, The match arm processing in the
loop around pat_cond only includes the current pattern condition in the path
conditions, but for ordered matches, later arms are only reached if all previous
arms failed. To fix this, maintain a collection of pattern conditions from
previously processed arms. For each arm being processed, construct the effective
path condition to include both the current pattern condition (pat_cond) AND the
negation of all accumulated previous pattern conditions. After processing each
arm's body in the _walk_for_primitive_op_obligations call, add the current arm's
translatable pattern condition to the collection of previous conditions so that
subsequent iterations correctly account for this arm's failure as a
precondition. This ensures the SMT solver receives the complete path condition
including why earlier arms were not taken, preventing false positives in safety
checks.

---

1970-1985: ⚠️ Potential issue | 🔴 Critical | ⚡ Quick win

Mirror binding semantics so obligations do not use stale slots.

The primitive-op walker does not handle LetDestruct at all, so a RHS like Tuple(@Int.0/@Int.1) can hide E526. It also leaves cur_env/arm_env unchanged when a let RHS or match scrutinee is untranslatable, so a later @Int.0 or @Array<T>.0 can resolve to a stale outer binding and be proved safe incorrectly. Mirror the nat-binding walker here: walk LetDestruct.value, shadow destructured slots, and use fresh slot/pattern bindings when translation fails.

Minimal direction for preserving shadowing

                 if isinstance(stmt, ast.LetStmt):
                     self._walk_for_primitive_op_obligations(
                         decl, stmt.value, smt, cur_env, assumptions,
                     )
                     val = smt.translate_expr(stmt.value, cur_env)
+                    type_name = smt._type_expr_to_slot_name(stmt.type_expr)
+                    if val is None and type_name is not None:
+                        val = self._fresh_slot_var(smt, stmt.type_expr)
+                        if val is None:
+                            stale = cur_env.resolve(type_name, 0)
+                            if stale is not None:
+                                val = z3.FreshConst(
+                                    stale.sort(), prefix="primlet",
+                                )
                     if val is not None:
-                        type_name = smt._type_expr_to_slot_name(stmt.type_expr)
                         if type_name is not None:
                             cur_env = cur_env.push(type_name, val)
+                elif isinstance(stmt, ast.LetDestruct):
+                    self._walk_for_primitive_op_obligations(
+                        decl, stmt.value, smt, cur_env, assumptions,
+                    )
+                    for te in stmt.type_bindings:
+                        type_name = smt._type_expr_to_slot_name(te)
+                        if type_name is None:
+                            continue
+                        fresh = self._fresh_slot_var(smt, te)
+                        if fresh is None:
+                            stale = cur_env.resolve(type_name, 0)
+                            if stale is not None:
+                                fresh = z3.FreshConst(
+                                    stale.sort(), prefix="primdestruct",
+                                )
+                        if fresh is not None:
+                            cur_env = cur_env.push(type_name, fresh)
@@
                 if scrutinee_z3 is not None:
                     bound = smt._bind_pattern(
                         scrutinee_z3, arm.pattern, slot_env,
                     )
                     if bound is not None:
                         arm_env = bound
                     pat_cond = smt._pattern_condition(
                         scrutinee_z3, arm.pattern,
                     )
+                else:
+                    arm_env = self._fresh_pattern_env(
+                        arm.pattern, slot_env, smt,
+                    )

Also applies to: 2041-2065

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 1970 - 1985, The primitive-op walker is
missing handling for LetDestruct statements, which allows hidden unsafe
operations and stale slot references. Add an elif branch to handle
isinstance(stmt, ast.LetDestruct) after the ExprStmt case: walk stmt.value for
primitive-op obligations just like in LetStmt, translate the value using
smt.translate_expr, and shadow the destructured slots with fresh bindings in
cur_env by updating it to push the new bindings. Ensure that when the value
translation fails, you still create fresh slot/pattern bindings to prevent later
references from resolving to stale outer bindings, mirroring the behavior of the
nat-binding walker.

vera/verifier.py (1)

2057-2086: ⚠️ Potential issue | 🟠 Major | ⚡ Quick win

Carry constructor-field source facts into primitive checks.

The match walker binds constructor patterns but does not add the source facts that _walk_for_nat_binding_obligations() already derives. For Option<{ @int|@Int.0 != 0 }> matched as Some(@nonZero), a division by the bound field can false-fail E526 because the arm assumptions lack the field’s source refinement.

🐛 Proposed fix

             for arm in expr.arms:
                 arm_env = slot_env
                 pat_cond = None
+                arm_assumptions = assumptions
                 if scrutinee_z3 is not None:
                     bound = smt._bind_pattern(
                         scrutinee_z3, arm.pattern, slot_env,
                     )
@@
                     pat_cond = smt._pattern_condition(
                         scrutinee_z3, arm.pattern,
                     )
+                    if isinstance(arm.pattern, ast.ConstructorPattern):
+                        arm_assumptions = assumptions + self._subpattern_source_facts(
+                            expr.scrutinee, scrutinee_z3, arm.pattern, smt,
+                        )
                 if pat_cond is not None:
                     smt._path_conditions.append(pat_cond)
                     try:
                         self._walk_for_primitive_op_obligations(
-                            decl, arm.body, smt, arm_env, assumptions,
+                            decl, arm.body, smt, arm_env, arm_assumptions,
                         )
                     finally:
                         smt._path_conditions.pop()
                 else:
                     self._walk_for_primitive_op_obligations(
-                        decl, arm.body, smt, arm_env, assumptions,
+                        decl, arm.body, smt, arm_env, arm_assumptions,
                     )

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 2057 - 2086, When processing match expressions
(ast.MatchExpr), the pattern binding logic in the arm loop does not carry
constructor-field source facts from the patterns into the arm assumptions,
causing false E526 failures. After successfully binding a pattern with
smt._bind_pattern() in the arm processing loop, extract the source refinement
facts from the matched constructor's fields and add them to the assumptions
passed to the recursive _walk_for_primitive_op_obligations call for the arm
body. This ensures that field constraints (like non-zero refinements) are
available when checking primitive operations in the matched arm, similar to how
_walk_for_nat_binding_obligations() handles them.

vera/verifier.py (1)

2142-2172: ⚠️ Potential issue | 🟠 Major | ⚡ Quick win

Thread constructor sub-pattern source facts into primitive-op arm checks.

This arm walk binds projected fields into arm_env, but still passes the original assumptions. For a scrutinee with a refined field such as Box(NonZero), Box(@nonZero) -> 1 / @NonZero.0`` checks E526 against an unconstrained accessor instead of the field’s != 0 source fact, so safe code can be rejected.

🐛 Proposed fix

             for arm in expr.arms:
                 arm_env = slot_env
                 pat_cond = None
+                arm_assumptions = assumptions
                 if scrutinee_z3 is not None:
                     bound = smt._bind_pattern(
                         scrutinee_z3, arm.pattern, slot_env,
                     )
                     if bound is not None:
                         arm_env = bound
                     pat_cond = smt._pattern_condition(
                         scrutinee_z3, arm.pattern,
                     )
+                    if isinstance(arm.pattern, ast.ConstructorPattern):
+                        arm_assumptions = assumptions + self._subpattern_source_facts(
+                            expr.scrutinee, scrutinee_z3, arm.pattern, smt,
+                        )
                 else:
                     # Untranslatable scrutinee (e.g. an effect op): the arm
                     # still binds pattern slots, so shadow them as TRACKED
                     # opaque consts.
                     arm_env = self._fresh_pattern_env(
                         arm.pattern, slot_env, smt, track=True,
                     )
                 if pat_cond is not None:
                     smt._path_conditions.append(pat_cond)
                     try:
                         self._walk_for_primitive_op_obligations(
-                            decl, arm.body, smt, arm_env, assumptions,
+                            decl, arm.body, smt, arm_env, arm_assumptions,
                         )
                     finally:
                         smt._path_conditions.pop()
                 else:
                     self._walk_for_primitive_op_obligations(
-                        decl, arm.body, smt, arm_env, assumptions,
+                        decl, arm.body, smt, arm_env, arm_assumptions,
                     )

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/verifier.py` around lines 2142 - 2172, The
`_walk_for_primitive_op_obligations` calls for pattern match arms do not include
source facts from the refined pattern sub-types in their assumptions parameter,
causing safe field accesses to be incorrectly rejected. Update both calls to
`_walk_for_primitive_op_obligations` (the one inside the try/finally block when
pat_cond is not None, and the one in the else branch) to construct and pass
augmented assumptions that include the source facts and constraints derived from
the pattern refinements in arm.pattern, so that field operations like division
checks on refined fields (e.g. Box(NonZero).0) can use the inferred non-zero
constraint.