Repository files navigation

Welcome to VerifiedReact! This is work in progress - stay in touch via@VerifiedByAI, or come chat with us onDiscord.

For an overview, read our Medium postIntroducing Verified React.

• Stage 1 (Counter, TicTacToe)

  • Simpler automation of Imandra:
    • addedimandra-http-server as an alternative toimandra-repl to allow automation via an HTTP api, bundled with theImandra installer. Previously you could automate ourimandra-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 ourImandra_client OCaml library, which we're hoping to make available as anopam package in the future, so OCaml users can use the Imandra client directly from their code.
    • addedbs-imandra-client - bucklescript bindings to that HTTP api to be used when running on Node
  • Allow export of export of core logic verified with Imandra to code that can be compiled to executable JS
    • Imandra comes with a prelude of pre-verified functions for use from.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 benpm installed from theimandra-prelude repo.
  • Automation of verification goals viajest, viaimandra-http-server. See:
    • examples/simple/__tests__/Counter_Goals.ml
    • examples/tictactoe/__tests__/TicTacToe_Logic_Goals.re
    • examples/todomvc/__tests__/TodoMvc_Model_Goals.re
  • Hook verified state machine up to React reducer component. See:
    • examples/tictactoe/TicTacToe.re

• Stage 2

  • Viewing instances - also seeour blog post
  • TodoMVC as a larger example
  • Decomposition visualisation

• Stage 3

  • Collecting React reducer events from React unit test runs
  • Map reducer events back to state machine events, and visualise coverage on the decomposition
  • Coverage report of state space as hit by your jest tests

Make sure you have the latest version ofimandra-repl installed via theImandra 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 withcomponents inbsb.exe as they are a WIP. However, if you runnpm 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 usingimandra-extract (which is bundled with theImandra Installer), and integrated into the build viabsb components.
• .ml and.re files are compiled to.bs.js viabsb itself.
• Imandra_prelude is available automatically insideimandra-http-server
• When compiling to javascript,Imandra_prelude is provided byimandra-prelude, added as an npm/bucklescript dependency.

• Tests are run via Jest on node.js using the compiled runtime JS files.
• As part of the test run, the Imandra client bucklescript bindings (bs-imandra-client) are used to spin upimandra-http-server (which is bundled as part of theImandra Installer), which is an OCaml binary talking to Imandra's reasoning engine in the cloud.
• The HTTP Imandra client API is used to load.iml and.ire files into the runningimandra-http-server OCaml process, and perform verification statements.
• The verification results are captured and reported back as part of the Jest test run.

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 theverified-react repo root run:

imandra-http-server -reason

to start Imandra's http server withreason syntax loaded. Then for bucklescript compilation, (in another terminal) run:

npm installnpm run watch

Then, to start the parcel.js dev server, (in another terminal) run:

npm run watch-tictactoe

You should now be able to visithttp://localhost:1234 to see/play the TicTacToe game (verified via thenpm run test Jest tests), and also query for instances from Imandra.

The TicTacToe UI iswrapped in an InstanceBrowser component, which loads the game logic into Imandra (along with some JSON encoders and decoders) viaexamples/tictactoe/Setup.ire.

The TicTacToe UI component has been edited slightly to allow a default intial state to be passed from its parent via thecustomInitialLogicState prop.

When the instance query box's contents change, the query is sent toimandra-http-server's/instance/by-src endpoint as a lambda expression,x : game_state => <constraint>, so an instance of typegame_state matching the constraint is returned, printed to a JSON string via a serialisation function (instancePrinterFn).

This returned instance is then passed to thecustomInitialLogicState prop and rendered by the UI component.