Introduction

This book teaches the RCE programming language from the beginning. It assumes you can use a terminal and have written a little code in some language. It does not assume you know any particular one.

What RCE is

RCE is a small language for programs whose meaning is fixed by a written specification. A program is a text. Its meaning is a Form: a state machine made of states, events, a step function that takes a state and an event to a new state and some outputs, and a log of the events that happened.

RCE at a glance: the checker accepts a program or names the rule it breaks; an accepted program is a Form; every step goes into the log; emitters project it to other languages; a host runs it. More figures: openIE-dev/rce docs/figures.

Three ideas run through the whole book:

1. The same program gives the same answer everywhere. Arithmetic, text and floating point have one defined meaning. There is no undefined behaviour, so a result does not depend on the machine.
2. Every program finishes. Loops have a limit, recursion has to make the input smaller, and iterators are counted. A step can never run forever.
3. Mistakes are refused before the program runs. The checker refuses a program that could use memory after giving it away, that forgets a case, or whose own tests do not hold. Each refusal names the rule it broke.

Status

The specification is at draft 0.7. That draft is published for review and can still change. This book teaches language version 0.5, the language of sections 2 to 10; a module opts into version 0.6 (Appendix C of the specification) with the first-line comment # rce-version: 0.6, or into version 0.7 (C.15) with # rce-version: 0.7. What exists today:

• the specification, with its grammar checked by machine;
• a reference checker and interpreter, rce, which this book uses for every example;
• emitters that translate a checked program to Rust, Python or JavaScript.

What does not exist yet: a production compiler and a fast runtime. The reference interpreter defines what programs mean. It is not built for speed.

How the examples are checked

Every program in this book is a file in the listings/ directory of the book's repository. The chapters include those files directly, so what you read is what was checked. The script scripts/check-listings.sh runs the real rce command over all of them:

• a program shown as working must pass rce test;
• a program shown as refused must be refused, with the rule the text names;
• a terminal transcript must match what rce prints today.

If you find a place where the book and the checker disagree, that is a bug in one of them. Please open an issue.

Conventions

Program text looks like this:

fn half(x: u64) -> u64 = x / 2

A line that starts with $ is a command you type. The lines below it are what rce printed. The book also shows the exit status, because rce uses it to say whether something was refused: 0 means success, 1 means refused or failed, 2 means the command itself was used wrongly.

Getting started

To try RCE without installing anything, open the RCE playground: it runs the reference checker in your browser and shows whether a program is accepted and the trace of each example. To run programs with rce run, install rce.

Install rce

rce is built from source with Rust. The repository pins the Rust version in rust-toolchain.toml, and rustup installs that version for you.

git clone https://github.com/openIE-dev/rce
cd rce/spec/checker
cargo build --release

The program is now at target/release/rce. Put it on your PATH, for example:

install -m 755 target/release/rce ~/.local/bin/

Prebuilt binaries of rce (together with the desktop IDE) for Linux, macOS and Windows are on the rce-ide releases page; unpack one and put rce on your PATH instead of building.

Check that it runs. rce --version names the specification draft it implements, and with no arguments rce prints the list of commands:

rce --version
rce

Hello, world

Make a file called hello.rce:

fn main()
    emit "hello, world"

fn main() declares a function called main with no parameters. The body is the indented line under it. RCE uses indentation for blocks, as Python does. Indent with spaces; a tab is refused.

emit produces an output value. A program does not print directly. It emits values, and the tool running it decides how to show them.

Run it:

$ rce run hello.rce
emit "hello, world"
exit status: 0

rce run evaluated main and showed each emitted value.

Checking without running

$ rce check hello.rce
ok hello.rce
exit status: 0

rce check reads the file, checks types and the other rules, and evaluates every test the file contains. It never runs main. You will use rce check and rce test far more often than rce run.

Comments

A comment starts with # and runs to the end of the line.

# This line is a comment.
fn main()
    emit 1   # so is the end of this one

What you learned

• rce run FILE runs fn main() and shows what it emits.
• rce check FILE checks a program without running it.
• Blocks are marked by indentation with spaces.

Values, types and functions

Constants, functions and checks

# Constants, functions and checks.
const SECONDS_PER_MINUTE: i64 = 60

fn to_seconds(minutes: i64) -> i64 = minutes * SECONDS_PER_MINUTE

fn area(width: i64, height: i64) -> i64
    let a = width * height
    return a

check to_seconds(3) == 180
check area(4, 5) == 20

• const names a value that never changes. Its type is written after :.
• fn to_seconds(minutes: i64) -> i64 = ... is a function with one parameter of type i64 (a 64-bit signed integer) that returns an i64. When the body is a single expression, write it after =.
• A longer body goes in an indented block. let names a value inside the block. return gives the result.
• check is a test. The checker evaluates it while checking the program, and the program is accepted only if every check is true.

Names at the top level of a file can be used before they are declared, so the order of declarations does not matter.

Integer types

RCE has the integer types i8, i16, i32, i64 (signed), u8, u16, u32, u64 (unsigned) and usize (used for lengths and positions). Each one stands for exactly the whole numbers in its range: a u8 is a number from 0 to 255.

# Every integer type has a fixed range. Mixing types needs an explicit `as`.
fn small_sum(a: u8, b: u8) -> u8 = a + b

fn widen(a: u8, b: i64) -> i64 = (a as i64) + b

check small_sum(100, 27) == 127
check widen(200, 1000) == 1200
check (250 as u8).wrapping_add(10) == 4
check (250 as u8).saturating_add(10) == 255
check (250 as u8).checked_add(10).isnone()

A number written in the program is an i64 unless the place it is used needs a different integer type. In small_sum(100, 27) the parameters are u8, so 100 and 27 are u8.

Different integer types never mix silently. To add a u8 to an i64, turn it into an i64 with as first, as widen does.

When a result does not fit

What is 200 + 100 as a u8? The true answer, 300, is not a u8. Many languages quietly wrap it around to 44. RCE does not guess. The addition traps: it stops with an error. Because the check below needs that addition, the program is refused:

fn small_sum(a: u8, b: u8) -> u8 = a + b

check small_sum(200, 100) == 44

rce check says:

$ rce check overflow.rce
REFUSED overflow.rce: line 3: W-INT-1 check: trap: overflow: 300 is outside u8
exit status: 1

W-INT-1 is the name of the rule in the specification: every check and example must hold. When you want wrapping or clamping, ask for it by name, as sizes.rce does: wrapping_add wraps around, saturating_add stops at the largest value, and checked_add gives an option that is empty when the result does not fit. (Options come back in chapter 7.)

Mixing types without as is refused too, by the type rule W-TY-1:

fn add(a: u8, b: i64) -> i64 = a + b

$ rce check mixed_types.rce
REFUSED mixed_types.rce: line 1: W-TY-1 `+` on u8 and i64: no implicit conversion; line 1: W-TY-1 expected i64, found u8
exit status: 1

Other basic types

