4 Numbers — fixed-width integers and floating point

4.1 Integer types name their width#

An integer type’s name is its sign and bit width. u means unsigned, i means signed.

C’s int can have different sizes on different machines, but Lowent’s u32 is 32 bits everywhere. Negative numbers use two’s complement. usize is a different type from u64 even on a machine where they have the same width, and the two do not convert automatically — so that places mixing address counts with plain numbers show in the source.

4.2 Widening is automatic, narrowing is written#

A conversion that loses no value is called widening. Passing a u8 where a u32 is expected keeps the value, so the compiler does it for you. Even with mixed signs, arithmetic is allowed if a value-preserving widening exists — every u8 fits in an i16.

module widths .
rem run: mix 200 -100
rem run: shrink 200
rem trap: shrink 300
rem run: shrink_sat 300
rem run: shrink_wrap 300

fn mix input a u8 . input b i16 . output i16 .
do
  return add a b .
end

fn shrink input x u64 . output u8 .
do
  return narrow u8 x .
end

fn shrink_sat input x u64 . output u8 .
do
  return narrow_sat u8 x .
end

fn shrink_wrap input x u64 . output u8 .
do
  return narrow_wrap u8 x .
end

$ lowentc --run mix widths.low 200 -100
mix(200, -100) = 100
$ lowentc --run shrink widths.low 200
shrink(200) = 200
$ lowentc --run shrink_sat widths.low 300
shrink_sat(300) = 255
$ lowentc --run shrink_wrap widths.low 300
shrink_wrap(300) = 44
$ lowentc --run shrink widths.low 300
== ir diagnostics (1) ==
0:0 E-VM-CAST: value does not fit the target width (use narrow_wrap / narrow_sat / narrow_try)

mix adds a u8 and an i16, and the result has the wider type, i16. To make the widening visible, write widen u64 x. An i32 and a u32 of the same width cannot be mixed, because neither fits entirely in the other.

module sign_bad .
rem expect: E-TYPE-SIGN

fn total input a i32 . input b u32 . output i32 .
do
  return add a b .
end

$ lowentc --check sign_bad.low
sign_bad.low:6:0 E-TYPE-SIGN: sign mismatch: no value-preserving widening exists (widen both to a strictly wider signed type, or bitcast_sign)

A conversion that can lose a value is narrowing, and it must be written. shrink in the same file narrows a u64 to a u8 with narrow u8 x. 200 fits and comes out unchanged, but 300 does not, so execution stops (E-VM-CAST). If you do not want it to stop, choose the treatment you want by name. narrow_sat stops at the end value 255, and narrow_wrap wraps like C and gives 44. narrow_try gives none when the value does not fit.

4.3 Overflow stops#

Arithmetic happens at the declared width. If the result does not fit the width, execution stops (a trap).

module overflow .
rem run: bump 254
rem trap: bump 255
rem run: bump_wrap 255
rem run: bump_sat 255

fn bump input a u8 . output u8 .
do
  return add a 1 .
end

fn bump_wrap input a u8 . output u8 .
do
  return wrap_add a 1 .
end

fn bump_sat input a u8 . output u8 .
do
  return sat_add a 1 .
end

$ lowentc --run bump overflow.low 254
bump(254) = 255
$ lowentc --run bump_wrap overflow.low 255
bump_wrap(255) = 0
$ lowentc --run bump_sat overflow.low 255
bump_sat(255) = 255
$ lowentc --run bump overflow.low 255
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)

bump 254 fits as 255, but bump 255 would have to be 256, so the VM stops with E-VM-OVERFLOW. Native code stops at the same place with a non-zero exit code (the verification script checks that both stop). As with widening, you change the treatment by choosing a name.

The “as a value” family turns overflow into an event the program can handle.

module chk .
rem run: safe_bump 255
rem run: safe_bump 7

fn safe_bump input a u8 . output u64 .
do
  let r option u8 be chk_add a 1 .
  guard is_some r . else return 999 .
  return widen u64 (some_value r) .
end

$ lowentc --run safe_bump chk.low 255
safe_bump(255) = 999
$ lowentc --run safe_bump chk.low 7
safe_bump(7) = 8

chk_add a 1 gives an option u8. On overflow it is none, and guard is_some r . else … handles that case first. You will meet this shape again in chapter 11.

4.4 Division and remainder#

Dividing an integer by zero stops. Signed division truncates towards zero, and the sign of the remainder mod follows the divisor.

