For information about OSL, see: https://eprint.iacr.org/2022/1003
This version of OSL differs from the one described in the above paper in that it features bounded quantification, as in: https://eprint.iacr.org/2022/1105
The system must have Nix, with flakes enabled.
To install Nix: https://nixos.org/download.html
To enable flakes: https://nixos.wiki/wiki/Flakes#Enable_flakes
To build the OSL compiler, run:
nix build
If successful, the binary will be output at ./result/bin/osl.
The compiler expects two command line arguments: first, a path to an OSL source file, and second, the name of a declaration in the file. The provided name must name a value of type
a1 -> ... -> an -> Prop
for some types a1, ..., an.
Example usage:
./result/bin/osl examples/sudoku.osl problemIsSolvable
To enter the dev shell, run:
nix develop
To get interactive compiler feedback, run:
ghcid --command "cabal repl"
To run the tests:
cabal test