• bool: true and false, combined with and, or, not.
• f64 and f32: floating-point numbers. A literal such as 2.5 is an f64. The specification fixes how every operation rounds, so the same float code gives the same bits on every target.
• text: a string of Unicode text, such as "hello". Chapter 8 covers it.
• (): the unit type, the result of a function that returns nothing.

What you learned

• Functions, constants and check tests.
• Integer types have exact ranges, and going outside a range traps.
• Conversions between types are always written with as.

Choices and loops

if, elif and else

fn grade(score: u32) -> text
    if score >= 90
        return "A"
    elif score >= 80
        return "B"
    elif score >= 70
        return "C"
    else
        return "F"

fn sign(x: i64) -> i64 = if x < 0 then -1 else 1

check grade(95) == "A"
check grade(71) == "C"
check grade(3) == "F"
check sign(-7) == -1

if as a statement takes a block under each branch. There is also an if expression, written on one line with then and else, as in sign. The expression form must always have an else, because it has to produce a value either way.

Comparisons cannot be chained: 0 < x < 10 is refused by the grammar. Write x in 0..10 instead.

Three loops, each with a limit

# Three kinds of loop. Each one has a limit on how often it can repeat.
fn sum_to(n: u64) -> u64
    var total: u64 = 0
    for i in 0..=n
        total += i
    return total

fn fib(n: u32) -> u64
    var a: u64 = 0
    var b: u64 = 1
    for _ in 0..n
        let t = a + b
        a = b
        b = t
    return a

fn collatz_steps(n: u64) -> u64
    var x = n
    var k: u64 = 0
    while x != 1 bound 10_000
        x = if x % 2 == 0 then x / 2 else 3 * x + 1
        k += 1
    return k

fn first_square_over(limit: u64) -> u64
    var i: u64 = 0
    loop bound 1_000
        if i * i > limit
            break
        i += 1
    return i * i

check sum_to(10) == 55
check fib(10) == 55
check collatz_steps(6) == 8
check first_square_over(50) == 64

• for i in 0..=n runs over a range. 0..n excludes n; 0..=n includes it. A for loop can also run over a list, a map or a text.
• while condition bound 10_000 repeats while the condition is true, at most 10,000 times. Underscores in numbers are only for reading.
• loop bound 1_000 repeats until break, at most 1,000 times.

Why a limit? Because RCE promises that every program finishes. A for loop always has a known length. A while or loop without bound gets the default limit of 1,000,000 repetitions. A program can change that default with const LOOP_LIMIT: u64 = ....

Reaching the limit is not a hang. It is a trap with the message loop bound:

fn spin() -> u64
    var k: u64 = 0
    while true bound 10
        k += 1
    return k

check spin() == 10

$ rce check spin.rce
REFUSED spin.rce: line 7: W-INT-1 check: trap: loop bound
exit status: 1

The loop condition is always true, so the eleventh repetition traps, the check cannot be evaluated, and the program is refused.

var and assignment

let names a value that does not change. var names one that does. You change it with = or with a compound operator such as +=, -=, *=. Assignment is a statement, never an expression, so if (x = 1) is a syntax error.

What you learned

• if statements, if ... then ... else ... expressions, ranges with in.
• for, while ... bound and loop bound, and why each one is limited.
• let for fixed names, var for names that change.

Checks and examples

Tests in RCE are part of the program, not a separate file. A program whose tests fail is not accepted at all.

check

You have already seen check: a bool expression that must be true. The checker evaluates every check while it checks the program.

intent and example

An intent says in words what a piece of code is for, and holds the tests that pin it down:

intent "a counter that never goes below zero"
    example Inc, Inc, Dec -> 1
    example Dec -> refused: Underflow

state Counter
    n: u64 = 0

event Inc
event Dec

error Underflow

step Counter on Inc -> n + 1
step Counter on Dec -> try n.checked_sub(1) else Underflow

The parts after the intent (state, event, step) are the subject of the next chapter. For now, read the two examples:

• example Inc, Inc, Dec -> 1 means: start from the initial state, apply the events Inc, Inc, Dec, and the counter must then be 1.
• example Dec -> refused: Underflow means: applying Dec to a fresh counter must be refused with the error Underflow.

rce test reports how many examples and checks each file has:

$ rce test counter.rce
ok counter.rce (2 examples, 0 checks)
1 passed, 0 failed
exit status: 0

A failing example is a refused program

Change the expected value and the program is refused:

intent "a counter"
    example Inc, Inc -> 3

state Counter
    n: u64 = 0

event Inc

step Counter on Inc -> n + 1

$ rce check wrong_example.rce
REFUSED wrong_example.rce: line 2: W-INT-1 example does not hold: final value is 2, expected 3
exit status: 1

This is the admission rule W-INT-1: every check and every example must hold for the program to be admitted. rce test and rce check give the same verdict; rce test also counts the cases.

What an example compares

When the program has one state with one field, the value after -> is compared with that field. Otherwise the part after -> must be a bool expression over the final state, such as light == Yellow or items == ["jam"] and adds == 2. Chapter 10 has an example of the second kind.

What you learned

• check and example are tests that live in the program.
• A program whose tests fail is refused (rule W-INT-1).
• rce test runs the same checks as rce check and counts them.

State, events and steps

This chapter is the centre of the language. Most RCE programs are built from four kinds of declaration:

• a state holds data that lasts between events;
• an event is something that happens, with an optional payload;
• a step says how a state changes when an event arrives;
• an error is a reason to refuse an event.

A door

intent "a door that can be locked only when it is closed"
    "the door starts closed and unlocked"
    example Open, Close, Lock -> locked
    example Open, Lock -> refused: DoorOpen

state Door
    open: bool = false
    locked: bool = false

event Open
event Close
event Lock
event Unlock

error DoorOpen
error Locked

step Door on Open if locked
    fail Locked
step Door on Open
    open = true
step Door on Close
    open = false
step Door on Lock if open
    fail DoorOpen
step Door on Lock
    locked = true
step Door on Unlock
    locked = false

• state Door has two fields, each with a starting value.
• Four events have no payload.
• step Door on Open if locked is a step with a guard. When Open arrives and locked is true, this step runs and fail Locked refuses the event.
• When the guard is false, the next step for Open in the file is used, and it sets open = true.

For each event, the checker picks the first step, in source order, whose event matches and whose guard is true. If no step matches, the state stays as it was.

Every declared event must have at least one step. Otherwise the step function would have no answer for that event, and the program is refused:

state Counter
    n: u64 = 0

event Inc
event Dec

step Counter on Inc -> n + 1

$ rce check unhandled_event.rce
REFUSED unhandled_event.rce: line 5: W-STEP-2 event `Dec` is handled by no step or actor: δ would not be total
exit status: 1

Inside a step, the state's fields are variables you can read and change. The changes become the new state only if the step finishes without being refused.

Running events

rce run FILE EVENTS applies events one by one and prints the state after each:

$ rce run door.rce "Open, Close, Lock, Unlock, Open"
0 (initial) Door { open = false, locked = false }
1 Open Door { open = true, locked = false }
2 Close Door { open = false, locked = false }
3 Lock Door { open = false, locked = true }
4 Unlock Door { open = false, locked = false }
5 Open Door { open = true, locked = false }
exit status: 0

