Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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.

Changing a program

Behaviour is also what decides whether a change to a program is safe. Three commands answer the question from different sides.

rce hash names each definition by a hash of its text with every declared name replaced by its position. Here is a second version of the counter of the tour, whose Dec is written as two steps instead of one:

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 if n == 0
    fail Underflow
step Counter on Dec -> n - 1

$ rce hash counter_v2.rce
b0562f9794dc5733c70479eefac5879016a9a517b51a082af124c766284395ed  state Counter  pub
2dc6cdf92460a1f39f996982a11bb4d58e477640faa6c59cd94d7e1d44981ced  event Inc  pub
2dc6cdf92460a1f39f996982a11bb4d58e477640faa6c59cd94d7e1d44981ced  event Dec  pub
76507de38a8fce86b67180b9da859c60b592c2cffc85212887300d323b15e40d  error Underflow  pub
a8374f2c4d3a0420f18870c5dfc0df15adec88465b3d552861d60dbe0f489127  program
exit status: 0

Inc and Dec have the same hash: without their names, two events with no payload are the same definition. pub marks an export, a definition that other programs can name. The last line is the hash of the whole program. rce api-diff OLD NEW compares the exports of two versions, one row per change, each compatible or breaking.

rce change OLD NEW puts the two together: both program hashes, the api-diff rows and the check of rce equiv. It decides an erratum when every export is compatible and every behaviour is kept:

$ rce change --fuel 1000 ../tour/counter.rce counter_v2.rce
program             4631c798c37181944d74d4c6a90fdfc273747787b15df8388f524550327c4cb5
                    a8374f2c4d3a0420f18870c5dfc0df15adec88465b3d552861d60dbe0f489127
api                 no export changed
behaviour alphabet            2        event instances explored
behaviour states              1000 / 1000
behaviour verdict             equivalent  same behaviour on the explored alphabet (to the explored bound)
verdict             erratum to the explored bound  every export compatible and every behaviour kept as far as explored
exit status: 0

A meaning change when a behaviour changed, with the sequence that shows it:

$ rce change --fuel 1000 ../tour/counter.rce ../tour/sloppy.rce
program             4631c798c37181944d74d4c6a90fdfc273747787b15df8388f524550327c4cb5
                    fe1f224134b853b16bb3cac10037d20b40584f8e60ce726a02062a59842da59b
api                 breaking	error Underflow	export removed or renamed
behaviour alphabet            2        event instances explored
behaviour states              1000 / 1000
behaviour verdict             different
behaviour after               Dec()
behaviour   A                 kept: Underflow
behaviour   B                 silent
verdict             meaning change  the behaviour of the program changed
exit status: 1

And an interface change when the behaviour is kept but an export a caller could name is gone. The renamed counter of the tour behaves the same, but every name a caller used has changed:

$ rce change --fuel 1000 ../tour/counter.rce ../tour/tally.rce
program             4631c798c37181944d74d4c6a90fdfc273747787b15df8388f524550327c4cb5
                    7d16ded6e2398dda981219bd7ade850624b68f4b8b7bbe74115287c9d87e383f
api                 compatible	error BelowZero	export added
api                 breaking	state Counter	export removed or renamed
api                 breaking	event Dec	export removed or renamed
api                 compatible	event Down	export added
api                 breaking	event Inc	export removed or renamed
api                 compatible	state Tally	export added
api                 breaking	error Underflow	export removed or renamed
api                 compatible	event Up	export added
behaviour alphabet            2        event instances explored
behaviour states              1000 / 1000
behaviour verdict             equivalent  same behaviour on the explored alphabet (to the explored bound)
verdict             interface change  behaviour kept, an export broken (F.4.3): callers must change
exit status: 1

The counter grows without end, so each verdict holds "to the explored bound". When the bound is reached before the two programs are told apart or shown equal, the verdict is undecided, with exit status 3: raise --fuel. The decision is the tool's, read off the two programs, not a version number someone typed. Chapter 16 shows where it is used: a log may be rebound to a changed program only after an erratum.

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.
  • rce hash, rce api-diff and rce change say whether a change keeps the exports and the behaviour: erratum, meaning change or interface change.