4 수 — 폭이 정해진 정수와 부동소수

4.1 정수 타입은 이름에 폭을 적는다#

정수 타입의 이름은 부호와 비트 폭이다. u 는 부호 없음, i 는 부호 있음이다.

C 의 int 는 기계마다 크기가 다를 수 있지만, Lowent 의 u32 는 어디서나 32 비트다. 음수는 2 의 보수로 표현한다. usize 는 u64 와 폭이 같은 기계에서도 다른 타입이고 서로 자동으로 바뀌지 않는다 — 주소를 세는 수와 그냥 수를 섞는 자리를 소스에 드러내기 위해서다.

4.2 넓히기는 자동, 좁히기는 적는다#

값을 잃지 않는 변환을 넓히기라 한다. u8 을 u32 자리에 넘기는 일은 값이 그대로이므로 컴파일러가 알아서 한다. 부호가 섞여도 값을 지키는 넓히기가 있으면 계산할 수 있다 — u8 은 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 는 u8 과 i16 을 더했고 결과는 넓은 쪽인 i16 이다. 넓히기를 눈에 보이게 적고 싶으면 widen u64 x 로 적는다. 같은 폭의 i32 와 u32 는 어느 쪽도 다른 쪽에 다 들어가지 않으므로 섞을 수 없다.

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)

값을 잃을 수 있는 변환은 좁히기이고 반드시 적는다. 같은 파일의 shrink 는 narrow u8 x 로 u64 를 u8 로 줄인다. 200 은 들어가서 그대로 나오지만, 300 은 들어가지 않으므로 실행이 멈춘다 (E-VM-CAST). 멈추지 않기를 원하면 원하는 처분을 이름으로 고른다. narrow_sat 는 끝값 255 에 서고, narrow_wrap 은 C 처럼 감아서 44 를 준다. narrow_try 는 들어가지 않으면 none 을 준다.

4.3 넘치면 멈춘다#

산술은 선언된 폭에서 일어난다. 결과가 폭에 들어가지 않으면 멈춘다(트랩).

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 는 255 로 들어가지만 bump 255 는 256 이 되어야 하므로 VM 이 E-VM-OVERFLOW 로 멈춘다. 네이티브도 같은 자리에서 멈추고 비영 종료 코드를 낸다(검증 스크립트는 둘 다 멈추는지를 확인한다). 처분을 바꾸려면 넓히기와 마찬가지로 이름을 고른다.

“값으로” 알리는 쪽은 넘침을 프로그램이 다룰 수 있는 사건으로 만든다.

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 은 option u8 을 준다. 넘치면 none 이고, guard is_some r . else … 가 그 경우를 먼저 처리한다. 이 모양은 11장에서 다시 만난다.

4.4 나눗셈과 나머지#

정수를 0 으로 나누면 멈춘다. 부호 있는 나눗셈은 0 쪽으로 버리고, 나머지 mod 의 부호는 나누는 수를 따른다.

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 는 −3 이고 modulo -7 2 는 1 이다. 나머지가 나누는 수의 부호를 따르므로, 양수 n 으로 나눈 mod h n 은 언제나 0 이상 n 미만이다. 해시 테이블이 슬롯을 고를 때 index slots (mod h n) 의 경계 검사가 지워지는 근거가 이 성질이고, 이 성질은 Coq 로 증명되어 있다(40장).

부호 있는 나눗셈이 넘치는 경우는 MIN / −1 하나뿐이고, 이것도 멈춘다. C 에서는 미정의 동작이다.

0 이 아님을 한 번 확인하고 그 사실을 들고 다니는 길도 있다. nonzero_of b 는 option nonzero u32 를 주고, 그 안의 값은 div_nz 에 넘길 수 있다. div_nz 자리에는 0 검사가 남지 않는다. 검사를 없앤 것이 아니라 한 자리로 옮기고 그 결과를 타입에 실은 것이다.

4.5 참거짓은 수가 아니다#

bool 은 true 와 false 두 값이다. 정수를 조건 자리에 쓰면 거절된다.

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 의 if (n) 은 “n 이 0 이 아니다” 로 읽히지만, 읽는 사람은 그것이 “n 이 있다” 인지 “n 이 참이다” 인지 문맥으로 짐작해야 한다. Lowent 는 묻는 것을 적게 한다 — if gt n 0 . 이다. 반대로 bool 을 수처럼 더할 수도 없다. and·or·not 은 참거짓만 받고, and 와 or 는 앞쪽만으로 답이 정해지면 뒤쪽을 계산하지 않는다.

4.6 비트 연산#

비트 연산은 값을 비트의 나열로 보고 다룬다. 기호 대신 낱말이다.

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 — 비트별 논리. flip 12 가 243 인 것은 u8 이기 때문이다. 비트 연산의 답은 언제나 타입의 폭에 매여 있다.
• shl·shr 은 옮기기, rotl·rotr 은 돌리기다. spin 129 1 이 3 인 것은 맨 앞의 1 이 맨 뒤로 돌아 들어왔기 때문이고, shl 이었다면 그 1 은 버려진다.
• shr 은 부호에 따라 뜻이 다르다. −8 과 4294967288 은 32 비트에서 같은 비트열이지만, 부호 있는 쪽은 부호 비트가 들어와 −4 가 되고 부호 없는 쪽은 0 이 들어와 2147483644 가 된다.
• count_ones·leading_zeros·trailing_zeros 는 비트를 세고, byte_swap 은 바이트 차례를 뒤집는다.
• clmul_lo·clmul_hi 는 캐리 없는 곱셈이다 — 자리 올림 대신 배타합으로 더하는 곱셈이고, 암호와 검사합(GF(2^128)·CRC)이 이것 위에 선다. 답이 128 비트라 낱말 둘로 나온다. 기계에 그 명령이 있으면 처리기가 그것으로 내리고(lowentc --hw pclmul 또는 auto), 없으면 같은 답을 내는 셈으로 내린다 — 뜻은 하나이고 빠르기만 다르다.