A refused event leaves the state unchanged, and nothing after it is applied:

$ rce run door.rce "Lock, Open, Close"
0 (initial) Door { open = false, locked = false }
1 Lock Door { open = false, locked = true }
2 Open refused: Locked
exit status: 1

The exit status is 1 because an event was refused.

The counter again

In the counter from chapter 4, both steps use the short arrow form:

step Counter on Inc -> n + 1

When a state has exactly one field, -> expression sets that field to the value of the expression. try n.checked_sub(1) else Underflow subtracts one if the result fits in a u64, and otherwise refuses the event with Underflow.

$ rce run counter.rce "Inc, Inc, Dec, Dec, Dec"
0 (initial) Counter { n = 0 }
1 Inc Counter { n = 1 }
2 Inc Counter { n = 2 }
3 Dec Counter { n = 1 }
4 Dec Counter { n = 0 }
5 Dec refused: Underflow
exit status: 1

Why build programs this way

A state, a set of events and a step function together form a state machine, which the specification calls the program's Form. Because the step function is a plain function of the old state and the event, a list of events always leads to the same states. You can replay the list and get exactly the same run. Chapter 15 shows the Form itself.

The states, events and steps of this chapter are the S, E and δ of the Form; the log of events is D. More figures: openIE-dev/rce docs/figures.

What you learned

• state, event, step and error, and how a step is chosen.
• Guards with if on a step.
• rce run FILE "Event, Event" to watch a state change.

Errors and refusals

RCE has no exceptions. A step either finishes or is refused, and a function either returns a value or fails with a declared error.

Refusing an event

intent "a bank account that refuses overdrafts"
    example Deposit(amount: 50), Withdraw(amount: 20) -> 30
    example Withdraw(amount: 1) -> refused: Insufficient

state Account
    balance: i64 = 0

event Deposit(amount: i64)
event Withdraw(amount: i64)

error Insufficient(need: i64)
error NotPositive

struct Withdrawn
    amount: i64

step Account on Deposit(amount: a)
    if a <= 0
        fail NotPositive
    balance += a
step Account on Withdraw(amount: a)
    if a > balance
        fail Insufficient(need: a - balance)
    balance -= a
    emit Withdrawn(amount: a)

• error Insufficient(need: i64) declares an error with a payload.
• fail Insufficient(need: a - balance) refuses the event with that error.
• emit Withdrawn(amount: a) produces an output value as part of the step.
• event Deposit(amount: i64) has a payload, and the step's pattern Deposit(amount: a) names it a.

$ rce run account.rce "Deposit(amount: 50), Withdraw(amount: 20), Withdraw(amount: 40)"
0 (initial) Account { balance = 0 }
1 Deposit(amount: 50) Account { balance = 50 }
2 Withdraw(amount: 20) Account { balance = 30 }
  emit Withdrawn(amount: 20)
3 Withdraw(amount: 40) refused: Insufficient
exit status: 1

The third event asks for more than the balance, so it is refused and the balance stays at 30.

Functions that can fail

A function that can fail says so in its return type. u8 ! NotADigit means "a u8, or the error NotADigit".

error NotADigit(at: u32)

fn digit(c: text, at: u32) -> u8 ! NotADigit
    if c.isdigit()
        return c.toint() as u8
    fail NotADigit(at: at)

fn sum_digits(s: text) -> u32 ! NotADigit
    var total: u32 = 0
    var i: u32 = 0
    for c in s.chars()
        total += (try digit(c, i)) as u32
        i += 1
    return total

fn sum_or_zero(s: text) -> u32 = sum_digits(s) catch 0

fn where_it_broke(s: text) -> u32 = sum_digits(s) catch |e| e.at

check sum_or_zero("123") == 6
check sum_or_zero("1x3") == 0
check where_it_broke("12x") == 2

• fail NotADigit(at: at) returns the error from the function.
• try digit(c, i) uses the value if there is one, and otherwise passes the error on to the caller. That is why sum_digits also has ! NotADigit in its type.
• sum_digits(s) catch 0 turns an error into a default value.
• catch |e| e.at gives the error a name so you can use its payload.

A value of type u32 ! NotADigit is not a u32. The checker refuses code that uses it as one until the error is handled with try or catch, so an error cannot be ignored by accident. A step whose code fails with an error refuses the event.

Traps

A trap is a failure that is not a declared error: an integer that does not fit, a division by zero, a loop that reaches its limit. A trap inside a step refuses the event, exactly like fail. A trap in a check or an example makes the program inadmissible, as you saw in chapters 2 and 3.

What you learned

• error, fail and refused events.
• Error unions T ! E, with try, catch and catch |e|.
• Traps refuse an event in the same way an error does.

Structs, kinds and matching

Kinds

A kind is a type whose value is one of several variants. Each variant can carry its own fields.

kind Shape
    Circle(r: f64)
    Rect(w: f64, h: f64)
    Empty

fn area(s: &Shape) -> f64
    match s
        Circle(r: r) -> 3.0 * r * r
        Rect(w: w, h: h) -> w * h
        Empty -> 0.0

struct Point
    x: i64
    y: i64

impl Point
    fn origin() -> Point = Point(x: 0, y: 0)
    fn moved(self, dx: i64) -> Point = Point(x: self.x + dx, y: self.y)

fn first_even(xs: &[i64]) -> i64?
    for x in xs
        if x % 2 == 0
            return some(x)
    return none

fn or_zero(v: i64?) -> i64
    match v
        some(x) -> x
        none -> 0

const NUMS: List[i64] = [3, 5, 8, 9]
const BOX: Shape = Rect(w: 2.0, h: 3.0)
const NOTHING: Shape = Empty

check area(&BOX) == 6.0
check area(&NOTHING) == 0.0
check Point.origin().moved(4).x == 4
check or_zero(first_even(&NUMS)) == 8

match looks at a value and runs the arm whose pattern fits. Circle(r: r) matches a circle and names its radius r.

The checker requires a match to cover every variant. Forgetting one is refused, so adding a variant later shows you every place that must handle it:

kind Light
    Red
    Green
    Yellow

fn next(l: Light) -> Light
    match l
        Red -> return Green
        Green -> return Yellow

$ rce check missing_case.rce
REFUSED missing_case.rce: line 7: W-MATCH-1 match is not exhaustive: missing Yellow
exit status: 1

A _ pattern matches anything and can serve as the last arm.

Structs and impl

A struct groups named fields. Point(x: 0, y: 0) builds one; fields are always passed by name. impl Point adds functions that belong to the type. Point.origin() calls one that takes no self; p.moved(4) calls one that does.

Options

i64? is an option: either some(value) or none. RCE has no null, so an empty result is always visible in the type. first_even returns none when it finds no even number, and or_zero uses match to handle both cases.

Borrowed arguments

area(s: &Shape) takes a borrow of a shape: it can read the shape but does not take it over. You pass a borrow with &, as in area(&BOX). Borrows are what chapter 9 is about. One rule shows up already: you can only borrow a place, such as a variable or a constant, not a value that was just built. That is why the checks use the named constants BOX and NOTHING.

