Skip to content

EasyCrypt Circuit Based Reasoning Extension #752

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Gustavo2622 wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

EasyCrypt Circuit Based Reasoning Extension #752

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
bada5a0
Circuit reasoning functionality
Gustavo2622 Jan 20, 2026
1cbd638
First pass on new error reporting
Gustavo2622 Jan 22, 2026
60eb802
Added implicit type translation
Gustavo2622 Jan 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[submodule "libs/lospecs/tests/simde"]
path = libs/lospecs/tests/simde
url = git@github.com:simd-everywhere/simde.git
2 changes: 1 addition & 1 deletion config/tests.config
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

@strub strub Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What the point of adding examples that are directly excluded?

Copy link
Contributor Author

@Gustavo2622 Gustavo2622 Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No point, that line was changed in a commit that was removing examples dependent on JWord, so ideally we remove both


[test-mee-cbc]
okdirs = examples/MEE-CBC
Expand Down
7 changes: 6 additions & 1 deletion dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,9 @@
(dirs 3rdparty src etc theories examples assets scripts)
(env
Copy link
Member

@strub strub Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Move the OCaml flags from src so that we use the same flags everywhere.

(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)))
Expand Down
9 changes: 8 additions & 1 deletion dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))
))
9 changes: 8 additions & 1 deletion easycrypt.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"}
Expand All @@ -10,6 +11,12 @@ depends: [
"markdown"
"pcre2" {>= "8"}
"why3" {>= "1.8.0" & < "1.9"}
"ppx_deriving"
"ppx_deriving_yojson"
"hex"
Copy link
Member

@strub strub Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we really need these 4 last dependencies?

Copy link
Contributor Author

@Gustavo2622 Gustavo2622 Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Both ppx_derivings were for the printing of spec language ASTs, we can add a custom printing method to replace it. Hex was for the parsing of hexadecimal integers in the spec language, so that one seems wise to keep instead of rolling our own

"iter"
"cmdliner"
"progress"
"yojson"
"zarith" {>= "1.10"}
"odoc" {with-doc}
Expand Down
Loading
Loading