EasyCrypt Circuit Based Reasoning Extension #752

Gustavo2622 · 2025-03-18T14:27:19Z

Adds circuit based reasoning to EasyCrypt in the form of a module for converting EC constructs into circuits and reasoning over said circuits.
Adds various tactics to use the added functionality in proofs.
Depends on external SMT solver BitWutzla and on external circuit library Lospecs.

strub · 2026-01-20T12:56:51Z

easycrypt.opam

  "why3" {>= "1.8.0" & < "1.9"}
+  "ppx_deriving"
+  "ppx_deriving_yojson"
+  "hex"


Do we really need these 4 last dependencies?

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

strub · 2026-01-20T12:57:51Z

dune

@@ -1,4 +1,9 @@
-(dirs 3rdparty src etc theories examples assets scripts)
+(env


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

strub · 2026-01-20T12:58:05Z

config/tests.config

 [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


What the point of adding examples that are directly excluded?

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

strub · 2026-01-20T12:59:10Z

flake.nix

@@ -4,22 +4,23 @@



Why this file is modified at all?

These are change I made locally to make it actually work, it should not be part of this PR (but it is rather useful, so we can think about if we want to propagate some version of them)

strub · 2026-01-20T13:04:32Z

src/ecCircuits.ml

+    in
+    doit {level = 0; subst = EcSubst.empty} f
+
+  (* FIXME: Check that this does not incur false positives *)


Solve FIXME

strub · 2026-01-20T13:14:58Z

src/ecCoreFol.mli

 val f_pr   : memory -> xpath -> form -> ss_inv -> form

+(* FIXME: Check this V *)
+(* FIXME CIRCUIT PR: do we want to keep this? *)


strub · 2026-01-20T13:15:03Z

src/ecCoreFol.mli

+val ty_chunk   : ty -> ty
+val ty_all     : ty -> ty
+
+(* FIXME CIRCUIT PR: if keeping, maybe change names *)


strub · 2026-01-20T13:15:29Z

src/ecDecl.ml

+  ; size   : binding_size
+  ; theory : EcPath.path }
+
+type bv_opkind = [


Should we use a non-variant-polymorphic datatype?

Non-polymorphic variant?

strub · 2026-01-20T13:16:22Z

src/ecEnv.ml

  sp_params : int * (EcIdent.t * module_type) list;
 }

-


This file as a lot of modifications that are not related to bdep. Problem with merge?

Might be, but there was a reordering of the file contents needed by bdep, so that might be confusing the diff (or might have confused the merge algo)

strub · 2026-01-20T13:16:45Z

src/ecHiTacticals.ml

  FApi.t_try (process1_core ttenv t) tc

+(* -------------------------------------------------------------------- *)
+(* FIXME: Maybe move the extens tactic to this file as well? *)


Was creating a dependency loop when I first tried to put it there, but might have been because of some debugging instructions, we can move before the merge

…rcuit test

Gustavo2622 · 2026-02-10T12:22:53Z

src/phl/ecPhlBDep.ml

+  EcEnv.notify ~immediate:true env `Info "[W] %s, took %f s@." msg (new_t -. t);
+  new_t
+
+(* FIXME: move? V *)


Do we want this here or should it be moved?

Gustavo2622 · 2026-02-10T12:23:30Z

src/phl/ecPhlBDep.ml

+    end
+
+let t_bdep_simplify (tc: tcenv1) =
+  let time (env: env) (t: float) (msg: string) : float =


Do we want to keep this timing information?

Gustavo2622 · 2026-02-10T12:28:23Z

src/ecCircuits.ml

+        Why3.Hashcons.combine (doit st tp) i 
+      | FhoareF _hF -> 
+          assert false
+(*      FIXME: do we want this case and the one below?


Do we want to handle this?

Gustavo2622 · 2026-02-10T12:29:34Z

src/ecCircuits.ml

+    end
+    | Fapp (f, fs) -> 
+    (* TODO: Maybe add cache statistics? *)
+    (* TODO: Maybe cache all forms       *)


Do we want to cache all forms or just function applications?

Gustavo2622 · 2026-02-10T12:30:02Z

src/ecCircuits.ml

+    end
+
+    | Fquant (qnt, binds, f) -> 
+      (* FIXME Does this type conversion make sense? *)


Is this okay? (using gty_as_ty here)

Gustavo2622 · 2026-02-10T12:30:30Z

src/ecCircuits.ml

+      | Lforall 
+      | Llambda -> circ_lambda_oneshot st binds (fun st -> doit st f) (* FIXME: look at this interaction *)
+      | Lexists -> circ_error (CantConvertToCirc (`Quantif qnt))
+      (* FIXME: Do we want to handle existentials? *)


Do we want to do the usual Exists f => not Forall not f conversion here or just not handle it?

Gustavo2622 · 2026-02-10T12:30:43Z

src/ecCircuits.ml

+    | Fpvar   (pv, mem) -> 
+      let v = match pv with
+      | PVloc v -> v
+      (* FIXME: Should globals be supported? *)


Do we want to support globals for this merge?

Gustavo2622 · 2026-02-10T12:31:30Z

src/ecCircuits.ml

+    | FequivS  _
+    | FeagerF  _
+    | Fpr _ -> circ_error (CantConvertToCirc `Hoare) 
+    (* FIXME: do we want to allow conversion of hoare statements? 


Do we want to be able to generate a circuit from these things?

Gustavo2622 · 2026-02-10T12:32:19Z

src/ecCircuits.ml

+      false
+    end
+
+(* FIXME: add support for spec bindings for abstract/opaque operators 


Not used currently, but do we want this for the merge? Should not be too hard to do

Gustavo2622 · 2026-02-10T12:32:57Z

src/ecCircuits.ml

+  | CircError e ->
+    propagate_circ_error (`Instr inst) e
+
+(* FIXME: check if memory is the right one in calls to state *)