What you learned

• kind with variants, struct with fields, impl for functions on a type.
• match must cover every case (rule W-MATCH-1).
• T? options with some and none instead of null.

Lists, maps and text

Lists and maps

fn squares(xs: &[i64]) -> List[i64] = xs.map(fn(x: i64) => x * x)

fn evens(xs: &[i64]) -> List[i64] = [x for x in xs if x % 2 == 0]

fn total(xs: &[i64]) -> i64 = xs.fold(0, fn(acc: i64, x: i64) => acc + x)

fn count_words(words: &[text]) -> Map[text, u32]
    var m: Map[text, u32] = {}
    for w in words
        m[w] = (m.get(w) catch 0) + 1
    return m

const XS: List[i64] = [1, 2, 3, 4]
const WORDS: List[text] = ["a", "b", "a"]

check squares(&XS) == [1, 4, 9, 16]
check evens(&XS) == [2, 4]
check total(&XS) == 10
check count_words(&WORDS)["a"] == 2
check (count_words(&WORDS).get("z") catch 0) == 0

• List[i64] is a list of i64. [1, 2, 3, 4] is a list literal.
• &[i64] is a borrowed slice: a view of a list or array that the function reads but does not own.
• xs.map(fn(x: i64) => x * x) applies a function to every element. fn(x: i64) => ... is a function written inline.
• [x for x in xs if x % 2 == 0] builds a new list from the old one.
• fold combines the elements into one value, starting from 0.
• Map[text, u32] maps text keys to u32 values. m.get(w) fails when the key is missing, and catch 0 supplies a default.

Text

fn shout(s: &text) -> text = s.strip().upper() + "!"

fn is_palindrome(s: &text) -> bool
    let t = [c for c in s.lower().chars() if c.isalpha()]
    return t == t.reverse()

const GREETING: text = "  hi "
const PHRASE: text = "Never odd or even"

check shout(&GREETING) == "HI!"
check is_palindrome(&PHRASE)
check "héllo".len() == 6
check "héllo"[1:3] == "é"

Text is stored as UTF-8. len() counts bytes, not characters: "héllo" has five characters and six bytes, because é takes two bytes. s[1:3] takes the bytes from position 1 up to 3, which here is exactly the é. Slicing in the middle of a character traps. To go through text one character at a time, use chars() or for c in s.

What you learned

• List, Map, slices, inline functions and list comprehensions.
• Text is UTF-8, measured and indexed in bytes.

Ownership and borrowing

RCE has no manual free, and a value cannot be used after it is released. Two ideas, also found in Rust, make this work: every value has one owner, and other code can borrow a value for a short time. A value is released when the block that owns it ends. RCE's borrows are more restricted than Rust's, which makes them simpler to check.

Moving

Small fixed-size values such as integers, bool and f64 are copied when you pass them. Values that own memory, such as text, List and Map, are moved: passing one to a function hands it over, and the old name can no longer be used.

fn take(s: text) -> u64 = s.len() as u64

fn twice(s: text) -> u64
    let a = take(s)
    return a + take(s)

$ rce check use_after_move.rce
REFUSED use_after_move.rce: line 5: W-OWN-1 `s` is used after it was moved
exit status: 1

The first call to take moved s, so the second call is refused. If you really need two independent values, copy(s) makes a full copy.

Borrowing

fn length(s: &text) -> u64 = s.len() as u64

fn push_all(dst: &mut List[i64], src: &[i64])
    for x in src
        dst.append(x)

fn demo() -> u64
    let name = "Ada"
    let n = length(&name)
    let again = length(&name)
    var a: List[i64] = [1, 2, 3]
    let b: List[i64] = [4, 5]
    push_all(&mut a, &b)
    let c = copy(a)
    return n + again + (c.len() as u64) + (a.len() as u64)

check demo() == 16

• &name lends name for reading. The owner keeps it, so length can be called twice.
• &mut a lends a for changing. push_all appends to the caller's list.
• copy(a) makes a separate list.

The one rule about borrows

While something is borrowed for changing, nothing else may look at it in the same call:

fn both(a: &mut List[i64], b: &List[i64])
    pass

fn bad()
    var xs: List[i64] = [1]
    both(&mut xs, &xs)

$ rce check mut_alias.rce
REFUSED mut_alias.rce: line 6: W-OWN-2 `xs` is borrowed mutably and again in one call
exit status: 1

Why RCE borrows need no lifetimes

In RCE a borrow lives only as long as the call or statement that made it. A borrow cannot be stored in a field, a list, an event or a state, and in general cannot be returned. (A function may return a borrow of one of its own parameters, such as a slice of a list it was given.) Because borrows never outlive the statement that created them, the checker does not need lifetime annotations, and the check is a local pass through each function.

The specification calls these second-class borrows, a design also used by Swift's inout parameters and by the Hylo language.

What you learned

• Copy types are copied; owning types are moved, and a moved name is dead.
• &x lends for reading, &mut x for writing, copy(x) duplicates.
• A mutable borrow excludes every other use for its duration.

Several regions and guards

A program can declare more than one state. The specification calls each one a region. One event can update several regions at once.

intent "a cart and its statistics, updated by the same events"
    example AddItem(name: "tea"), AddItem(name: "jam"), RemoveItem(name: "tea") -> items == ["jam"] and adds == 2
    example AddItem(name: "a"), AddItem(name: "b"), AddItem(name: "c"), AddItem(name: "d") -> refused: CartFull

state Cart
    items: List[text] = []

state Stats
    adds: u64 = 0
    removes: u64 = 0

event AddItem(name: text)
event RemoveItem(name: text)

error CartFull

step Cart on AddItem(name: _) if items.len() >= 3
    fail CartFull
step Cart on AddItem(name: n) -> items.with(n)
step Stats on AddItem(name: _)
    adds += 1
step Cart on RemoveItem(name: n)
    items = [copy(i) for i in items if i != n]
step Stats on RemoveItem(name: _)
    removes += 1

AddItem has steps in both Cart and Stats. When it arrives, the step of each region runs. Each step sees the state as it was before the event, so the order in which regions are listed does not change the result.

All or nothing

The cart holds at most three items. The guarded step refuses a fourth:

$ rce run cart.rce "AddItem(name: \"a\"), AddItem(name: \"b\"), AddItem(name: \"c\"), AddItem(name: \"d\")"
0 (initial) Cart { items = [] }; Stats { adds = 0, removes = 0 }
1 AddItem(name: "a") Cart { items = ["a"] }; Stats { adds = 1, removes = 0 }
2 AddItem(name: "b") Cart { items = ["a", "b"] }; Stats { adds = 2, removes = 0 }
3 AddItem(name: "c") Cart { items = ["a", "b", "c"] }; Stats { adds = 3, removes = 0 }
4 AddItem(name: "d") refused: CartFull
exit status: 1

Look at the last line. Stats would have counted the fourth add, but because Cart refused the event, neither region changed. An event applies to every region or to none. This is what makes a refused event safe to ignore: nothing half-happened.

