Skip to content

checked arithmetic#1319

Merged
sbillig merged 11 commits intoargotorg:masterfrom
cburgdorf:checked_arithmetic2
Mar 10, 2026
Merged

checked arithmetic#1319
sbillig merged 11 commits intoargotorg:masterfrom
cburgdorf:checked_arithmetic2

Conversation

@cburgdorf
Copy link
Collaborator

@cburgdorf cburgdorf commented Mar 5, 2026

Summary

  • Arithmetic operators (+, -, *, unary -) now perform overflow/underflow checks at runtime for all integer types, reverting the transaction on overflow — matching Solidity 0.8+ behavior
  • Adds __checked_{add,sub,mul,neg}_<type> extern intrinsics in core::num that the MIR lowers operator expressions into, with overflow detection handled directly in the Sonatina and Yul backends
  • Introduces WrappingAdd/WrappingSub/WrappingMul and SaturatingAdd/SaturatingSub/SaturatingMul traits in core::ops as opt-in escape hatches for intentional wrapping/saturating semantics
  • Supports both signed and unsigned types across all bit widths (u8–u256, i8–i256, usize, isize), including proper sub-word masking and sign extension for types smaller than 256 bits
  • Adds compile-time overflow detection for const-context arithmetic (division by zero, overflow in const expressions)
  • Adds signed division (sdiv), signed modulo (smod), and arithmetic right shift (sar) support in the Sonatina backend
  • Adds comprehensive test coverage: checked_arithmetic_methods.fe, checked_arithmetic_regressions.fe, signed_arithmetic.fe with both happy-path and should_revert tests

Architecture: layered approach across backends

The implementation uses a layered strategy that keeps overflow semantics consistent while respecting the different needs of the Yul and Sonatina backends:

  1. Core stdlib (core::num): Operator trait impls (e.g. Add for u8) now call __checked_add_u8 instead of __add_u8. These __checked_* functions are declared as extern intrinsics — they have no Fe
    body. The unchecked __add_* variants remain available and are used by the Wrapping*/Saturating* trait impls.

  2. MIR: When the MIR lowers a call to a __checked_* extern, it attaches a CheckedIntrinsic metadata struct (carrying the CheckedArithmeticOp and the concrete TyId) to the CallOrigin. This gives
    backends typed information about what overflow check is needed without embedding any particular lowering strategy at the MIR level.

  3. Sonatina backend: The lower_checked_intrinsic function pattern-matches on the CheckedIntrinsic to emit the arithmetic instruction followed by an inline overflow test (e.g. result < lhs for unsigned
    add, sign-flag analysis for signed add) and a conditional branch to a revert block. All overflow logic is emitted as native Sonatina IR — no function calls, no runtime helpers.

  4. Yul backend: The YUL backend takes a fundamentally different approach. The overflow logic is implemented in Fe itself via core::num_yul
    — a set of generic helper functions (checked_add_unsigned_impl, checked_sub_signed_impl, etc.) that use the IntWord trait to operate on the word-level representation of any integer type. These generic
    helpers are monomorphized per type via thin wrappers (e.g. checked_add_u8, checked_neg_i256). When the Yul emitter encounters a __checked_* extern call, it resolves it to the corresponding
    core::num_yul::checked_* function, which gets compiled to Yul like any other Fe function. This means the Yul backend gets overflow checking "for free" through normal Fe compilation, without needing any
    special intrinsic handling.

@sbillig That part ☝️, I'm most unsure about. I remember from the last time we spoke that you set we should keep what we have implement in Fe but keep it YUL specific so this is why now the YUL backend uses num_yul.fe for all the safemath stuff whereas Sonatina doesn't go that extra route.

@cburgdorf cburgdorf force-pushed the checked_arithmetic2 branch 2 times, most recently from 90a6ce9 to ad76396 Compare March 6, 2026 17:35
@sbillig
Copy link
Collaborator

sbillig commented Mar 6, 2026

@cburgdorf
I think we should add instructions to sonatina for the overflow check; something like this:

v2.i64 = add v1 v0
v3.i1 = uadd_overflow v0 v1
br v3 %panic %ok
panic:
  evm_revert ...
ok:
  ...

Or, we could add support for multiple returns to the sonatina ir, and add arithmetic instructions that output two values.
v2.i64, v3.i1 = sadd_overflow v0 v1

