EasyCrypt Circuit Based Reasoning Extension

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "libs/lospecs/tests/simde"]
+	path = libs/lospecs/tests/simde
+	url = git@github.com:simd-everywhere/simde.git

config/tests.config

@@ -8,7 +8,7 @@ exclude = theories/prelude
 
 [test-examples]
 okdirs  = !examples
-exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomplete examples/to-port
+exclude = examples/MEE-CBC examples/exclude examples/old examples/old/list-ddh !examples/incomplete examples/to-port
 
 [test-mee-cbc]
 okdirs = examples/MEE-CBC

dune

@@ -1,4 +1,9 @@
-(dirs 3rdparty src etc theories examples assets scripts)
+(env
+ (dev     (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69))
+ (release (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69)
+          (ocamlopt_flags -O3 -unbox-closures)))
+
+(dirs 3rdparty src etc libs theories examples assets scripts)
 
 (install
   (section (site (easycrypt commands)))

dune-project

@@ -13,7 +13,8 @@
  (sites (lib theories) (libexec commands) (lib doc) (lib config))
  (depends
   (ocaml (>= 4.08.0))
-  (batteries (>= 3))
+  (batteries (>= 3.9))
+  bitwuzla
   (camlp-streams (>= 5))
   camlzip
   dune
@@ -22,6 +23,12 @@
   markdown
   (pcre2 (>= 8))
   (why3 (and (>= 1.8.0) (< 1.9)))
+  ppx_deriving
+  ppx_deriving_yojson
+  hex
+  iter
+  cmdliner
+  progress
   yojson
   (zarith (>= 1.10))
 ))

easycrypt.opam

@@ -1,7 +1,8 @@
 # This file is generated by dune, edit dune-project instead
 depends: [
   "ocaml" {>= "4.08.0"}
-  "batteries" {>= "3"}
+  "batteries" {>= "3.9"}
+  "bitwuzla"
   "camlp-streams" {>= "5"}
   "camlzip"
   "dune" {>= "3.13"}
@@ -10,6 +11,12 @@ depends: [
   "markdown"
   "pcre2" {>= "8"}
   "why3" {>= "1.8.0" & < "1.9"}
+  "ppx_deriving"
+  "ppx_deriving_yojson"
+  "hex"
+  "iter"
+  "cmdliner"
+  "progress"
   "yojson"
   "zarith" {>= "1.10"}
   "odoc" {with-doc}