module divide .
rem run: quot -7 2
rem run: modulo -7 2
rem trap: quot 1 0
rem run: safe_div 7 0
rem run: safe_div 7 2

fn quot input a i32 . input b i32 . output i32 .
do
  return div a b .
end

fn modulo input a i32 . input b i32 . output i32 .
do
  return mod a b .
end

fn safe_div input a u32 . input b u32 . output u32 .
do
  let nz option nonzero u32 be nonzero_of b .
  guard is_some nz . else return 0 .
  return div_nz a (some_value nz) .
end

$ lowentc --run quot divide.low -7 2
quot(-7, 2) = -3
$ lowentc --run modulo divide.low -7 2
modulo(-7, 2) = 1
$ lowentc --run safe_div divide.low 7 0
safe_div(7, 0) = 0
$ lowentc --run safe_div divide.low 7 2
safe_div(7, 2) = 3
$ lowentc --run quot divide.low 1 0
== ir diagnostics (1) ==
0:0 E-VM-DIV0: divide by zero

quot -7 2 is −3 and modulo -7 2 is 1. Because the remainder follows the divisor’s sign, mod h n for a positive n is always at least 0 and less than n. That property is why the bounds check in index slots (mod h n) disappears when a hash table picks a slot, and it is proven in Coq (chapter 40).

The only case where signed division overflows is MIN / −1, and that stops too. In C it is undefined behaviour.

There is also a way to check once that a divisor is not zero and carry that fact around. nonzero_of b gives an option nonzero u32, and the value inside can be passed to div_nz. No zero check remains at the div_nz site. The check was not removed but moved to one place, with its result carried in the type.

4.5 Booleans are not numbers#

bool has two values, true and false. An integer in a condition is rejected.

module cond_bad .
rem expect: E-TYPE-COND

fn nonzero_flag input n u32 . output u8 .
do
  if n . do return 1 . end
  return 0 .
end

$ lowentc --check cond_bad.low
cond_bad.low:6:0 E-TYPE-COND: a condition must be bool, not a number — this language has no truthiness (D12: no implicit int↔bool). Say what the test is: `ne x 0`

C’s if (n) reads as “n is not zero”, but the reader has to guess from context whether it means “n exists” or “n is true”. Lowent makes you write what you are asking — if gt n 0 .. Conversely, a bool cannot be added like a number. and, or and not take only booleans, and and and or skip the right-hand side when the left-hand side already decides the answer.

4.6 Bitwise operations#

Bitwise operations treat a value as a sequence of bits. They use words instead of symbols.

module bits .
rem run: mask 12 10
rem run: flip 12
rem run: spin 129 1
rem run: s_shr -8 1
rem run: u_shr 4294967288 1
rem run: ones 7

rem 12 = 0000_1100 · 10 = 0000_1010
fn mask input a u8 . input b u8 . output u8 . do return bit_and a b . end
fn flip input a u8 . output u8 . do return bit_not a . end
fn spin input a u8 . input n u8 . output u8 . do return rotl a n . end
fn s_shr input a i32 . input n i32 . output i32 . do return shr a n . end
fn u_shr input a u32 . input n u32 . output u32 . do return shr a n . end
fn ones input a u8 . output u8 . do return count_ones a . end

$ lowentc --run mask bits.low 12 10
mask(12, 10) = 8
$ lowentc --run flip bits.low 12
flip(12) = 243
$ lowentc --run spin bits.low 129 1
spin(129, 1) = 3
$ lowentc --run s_shr bits.low -8 1
s_shr(-8, 1) = -4
$ lowentc --run u_shr bits.low 4294967288 1
u_shr(4294967288, 1) = 2147483644
$ lowentc --run ones bits.low 7
ones(7) = 3

• bit_and · bit_or · bit_xor · bit_not — bitwise logic. flip 12 is 243 because the type is u8. The answer of a bitwise operation is always tied to the width of its type.
• shl and shr shift; rotl and rotr rotate. spin 129 1 is 3 because the top 1 came back in at the bottom; with shl that 1 would have been discarded.
• shr means different things depending on sign. −8 and 4294967288 are the same bit pattern in 32 bits, but the signed one shifts in the sign bit and becomes −4, while the unsigned one shifts in 0 and becomes 2147483644.
• count_ones · leading_zeros · trailing_zeros count bits, and byte_swap reverses byte order.
• clmul_lo · clmul_hi are carry-less multiplication — a product whose addition is xor, with no carries. Cryptography and checksums (GF(2^128), CRC) stand on it. The answer is 128 bits, so it comes back as two words. When the machine has the instruction the processor lowers to it (lowentc --hw pclmul, or auto), and when it does not, to the same computation in plain code — one meaning, two speeds.