Examples over several fields

With more than one field in the program, an example's expected outcome is a condition on the final state, such as items == ["jam"] and adds == 2 in the intent above.

What you learned

• Several state regions can react to the same event.
• Every step reads the state from before the event.
• An event is applied to all regions or refused for all of them.

Traits and generics

trait Describe
    fn describe(&self) -> text

struct Point
    x: i64
    y: i64

impl Describe for Point
    fn describe(&self) -> text = "(" + self.x.tostr() + ", " + self.y.tostr() + ")"

impl forall[T: Describe] Describe for List[T]
    fn describe(&self) -> text = ", ".join([x.describe() for x in self])

fn largest[T: Ord](xs: &[T]) -> T?
    var best: T? = none
    for x in xs
        match best
            none -> best = some(copy(x))
            some(b) if x > b -> best = some(copy(x))
            _ -> pass
    return best

const PTS: List[Point] = [Point(x: 1, y: 2), Point(x: 3, y: 4)]
const NUMS: List[i64] = [4, 9, 2]

check Point(x: 1, y: 2).describe() == "(1, 2)"
check PTS.describe() == "(1, 2), (3, 4)"
check largest(&NUMS) == some(9)

Traits

A trait lists functions that a type promises to have. impl Describe for Point keeps that promise for Point.

impl forall[T: Describe] Describe for List[T] says: for every type T that implements Describe, a list of T implements it too. The word forall is needed so the grammar can tell the parameter list apart from a slice type [T].

Generic functions

largest[T: Ord](xs: &[T]) -> T? works for any type T that can be ordered. Ord is a bound: the checker refuses a call with a type that cannot be compared. Inside, copy(x) is needed because best keeps its own value while xs is only borrowed.

The arm some(b) if x > b -> ... shows a guard on a match arm, the same idea as a guard on a step.

What you learned

• trait and impl ... for ....
• Generic functions and impls with bounds such as T: Ord.

Modules

Each source file is a module. A larger program is several files checked together.

module shop.pricing

pub fn discount(total: i64, percent: i64) -> i64 = total - total * percent / 100

fn round_down(x: i64) -> i64 = x - x % 10

module shop.orders
use shop.pricing

pub struct Order
    id: u64
    total: i64 = 0

pub fn new_order(id: u64) -> Order = Order(id: id)

check new_order(7).total == 0

• module shop.pricing gives the module its name. Without it, the name comes from the file path.
• use shop.pricing makes that module visible.
• pub marks an item other modules may use. Everything else stays private to its module.

Give all the files of a program to rce in one command:

$ rce check shop/pricing.rce shop/orders.rce
ok shop/pricing.rce
ok shop/orders.rce
exit status: 0

Checked alone, orders.rce is refused, because the module it uses is not part of the program:

$ rce check shop/orders.rce
REFUSED shop/orders.rce: line 2: W-NAME-1 unknown module `shop.pricing`
exit status: 1

Calling into another module

A used module is visible by its last name, so shop.checkout calls pricing.discount(...):

module shop.checkout
use shop.pricing

pub fn sale_price(total: i64) -> i64 = pricing.discount(total, 10)

check sale_price(200) == 180

$ rce test shop/pricing.rce shop/checkout.rce
ok shop/pricing.rce (0 examples, 0 checks)
ok shop/checkout.rce (0 examples, 1 checks)
2 passed, 0 failed
exit status: 0

Only pub items can be reached this way. round_down in shop.pricing has no pub, so a call to it from another module is refused:

module shop.rounding
use shop.pricing

fn rounded(total: i64) -> i64 = pricing.round_down(total)

$ rce check ../shop/pricing.rce private_call.rce
ok ../shop/pricing.rce
REFUSED private_call.rce: line 4: W-VIS-1 `round_down` is private to module `shop.pricing`
exit status: 1

The modules std.text, std.collections and std.math are built in and can always be used.

What you learned

• module, use and pub.
• All files of a program are checked together.
• A used module is reached by its last name, and only its pub items are visible.

Recursion and iterators

Structural recursion

A function may call itself only on a part of a value it received:

# Structural recursion: each call works on a smaller part of the tree.
kind Tree
    Leaf(v: i64)
    Node(l: Box[Tree], r: Box[Tree])

fn tree_sum(t: &Tree) -> i64
    match t
        Leaf(v: v) -> return v
        Node(l: l, r: r) -> return tree_sum(l) + tree_sum(r)

fn sample() -> i64
    let t = Node(l: Box(Leaf(v: 2)), r: Box(Node(l: Box(Leaf(v: 3)), r: Box(Leaf(v: 4)))))
    return tree_sum(&t)

check sample() == 9

tree_sum calls itself on l and r, which are fields of the Node it matched. Each call gets a smaller tree, so the recursion has to stop. Box[Tree] is needed because a Tree that contains a Tree directly would have no fixed size.

Recursion that does not shrink its input is refused, even when it would in fact stop:

fn countdown(n: u64) -> u64
    if n == 0
        return 0
    return countdown(n - 1)

$ rce check countdown.rce
REFUSED countdown.rce: line 4: W-REC-1 recursion through countdown has no decreasing measure (6.7): no layers of summed measures, each kept by every call not yet done and shrunk by at least one, leave the remaining calls without a cycle, and a cycle of its calls passes through no function declared with `bound`
exit status: 1

Write countdown as a loop instead. Two functions that call each other are refused for the same reason. This rule is part of how RCE keeps its promise that every step finishes.

Iterators

A function whose return type is iter T produces values one at a time with yield:

fn evens(n: u64) -> iter u64
    var i: u64 = 0
    while i < n
        yield i * 2
        i += 1

fn total(n: u64) -> u64
    var s: u64 = 0
    for x in evens(n)
        s += x
    return s

check total(4) == 12
check evens(3).collect() == [0, 2, 4]

A for loop takes the values as they are produced. collect() gathers them into a list. Each yield counts against the loop limit from chapter 3, so an iterator cannot run forever either.

What you learned

• Recursion is allowed on parts of a matched value (rule W-REC-1).
• iter T functions with yield, consumed by for or collect().

Tasks and channels

RCE programs can run several tasks that talk over channels.

fn producer(out: chan i64, n: i64)
    for i in 0..n
        out <- i
    out.close()

fn main()
    let c = chan[i64](8)
    spawn producer(c, 10)
    var total = 0
    loop
        match <- c
            some(v) -> total += v
            none -> break
    emit total

• chan[i64](8) makes a channel that holds up to 8 values of type i64.
• spawn producer(c, 10) starts producer as a new task.
• out <- i sends i on the channel. <- c receives. When the channel is closed and empty, receiving gives none.

$ rce run channels.rce
emit 45
exit status: 0

Why the result is always the same

Tasks in RCE are scheduled in ticks. In each tick, every task that can move takes one communication step, in an order fixed by the tasks' ids. The ids are computed from the program itself, not from a clock or a counter. So the whole run is a function of the program and its inputs, and running it again gives the same result. When no task can move, the run ends with the outcome Deadlock instead of hanging.

