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, rce emit js and rce emit scala 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.

$ 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, runs each one, and requires its output to equal the reference interpreter's.

Started with the argument --run, an emitted program runs fn main instead, with its tasks and channels (chapter 14). An emitter does not yet print a module with a contract (chapter 4) or a ct fn (chapter 19): for such a module rce emit prints the rule (W-RES-1 or W-CTFN-2) and the construct, and exits with status 1. rce run and rce test still run it.

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.