Shifting by at least the width of the type stops. In C that is undefined behaviour. If you want the shift amount wrapped into the width, use wrap_shl and wrap_shr.

4.7 Floating point#

f32 and f64 are the IEEE 754 binary 32- and 64-bit formats. Operations happen at the width of their operands, and integers and floating-point values do not convert to each other automatically.

module floats .
rem run: third 1.0
rem run: hyp 3.0 4.0

fn third input x f64 . output f64 .
do
  return div x 3.0 .
end

fn hyp input a f64 . input b f64 . output f64 .
do
  return sqrt (add (mul a a) (mul b b)) .
end

$ lowentc --run third floats.low 1.0
third(1.0) = 0.333333
$ lowentc --run hyp floats.low 3.0 4.0
hyp(3.0, 4.0) = 5.0

The VM shows floating-point results briefly (0.333333). Dividing a floating-point value by zero does not stop; it becomes infinity as IEEE 754 prescribes. Transcendental functions such as sqrt, sin and exp are floating-point only and available only on machines with an operating system. The exact last bit of their results is up to the machine and its maths library.

f32 and the size types follow the same rules.

module sizes .
rem run: step 5 -8
rem run: third32 1.0
rem run: same_third 1.0 1.0

rem usize and isize have the machine's address width (64 bits on a 64-bit machine); use them to exchange lengths and indexes with C
fn step input n usize . input k isize . output isize .
  requires le n 1000 .
  requires ge k -1000 .
  requires le k 1000 .
do
  return add (cast isize n) k .
end

rem f32 is a 32-bit float: half the memory, about seven significant digits
fn third32 input x f32 . output f32 . do
  return div x 3.0 .
end

rem even 1/3 is a different number in f32 and f64; widened and compared, they are not equal
fn same_third input x f32 . input y f64 . output bool . do
  let a f32 be div x 3.0 .
  let b f64 be div y 3.0 .
  return eq (widen f64 a) b .
end

$ lowentc --run step sizes.low 5 -8
step(5, -8) = -3
$ lowentc --run third32 sizes.low 1.0
third32(1.0) = 0.333333
$ lowentc --run same_third sizes.low 1.0 1.0
same_third(1.0, 1.0) = 0

• usize and isize are unsigned and signed integers with the machine’s address width. Use them to exchange lengths and indexes with C’s size_t and ptrdiff_t (chapter 29). Their width may differ between machines, so use u64 and i64 for fixed-width arithmetic. Moving to a type of the other signedness goes through a named operation such as cast isize n.
• f32 takes half the memory and has about seven significant digits. Use it where quantity matters more than precision, as in large arrays or graphics.
• same_third computes the same 1/3 as f32 and as f64, widens, and compares. The answer is false (0). Even though the VM shows both briefly as 0.333333, they are different numbers.

4.8 Common mistakes#

Many number mistakes pass compilation and only show up while running. Where other languages would quietly produce a wrong value, Lowent stops — and the place it stops is the place to fix.

module mistake_midpoint .
rem trap: mid 200 100

fn mid input a u8 . input b u8 . output u8 .
do
  rem ✘ adding first gives 300, which does not fit in u8
  return div (add a b) 2 .
end

$ lowentc --run mid mistake_midpoint.low 200 100
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)

module midpoint_fixed .
rem run: mid 200 100
rem run: mid 255 255

fn mid input a u8 . input b u8 . output u8 .
do
  rem add one width up --- u16 holds up to 510
  let both u16 be add (widen u16 a) (widen u16 b) .
  rem half of it fits in u8 again; we know that, and narrow checks it
  return narrow u8 (div both 2) .
end

$ lowentc --run mid midpoint_fixed.low 200 100
mid(200, 100) = 150
$ lowentc --run mid midpoint_fixed.low 255 255
mid(255, 255) = 255

module mistake_usub .
rem trap: gap 3 5

fn gap input a u64 . input b u64 . output u64 .
do
  rem ✘ unsigned numbers cannot go below 0 --- 3 − 5 is not negative, it stops
  return sub a b .
end

$ lowentc --run gap mistake_usub.low 3 5
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)

module mistake_narrowloop .
rem expect: E-TYPE-WIDTH