옮기는 칸 수가 타입의 폭 이상이면 멈춘다. C 에서는 미정의 동작인 자리다. 칸 수를 폭 안으로 감싸기를 원하면 wrap_shl·wrap_shr 을 쓴다.

4.7 부동소수#

f32 와 f64 는 IEEE 754 의 이진 32·64 비트 형식이다. 연산은 피연산자의 폭에서 일어나고, 정수와 부동소수는 서로 자동으로 바뀌지 않는다.

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

VM 은 부동소수 결과를 짧게 보여 준다(0.333333). 부동소수를 0 으로 나누면 멈추지 않고 IEEE 754 가 정한 대로 무한이 된다. sqrt·sin·exp 같은 초월 함수는 부동소수 전용이고 운영체제가 있는 기계에서만 쓸 수 있다. 이 함수들의 마지막 비트가 어떤 값인지는 기계와 셈 라이브러리가 정한다.

f32 와 크기 타입도 같은 규칙을 따른다.

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

rem usize · isize — 기계의 주소 폭(64 비트 기계에서 64 비트). 길이와 색인을 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 — 32 비트 부동소수. 메모리가 절반이고 정밀도는 약 일곱 자리
fn third32 input x f32 . output f32 . do
  return div x 3.0 .
end

rem 같은 1/3 도 f32 와 f64 는 다른 수다 — 넓혀서 비교하면 거짓
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·isize 는 기계의 주소 폭을 가진 부호 없는·있는 정수다. C 의 size_t·ptrdiff_t 와 길이·색인을 주고받을 때 쓴다(29장). 폭이 기계마다 달라질 수 있으므로, 폭이 정해진 계산에는 u64·i64 를 쓴다. cast isize n 처럼 부호가 다른 타입으로는 이름 붙은 연산으로 옮긴다.
• f32 는 메모리가 절반이고 유효 숫자가 약 일곱 자리다. 큰 배열이나 그래픽처럼 정밀도보다 양이 중요한 곳에 쓴다.
• same_third 는 같은 1/3 을 f32 와 f64 로 셈해 넓힌 뒤 비교한다. 거짓(0)이다. VM 이 둘 다 0.333333 으로 짧게 보여 주어도 둘은 다른 수다.

4.8 흔한 실수#

수의 실수는 번역을 통과하고 실행 중에 드러나는 것이 많다. 다른 언어라면 조용히 틀린 값이 나올 자리에서 Lowent 는 멈춘다. 멈춘 자리가 곧 고칠 자리다.

module mistake_midpoint .
rem trap: mid 200 100

fn mid input a u8 . input b u8 . output u8 .
do
  rem ✘ 둘을 먼저 더하면 300 이 되어 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 한 폭 넓혀서 더한다 --- u16 은 510 까지 담는다
  let both u16 be add (widen u16 a) (widen u16 b) .
  rem 둘로 나눈 값은 다시 u8 에 들어간다는 것을 우리는 알고, narrow 가 그것을 확인한다
  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 ✘ 부호 없는 수는 0 아래로 내려가지 않는다 --- 3 − 5 는 음수가 아니라 멈춤이다
  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 ✘ u8 반복 변수는 255 다음이 없다 --- 256 번째 `add i 1` 에서 멈춘다
  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 ✘ f64 를 정수 리터럴 2 로 나눴다 --- 부동소수 자리에는 2.0 을 쓴다
  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 ✘ u64 의 위쪽 절반을 `--run` 인자로 주면 경계에서 거절된다 — 구간 분석이 u64 의 상한을 i64 최댓값으로 믿기 때문이다
fn echo input n u64 . output u64 .
do
  return n .
end

rem 경계값은 시험 안에서 리터럴로 적는다
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 ✘ 리터럴을 그대로 담은 f32 — 이 판에서는 32 비트로 반올림되지 않아 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 셈을 한 번 거친 f32(0.1 + 0)는 32 비트로 반올림되어 다르다고 나온다
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 정수 나눗셈은 소수점 아래를 버린다 --- 7 / 2 는 3
  return div (add a b) 2 .
end

fn avg_f input a f64 . input b f64 . output f64 .
do
  rem 소수점 아래가 필요하면 처음부터 부동소수로 계산한다
  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

부동소수의 나머지는 정수의 mod 와 이름을 갈라 fmod 로 적는다.

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

rem 부동소수의 나머지는 `fmod` --- 정수의 `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 은 1.5, mod 7 2 는 1 이다. 한 이름에 두 갈래를 싣지 않는 것은 div 와 같은 까닭이다 — 무엇을 셈하는지가 이름에서 보인다.

4.9 이 장의 문법 한눈에#