Target EasyCrypt release 2024.01

CHANGELOG.md

@@ -47,6 +47,9 @@
   when the `-g` command-line flag is given (off by default).
   ([PR #684](https://github.com/jasmin-lang/jasmin/pull/684)).
 
+- Extraction as EasyCrypt code targets version 2024.01
+  ([PR #690](https://github.com/jasmin-lang/jasmin/pull/690)).
+
 ## Bug fixes
 
 - Type-checking rejects invalid variants of primitive operators

compiler/src/toEC.ml

@@ -126,105 +126,86 @@ let leaks_lval pd = function
   | Lmem (_, x,e) -> leaks_e_rec pd [int_of_word pd (snd (add_ptr pd (gkvar x) e))] e
 
 (* FIXME: generate this list automatically *)
+(* Adapted from EasyCrypt source file src/ecLexer.mll *)
 let ec_keyword = 
- [ "exact"
- ; "assumption"
- ; "smt"
- ; "by"
- ; "reflexivity"
- ; "done"
- ; "admit"
- ; "axiom"
- ; "axiomatized"
- ; "lemma"
- ; "realize"
- ; "choice"
- ; "proof"
- ; "qed"
- ; "goal"
- ; "end"
- ; "import"
- ; "export"
- ; "include"
- ; "local"
- ; "declare"
- ; "hint"
- ; "nosmt"
- ; "module"
- ; "of"
- ; "const"
- ; "op"
- ; "pred"
- ; "require"
- ; "theory"
- ; "abstract"
- ; "section"
- ; "type"
- ; "class"
- ; "instance"
- ; "print"
- ; "search"
- ; "as"
- ; "Pr"
- ; "clone"
- ; "with"
- ; "rename"
- ; "prover"
- ; "timeout"
- ; "why3"
- ; "dump"
- ; "Top"
- ; "Self"
- ; "time"
- ; "undo"
- ; "debug"
- ; "pragma"
+ ["admit"
+ ; "admitted"
+
  ; "forall"
  ; "exists"
  ; "fun"
  ; "glob"
  ; "let"
  ; "in"
+ ; "for"
  ; "var"
  ; "proc"
  ; "if"
+ ; "is"
+ ; "match"
  ; "then"
  ; "else"
  ; "elif"
+ ; "match"
+ ; "for"
  ; "while"
  ; "assert"
  ; "return"
  ; "res"
  ; "equiv"
  ; "hoare"
+ ; "ehoare"
+ ; "choare"
+ ; "cost"
  ; "phoare"
  ; "islossless"
+ ; "async"
+
+ ; "try"
+ ; "first"
+ ; "last"
+ ; "do"
+ ; "strict"
+ ; "expect"
+
+ ; (* Lambda tactics *)
  ; "beta"
  ; "iota"
  ; "zeta"
+ ; "eta"
  ; "logic"
  ; "delta"
  ; "simplify"
+ ; "cbv"
  ; "congr"
+
+ ; (* Logic tactics *)
  ; "change"
  ; "split"
  ; "left"
  ; "right"
- ; "generalize"
  ; "case"
- ; "intros"
+
  ; "pose"
- ; "cut"
+ ; "gen"
  ; "have"
+ ; "suff"
  ; "elim"
+ ; "exlim"
+ ; "ecall"
  ; "clear"
+ ; "wlog"
+
+ ; (* Auto tactics *)
  ; "apply"
  ; "rewrite"
  ; "rwnormal"
  ; "subst"
  ; "progress"
  ; "trivial"
  ; "auto"
+
+ ; (* Other tactics *)
  ; "idtac"
  ; "move"
  ; "modpath"
@@ -233,6 +214,17 @@ let ec_keyword =
  ; "ring"
  ; "ringeq"
  ; "algebra"
+
+ ; "exact"
+ ; "assumption"
+ ; "smt"
+ ; "by"
+ ; "reflexivity"
+ ; "done"
+ ; "solve"
+
+ ; (* PHL: tactics *)
+ ; "replace"
  ; "transitivity"
  ; "symmetry"
  ; "seq"
@@ -246,28 +238,86 @@ let ec_keyword =
  ; "swap"
  ; "cfold"
  ; "rnd"
+ ; "rndsem"
  ; "pr_bounded"
  ; "bypr"
  ; "byphoare"
+ ; "byehoare"
  ; "byequiv"
+ ; "byupto"
  ; "fel"
+
  ; "conseq"
  ; "exfalso"
  ; "inline"
+ ; "outline"
+ ; "interleave"
  ; "alias"
+ ; "weakmem"
  ; "fission"
  ; "fusion"
  ; "unroll"
  ; "splitwhile"
  ; "kill"
  ; "eager"
- ; "try"
- ; "first"
- ; "last"
- ; "do"
- ; "strict"
- ; "expect"
- ; "interleave" ]
+
+ ; "axiom"
+ ; "schema"
+ ; "axiomatized"
+ ; "lemma"
+ ; "realize"
+ ; "proof"
+ ; "qed"
+ ; "abort"
+ ; "goal"
+ ; "end"
+ ; "from"
+ ; "import"
+ ; "export"
+ ; "include"
+ ; "local"
+ ; "declare"
+ ; "hint"
+ ; "nosmt"
+ ; "module"
+ ; "of"
+ ; "const"
+ ; "op"
+ ; "pred"
+ ; "inductive"
+ ; "notation"
+ ; "abbrev"
+ ; "require"
+ ; "theory"
+ ; "abstract"
+ ; "section"
+ ; "type"
+ ; "class"
+ ; "instance"
+ ; "instantiate"
+ ; "print"
+ ; "search"
+ ; "locate"
+ ; "as"
+ ; "Pr"
+ ; "clone"
+ ; "with"
+ ; "rename"
+ ; "prover"
+ ; "timeout"
+ ; "why3"
+ ; "dump"
+ ; "remove"
+ ; "exit"
+
+ ; "fail"
+ ; "time"
+ ; "undo"
+ ; "debug"
+ ; "pragma"
+
+ ; "Top"
+ ; "Self" ]
 
 let syscall_mod_arg = "SC"
 let syscall_mod_sig = "Syscall_t"

scripts/easycrypt.nix

@@ -17,13 +17,13 @@ with {
   };
 
   "release" = rec {
-    version = "2023.09";
+    version = "2024.01";
     rev = "r${version}";
     src = fetchFromGitHub {
       owner = "easycrypt";
       repo = "easycrypt";
       inherit rev;
-      hash = "sha256-9xavU9jRisZekPqC87EyiLXtZCGu/9QeGzq6BJGt1+Y=";
+      hash = "sha256-UYDoVMi5TtYxgPq5nkp/oRtcMcHl2p7KAG8ptvuOL5U=";
     };
   };