fn tally output u64 .
do
  rem ✘ a u8 loop counter has nothing after 255 --- the 256th `add i 1` stops
  var i u8 be 0 .
  var n u64 be 0 .
  while lt i 256 . do
    set n (add n 1) .
    set i (add i 1) .
  end
  return n .
end

$ lowentc --check mistake_narrowloop.low
mistake_narrowloop.low:9:0 E-TYPE-WIDTH: this comparison holds a value that the other side's type cannot hold, so the answer is the same for every input — the comparison decides nothing. A name declared `u8` is at most 255, `u16` at most 65535, `i8` at most 127; a literal beyond that is out of range exactly as it would be in an assignment, where the tool has always refused it. Widen the name's type, or compare against a value the type can reach. (This is how a loop written `while lt i 256 .` over a `u8` counter never ends)

module mistake_floatint .
rem expect: E-TYPE-MIX

fn half input x f64 . output f64 .
do
  rem ✘ divides an f64 by the integer literal 2 --- write 2.0 where a float is expected
  return div x 2 .
end

$ lowentc --check mistake_floatint.low
mistake_floatint.low:7:0 E-TYPE-MIX: a floating-point value and an INTEGER literal are mixed in one operation. Floating point and integers do not convert implicitly (§6.2.5), so write the literal as a float (`2.0`) — or convert the other side. It used to pass `--check` and stop at run time (`E-VM-TYPE: arithmetic needs ints`)

module mistake_runmax .
rem trap: echo 18446744073709551615
rem test

rem ✘ giving the upper half of u64 as a `--run` argument is refused at the boundary: the interval analysis believes u64 tops out at the i64 maximum
fn echo input n u64 . output u64 .
do
  return n .
end

rem write boundary values as literals inside a test
test largest_u64
do
  let m u64 be 18446744073709551615 .
  expect gt m 9223372036854775807 .
  expect eq (div m 2) 9223372036854775807 .
end

$ lowentc --run echo mistake_runmax.low 18446744073709551615
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: a parameter's TYPE range was violated at the program boundary — the value does not fit the declared type (the interval analysis TRUSTS the type and deletes checks on that basis; the boundary is what makes that trust true)
$ lowentc --test mistake_runmax.low
  [PASS] largest_u64
== tests: 1 run, 1 passed, 0 FAILED ==

module mistake_f32literal .
rem run: stored
rem run: computed

rem ✘ an f32 holding a literal as is; in this edition it is not rounded to 32 bits, so it compares equal to the f64 0.1
fn stored output bool . do
  let a f32 be 0.1 .
  let b f64 be 0.1 .
  return eq (widen f64 a) b .
end

rem an f32 that went through one operation (0.1 + 0) is rounded to 32 bits and compares unequal
fn computed output bool . do
  let a f32 be 0.1 .
  let c f32 be add a 0.0 .
  let b f64 be 0.1 .
  return eq (widen f64 c) b .
end

$ lowentc --run stored mistake_f32literal.low
stored() = 0
$ lowentc --run computed mistake_f32literal.low
computed() = 0

module intdiv .
rem run: avg2 3 4
rem run: avg_f 3.0 4.0

fn avg2 input a u64 . input b u64 . output u64 .
do
  rem integer division drops the fraction --- 7 / 2 is 3
  return div (add a b) 2 .
end

fn avg_f input a f64 . input b f64 . output f64 .
do
  rem if you need the fraction, compute in floating point from the start
  return div (add a b) 2.0 .
end

$ lowentc --run avg2 intdiv.low 3 4
avg2(3, 4) = 3
$ lowentc --run avg_f intdiv.low 3.0 4.0
avg_f(3.0, 4.0) = 3.5

The floating-point remainder gets its own name, fmod, separate from the integer mod.

module floatmod .
rem run: rest
rem run: whole_rest 7 2

rem the floating-point remainder is `fmod` --- a different name from the integer `mod`
fn rest output f64 .
do
  return fmod 7.5 2.0 .
end

fn whole_rest input a u64 . input b u64 . output u64 .
  requires gt b 0 .
do
  return mod a b .
end

$ lowentc --run rest floatmod.low
rest() = 1.5
$ lowentc --run whole_rest floatmod.low 7 2
whole_rest(7, 2) = 1

fmod 7.5 2.0 is 1.5 and mod 7 2 is 1. Not loading two kinds onto one name is the same reason as for div — what is computed shows in the name.

4.9 This chapter’s syntax at a glance#