Minor nitpick, the fe intrinsics could be generic: checked_add<T>(_: T, _: T). Could add a private marker trait to restrict usage to primitive int types.


/// Returns the masking info for a sub-256-bit intrinsic, or `None` for 256-bit
/// types that don't need masking.
fn sub_word_mask(callee_name: &str) -> Option<SubWordMask> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fe should create sonatina ir that uses sonatina int sizes (i8, i16, etc) that match the fe int size, instead of always using i256, and let sonatina handle any masking etc. I don't think it currently does this, so doing it in fe would be fine for now.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think it currently does this

Yes, right. The normal arithmetic doesn't do it yet but I now did so for the checked arithmetic. I'll add another commit to expand it to the non-checked arithmetic.

@sbillig
Copy link
Collaborator

sbillig commented Mar 6, 2026

@cburgdorf I think we should add instructions to sonatina for the overflow check; something like this:

v2.i64 = add v1 v0
v3.i1 = uadd_overflow v0 v1
br v3 %panic %ok
panic:
  evm_revert ...
ok:
  ...

Or, we could add support for multiple returns to the sonatina ir, and add arithmetic instructions that output two values. v2.i64, v3.i1 = sadd_overflow v0 v1

Minor nitpick, the fe intrinsics could be generic: checked_add<T>(_: T, _: T). Could add a private marker trait to restrict usage to primitive int types.

I'm leaning toward allowing multiple returns in sonatina ir. This would be useful for optimizing functions that return an aggregate; we could transform them into functions that return multiple scalar values. I'll start working on this today.

@cburgdorf cburgdorf force-pushed the checked_arithmetic2 branch from ad76396 to 1eb230d Compare March 7, 2026 16:49
@cburgdorf cburgdorf marked this pull request as ready for review March 7, 2026 17:31
@cburgdorf
Copy link
Collaborator Author

@codex review

@cburgdorf
Copy link
Collaborator Author

cburgdorf commented Mar 7, 2026

Minor nitpick, the fe intrinsics could be generic: checked_add<T>(_: T, _: T). Could add a private marker trait to restrict usage to primitive int types.

I refactored that but used the existing IntWord trait as the bound.

Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1eb230d6e2

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@cburgdorf cburgdorf force-pushed the checked_arithmetic2 branch from 1eb230d to 4bac28c Compare March 7, 2026 18:19
@sbillig
Copy link
Collaborator

sbillig commented Mar 7, 2026

@cburgdorf fe-lang/sonatina#210

let overflow_block = builder.append_block();
let ok_block = builder.append_block();

let [sum, overflow] = builder.insert_uaddo(lhs, rhs);
builder.insert_inst_no_result(Br::new(is, overflow, overflow_block, ok_block));

new ops are:
uaddo (unsigned add overflow)
uaddo
saddo
usubo
ssubo
umulo
smulo
snego

EVM-specific ops: (div-by-zero = 0)
evm_udivo
evm_sdivo
evm_umodo
evm_smodo

@sbillig
Copy link
Collaborator

sbillig commented Mar 7, 2026

I also have this branch that adds a legalization pass for the evm backend, to properly handle smaller int sizes (with appropriate masks, sign extension, etc): fe-lang/sonatina#209

So, the sonatina codegen in fe can just emit ops on small int sizes.

I'll try to get both of these checked and merged today.

@cburgdorf
Copy link
Collaborator Author

@sbillig I can look deeper into the Sonatina tomorrow evening or on Monday. For now I'm just cleaning up the current state to address all the remaining issues that codex highlighted.

@cburgdorf
Copy link
Collaborator Author

@codex review

@cburgdorf
Copy link
Collaborator Author

@sbillig I updated this to your latest Sonatina changes. It does depend on this extra fix though fe-lang/sonatina#213

@chatgpt-codex-connector
Copy link

Codex Review: Didn't find any major issues. More of your lovely PRs please.

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@sbillig
Copy link
Collaborator

sbillig commented Mar 10, 2026

@codex review

Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 817a45a4ac

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@sbillig
Copy link
Collaborator

sbillig commented Mar 10, 2026

@codex review

Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0409f74d7b

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@sbillig sbillig merged commit c6f0441 into argotorg:master Mar 10, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants