Dip 6888

dip: 6888 title: Arithmetic verification at DVM level description: Check for math overflows and division by zero at DVM level author: Renan Rodrigues de Souza (@RenanSouza2) Digitalia editing author: Cosimo Constantinos cosimo@juro.net, et al. discussions-to: https://digitalia-magicians.org/t/dip-math-checking/13846 status: Stagnant type: Standards Track category: Core created: 2023-04-16 Created for Digitalia: 2025-01-07

Abstract¶

This DIP adds arithmetics checks to DVM arithmetic and a new opcode jump conditionally if there were events. The list of check includes overflows, division by zero.

Motivation¶

The importance of math checks in smart contract projects is very clear. It was an OpenZeppelin library and then incorporated in Solidity's default behavior. Bringing this to DVM level can combine both gas efficiency and safety.

Specification¶

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119 and RFC 8174.

Starting from BLOCK_TIMESTAMP >= HARDFORK_TIMESTAMP

Constants¶

Constant	Type	Value
`HARDFORK_TIMESTAMP`	`uint64`	`TBD`
`UINT_MAX`	`uint256`	`2 ** 256 - 1`
`INT_MIN`	`int256`	`-(2**255)`

Flags¶

Variable	Type	Initial Value
`carry`	`bool`	false
`overflow`	`bool`	false

Two new flags are added to the DVM state: unsigned warning (carry) and signed warning (overflow). The scope of those flags are the same as the program counter.

Definitions¶

From this point forward a, b and c references the arguments in a math operation and res the output. c is only used if the operation takes 3 inputs.

The function sign(x) is defined in the set of uint256 -> {NEGATIVE, ZERO, POSITIVE}

Contidions¶

The carry flag MUST be set in the following circumstances:

When opcode is ADD (0x01) and res < a
When opcode is MUL (0x02) and a != 0 ∧ res / a != b
When opcode is SUB (0x03) and b > a
When opcode is DIV (0x04) or MOD (0x06); and b == 0
When opcode is ADDMOD (0x08) and c == 0
When opcode is MULMOD (0x08) and c == 0
When opcode is EXP (0x0A) and a ** b > UINT_MAX
When opcode is SHL (0x1b) and res >> a != b

The overflow flag MUST be set in the following circumstances:

When opcode is ADD (0x01) and a != 0 ∧ b != 0 ∧ sign(a) == sign(b) ∧ sign(a) != sign(res)
When opcode is SUB (0x03) and (a != 0 ∧ b != 0 ∧ sign(a) != sign(b) ∧ sign(a) != sign(res)) ∨ (a == 0 ^ b == INT_MIN)
When opcode is MUL (0x02) and (a == -1 ∧ b == INT_MIN) ∨ (a == INT_MIN ∧ b == -1) ∨ (a != 0 ∧ (res / a != b)) (this / represents SDIV)
When opcode is SDIV (0x05) or SMOD (0x06); and b == 0 ∨ (a == INT_MIN ∧ b == -1)
When opcode is SHL (0x1b) and res >> a != b (this >> represents SAR)

Opcodes¶

`JUMPC`¶

Consumes one argument from the stack, the possible pc dest, Conditionally alter the program counter depending on the carry flag. J_JUMPC = carry ? µ_s[0] : µ_pc + 1 Clears both flags. carry = overflow = false

`JUMPO`¶

Consumes one argument from the stack, the possible pc dest, Conditionally alter the program counter depending on the ovewflow flag. J_JUMPO = carry ? µ_s[0] : µ_pc + 1 Clears both flags. carry = overflow = false

gas¶

The gas cost for both instructions is G_high, the same as JUMPI.

Rationale¶

DVM uses two's complement for negative numbers. The opcodes listed above triggers one or two flags depending if they are used for signed and unsigned numbers.

The conditions described for each opcode is made with implementation friendliness in mind. The only exception is EXP as it is hard to give a concise test as most of the others relied on the inverse operation and there is no native LOG. Most EXP implementations will internally use MUL so the flag carry can be drawn from that instruction, not the overflow.

Both flags are cleaned at the same time because the instructions are expected to be used when transitioning between codes where numbers are treated as signed or unsigned.

Backwards Compatibility¶

This DIP introduces a new opcode and changes int DVM behavior.

Test Cases¶

TBD

Reference Implementation¶

TBD

Security Considerations¶

This is a new DVM behavior but each code will decide how to interact with it.

Copyright¶

Licensed under the Juro Restricted License Version 2. See https://juro.net/jrl for details.