Getting started with jasmin


Install Jasmin and EasyCrypt (via OPAM)

sudo apt install opam cvc4 pkg-config libgmp-dev libpcre3-dev zlib1g-dev libmpfr-dev libppl-dev autoconf python3-distutils
opam init -c ocaml-base-compiler.4.12.0
eval $(opam env)
git clone https://github.com/jasmin-lang/jasmin.git
opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
opam pin -yn add jasmin https://github.com/jasmin-lang/jasmin.git
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin -yn add coq-mathcomp-word https://github.com/jasmin-lang/coqword.git
opam install alt-ergo.2.4.1 z3.4.11.0
opam install easycrypt
easycrypt why3config
opam install --deps-only jasmin
cd jasmin/compiler
make CIL
make
echo -e "[general]\nidirs=Jasmin:~/jasmin/eclib" > ~/.config/easycrypt/easycrypt.conf

A first example

main.c
addvec.jazz
Makefile


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 and examples