Introduction

This book teaches the RCE programming language from the beginning. RCE stands for Reality Code Engine: a language and toolchain made for the AI coding era, in which every program has the one shape of the Form, so that programs can be written, checked, changed and run by machines with no language model in the loop. The shape is rigid at each commit of the specification and grows inside the same text when a program needs a form it lacks. 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 language whose programs take their meaning from a written specification, and there is one language: the specification at one commit, extended inside the same text when a program needs a form it lacks, with no per-module version selection. 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 reads a program into its Form, naming the place where a text does not yet have the Form's shape; 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. A program's meaning is settled before it runs. Ownership, every case of a match and the program's own tests are part of its Form, so an accepted program never uses memory after giving it away, never leaves a case unhandled, and its tests hold. Where a text does not yet have that shape, the checker names the place and the rule.

Status

Reality Code Engine, draft 0.9. The specification is published for review and can still change. There is one language: the specification at one commit. Drafts 0.5 to 0.9 are labels of past commits of that language, not alternatives. A # rce-version: line is a release label. It is tolerated, ignored and not hashed, and it is not a per-module language selection. This book teaches sections 2 to 10 of that one text. What exists today:

• the specification, with its grammar checked by machine;
• a reference checker and interpreter, rce, which this book uses for every example, with the whole standard library built in (use enc, use data.events: nothing to install);
• emitters that translate a checked program to Rust, Python, JavaScript and Scala, which agree with the reference; emitting every language by table, and lifts that bring programs in those languages into the Form, are the design of spec/proposals/rce-form.md (one Go pattern is lifted by a probe today).

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 requiring change must require change, 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 how a command ended: 0 means success, 1 means the program requires change, a step kept the state, or a test failed, and 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 requires change.

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 pick a value. The addition traps: it stops with an error. Because the check below needs that addition, the program requires change:

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

check small_sum(200, 100) == 44

rce check says:

$ rce check overflow.rce
requires change 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 requires change too, under the type rule W-TY-1:

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

$ rce check mixed_types.rce
requires change 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 requires change under 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(limit: u64) -> u64
    var k: u64 = 0
    while k < limit bound 10
        k += 1
    return k

check spin(100) == 10

$ rce check spin.rce
requires change 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 requires change.

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 -> kept: 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 -> kept: Underflow means: applying Dec to a fresh counter must keep the state, with the error Underflow as the reason.

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 means the program requires change

Change the expected value and the program requires change:

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
requires change 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 requires change (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 a step keeps the state.

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 -> kept: 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 keeps the state, with Locked as the reason.
• 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 requires change:

state Counter
    n: u64 = 0

event Inc
event Dec

step Counter on Inc -> n + 1

$ rce check unhandled_event.rce
requires change 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 failing; otherwise the step keeps the state.

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 step that keeps the state leaves it unchanged, and the run stops there: 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 kept: Locked
exit status: 1

The exit status is 1 because a step kept the state.

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 keeps the state with Underflow as the reason.

$ 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 kept: 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 kept outcomes

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

Keeping the state

intent "a bank account that keeps its balance on an overdraft (Insufficient)"
    example Deposit(amount: 50), Withdraw(amount: 20) -> 30
    example Withdraw(amount: 1) -> kept: 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) keeps the state, with that error as the reason.
• 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) kept: Insufficient
exit status: 1

The third event asks for more than the balance, so its step keeps the state 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. Code that uses it as one requires change 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 keeps the state.

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 keeps the state, 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 steps that keep the state.
• Error unions T ! E, with try, catch and catch |e|.
• A trap keeps the state 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. A match that forgets one requires change, 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
requires change 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_chars() == 5
check "héllo".len_bytes() == 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_chars() as u64

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

$ rce check use_after_move.rce
requires change 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 requires change. If you really need two independent values, copy(s) makes a full copy.

Borrowing

fn length(s: &text) -> u64 = s.len_chars() 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
requires change 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") -> kept: 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. On a fourth, the guarded step keeps the state:

$ 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") kept: CartFull
exit status: 1

Look at the last line. Stats would have counted the fourth add, but because the step of Cart kept the state, neither region changed. An event applies to every region or to none. This is what makes a kept step 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 the state of all of them is kept.

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: a call with a type that cannot be compared requires change. 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)

pub fn priced(id: u64, cents: i64) -> Order = Order(id: id, total: pricing.discount(cents, 10))

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 requires change, because the module it uses is not part of the program:

$ rce check shop/orders.rce
requires change shop/orders.rce: line 2: W-NAME-1 unknown module `shop.pricing`; line 10: W-NAME-1 unknown name `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 requires change:

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
requires change 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 requires change, 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
requires change 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 require change 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":"16ec075c0865aec98a67b14c2a42302d34ff5a694a31055d3ee1b6847478cf84","hashed":{"event":{"payload":[],"type":0},"state":[[1]]},"out":[],"outcome":"applied","prev_hash":"0000000000000000000000000000000000000000000000000000000000000000","seq":0,"state":{"Counter":{"n":1}},"state_hash":"043f347c2cdc0d8ce70c38775d24e556c0290acf6d0c87a3a52aa85471cb8d02"},{"event":{"payload":{},"type":"Inc"},"hash":"8911401820cf55e5fb432c9759efc78c60a54fb3fa8f6e3cc2647fc6f288a3e2","hashed":{"event":{"payload":[],"type":0},"state":[[2]]},"out":[],"outcome":"applied","prev_hash":"16ec075c0865aec98a67b14c2a42302d34ff5a694a31055d3ee1b6847478cf84","seq":1,"state":{"Counter":{"n":2}},"state_hash":"24227028f5989317de063afa979c6b34bfd191537b8fd2ed796a820bf47b2024"},{"event":{"payload":{},"type":"Dec"},"hash":"889e65598130b4034cb95afb4a80628291433e7089139e54478e0b0b2b343bdb","hashed":{"event":{"payload":[],"type":1},"state":[[1]]},"out":[],"outcome":"applied","prev_hash":"8911401820cf55e5fb432c9759efc78c60a54fb3fa8f6e3cc2647fc6f288a3e2","seq":2,"state":{"Counter":{"n":1}},"state_hash":"043f347c2cdc0d8ce70c38775d24e556c0290acf6d0c87a3a52aa85471cb8d02"}]},{"example_line":3,"D":[{"event":{"payload":{},"type":"Dec"},"hash":"07ad897ce740329566c1740b942501d6ccf683d3b86e9de3a42c3b06c238e47c","hashed":{"event":{"payload":[],"type":1},"state":[[0]]},"out":[{"Kept":{"error":"Underflow","payload":{}}}],"outcome":{"kept":"Underflow"},"prev_hash":"0000000000000000000000000000000000000000000000000000000000000000","seq":0,"state":{"Counter":{"n":0}},"state_hash":"db407f11d7ede59abaab0e98e097ff2dae10a048207b801745d7199ef19c2387"}]}],"main":null,"source":"\nintent \"a counter that never goes below zero\"\n    example Inc, Inc, Dec -> 1\n    example Dec -> kept: 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",[]]],"kept":null,"value":{"Int":[1,2]},"line":2},{"events":[["Dec",[]]],"kept":"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,"foreign":null}},{"Event":{"name":"Dec","payload":[],"line":9,"interrupt":null,"foreign":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,true]},{"Name":["Underflow",14]},14]}},"line":14,"deadline":null}}],"pubs":[]},"names":{"intent":["a counter that never goes below zero"],"items":[{"key":"#1","kind":"state","name":"Counter"},{"key":"#2","kind":"event","name":"Inc"},{"key":"#3","kind":"event","name":"Dec"},{"key":"#4","kind":"error","name":"Underflow"}]}}
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 names, the concept record of specification 6.6: the names as written and the intent strings, keyed by declaration index, printed after the hashed fields and never read by a step. 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. What is hashed is not the readable state and event you see but their positional forms, repeated under hashed: the regions and fields as lists in declaration order, and the event by its index. So renaming everything in a program changes no hash, which is what theorem T7 promises. 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 a target language

RCE is designed so that every language is both an output and an input of the Form. In that design a target is a row of the emit registry (spec/proposals/emit-targets.md), one table per language, each passing the same gate, the reference trace of every example program byte for byte; the design is not built yet. This chapter uses the targets the reference checker emits today.

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 kept: 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 kept: 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, JavaScript and Scala that print the same observations as the reference interpreter on the conformance suite; further targets are to be registry rows, not new emitters.

Host tools: RCEdb, HTTP, media, redacted replay and chat

This chapter covers five 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. The program of this chapter, hello_http.rce, is checked with rce test like the listings of the other chapters; serving it needs a network, so the exchange shown with it is an example, not checked output.

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 KEPT E with the error E the module raised; a kept 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 keeps the state, 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.

Serving HTTP: rce host serve FILE --log D --http HOST:PORT

rce host serve is the host loop. It admits each input into D as it arrives, performs the effects the step emits, and admits each effect's result as another input. A line on standard input is an input written in event syntax, a declared Tick(n) arrives every frame, and Display(data) is written to standard output. When the loop ends, D is replayed with every adapter disconnected, and the run counts only if replay gives the state hash the live run had.

With --http HOST:PORT the host listens on that address itself and turns each request of the Hypertext Transfer Protocol (HTTP/1.1) into one input. The listing declares the request, the malformed request, the response and its result with the host's own shapes, so each is delivered exactly. A program may declare them with other fields, or not at all: the host then delivers each value as the declaration takes it, matching fields by name, and records in D what it did not deliver and why (Appendix E, E.4c, HD-2).

module hello_http

intent "answer GET /hello with a greeting and any other request with 404; a malformed request gets the status the host names, and a step that keeps the state 500"
    example HttpRequest(id: 5, method: "GET", target: "/hello", version: "HTTP/1.1", names: ["Host"], values: ["x"], body: []) -> answered == 1 and last == 200
    example HttpRequest(id: 5, method: "POST", target: "/hello", version: "HTTP/1.1", names: ["Host"], values: ["x"], body: [104, 105]) -> last == 404
    example HttpMalformed(id: 5, status: 431, why: "over 100 fields") -> last == 431
    example StepKept(seq: 5, cause: "fuel") -> last == 500

struct HttpRespond
    req: u64
    status: u64
    names: List[text]
    values: List[text]
    body: text

event HttpRequest(id: u64, method: text, target: text, version: text, names: List[text], values: List[text], body: List[i64])
event HttpMalformed(id: u64, status: u64, why: text)
event HttpRespondDone(req: u64, status: text, data: u64?, err: text)
event StepKept(seq: u64, cause: text)

state Greeter
    answered: u64 = 0
    last: u64 = 0

fn reply(id: u64, status: u64, body: text) -> HttpRespond = HttpRespond(req: id, status: status, names: ["Content-Type"], values: ["text/plain"], body: body)

step Greeter on HttpRequest(id: id, method: m, target: t, version: _, names: _, values: _, body: _)
    let found = m == "GET" and t == "/hello"
    last = if found then 200 else 404
    answered += 1
    emit reply(id, last, if found then "hello\n" else "not found\n")

step Greeter on HttpMalformed(id: id, status: st, why: w)
    last = st
    emit reply(id, st, w + "\n")

step Greeter on StepKept(seq: q, cause: c)
    last = 500
    emit reply(q, 500, "kept: " + c + "\n")

step Greeter on HttpRespondDone(_, _, _, _)
    pass

Each request arrives as HttpRequest(id, method, target, version, names, values, body). The id is the sequence number of the request's own entry in D, and the step answers by emitting HttpRespond with the same req. Run rce host serve hello_http.rce --log D --http 127.0.0.1:8080 and, in another terminal, curl -i http://127.0.0.1:8080/hello prints:

HTTP/1.1 200 OK
Content-Type: text/plain
Content-Length: 6

hello

The host wrote the status line and Content-Length; every other byte came from the program. Whether the host also writes Connection: close and closes the connection depends on the request's version and its Connection field, which D records, so every response is a function of D (HC-26). A response the host cannot write correctly, for example one with a status outside 200 to 599 or a Content-Length written by the program, fails the effect, with the reason in HttpRespondDone, and leaves the request open, so the step that receives that result can answer again. A delivered result means the host handed the response to the connection; a client that has gone by the time it is written is not reported.

The host reads requests from many connections at once, so a client that sends nothing holds up no other. It applies its limits before a byte enters D: a request line over 8,192 bytes, a head over 64 KiB or 100 fields, a body over 1,000,000 bytes, a head not complete within 10 seconds of its first byte, and any error of syntax arrive as HttpMalformed(id, status, why), with 414, 431, 413, 408 or 400 as the status, and the program answers them like any other request (HC-25). A connection that closes before its request is complete adds nothing. An idle host appends nothing to D. The termination signal (SIGTERM) stops the loop: the host stops accepting connections, gives the open requests up to 5 seconds, makes D durable and validates it.

programs/network/notes_http.rce is a complete JSON notes service written this way. Its examples test every answer without a network.

Bytes, kept steps and restarts

Three inputs reach a program on the host that it never asks for.

• Bytes. Bytes from outside arrive exactly as they were received, as a List[i64] of values from 0 to 255: the body of HttpRequest, and the data of NetRecvDone below (HC-10a). A body that is not valid UTF-8 is therefore a value, not a trap; utf8.utf8_valid(&b) from use text.utf8 tells the step whether it may call b.utf8().
• Kept steps. When a step keeps the state, by a declared error, a trap or a limit such as fuel, D records the input with the state unchanged (chapter 6), then host.StepKept, and then, if the program declares event StepKept(seq: u64, cause: text), the input StepKept with the kept entry's seq and a cause: fail, trap, fuel, size, value or depth (HC-21). On the HTTP event host the seq is the id of the request, so the StepKept step of hello_http.rce answers that request with 500 instead of leaving its client waiting.
• Restarts. Sockets and terminals belong to one host process. A host started on an existing D appends host.Restarted with its own seq, and admits Restarted(below: u64) if the program declares it, before it reports every request the earlier process left unanswered as failed with interrupted (HC-22). New ids start at below, so an id the program kept from before the restart names no new socket.

The net adapter: --net HOST:PORT

--net HOST:PORT grants connections of the Transmission Control Protocol (TCP) as effects, at that exact address: NetConnect, NetListen, NetAccept, NetSend, NetRecv and NetClose, each with one result event (HC-23). NetRecv returns the bytes that have arrived so far, possibly none, and never waits; NetSend hands its bytes to a writer of the connection and returns at once. A program on this adapter frames its own protocol and asks for more bytes on each Tick, so it serves one connection per frame. For HTTP the event host above does the framing, serves connections concurrently and needs no Tick.

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 does not play 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: no input from a peer makes a step of the SFU keep the state. 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 does not perform 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, in a line made from the rules it installed (HC-5a): on Linux, Landlock restricts TCP bind and connect by port and not by address, so the line says "by port" and names the addresses the net adapter allows, and it says when the User Datagram Protocol (UDP) is not restricted; with --http alone the listener is opened before the target is entered and the line says that no new Internet Protocol (IP) socket can be opened. 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).

Behaviour, sameness and dimension

Two programs can look different and be the same. This chapter says what "the same" means in RCE, how the checker can tell, and how to measure how much of a program's state is doing work.

The behaviour of a program

Run any sequence of events through a program and write down what it emits at each step. That table, for every possible sequence, is the program's behaviour. Nothing else about the program is part of its behaviour: not the names of its fields, not the order its steps are written in, not what it keeps in state and never reads. The specification (section 6.10) defines behaviour exactly this way, and defines two programs to be equivalent when their behaviours are equal.

That is the only sense of "same" the Form needs. It is also why the emitters can be checked: a Rust program and a Python program emitted from one Form are correct when they have the same behaviour, and the reference trace of chapter 15 is a prefix of that table.

How the checker decides it

You cannot list every event sequence; there are infinitely many. The specification gives two ways round that.

The first is a bisimulation: a relation between the states of two programs such that related states emit the same thing on every event and land in related states. If the starting states are related, the behaviours are equal (T58). To show two programs are the same, exhibit the relation; to show they differ, exhibit one event sequence where the outputs part.

The second is a distance. Two behaviours that agree on every sequence up to length k and differ at k + 1 are at distance 2^-(k+1). Trace tests like those of chapter 15 therefore prove closeness, not equality: rce trace agreeing on 40 events shows the two programs are within 2^-41 of each other. That is why a trace never enters a hash in RCE; a hash names one thing, and a trace names a neighbourhood.

Dimension: how many behaviours can a program be in?

Every RCE program has finite state, so the set of states it can reach is finite, and the number of different behaviours among those states is a number. The specification calls it the program's dimension, dim(P). It is the count of states a minimal machine with the same behaviour would need. State beyond that is redundancy: bits that no future output depends on.

rce dim measures it. It explores the states reachable from the start through every event, with payloads drawn from each type's edge values, then groups states that behave alike.

Here is a counter mod 4 that also remembers whether the last event was an increment. Nothing reads that flag:

intent "a counter mod 4 that also records the last event, which nothing reads"
    "rce dim (10.11): 8 states explored, 4 behaviours, redundancy 1.00 bit; region DimCounter reports the 1 bit"
    example DimInc, DimInc, DimInc, DimInc -> n == 0
    example DimInc, DimDec -> last_inc == false

state DimCounter
    n: u64 = 0
    last_inc: bool = false

event DimInc
event DimDec

step DimCounter on DimInc
    n = (n + 1) % 4
    last_inc = true
    emit n
step DimCounter on DimDec
    n = (n + 3) % 4
    last_inc = false
    emit n

$ rce dim counter_flag.rce
states explored     8        bound reached: no
behaviours          4        dim(P) (exact)
redundancy          1.00     bits: log2(states) - log2(behaviours)
outputs             yes      some explored step has a λ output (emits: yes, keeps: no)
distinct outputs    4        distinct output sequences over the explored steps (silent steps excluded)
  region DimCounter   1.00     (8 values, 4 distinguish behaviours)
exit status: 0

Eight states, four behaviours, one bit of redundancy, and the report says which region carries it. The flag can go.

Redundancy is not always a spare field. This program keeps a count mod 6 but only ever emits its parity:

intent "a counter mod 6 whose only output is its parity"
    "rce dim (10.11): 6 states explored, 2 behaviours, redundancy 1.58 bits: the state carries a period of 6 but the behaviour has a period of 2"
    example DimStep -> n == 1
    example DimStep, DimStep, DimStep, DimStep, DimStep, DimStep -> n == 0

state DimPhase
    n: u64 = 0

event DimStep

step DimPhase on DimStep
    n = (n + 1) % 6
    emit n % 2

$ rce dim phase.rce
states explored     6        bound reached: no
behaviours          2        dim(P) (exact)
redundancy          1.58     bits: log2(states) - log2(behaviours)
outputs             yes      some explored step has a λ output (emits: yes, keeps: no)
distinct outputs    2        distinct output sequences over the explored steps (silent steps excluded)
  region DimPhase     1.58     (6 values, 2 distinguish behaviours)
exit status: 0

Six states, two behaviours: the state has a period of six, the behaviour has a period of two, and log2(6) − log2(2) = 1.58 bits of state change no future output.

And here is the door from chapter 10, where every reachable state answers some future event differently:

intent "a door whose state is exactly its behaviour"
    "rce dim (10.11): 3 states explored (open and locked at once is unreachable), 3 behaviours, redundancy 0.00 bits: every reachable state answers some future event differently"
    example DimOpen, DimClose, DimLock -> locked
    example DimOpen, DimLock -> kept: DimDoorOpen

state DimDoor
    open: bool = false
    locked: bool = false

event DimOpen
event DimClose
event DimLock
event DimUnlock

error DimDoorOpen
error DimLocked

step DimDoor on DimOpen if locked
    fail DimLocked
step DimDoor on DimOpen
    open = true
step DimDoor on DimClose
    open = false
step DimDoor on DimLock if open
    fail DimDoorOpen
step DimDoor on DimLock
    locked = true
step DimDoor on DimUnlock
    locked = false

$ rce dim door.rce
states explored     3        bound reached: no
behaviours          3        dim(P) (exact)
redundancy          0.00     bits: log2(states) - log2(behaviours)
outputs             yes      some explored step has a λ output (emits: no, keeps: yes)
distinct outputs    2        distinct output sequences over the explored steps (silent steps excluded)
  region DimDoor      0.00     (3 values, 3 distinguish behaviours)
exit status: 0

Three states, not four: a door cannot be open and locked at once, because Lock keeps the state while open and Open keeps it while locked. Three behaviours, no redundancy. This program's state is exactly its behaviour.

State nobody can see

The traffic light of chapter 5 has three states and, by this measure, one behaviour: it never emits and no step of it keeps the state, so no sequence of events gets a different answer from any state. Its examples check light == Yellow, but an example reads the state from inside; the Form's behaviour is what comes out. rce dim on that program reports 3 states, 1 behaviour and 1.58 bits of redundancy, and it is right: as written, the light's colour is in the state, and in the log, but no output depends on it. Add emit light to its step and the three states become three behaviours. When the first run of rce dim over the specification's own examples was made, most of its state machines turned out to be of this kind.

The control view

rce dim --control asks a coarser question: not what the program emits, but which steps fire. Two states are control-equivalent when every event sequence makes the same steps fire, keep the state or emit the same kinds of thing from both. The count is never larger than the behaviour count, and its canonical form is hashed as shape_ctl, a key that does not change when you rename anything:

$ rce dim --control door.rce
states explored     3        bound reached: no
behaviours          3        dim(P) (exact)
redundancy          0.00     bits: log2(states) - log2(behaviours)
outputs             yes      some explored step has a λ output (emits: no, keeps: yes)
distinct outputs    2        distinct output sequences over the explored steps (silent steps excluded)
  region DimDoor      0.00     (3 values, 3 distinguish behaviours)
control states      3        dim_c(P) (exact)
shape_ctl           sha256:cf0bc0895132723a218efd65c63e69596fb0f05e0bb348feeaef5cd85dd1e392
exit status: 0

For the door the two counts agree. For the mod-4 counter they do not: every event fires the same step with the same kind of output, so it has one control state and four behaviours. The gap between the two numbers is how much of the behaviour lives in data rather than in control.

When the count is a lower bound

A program whose state can grow without limit, like the plain counter of chapter 4, has more reachable states than rce dim will visit. It stops at --fuel states (100,000 by default), says bound reached: yes, and reports the behaviours it found as a lower bound. Exploration is deterministic: the same program and the same fuel give the same report, byte for byte.

What you learned

• A program's behaviour is what it emits on every event sequence; two programs are the same when their behaviours are equal.
• A bisimulation proves sameness; one distinguishing sequence proves difference; a trace proves closeness to within 2^-(k+1).
• rce dim counts the behaviours a program can be in and reports the redundancy of its state per region, in bits; --control counts the control states and hashes their canonical form as shape_ctl.

Appendix A: commands

All files given to one command form one program.

Exit status: 0 success; 1 a program requires change, a test failed, a run reached a step that kept the state, 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      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 "requires change" report, 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 require change.
• programs/ 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.