fix(checker): Int op Nat types as Int — the formal LUB, not a silent Nat assertion

[aallan]

Summary

Burndown PR for #755. Mixed Int <op> Nat arithmetic typed as Nat whenever the Int operand came first — the join used bidirectional is_subtype, and the verifier-mediated narrowing relaxation (Int <: Nat, spec §2.8 rule 5) leaked into the checker's widening join. Typing @Int.0 - 2 as Nat silently asserts non-negativity with no obligation behind it (spurious Future<Nat> inferences, E503s the author never asked for), violating §0.2.2 no-implicit-behaviour.

• New numeric_join LUB helper in vera/types.py: only Nat <: Int (the formal refinement subtyping, §2.2.1) participates; Int op Nat → Int for all five operators, both operand orders. Nat op Nat → Nat and Int/Float64 mismatches (E141) unchanged.
• Spec §4.4 gains the explicit mixed-arithmetic result-type rule; the checker now agrees with what the verifier/smt.py: integer arithmetic overflow unmodeled — Tier 1 proves contracts false under i64/u64 wraparound #798 overflow classifier and Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 subtraction guard already assumed.
• Blast radius handled honestly: one overflow-differential test re-baselined (its load-bearing i64-width assertion preserved, plus a new mixed-operand case restoring lost coverage); ch09_async.vera's requires(@Int.0 >= 0) workaround for this exact bug removed.
• Obligations shift as expected: @Int.0 - 2 now carries int_overflow (was nat_sub); genuine @Nat - @Nat keeps its underflow guard (verified).
• Tests observe the synthesized type directly via typecheck_with_artifacts (cannot coincide with a fallback); 3 RED on the unfixed tree; mutation kill: reverting the join flips them RED.
• Residual note: the runtime negative-Nat at a bare return-position narrowing is pre-existing and already tracked by Verifier: @Nat narrowing not obligated at function return position or value-position tuple/constructor components #758 (spec §11.2.1 documents it) — this PR makes the type honest, Verifier: @Nat narrowing not obligated at function return position or value-position tuple/constructor components #758 owns the guard.

Orchestrator flip: the branch's type-observation tests fail 3/6 against main's compiler, 6/6 pass on the branch.

Closes #755

🤖 Generated with Claude Code

Summary by CodeRabbit

• Bug Fixes

  • Mixed Int/Nat binary arithmetic now consistently yields an Int result type (with Nat <op> Nat staying Nat and Int <op> Int staying Int).
  • Overflow/narrowing behaviour for mixed numeric expressions into @Nat contexts is corrected to match the intended typing rules.

• Tests

  • Added regression coverage for the mixed Int/Nat result-typing cases, plus updated overflow-related expectations and metrics.

• Documentation

  • Specification updated to clarify the least-upper-bound result typing rule for mixed arithmetic, and related project documentation refreshed.

[coderabbitai]

Important

Review skipped

No new commits to review since the last review.

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: c2ec8e04-a89e-4d9f-af38-8b6f30e218e5

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

📝 Walkthrough

Walkthrough

This PR changes mixed Int/Nat arithmetic typing so the checker returns Int for mixed cases. It also updates the spec, regression tests, overflow-classification tests, and project tracking documents.

Changes

Numeric join fix and validation

Layer / File(s)	Summary
numeric_join type-lattice helper vera/types.py	Adds numeric_join(left, right) to compute numeric least-upper-bounds, including Int for mixed Int/Nat.
Wire numeric_join into arithmetic type checking vera/checker/expressions.py	Replaces the arithmetic result-typing path with numeric_join for binary numeric operands.
Spec clarification for mixed arithmetic typing spec/04-expressions.md, scripts/check_spec_examples.py	Documents the mixed Int/Nat rule and updates the allowlisted example line number.
Regression tests for mixed Int/Nat typing tests/test_checker_int_nat.py	Adds coverage for mixed and same-kind binary arithmetic typing outcomes.
Update overflow-differential test expectations tests/test_int_overflow_differential.py	Updates the narrowed-result classification expectation and related docstring.
Changelog, known issues, roadmap, and testing docs updates CHANGELOG.md, KNOWN_ISSUES.md, ROADMAP.md, TESTING.md	Refreshes the release note, removes the resolved issue row, and updates test metrics and file listings.

Estimated code review effort: 3 (Moderate) | ~25 minutes

Sequence Diagram(s)

sequenceDiagram
  participant Source as Source expression
  participant Checker as _check_binary
  participant Join as numeric_join
  participant Verifier as overflow classification

  Source->>Checker: Int <op> Nat expression
  Checker->>Join: numeric_join(left_base, right_base)
  Join-->>Checker: Int for mixed Int/Nat, or shared base, or None
  Checker-->>Source: synthesised result type
  Source->>Verifier: overflow queries
  Verifier-->>Source: _overflow_int_type = Int, _overflow_arith_type = Int

Loading

Suggested labels: compiler, tests, spec, ci, docs

🚥 Pre-merge checks | ✅ 8

✅ Passed checks (8 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title is concise and accurately highlights the core fix: mixed Int/Nat arithmetic now resolves to Int via the formal LUB.
Linked Issues check	✅ Passed	The checker, type join, spec, and tests implement the required mixed Int/Nat arithmetic behaviour, with Nat only for Nat/Nat.
Out of Scope Changes check	✅ Passed	The changes are focused on the checker fix and supporting spec, tests, and docs updates; no unrelated code paths stand out.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Changelog Covers Public-Surface Changes	✅ Passed	PASS: the only public-surface change is spec/04-expressions.md, and CHANGELOG.md explicitly records the new mixed-arithmetic rule in spec §4.4.
Spec And Implementation Move Together	✅ Passed	PASS: checker/types use numeric_join for mixed Int/Nat arithmetic, and spec §4.4 now states the same LUB rule; Float64 remains excluded.
Diagnostics Carry An Error Code	✅ Passed	No new or changed diagnostic lost its stable code; the only touched checker error path still carries E141, and no uncoded Diagnostic/_error call was added.

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/755-int-nat-typing

---

_{Comment @coderabbitai help to get the list of available commands.}

[codecov]

Codecov Report

❌ Patch coverage is 84.61538% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 92.00%. Comparing base (99b250b) to head (575a7d3).

Files with missing lines	Patch %	Lines
vera/types.py	80.00%	2 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #862   +/-   ##
=======================================
  Coverage   92.00%   92.00%           
=======================================
  Files          95       95           
  Lines       28800    28809    +9     
  Branches      332      332           
=======================================
+ Hits        26497    26506    +9     
  Misses       2295     2295           
  Partials        8        8           

Flag	Coverage Δ
javascript	65.23% <ø> (ø)
python	94.95% <84.61%> (+<0.01%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[aallan]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[aallan]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.