The specification also defines select (wait on several channels) and actor (a state with its own mailbox). See section 6.8 of the specification.

Current limits

The reference interpreter runs tasks and channels as shown here. The Rust, Python and JavaScript emitters of chapter 15 do not translate them yet: in emitted code, channel operations trap.

What you learned

• spawn, chan[T](n), send with <- and receive with <- c.
• Scheduling is fixed by the program, so concurrent runs repeat exactly.

The Form and the emitters

The Form

Every RCE program means a Form: its states, events, step function, and the log of events it was tested with. rce emit form prints the Form of the counter from chapter 4 as one line of JSON:

The Form and the targets rce emit writes. More figures: openIE-dev/rce docs/figures.

$ rce emit form counter.rce
{"S":{"regions":[{"name":"Counter","kind":"state","fields":[{"name":"n","type":"u64"}]}],"s0":{"Counter":{"n":0}}},"E":[{"name":"Inc","payload":[]},{"name":"Dec","payload":[]},{"name":"Tick","payload":[{"name":"n","type":"u64"}],"builtin":true}],"errors":[{"name":"Underflow","payload":[]}],"delta":[{"region":"Counter","on":"Inc","guarded":false,"line":13},{"region":"Counter","on":"Dec","guarded":false,"line":14}],"logs":[{"example_line":2,"D":[{"event":{"payload":{},"type":"Inc"},"hash":"f5b9e4f9376ffb85dcfaaf9ec0ba5e83a84e87e6d9a4920e99d3db076fa8fae6","out":[],"outcome":"applied","prev_hash":"0000000000000000000000000000000000000000000000000000000000000000","seq":0,"state":{"Counter":{"n":1}},"state_hash":"a8d94f4388d06db57160fa4235a0c303c6da53e9dd48d7ff7b4a08c5689de184"},{"event":{"payload":{},"type":"Inc"},"hash":"3306704544d8fa499ed5b03494631c69eb8deeaee185f8258dafe223b76eb0d6","out":[],"outcome":"applied","prev_hash":"f5b9e4f9376ffb85dcfaaf9ec0ba5e83a84e87e6d9a4920e99d3db076fa8fae6","seq":1,"state":{"Counter":{"n":2}},"state_hash":"51d8f1a4d82e7fea81432c901de1a0fcf16ca165c560a10ecd5c3ca48968151d"},{"event":{"payload":{},"type":"Dec"},"hash":"fe10321c292127aeb0bb33654e4363288eb3728cdfd6f64c5f66fda65462de16","out":[],"outcome":"applied","prev_hash":"3306704544d8fa499ed5b03494631c69eb8deeaee185f8258dafe223b76eb0d6","seq":2,"state":{"Counter":{"n":1}},"state_hash":"a8d94f4388d06db57160fa4235a0c303c6da53e9dd48d7ff7b4a08c5689de184"}]},{"example_line":3,"D":[{"event":{"payload":{},"type":"Dec"},"hash":"1d2a3145733c6fab0cd1082fa75881ad8ff7f6ad68bd94af05bba41951571967","out":[{"Refused":{"error":"Underflow","payload":{}}}],"outcome":{"refused":"Underflow"},"prev_hash":"0000000000000000000000000000000000000000000000000000000000000000","seq":0,"state":{"Counter":{"n":0}},"state_hash":"587ca07dfb1b97a90a7bd017048d4a78d405ffbcbffb2468cf59afa1dab428aa"}]}],"main":null,"source":"\nintent \"a counter that never goes below zero\"\n    example Inc, Inc, Dec -> 1\n    example Dec -> refused: Underflow\n\nstate Counter\n    n: u64 = 0\n\nevent Inc\n\nevent Dec\n\nerror Underflow\n\nstep Counter on Inc -> n + (1)\n\nstep Counter on Dec -> try n.checked_sub(1) else Underflow\n","terms":{"path":null,"items":[{"Intent":["a counter that never goes below zero",[{"events":[["Inc",[]],["Inc",[]],["Dec",[]]],"refused":null,"value":{"Int":[1,2]},"line":2},{"events":[["Dec",[]]],"refused":"Underflow","value":null,"line":3}],[]]},{"State":{"name":"Counter","fields":[{"name":"n","ty":{"Path":[["u64"],[]]},"init":{"Int":[0,6]},"line":6}],"line":5,"replicated":false}},{"Event":{"name":"Inc","payload":[],"line":8,"interrupt":null}},{"Event":{"name":"Dec","payload":[],"line":9,"interrupt":null}},{"Error":{"name":"Underflow","payload":[],"line":11}},{"Step":{"region":"Counter","pat":{"Path":["Inc"]},"guard":null,"body":{"Arrow":{"Bin":["+",{"Name":["n",13]},{"Int":[1,13]},13]}},"line":13,"deadline":null}},{"Step":{"region":"Counter","pat":{"Path":["Dec"]},"guard":null,"body":{"Arrow":{"Try":[{"Call":[{"Member":[{"Name":["n",14]},"checked_sub",14]},[{"label":null,"e":{"Int":[1,14]}}],14,false]},{"Name":["Underflow",14]},14]}},"line":14,"deadline":null}}],"pubs":[],"draft06":false,"v07":false,"v08":false,"v09":false}}
exit status: 0

You can see the state Counter with its starting value, the events, the error Underflow, the two steps, and a log for each example, with the state after every event. After the logs, the same line carries the program source, its parsed terms and the version flags (draft06, v07, v08), which are all false for this version 0.5 program. Each log entry also carries seq, its position, state_hash, the SHA-256 of the state after the event, prev_hash, the hash of the entry before it (64 zeros for the first), and hash, which covers the other four. The entries form a chain: changing any past entry changes every later hash. The JSON is ordered in a fixed way, so the same program always gives the same bytes. The event Tick marked builtin is part of every Form: it is the program's logical clock. No RCE construct reads a wall clock.

Emitting Rust, Python and JavaScript

rce emit rust, rce emit python and rce emit js translate a checked program into one self-contained file. Running that file prints the program's observations: the result of each check, and the state after each event of each example.

Test and differential results for the emitters and the IDE, October 2026. More figures: openIE-dev/rce docs/figures.

$ rce emit python counter.rce | python3 -
example 2
0 (initial) Counter { n = 0 }
1 Inc Counter { n = 1 }
2 Inc Counter { n = 2 }
3 Dec Counter { n = 1 }
example 3
0 (initial) Counter { n = 0 }
1 Dec refused: Underflow
exit status: 0

$ rce emit js counter.rce > counter.mjs && node counter.mjs
example 2
0 (initial) Counter { n = 0 }
1 Inc Counter { n = 1 }
2 Inc Counter { n = 2 }
3 Dec Counter { n = 1 }
example 3
0 (initial) Counter { n = 0 }
1 Dec refused: Underflow
exit status: 0

The two outputs are the same line for line. The checker's own test suite holds the emitters to this: it emits every example program of the specification in all three languages, runs each one, and requires its output to equal the reference interpreter's.

What you learned

• rce emit form shows the Form behind a program.
• The emitters produce Rust, Python and JavaScript that print the same observations as the reference interpreter.

