fix: correct OTP 29 conformance gaps in BIFs, map order, and actors

[henry-hz]

Summary

A review of the interpreter, importer, actor runtime, and CLI (Main.lean) found seven places where the model disagreed with OTP 29 or accepted invalid input. Each fix keeps the existing proofs and axiom audit intact — no sorry, no new unsound axioms.

• byte_size/1 raised badarg on a bitstring that doesn't end on a byte boundary. OTP rounds up instead (byte_size(<<1:1>>) is 1). Fixed in Erlean/Semantics/Machine.lean.
• iolist_to_binary/1 accepted a bare integer (iolist_to_binary(65)) and an integer as the list tail ([65|66]). OTP raises badarg for both; a binary on its own or as the list tail is still accepted.
• Map ordering: maps:iterator(M, ordered | reversed), maps:keys/1, and maps:values/1 returned the model's internal storage order, which is not Erlang term order (e.g. it put negative integers after positive ones and [] before tuples). Added Erlean/Core/TermOrder.lean, defining Erlang's term order for the supported key types, and wired it into these functions.
• Other maps gaps:
  • maps:next(none) now returns none, as in OTP.
  • maps:iterator(M, undefined) is now accepted.
  • An ordering fun passed to maps:iterator/2 is now reported as unsupported instead of wrongly raising badarg.
• demonitor/1 with a monitor reference owned by another process raised badarg. OTP only looks at the caller's own monitors, so it now does nothing and returns true (Erlean/Runtime/Actors.lean).
• Number parsing: input integers, bitstring lengths, and the CLI fuel argument were read with Lean's toNat?/toInt?, which also accept _ separators such as "1_000". Added strict decimal parsers in Erlean/Import/RawCore.lean.
• CLI: emit produced a broken Lean file when the declaration name was a Lean keyword (e.g. end); it now rejects such names and names not starting with a letter. run-linked with no artifact files now gives a clear error.

Testing

• Regression tests: new cases in tests/semantics/Regression.lean, tests/semantics/ActorChecks.lean, and tests/import/Smoke.lean. The old test that expected byte_size to reject a partial byte now expects the OTP result.
• OTP comparison cases: new cases for the byte_size and iolist_to_binary fixes in tools/check_scalar_bifs.mjs.
• Proofs: two new lemmas about the term order, proved without sorry, added to tests/semantics/Axioms.lean: every key compares equal to itself (termCompare_self), and sorting keeps the number of entries (termOrdered_length). No existing proof needed changes.

Test plan

• node tools/build.mjs — full serialized dependency-ordered build succeeds
• lake env lean -j1 -M2048 --run tests/import/Smoke.lean passes
• lake env lean -j1 -M2048 --run tests/semantics/Regression.lean passes
• lake env lean -j1 -M2048 --run tests/semantics/ActorChecks.lean passes
• lake env lean -j1 -M2048 tests/semantics/Axioms.lean — clean axiom audit (no sorryAx, ofReduceBool, or native_decide)
• node tools/check_all.mjs (full OTP/Elixir/Gleam differential suite) — not run; this environment does not have the pinned Erlang/Elixir/Gleam toolchain installed, so the OTP-side behavior changes are not yet differentially confirmed. Please run this before merging on a machine with OTP 29.0.6, Elixir 1.20.0, and Gleam 1.18.1 installed per .tool-versions.

🤖 Generated with Claude Code

---

^{Need help on this PR? Tag @codesmith-bot with what you need. Autofix is disabled.}