Seam assert pre-scan: three traversal gaps left open after #621

Follow-up to https://github.com/vx-lang/Vx/pull/621, which widened the seam-contract
pre-scan (collect_assert_contracts / scan_expr_for_asserts in
src/hir/check/transfer.rs) so it walks expression children and nested statement
blocks. That closed #620, but three gaps in the same class are still open.

Related: #620, #491

1. An assert made of a conjunction records nothing

assert(a == 1 && b == 2);

This collects neither a nor b.

Statement::Assert is the one position where the pre-scan calls extract_eq_const
directly on the assert's expression instead of walking it. extract_eq_const returns
immediately unless the top node is a RelationalOp::Eq, so a LogicalOp::And at the
top is dropped whole. Every other position in the pre-scan now descends a
LogicalOp, which makes the assert site the odd one out.

Suggested fix: let extract_eq_const recurse through LogicalOp::And and record each
conjunct.

2. Loop invariant expressions are never walked

for i in 0..2 invariant(if c { assert(v == 7); true } else { true }) {
    let x = i;
}

The assert is missed.

Both ForLoopStmt and LoopStmt carry an invariants: Vec<Expr> field
(src/syntax/stmt.rs), and invariant(...) is parsed with the general expression
parser (src/parser/stmt.rs), so an invariant can hold a block-bearing expression.
The pre-scan's ForLoop arm scans only iterable and body, and its Loop arm
scans only body. Neither touches invariants.

This one also makes the new doc comment inaccurate: it says the pre-scan "recurses
through every evaluated expression and nested statement block", and an invariant is an
evaluated expression.

Suggested fix: scan each expression in invariants in both arms.

3. Match arms are flattened, so the last arm silently wins

let r = match t {
    0 => { assert(v == 1); 10 }
    _ => { assert(v == 2); 20 }
};

This records v -> 2.

The Expr::Match arm collects asserts from every arm into one flat map. Because the
map is a HashMap and extract_eq_const ends in out.insert(...), two arms that
assert different values for the same name overwrite each other, and which one survives
depends on the order the arms are written in. The recorded contract then holds on at
most one execution path.

The pre-existing Expr::If arm has the same shape, so this is not new behaviour, but
#621 extends it to match and makes it easier to hit.

Suggested fix: when two branches of the same construct give different values for one
name, drop that name from the map rather than keeping the last write. A contract that
holds on only one path is not a contract.

A note on scope

These three are all traversal gaps, so they are worth fixing together. They do not
change any program's accept/reject verdict today, for a reason that needs its own
issue: the value contract the pre-scan feeds is currently compared against itself in
run_seam_hop, so it only affects the text of the E6004 message. Fixing that is a
separate change; these three should be fixed regardless, because they are what makes
the collected contract correct once it starts being used.

Testing

Each gap wants its own unit test next to
seam_assert_prescan_collects_an_assert_nested_in_a_binary_expression in
src/hir/mod.rs, calling TypeChecker::collect_assert_contracts directly. Note that
going through check_function does not exercise the pre-scan: it is gated behind
self.seam.verify, which is off by default.

Per agents/AGENTS.md, break each assertion separately and watch it fail before
trusting the test.

Start with collect_assert_contracts and extract_eq_const in src/hir/check/transfer.rs, then inspect invariant handling in src/syntax/stmt.rs and src/parser/stmt.rs. Add focused tests beside seam_assert_prescan_collects_an_assert_nested_in_a_binary_expression in src/hir/mod.rs, calling TypeChecker::collect_assert_contracts directly; done means conjunctions and loop invariants are traversed and branch-only conflicting contracts are omitted.