Experiments in Quint ML

This repo holds some experiments focused on or around quint and conducted in the MLs OCaml and F*.

Everything in here is very rough and a WIP.

Contents Worth Remarking

./tryf/

An EDSL aiming to capture the pure and action fragments of quint in F*.

• See the example in ./tryf/Quint.Ex.TicTacToe.fst for an example of how this EDSL can be used.

./bin/main.ml

Entrypoint for a CLI that runs the ./tryf/Quint.Ex.TicTacToe.fst example. This shows how we can integrate the code compiled from F* with normal ocaml code.

./test/quint-ml-demo.t

Blackbox CLI tests showing invocation of the CLI.

./notes.org

Working notes on the project

./bin/ocaml_ttt_ex_main.ml

A sketch of an OCaml approach to a toy quint spec. This was a prelude to the F* code.

Building for development

Assuming you have opam installed:

Install dependencies

git clone git@github.com:informalsystems/quint-ml-experiments.git
cd quint-ml-experiments
opam switch create . --deps-only --with-test --locked

Build

dune build

Test

dune test

Run the demo simulation

dune exec quint-ml-demo

See the integration tests for more usage examples.

Installing from source

opam pin add https://github.com/shonfeder/quint-ml-experiments.git --locked