Our meeting with Nate drove the conversation around developing a better formalization for Rio – via a type system and an operational semantics. The type system lives on now as a checker at parsing-time. The operational semantics may prove more long-lasting.
67 (linked above as well) presents my first-draft model of the Operational Semantics for the language. My eventual intent is to be able to formally verify its equivalence with Rio-to-tree compilation (more formally, show that pushing and popping from a Rio program interpreted via these semantics will always give the same result as pushing and popping from a PIFO tree result of compilation).
Content
This PR solidifies the semantics by presenting a concrete OCaml artifact of them. Within it, I have defined modules for packets, queues and semantics, and defined popping and pushing (with respect to programs and queues) as I do in #67.
I also present a test suite which generates random tests, stores them similarly to the .data input files we used to work with with Calyx, and then tests them against their output.
Final Touches (Incoming)
Testing doesn't quite work yet! While the framework, inputs & outputs are set up, they're not quite working according to plan. I'm debugging it and I expect it to be fixed pretty soon.
I'm marking this as a draft for the time being. I just like having it here since it's a tidy link to point folks to about the current status on the semantics.
Background and Context
Our meeting with Nate drove the conversation around developing a better formalization for Rio – via a type system and an operational semantics. The type system lives on now as a checker at parsing-time. The operational semantics may prove more long-lasting.
67 (linked above as well) presents my first-draft model of the Operational Semantics for the language. My eventual intent is to be able to formally verify its equivalence with Rio-to-tree compilation (more formally, show that pushing and popping from a Rio program interpreted via these semantics will always give the same result as pushing and popping from a PIFO tree result of compilation).
Content
This PR solidifies the semantics by presenting a concrete OCaml artifact of them. Within it, I have defined modules for packets, queues and semantics, and defined popping and pushing (with respect to programs and queues) as I do in #67.
I also present a test suite which generates random tests, stores them similarly to the .data input files we used to work with with Calyx, and then tests them against their output.
Final Touches (Incoming)
Testing doesn't quite work yet! While the framework, inputs & outputs are set up, they're not quite working according to plan. I'm debugging it and I expect it to be fixed pretty soon.
I'm marking this as a draft for the time being. I just like having it here since it's a tidy link to point folks to about the current status on the semantics.