Host tools: RCEdb, media, redacted replay and chat

This chapter covers four tools of the RCE host runtime, the program that runs an RCE program against the outside world and keeps its log D of admitted events. Codes such as HC-3 (host contract rule 3), HS-9 (host storage rule 9) and T8 (theorem 8), and section numbers such as 6.7 or E.8, name rules of the RCE specification.

These commands ship in the rce binary of the host runtime. They are not yet in the public reference checker that the listings of this book are checked with, so this chapter has no checked listings.

rce db D CMD [ARGS]: RCEdb from the command line

RCEdb is the database of an RCE system: its tables, rows, edges, schemas and indexes are state of an RCE module (rcedb/rcedb.rce), and its only storage is a durable log D of the host runtime. Appendix E.8 gives the normative rules; this section describes the command. rce db is serverless and in-process: the directory D is the database, and each command opens it, admits at most one event and closes it. There is no daemon, no network listener and no query engine outside RCE.

Write commands admit one event to D and print ok seq N, where N is the sequence number of the entry they appended, or REFUSED E with the error E the module raised; a refused write changes no state (T8).

Under a schema a row is its cells in column order, separated by the horizontal tab U+0009; a row whose cells do not parse as their column types is refused with BadRow. Read commands append nothing (HS-8):

An emitted store is a projection of D and never feeds back into it: the foreign engine's durability and ordering do not reach δ. A runnable example is run.sh rcedb in the examples of the host runtime.

Media capture and playback: --media DIR

rce host run and rce host serve take --media DIR to connect the media adapters. A program requests them with three output kinds, each with one result event (HC-3):

• MediaOpen(req, source) opens a track. The source is dir:NAME, the files of DIR/capture/NAME in name order, one per frame, or pattern:N, N generated test frames (at most 100000). The result carries the track id.
• MediaRead(req, id) reads the next frame of a track. Its bytes are stored as a blob under DIR addressed by their Secure Hash Algorithm 256 (SHA-256) digest, and the result carries only the digest.
• MediaPlay(req, track, digest) plays a frame to the sink by digest; the sink refuses a frame whose stored bytes do not hash to the digest.

D therefore holds the track, the sequence number and the digest of each frame, and the Tick that read it, never the frame bytes. Replay with every adapter disconnected (HC-8) reaches the same state without capturing again. In a call, frames travel between peers through a selective forwarding unit (SFU), a relay that forwards each frame to the other subscribers of its track without reading it; chapter 17 describes it.

Redacted replay: rce host replay FILE --log D --redact F,...

rce host replay re-derives every state hash of D with every adapter disconnected and prints the final state. With --redact F,G the fields named F and G are printed as <redacted sha256:H>, where H is the first six bytes of the SHA-256 digest of the field's value in canonical form. Redaction changes only what is printed: D, the replay and every state hash are unchanged, and two replays of the same field print the same H, so a reviewer can compare runs without seeing a secret. Private keys, ratchet state and frame digests are the fields to redact. D itself still holds the secrets and stays on the device that wrote it.

The chat user interface

