Getting started with jasmin


Installing jasmin (via nix)

Installing nix
sudo install -d -m755 -o $(id -u) -g $(id -g) /nix
curl -L https://nixos.org/nix/install | sh

Follow instructions by the install script.

Installing jasmin
git clone https://github.com/jasmin-lang/jasmin.git
cd jasmin
git fetch -a
git checkout main
nix-channel --update
nix-shell
cd compiler
make CIL
make
make check
exit

A first example

main.c
addvec.jazz
Makefile

Installing EasyCrypt (on Debian Bullseye)

First install dependencies and SMT solvers used by EasyCrypt
sudo apt install ocaml-findlib ocamlbuild nix autoconf opam z3 cvc4

As Alt-Ergo in Debian is too old and not supported by EasyCrypt anymore, install via opam:

opam init
opam update
opam install alt-ergo
Install EasyCrypt
git clone https://github.com/EasyCrypt/easycrypt.git
cd easycrypt
git fetch -a
git checkout 1.0
nix-shell --command make
sudo env "PATH=$PATH" make install
nix-shell --command "easycrypt why3config" || true
Install ProofGeneral (for vi users)

First install emacs:

sudo apt install emacs

Create a file ~/.emacs with the following content:

(setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3")

;; Set up package.el to work with MELPA
(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
;; (package-refresh-contents)

;; Download Evil
(unless (package-installed-p 'evil)
(package-install 'evil))

;; Enable Evil
(require 'evil)
(evil-mode 1)
(evil-define-key 'normal proof-mode-map (kbd "C-c RET") 'proof-goto-point)
(setq evil-want-abbrev-expand-on-insert-exit nil)

(require 'evil-tabs)
(global-evil-tabs-mode t)

(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(package-selected-packages '(proof-general evil-tabs evil)))
(custom-set-faces
;; custom-set-faces was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
)
Now start emacs and inside emacs run
:package-refresh-contents
:package-install <ENTER>
proof-general

Further resources