Type Int.div and Int.mod with a nonzero literal divisor as total

[jasisz]

Rule

Int.div(x, K) / Int.mod(x, K) where K is a syntactic nonzero integer literal now type as plain Int (previously Result<Int, String>), and every backend emits direct Euclidean division. A 0 literal and every non-literal divisor are completely unchanged (Result path, no error, no warning).

Boundary (deliberate, syntactic only): a literal, optionally under one unary minus, plus BigInt literals (nonzero by construction — the lexer only produces them past i64). Identifiers, named constants, constant expressions (8 + 8), and --5 do not discharge. Pinned by literal_divisor_discharge_boundary_is_syntactic_literals_only in tests/typechecker_spec.rs, so widening the rule later requires touching a test named after the boundary. The typechecker stays solver-free.

Mechanism

One shared predicate (ast::is_literal_nonzero_int_divisor) drives two seams:

• the typechecker's Int.div/Int.mod special-case arm returns Int (arg checks unchanged; the registered Result signature stays for the dynamic path);
• the HIR resolver lowers the same shape to the pre-existing IntDivEuclid/IntModEuclid intrinsics, which every consumer already handles: VM opcodes, Rust div_euclid().unwrap(), the wasm-gc/wasip2 bignum __aint_divmod helper, Lean (a / k) (Int.ediv), Dafny (a / k) (Euclidean). The resolver keys on syntax, not type stamps — some pipelines resolve without typechecking.

Semantics evidence

• New cross-backend differential (cross_literal_divisor_discharge_vm_vs_wasm_gc_vs_rust): VM, wasm-gc, and generated Rust are byte-identical over the sign/boundary matrix (7 dividends × 6 literal divisors, incl. -1, i64::MIN, and Big 2^63), and in-program the discharged value == the dynamic-divisor Result.Ok value on every pair.
• wasip2 smoke: byte-identical to the VM, incl. Int.div(i64::MIN, -1) = 9223372036854775808.
• Proof export: tests/fixtures/discharged_div_law.av (half(a) = Int.div(a, 2) rendered as (a / 2)) — the doubling law certifies universally in Lean (0 sorries, universal: true) and verifies in Dafny (7 verified, 0 errors). Both new proof_spec tests are toolchain-gated like their neighbors and were run locally with lake (Lean 4.32) and Dafny 4.11.

Stale-premise rider

Over ℤ there is no i64::MIN / -1 overflow — it is the valid Big quotient 2^63. Lifted the const-fold's dead k == -1 exclusion (unit test flipped to assert the fold fires; an eval differential routes MIN / (0 - 1) through the lifted arm), and corrected the false overflow claim in the Int.div/Int.mod header docs (src/types/int.rs, which also claimed truncating div and sign-of-b mod), the VM opcode caller contract, and the /-operator diagnostic (message, pinned test, int-div repair hint).

Migration and proof coverage

The old idiom Result.withDefault(Int.div(a, K), d) is a type error under the new rule; all 66 example sites and the test corpus migrated mechanically to bare Int.div(a, K) (value-identical — the default was dead code for nonzero literal K). The literal-divisor termination recognizers (shared inline_floor_div_shrink, Dafny-local is_literal_div_shrink) now accept the bare shape alongside the legacy wrapper, so the floor-window family and the bigint base-10⁹ digit peel keep their well-founded emissions. tests/fixtures/result_default_cone.av keeps its decline-testing intent via a bound (non-literal) divisor.

Out of scope

• Self-hosted pipeline (same scoping as the sendBytes precedent): a separate Aver-written implementation with no typechecker and zero literal-divisor sites in its own sources. A discharged-form program evaluated under --self-host still gets a Result value from builtin div — divergence documented here.
• tools/website/playground/sources/ copies of the migrated examples: they pair with the checked-in playground WASM and both regenerate at release time, so they are deliberately untouched.

Tests

• cargo test --workspace: 2512 passed
• full proof_spec with lake + Dafny available locally: 227 passed
• wasm suites (--features wasm,wasip2): wasm_gc_spec, capture_output, games differential, carrier differential, new cross-backend differential — all green
• cargo fmt --check clean; clippy (--features wasm,wasip2 --tests) has no warnings in touched files

🤖 Generated with Claude Code