apps/chat.rce is a complete chat program: workspaces, channels and topic threads, direct messages and groups, reactions, presence, file shares and call rooms, as one replicated RCE state. Every change is an operation applied locally and sent to peers over remote channels (P4, the host's channel adapter, enabled with --chan HOST:PORT and --peer HOST:PORT, with Transport Layer Security (TLS) under --tls). Replicas order messages by (Lamport clock, author) and so converge. Direct messages are end-to-end encrypted (E2EE) as chapter 17 describes. apps/chat.rce is generated from apps/chat-app.rce and lib/crypto.rce by scripts/build-chat.sh.

The front end scripts/chat-ui.py runs rce host serve apps/chat.rce as a child process and holds no chat state of its own. Each command it accepts becomes an event in D, so a session replays:

It renders two queries of the program that change no state: View(conv, topic), one tab-separated line per message (view, the message key, the author, the flags new, edited, deleted and e2e, the text) ending with view-end, and Unread, one line per thread with messages from others after the read marker. Run it with python3 scripts/chat-ui.py --me ann --log /tmp/ann.log [--chan ADDR --peer ADDR ...].

Media, calls and end-to-end encryption

This appendix describes the programs and libraries that give RCE programs media, calls and end-to-end encryption (E2EE): encryption in which only the communicating peers hold the keys, so relays and storage see ciphertext only. Everything here is ordinary RCE code run on the host contract of Appendix E of the RCE specification. Nothing in it adds a primitive to that contract or changes the meaning of any program. The rules it relies on are HC-3 (one result event per output request), HC-7a (fuel per input), HC-8 (replay with adapters disconnected) and HC-10 (every input is an event in the log D).

Principles

• Randomness is an input. No library here draws random bytes. Every private key, ephemeral key and seed comes from a logged Random result (HC-10), so a session replays bit for bit and a test can fix every byte.
• One public-key operation per input. A step that runs X25519 (the Diffie-Hellman function on Curve25519 of RFC 7748, a Request for Comments of the Internet Engineering Task Force) or a post-quantum key encapsulation does one such operation per input, so each input stays within the fuel of 6.7 that HC-7a grants it. Programs queue the work and run one job per Poll input.
• Not constant time. The libraries are reference code for correctness and replay. Their running time depends on secret data, so a host that faces timing attackers runs them where timing is not observable or uses a vetted adapter through 5.11.
• Secrets stay in D, and D stays on the device. Private keys and ratchet state are program state, and the Random results that made them are entries of D. D is device-local; rce host replay --redact (chapter 16) shows such fields as digests.
• Checked against official vectors. Each library carries check lines for its primitives (run with rce test lib/FILE.rce), and the test suite runs the official vectors of each standard as host steps and then replays the log.

Media and the selective forwarding unit (SFU)

The media adapters (chapter 16, enabled with --media DIR) turn capture and playback into events: D holds (track, sequence number, digest) per frame and the frame bytes are blobs addressed by their Secure Hash Algorithm 256 (SHA-256) digest. A call between more than two peers needs a relay so that each publisher sends a frame once. apps/sfu.rce is that relay, a selective forwarding unit (SFU), written in RCE.

Peers reach the SFU over remote channels. Each wire body is fields separated by U+001F:

The SFU forwards a frame, naming its publisher, to every other subscriber of the track, as an unreliable send: never retried, so a lost frame is one ChanSendDone result that is not delivered (HC-3). A frame whose SEQ is not newer than the last one forwarded for that (room, track, publisher) is dropped as stale, so the latest frame wins. A SEQ that is not 1 to 18 decimal digits, or a body of another shape, is counted as malformed: a peer cannot make the SFU refuse an input. The SFU folds only (track, sequence number, digest) into its state, never a payload, and payloads are end-to-end ciphertext it cannot read. A runnable example is run.sh sfu in the examples of the host runtime.

Direct messages: X3DH and the Double Ratchet

lib/crypto.rce provides SHA-256, the keyed hash HMAC (Hash-based Message Authentication Code), HKDF (the HMAC-based Key Derivation Function of RFC 5869), X25519, the Ed25519 signature scheme (RFC 8032) and an authenticated encryption with associated data (AEAD) built from the ChaCha20 stream cipher with an HMAC-SHA-256 tag. The chat program of chapter 16 uses them for direct messages. Each replica has an X25519 identity key, an Ed25519 signing key and an X25519 signed prekey. It publishes a bundle of the public keys with an Ed25519 signature over the prekey; a received bundle is used only when its signature verifies. For each pair of peers, the one whose name sorts first runs X3DH (the Extended Triple Diffie-Hellman key agreement) as initiator, and both sides then keep one Double Ratchet per peer, so every message has its own key. A message whose plaintext is not well-formed UTF-8 is dropped and counted.

Post-quantum key agreement: ML-KEM-768 and PQXDH

lib/pq.rce adds post-quantum key agreement, used together with lib/crypto.rce:

• Keccak and its functions SHA3-256, SHA3-512, SHAKE128 and SHAKE256 of the Federal Information Processing Standard (FIPS) 202.
• ML-KEM-768, the Module-Lattice-based Key Encapsulation Mechanism (KEM) of FIPS 203 at its middle security level: mlkem_keygen(d, z) gives an encapsulation key and a decapsulation key, mlkem_encaps(ek, m) a ciphertext and a shared secret, mlkem_decaps(dk, c) the shared secret. A forged ciphertext yields an unrelated secret (implicit rejection) rather than an error.
• PQXDH, Signal's post-quantum extension of X3DH. The responder publishes an identity key, a signed prekey and an ML-KEM prekey signed with its Ed25519 identity. The initiator runs three X25519 exchanges (pqxdh_dh_init) and encapsulates to the ML-KEM prekey; the responder runs the same exchanges from its side (pqxdh_dh_resp) and decapsulates. Both derive the session key SK = HKDF(F ‖ DH1 ‖ DH2 ‖ DH3 ‖ SS) with pqxdh_sk, where F is 32 bytes of 0xFF and SS the KEM shared secret. An attacker must break both X25519 and ML-KEM to learn SK.

Each of these is several inputs, one operation each (see Principles). A runnable example is run.sh pqxdh in the examples of the host runtime, which checks the ML-KEM shared secret against the RustCrypto ml-kem crate, that both sides derive the same SK, and that the log replays with secrets redacted.

HPKE and AES-128-GCM

lib/hpke.rce provides AES-128-GCM, the Advanced Encryption Standard of FIPS 197 with a 128-bit key in Galois/Counter Mode (GCM) of the National Institute of Standards and Technology (NIST) Special Publication 800-38D, an AEAD. On top of it is HPKE, Hybrid Public Key Encryption of RFC 9180, in base mode with the suite DHKEM(X25519, HKDF-SHA256), HKDF-SHA256 and AES-128-GCM:

• hp_derive_sk(ikm) derives a private key from input keying material (DeriveKeyPair).
• hpke_seal(pkr, ske, info, aad, pt, seq) encrypts to the recipient's public key with the ephemeral private key ske (from logged random bytes) and gives enc.ciphertext in hexadecimal; seq is the message number of the context.
• hpke_open(skr, enc, info, aad, ct, seq) gives the plaintext, or the empty text when the ciphertext, the additional authenticated data (AAD) or the key does not match.
• encrypt_with_label and decrypt_with_label are the EncryptWithLabel and DecryptWithLabel operations of MLS (below).

The test suite checks the RFC 9180 base-mode vector at sequence numbers 0, 1, 2, 255 and 256 and the MLS EncryptWithLabel vector. A runnable example is run.sh hpke in the examples of the host runtime.

Group keys: MLS

lib/mls.rce is the first part of Messaging Layer Security (MLS), the group key agreement of RFC 9420, for cipher suite 1 (MLS_128_DHKEMX25519_AES128GCM_SHA256_Ed25519). It provides:

• The ratchet tree math of Appendix C of RFC 9420: the nodes of a tree of n leaves are 0 to 2n-2 with leaves at even indices, and tm_root, tm_parent, tm_sibling, tm_direct_path and tm_copath give the structure.
• The key schedule of section 8: mls_epoch(init, commit, psk, ctx) takes the previous epoch's init secret, this commit's commit secret, the pre-shared key (PSK) secret and the serialized GroupContext, and gives the joiner, welcome and epoch secrets, every secret derived from the epoch and the next init secret.
• mls_export, the MLS exporter, and mls_external_pub, the external HPKE public key of an epoch.

The test suite checks the official tree-math.json and key-schedule.json vectors (all five epochs of suite 1). TreeKEM path secrets, commits, adds and removes are later parts. A runnable example is run.sh mls in the examples of the host runtime, whose examples hold the epoch 0 vector.

The sandbox under these programs

The sandbox of HC-5 is one contract, independent of any operating system (OS): the checker admits only programs whose effects go through granted capabilities, and the host refuses any effect without one before any OS layer is involved. The media, channel and storage adapters above are reached only through such capabilities. The same contract has enforcement targets underneath the host: WebAssembly (WASM), bare metal, Linux, macOS, Windows and other OSes, each entered as strictly as the target allows (HC-5 lists the mechanisms). rce host prints the target it entered at start. The contract conforms to OpenIE Sandbox v0.1 (https://sandbox.transaction.science) and to the Joule Context Protocol (JCP) v0.3 (https://jcp.transaction.science).

Appendix A: commands

All files given to one command form one program.

Exit status: 0 success; 1 a program was refused, a test failed, a run reached a refused event, or fmt --check found a file to change; 2 the command was used wrongly.

Every command is deterministic: the same input files give the same output bytes. No command reads the clock, the network or environment variables. The full definitions are in section 10 of the specification.

Appendix B: keywords

These words are reserved and cannot be used as names (specification, section 2.4):

actor     after     and       arena     as        bound     break
chan      check     comptime  const     continue  default   device
elif      else      emit      error     event     example   extern
fail      false     fn        for       forall    from      if
impl      in        intent    iter      kind      let       linear
loop      match     module    mut       none      not       on
or        pass      pub       recv      refused   return    select
self      send      spawn     state     step      struct    then
to        trait     true      try       type      use       var
while     with      yield

Some of them belong to parts of the language this book does not cover yet: arena (memory regions), comptime (evaluation while checking), extern (foreign functions), linear (values that must be used exactly once) and device (accelerator regions). The specification describes each one.

Appendix C: where to read next

• The specification, in spec/book/ of the rce repository, is the definition of the language. Start with 00-overview.md. Section 7 lists every rule name you saw in a refusal, such as W-OWN-1 or W-INT-1.
• Version 0.6, in Appendix C of the specification (spec/book/14-draft06-concurrency.md), adds par, budgets, workgroups, LVars, sessions and supervisors to modules that declare # rce-version: 0.6 on their first line.
• The examples in the specification (spec/examples/) are small programs for each feature, including programs that must be refused.
• rce-examples has longer programs grouped by area: simulation, control, media, networks, text, data, money, science, systems and hardware.
• rce-ide is an editor for RCE that uses the same checker.