The Form and the emitters

The Form

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

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

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

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

Emitting Rust, Python and JavaScript

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

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

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

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

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

What you learned

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