This is assuming a single memory for both sets of instructions, is this what we want?

Gustavo2622 · 2026-02-10T12:33:09Z

src/ecCircuits.ml

+
+  let st1 = close_circ_lambda st1 in 
+  let st2 = close_circ_lambda st2 in
+  (* FIXME: what was the intended behaviour for keep? *)


Gustavo2622 · 2026-02-10T12:35:55Z

src/ecCircuits.ml

+    circ_equiv circ1 circ2 
+  )
+
+(* FIXME: change memory -> memenv Why?            *)


Not needed, remove this (the comment)

Gustavo2622 · 2026-02-10T12:36:50Z

src/ecCircuits.ml

+  in check f
+
+
+(* Mli stuff needed: *)


Redo these exports

Gustavo2622 · 2026-02-10T12:37:11Z

src/ecCircuits.ml

+      EcEnv.notify env `Debug "Assigning %a to %a@." EcPrinting.(pp_form ppe) f EcIdent.pp_ident id;
+      begin try
+        update_state st id (circuit_of_form st hyps f)
+      (* FIXME PR: Should only catch circuit translation errors, hack *)


This is fixed, remove the comment

Gustavo2622 · 2026-02-10T12:37:22Z

src/ecCircuits.ml

+        EcEnv.notify env `Debug "Failed to translate hypothesis for var %s with error %a, skipping@." (tostring_internal id) (pp_circ_error ppe) e;
+        try 
+          open_circ_lambda st [(id, ctype_of_ty env t)]
+        (* FIXME PR: Should only catch circuit translation errors, hack *)


Fixed, remove the comment

Gustavo2622 · 2026-02-10T12:37:32Z

src/ecCircuits.ml

+      | {f_node=Fapp ({f_node = Fop (p, _); _}, [fv; {f_node = Fpvar (PVloc pv, m); _}])} when EcFol.op_kind p = Some `Eq ->
+        begin try
+          update_state_pv st m pv (circuit_of_form st hyps fv)
+        (* FIXME PR: Should only catch circuit translation errors, hack *)


Fixed, remove the comment

Gustavo2622 added enhancement library tactics labels Mar 18, 2025

Gustavo2622 requested a review from strub March 18, 2025 14:27

Gustavo2622 self-assigned this Mar 18, 2025

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch 3 times, most recently from 1b12249 to 66efdd7 Compare March 24, 2025 16:44

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from fdefb72 to 7ec289f Compare March 31, 2025 20:40

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch 2 times, most recently from aef3a2b to 01f21ac Compare August 8, 2025 11:15

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from 58c193f to 433cbb4 Compare August 19, 2025 08:24

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch 3 times, most recently from d7c187a to f433cb0 Compare September 8, 2025 14:24

Gustavo2622 changed the title ~~EasyCrypt Circuit Based Reasoning Extension~~ EasyCrypt Circuit Based Reasoning Extension (NOT UP TO DATE) Sep 14, 2025

Gustavo2622 changed the title ~~EasyCrypt Circuit Based Reasoning Extension (NOT UP TO DATE)~~ EasyCrypt Circuit Based Reasoning Extension Sep 14, 2025

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from 8288caf to 57a2e2b Compare September 17, 2025 15:19

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from 5b0ce21 to d299f15 Compare December 4, 2025 00:13

Circuit reasoning functionality

bada5a0

Gustavo2622 force-pushed the bdep_ecCircuitsRefactor branch from a828b25 to bada5a0 Compare January 20, 2026 12:47

strub requested changes Jan 20, 2026

View reviewed changes

Gustavo2622 added 8 commits January 22, 2026 20:34

First pass on new error reporting

1cbd638

Added implicit type translation

60eb802

Added duplicate checking for spec files and general cleanup

267854c

Merge remote-tracking branch 'origin/main' into bdep_ecCircuitsRefactor

60577ad

Killed warnings

973b124

Error and printing improvements

bc07042

Added fail case circuit tests

b116717

Minor error propagation fix

de7b295

Gustavo2622 added 5 commits February 6, 2026 16:08

Allow uninitialized program variable in circuit solve for hoare goals

4b94cb8

Changed alpha equiv hash to not compute form normal form and fixed ci…

f21c0cb

…rcuit test

Merge remote-tracking branch 'origin/main' into bdep_ecCircuitsRefactor

4f43916

Fixed merge problems + nits on error printing

9b11172

Fixing FIXMEs

08d87a3

Gustavo2622 commented Feb 10, 2026

View reviewed changes

Moved map reference to inside function scope in hash

fc94b6c

Gustavo2622 commented Feb 10, 2026

View reviewed changes

src/ecCircuits.ml

in check f

(* Mli stuff needed: *)

Copy link

Contributor Author

Gustavo2622 Feb 10, 2026

Choose a reason for hiding this comment

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

Redo these exports

Gustavo2622 commented Feb 10, 2026

View reviewed changes

		@@ -1,4 +1,9 @@
		(dirs 3rdparty src etc theories examples assets scripts)
		(env

EasyCrypt Circuit Based Reasoning Extension #752

Are you sure you want to change the base?

EasyCrypt Circuit Based Reasoning Extension #752

Conversation

Gustavo2622 commented Mar 18, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Gustavo2622 Feb 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Gustavo2622 Feb 10, 2026 •

edited

Loading