Automated reasoning for React/ReasonML
Welcome to VerifiedReact! This is work in progress - stay in touch via @VerifiedByAI, or come chat with us on Discord.
For an overview, read our Medium post Introducing Verified React.
Stage 1 (Counter, TicTacToe)
imandra-http-server
as an alternative to imandra-repl
to allow automation via an HTTP api, bundled with the Imandra installer. Previously you could automate our imandra-repl
process via stdin/stdout, but having an HTTP interface to the Imandra client naturally makes life a lot easier. imandra-http-server
is built using our Imandra_client
OCaml library, which we're hoping to make available as an opam
package in the future, so OCaml users can use the Imandra client directly from their code.bs-imandra-client
- bucklescript bindings to that HTTP api to be used when running on Node.iml
(Imandra-ml) or .ire
(Imandra-reason) code. When you're done reasoning and want to compile the verified module into a larger program, you need a .ml
version of the prelude to compile alongside your module. Previously this was available to compile as native OCaml package, but we've now also included an initial amended version that compiles to javascript via the bucklescript compiler too, which can be npm installed
from the imandra-prelude
repo.jest
, via imandra-http-server
. See:
examples/simple/__tests__/Counter_Goals.ml
examples/tictactoe/__tests__/TicTacToe_Logic_Goals.re
examples/todomvc/__tests__/TodoMvc_Model_Goals.re
examples/tictactoe/TicTacToe.re
Stage 2
Stage 3
Make sure you have the latest version of imandra-repl
installed via the Imandra Installer, then run
imandra-repl
and make sure it starts up successfully (i.e. all updates are installed). Once it's started, quit it again with Ctrl-D. Next:
npm install
to install the bucklescript compiler, imandra-prelude
and Imandra client bindings for bucklescript. Then:
npm run watch
You may see a few errors the first time you run watch - this I believe is due to an issue with components
in bsb.exe
as they are a WIP. However, if you run npm run watch
multiple times, you should stop seeing errors after a few builds, and from then on incremental compilation will work sucessfully.
For runtime:
.iml
and .ire
files are compiled to .ml
files using imandra-extract
(which is bundled with the Imandra Installer), and integrated into the build via bsb
components..ml
and .re
files are compiled to .bs.js
via bsb
itself.Imandra_prelude
is available automatically inside imandra-http-server
Imandra_prelude
is provided by imandra-prelude, added as an npm/bucklescript dependency.bs-imandra-client
) are used to spin up imandra-http-server
(which is bundled as part of the Imandra Installer), which is an OCaml binary talking to Imandra's reasoning engine in the cloud..iml
and .ire
files into the running imandra-http-server
OCaml process, and perform verification statements.To run the verification goals:
npm run test
Read our post about viewing instances in your UIs with Imandra.
The TicTacToe example is hooked up to Imandra to allow querying and viewing instances. To start it, from the verified-react
repo root run:
imandra-http-server -reason
to start Imandra's http server with reason
syntax loaded. Then for bucklescript compilation, (in another terminal) run:
npm install
npm run watch
Then, to start the parcel.js dev server, (in another terminal) run:
npm run watch-tictactoe
You should now be able to visit http://localhost:1234
to see/play the TicTacToe game (verified via the npm run test
Jest tests), and also query for instances from Imandra.
The TicTacToe UI is wrapped in an InstanceBrowser component, which loads the game logic into Imandra (along with some JSON encoders and decoders) via examples/tictactoe/Setup.ire
.
The TicTacToe UI component has been edited slightly to allow a default intial state to be passed from its parent via the customInitialLogicState
prop.
When the instance query box's contents change, the query is sent to imandra-http-server
's /instance/by-src
endpoint as a lambda expression, x : game_state => <constraint>
, so an instance of type game_state
matching the constraint is returned, printed to a JSON string via a serialisation function (instancePrinterFn
).
This returned instance is then passed to the customInitialLogicState
prop and rendered by the UI component.